Commit 458189b2 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Simplify a couple of proofs

parent 8016c378
......@@ -245,7 +245,7 @@ Module BoundedN.
specialize (x_bound (or_introl eq_refl)).
destruct x_bound as [useless x_bound]; clear useless.
cbn in x_bound.
destruct (of_nat x) eqn:ofnatx. all: cycle 1.
destruct (of_nat x) eqn:ofnatx; cycle 1.
apply of_nat_none in ofnatx.
lia.
constructor.
......
......@@ -256,11 +256,8 @@ Section ExecuteActions.
destruct (env_contract_states _ _) as [prev_state|] eqn:prev_state_eq;
[|cbn in *; congruence].
cbn -[lc_to_env] in *.
destruct (wc_receive wc _ _ _ _) eqn:receive;
destruct (wc_receive wc _ _ _ _) as [[new_state resp_acts]|] eqn:receive;
[|cbn in *; congruence].
match goal with
| [p: SerializedValue * list ActionBody |- _] => destruct p as [new_state resp_acts]
end.
Hint Resolve gtb_le ltb_ge : core.
apply (eval_call from to amount wc msg prev_state new_state resp_acts);
try solve [cbn in *; auto; congruence].
......
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