From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 tactics/eqdecide.ml4 | 188 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 188 insertions(+)
 create mode 100644 tactics/eqdecide.ml4

(limited to 'tactics/eqdecide.ml4')

diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
new file mode 100644
index 00000000..8edfcb3e
--- /dev/null
+++ b/tactics/eqdecide.ml4
@@ -0,0 +1,188 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(************************************************************************)
+(*                              EqDecide                               *)
+(*   A tactic for deciding propositional equality on inductive types   *)
+(*                           by Eduardo Gimenez                        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id: eqdecide.ml4,v 1.6.2.1 2004/07/16 19:30:53 herbelin Exp $ *)
+
+open Util
+open Names
+open Nameops
+open Term
+open Declarations
+open Tactics
+open Tacticals
+open Hiddentac
+open Equality
+open Auto
+open Pattern
+open Matching
+open Hipattern
+open Proof_trees
+open Proof_type
+open Tacmach
+open Coqlib
+
+(* 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 [destVar c])))
+
+let mkBranches = 
+  tclTHENSEQ
+    [intro; 
+     tclLAST_HYP h_simplest_elim;
+     clear_last;
+     intros ;
+     tclLAST_HYP h_simplest_case;
+     clear_last;
+     intros]
+
+let solveRightBranch  = 
+  tclTHEN h_simplest_right
+    (tclTHEN (intro_force true)
+      (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id))))
+
+let h_solveRightBranch =
+  Refiner.abstract_extended_tactic "solveRightBranch" [] solveRightBranch
+
+(*
+let h_solveRightBranch =
+  hide_atomic_tactic "solveRightBranch" solveRightBranch
+*)
+
+(* Constructs the type {c1=c2}+{~c1=c2} *)
+
+let mkDecideEqGoal rectype c1 c2 g = 
+  let equality    = mkApp(build_coq_eq(), [|rectype; c1; c2|]) in
+  let disequality = mkApp(build_coq_not (), [|equality|]) in
+  mkApp(build_coq_sumbool (), [|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 Extratactics.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  (Extratactics.h_injHyp (Rawterm.NamedHyp 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_elim_type decide) 
+     [(eqCase tac);diseqCase;default_auto]) g
+
+let solveLeftBranch rectype g =
+  try
+    let (lhs,rhs) = match_eqdec_partial (pf_concl g) in
+    let (mib,mip) = Global.lookup_inductive rectype in
+    let nparams   = mip.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 largs rargs (tclTHEN h_simplest_left h_reflexivity) g
+  with PatternMatchingFailure -> error "Unexpected conclusion!"
+
+(* The tactic Decide Equality *)
+
+let hd_app c = match kind_of_term c with
+  | App (h,_) -> h
+  | _ -> c
+
+let decideGralEquality g =
+  try
+    let typ = match_eqdec (pf_concl g) in
+    let headtyp = hd_app (pf_compute g typ) in
+    let rectype =
+      match kind_of_term headtyp with
+        | Ind mi -> mi
+	| _ -> error "This decision procedure only works for inductive objects"
+    in 
+    (tclTHEN
+      mkBranches 
+      (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
+  with PatternMatchingFailure ->
+    error "The goal does not have the expected form"
+
+
+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
+
+
+(* User syntax *)
+
+TACTIC EXTEND DecideEquality
+  [ "Decide" "Equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ]
+| [ "Decide" "Equality" ] -> [ decideGralEquality ]
+END
+
+TACTIC EXTEND Compare
+| [ "Compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+END
+
-- 
cgit v1.2.3