From b2109c25442e833f2bb398259a395a3ef0cb81ca Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 7 Feb 2015 01:03:55 +0100
Subject: [PATCH] Support function pointers and use a state monad in the
 frontend.

Important changes in the core semantics:
* Types extended with function types. Since function types are a special kind
  of pointer types, types now have an additional mutual part called "ptr_type".
* Pointers extended with function pointers. Theses are just names that refer
  to an actual function in the function environment.
* Typing environments extended to assign argument and return types to function
  names. Before we used a separate environment for these, but since the
  argument and return types are already needed to type function pointers, this
  environment would appear in pretty much every typing judgment.

As a side-effect, the frontend has been rewritten entirely. The important
changes are:

* Type checking of expressions is more involved: there is a special kind of
  expression type corresponding to a function designator.
* To handle things like block scoped extern function, more state-fullness was
  needed. To prepare for future extensions, the entire frontend now uses a
  state monad.
---
 theories/base.v        |   2 +
 theories/collections.v |  17 ++--
 theories/error.v       | 191 +++++++++++++++++++++++++----------------
 theories/fin_maps.v    |  84 +++++++++++++-----
 theories/finite.v      |  31 ++++---
 theories/hashset.v     |  55 ++++++++----
 theories/list.v        |  30 +++----
 theories/tactics.v     |  34 --------
 8 files changed, 257 insertions(+), 187 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 8dbbfa89..88ad2357 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -844,6 +844,8 @@ Instance idem_propholds {A} (R : relation A) f :
   Idempotent R f → ∀ x, PropHolds (R (f x x) x).
 Proof. red. trivial. Qed.
 
+Instance: @PreOrder A (=).
+Proof. split; repeat intro; congruence. Qed.
 Lemma injective_iff {A B} {R : relation A} {S : relation B} (f : A → B)
   `{!Injective R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y.
 Proof. firstorder. Qed.
diff --git a/theories/collections.v b/theories/collections.v
index d76fe388..c3ef61df 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -254,7 +254,7 @@ Section collection.
   Proof. esolve_elem_of. Qed.
   Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
   Proof. esolve_elem_of. Qed.
-  Lemma empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅.
+  Lemma subseteq_empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅.
   Proof. esolve_elem_of. Qed.
   Lemma difference_diag X : X ∖ X ≡ ∅.
   Proof. esolve_elem_of. Qed.
@@ -269,8 +269,8 @@ Section collection.
     Proof. unfold_leibniz. apply intersection_singletons. Qed.
     Lemma difference_twice_L X Y : (X ∖ Y) ∖ Y = X ∖ Y.
     Proof. unfold_leibniz. apply difference_twice. Qed.
-    Lemma empty_difference_L X Y : X ⊆ Y → X ∖ Y = ∅.
-    Proof. unfold_leibniz. apply empty_difference. Qed.
+    Lemma subseteq_empty_difference_L X Y : X ⊆ Y → X ∖ Y = ∅.
+    Proof. unfold_leibniz. apply subseteq_empty_difference. Qed.
     Lemma difference_diag_L X : X ∖ X = ∅.
     Proof. unfold_leibniz. apply difference_diag. Qed.
     Lemma difference_union_distr_l_L X Y Z : (X ∪ Y) ∖ Z = X ∖ Z ∪ Y ∖ Z.
@@ -296,12 +296,15 @@ Section collection.
       intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
       destruct (decide (x ∈ X)); esolve_elem_of.
     Qed.
-
+    Lemma empty_difference_subseteq X Y : X ∖ Y ≡ ∅ → X ⊆ Y.
+    Proof. intros ? x ?; apply dec_stable; esolve_elem_of. Qed.
     Context `{!LeibnizEquiv C}.
     Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
     Proof. unfold_leibniz. apply union_difference. Qed.
     Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠ ∅.
     Proof. unfold_leibniz. apply non_empty_difference. Qed.
+    Lemma empty_difference_subseteq_L X Y : X ∖ Y = ∅ → X ⊆ Y.
+    Proof. unfold_leibniz. apply empty_difference_subseteq. Qed.
   End dec.
 End collection.
 
@@ -432,16 +435,14 @@ Section fresh.
 
   Definition fresh_sig (X : C) : { x : A | x ∉ X } :=
     exist (∉ X) (fresh X) (is_fresh X).
