proposition: 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, i < j ∧ ¬P x ∧ P y ∧ P z ∧ l !! i = Some z ∧ l !! j = Some y ∧ ∀ k z, l !! k = Some z → k ≠ i → k < j → ¬P z).
proof: Proof. split. - intros ([(->&->&?)|[??]]%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|]. destruct (decide (P z)). { right. exists z. split_and!; [done| |done..|]. + apply (Hleast i); [|done]. by rewrite list_lookup_insert by lia. + intros k z' ???. apply (Hleast k); [|lia]. by rewrite list_lookup_insert_ne by lia. } left. split_and!; [done|..|naive_solver]. + apply (Hleast i); [|done]. by rewrite list_lookup_insert by lia. + 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&?&?&?&?&?&?&?Hleast)]]]; 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. + rewrite list_lookup_insert_ne by lia. split_and!; [done..|]. intros k z' [(->&->&?)|[??]]%list_lookup_insert_Some; eauto with lia. Qed.
imports: stdpp(options)