diff options
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 6 | ||||
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 2 | ||||
| -rw-r--r-- | src/Util/Tactics/SplitInContext.v | 10 |
3 files changed, 11 insertions, 7 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 01018c3e2..6eeee9f48 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -232,7 +232,7 @@ Module Ring. Lemma Good : GoodT. Proof. - split_and. + split_and; simpl in *. repeat match goal with | [ H : context[andb _ true] |- _ ] => setoid_rewrite andb_true_r in H end. @@ -441,7 +441,7 @@ Module MontgomeryStyleRing. Qed. Lemma Good : GoodT. Proof. - split_and. + split_and; simpl in *. repeat match goal with | [ H : context[andb _ true] |- _ ] => setoid_rewrite andb_true_r in H end. @@ -839,7 +839,7 @@ Module Pipeline. | _ => eassumption || reflexivity end.. ]. { subst; split; [ | assumption ]. - split_and. + split_and; simpl in *. split; [ solve [ eauto with nocore ] | ]. { intros; match goal with H : _ |- _ => erewrite H; clear H end; eauto. transitivity (type.app_curried (Interp (PartialEvaluateWithListInfoFromBounds e arg_bounds)) arg1). diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index abbf08a05..92799222e 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -2173,7 +2173,7 @@ Module Ring. Lemma Good : GoodT. Proof. - split_and. + split_and; simpl in *. eapply subsetoid_ring_by_ring_isomorphism; cbv [ring_opp ring_add ring_sub ring_mul ring_encode F.sub] in *; repeat match goal with diff --git a/src/Util/Tactics/SplitInContext.v b/src/Util/Tactics/SplitInContext.v index 3ff313197..dd4e424a3 100644 --- a/src/Util/Tactics/SplitInContext.v +++ b/src/Util/Tactics/SplitInContext.v @@ -5,9 +5,13 @@ Require Export Crypto.Util.FixCoqMistakes. Ltac split_in_context_by ident funl funr tac := repeat match goal with | [ H : context p [ident] |- _ ] => - let H0 := context p[funl] in let H0' := eval simpl in H0 in assert H0' by (tac H); - let H1 := context p[funr] in let H1' := eval simpl in H1 in assert H1' by (tac H); - clear H + let H0 := context p[funl] in + let H1 := context p[funr] in + let H0' := (eval cbv beta in H0) in + let H1' := (eval cbv beta in H1) in + assert H0' by (tac H); + assert H1' by (tac H); + clear H end. Ltac split_in_context ident funl funr := split_in_context_by ident funl funr ltac:(fun H => apply H). |