-
-  Global Instance fresh_proper: Proper ((≡) ==> (=)) fresh.
-  Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
-
   Fixpoint fresh_list (n : nat) (X : C) : list A :=
     match n with
     | 0 => []
     | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
     end.
 
+  Global Instance fresh_proper: Proper ((≡) ==> (=)) fresh.
+  Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
   Global Instance fresh_list_proper: Proper ((=) ==> (≡) ==> (=)) fresh_list.
   Proof.
     intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal'; [by rewrite E|].
diff --git a/theories/error.v b/theories/error.v
index f1a87285..05c36b7b 100644
--- a/theories/error.v
+++ b/theories/error.v
@@ -2,91 +2,134 @@
 (* This file is distributed under the terms of the BSD license. *)
 Require Export list.
 
-Instance error_ret {E} : MRet (sum E) := λ A, inr.
-Instance error_bind {E} : MBind (sum E) := λ A B f x,
-  match x with inr a => f a | inl e => inl e end.
-Instance error_fmap {E} : FMap (sum E) := λ A B f x,
-  match x with inr a => inr (f a) | inl e => inl e end.
+Definition error (S E A : Type) : Type := S → E + (A * S).
 
-Definition error_guard {E} P {dec : Decision P} {A}
-    (e : E) (f : P → E + A) : E + A :=
-  match decide P with left H => f H | right _ => inl e end.
+Definition error_eval {S E A} (x : error S E A) (s : S) : E + A :=
+  match x s with inl e => inl e | inr (a,_) => inr a end.
+
+Instance error_ret {S E} : MRet (error S E) := λ A x s, inr (x,s).
+Instance error_bind {S E} : MBind (error S E) := λ A B f x s,
+  match x s with
+  | inr (a,s') => f a s'
+  | inl e => inl e
+  end.
+Instance error_fmap {S E} : FMap (error S E) := λ A B f x s,
+  match x s with
+  | inr (a,s') => inr (f a,s')
+  | inl e => inl e
+  end.
+Definition fail {S E A} (e : E) : error S E A := λ s, inl e.
+
+Definition modify {S E} (f : S → S) : error S E () := λ s, inr ((), f s).
+Definition gets {S E A} (f : S → A) : error S E A := λ s, inr (f s, s).
+
+Definition error_guard {E} P {dec : Decision P} {S A}
+    (e : E) (f : P → error S E A) : error S E A :=
+  match decide P with left H => f H | right _ => fail e end.
 Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o))
   (at level 65, next at level 35, only parsing, right associativity) : C_scope.
-Definition error_of_option {A E} (x : option A) (e : E) : sum E A :=
-  match x with Some a => inr a | None => inl e end.
+Definition error_of_option {S A E} (x : option A) (e : E) : error S E A :=
+  match x with Some a => mret a | None => fail e end.
 
