Commit 7526b4eb authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Lots of work

parent 99b27297
(* Copyright (c) 2008-2012, Adam Chlipala
*
* This work is licensed under a
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
* Unported License.
* The license text is available at:
* http://creativecommons.org/licenses/by-nc-nd/3.0/
*)
Require Import Eqdep List Omega Permutation.
Import ListNotations.
Set Implicit Arguments.
(** A version of [injection] that does some standard simplifications afterward: clear the hypothesis in question, bring the new facts above the double line, and attempt substitution for known variables. *)
Ltac inject H := injection H; clear H; intros; try subst.
(** Try calling tactic function [f] on all hypotheses, keeping the first application that doesn't fail. *)
Ltac appHyps f :=
match goal with
| [ H : _ |- _ ] => f H
end.
(** Succeed iff [x] is in the list [ls], represented with left-associated nested tuples. *)
Ltac inList x ls :=
match ls with
| x => idtac
| (_, x) => idtac
| (?LS, _) => inList x LS
end.
(** Try calling tactic function [f] on every element of tupled list [ls], keeping the first call not to fail. *)
Ltac app f ls :=
match ls with
| (?LS, ?X) => f X || app f LS || fail 1
| _ => f ls
end.
(** Run [f] on every element of [ls], not just the first that doesn't fail. *)
Ltac all f ls :=
match ls with
| (?LS, ?X) => f X; all f LS
| (_, _) => fail 1
| _ => f ls
end.
(** Workhorse tactic to simplify hypotheses for a variety of proofs.
* Argument [invOne] is a tuple-list of predicates for which we always do inversion automatically. *)
Ltac simplHyp invOne :=
(** Helper function to do inversion on certain hypotheses, where [H] is the hypothesis and [F] its head symbol *)
let invert H F :=
(** We only proceed for those predicates in [invOne]. *)
inList F invOne;
(** This case covers an inversion that succeeds immediately, meaning no constructors of [F] applied. *)
(inversion H; fail)
(** Otherwise, we only proceed if inversion eliminates all but one constructor case. *)
|| (inversion H; [idtac]; clear H; try subst) in
match goal with
(** Eliminate all existential hypotheses. *)
| [ H : ex _ |- _ ] => destruct H
(** Find opportunities to take advantage of injectivity of data constructors, for several different arities. *)
| [ H : ?F ?X = ?F ?Y |- ?G ] =>
(** This first branch of the [||] fails the whole attempt iff the arguments of the constructor applications are already easy to prove equal. *)
(assert (X = Y); [ assumption | fail 1 ])
(** If we pass that filter, then we use injection on [H] and do some simplification as in [inject].
* The odd-looking check of the goal form is to avoid cases where [injection] gives a more complex result because of dependent typing, which we aren't equipped to handle here. *)
|| (injection H;
match goal with
| [ |- X = Y -> G ] =>
try clear H; intros; try subst
end)
| [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
(assert (X = Y); [ assumption
| assert (U = V); [ assumption | fail 1 ] ])
|| (injection H;
match goal with
| [ |- U = V -> X = Y -> G ] =>
try clear H; intros; try subst
end)
(** Consider some different arities of a predicate [F] in a hypothesis that we might want to invert. *)
| [ H : ?F _ |- _ ] => invert H F
| [ H : ?F _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ _ |- _ ] => invert H F
| [ H : Some _ = Some _ |- _ ] => injection H; clear H
end.
(** Find some hypothesis to rewrite with, ensuring that [auto] proves all of the extra subgoals added by [rewrite]. *)
Ltac rewriteHyp :=
match goal with
| [ H : _ |- _ ] => rewrite H by solve [ auto ]
end.
(** Combine [autorewrite] with automatic hypothesis rewrites. *)
Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
Ltac rewriter := autorewrite with core in *; rewriterP.
Hint Rewrite app_ass.
Hint Rewrite app_comm_cons.
Ltac prove' invOne :=
let sintuition :=
simpl in *; intuition auto; try subst;
repeat (simplHyp invOne; intuition auto; try subst); try congruence in
let rewriter := autorewrite with core in *;
repeat (match goal with
| [ H : ?P |- _ ] => rewrite H by prove' invOne
end; autorewrite with core in *) in
do 3 (sintuition; autounfold; rewriter); try omega; try (elimtype False; omega).
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)).
Proof.
intros perm.
induction xs as [| x xs IH]; prove.
Qed.
(* Change all x :: l into [x] ++ l *)
Ltac appify :=
match goal with
| [|- context[?e :: ?l]] =>
match l with
| nil => fail 1
| _ => change (e :: l) with ([e] ++ l)
end
end.
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 :=
repeat
match goal with
| [|- Permutation _ ((?l1 ++ ?l2) ++ ?l3)] => rewrite <- (app_assoc l1 l2 l3)
end.
Local Ltac simplify_perm_once :=
let rec aux :=
apply Permutation_app_middle ||
(tryif reassoc_right
then aux
else (unassoc_right; reassoc_left; aux)) in
repeat rewrite <- app_assoc;
aux.
Local Ltac simplify_perm_round :=
simpl;
repeat appify;
(* Change into [] ++ l ++ [] *)
match goal with
| [|- Permutation ?l1 ?l2] => change l1 with ([] ++ l1);
change l2 with ([] ++ l2);
rewrite <- (app_nil_r l1), <- (app_nil_r l2)
end;
repeat simplify_perm_once;
simpl;
repeat rewrite <- app_assoc;
repeat rewrite app_nil_r;
repeat
match goal with
| [H: Permutation ?l1 ?l2|-_] => rewrite H
end.
Ltac simplify_perm :=
repeat simplify_perm_round;
simpl;
try apply Permutation_refl.
This diff is collapsed.
From Coq Require Import String.
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
......@@ -336,7 +337,6 @@ Qed.
Definition contract : Contract Setup Msg State :=
build_contract version init receive.
(*
(* This first property states that the Congress will only send out actions
to be performed if there is a matching CreateProposal somewhere in the
......
From Coq Require Import ZArith.
From Coq Require Import List.
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Psatz.
From SmartContracts Require Import Automation.
Import ListNotations.
Fixpoint find_first {A B : Type} (f : A -> option B) (l : list A)
......@@ -20,3 +25,87 @@ Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A)
end
| [] => []
end.
Fixpoint sumZ {A : Type} (f : A -> Z) (xs : list A) : Z :=
match xs with
| [] => 0
| x :: xs' => f x + sumZ f xs'
end.
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.
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.
Lemma incl_split {A : Type} (l m n : list A) :
incl (l ++ m) n -> incl l n /\ incl m n.
Proof. unfold incl; generalize in_or_app; prove. Qed.
Lemma NoDup_incl_reorganize
{A : Type}
(l l' : list A) :
NoDup l' ->
incl l' l ->
exists suf, Permutation (l' ++ suf) l.
Proof.
revert l.
induction l' as [| x xs IH]; intros l nodup_l' incl_l'_l.
- exists l. apply Permutation_refl.
- assert (x_in_l: In x l).
+ apply (incl_l'_l x). left. constructor.
+ destruct (in_split _ _ x_in_l) as [pref [suf eq]]; subst.
inversion nodup_l'; subst.
assert (incl xs (pref ++ suf)).
* intros a a_in.
apply in_or_app.
apply (incl_split [x] xs _) in incl_l'_l.
destruct incl_l'_l as [incl_x incl_xs].
intuition.
specialize (incl_xs a a_in).
apply in_app_or in incl_xs.
destruct incl_xs as [in_pref | [in_x | in_suf]]; prove.
* destruct (IH _ H2 H) as [suf' perm_suf'].
exists suf'.
simplify_perm.
Qed.
Lemma in_NoDup_app {A : Type} (x : A) (l m : list A) :
In x l -> NoDup (l ++ m) -> ~In x m.
Proof.
intros in_x_l nodup_l_app_m in_x_m.
destruct (in_split _ _ in_x_l) as [l1 [l2 eq]]; subst.
replace ((l1 ++ x :: l2) ++ m) with (l1 ++ x :: (l2 ++ m)) in nodup_l_app_m;
[|prove].
apply (NoDup_remove_2 _ _ _) in nodup_l_app_m.
rewrite app_assoc in nodup_l_app_m.
generalize in_or_app; prove.
Qed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment