Prove function rules.

theories/collections.v

@@ -178,6 +178,7 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
     let H1 := fresh H in let H2 := fresh H in apply elem_of_guard in H;
     destruct H as [H1 H2]; go H2
   | _ ∈ of_option _ => apply elem_of_of_option in H
+  | _ ∈ of_list _ => apply elem_of_of_list in H
   | _ => idtac
   end in go H.
 Tactic Notation "decompose_elem_of" :=
@@ -221,6 +222,8 @@ Ltac unfold_elem_of :=
     | context [ _ ∈ _ ≫= _ ] => setoid_rewrite elem_of_bind in H
     | context [ _ ∈ mjoin _ ] => setoid_rewrite elem_of_join in H
     | context [ _ ∈ guard _; _ ] => setoid_rewrite elem_of_guard in H
+    | context [ _ ∈ of_option _ ] => setoid_rewrite elem_of_of_option in H
+    | context [ _ ∈ of_list _ ] => setoid_rewrite elem_of_of_list in H
     end);
   repeat match goal with
   | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq
@@ -239,6 +242,8 @@ Ltac unfold_elem_of :=
   | |- context [ _ ∈ _ ≫= _ ] => setoid_rewrite elem_of_bind
   | |- context [ _ ∈ mjoin _ ] => setoid_rewrite elem_of_join
   | |- context [ _ ∈ guard _; _ ] => setoid_rewrite elem_of_guard
+  | |- context [ _ ∈ of_option _ ] => setoid_rewrite elem_of_of_option
+  | |- context [ _ ∈ of_list _ ] => setoid_rewrite elem_of_of_list
   end.
 
 (** The tactic [solve_elem_of tac] composes the above tactic with [intuition].
@@ -485,6 +490,9 @@ Section fresh.
     rewrite <-Forall_forall.
     intros [Hxs Hxs']. induction Hxs; decompose_Forall_hyps; constructor; auto.
   Qed.
+  Lemma Forall_fresh_subseteq X Y xs :
+    Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
+  Proof. rewrite !Forall_fresh_alt; esolve_elem_of. Qed.
 
   Lemma fresh_list_length n X : length (fresh_list n X) = n.
   Proof. revert X. induction n; simpl; auto. Qed.

theories/fin_maps.v

@@ -240,10 +240,12 @@ Proof.
   by destruct (decide (i = j)) as [->|?];
     rewrite ?lookup_alter, ?fmap_None, ?lookup_alter_ne.
 Qed.
-Lemma alter_None {A} (f : A → A) m i : m !! i = None → alter f i m = m.
+Lemma alter_id {A} (f : A → A) m i :
+  (∀ x, m !! i = Some x → f x = x) → alter f i m = m.
 Proof.
-  intros Hi. apply map_eq. intros j. by destruct (decide (i = j)) as [->|?];
-    rewrite ?lookup_alter, ?Hi, ?lookup_alter_ne.
+  intros Hi; apply map_eq; intros j; destruct (decide (i = j)) as [->|?].
+  { rewrite lookup_alter; destruct (m !! j); f_equal'; auto. }
+  by rewrite lookup_alter_ne by done.
 Qed.
 
 (** ** Properties of the [delete] operation *)
@@ -340,7 +342,7 @@ Proof.
   destruct (decide (i = j)) as [->|];
     rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
 Qed.
-Lemma insert_lookup {A} (m : M A) i x : m !! i = Some x → <[i:=x]>m = m.
+Lemma insert_id {A} (m : M A) i x : m !! i = Some x → <[i:=x]>m = m.
 Proof.
   intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|];
     by rewrite ?lookup_insert, ?lookup_insert_ne by done.

theories/list.v

@@ -172,6 +172,15 @@ Definition zipped_map {A B} (f : list A → list A → A → B) :
   list A → list A → list B := fix go l k :=
   match k with [] => [] | x :: k => f l k x :: go (x :: l) k end.
 
+Definition imap2_go {A B C} (f : nat → A → B → C) :
+    nat → list A → list B → list C:=
+  fix go (n : nat) (l : list A) (k : list B) :=
+  match l, k with
+  | [], _ |_, [] => [] | x :: l, y :: k => f n x y :: go (S n) l k
+  end.
+Definition imap2 {A B C} (f : nat → A → B → C) :
+  list A → list B → list C := imap2_go f 0.
+
 Inductive zipped_Forall {A} (P : list A → list A → A → Prop) :
     list A → list A → Prop :=
   | zipped_Forall_nil l : zipped_Forall P l []