diff options
-rw-r--r-- | Makefile | 5 | ||||
-rw-r--r-- | states/MakeInitial.v | 1 | ||||
-rw-r--r-- | tactics/EqDecide.v | 33 | ||||
-rw-r--r-- | tactics/eqdecide.ml | 196 | ||||
-rw-r--r-- | test-suite/success/eqdecide.v | 22 |
5 files changed, 255 insertions, 2 deletions
@@ -119,7 +119,7 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo \ HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo tactics/equality.cmo \ tactics/inv.cmo tactics/leminv.cmo tactics/eauto.cmo \ - tactics/autorewrite.cmo tactics/refine.cmo + tactics/autorewrite.cmo tactics/refine.cmo tactics/eqdecide.cmo SPECTAC=tactics/tauto.ml4 USERTAC = $(SPECTAC) @@ -237,7 +237,8 @@ theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) init: $(INITVO) TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo \ - tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo + tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo \ + tactics/EqDecide.vo tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) $(COQC) -$(BEST) -bindir bin -q -I tactics -is states/barestate.coq $< diff --git a/states/MakeInitial.v b/states/MakeInitial.v index b8c75307a..151306194 100644 --- a/states/MakeInitial.v +++ b/states/MakeInitial.v @@ -7,3 +7,4 @@ Require Export Inv. Require Export EAuto. Require Export AutoRewrite. Require Export Refine. +Require Export EqDecide. diff --git a/tactics/EqDecide.v b/tactics/EqDecide.v new file mode 100644 index 000000000..4fa3c2f06 --- /dev/null +++ b/tactics/EqDecide.v @@ -0,0 +1,33 @@ +(****************************************************************************) +(* EqDecide.v *) +(* A tactic for deciding propositional equality on inductive types *) +(* by Eduardo Gimenez *) +(****************************************************************************) + +(*i $Id$ i*) + +Declare ML Module "equality" "eqdecide". + + +Grammar tactic simple_tactic : ast := + EqDecideRuleG1 + [ "Decide" "Equality" constrarg($com1) constrarg($com2) ] -> + [ (DecideEquality $com1 $com2) ] + +| EqDecideRuleG2 + [ "Decide" "Equality" ] -> [ (DecideEquality) ] + +| CompareRule + [ "Compare" constrarg($com1) constrarg($com2) ] -> [ (Compare $com1 $com2) ]. + + +Syntax tactic level 0: + EqDecideRulePP1 + [ <<(DecideEquality)>> ] -> [ "Decide Equality" ] + +| EqDecideRulePP2 + [ <<(DecideEquality $com1 $com2)>> ] -> + [ "Decide Equality" [1 2] $com1 [1 2] $com2 ] + +| ComparePP + [ <<(Compare $com1 $com2)>> ] -> [ "Compare" [1 2] $com1 [1 2] $com2 ]. diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml new file mode 100644 index 000000000..728430f06 --- /dev/null +++ b/tactics/eqdecide.ml @@ -0,0 +1,196 @@ + +(*i $Id$ i*) + +open Util +open Names +open Term +open Tactics +open Tacticals +open Hiddentac +open Equality +open Auto +open Pattern +open Hipattern +open Proof_trees +open Proof_type +open Tacmach + +(* This file containts the implementation of the tactics ``Decide + Equality'' and ``Compare''. They can be used to decide the + propositional equality of two objects that belongs to a small + inductive datatype --i.e., an inductive set such that all the + arguments of its constructors are non-functional sets. + + The procedure for proving (x,y:R){x=y}+{~x=y} can be scketched as + follows: + 1. Eliminate x and then y. + 2. Try discrimination to solve those goals where x and y has + been introduced by different constructors. + 3. If x and y have been introduced by the same constructor, + then analyse one by one the correspoing pairs of arguments. + If they are equal, rewrite one into the other. If they are + not, derive a contradiction from the injectiveness of the + constructor. + 4. Once all the arguments have been rewritten, solve the left half + of the disjunction by reflexivity. + + Eduardo Gimenez (30/3/98). +*) + +let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c)))) + +let mkBranches = + (tclTHEN intro + (tclTHEN (tclLAST_HYP h_simplest_elim) + (tclTHEN clear_last + (tclTHEN intros + (tclTHEN (tclLAST_HYP h_simplest_case) + (tclTHEN clear_last + intros)))))) + +let solveRightBranch = (tclTHEN h_simplest_right h_discrConcl) + +let h_solveRightBranch = + hide_atomic_tactic "solveRightBranch" solveRightBranch + + +(* Constructs the type {c1=c2}+{~c1=c2} *) + +let mmk = make_module_marker [ "Logic"; "Specif" ] +let eqpat = put_squel mmk "eq" +let sumboolpat = put_squel mmk "sumbool" +let notpat = put_squel mmk "not" + +let mkDecideEqGoal rectype c1 c2 g = + let equality = mkAppA [|get_squel eqpat;rectype;c1;c2|] in + let disequality = mkAppA [|get_squel notpat;equality|] in + mkAppA [|get_squel sumboolpat;equality;disequality |] + + +(* 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 rectype (mkVar xname) (mkVar yname) g))) + +let eqCase tac = + (tclTHEN intro + (tclTHEN (tclLAST_HYP h_rewriteLR) + (tclTHEN clear_last + tac))) + +let diseqCase = + let diseq = id_of_string "diseq" in + let absurd = id_of_string "absurd" in + (tclTHEN (intro_using diseq) + (tclTHEN h_simplest_right + (tclTHEN red_in_concl + (tclTHEN (intro_using absurd) + (tclTHEN (h_simplest_apply (mkVar diseq)) + (tclTHEN (h_injHyp absurd) + full_trivial)))))) + +let solveArg a1 a2 tac g = + let rectype = pf_type_of g a1 in + let decide = mkDecideEqGoal rectype a1 a2 g in + (tclTHENS + (h_elimType decide) + [(eqCase tac);diseqCase;default_auto]) g + +let conclpatt = lazy (get_pat (put_pat mmk "{<?1>?2=?3}+{?4}")) + +let solveLeftBranch rectype g = + match + try matches (Lazy.force conclpatt) (pf_concl g) + with Pattern.PatternMatchingFailure -> error "Unexpected conclusion!" + with + | _ :: lhs :: rhs :: _ -> + let nparams = Global.mind_nparams rectype in + let getargs l = snd (list_chop nparams (snd (decomp_app l))) in + let rargs = getargs (snd rhs) + and largs = getargs (snd lhs) in + List.fold_right2 + solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g + | _ -> anomaly "Unexpected pattern for solveLeftBranch" + + +(* The expected form of the goal for the tactic Decide Equality *) + +let initialpatt = lazy (get_pat (put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}")) + +(* The tactic Decide Equality *) + +let hd_app c = match kind_of_term c with + | IsApp (h,_) -> h + | _ -> c + +let decideGralEquality g = + match + try matches (Lazy.force initialpatt) (pf_concl g) + with Pattern.PatternMatchingFailure -> + error "The goal does not have the expected form" + with + | (_,typ) :: _ -> + let headtyp = hd_app (pf_compute g typ) in + let rectype = + match kind_of_term headtyp with + | IsMutInd mi -> mi + | _ -> error + "This decision procedure only works for inductive objects" + in + (tclTHEN + mkBranches + (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g + | _ -> anomaly "Unexpected pattern for decideGralEquality" + + +let decideEquality c1 c2 g = + let rectype = (pf_type_of g c1) in + let decide = mkGenDecideEqGoal rectype g in + (tclTHENS (cut decide) [default_auto;decideGralEquality]) g + + +(* The tactic Compare *) + +let compare c1 c2 g = + let rectype = pf_type_of g c1 in + let decide = mkDecideEqGoal rectype c1 c2 g in + (tclTHENS (cut decide) + [(tclTHEN intro + (tclTHEN (tclLAST_HYP simplest_case) + clear_last)); + decideEquality c1 c2]) g + + +(* The dynamic tactics to be registered in the tactics table *) + +let dyn_decideEquality args g = match args with + | [ Constr c1; Constr c2 ] -> + decideEquality c1 c2 g + | [ Command com1; Command com2 ] -> + let c1 = pf_interp_constr g com1 + and c2 = pf_interp_constr g com2 in + decideEquality c1 c2 g + | [] -> decideGralEquality g + | _ -> error "Invalid arguments for dynamic tactic" + +let dyn_compare args g = match args with + | [ Constr c1; Constr c2 ] -> + compare c1 c2 g + | [ Command com1; Command com2 ] -> + let c1 = pf_interp_constr g com1 + and c2 = pf_interp_constr g com2 in + compare c1 c2 g + | _ -> error "Invalid arguments for dynamic tactic" + + +(* Tactic registration *) + +let _ = add_tactic "DecideEquality" dyn_decideEquality +let _ = add_tactic "Compare" dyn_compare + + diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v new file mode 100644 index 000000000..f118bc830 --- /dev/null +++ b/test-suite/success/eqdecide.v @@ -0,0 +1,22 @@ + +Inductive T : Set := A: T | B :T->T. + +Lemma lem1 : (x,y:T){x=y}+{~x=y}. +Decide Equality. +Qed. + +Lemma lem2 : (x,y:T){x=y}+{~x=y}. +Intros x y. +Decide Equality x y. +Qed. + +Lemma lem3 : (x,y:T){x=y}+{~x=y}. +Intros x y. +Decide Equality y x. +Qed. + +Lemma lem4 : (x,y:T){x=y}+{~x=y}. +Intros x y. +Compare x y; Auto. +Qed. + |