Lots more work

src/Automation.v

@@ -191,7 +191,7 @@ Ltac solve_by_inversion :=
   | [H: _ |- _] => solve [inversion H]
   end.
 
-Ltac simplify_hypotheses :=
+Ltac specialize_hypotheses :=
   repeat
     match goal with
     | [H: _ -> _ |- _] => specialize (H ltac:(auto))

src/Blockchain.v

@@ -848,7 +848,7 @@ Proof.
     split; [eapply new_acts_no_out_queue|eapply list.Forall_cons]; eauto.
   - (* Permutation *)
     subst.
-    simplify_hypotheses.
+    specialize_hypotheses.
     match goal with
     | [prev_eq_new: _ = _, perm: Permutation _ _ |- _] =>
       now rewrite prev_eq_new in *; rewrite <- perm; auto

src/Containers.v

 From Coq Require Import List.
 From Coq Require Import ZArith.
+From Coq Require Import Permutation.
 From stdpp Require gmap.
 From SmartContracts Require Import Monads.
 From SmartContracts Require Import BoundedN.
+From SmartContracts Require Import Automation.
 Import ListNotations.
 
 Notation FMap := gmap.gmap.
@@ -66,6 +68,45 @@ Module FMap.
       k <> k' ->
       find k' (partial_alter f k m) = find k' m.
     Proof. apply fin_maps.lookup_partial_alter_ne. Qed.
+
+    Lemma find_empty k :
+      FMap.find k (FMap.empty : FMap K V) = None.
+    Proof. apply fin_maps.lookup_empty. Qed.
+
+    Lemma elements_add (m : FMap K V) k v :
+      find k m = None ->
+      Permutation (elements (add k v m)) ((k, v) :: elements m).
+    Proof. apply fin_maps.map_to_list_insert. Qed.
+
+    Lemma elements_empty : (elements empty : list (K * V)) = [].
+    Proof. now rewrite fin_maps.map_to_list_empty. Qed.
+
+    Lemma elements_add_empty (k : K) (v : V) :
+      FMap.elements (FMap.add k v FMap.empty) = [(k, v)].
+    Proof. now rewrite fin_maps.insert_empty, fin_maps.map_to_list_singleton. Qed.
+
+    Lemma add_remove (m : FMap K V) k v :
+      add k v (remove k m) = add k v m.
+    Proof. apply fin_maps.insert_delete. Qed.
+
+    Lemma remove_add (m : FMap K V) k v :
+      find k m = None ->
+      remove k (add k v m) = m.
+    Proof. apply fin_maps.delete_insert. Qed.
+
+    Lemma find_remove (m : FMap K V) k :
+      find k (remove k m) = None.
+    Proof. apply fin_maps.lookup_delete. Qed.
+
+    Lemma add_commute (m : FMap K V) (k k' : K) (v v' : V) :
+      k <> k' ->
+      FMap.add k v (FMap.add k' v' m) = FMap.add k' v' (FMap.add k v m).
+    Proof. apply fin_maps.insert_commute. Qed.
+
+    Lemma add_id (m : FMap K V) k v :
+      find k m = Some v ->
+      add k v m = m.
+    Proof. apply fin_maps.insert_id. Qed.
   End Theories.
 End FMap.
 

src/Extras.v

@@ -56,11 +56,21 @@ Proof.
   lia.
 Qed.
 
+Lemma sumnat_permutation
+      {A : Type} {f : A -> nat} {xs ys : list A}
+      (perm_eq : Permutation xs ys) :
+  sumnat f xs = sumnat f ys.
+Proof. induction perm_eq; perm_simplify; lia. Qed.
+
+Instance sumnat_perm_proper {A : Type} {f : A -> nat} :
+  Proper (Permutation (A:=A) ==> eq) (sumnat f).
+Proof. intros x y perm. now apply sumnat_permutation. Qed.
+
 Lemma sumZ_permutation
       {A : Type} {f : A -> Z} {xs ys : list A}
       (perm_eq : Permutation xs ys) :
   sumZ f xs = sumZ f ys.
-Proof. induction perm_eq; prove. Qed.
+Proof. induction perm_eq; perm_simplify; lia. Qed.
 
 Instance sumZ_perm_proper {A : Type} {f : A -> Z} :
   Proper (Permutation (A:=A) ==> eq) (sumZ f).