-Lemma bind_inr {A B E} (f : A → E + B) x b :
-  x ≫= f = inr b ↔ ∃ a, x = inr a ∧ f a = inr b.
-Proof. destruct x; naive_solver. Qed.
-Lemma fmap_inr {A B E} (f : A → B) (x : E + A) b :
-  f <$> x = inr b ↔ ∃ a, x = inr a ∧ f a = b.
-Proof. destruct x; naive_solver. Qed.
-Lemma error_of_option_inr {A E} (o : option A) (e : E) a :
-  error_of_option o e = inr a ↔ o = Some a.
-Proof. destruct o; naive_solver. Qed.
+Lemma error_bind_ret {S E A B} (f : A → error S E B) s s'' x b :
+  (x ≫= f) s = mret b s'' ↔ ∃ a s', x s = mret a s' ∧ f a s' = mret b s''.
+Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
+Lemma error_fmap_ret {S E A B} (f : A → B) s s' (x : error S E A) b :
+  (f <$> x) s = mret b s' ↔ ∃ a, x s = mret a s' ∧ b = f a.
+Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
+Lemma error_of_option_ret {S E A} (s s' : S) (o : option A) (e : E) a :
+  error_of_option o e s = mret a s' ↔ o = Some a ∧ s = s'.
+Proof. compute; destruct o; naive_solver. Qed.
+Lemma error_guard_ret {S E A} `{dec : Decision P} s s' (x : error S E A) e a :
+  (guard P with e ; x) s = mret a s' ↔ P ∧ x s = mret a s'.
+Proof. compute; destruct dec; naive_solver. Qed.
+Lemma error_fmap_bind {S E A B C} (f : A → B) (g : B → error S E C) x s :
+  ((f <$> x) ≫= g) s = (x ≫= g ∘ f) s.
+Proof. by compute; destruct (x s) as [|[??]]. Qed.
 
-Tactic Notation "case_error_guard" "as" ident(Hx) :=
-  match goal with
-  | H : context C [@error_guard _ ?P ?dec _ ?e ?x] |- _ =>
-    let X := context C [ match dec with left H => x H | _ => inl e end ] in
-    change X in H; destruct_decide dec as Hx
-  | |- context C [@error_guard _ ?P ?dec _ ?e ?x] =>
-    let X := context C [ match dec with left H => x H | _ => inl e end ] in
-    change X; destruct_decide dec as Hx
-  end.
-Tactic Notation "case_error_guard" :=
-  let H := fresh in case_error_guard as H.
+Lemma error_associative {S E A B C} (f : A → error S E B) (g : B → error S E C) x s :
+  ((x ≫= f) ≫= g) s = (a ← x; f a ≫= g) s.
+Proof. by compute; destruct (x s) as [|[??]]. Qed.
+Lemma error_of_option_bind {S E A B} (f : A → option B) o e :
+  error_of_option (S := S) (E:=E) (o ≫= f) e
+  = a ← error_of_option o e; error_of_option (f a) e.
+Proof. by destruct o. Qed.
+
+Lemma error_gets_spec {S E A} (g : S → A) s : gets (E:=E) g s = mret (g s) s.
+Proof. done. Qed.
+Lemma error_modify_spec {S E} (g : S → S) s : modify (E:=E) g s = mret () (g s).
+Proof. done. Qed.
+Lemma error_left_gets {S E A B} (g : S → A) (f : A → error S E B) s :
+  (gets (E:=E) g ≫= f) s = f (g s) s.
+Proof. done. Qed.
+Lemma error_left_modify {S E B} (g : S → S) (f : unit → error S E B) s :
+  (modify (E:=E) g ≫= f) s = f () (g s).
+Proof. done. Qed.
+Lemma error_left_id {S E A B} (a : A) (f : A → error S E B) :
+  (mret a ≫= f) = f a.
+Proof. done. Qed.
 
+Ltac generalize_errors :=
+  csimpl;
+  let gen_error e :=
+    try (is_var e; fail 1); generalize e;
+    let x := fresh "err" in intros x in
+  repeat match goal with
+  | |- appcontext[ fail ?e ] => gen_error e
+  | |- appcontext[ error_guard _ ?e ] => gen_error e
+  | |- appcontext[ error_of_option _ ?e ] => gen_error e
+  end.
 Tactic Notation "simplify_error_equality" :=
   repeat match goal with
+  | H : context [ gets _ _ _ ] |- _ => rewrite error_gets_spec in H
+  | H : context [ modify _ _ _ ] |- _ => rewrite error_modify_spec in H
+  | H : (mret (M:=error _ _) _ ≫= _) _ = _ |- _ => rewrite error_left_id in H
+  | H : (gets _ ≫= _) _ = _ |- _ => rewrite error_left_gets in H
+  | H : (modify _ ≫= _) _ = _ |- _ => rewrite error_left_modify in H
+  | H : error_guard _ _ _ _ = _ |- _ => apply error_guard_ret in H; destruct H
   | _ => progress simplify_equality'
-  | H : appcontext [@mret (sum ?E) _ ?A] |- _ =>
-     change (@mret (sum E) _ A) with (@inr E A) in H
-  | |- appcontext [@mret (sum ?E) _ ?A] => change (@mret _ _ A) with (@inr E A)
-  | _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x
-  | _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
-  | _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
-  | _ : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
-  | H : error_of_option ?o ?e = ?x |- _ => apply error_of_option_inr in H
-  | H : mbind (M:=sum _) ?f ?o = ?x |- _ =>
-    apply bind_inr in H; destruct H as (?&?&?)
-  | H : fmap (M:=sum _) ?f ?o = ?x |- _ =>
-    apply fmap_inr in H; destruct H as (?&?&?)
-  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
+  | H : error_of_option _ _ _ = _ |- _ =>
+    apply error_of_option_ret in H; destruct H
+  | H : mbind (M:=error _ _) _ _ _ = _ |- _ =>
+    apply error_bind_ret in H; destruct H as (?&?&?&?)
+  | H : fmap (M:=error _ _) _ _ _ = _ |- _ =>
+    apply error_fmap_ret in H; destruct H as (?&?&?)
+  | H : mbind (M:=option) _ _ = _ |- _ =>
     apply bind_Some in H; destruct H as (?&?&?)
-  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
+  | H : fmap (M:=option) _ _ = _ |- _ =>
     apply fmap_Some in H; destruct H as (?&?&?)
+  | H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
   | _ => progress case_decide
-  | _ => progress case_error_guard
-  | _ => progress case_option_guard
   end.
 
-Section mapM.
-  Context {A B E : Type} (f : A → E + B).
-
-  Lemma error_mapM_ext (g : A → sum E B) l :
-    (∀ x, f x = g x) → mapM f l = mapM g l.
-  Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed.
-  Lemma error_Forall2_mapM_ext (g : A → E + B) l k :
-    Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k.
-  Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
-  Lemma error_Forall_mapM_ext (g : A → E + B) l :
-    Forall (λ x, f x = g x) l → mapM f l = mapM g l.
-  Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
-  Lemma mapM_inr_1 l k : mapM f l = inr k → Forall2 (λ x y, f x = inr y) l k.
-  Proof.
-    revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
-    * destruct (f x); simpl; [discriminate|]. by destruct (mapM f l).
-    * destruct (f x) eqn:?; intros; simplify_error_equality; auto.
-  Qed.
-  Lemma mapM_inr_2 l k : Forall2 (λ x y, f x = inr y) l k → mapM f l = inr k.
-  Proof.
-    induction 1 as [|???? Hf ? IH]; simpl; [done |].
-    rewrite Hf. simpl. by rewrite IH.
-  Qed.
-  Lemma mapM_inr l k : mapM f l = inr k ↔ Forall2 (λ x y, f x = inr y) l k.
-  Proof. split; auto using mapM_inr_1, mapM_inr_2. Qed.
-  Lemma error_mapM_length l k : mapM f l = inr k → length l = length k.
-  Proof. intros. by eapply Forall2_length, mapM_inr_1. Qed.
-End mapM.
+Tactic Notation "error_proceed" :=
+  repeat match goal with
+  | H : context [ gets _ _ ] |- _ => rewrite error_gets_spec in H
+  | H : context [ modify _ _ ] |- _ => rewrite error_modify_spec in H
+  | H : context [ error_of_option _ _ ] |- _ => rewrite error_of_option_bind in H
+  | H : (mret (M:= _ _) _ ≫= _) _ = _ |- _ => rewrite error_left_id in H
+  | H : (gets _ ≫= _) _ = _ |- _ => rewrite error_left_gets in H
+  | H : (modify _ ≫= _) _ = _ |- _ => rewrite error_left_modify in H
+  | H : ((_ <$> _) ≫= _) _ = _ |- _ => rewrite error_fmap_bind in H
+  | H : ((_ ≫= _) ≫= _) _ = _ |- _ => rewrite error_associative in H
+  | H : (error_guard _ _ _) _ = _ |- _ =>
+     let H' := fresh in apply error_guard_ret in H; destruct H as [H' H]
+  | _ => progress simplify_equality'
+  | H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
+  end.
+Tactic Notation "error_proceed"
+    simple_intropattern(a) "as" simple_intropattern(s) :=
+  error_proceed;
+  lazymatch goal with
+  | H : (error_of_option ?o _ ≫= _) _ = _ |- _ => destruct o as [a|] eqn:?
+  | H : error_of_option ?o _ _ = _ |- _ => destruct o as [a|] eqn:?
+  | H : (_ ≫= _) _ = _ |- _ => apply error_bind_ret in H; destruct H as (a&s&?&H)
+  | H : (_ <$> _) _ = _ |- _ => apply error_fmap_ret in H; destruct H as (a&?&?)
+  end;
+  error_proceed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 95365bc6..a3ae2432 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -84,14 +84,8 @@ Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
   | None, Some y => Q y
   | None, None => True
   end.
-Definition map_Forall3 `{∀ A, Lookup K A (M A)} {A B C}
-    (R : A → B → C → Prop) (m1 : M A) (m2 : M B) (m3 : M C): Prop := ∀ i,
-  match m1 !! i, m2 !! i, m3 !! i with
-  | Some x, Some y, Some z => R x y z
-  | None, None, None => True
-  | _, _, _ => False
-  end.
-
+Definition map_included `{∀ A, Lookup K A (M A)} {A}
+  (R : relation A) : relation (M A) := map_Forall2 R (λ _, False) (λ _, True).
 Instance map_disjoint `{∀ A, Lookup K A (M A)} {A} : Disjoint (M A) :=
   map_Forall2 (λ _ _, False) (λ _, True) (λ _, True).
 Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
@@ -127,13 +121,17 @@ Proof.
   intros A m. rewrite !map_subseteq_spec.
   intros i x. by rewrite lookup_empty.
 Qed.
+Global Instance: ∀ {A} (R : relation A), PreOrder R → PreOrder (map_included R).
+Proof.
+  split; [intros m i; by destruct (m !! i)|].
+  intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
+  destruct (m1 !! i), (m2 !! i), (m3 !! i); try done; etransitivity; eauto.
+Qed.
 Global Instance: PartialOrder ((⊆) : relation (M A)).
 Proof.
-  repeat split.
-  * intros m; rewrite !map_subseteq_spec; naive_solver.
-  * intros m1 m2 m3; rewrite !map_subseteq_spec; naive_solver.
-  * intros m1 m2; rewrite !map_subseteq_spec.
-    intros; apply map_eq; intros i; apply option_eq; naive_solver.
+  split; [apply _|].
+  intros m1 m2; rewrite !map_subseteq_spec.
+  intros; apply map_eq; intros i; apply option_eq; naive_solver.
 Qed.
 Lemma lookup_weaken {A} (m1 m2 : M A) i x :
   m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x.
@@ -342,6 +340,18 @@ 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.
+Proof.
+  intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|];
+    by rewrite ?lookup_insert, ?lookup_insert_ne by done.
+Qed.
+Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
+  (∀ y, m !! i = Some y → R y x) → map_included R m (<[i:=x]>m).
+Proof.
+  intros ? j; destruct (decide (i = j)) as [->|].
+  * rewrite lookup_insert. destruct (m !! j); eauto.
+  * rewrite lookup_insert_ne by done. by destruct (m !! j).
+Qed.
 Lemma insert_subseteq {A} (m : M A) i x : m !! i = None → m ⊆ <[i:=x]>m.
 Proof. apply partial_alter_subseteq. Qed.
 Lemma insert_subset {A} (m : M A) i x : m !! i = None → m ⊂ <[i:=x]>m.
