Several bugs fixed in discriminate.

Discriminate now works on inductive types with any number of left or right
parameters.

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 7c5df0d82eafbbf9bfc7da73ddf573e405e72b12..69739a4b0ccd1f70a128c085b39914b720c3fcf4 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -306,8 +306,6 @@ let injection_tac =
  injection_tac ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)
 ;;
 
-exception TwoDifferentSubtermsFound of int 
-
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
 
@@ -357,33 +355,69 @@ let discriminate'_tac ~term =
    in
    aux t1 t2
  in
- let mk_pattern turi typeno consno context left_args =
+ 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,_,nr_ind_params,_)  ->
-        let _,_,_,constructor_list = List.nth ind_type_list typeno in 
+    | 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
-        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 <= nr_ind_params) ->
-                  CicSubstitution.subst (List.nth left_args (k-1))
-                    (aux target (k+1))
-              | C.Prod (binder,source,target) when (k > nr_ind_params) ->
-                  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
-    | _ -> (* object is not an inductive definition *)
-        assert false
+        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
@@ -393,14 +427,14 @@ let discriminate'_tac ~term =
     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,left_args = 
+   | 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)::left_args)) ->
-            turi,typeno,exp_named_subst,left_args
+        | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) ->
+            turi,typeno,exp_named_subst,args
         | _ -> fail "not a discriminable equality"
       in
       let consno =
@@ -408,43 +442,32 @@ let discriminate'_tac ~term =
         | Some consno -> consno
         | None -> fail "discriminating terms are structurally equal"
       in
-      let pattern = mk_pattern turi typeno consno context left_args in
-      let (proof',goals') = 
-        ProofEngineTypes.apply_tactic 
-          (EliminationTactics.elim_type_tac
-            (C.MutInd (false_URI, 0, [])))
-          status 
+      let branches,outtype =
+       mk_branches_and_outtype turi typeno consno context args
       in
