diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-21 16:58:35 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-21 16:58:35 -0700 |
| commit | 2e80edafe48a01aa3bb43fa7e32da518822418a0 (patch) | |
| tree | fb12fb11ae3fcded59d4d697deb2997054c49d22 | |
| parent | 475eb51406c5bf9620199a8af2afddf37e7f5eb0 (diff) | |
Make [bash] tactic easier to debug
Now you don't have to copy/paste the [match goal with ... end].
| -rw-r--r-- | .mailmap | 1 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 26 |
2 files changed, 15 insertions, 12 deletions
@@ -9,6 +9,7 @@ Jade Philipoom <jadep@mit.edu> Jade Philipoom <jadep Jade Philipoom <jadep@mit.edu> jadep <jade.philipoom@gmail.com> Jade Philipoom <jadep@mit.edu> jadep <jadep@mit.edu> Jason Gross <jgross@mit.edu> Jason Gross <jgross@mit.edu> +Jason Gross <jgross@mit.edu> Jason Gross <jagro@google.com> Robert Sloan <varomodt@gmail.com> Robert Sloan <rsloan@sumologic.com> Robert Sloan <varomodt@gmail.com> Robert Sloan <varomodt@dhcp-18-189-26-21.dyn.MIT.EDU> Robert Sloan <varomodt@gmail.com> Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU> diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index b843cd54c..7d728719a 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -109,17 +109,19 @@ Module E. Program Definition opp (P:point) : point := exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _. - Ltac bash := - repeat match goal with - | |- _ => progress intros - | [H: _ /\ _ |- _ ] => destruct H - | |- _ => progress destruct_points - | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in * - | |- _ => split - | |- Feq _ _ => field_algebra - | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto] - | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances - end. + Ltac bash_step := + match goal with + | |- _ => progress intros + | [H: _ /\ _ |- _ ] => destruct H + | |- _ => progress destruct_points + | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in * + | |- _ => split + | |- Feq _ _ => field_algebra + | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto] + | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances + end. + + Ltac bash := repeat bash_step. Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. bash. Qed. Global Instance Proper_opp : Proper (eq==>eq) opp. Proof. bash. Qed. @@ -225,4 +227,4 @@ Module E. end. Qed. End Homomorphism. -End E.
\ No newline at end of file +End E. |