@@ -520,6 +530,12 @@ Proof.
   intros. rewrite <-(map_of_to_list m1), <-(map_of_to_list m2).
   auto using map_of_list_proper, NoDup_fst_map_to_list.
 Qed.
+Lemma map_to_of_list_flip {A} (m1 : M A) l2 :
+  map_to_list m1 ≡ₚ l2 → m1 = map_of_list l2.
+Proof.
+  intros. rewrite <-(map_of_to_list m1).
+  auto using map_of_list_proper, NoDup_fst_map_to_list.
+Qed.
 Lemma map_to_list_empty {A} : map_to_list ∅ = @nil (K * A).
 Proof.
   apply elem_of_nil_inv. intros [i x].
@@ -620,6 +636,35 @@ Proof.
   * intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
   * intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
 Qed.
+Lemma map_Forall_empty : map_Forall P ∅.
+Proof. intros i x. by rewrite lookup_empty. Qed.
+Lemma map_Forall_impl (Q : K → A → Prop) m :
+  map_Forall P m → (∀ i x, P i x → Q i x) → map_Forall Q m.
+Proof. unfold map_Forall; naive_solver. Qed.
+Lemma map_Forall_insert_11 m i x : map_Forall P (<[i:=x]>m) → P i x.
+Proof. intros Hm. by apply Hm; rewrite lookup_insert. Qed.
+Lemma map_Forall_insert_12 m i x :
+  m !! i = None → map_Forall P (<[i:=x]>m) → map_Forall P m.
+Proof.
+  intros ? Hm j y ?; apply Hm. by rewrite lookup_insert_ne by congruence.
+Qed.
+Lemma map_Forall_insert_2 m i x :
+  P i x → map_Forall P m → map_Forall P (<[i:=x]>m).
+Proof. intros ?? j y; rewrite lookup_insert_Some; naive_solver. Qed.
+Lemma map_Forall_insert m i x :
+  m !! i = None → map_Forall P (<[i:=x]>m) ↔ P i x ∧ map_Forall P m.
+Proof.
+  naive_solver eauto using map_Forall_insert_11,
+    map_Forall_insert_12, map_Forall_insert_2.
+Qed.
+Lemma map_Forall_ind (Q : M A → Prop) :
+  Q ∅ →
+  (∀ m i x, m !! i = None → P i x → map_Forall P m → Q m → Q (<[i:=x]>m)) →
+  ∀ m, map_Forall P m → Q m.
+Proof.
+  intros Hnil Hinsert m. induction m using map_ind; auto.
+  rewrite map_Forall_insert by done; intros [??]; eauto.
+Qed.
 
 Context `{∀ i x, Decision (P i x)}.
 Global Instance map_Forall_dec m : Decision (map_Forall P m).
@@ -630,11 +675,10 @@ Defined.
 Lemma map_not_Forall (m : M A) :
   ¬map_Forall P m ↔ ∃ i x, m !! i = Some x ∧ ¬P i x.
 Proof.
-  split.
-  * rewrite map_Forall_to_list. intros Hm.
-    apply (not_Forall_Exists _), Exists_exists in Hm.
-    destruct Hm as ([i x]&?&?). exists i x. by rewrite <-elem_of_map_to_list.
-  * intros (i&x&?&?) Hm. specialize (Hm i x). tauto.
+  split; [|intros (i&x&?&?) Hm; specialize (Hm i x); tauto].
+  rewrite map_Forall_to_list. intros Hm.
+  apply (not_Forall_Exists _), Exists_exists in Hm.
+  destruct Hm as ([i x]&?&?). exists i x. by rewrite <-elem_of_map_to_list.
 Qed.
 End map_Forall.
 
@@ -745,7 +789,7 @@ Let f (mx : option A) (my : option B) : option bool :=
   | None, None => None
   end.
 Lemma map_Forall2_alt (m1 : M A) (m2 : M B) :
-  map_Forall2 R P Q m1 m2 ↔ map_Forall (λ _ P, Is_true P) (merge f m1 m2).
+  map_Forall2 R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
 Proof.
   split.
   * intros Hm i P'; rewrite lookup_merge by done; intros.
@@ -758,7 +802,7 @@ Qed.
 Global Instance map_Forall2_dec `{∀ x y, Decision (R x y), ∀ x, Decision (P x),
   ∀ y, Decision (Q y)} m1 m2 : Decision (map_Forall2 R P Q m1 m2).
 Proof.
