bug fix in subst tactic

diff --git a/components/tactics/.depend b/components/tactics/.depend
index bac580671fa8e2eb127ba90dac0e914569184089..6908172de23b282e61ae6012fd8db0454dfc606a 100644 (file)
--- a/components/tactics/.depend
+++ b/components/tactics/.depend
@@ -1,6 +1,6 @@
 proofEngineHelpers.cmi: proofEngineTypes.cmi 
 continuationals.cmi: proofEngineTypes.cmi 
-tacticals.cmi: proofEngineTypes.cmi continuationals.cmi 
+tacticals.cmi: proofEngineTypes.cmi 
 reductionTactics.cmi: proofEngineTypes.cmi 
 proofEngineStructuralRules.cmi: proofEngineTypes.cmi 
 primitiveTactics.cmi: proofEngineTypes.cmi 
@@ -31,7 +31,7 @@ setoids.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
-tactics.cmi: universe.cmi proofEngineTypes.cmi 
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi 
 declarative.cmi: universe.cmi proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
@@ -155,12 +155,12 @@ discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
     proofEngineTypes.cmx proofEngineStructuralRules.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi 
-substTactic.cmo: tacticals.cmi proofEngineTypes.cmi \
+substTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \
-    substTactic.cmi 
-substTactic.cmx: tacticals.cmx proofEngineTypes.cmx \
+    discriminationTactics.cmi substTactic.cmi 
+substTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
     proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \
-    substTactic.cmi 
+    discriminationTactics.cmx substTactic.cmi 
 inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     equalityTactics.cmi inversion.cmi 
@@ -199,18 +199,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \
     statefulProofEngine.cmi 
 statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \
     statefulProofEngine.cmi 
-tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi ring.cmi \
-    reductionTactics.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
-    negationTactics.cmi inversion.cmi introductionTactics.cmi \
-    fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \
-    eliminationTactics.cmi discriminationTactics.cmi autoTactic.cmi auto.cmi \
-    tactics.cmi 
-tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
-    reductionTactics.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
-    negationTactics.cmx inversion.cmx introductionTactics.cmx \
-    fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
-    eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \
-    tactics.cmi 
+tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \
+    ring.cmi reductionTactics.cmi proofEngineStructuralRules.cmi \
+    primitiveTactics.cmi negationTactics.cmi inversion.cmi \
+    introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \
+    equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \
+    autoTactic.cmi auto.cmi tactics.cmi 
+tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \
+    ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \
+    primitiveTactics.cmx negationTactics.cmx inversion.cmx \
+    introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
+    equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
+    autoTactic.cmx auto.cmx tactics.cmi 
 declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
 declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \

diff --git a/components/tactics/.depend.opt b/components/tactics/.depend.opt
index bac580671fa8e2eb127ba90dac0e914569184089..6908172de23b282e61ae6012fd8db0454dfc606a 100644 (file)
--- a/components/tactics/.depend.opt
+++ b/components/tactics/.depend.opt
@@ -1,6 +1,6 @@
 proofEngineHelpers.cmi: proofEngineTypes.cmi 
 continuationals.cmi: proofEngineTypes.cmi 
-tacticals.cmi: proofEngineTypes.cmi continuationals.cmi 
+tacticals.cmi: proofEngineTypes.cmi 
 reductionTactics.cmi: proofEngineTypes.cmi 
 proofEngineStructuralRules.cmi: proofEngineTypes.cmi 
 primitiveTactics.cmi: proofEngineTypes.cmi 
@@ -31,7 +31,7 @@ setoids.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
-tactics.cmi: universe.cmi proofEngineTypes.cmi 
+tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi 
 declarative.cmi: universe.cmi proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
@@ -155,12 +155,12 @@ discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
     proofEngineTypes.cmx proofEngineStructuralRules.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi 
-substTactic.cmo: tacticals.cmi proofEngineTypes.cmi \
+substTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineStructuralRules.cmi proofEngineHelpers.cmi equalityTactics.cmi \
-    substTactic.cmi 
-substTactic.cmx: tacticals.cmx proofEngineTypes.cmx \
+    discriminationTactics.cmi substTactic.cmi 
+substTactic.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
     proofEngineStructuralRules.cmx proofEngineHelpers.cmx equalityTactics.cmx \
-    substTactic.cmi 
+    discriminationTactics.cmx substTactic.cmi 
 inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     equalityTactics.cmi inversion.cmi 
@@ -199,18 +199,18 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \
     statefulProofEngine.cmi 
 statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \
     statefulProofEngine.cmi 
-tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi ring.cmi \
-    reductionTactics.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
-    negationTactics.cmi inversion.cmi introductionTactics.cmi \
-    fwdSimplTactic.cmi fourierR.cmi equalityTactics.cmi \
-    eliminationTactics.cmi discriminationTactics.cmi autoTactic.cmi auto.cmi \
-    tactics.cmi 
-tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx ring.cmx \
-    reductionTactics.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
-    negationTactics.cmx inversion.cmx introductionTactics.cmx \
-    fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
-    eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \
-    tactics.cmi 
+tactics.cmo: variousTactics.cmi tacticals.cmi substTactic.cmi setoids.cmi \
+    ring.cmi reductionTactics.cmi proofEngineStructuralRules.cmi \
+    primitiveTactics.cmi negationTactics.cmi inversion.cmi \
+    introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \
+    equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \
+    autoTactic.cmi auto.cmi tactics.cmi 
+tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \
+    ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \
+    primitiveTactics.cmx negationTactics.cmx inversion.cmx \
+    introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
+    equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
+    autoTactic.cmx auto.cmx tactics.cmi 
 declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
     declarative.cmi 
 declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \

diff --git a/components/tactics/substTactic.ml b/components/tactics/substTactic.ml
index 1c01246485443179fe9eaac7eeb098f7272d2d8b..fd11631ac6343f4cb2368e1054e0210cfcbae1ed 100644 (file)
--- a/components/tactics/substTactic.ml
+++ b/components/tactics/substTactic.ml
@@ -24,6 +24,7 @@
  *)
 
 module C    = Cic
+module DT   = DiscriminationTactics
 module DTI  = DoubleTypeInference
 module ET   = EqualityTactics
 module HEL  = HExtlib
@@ -31,36 +32,46 @@ module LO   = LibraryObjects
 module PEH  = ProofEngineHelpers
 module PESR = ProofEngineStructuralRules
 module PET  = ProofEngineTypes
+module RT   = ReductionTactics
 module S    = CicSubstitution
 module T    = Tacticals
 module TC   = CicTypeChecker
 
-(* FG: This should be replaced by T.try_tactic *)
-let try_tactic ~tactic =
-   let try_tactic status =
-      try PET.apply_tactic tactic status with
-         | PET.Fail _ -> PET.apply_tactic T.id_tac status
-   in
-   PET.mk_tactic try_tactic
-
-let rec lift_rewrite_tac ~context ~direction ~pattern equality =
+let lift_rewrite_tac ~context ~direction ~pattern equality =
    let lift_rewrite_tac status =
       let (proof, goal) = status in
       let (_, metasenv, _, _, _) = proof in
       let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
       let n = List.length new_context - List.length context in
-      let equality = if n > 0 then S.lift n equality else equality in
+      let equality = S.lift n equality in
       PET.apply_tactic (ET.rewrite_tac ~direction ~pattern equality []) status
    in
    PET.mk_tactic lift_rewrite_tac
 
-
+let lift_destruct_tac ~context ~what =
+   let lift_destruct_tac status =
+      let (proof, goal) = status in
+      let (_, metasenv, _, _, _) = proof in
+      let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
+      let n = List.length new_context - List.length context in
+      let what = S.lift n what in
+      PET.apply_tactic (DT.destruct_tac ~term:what) status
+   in
+   PET.mk_tactic lift_destruct_tac
+      
 let msg0 = lazy "Subst: not found in context"
-let msg1 = lazy "Subst: not a simple equality"
+let msg1 = lazy "Subst: not an erasable equation"
 let msg2 = lazy "Subst: recursive equation" 
+let msg3 = lazy "Subst: no progress" 
 
