injection_tac and discriminate_tac now replaced by destruct_tac

diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index 69739a4b0ccd1f70a128c085b39914b720c3fcf4..9c5d002ca2720a3f3aecb0531f1cba705301d146 100644 (file)
--- a/components/tactics/discriminationTactics.ml
+++ b/components/tactics/discriminationTactics.ml
@@ -27,6 +27,173 @@
 
 let debug_print = fun _ -> ()
 
+(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
+diversi *)
+
+let discriminate_tac ~term =
+ let module C = Cic in
+ let module U = UriManager in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ let true_URI =
+  match LibraryObjects.true_URI () with
+     Some uri -> uri
+   | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
+ let false_URI =
+  match LibraryObjects.false_URI () with
+     Some uri -> uri
+   | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
+ let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
+ let find_discriminating_consno t1 t2 =
+   let rec aux t1 t2 =
+     match t1, t2 with
+     | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None
+     | C.Appl ((C.MutConstruct _ as constr1) :: args1),
+       C.Appl ((C.MutConstruct _ as constr2) :: args2)
+       when constr1 = constr2 ->
+         let rec aux_list l1 l2 =
+           match l1, l2 with
+           | [], [] -> None
+           | hd1 :: tl1, hd2 :: tl2 ->
+               (match aux hd1 hd2 with
+               | None -> aux_list tl1 tl2
+               | Some _ as res -> res)
+           | _ -> (* same constructor applied to a different number of args *)
+               assert false
+         in
+         aux_list args1 args2
+     | ((C.MutConstruct (_,_,consno1,subst1)),
+       (C.MutConstruct (_,_,consno2,subst2)))
+     | ((C.MutConstruct (_,_,consno1,subst1)),
+       (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
+     | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
+       (C.MutConstruct (_,_,consno2,subst2)))
+     | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
+       (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
+       when (consno1 <> consno2) || (subst1 <> subst2) ->
+         Some consno2
+     | _ -> fail "not a discriminable equality"
+   in
+   aux t1 t2
+ in
+ let mk_branches_and_outtype turi typeno consno context args =
+    (* a list of "True" except for the element in position consno which
+     * is "False" *)
+    match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
+    | C.InductiveDefinition (ind_type_list,_,paramsno,_)  ->
+        let _,_,rty,constructor_list = List.nth ind_type_list typeno in 
+        let false_constr_id,_ = List.nth constructor_list (consno - 1) in
+        let branches =
+         List.map 
+           (fun (id,cty) ->
+             (* dubbio: e' corretto ridurre in questo context ??? *)
+             let red_ty = CicReduction.whd context cty in
+             let rec aux t k =
+               match t with
+               | C.Prod (_,_,target) when (k <= paramsno) ->
+                   CicSubstitution.subst (List.nth args (k-1))
+                     (aux target (k+1))
+               | C.Prod (binder,source,target) when (k > paramsno) ->
+                   C.Lambda (binder, source, (aux target (k+1)))
+               | _ -> 
+                   if (id = false_constr_id)
+                   then (C.MutInd(false_URI,0,[]))
+                   else (C.MutInd(true_URI,0,[]))
+             in
+             (CicSubstitution.lift 1 (aux red_ty 1)))
+           constructor_list in
+        let outtype =
+         let seed = ref 0 in
+         let rec mk_lambdas rev_left_args =
+          function
+             0, args, C.Prod (_,so,ta) ->
+              C.Lambda
+               (C.Name (incr seed; "x" ^ string_of_int !seed),
+               so,
+               mk_lambdas rev_left_args (0,args,ta))
+           | 0, args, C.Sort _ ->
+              let rec mk_rels =
+               function
+                  0 -> []
+                | n -> C.Rel n :: mk_rels (n - 1) in
+              let argsno = List.length args in
+               C.Lambda
+                (C.Name "x",
+                 (if argsno + List.length rev_left_args > 0 then
+                   C.Appl
+                    (C.MutInd (turi, typeno, []) ::
+                     (List.map
+                      (CicSubstitution.lift (argsno + 1))
+                      (List.rev rev_left_args)) @
+                     mk_rels argsno)
+                  else
+                   C.MutInd (turi,typeno,[])),
+                 C.Sort C.Prop)
+           | 0, _, _ -> assert false (* seriously screwed up *)
+           | n, he::tl, C.Prod (_,_,ta) ->
+              mk_lambdas (he::rev_left_args)(n-1,tl,CicSubstitution.subst he ta)
+           | n,_,_ ->
+              assert false (* we should probably reduce in some context *)
+         in
+          mk_lambdas [] (paramsno, args, rty)
+        in
+         branches, outtype 
+    | _ -> assert false
+ in
+ let discriminate'_tac ~term status = 
+  let (proof, goal) = status in
+  let _,metasenv,_,_ = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let termty,_ = 
+    CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+  in
+  match termty with
+   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
+     when LibraryObjects.is_eq_URI equri ->
+      let turi,typeno,exp_named_subst,args = 
+        match tty with
+        | (C.MutInd (turi,typeno,exp_named_subst)) ->
+            turi,typeno,exp_named_subst,[]
+        | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) ->
+            turi,typeno,exp_named_subst,args
+        | _ -> fail "not a discriminable equality"
+      in
+      let consno =
+        match find_discriminating_consno t1 t2 with
+        | Some consno -> consno
+        | None -> fail "discriminating terms are structurally equal"
+      in
+      let branches,outtype =
+       mk_branches_and_outtype turi typeno consno context args
+      in
+      ProofEngineTypes.apply_tactic
+       (T.then_
+         ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
+         ~continuation:
+           (T.then_
+             ~start:
+               (ReductionTactics.change_tac 
+                 ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                 (fun _ m u ->
+                   C.Appl [
+                     C.Lambda ( C.Name "x", tty,
+                       C.MutCase (turi, typeno, outtype, (C.Rel 1), branches));
+                     t2 ],
+                   m, u))
+             ~continuation:
+               (T.then_
+                 ~start:
+                   (EqualityTactics.rewrite_simpl_tac
+                     ~direction:`RightToLeft
+                     ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                     term)
+                 ~continuation:
+                   (IntroductionTactics.constructor_tac ~n:1)))) status
+    | _ -> fail "not an equality"
+  in
+  ProofEngineTypes.mk_tactic (discriminate'_tac ~term)
+;;
+
 let rec injection_tac ~first_time ~term ~liftno ~continuation =
  let injection_tac ~term status = 
   let (proof, goal) = status in
@@ -99,7 +266,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation =
                            else
                             injection1_tac ~i ~term
                              ~continuation:(traverse_list (i+1) tl1 tl2)
-                        | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
+                        | _ -> assert false (* i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini *)
                      in
                       traverse_list 1 applist1 applist2 ~liftno
                  | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
@@ -111,7 +278,8 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation =
                  | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
                     (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
                       when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) ->
-                    raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one"))
+                    discriminate_tac ~term
+                    (*raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one"))*)
                  | _ ->
                    if first_time then
                     raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
@@ -302,182 +470,9 @@ and injection1_tac ~term ~i ~liftno ~continuation =
   ProofEngineTypes.mk_tactic (injection1_tac ~term ~i)
 ;;
 
-let injection_tac =
- injection_tac ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)
+(* destruct performs either injection or discriminate *)
+(* equivalent to Coq's "analyze equality"             *)
+let destruct_tac =
+ injection_tac
+  ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)
 ;;
-
-(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
-diversi *)
-
-let discriminate'_tac ~term =
- let module C = Cic in
- let module U = UriManager in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let true_URI =
-  match LibraryObjects.true_URI () with
-     Some uri -> uri
-   | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
- let false_URI =
-  match LibraryObjects.false_URI () with
-     Some uri -> uri
-   | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
- let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
- let find_discriminating_consno t1 t2 =
-   let rec aux t1 t2 =
-     match t1, t2 with
-     | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None
-     | C.Appl ((C.MutConstruct _ as constr1) :: args1),
-       C.Appl ((C.MutConstruct _ as constr2) :: args2)
-       when constr1 = constr2 ->
-         let rec aux_list l1 l2 =
-           match l1, l2 with
-           | [], [] -> None
-           | hd1 :: tl1, hd2 :: tl2 ->
-               (match aux hd1 hd2 with
-               | None -> aux_list tl1 tl2
-               | Some _ as res -> res)
-           | _ -> (* same constructor applied to a different number of args *)
-               assert false
-         in
-         aux_list args1 args2
-     | ((C.MutConstruct (_,_,consno1,subst1)),
-       (C.MutConstruct (_,_,consno2,subst2)))
-     | ((C.MutConstruct (_,_,consno1,subst1)),
-       (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
-     | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
-       (C.MutConstruct (_,_,consno2,subst2)))
-     | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
-       (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
-       when (consno1 <> consno2) || (subst1 <> subst2) ->
-         Some consno2
-     | _ -> fail "not a discriminable equality"
-   in
-   aux t1 t2
- in
- let mk_branches_and_outtype turi typeno consno context args =
-    (* a list of "True" except for the element in position consno which
-     * is "False" *)
-    match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
-    | C.InductiveDefinition (ind_type_list,_,paramsno,_)  ->
-        let _,_,rty,constructor_list = List.nth ind_type_list typeno in 
-        let false_constr_id,_ = List.nth constructor_list (consno - 1) in
-        let branches =
-         List.map 
-           (fun (id,cty) ->
-             (* dubbio: e' corretto ridurre in questo context ??? *)
-             let red_ty = CicReduction.whd context cty in
-             let rec aux t k =
-               match t with
-               | C.Prod (_,_,target) when (k <= paramsno) ->
-                   CicSubstitution.subst (List.nth args (k-1))
-                     (aux target (k+1))
-               | C.Prod (binder,source,target) when (k > paramsno) ->
-                   C.Lambda (binder, source, (aux target (k+1)))
-               | _ -> 
-                   if (id = false_constr_id)
-                   then (C.MutInd(false_URI,0,[]))
-                   else (C.MutInd(true_URI,0,[]))
-             in
-             (CicSubstitution.lift 1 (aux red_ty 1)))
-           constructor_list in
-        let outtype =
-         let seed = ref 0 in
-         let rec mk_lambdas rev_left_args =
-          function
-             0, args, C.Prod (_,so,ta) ->
-              C.Lambda
-               (C.Name (incr seed; "x" ^ string_of_int !seed),
-               so,
-               mk_lambdas rev_left_args (0,args,ta))
-           | 0, args, C.Sort _ ->
-              let rec mk_rels =
-               function
-                  0 -> []
-                | n -> C.Rel n :: mk_rels (n - 1) in
-              let argsno = List.length args in
-               C.Lambda
-                (C.Name "x",
-                 (if argsno + List.length rev_left_args > 0 then
-                   C.Appl
-                    (C.MutInd (turi, typeno, []) ::
-                     (List.map
-                      (CicSubstitution.lift (argsno + 1))
-                      (List.rev rev_left_args)) @
-                     mk_rels argsno)
-                  else
-                   C.MutInd (turi,typeno,[])),
-                 C.Sort C.Prop)
-           | 0, _, _ -> assert false (* seriously screwed up *)
-           | n, he::tl, C.Prod (_,_,ta) ->
-              mk_lambdas (he::rev_left_args)(n-1,tl,CicSubstitution.subst he ta)
-           | n,_,_ ->
-              assert false (* we should probably reduce in some context *)
-         in
-          mk_lambdas [] (paramsno, args, rty)
-        in
-         branches, outtype 
-    | _ -> assert false
- in
- let discriminate'_tac ~term status = 
-  let (proof, goal) = status in
-  let _,metasenv,_,_ = proof in
-  let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let termty,_ = 
-    CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
-  in
-  match termty with
-   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
-     when LibraryObjects.is_eq_URI equri ->
-      let turi,typeno,exp_named_subst,args = 
-        match tty with
-        | (C.MutInd (turi,typeno,exp_named_subst)) ->
-            turi,typeno,exp_named_subst,[]
-        | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) ->
-            turi,typeno,exp_named_subst,args
-        | _ -> fail "not a discriminable equality"
-      in
-      let consno =
-        match find_discriminating_consno t1 t2 with
-        | Some consno -> consno
-        | None -> fail "discriminating terms are structurally equal"
-      in
-      let branches,outtype =
-       mk_branches_and_outtype turi typeno consno context args
-      in
-      ProofEngineTypes.apply_tactic
-       (T.then_
-         ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
-         ~continuation:
-           (T.then_
-             ~start:
-               (ReductionTactics.change_tac 
-                 ~pattern:(ProofEngineTypes.conclusion_pattern None)
-                 (fun _ m u ->
-                   C.Appl [
-                     C.Lambda ( C.Name "x", tty,
-                       C.MutCase (turi, typeno, outtype, (C.Rel 1), branches));
-                     t2 ],
-                   m, u))
-             ~continuation:
-               (T.then_
-                 ~start:
-                   (EqualityTactics.rewrite_simpl_tac
-                     ~direction:`RightToLeft
-                     ~pattern:(ProofEngineTypes.conclusion_pattern None)
-                     term)
-                 ~continuation:
-                   (IntroductionTactics.constructor_tac ~n:1)))) status
-    | _ -> fail "not an equality"
-  in
-  ProofEngineTypes.mk_tactic (discriminate'_tac ~term)
-
-let discriminate_tac ~term = 
- let discriminate_tac ~term status =
-  ProofEngineTypes.apply_tactic 
-  (Tacticals.then_
-    ~start:(* (injection_tac ~term) *) Tacticals.id_tac
-    ~continuation:(discriminate'_tac ~term)) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *)
-   status
- in
-  ProofEngineTypes.mk_tactic (discriminate_tac ~term)

diff --git a/components/tactics/discriminationTactics.mli b/components/tactics/discriminationTactics.mli
index 5815bb551a0d5c34e4a0b2c59f8339a2a53cd7a9..3a74e3d7df7abaf7935482e8c1b8fb4d64f9013b 100644 (file)
--- a/components/tactics/discriminationTactics.mli
+++ b/components/tactics/discriminationTactics.mli
@@ -23,5 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val injection_tac: term:Cic.term -> ProofEngineTypes.tactic
-val discriminate_tac: term:Cic.term -> ProofEngineTypes.tactic
+(* Performs a recursive comparisons of the two sides of an equation
+   looking for constructors. If the two sides differ on two constructors,
+   it closes the current goal. If they differ by other two terms it introduces
+   an equality. *)
+val destruct_tac: term:Cic.term -> ProofEngineTypes.tactic

diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml
index 4676d2d10c6217214abae20e46a444afcc86058c..5a2cc0e16978c792b1c0f53fc1c49f79f9e38f42 100644 (file)
--- a/components/tactics/tactics.ml
+++ b/components/tactics/tactics.ml
@@ -38,7 +38,7 @@ let contradiction = NegationTactics.contradiction_tac
 let cut = PrimitiveTactics.cut_tac
 let decompose = EliminationTactics.decompose_tac
 let demodulate = Saturation.demodulate_tac
-let discriminate = DiscriminationTactics.discriminate_tac
+let destruct = DiscriminationTactics.destruct_tac
 let elim_intros = PrimitiveTactics.elim_intros_tac
 let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
 let elim_type = EliminationTactics.elim_type_tac
@@ -50,7 +50,6 @@ let fourier = FourierR.fourier_tac
 let fwd_simpl = FwdSimplTactic.fwd_simpl_tac
 let generalize = VariousTactics.generalize_tac
 let id = Tacticals.id_tac
-let injection = DiscriminationTactics.injection_tac
 let intros = PrimitiveTactics.intros_tac
 let inversion = Inversion.inversion_tac
 let lapply = FwdSimplTactic.lapply_tac

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 862f781618cb55f34fed68f433970db769355490..a5d6f00862a468df0a9c6642b3064779ab5d8940 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Aug 31 14:46:00 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Sep 25 18:28:48 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
@@ -20,7 +20,7 @@ val decompose :
   ?user_types:(UriManager.uri * int) list ->
   ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
 val demodulate : dbd:HMysql.dbd -> ProofEngineTypes.tactic
-val discriminate : term:Cic.term -> ProofEngineTypes.tactic
+val destruct : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
@@ -45,7 +45,6 @@ val generalize :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val id : ProofEngineTypes.tactic
-val injection : term:Cic.term -> ProofEngineTypes.tactic
 val intros :
   ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->