Commit 7f3a1b38 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Improve a proof

parent b90d97fe
......@@ -70,10 +70,10 @@ Ltac perm_simplify :=
simpl;
try apply Permutation_refl.
Ltac case_match :=
Ltac destruct_match :=
match goal with
| [H: context [ match ?x with _ => _ end ] |- _] => destruct x eqn:?
| [|- context [ match ?x with _ => _ end ]] => destruct x eqn:?
| [H: context [ match ?x with _ => _ end ] |- _] => destruct x eqn:?
end.
Ltac destruct_units :=
......
......@@ -228,25 +228,26 @@ Program Definition contract_to_weak_contract
end in
build_weak_contract weak_init _ weak_recv _.
Next Obligation.
intros.
intros c1 c2 eq_chains ctx1 ctx2 eq_ctx setup1 setup2 eq_setups.
subst ctx2 setup2.
repeat intro.
subst.
subst weak_init.
simpl.
destruct (deserialize setup1); auto; simpl.
cbn.
destruct (deserialize _); auto.
cbn.
now rewrite init_proper.
Qed.
Next Obligation.
intros.
intros c1 c2 eq_chains ctx1 ctx2 eq_ctx state1 state2 eq_states msg1 msg2 eq_msgs.
subst ctx2 state2 msg2.
repeat intro.
subst.
subst weak_recv.
simpl.
destruct (deserialize state1); auto; simpl.
destruct msg1.
+ destruct (deserialize _); auto; simpl.
cbn.
destruct (deserialize _); auto.
cbn.
destruct_match.
- destruct (deserialize _); auto.
cbn.
now rewrite receive_proper.
+ now rewrite receive_proper.
- now rewrite receive_proper.
Qed.
Coercion contract_to_weak_contract : Contract >-> WeakContract.
......
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