From 0c687b54156b415684a78ae6d702f5efc41aca87 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Jul 2016 14:49:11 -0700 Subject: Add useful tactics and util lemmas --- src/Util/Tactics.v | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'src/Util/Tactics.v') diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 304ae3c20..4630e4ab7 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -260,3 +260,30 @@ Ltac side_conditions_before_to_side_conditions_after tac_in H := here, after evars are instantiated, and not above. *) move H after H'; clear H' | .. ]. + +(** Do something with every hypothesis. *) +Ltac do_with_hyp' tac := + match goal with + | [ H : _ |- _ ] => tac H + end. + +(** Rewrite with any applicable hypothesis. *) +Tactic Notation "rewrite_hyp" "*" := do_with_hyp' ltac:(fun H => rewrite H). +Tactic Notation "rewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => rewrite -> H). +Tactic Notation "rewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => rewrite <- H). +Tactic Notation "rewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite !H). +Tactic Notation "rewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H). +Tactic Notation "rewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H). +Tactic Notation "rewrite_hyp" "!*" := progress rewrite_hyp ?*. +Tactic Notation "rewrite_hyp" "->" "!*" := progress rewrite_hyp -> ?*. +Tactic Notation "rewrite_hyp" "<-" "!*" := progress rewrite_hyp <- ?*. + +Tactic Notation "rewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite H in * ). +Tactic Notation "rewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite -> H in * ). +Tactic Notation "rewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite <- H in * ). +Tactic Notation "rewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite !H in * ). +Tactic Notation "rewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H in * ). +Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H in * ). +Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *. +Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *. +Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *. -- cgit v1.2.3 From 71179e46a7c404e76bc58c2465d547ead6df3e26 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 7 Jul 2016 16:02:23 -0400 Subject: wrap nsatz in Algebra --- _CoqProject | 3 +- src/Algebra.v | 12 +- .../CompleteEdwardsCurveTheorems.v | 2 +- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 2 +- src/CompleteEdwardsCurve/Pre.v | 2 +- src/Tactics/Algebra_syntax/Nsatz.v | 159 +++++++++++++++++++++ src/Tactics/Nsatz.v | 156 -------------------- src/Util/Tactics.v | 3 + 8 files changed, 176 insertions(+), 163 deletions(-) create mode 100644 src/Tactics/Algebra_syntax/Nsatz.v delete mode 100644 src/Tactics/Nsatz.v (limited to 'src/Util/Tactics.v') diff --git a/_CoqProject b/_CoqProject index f3f07e840..f8aa1e966 100644 --- a/_CoqProject +++ b/_CoqProject @@ -28,6 +28,7 @@ src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v +src/Encoding/PointEncodingPre.v src/Experiments/DerivationsOptionRectLetInEncoding.v src/Experiments/EdDSARefinement.v src/Experiments/GenericFieldPow.v @@ -54,8 +55,8 @@ src/Spec/ModularWordEncoding.v src/Spec/WeierstrassCurve.v src/Specific/GF1305.v src/Specific/GF25519.v -src/Tactics/Nsatz.v src/Tactics/VerdiTactics.v +src/Tactics/Algebra_syntax/Nsatz.v src/Util/CaseUtil.v src/Util/Decidable.v src/Util/IterAssocOp.v diff --git a/src/Algebra.v b/src/Algebra.v index f9dfbd519..9f53c0613 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -1,9 +1,10 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Util.Tactics Crypto.Tactics.Nsatz. +Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Notations. Require Coq.Numbers.Natural.Peano.NPeano. Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope. +Require Crypto.Tactics.Algebra_syntax.Nsatz. Module Import ModuloCoq8485. Import NPeano Nat. @@ -637,6 +638,11 @@ Module Field. End Homomorphism. End Field. +(** Tactics *) + +Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax. +Ltac nsatz_contradict := Algebra_syntax.Nsatz.nsatz_contradict; dropRingSyntax. + (*** Tactics for manipulating field equations *) Require Import Coq.setoid_ring.Field_tac. @@ -981,7 +987,7 @@ Ltac neq01 := Ltac conservative_field_algebra := intros; conservative_common_denominator_all; - try (nsatz; dropRingSyntax); + try nsatz; repeat (apply conj); try solve [neq01 @@ -991,7 +997,7 @@ Ltac conservative_field_algebra := Ltac field_algebra := intros; common_denominator_all; - try (nsatz; dropRingSyntax); + try nsatz; repeat (apply conj); try solve [neq01 diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 65d899463..44bb80157 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 364d7f9ec..263582508 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -1,6 +1,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index ed4511fc9..432e834aa 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. -Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.Algebra Crypto.Algebra. Require Import Crypto.Util.Notations. Generalizable All Variables. diff --git a/src/Tactics/Algebra_syntax/Nsatz.v b/src/Tactics/Algebra_syntax/Nsatz.v new file mode 100644 index 000000000..a5b04cfa2 --- /dev/null +++ b/src/Tactics/Algebra_syntax/Nsatz.v @@ -0,0 +1,159 @@ +(*** Tactics for manipulating polynomial equations *) +Require Coq.nsatz.Nsatz. +Require Import List. + +Generalizable All Variables. +Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)} + : forall x y, eq (sub x y) zero <-> eq x y. +Proof. + split;intros Hx. + { eapply Nsatz.psos_r1b. eapply Hx. } + { eapply Nsatz.psos_r1. eapply Hx. } +Qed. + +Ltac get_goal := lazymatch goal with |- ?g => g end. + +Ltac nsatz_equation_implications_to_list eq zero g := + lazymatch g with + | eq ?p zero => constr:(p::nil) + | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l) + end. + +Ltac nsatz_reify_equations eq zero := + let g := get_goal in + let lb := nsatz_equation_implications_to_list eq zero g in + lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with + (?variables, ?le) => + lazymatch (eval compute in (List.rev le)) with + | ?reified_goal::?reified_givens => constr:((variables, reified_givens, reified_goal)) + end + end. + +Ltac nsatz_get_free_variables reified_package := + lazymatch reified_package with (?fv, _, _) => fv end. + +Ltac nsatz_get_reified_givens reified_package := + lazymatch reified_package with (_, ?givens, _) => givens end. + +Ltac nsatz_get_reified_goal reified_package := + lazymatch reified_package with (_, _, ?goal) => goal end. + +Require Import Coq.setoid_ring.Ring_polynom. +(* Kludge for 8.4/8.5 compatibility *) +Module Import mynsatz_compute. + Import Nsatz. + Global Ltac mynsatz_compute x := nsatz_compute x. +End mynsatz_compute. +Ltac nsatz_compute x := mynsatz_compute x. + +Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens := + nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens). + +Ltac nsatz_compute_get_leading_coefficient := + lazymatch goal with + |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a + end. + +Ltac nsatz_compute_get_certificate := + lazymatch goal with + |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:((c,b)) + end. + +Ltac nsatz_rewrite_and_revert domain := + lazymatch type of domain with + | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => + lazymatch goal with + | |- eq _ zero => idtac + | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring)) + end; + repeat match goal with + | [H : eq _ zero |- _ ] => revert H + | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H + end + end. + +(** As per https://coq.inria.fr/bugs/show_bug.cgi?id=4851, [nsatz] + cannot handle duplicate hypotheses. So we clear them. *) +Ltac nsatz_clear_duplicates_for_bug_4851 domain := + lazymatch type of domain with + | @Integral_domain.Integral_domain _ _ _ _ _ _ _ ?eq _ _ _ => + repeat match goal with + | [ H : eq ?x ?y, H' : eq ?x ?y |- _ ] => clear H' + end + end. + +Ltac nsatz_nonzero := + try solve [apply Integral_domain.integral_domain_one_zero + |apply Integral_domain.integral_domain_minus_one_zero + |trivial + |assumption]. + +Ltac nsatz_domain_sugar_power domain sugar power := + let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *) + lazymatch type of domain with + | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => + nsatz_clear_duplicates_for_bug_4851 domain; + nsatz_rewrite_and_revert domain; + let reified_package := nsatz_reify_equations eq zero in + let fv := nsatz_get_free_variables reified_package in + let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in + let reified_givens := nsatz_get_reified_givens reified_package in + let reified_goal := nsatz_get_reified_goal reified_package in + nsatz_compute_to_goal sugar nparams reified_goal power reified_givens; + let a := nsatz_compute_get_leading_coefficient in + let crt := nsatz_compute_get_certificate in + intros _ (* discard [nsatz_compute] output *); intros; + apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond)); + [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS] + | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *) + | solve [repeat (split; [assumption|]); exact I] ] + end. + +Ltac nsatz_guess_domain := + match goal with + | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) + | |- not (?eq _ _) => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) + | [H: ?eq _ _ |- _ ] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) + | [H: not (?eq _ _) |- _] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) + end. + +Ltac nsatz_sugar_power sugar power := + let domain := nsatz_guess_domain in + nsatz_domain_sugar_power domain sugar power. + +Ltac nsatz_power power := + let power_N := (eval compute in (BinNat.N.of_nat power)) in + nsatz_sugar_power BinInt.Z0 power_N. + +Ltac nsatz := nsatz_power 1%nat || nsatz_power 2%nat || nsatz_power 3%nat || nsatz_power 4%nat || nsatz_power 5%nat. + +Tactic Notation "nsatz" := nsatz. +Tactic Notation "nsatz" constr(n) := nsatz_power n. + +(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y] + contradicts any hypothesis of the form [?x' <> ?y'], we turn this + problem about inequalities into one about equalities and give it + to [nsatz]. *) +Ltac nsatz_contradict_single_hypothesis domain := + lazymatch type of domain with + | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => + unfold not in *; + match goal with + | [ H : eq _ _ -> False |- eq _ _ -> False ] + => intro; apply H; nsatz + | [ H : eq _ _ -> False |- False ] + => apply H; nsatz + end + end. + +Ltac nsatz_contradict := + let domain := nsatz_guess_domain in + nsatz_contradict_single_hypothesis domain + || (unfold not; + intros; + lazymatch type of domain with + | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => + assert (eq one zero) as Hbad; + [nsatz; nsatz_nonzero + |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)] + end). diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v deleted file mode 100644 index 04f35c200..000000000 --- a/src/Tactics/Nsatz.v +++ /dev/null @@ -1,156 +0,0 @@ -(*** Tactics for manipulating polynomial equations *) -Require Coq.nsatz.Nsatz. -Require Import List. - -Generalizable All Variables. -Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)} - : forall x y, eq (sub x y) zero <-> eq x y. -Proof. - split;intros Hx. - { eapply Nsatz.psos_r1b. eapply Hx. } - { eapply Nsatz.psos_r1. eapply Hx. } -Qed. - -Ltac get_goal := lazymatch goal with |- ?g => g end. - -Ltac nsatz_equation_implications_to_list eq zero g := - lazymatch g with - | eq ?p zero => constr:(p::nil) - | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l) - end. - -Ltac nsatz_reify_equations eq zero := - let g := get_goal in - let lb := nsatz_equation_implications_to_list eq zero g in - lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with - (?variables, ?le) => - lazymatch (eval compute in (List.rev le)) with - | ?reified_goal::?reified_givens => constr:((variables, reified_givens, reified_goal)) - end - end. - -Ltac nsatz_get_free_variables reified_package := - lazymatch reified_package with (?fv, _, _) => fv end. - -Ltac nsatz_get_reified_givens reified_package := - lazymatch reified_package with (_, ?givens, _) => givens end. - -Ltac nsatz_get_reified_goal reified_package := - lazymatch reified_package with (_, _, ?goal) => goal end. - -Require Import Coq.setoid_ring.Ring_polynom. -(* Kludge for 8.4/8.5 compatibility *) -Module Import mynsatz_compute. - Import Nsatz. - Global Ltac mynsatz_compute x := nsatz_compute x. -End mynsatz_compute. -Ltac nsatz_compute x := mynsatz_compute x. - -Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens := - nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens). - -Ltac nsatz_compute_get_leading_coefficient := - lazymatch goal with - |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a - end. - -Ltac nsatz_compute_get_certificate := - lazymatch goal with - |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:((c,b)) - end. - -Ltac nsatz_rewrite_and_revert domain := - lazymatch type of domain with - | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => - lazymatch goal with - | |- eq _ zero => idtac - | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring)) - end; - repeat match goal with - | [H : eq _ zero |- _ ] => revert H - | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H - end - end. - -(** As per https://coq.inria.fr/bugs/show_bug.cgi?id=4851, [nsatz] - cannot handle duplicate hypotheses. So we clear them. *) -Ltac nsatz_clear_duplicates_for_bug_4851 domain := - lazymatch type of domain with - | @Integral_domain.Integral_domain _ _ _ _ _ _ _ ?eq _ _ _ => - repeat match goal with - | [ H : eq ?x ?y, H' : eq ?x ?y |- _ ] => clear H' - end - end. - -Ltac nsatz_nonzero := - try solve [apply Integral_domain.integral_domain_one_zero - |apply Integral_domain.integral_domain_minus_one_zero - |trivial - |assumption]. - -Ltac nsatz_domain_sugar_power domain sugar power := - let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *) - lazymatch type of domain with - | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring => - nsatz_clear_duplicates_for_bug_4851 domain; - nsatz_rewrite_and_revert domain; - let reified_package := nsatz_reify_equations eq zero in - let fv := nsatz_get_free_variables reified_package in - let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in - let reified_givens := nsatz_get_reified_givens reified_package in - let reified_goal := nsatz_get_reified_goal reified_package in - nsatz_compute_to_goal sugar nparams reified_goal power reified_givens; - let a := nsatz_compute_get_leading_coefficient in - let crt := nsatz_compute_get_certificate in - intros _ (* discard [nsatz_compute] output *); intros; - apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond)); - [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS] - | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *) - | solve [repeat (split; [assumption|]); exact I] ] - end. - -Ltac nsatz_guess_domain := - match goal with - | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) - | |- not (?eq _ _) => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) - | [H: ?eq _ _ |- _ ] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) - | [H: not (?eq _ _) |- _] => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq)) - end. - -Ltac nsatz_sugar_power sugar power := - let domain := nsatz_guess_domain in - nsatz_domain_sugar_power domain sugar power. - -Tactic Notation "nsatz" constr(n) := - let nn := (eval compute in (BinNat.N.of_nat n)) in - nsatz_sugar_power BinInt.Z0 nn. - -Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat. - -(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y] - contradicts any hypothesis of the form [?x' <> ?y'], we turn this - problem about inequalities into one about equalities and give it - to [nsatz]. *) -Ltac nsatz_contradict_single_hypothesis domain := - lazymatch type of domain with - | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => - unfold not in *; - match goal with - | [ H : eq _ _ -> False |- eq _ _ -> False ] - => intro; apply H; nsatz - | [ H : eq _ _ -> False |- False ] - => apply H; nsatz - end - end. - -Ltac nsatz_contradict := - let domain := nsatz_guess_domain in - nsatz_contradict_single_hypothesis domain - || (unfold not; - intros; - lazymatch type of domain with - | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring => - assert (eq one zero) as Hbad; - [nsatz; nsatz_nonzero - |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)] - end). diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 4630e4ab7..01d72def9 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -7,6 +7,9 @@ Tactic Notation "test" tactic3(tac) := (** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *) Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds"). +Ltac get_goal := + match goal with |- ?G => G end. + (** find the head of the given expression *) Ltac head expr := match expr with -- cgit v1.2.3