EqDecide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1336 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 255 insertions, 2 deletions

diff --git a/Makefile b/Makefile
index 0f65fc7a2..33a7321e9 100644
--- a/Makefile
+++ b/Makefile
@@ -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.
+