Skip to content

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

Robbert Krebbers requested to merge robbert/list_find into master

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.

Merge request reports