Commit 5cd83c67 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Various clean ups

- Remove 'prove' tactic
- Remove some duplicated tactics and make some proofs more efficient
parent e0780ad4
Pipeline #12241 failed with stage
in 1 minute
From Coq Require Import Eqdep List Omega Permutation.
Import ListNotations.
Set Implicit Arguments.
Ltac inject H := injection H; clear H; intros; try subst.
Ltac appHyps f :=
match goal with
| [ H : _ |- _ ] => f H
end.
Ltac inList x ls :=
match ls with
| x => idtac
| (_, x) => idtac
| (?LS, _) => inList x LS
end.
Ltac app f ls :=
match ls with
| (?LS, ?X) => f X || app f LS || fail 1
| _ => f ls
end.
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.
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.
Hint Rewrite <- Permutation_middle.
intros perm.
induction xs; prove.
rewrite 2!(Permutation_app_comm xs).
rewrite 2!app_assoc.
apply Permutation_app_tail.
auto.
Qed.
(* Change all x :: l into [x] ++ l *)
......
......@@ -429,6 +429,11 @@ Record EnvironmentEquiv (e1 e2 : Environment) : Prop :=
contracts_eq : forall a, env_contracts e1 a = env_contracts e2 a;
}.
Ltac rewrite_environment_equiv :=
match goal with
| [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
end.
Global Program Instance environment_equiv_equivalence : Equivalence EnvironmentEquiv.
Next Obligation.
intros x; apply build_env_equiv; reflexivity.
......@@ -481,10 +486,7 @@ Ltac solve_proper :=
[apply build_chain_equiv|];
cbn;
repeat intro;
repeat
match goal with
| [H: EnvironmentEquiv _ _|- _] => rewrite H
end;
repeat rewrite_environment_equiv;
auto.
Global Instance add_tx_proper :
......@@ -633,10 +635,7 @@ Lemma account_balance_post (addr : Address) :
- (if (addr =? step_from step)%address then step_amount step else 0).
Proof.
unfold account_balance.
destruct step; subst; cbn;
match goal with
| [H: EnvironmentEquiv _ _ |- _] => rewrite H
end;
destruct step; subst; cbn; rewrite_environment_equiv;
cbn; unfold add_tx_to_map; destruct_address_eq; cbn; lia.
Qed.
......@@ -645,8 +644,10 @@ Lemma account_balance_post_to :
account_balance post (step_to step) =
account_balance pre (step_to step) + step_amount step.
Proof.
intros neq.
rewrite account_balance_post.
destruct_address_eq; prove.
rewrite address_eq_refl, address_eq_ne by auto.
lia.
Qed.
Lemma account_balance_post_from :
......@@ -654,8 +655,10 @@ Lemma account_balance_post_from :
account_balance post (step_from step) =
account_balance pre (step_from step) - step_amount step.
Proof.
intros neq.
rewrite account_balance_post.
destruct_address_eq; prove.
rewrite address_eq_refl, address_eq_ne by auto.
lia.
Qed.
Lemma account_balance_post_irrelevant (addr : Address) :
......@@ -663,27 +666,22 @@ Lemma account_balance_post_irrelevant (addr : Address) :
addr <> step_to step ->
account_balance post addr = account_balance pre addr.
Proof.
intros neq_from neq_to.
rewrite account_balance_post.
destruct_address_eq; prove.
repeat rewrite address_eq_ne by auto.
lia.
Qed.
Lemma block_header_post_step : block_header post = block_header pre.
Proof.
destruct step;
match goal with
| [H: EnvironmentEquiv _ _ |- _] => now rewrite H
end.
Qed.
Proof. destruct step; rewrite_environment_equiv; auto. Qed.
Lemma contracts_post_pre_none contract :
env_contracts post contract = None ->
env_contracts pre contract = None.
Proof.
intros H.
destruct step;
match goal with
| [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
end; cbn in *; auto.
destruct step; rewrite_environment_equiv; auto.
cbn in *.
destruct_address_eq; congruence.
Qed.
End Theories.
......@@ -772,19 +770,14 @@ different environment and queue of actions. *)
Definition ChainTrace := CursorList ChainState ChainEvent.
Section Theories.
Ltac rewrite_environment_equiv :=
match goal with
| [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
end.
Ltac destruct_event :=
Ltac destruct_chain_event :=
match goal with
| [H: ChainEvent _ _ |- _] => destruct H
| [evt: ChainEvent _ _ |- _] => destruct evt
end.
Ltac destruct_step :=
Ltac destruct_chain_step :=
match goal with
| [H: ChainStep _ _ _ _ |- _] => destruct H
| [step: ChainStep _ _ _ _ |- _] => destruct step
end.
Lemma contract_addr_format
......@@ -798,11 +791,12 @@ Proof.
remember empty_state eqn:eq.
induction trace; rewrite eq in *; clear eq.
- cbn in *; congruence.
- destruct_event.
- destruct_chain_event.
+ rewrite_environment_equiv; cbn in *; auto.
+ destruct_step; rewrite_environment_equiv; cbn in *; destruct_address_eq; subst; auto.
+ destruct_chain_step; rewrite_environment_equiv; cbn in *; destruct_address_eq; subst; auto.
+ intuition.
Qed.
Lemma new_acts_no_out_queue addr1 addr2 new_acts resp_acts :
addr1 <> addr2 ->
new_acts = map (build_act addr2) resp_acts ->
......@@ -813,16 +807,6 @@ Proof.
constructor; destruct_address_eq; cbn in *; congruence.
Qed.
Ltac destruct_chain_event :=
match goal with
| [evt: ChainEvent _ _ |- _] => destruct evt
end.
Ltac destruct_chain_step :=
match goal with
| [step: ChainStep _ _ _ _ |- _] => destruct step
end.
Local Open Scope address.
(* This next lemma shows that any for a full chain trace,
the ending state will not have any queued actions from
......@@ -887,21 +871,20 @@ Proof.
Hint Resolve contracts_post_pre_none : core.
pose proof
(undeployed_contract_no_out_queue
contract prev
ltac:(auto) ltac:(auto) ltac:(eauto)) as Hqueue.
repeat
match goal with
| [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
end.
inversion_clear Hqueue.
destruct_chain_step; rewrite_environment_equiv;
repeat
match goal with
| [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
end;
subst;
subst tx;
inversion Hqueue;
cbn in *;
unfold add_tx_to_map;
inversion Hqueue;
subst;
cbn in *;
destruct_address_eq;
subst; try tauto; congruence.
- match goal with
......
......@@ -195,13 +195,13 @@ Module BoundedN.
* tauto.
+ destruct H as [eq | Hin].
* left.
rewrite eq in of_nat_x.
rewrite of_to_nat in of_nat_x; prove.
* prove.
rewrite eq, of_to_nat in of_nat_x.
congruence.
* cbn. tauto.
+ tauto.
+ destruct H as [eq | Hin].
* rewrite eq, of_to_nat in of_nat_x; inversion of_nat_x.
* prove.
* tauto.
Qed.
Module Stdpp.
......
......@@ -25,7 +25,10 @@ Lemma address_reorganize {a b : Address} :
Proof.
intros a_neq_b.
apply (NoDup_incl_reorganize _ [a; b]);
repeat constructor; unfold incl; prove.
repeat constructor; unfold incl; auto.
intros Hin.
cbn in *.
intuition.
Qed.
Lemma step_from_to_same
......@@ -61,20 +64,23 @@ Proof.
destruct (address_reorganize from_neq_to) as [suf perm].
apply Permutation_sym in perm.
unfold circulation.
rewrite 2!(sumZ_permutation perm); prove.
rewrite 2!(sumZ_permutation perm).
cbn.
rewrite (account_balance_post_to step from_neq_to).
rewrite (account_balance_post_from step from_neq_to).
enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by prove.
enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by lia.
pose proof (Permutation_NoDup perm) as perm_set.
assert (from_not_in_suf: ~In (step_from step) suf).
{ apply (in_NoDup_app _ [step_from step; step_to step] _); prove. }
{ apply (in_NoDup_app _ [step_from step; step_to step] _); intuition. }
assert (to_not_in_suf: ~In (step_to step) suf).
{ apply (in_NoDup_app _ [step_from step; step_to step] _); prove. }
{ apply (in_NoDup_app _ [step_from step; step_to step] _); intuition. }
clear perm perm_set.
pose proof (account_balance_post_irrelevant step).
induction suf as [| x xs IH]; prove.
pose proof (account_balance_post_irrelevant step) as balance_irrel.
induction suf as [| x xs IH]; auto.
cbn in *.
rewrite IH, balance_irrel; auto.
Qed.
Hint Resolve step_circulation_unchanged : core.
......@@ -84,7 +90,13 @@ Instance circulation_proper :
Proof.
intros x y [].
unfold circulation, account_balance.
induction (elements Address); prove.
induction (elements Address) as [|z zs IH]; auto.
cbn.
now
repeat
match goal with
| [H: _ |- _] => rewrite H
end.
Qed.
Lemma circulation_add_new_block header baker env :
......@@ -92,7 +104,7 @@ Lemma circulation_add_new_block header baker env :
(circulation env + compute_block_reward (block_height header))%Z.
Proof.
assert (Hperm: exists suf, Permutation ([baker] ++ suf) (elements Address)).
{ apply NoDup_incl_reorganize; repeat constructor; unfold incl; prove. }
{ apply NoDup_incl_reorganize; repeat constructor; unfold incl; auto. }
destruct Hperm as [suf perm].
symmetry in perm.
pose proof (Permutation_NoDup perm (elements_set Address)) as perm_set.
......@@ -108,7 +120,7 @@ Proof.
enough (e = f) by lia
end.
pose proof (in_NoDup_app baker [baker] suf ltac:(prove) perm_set) as not_in_suf.
pose proof (in_NoDup_app baker [baker] suf ltac:(intuition) perm_set) as not_in_suf.
clear perm perm_set e.
induction suf as [| x xs IH]; auto.
cbn in *.
......
......@@ -348,7 +348,8 @@ Ltac solve_contract_proper :=
| [|- pair _ _ = pair _ _] => f_equal
| [|- (if ?x then _ else _) = (if ?x then _ else _)] => destruct x
| [|- match ?x with | _ => _ end = match ?x with | _ => _ end ] => destruct x
| _ => prove
| [H: ChainEquiv _ _ |- _] => rewrite H in *
| _ => subst; auto
end.
Lemma init_proper :
......
......@@ -96,12 +96,18 @@ Proof.
intros x_neq_y x_in.
apply in_or_app.
apply in_app_or in x_in.
prove.
destruct x_in as [?|x_in]; auto.
destruct x_in; auto; congruence.
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.
Proof.
intros H.
unfold incl in *.
Hint Resolve in_or_app : core.
auto.
Qed.
Lemma NoDup_incl_reorganize
{A : Type}
......@@ -125,7 +131,8 @@ Proof.
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 incl_xs as [in_pref | [in_x | in_suf]]; auto.
congruence.
* destruct (IH _ H2 H) as [suf' perm_suf'].
exists suf'.
perm_simplify.
......@@ -136,11 +143,13 @@ Lemma in_NoDup_app {A : Type} (x : A) (l m : list A) :
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.
replace ((l1 ++ x :: l2) ++ m) with (l1 ++ x :: (l2 ++ m)) in nodup_l_app_m.
- apply (NoDup_remove_2 _ _ _) in nodup_l_app_m.
rewrite app_assoc in nodup_l_app_m.
auto.
- rewrite app_comm_cons.
appify.
now rewrite app_assoc.
Qed.
Lemma seq_app start len1 len2 :
......
......@@ -132,7 +132,7 @@ Qed.
Program Instance oak_positive_equivalence : OakTypeEquivalence positive :=
{| serialize p := serialize (Zpos p);
deserialize z := do z' <- deserialize z; Some (Z.to_pos z'); |}.
Next Obligation. prove. Qed.
Next Obligation. auto. Qed.
Program Instance oak_value_equivalence : OakTypeEquivalence OakValue :=
{| serialize v := v;
......
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