Save work before changes

.gitignore

@@ -3,5 +3,6 @@
 .*.aux
 *.v.d
 .coqdeps.d
+*.cache
 CoqMakefile
 CoqMakefile.conf

src/Automation.v

@@ -7,7 +7,7 @@
  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
  *)
 
-Require Import Eqdep List Omega Permutation.
+From Coq Require Import Eqdep List Omega Permutation.
 Import ListNotations.
 
 Set Implicit Arguments.
@@ -118,14 +118,13 @@ Ltac prove' invOne :=
 
 Ltac prove := prove' fail.
 
-Hint Rewrite <- Permutation_middle.
-
 Lemma Permutation_app_middle {A : Type} (xs l1 l2 l3 l4 : list A) :
   Permutation (l1 ++ l2) (l3 ++ l4) ->
-  Permutation (l1 ++ (xs ++ l2)) (l3 ++ (xs ++ l4)).
+  Permutation (l1 ++ xs ++ l2) (l3 ++ xs ++ l4).
 Proof.
+  Hint Rewrite <- Permutation_middle.
   intros perm.
-  induction xs as [| x xs IH]; prove.
+  induction xs; prove.
 Qed.
 
 (* Change all x :: l into [x] ++ l *)
@@ -141,13 +140,11 @@ Ltac appify :=
 Local Ltac reassoc_right :=
   match goal with
   | [|- Permutation _ (?l1 ++ ?l2 ++ ?l3)] => rewrite (app_assoc l1 l2 l3)
-  | _ => fail 1
   end.
 
 Local Ltac reassoc_left :=
   match goal with
   | [|- Permutation (?l1 ++ ?l2 ++ ?l3) _] => rewrite (app_assoc l1 l2 l3)
-  | _ => fail 1
   end.
 
 Local Ltac unassoc_right :=
@@ -159,9 +156,9 @@ Local Ltac unassoc_right :=
 Local Ltac simplify_perm_once :=
   let rec aux :=
       apply Permutation_app_middle ||
-      (tryif reassoc_right
+      tryif reassoc_right
         then aux
-        else (unassoc_right; reassoc_left; aux)) in
+        else (unassoc_right; reassoc_left; aux) in
   repeat rewrite <- app_assoc;
   aux.
 

src/Blockchain.v

@@ -26,7 +26,6 @@ Definition BlockId := nat.
 Definition Version := nat.
 
 Open Scope Z.
-(*Set Primitive Projections.*)
 
 Record ContractDeployment :=
   build_contract_deployment {
@@ -412,13 +411,13 @@ Section Transfer.
       head_block_post : head_block post = head_block pre;
       account_balance_pre_from : account_balance pre from >= amount;
       account_balance_post_to : account_balance post to >= amount;
-      incoming_txs_post_to :
+      incoming_txs_consed :
         incoming_txs post to = (action : Tx) :: incoming_txs pre to;
-      outgoing_txs_post_from :
+      outgoing_txs_consed :
         outgoing_txs post from = (action : Tx) :: outgoing_txs pre from;
-      incoming_txs_post :
+      incoming_txs_unchanged :
         forall a, a <> to -> incoming_txs post a = incoming_txs pre a;
-      outgoing_txs_post :
+      outgoing_txs_unchanged :
         forall a, a <> from -> outgoing_txs post a = outgoing_txs pre a;
 
       body_transfer : match body with
@@ -566,6 +565,7 @@ Section StepCirculation.
     rewrite 2!(sumZ_permutation perm); prove.
     rewrite (account_balance_from_pre_post transfer).
     rewrite (account_balance_to_pre_post transfer).
+    rewrite account_balance_from_pre_post.
     enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by prove.
 
     pose proof (Permutation_NoDup perm addrs_set) as perm_set.

src/Extras.v

@@ -38,33 +38,16 @@ Lemma sumZ_permutation
   sumZ f xs = sumZ f ys.
 Proof. induction perm_eq; prove. Qed.
 
-Lemma count_occ_split
-      {A : Type}
-      (A_dec : (forall a b, {a = b} + {a <> b}))
-      (l : list A)
-      (x : A)
-      (n : nat)
-      (c_before : count_occ A_dec l x = S n)
-  : exists pref suf, l = pref ++ x :: suf /\ count_occ A_dec (pref ++ suf) x = n.
-Proof.
-  revert n c_before.
-  induction l as [| hd tl IH]; intros n c_before; [inversion c_before |].
-  simpl in *.
-  destruct (A_dec hd x) as [hd_eq_x | hd_neq_x].
-  - subst.
-    exists [], tl; prove.
-  - specialize (IH _ c_before).
-    destruct IH as [pref [suf [tl_eq count]]]; subst.
-    exists (hd :: pref), suf.
-    simpl.
-    destruct (A_dec hd x); prove.
-Qed.
-
 Lemma in_app_cons_or {A : Type} (x y : A) (xs ys : list A) :
   x <> y ->
   In x (xs ++ y :: ys) ->
   In x (xs ++ ys).
-Proof. prove. Qed.
+Proof.
+  intros x_neq_y x_in.
+  apply in_or_app.
+  apply in_app_or in x_in.
+  prove.
+Qed.
 
 Lemma incl_split {A : Type} (l m n : list A) :
   incl (l ++ m) n -> incl l n /\ incl m n.