From 89af6fc3f3940cb03553c403432dfff52e6d8d7a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 26 Mar 2014 13:33:54 +0100 Subject: Adding an interface to Eqdecide and putting the grammar rules in a dedicated file. --- tactics/eqdecide.ml | 208 +++++++++++++++++++++++++++++++++++++++++++ tactics/eqdecide.ml4 | 219 ---------------------------------------------- tactics/eqdecide.mli | 17 ++++ tactics/g_eqdecide.ml4 | 25 ++++++ tactics/hightactics.mllib | 1 + 5 files changed, 251 insertions(+), 219 deletions(-) create mode 100644 tactics/eqdecide.ml delete mode 100644 tactics/eqdecide.ml4 create mode 100644 tactics/eqdecide.mli create mode 100644 tactics/g_eqdecide.ml4 diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml new file mode 100644 index 0000000000..0effc3136e --- /dev/null +++ b/tactics/eqdecide.ml @@ -0,0 +1,208 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (clear [destVar c]))) + +let choose_eq eqonleft = + if eqonleft then + left_with_bindings false Misctypes.NoBindings + else + right_with_bindings false Misctypes.NoBindings +let choose_noteq eqonleft = + if eqonleft then + right_with_bindings false Misctypes.NoBindings + else + left_with_bindings false Misctypes.NoBindings + +let mkBranches c1 c2 = + Tacticals.New.tclTHENLIST + [Proofview.V82.tactic (generalize [c2]); + Simple.elim c1; + intros; + Tacticals.New.onLastHyp Simple.case; + Proofview.V82.tactic clear_last; + intros] + +let solveNoteqBranch side = + Tacticals.New.tclTHEN (choose_noteq side) + (Tacticals.New.tclTHEN introf + (Tacticals.New.onLastHypId (fun id -> Extratactics.discrHyp id))) + +(* Constructs the type {c1=c2}+{~c1=c2} *) + +let mkDecideEqGoal eqonleft op rectype c1 c2 g = + let equality = mkApp(build_coq_eq(), [|rectype; c1; c2|]) in + let disequality = mkApp(build_coq_not (), [|equality|]) in + if eqonleft then mkApp(op, [|equality; disequality |]) + else mkApp(op, [|disequality; equality |]) + + +(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *) + +let mkGenDecideEqGoal rectype g = + let hypnames = pf_ids_of_hyps g in + let xname = next_ident_away (Id.of_string "x") hypnames + and yname = next_ident_away (Id.of_string "y") hypnames in + (mkNamedProd xname rectype + (mkNamedProd yname rectype + (mkDecideEqGoal true (build_coq_sumbool ()) + rectype (mkVar xname) (mkVar yname) g))) + +let eqCase tac = + (Tacticals.New.tclTHEN intro + (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp Equality.rewriteLR) + (Tacticals.New.tclTHEN (Proofview.V82.tactic clear_last) + tac))) + +let diseqCase eqonleft = + let diseq = Id.of_string "diseq" in + let absurd = Id.of_string "absurd" in + (Tacticals.New.tclTHEN (intro_using diseq) + (Tacticals.New.tclTHEN (choose_noteq eqonleft) + (Tacticals.New.tclTHEN (Proofview.V82.tactic red_in_concl) + (Tacticals.New.tclTHEN (intro_using absurd) + (Tacticals.New.tclTHEN (Proofview.V82.tactic (Simple.apply (mkVar diseq))) + (Tacticals.New.tclTHEN (Extratactics.injHyp absurd) + (full_trivial []))))))) + +open Proofview.Notations + +(* spiwack: a small wrapper around [Hipattern]. *) + +let match_eqdec c = + try Proofview.tclUNIT (match_eqdec c) + with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure + +(* /spiwack *) + +let solveArg eqonleft op a1 a2 tac = + Proofview.Goal.enter begin fun gl -> + let rectype = Tacmach.New.of_old (fun g -> pf_type_of g a1) gl in + let decide = + Tacmach.New.of_old (fun g -> mkDecideEqGoal eqonleft op rectype a1 a2 g) gl + in + let subtacs = + if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto] + else [diseqCase eqonleft;eqCase tac;default_auto] in + (Tacticals.New.tclTHENS (Proofview.V82.tactic (elim_type decide)) subtacs) + end + +let solveEqBranch rectype = + Proofview.tclORELSE + begin + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) -> + let (mib,mip) = Global.lookup_inductive rectype in + let nparams = mib.mind_nparams in + let getargs l = List.skipn nparams (snd (decompose_app l)) in + let rargs = getargs rhs + and largs = getargs lhs in + List.fold_right2 + (solveArg eqonleft op) largs rargs + (Tacticals.New.tclTHEN (choose_eq eqonleft) intros_reflexivity) + end + end + begin function + | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!")) + | e -> Proofview.tclZERO e + end + +(* The tactic Decide Equality *) + +let hd_app c = match kind_of_term c with + | App (h,_) -> h + | _ -> c + +let decideGralEquality = + Proofview.tclORELSE + begin + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) -> + let headtyp = Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) gl in + begin match kind_of_term headtyp with + | Ind mi -> Proofview.tclUNIT mi + | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects.")) + end >>= fun rectype -> + (Tacticals.New.tclTHEN + (mkBranches c1 c2) + (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) + end + end + begin function + | PatternMatchingFailure -> + Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")) + | e -> Proofview.tclZERO e + end + +let decideEqualityGoal = Tacticals.New.tclTHEN intros decideGralEquality + +let decideEquality rectype = + Proofview.Goal.enter begin fun gl -> + let decide = Tacmach.New.of_old (mkGenDecideEqGoal rectype) gl in + (Tacticals.New.tclTHENS (cut decide) [default_auto;decideEqualityGoal]) + end + + +(* The tactic Compare *) + +let compare c1 c2 = + Proofview.Goal.enter begin fun gl -> + let rectype = Tacmach.New.of_old (fun g -> pf_type_of g c1) gl in + let decide = Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) gl in + (Tacticals.New.tclTHENS (cut decide) + [(Tacticals.New.tclTHEN intro + (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp simplest_case) + (Proofview.V82.tactic clear_last))); + decideEquality rectype]) + end diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 deleted file mode 100644 index 7b47605119..0000000000 --- a/tactics/eqdecide.ml4 +++ /dev/null @@ -1,219 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (clear [destVar c]))) - -let choose_eq eqonleft = - if eqonleft then - left_with_bindings false Misctypes.NoBindings - else - right_with_bindings false Misctypes.NoBindings -let choose_noteq eqonleft = - if eqonleft then - right_with_bindings false Misctypes.NoBindings - else - left_with_bindings false Misctypes.NoBindings - -let mkBranches c1 c2 = - Tacticals.New.tclTHENLIST - [Proofview.V82.tactic (generalize [c2]); - Simple.elim c1; - intros; - Tacticals.New.onLastHyp Simple.case; - Proofview.V82.tactic clear_last; - intros] - -let solveNoteqBranch side = - Tacticals.New.tclTHEN (choose_noteq side) - (Tacticals.New.tclTHEN introf - (Tacticals.New.onLastHypId (fun id -> Extratactics.discrHyp id))) - -(* Constructs the type {c1=c2}+{~c1=c2} *) - -let mkDecideEqGoal eqonleft op rectype c1 c2 g = - let equality = mkApp(build_coq_eq(), [|rectype; c1; c2|]) in - let disequality = mkApp(build_coq_not (), [|equality|]) in - if eqonleft then mkApp(op, [|equality; disequality |]) - else mkApp(op, [|disequality; equality |]) - - -(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *) - -let mkGenDecideEqGoal rectype g = - let hypnames = pf_ids_of_hyps g in - let xname = next_ident_away (Id.of_string "x") hypnames - and yname = next_ident_away (Id.of_string "y") hypnames in - (mkNamedProd xname rectype - (mkNamedProd yname rectype - (mkDecideEqGoal true (build_coq_sumbool ()) - rectype (mkVar xname) (mkVar yname) g))) - -let eqCase tac = - (Tacticals.New.tclTHEN intro - (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp Equality.rewriteLR) - (Tacticals.New.tclTHEN (Proofview.V82.tactic clear_last) - tac))) - -let diseqCase eqonleft = - let diseq = Id.of_string "diseq" in - let absurd = Id.of_string "absurd" in - (Tacticals.New.tclTHEN (intro_using diseq) - (Tacticals.New.tclTHEN (choose_noteq eqonleft) - (Tacticals.New.tclTHEN (Proofview.V82.tactic red_in_concl) - (Tacticals.New.tclTHEN (intro_using absurd) - (Tacticals.New.tclTHEN (Proofview.V82.tactic (Simple.apply (mkVar diseq))) - (Tacticals.New.tclTHEN (Extratactics.injHyp absurd) - (full_trivial []))))))) - -open Proofview.Notations - -(* spiwack: a small wrapper around [Hipattern]. *) - -let match_eqdec c = - try Proofview.tclUNIT (match_eqdec c) - with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure - -(* /spiwack *) - -let solveArg eqonleft op a1 a2 tac = - Proofview.Goal.enter begin fun gl -> - let rectype = Tacmach.New.of_old (fun g -> pf_type_of g a1) gl in - let decide = - Tacmach.New.of_old (fun g -> mkDecideEqGoal eqonleft op rectype a1 a2 g) gl - in - let subtacs = - if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto] - else [diseqCase eqonleft;eqCase tac;default_auto] in - (Tacticals.New.tclTHENS (Proofview.V82.tactic (elim_type decide)) subtacs) - end - -let solveEqBranch rectype = - Proofview.tclORELSE - begin - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) -> - let (mib,mip) = Global.lookup_inductive rectype in - let nparams = mib.mind_nparams in - let getargs l = List.skipn nparams (snd (decompose_app l)) in - let rargs = getargs rhs - and largs = getargs lhs in - List.fold_right2 - (solveArg eqonleft op) largs rargs - (Tacticals.New.tclTHEN (choose_eq eqonleft) intros_reflexivity) - end - end - begin function - | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!")) - | e -> Proofview.tclZERO e - end - -(* The tactic Decide Equality *) - -let hd_app c = match kind_of_term c with - | App (h,_) -> h - | _ -> c - -let decideGralEquality = - Proofview.tclORELSE - begin - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) -> - let headtyp = Tacmach.New.of_old (fun g -> hd_app (pf_compute g typ)) gl in - begin match kind_of_term headtyp with - | Ind mi -> Proofview.tclUNIT mi - | _ -> Proofview.tclZERO (UserError ("",Pp.str"This decision procedure only works for inductive objects.")) - end >>= fun rectype -> - (Tacticals.New.tclTHEN - (mkBranches c1 c2) - (Tacticals.New.tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype))) - end - end - begin function - | PatternMatchingFailure -> - Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")) - | e -> Proofview.tclZERO e - end - -let decideEqualityGoal = Tacticals.New.tclTHEN intros decideGralEquality - -let decideEquality rectype = - Proofview.Goal.enter begin fun gl -> - let decide = Tacmach.New.of_old (mkGenDecideEqGoal rectype) gl in - (Tacticals.New.tclTHENS (cut decide) [default_auto;decideEqualityGoal]) - end - - -(* The tactic Compare *) - -let compare c1 c2 = - Proofview.Goal.enter begin fun gl -> - let rectype = Tacmach.New.of_old (fun g -> pf_type_of g c1) gl in - let decide = Tacmach.New.of_old (fun g -> mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g) gl in - (Tacticals.New.tclTHENS (cut decide) - [(Tacticals.New.tclTHEN intro - (Tacticals.New.tclTHEN (Tacticals.New.onLastHyp simplest_case) - (Proofview.V82.tactic clear_last))); - decideEquality rectype]) - end - - -(* User syntax *) - -TACTIC EXTEND decide_equality -| [ "decide" "equality" ] -> [ decideEqualityGoal ] -END - -TACTIC EXTEND compare -| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] -END diff --git a/tactics/eqdecide.mli b/tactics/eqdecide.mli new file mode 100644 index 0000000000..32d0a38716 --- /dev/null +++ b/tactics/eqdecide.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Constr.t -> unit Proofview.tactic diff --git a/tactics/g_eqdecide.ml4 b/tactics/g_eqdecide.ml4 new file mode 100644 index 0000000000..c9d876d92f --- /dev/null +++ b/tactics/g_eqdecide.ml4 @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [ decideEqualityGoal ] +END + +TACTIC EXTEND compare +| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] +END diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 0d6322af61..bc94c722f5 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -7,3 +7,4 @@ Rewrite G_rewrite Tauto Eqdecide +G_eqdecide -- cgit v1.2.3