Lemmas for `list_find` in combination with `app` and `insert`.

This MR proposes an alternative to the lemmas for list_find by @msammler in #131 (closed) (but that he removed later).

All lemmas are stated using a bi-implication, and they are strong enough to prove @msammler's original lemmas:

Lemma list_find_insert_Some_ne1 l i i' x x':
  list_find P l = Some (i', x') → ¬ P x → i ≠ i' →
  list_find P (<[i:=x]> l) = Some (i', x').
Proof.
  rewrite list_find_insert_Some, !list_find_Some.
  destruct (decide (i < i')); naive_solver eauto with lia.
Qed.

Lemma list_find_insert_Some_ne_change2 l i i' x x':
  list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x' → i < i' →
  list_find P l = Some (i, x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver eauto with lia. Qed.

Lemma list_find_insert_Some_ne_same2 l i i' x x' x'':
  list_find P (<[i:=x]>l) = Some (i', x') →
  ¬ P x → l !! i = Some x'' → (i < i' → ¬ P x'') →
  list_find P l = Some (i', x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver. Qed.

Lemma list_find_insert_Some_ne2 l i i' x x' x'':
  list_find P (<[i:=x]>l) = Some (i', x') → ¬ P x → l !! i = Some x'' → (x'' = x' ∨ ¬ P x'') →
  ∃ i'', list_find P l = Some (i'', x').
Proof. rewrite list_find_insert_Some. repeat setoid_rewrite list_find_Some. naive_solver eauto with lia. Qed.

I very much dislike the statement of list_find_insert_Some, but I cannot come up with anything better that is true.

I don't like the last disjunct of list_find_insert_Some since it does not use list_find. So I played around with it a bit more and was able to prove the following version, which I think is easier to understand than the version you currently have:

  Lemma list_find_insert_Some l i j x y :
    list_find P (<[i:=x]> l) = Some (j,y) ↔
      (j < i ∧ list_find P l = Some (j,y)) ∨
      (i = j ∧ x = y ∧ j < length l ∧ P x ∧ ∀ k z, l !! k = Some z → k < i → ¬P z) ∨
      (i < j ∧ ¬P x ∧ ((list_find P l = Some (j,y) ∧ ∀ z, l !! i = Some z → ¬P z) ∨ (∃ z, list_find P l = Some (i,z) ∧ P z ∧ list_find P (drop (S i) l) = Some (j - S i, y)))).
  Proof.

naive_solver is still able to solve the other lemmas with this version. What do you think?

The proof is maybe a bit worse:

  Lemma list_find_insert_Some l i j x y :
    list_find P (<[i:=x]> l) = Some (j,y) ↔
      (j < i ∧ list_find P l = Some (j,y)) ∨
      (i = j ∧ x = y ∧ j < length l ∧ P x ∧ ∀ k z, l !! k = Some z → k < i → ¬P z) ∨
      (i < j ∧ ¬P x ∧ ((list_find P l = Some (j,y) ∧ ∀ z, l !! i = Some z → ¬P z) ∨ (∃ z, list_find P l = Some (i,z) ∧ P z ∧ list_find P (drop (S i) l) = Some (j - S i, y)))).
  Proof.
    split.
     - intros ([(->&->&?)|[? Hl]]%list_lookup_insert_Some&?&Hleast)%list_find_Some.
       { right; left. split_and!; [done..|]. intros k z ??.
         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
       assert (j < i ∨ i < j) as [?|?] by lia.
       { left. rewrite list_find_Some. split_and!; [by auto..|]. intros k z ??.
         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. }
       right; right. assert (j < length l) by eauto using lookup_lt_Some.
       destruct (lookup_lt_is_Some_2 l i) as [z ?]; [lia|].
       split_and!; [done |..].
       { apply (Hleast i); [|done]. by rewrite list_lookup_insert by lia. }
       destruct (decide (P z)).
       + right. exists z. split_and!; [|done|]; apply list_find_Some.
         * split_and!; [done..| ].
           intros k z' ??. apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia.
         * rewrite lookup_drop. split_and!;[|done|]. { rewrite <-Hl. f_equal. lia. }
           setoid_rewrite lookup_drop. intros k ???.
           apply (Hleast (S i + k)); [|lia]. by rewrite list_lookup_insert_ne by lia.
       + left. split_and!; [|naive_solver].
         apply list_find_Some. split_and!; [by auto..|]. intros k z' ??.
         destruct (decide (k = i)) as [->|]; [naive_solver|].
         apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia.
     - intros [[? Hl]|[(->&->&?&?&Hleast)|(?&?&[[Hl Hnot]|(z&Hl&?&Hd)])]];
         apply list_find_Some.
       + apply list_find_Some in Hl as (?&?&Hleast).
         rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
       + rewrite list_lookup_insert by done. split_and!; [by auto..|].
         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
       + apply list_find_Some in Hl as (?&?&Hleast).
         rewrite list_lookup_insert_ne by lia. split_and!; [done..|].
         intros k z [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia.
       + apply list_find_Some in Hl as (?&?&Hleast).
         apply list_find_Some in Hd as (Hd&?&Hleast2).
         rewrite list_lookup_insert_ne by lia. split_and!; [|done..|].
         { rewrite <-Hd, lookup_drop. f_equal. lia. }
         intros k z' [(->&->&?)|[? Hk]]%list_lookup_insert_Some ?; eauto with lia.
         destruct (decide (k < i)).
         * apply (Hleast k); naive_solver lia.
         * apply (Hleast2 (k - S i));[|lia]. rewrite lookup_drop, <-Hk. f_equal. lia.
  Qed.

@msammler told me in person that he does not need any of this list_find stuff anymore.

I think the lemmas about list_find and app in this MR make a lot of sense and should be merged.

The lemma list_find_insert_Some is not beautiful, but it's an ↔ so the RHS precisely defines the LHS. It appears to be the best we can think of, so unless there is opposition, I propose to merge that too.

I think the lemmas about list_find and app in this MR make a lot of sense and should be merged.

Agreed.

The lemma list_find_insert_Some is not beautiful, but it's an ↔ so the RHS precisely defines the LHS. It appears to be the best we can think of, so unless there is opposition, I propose to merge that too.

The statement could be made easier to parse by adding some comments for which cases, intuitively, these 4 disjuncts represent. Also, should there be a matching list_find_insert_None?

added 1 commit

• d12b94f8 - Lemmas for `list_find` in combination with `app` and `insert`.

Compare with previous version

added 1 commit

• 5bfe306d - Lemmas for `list_find` in combination with `app` and `insert`.

Compare with previous version

added 1 commit

• f326c081 - Lemmas for `list_find` in combination with `app` and `insert`.

Compare with previous version

resolved all threads

Merging this MR. Thanks all.

Never mind, will first add a changelog entry as this MR changes an existing lemma.

added 60 commits

• f326c081...199c984b - 57 commits from branch master
• 278a845b - Make `list_find_Some` more `apply` friendly.
• 4680e914 - Lemmas for `list_find` in combination with `app` and `insert`.
• e6b17ca4 - CHANGELOG entry.

Compare with previous version

@iris-users This is a breaking change, it changes the lemma list_find_Some.

mentioned in commit befe38d4

merged