-      (match goals' with
-      | [goal'] -> 
-          let _,metasenv',_,_ = proof' in
-          let _,context',gty' = CicUtil.lookup_meta goal' metasenv' in
-          ProofEngineTypes.apply_tactic
-            (T.then_
-              ~start:
-                (ReductionTactics.change_tac 
-                  ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
-                  (fun _ m u ->
-                    C.Appl [
-                      C.Lambda ( C.Name "x", tty,
-                        C.MutCase (turi, typeno,
-                          (C.Lambda ((C.Name "x"),
-                           (CicSubstitution.lift 1 tty),
-                           (C.Sort C.Prop))),
-                          (C.Rel 1), pattern));
-                      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)))
-            (proof',goal')
-      | [] -> fail "ElimType False left no goals"
-      | _ -> fail "ElimType False left more than one goal")
+      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)
@@ -458,155 +481,3 @@ let discriminate_tac ~term =
    status
  in
   ProofEngineTypes.mk_tactic (discriminate_tac ~term)
-
-(* DISCRIMINTATE SENZA INJECTION 
-
-exception TwoDifferentSubtermsFound of (Cic.term * Cic.term * int) 
-
-let discriminate_tac ~term status =
-  let module C = Cic in
-  let module U = UriManager in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-  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) in
-      match termty with
-         (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) 
-          when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) 
-            or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
-           match tty with
-              (C.MutInd (turi,typeno,exp_named_subst))
-            | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
-
-                let (t1',t2',consno2') = (* bruuutto: uso un eccezione per terminare con successo! buuu!! :-/ *)
-                 try
-                  let rec traverse t1 t2 =
-debug_print (lazy ("XXXX t1 " ^ CicPp.ppterm t1)) ;
-debug_print (lazy ("XXXX t2 " ^ CicPp.ppterm t2)) ;
-                   match t1,t2 with
-                      ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
-                       (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
-                         when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
-                       t1,t2,0
-                    | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
-                       (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2))) 
-                         when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
-                       let rec traverse_list l1 l2 =
-                         match l1,l2 with
-                            [],[] -> t1,t2,0
-                          | hd1::tl1,hd2::tl2 -> traverse hd1 hd2; traverse_list tl1 tl2
-                          | _ -> raise (ProofEngineTypes.Fail "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")
-                       in traverse_list applist1 applist2
-
-                    | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
-                       (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
-                    | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
-                       (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
-                    | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
-                       (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
-                    | ((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 (TwoDifferentSubtermsFound (t1,t2,consno2))
-                    | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
-                  in traverse t1 t2
-                 with (TwoDifferentSubtermsFound (t1,t2,consno2)) -> (t1,t2,consno2)
-                in
-debug_print (lazy ("XXXX consno2' " ^ (string_of_int consno2'))) ;
-                 if consno2' = 0 
-                  then raise (ProofEngineTypes.Fail "Discriminate: Discriminating terms are structurally equal")
-                  else
-
-                   let pattern = 
-                     (* a list of "True" except for the element in position consno2' which is "False" *)
-                     match fst(CicEnvironment.get_obj turi 
-                                 CicUniv.empty_ugraph) with
-                        C.InductiveDefinition (ind_type_list,_,nr_ind_params)  ->
-debug_print (lazy ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno))) ;
-                         let _,_,_,constructor_list = (List.nth ind_type_list typeno) in 
-debug_print (lazy ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2'))) ;
-                          let false_constr_id,_ = List.nth constructor_list (consno2' - 1) in
-debug_print (lazy "XXXX nth funzionano ") ;
-                           List.map 
-                            (function (id,cty) ->
-                              let red_ty = CicReduction.whd context cty in (* dubbio: e' corretto ridurre in questo context ??? *)
-                               let rec aux t k =
-                                match t with
-                                   C.Prod (_,_,target) when (k <= nr_ind_params) ->
-                                    aux target (k+1)
-                                 | C.Prod (binder,source,target) when (k > nr_ind_params) -> 
-                                    C.Lambda (binder,source,(aux target (k+1)))
-                                 | _ -> 
-                                    if (id = false_constr_id)
-                                     then (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [])
-                                     else (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/True.ind") 0 [])
-                               in aux red_ty 1
-                            ) 
-                            constructor_list
-                      | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible")
-                   in
-
-                    let (proof',goals') = 
-                     EliminationTactics.elim_type_tac 
-                      ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ) 
-                      status 
-                    in
-                     (match goals' with
-                         [goal'] -> 
-                          let _,metasenv',_,_ = proof' in
-                           let _,context',gty' =
-                             CicUtil.lookup_meta goal' metasenv'
-                           in
-                            T.then_
-                             ~start:
-                              (P.change_tac 
-                               ~what:gty' 
-                               ~with_what:
-                                (C.Appl [
-                                  C.Lambda (
-                                   C.Name "x", tty, 
-                                   C.MutCase (
-                                    turi, typeno,
-                                    (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
-                                    (C.Rel 1), pattern
-                                   )
-                                  ); 
-                                  t2']
-                                )
-                              )
-                             ~continuation:
-                              (
-debug_print (lazy ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))));
-debug_print (lazy ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))) ;
-debug_print (lazy ("XXXX equri: " ^ U.string_of_uri equri)) ;
-debug_print (lazy ("XXXX tty : " ^ CicPp.ppterm tty)) ;
-debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1'))) ;
-debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1'))) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ;
-if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> (CicTypeChecker.type_of_aux' metasenv' context' t2') 
- then debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux'
- metasenv' context' t1'))) ; debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ;
-
-                               let termty' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t1 ~with_what:t1' ~where:termty in
-                                let termty'' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t2 ~with_what:t2' ~where:termty' in
-
-debug_print (lazy ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term)));
-                                 T.then_
-                                   ~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term)
-                                   ~continuation:(IntroductionTactics.constructor_tac ~n:1) 
-                              )
-                             (proof',goal')
-                       | _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
-                     )    
-            | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
-           )
-       | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
-;;
-
-*)
-
-
-

diff --git a/helm/software/matita/tests/discriminate.ma b/helm/software/matita/tests/discriminate.ma
index d8e4bf2e25a84951c358c1437551c0d5a971d105..f25061245e8ad7da6fc240302b9770997d0b1246 100644 (file)
--- a/helm/software/matita/tests/discriminate.ma
+++ b/helm/software/matita/tests/discriminate.ma
@@ -17,9 +17,14 @@ include "legacy/coq.ma".
 alias id "not" = "cic:/Coq/Init/Logic/not.con".
 alias num (instance 0) = "natural number".
 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
 
 inductive foo: Prop \def I_foo: foo.
 
+alias num (instance 0) = "binary integer number".
 theorem stupid:
   1 = 0 \to (\forall p:Prop. p \to not p).
   intros.
@@ -31,10 +36,29 @@ inductive bar_list (A:Set): Set \def
   | bar_nil: bar_list A
   | bar_cons: A \to bar_list A \to bar_list A.
 
-alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+
 theorem stupid2:
   \forall A:Set.\forall x:A.\forall l:bar_list A.
   bar_nil A = bar_cons A x l \to False.
   intros.
   discriminate H.
 qed.
+
+inductive dt (A:Type): Type \to Type \def
+ | k1: \forall T:Type. dt A T
+ | k2: \forall T:Type. \forall T':Type. dt A (T \to T').
+ 
+theorem stupid3:
+ k1 False (False → True) = k2 False False True → False.
+ intros;
+ discriminate H.
+qed.
+
+inductive dddt (A:Type): Type \to Type \def
+ | kkk1: dddt A nat
+ | kkk2: dddt A nat.
+ 
+theorem stupid4: kkk1 False = kkk2 False \to False.
+ intros;
+ discriminate H.
+qed.
\ No newline at end of file