-  refine (cast_if (decide (map_Forall (λ _ P, Is_true P) (merge f m1 m2))));
+  refine (cast_if (decide (map_Forall (λ _, Is_true) (merge f m1 m2))));
     abstract by rewrite map_Forall2_alt.
 Defined.
 (** Due to the finiteness of finite maps, we can extract a witness if the
diff --git a/theories/finite.v b/theories/finite.v
index 6c78c6ab..66828c07 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -12,24 +12,26 @@ Arguments enum _ {_ _} : clear implicits.
 Arguments NoDup_enum _ {_ _} : clear implicits.
 Definition card A `{Finite A} := length (enum A).
 Program Instance finite_countable `{Finite A} : Countable A := {|
-  encode := λ x, Pos.of_nat $ S $ from_option 0 $ list_find (x =) (enum A);
+  encode := λ x,
+    Pos.of_nat $ S $ from_option 0 $ fst <$> list_find (x =) (enum A);
   decode := λ p, enum A !! pred (Pos.to_nat p)
 |}.
 Arguments Pos.of_nat _ : simpl never.
 Next Obligation.
   intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
-  destruct (list_find_eq_elem_of xs x) as [i Hi]; auto.
-  rewrite Nat2Pos.id by done; simpl.
-  rewrite Hi; eauto using list_find_eq_Some.
+  destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto.
+  rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
+  destruct (list_find_Some (x =) xs i y); naive_solver.
 Qed.
 Definition find `{Finite A} P `{∀ x, Decision (P x)} : option A :=
-  list_find P (enum A) ≫= decode_nat.
+  list_find P (enum A) ≫= decode_nat ∘ fst.
 
 Lemma encode_lt_card `{finA: Finite A} x : encode_nat x < card A.
 Proof.
   destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
-  rewrite Nat2Pos.id by done; simpl. destruct (list_find _ xs) eqn:?; simpl.
-  * eapply lookup_lt_Some, list_find_eq_Some; eauto.
+  rewrite Nat2Pos.id by done; simpl.
+  destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
+  * destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some.
   * destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
 Qed.
 Lemma encode_decode A `{finA: Finite A} i :
@@ -39,24 +41,25 @@ Proof.
   unfold encode_nat, decode_nat, encode, decode, card; simpl.
   intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
   exists x. rewrite !Nat2Pos.id by done; simpl.
-  destruct (list_find_eq_elem_of xs x) as [j Hj]; auto.
-  rewrite Hj. eauto using list_find_eq_Some, NoDup_lookup.
+  destruct (list_find_elem_of (x =) xs x) as [[j y] Hj]; auto.
+  destruct (list_find_Some (x =) xs j y) as [? ->]; auto.
+  rewrite Hj; csimpl; eauto using NoDup_lookup.
 Qed.
 Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
   find P = Some x → P x.
 Proof.
   destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl.
-  intros Hx. destruct (list_find _ _) as [i|] eqn:Hi; simplify_option_equality.
+  intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_equality'.
   rewrite !Nat2Pos.id in Hx by done.
-  destruct (list_find_Some P xs i) as (?&?&?); simplify_option_equality; eauto.
+  destruct (list_find_Some P xs i y); naive_solver.
 Qed.
 Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
   P x → ∃ y, find P = Some y ∧ P y.
 Proof.
   destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
-  intros Hx. destruct (list_find_elem_of P xs x) as [i Hi]; auto.
-  rewrite Hi. destruct (list_find_Some P xs i) as (y&?&?); subst; auto.
-  exists y. csimpl. by rewrite !Nat2Pos.id by done.
+  intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
+  rewrite Hi. destruct (list_find_Some P xs i y); simplify_equality'; auto.
+  exists y. by rewrite !Nat2Pos.id by done.
 Qed.
 
 Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P.
diff --git a/theories/hashset.v b/theories/hashset.v
index 2cb6359f..26dffddd 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -115,25 +115,6 @@ Proof.
       rewrite Forall_forall in Hm. eapply (Hm (_,_)); eauto. }
     destruct Hn; rewrite elem_of_list_fmap; exists (hash x, l'); eauto.
 Qed.
-
-Definition remove_dups_fast (l : list A) : list A :=
-  elements (foldr (λ x, ({[ x ]} ∪)) ∅ l : hashset hash).
-Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
-Proof.
-  unfold remove_dups_fast. rewrite elem_of_elements. split.
-  * revert x. induction l as [|y l IH]; intros x; simpl.
-    { by rewrite elem_of_empty. }
-    rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
-  * induction 1; esolve_elem_of.
-Qed.
-Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
-Proof. unfold remove_dups_fast. apply NoDup_elements. Qed.
-Definition listset_normalize (X : listset A) : listset A :=
-  let (l) := X in Listset (remove_dups_fast l).
-Lemma listset_normalize_correct X : listset_normalize X ≡ X.
-Proof.
-  destruct X as [l]. apply elem_of_equiv; intro; apply elem_of_remove_dups_fast.
-Qed.
 End hashset.
 
 (** These instances are declared using [Hint Extern] to avoid too
@@ -152,3 +133,39 @@ Hint Extern 1 (Difference (hashset _)) =>
   eapply @hashset_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (hashset _)) =>
   eapply @hashset_elems : typeclass_instances.
+
+Section remove_duplicates.
+Context `{∀ x y : A, Decision (x = y)} (hash : A → Z).
+
+Definition remove_dups_fast (l : list A) : list A :=
+  match l with
+  | [] => []
+  | [x] => [x]
+  | _ =>
+     let n :Z := length l in
+     elements (foldr (λ x, ({[ x ]} ∪)) ∅ l :
+       hashset (λ x, hash x `mod` n)%Z)
+  end.
+Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
+Proof.
+  destruct l as [|x1 [|x2 l]]; try reflexivity.
+  unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
+  generalize (λ x, hash x `mod` length l)%Z; intros f.
+  rewrite elem_of_elements; split.
+  * revert x. induction l as [|y l IH]; intros x; simpl.
+    { by rewrite elem_of_empty. }
+    rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
+  * induction 1; esolve_elem_of.
+Qed.
+Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
+Proof.
+  unfold remove_dups_fast; destruct l as [|x1 [|x2 l]].
+  apply NoDup_nil_2. apply NoDup_singleton. apply NoDup_elements.
+Qed.
+Definition listset_normalize (X : listset A) : listset A :=
+  let (l) := X in Listset (remove_dups_fast l).
+Lemma listset_normalize_correct X : listset_normalize X ≡ X.
+Proof.
+  destruct X as [l]. apply elem_of_equiv; intro; apply elem_of_remove_dups_fast.
+Qed.
+End remove_duplicates.
diff --git a/theories/list.v b/theories/list.v
index 3237f976..8be24df4 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -88,10 +88,11 @@ Instance list_filter {A} : Filter A (list A) :=
 
 (** The function [list_find P l] returns the first index [i] whose element
 satisfies the predicate [P]. *)
-Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option nat :=
+Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A) :=
   fix go l :=
   match l with
-  | [] => None | x :: l => if decide (P x) then Some 0 else S <$> go l
+  | [] => None
+  | x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
   end.
 
 (** The function [replicate n x] generates a list with length [n] of elements
@@ -702,29 +703,20 @@ End filter.
 (** ** Properties of the [find] function *)
 Section find.
   Context (P : A → Prop) `{∀ x, Decision (P x)}.
-  Lemma list_find_Some l i :
-    list_find P l = Some i → ∃ x, l !! i = Some x ∧ P x.
+  Lemma list_find_Some l i x :
+    list_find P l = Some (i,x) → l !! i = Some x ∧ P x.
   Proof.
-    revert i. induction l; intros [] ?; simplify_option_equality; eauto.
+    revert i; induction l; intros [] ?;
+      repeat (match goal with x : prod _ _ |- _ => destruct x end
+              || simplify_option_equality); eauto.
   Qed.
-  Lemma list_find_elem_of l x : x ∈ l → P x → ∃ i, list_find P l = Some i.
+  Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
   Proof.
     induction 1 as [|x y l ? IH]; intros; simplify_option_equality; eauto.
-    by destruct IH as [i ->]; [|exists (S i)].
+    by destruct IH as [[i x'] ->]; [|exists (S i, x')].
   Qed.
 End find.
 
-Section find_eq.
-  Context `{∀ x y, Decision (x = y)}.
-  Lemma list_find_eq_Some l i x : list_find (x =) l = Some i → l !! i = Some x.
-  Proof.
-    intros.
-    destruct (list_find_Some (x =) l i) as (?&?&?); auto with congruence.
-  Qed.
-  Lemma list_find_eq_elem_of l x : x ∈ l → ∃ i, list_find (x=) l = Some i.
-  Proof. eauto using list_find_elem_of. Qed.
-End find_eq.
-
 (** ** Properties of the [reverse] function *)
 Lemma reverse_nil : reverse [] = @nil A.
 Proof. done. Qed.
@@ -2244,6 +2236,8 @@ Section Forall2.
   Proof.
     naive_solver eauto using Forall2_length, Forall2_lookup_lr,Forall2_lookup_2.
   Qed.
+  Lemma Forall2_tail l k : Forall2 P l k → Forall2 P (tail l) (tail k).
+  Proof. destruct 1; simpl; auto. Qed.
   Lemma Forall2_alter_l f l k i :
     Forall2 P l k →
     (∀ x y, l !! i = Some x → k !! i = Some y → P x y → P (f x) y) →
diff --git a/theories/tactics.v b/theories/tactics.v
index af83a0f8..63bf8024 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -85,40 +85,6 @@ Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
   hyp (H6) hyp(H7) hyp(H8) hyp(H9) hyp(H10) :=
   clear dependent H1 H2 H3 H4 H5 H6 H7 H8 H9; clear dependent H10.
 
-(** The tactic [first_of t ft ot] calls [t] and then calls [ft] on the first
-subgoal generated by [t], and [ot] on the other subgoals. *)
-Ltac first_of t ft ot :=
-     solve [t]
-  || (t; [ ft ])
-  || (t; [ ft | ot ])
-  || (t; [ ft | ot | ot ])
-  || (t; [ ft | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot ])
-  || (t; [ ft | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot ]).
-
-Ltac last_of t ot lt :=
-     solve [t]
-  || (t; [ lt ])
-  || (t; [ ot | lt ])
-  || (t; [ ot | ot | lt ])
-  || (t; [ ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | lt ])
-  || (t; [ ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | ot | lt ]).
-
 (** The tactic [is_non_dependent H] determines whether the goal's conclusion or
 hypotheses depend on [H]. *)
 Tactic Notation "is_non_dependent" constr(H) :=
-- 
GitLab