-let subst_tac ~hyp =
+let rec subst_tac ~try_tactic ~hyp =
    let hole = C.Implicit (Some `Hole) in
+   let meta = C.Implicit None in
+   let rec constr = function
+      | C.MutConstruct _ -> true
+      | C.Appl (t :: tl) -> constr t
+      | _                -> false
+   in
    let subst_tac status =
       let (proof, goal) = status in
       let (_, metasenv, _, _, _) = proof in
@@ -70,46 +81,84 @@ let subst_tac ~hyp =
         | None   -> raise (PET.Fail msg0)
       in
       let ty, _ = TC.type_of_aux' metasenv context what CicUniv.empty_ugraph in
-      let direction, i, t = match ty with
+      let subst_g direction i t =
+         let rewrite pattern =
+            let tactic = lift_rewrite_tac ~context ~direction ~pattern what in
+           try_tactic ~tactic
+         in
+         let var = match PEH.get_name context i with
+            | Some name -> name
+           | None      -> raise (PET.Fail msg0)        
+         in
+         if DTI.does_not_occur i t then () else raise (PET.Fail msg2);
+         let map self = function
+            | Some (C.Name s, _) when s <> self -> 
+               Some (rewrite (None, [(s, hole)], None))
+            | _                                 -> None
+         in
+         let rew_hips = HEL.list_rev_map_filter (map hyp) context in
+         let rew_concl = rewrite (None, [], Some hole) in
+         let clear = PESR.clear ~hyps:[hyp; var] in
+         List.rev_append (rew_concl :: rew_hips) [clear]
+      in
+      let destruct_g () =
+         [lift_destruct_tac ~context ~what; PESR.clear ~hyps:[hyp]]
+      in
+      let whd_g () =
+         let whd_pattern = C.Appl [meta; meta; hole; hole] in
+        let pattern = None, [hyp, whd_pattern], None in
+        [RT.whd_tac ~pattern; subst_tac ~try_tactic ~hyp]
+      in
+      let tactics = match ty with
          | (C.Appl [(C.MutInd (uri, 0, [])); _; C.Rel i; t]) 
-           when LO.is_eq_URI uri -> `LeftToRight, i, t
+           when LO.is_eq_URI uri -> subst_g `LeftToRight i t
          | (C.Appl [(C.MutInd (uri, 0, [])); _; t; C.Rel i]) 
-           when LO.is_eq_URI uri -> `RightToLeft, i, t
+           when LO.is_eq_URI uri -> subst_g `RightToLeft i t
+        | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) 
+           when LO.is_eq_URI uri && constr t1 && constr t2 -> destruct_g ()
+        | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2])
+           when LO.is_eq_URI uri -> whd_g ()    
         | _ -> raise (PET.Fail msg1)
-      in    
-      let rewrite pattern =
-         let tactic = lift_rewrite_tac ~context ~direction ~pattern what in
-        try_tactic ~tactic
       in
-      let var = match PEH.get_name context i with
-         | Some name -> name
-        | None      -> raise (PET.Fail msg0)   
-      in
-      if DTI.does_not_occur i t then () else raise (PET.Fail msg2);
-      let map self = function
-         | Some (C.Name s, _) when s <> self -> 
-            Some (rewrite (None, [(s, hole)], None))
-         | _                                 -> None
-      in
-      let rew_hips = HEL.list_rev_map_filter (map hyp) context in
-      let rew_concl = rewrite (None, [], Some hole) in
-      let clear = PESR.clear ~hyps:[hyp; var] in
-      let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in
       PET.apply_tactic (T.seq ~tactics) status
    in
    PET.mk_tactic subst_tac
 
 let subst_tac =
-   let subst hyp = try_tactic ~tactic:(subst_tac hyp) in
-   let map = function
-      | Some (C.Name s, _) -> Some (subst s)
-      | _                  -> None
-   in
    let subst_tac status =
+      let progress = ref false in
+      let try_tactic ~tactic =
+         let try_tactic status =
+            try 
+              let result = PET.apply_tactic tactic status in
+              progress := true; result
+           with
+               | PET.Fail _ -> PET.apply_tactic T.id_tac status
+         in
+         PET.mk_tactic try_tactic
+      in
+      let subst hyp = try_tactic ~tactic:(subst_tac ~try_tactic ~hyp) in
+      let map = function
+         | Some (C.Name s, _) -> Some (subst s)
+         | _                  -> None
+      in
       let (proof, goal) = status in
       let (_, metasenv, _, _, _) = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let tactics = HEL.list_rev_map_filter map context in
-      PET.apply_tactic (T.seq ~tactics) status
+      let result = PET.apply_tactic (T.seq ~tactics) status in
+      if !progress then result else raise (PET.Fail msg3)
    in
    PET.mk_tactic subst_tac
+
+   let try_tac tactic = T.try_tactic ~tactic 
+   let then_tac start continuation = T.then_ ~start ~continuation 
+
+let rec repeat_tactic ~tactic =
+   try_tac (then_tac tactic (repeat_tactic ~tactic))
+
+let subst_tac = 
+   let subst_tac status =
+      PET.apply_tactic (repeat_tactic ~tactic:subst_tac) status
+   in 
+   PET.mk_tactic subst_tac

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 34bc2d4f361907d667c62ccc818ae0b4fa3d5854..81e19bcece8544038fcc9ea8b945627085efd0c5 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Apr 20 17:07:53 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Apr 26 15:04:41 CEST 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :