components/tactics/discriminationTactics.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 let debug_print = fun _ -> ()
  29
  30 let rec injection_tac ~term =
  31  let injection_tac ~term status =
  32   let (proof, goal) = status in
  33   let module C = Cic in
  34   let module U = UriManager in
  35   let module P = PrimitiveTactics in
  36   let module T = Tacticals in
  37   let _,metasenv,_,_ = proof in
  38   let _,context,_ = CicUtil.lookup_meta goal metasenv in
  39   let termty,_ = (* TASSI: FIXME *)
  40     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
  41   in
  42     ProofEngineTypes.apply_tactic
  43       (match termty with
  44           (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
  45              when LibraryObjects.is_eq_URI equri -> (
  46            match tty with
  47               (C.MutInd (turi,typeno,exp_named_subst))
  48             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
  49                    match t1,t2 with
  50                       ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
  51                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
  52                          when (uri1 = uri2) && (typeno1 = typeno2) &&
  53                               (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
  54                        (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) T.id_tac
  55                     | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
  56                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
  57                          when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
  58                        let rec traverse_list i l1 l2 =
  59                          match l1,l2 with
  60                             [],[] -> T.id_tac
  61                           | hd1::tl1,hd2::tl2 ->
  62                              T.then_
  63                               ~start:
  64                                 (injection1_tac ~i
  65                                   ~term:(CicSubstitution.lift (i-1) term))
  66                               ~continuation:(traverse_list (i+1) tl1 tl2)
  67                           | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
  68                        in traverse_list 1 applist1 applist2
  69                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
  70                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
  71                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
  72                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
  73                     | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
  74                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
  75                     | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
  76                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
  77                          when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) ->
  78                        (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality but a discriminable one") ; *) T.id_tac
  79                     | _ -> (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality") ; *) T.id_tac
  80                    )
  81             | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
  82            )
  83         | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation"))
  84       ) status
  85  in
  86   ProofEngineTypes.mk_tactic (injection_tac ~term)
  87
  88 and injection1_tac ~term ~i =
  89  let injection1_tac ~term ~i status =
  90   let (proof, goal) = status in
  91   (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *)
  92    let module C = Cic in
  93    let module S = CicSubstitution in
  94    let module U = UriManager in
  95    let module P = PrimitiveTactics in
  96    let module T = Tacticals in
  97    let _,metasenv,_,_ = proof in
  98    let _,context,_ = CicUtil.lookup_meta goal metasenv in
  99    let termty,_ = (* TASSI: FIXME *)
 100      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
 101      match termty with (* an equality *)
 102          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
 103              when LibraryObjects.is_eq_URI equri -> (
 104            match tty with (* some inductive type *)
 105               (C.MutInd (turi,typeno,exp_named_subst))
 106             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
 107                let t1',t2',consno = (* sono i due sottotermini che differiscono *)
 108                 match t1,t2 with
 109                    ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
 110                     (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
 111                       when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* controllo ridondante *)
 112                     (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2
 113                  | _ -> assert false
 114                in
 115                 let tty',_ =
 116                   CicTypeChecker.type_of_aux' metasenv context t1'
 117                     CicUniv.empty_ugraph  in
 118                 let patterns,outtype =
 119                  match
 120                   fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi)
 121                  with
 122                     C.InductiveDefinition (ind_type_list,_,paramsno,_)->
 123                      let _,_,_,constructor_list =
 124                       List.nth ind_type_list typeno in
 125                      let i_constr_id,_ =
 126                       List.nth constructor_list (consno - 1) in
 127                      let patterns =
 128                       List.map
 129                        (function (id,cty) ->
 130                          let reduced_cty = CicReduction.whd context cty in
 131                           let rec aux t k =
 132                            match t with
 133                               C.Prod (_,_,target) when k <= paramsno ->
 134                                aux target (k+1)
 135                             | C.Prod (binder,source,target) when k > paramsno ->
 136                                let binder' =
 137                                 match binder with
 138                                    C.Name b -> C.Name b
 139                                  | C.Anonymous -> C.Name "y"
 140                                in
 141                                 C.Lambda (binder',source,(aux target (k+1)))
 142                             | _ ->
 143                                let nr_param_constr = k - 1 - paramsno in
 144                                 if id = i_constr_id
 145                                  then C.Rel (nr_param_constr - i + 1)
 146                                  else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda aggiunto esternamente al case *)
 147                           in aux reduced_cty 1
 148                        ) constructor_list in
 149                      let outtype =
 150                       let rec to_lambdas te head =
 151                        match CicReduction.whd context te with
 152                         | C.Prod (name,so,ta) ->
 153                            C.Lambda (name,so,to_lambdas ta head)
 154                         | _ -> head in
 155                       let rec skip_prods n te =
 156                        match n, CicReduction.whd context te with
 157                           0, _ -> te
 158                         | n, C.Prod (_,_,ta) -> skip_prods (n - 1) ta
 159                         | _, _ -> assert false
 160                       in
 161                        let abstracted_tty =
 162                         match CicSubstitution.lift (paramsno + 1) tty with
 163                            C.MutInd _ as tty' -> tty'
 164                          | C.Appl l ->
 165                              let keep,abstract =
 166                               HExtlib.split_nth (paramsno +1) l in
 167                              let rec mk_rels =
 168                               function
 169                                  0 -> []
 170                                | n -> C.Rel n :: (mk_rels (n - 1))
 171                              in
 172                               C.Appl (keep@mk_rels (List.length abstract))
 173                          | _ -> assert false
 174                        in
 175                         match ind_type_list with
 176                            [] -> assert false
 177                          | (_,_,ty,_)::_ ->
 178                             to_lambdas (skip_prods paramsno ty)
 179                              (C.Lambda (C.Name "x", abstracted_tty,
 180                                S.lift (2+paramsno) tty'))
 181                       in
 182                        patterns,outtype
 183                   | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible"))
 184                 in
 185                 ProofEngineTypes.apply_tactic
 186                  (T.thens
 187                   ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2']))
 188                   ~continuations:[
 189                     T.then_
 190                      ~start:(injection_tac ~term:(C.Rel 1))
 191                      ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *)
 192                     ;
 193                     T.then_
 194                      ~start:(ProofEngineTypes.mk_tactic
 195                        (fun status ->
 196                          let (proof, goal) = status in
 197                          let _,metasenv,_,_ = proof in
 198                           let _,context,gty = CicUtil.lookup_meta goal metasenv in
 199                            let new_t1' =
 200                             match gty with
 201                                (C.Appl (C.MutInd (_,_,_)::arglist)) ->
 202                                 List.nth arglist 1
 203                              | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: goal after cut is not correct"))
 204                            in
 205                             ProofEngineTypes.apply_tactic
 206                             (ReductionTactics.change_tac
 207                                ~pattern:(ProofEngineTypes.conclusion_pattern
 208                                 (Some new_t1'))
 209                                (fun _ m u ->
 210 let xxx =
 211                                  C.Appl [
 212                                   C.Lambda
 213                                    (C.Name "x",
 214                                      tty,
 215                                      C.MutCase
 216                                       (turi,typeno,outtype,C.Rel 1,patterns)) ;
 217                                   t1]
 218 in
 219 (*prerr_endline ("XXX: " ^ CicPp.ppterm xxx);*)
 220 xxx,
 221                                  m, u))
 222                         status
 223                        ))
 224                      ~continuation:
 225                        (T.then_
 226                          ~start:
 227                            (EqualityTactics.rewrite_simpl_tac
 228                              ~direction:`LeftToRight
 229                              ~pattern:(ProofEngineTypes.conclusion_pattern None)
 230                              term)
 231                          ~continuation:EqualityTactics.reflexivity_tac
 232                        )
 233                    ])
 234                   status
 235             | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not a discriminable equality"))
 236            )
 237         | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not an equality"))
 238  in
 239   ProofEngineTypes.mk_tactic (injection1_tac ~term ~i)
 240 ;;
 241
 242 exception TwoDifferentSubtermsFound of int
 243
 244 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 245 diversi *)
 246
 247 let discriminate'_tac ~term =
 248  let module C = Cic in
 249  let module U = UriManager in
 250  let module P = PrimitiveTactics in
 251  let module T = Tacticals in
 252  let true_URI =
 253   match LibraryObjects.true_URI () with
 254      Some uri -> uri
 255    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
 256  let false_URI =
 257   match LibraryObjects.false_URI () with
 258      Some uri -> uri
 259    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
 260  let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
 261  let find_discriminating_consno t1 t2 =
 262    let rec aux t1 t2 =
 263      match t1, t2 with
 264      | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None
 265      | C.Appl ((C.MutConstruct _ as constr1) :: args1),
 266        C.Appl ((C.MutConstruct _ as constr2) :: args2)
 267        when constr1 = constr2 ->
 268          let rec aux_list l1 l2 =
 269            match l1, l2 with
 270            | [], [] -> None
 271            | hd1 :: tl1, hd2 :: tl2 ->
 272                (match aux hd1 hd2 with
 273                | None -> aux_list tl1 tl2
 274                | Some _ as res -> res)
 275            | _ -> (* same constructor applied to a different number of args *)
 276                assert false
 277          in
 278          aux_list args1 args2
 279      | ((C.MutConstruct (_,_,consno1,subst1)),
 280        (C.MutConstruct (_,_,consno2,subst2)))
 281      | ((C.MutConstruct (_,_,consno1,subst1)),
 282        (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
 283      | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
 284        (C.MutConstruct (_,_,consno2,subst2)))
 285      | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
 286        (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
 287        when (consno1 <> consno2) || (subst1 <> subst2) ->
 288          Some consno2
 289      | _ -> fail "not a discriminable equality"
 290    in
 291    aux t1 t2
 292  in
 293  let mk_pattern turi typeno consno context left_args =
 294     (* a list of "True" except for the element in position consno which
 295      * is "False" *)
 296     match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
 297     | C.InductiveDefinition (ind_type_list,_,nr_ind_params,_)  ->
 298         let _,_,_,constructor_list = List.nth ind_type_list typeno in
 299         let false_constr_id,_ = List.nth constructor_list (consno - 1) in
 300         List.map
 301           (fun (id,cty) ->
 302             (* dubbio: e' corretto ridurre in questo context ??? *)
 303             let red_ty = CicReduction.whd context cty in
 304             let rec aux t k =
 305               match t with
 306               | C.Prod (_,_,target) when (k <= nr_ind_params) ->
 307                   CicSubstitution.subst (List.nth left_args (k-1))
 308                     (aux target (k+1))
 309               | C.Prod (binder,source,target) when (k > nr_ind_params) ->
 310                   C.Lambda (binder, source, (aux target (k+1)))
 311               | _ ->
 312                   if (id = false_constr_id)
 313                   then (C.MutInd(false_URI,0,[]))
 314                   else (C.MutInd(true_URI,0,[]))
 315             in
 316             (CicSubstitution.lift 1 (aux red_ty 1)))
 317           constructor_list
 318     | _ -> (* object is not an inductive definition *)
 319         assert false
 320  in
 321  let discriminate'_tac ~term status =
 322   let (proof, goal) = status in
 323   let _,metasenv,_,_ = proof in
 324   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 325   let termty,_ =
 326     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
 327   in
 328   match termty with
 329   | (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
 330     when LibraryObjects.is_eq_URI equri ->
 331       let turi,typeno,exp_named_subst,left_args =
 332         match tty with
 333         | (C.MutInd (turi,typeno,exp_named_subst)) ->
 334             turi,typeno,exp_named_subst,[]
 335         | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::left_args)) ->
 336             turi,typeno,exp_named_subst,left_args
 337         | _ -> fail "not a discriminable equality"
 338       in
 339       let consno =
 340         match find_discriminating_consno t1 t2 with
 341         | Some consno -> consno
 342         | None -> fail "discriminating terms are structurally equal"
 343       in
 344       let pattern = mk_pattern turi typeno consno context left_args in
 345       let (proof',goals') =
 346         ProofEngineTypes.apply_tactic
 347           (EliminationTactics.elim_type_tac
 348             (C.MutInd (false_URI, 0, [])))
 349           status
 350       in
 351       (match goals' with
 352       | [goal'] ->
 353           let _,metasenv',_,_ = proof' in
 354           let _,context',gty' = CicUtil.lookup_meta goal' metasenv' in
 355           ProofEngineTypes.apply_tactic
 356             (T.then_
 357               ~start:
 358                 (ReductionTactics.change_tac
 359                   ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty'))
 360                   (fun _ m u ->
 361                     C.Appl [
 362                       C.Lambda ( C.Name "x", tty,
 363                         C.MutCase (turi, typeno,
 364                           (C.Lambda ((C.Name "x"),
 365                            (CicSubstitution.lift 1 tty),
 366                            (C.Sort C.Prop))),
 367                           (C.Rel 1), pattern));
 368                       t2 ], m, u))
 369               ~continuation:
 370                 (T.then_
 371                   ~start:
 372                     (EqualityTactics.rewrite_simpl_tac
 373                       ~direction:`RightToLeft
 374                       ~pattern:(ProofEngineTypes.conclusion_pattern None)
 375                       term)
 376                   ~continuation:
 377                     (IntroductionTactics.constructor_tac ~n:1)))
 378             (proof',goal')
 379       | [] -> fail "ElimType False left no goals"
 380       | _ -> fail "ElimType False left more than one goal")
 381     | _ -> fail "not an equality"
 382   in
 383   ProofEngineTypes.mk_tactic (discriminate'_tac ~term)
 384
 385 let discriminate_tac ~term =
 386  let discriminate_tac ~term status =
 387   ProofEngineTypes.apply_tactic
 388   (Tacticals.then_
 389     ~start:(* (injection_tac ~term) *) Tacticals.id_tac
 390     ~continuation:(discriminate'_tac ~term)) (* NOOO!!! non term ma una (qualunque) delle nuove hyp introdotte da inject *)
 391    status
 392  in
 393   ProofEngineTypes.mk_tactic (discriminate_tac ~term)
 394
 395 (* DISCRIMINTATE SENZA INJECTION
 396
 397 exception TwoDifferentSubtermsFound of (Cic.term * Cic.term * int)
 398
 399 let discriminate_tac ~term status =
 400   let module C = Cic in
 401   let module U = UriManager in
 402   let module P = PrimitiveTactics in
 403   let module T = Tacticals in
 404   let (proof, goal) = status in
 405    let _,metasenv,_,_ = proof in
 406     let _,context,_ = CicUtil.lookup_meta goal metasenv in
 407      let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
 408       match termty with
 409          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
 410           when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
 411             or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
 412            match tty with
 413               (C.MutInd (turi,typeno,exp_named_subst))
 414             | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
 415
 416                 let (t1',t2',consno2') = (* bruuutto: uso un eccezione per terminare con successo! buuu!! :-/ *)
 417                  try
 418                   let rec traverse t1 t2 =
 419 debug_print (lazy ("XXXX t1 " ^ CicPp.ppterm t1)) ;
 420 debug_print (lazy ("XXXX t2 " ^ CicPp.ppterm t2)) ;
 421                    match t1,t2 with
 422                       ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
 423                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
 424                          when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
 425                        t1,t2,0
 426                     | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)),
 427                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2)))
 428                          when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) ->
 429                        let rec traverse_list l1 l2 =
 430                          match l1,l2 with
 431                             [],[] -> t1,t2,0
 432                           | hd1::tl1,hd2::tl2 -> traverse hd1 hd2; traverse_list tl1 tl2
 433                           | _ -> raise (ProofEngineTypes.Fail "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")
 434                        in traverse_list applist1 applist2
 435
 436                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
 437                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
 438                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
 439                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
 440                     | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
 441                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
 442                     | ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::_)),
 443                        (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::_)))
 444                          when (consno1 <> consno2) || (exp_named_subst1 <> exp_named_subst2) ->
 445                        raise (TwoDifferentSubtermsFound (t1,t2,consno2))
 446                     | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
 447                   in traverse t1 t2
 448                  with (TwoDifferentSubtermsFound (t1,t2,consno2)) -> (t1,t2,consno2)
 449                 in
 450 debug_print (lazy ("XXXX consno2' " ^ (string_of_int consno2'))) ;
 451                  if consno2' = 0
 452                   then raise (ProofEngineTypes.Fail "Discriminate: Discriminating terms are structurally equal")
 453                   else
 454
 455                    let pattern =
 456                      (* a list of "True" except for the element in position consno2' which is "False" *)
 457                      match fst(CicEnvironment.get_obj turi
 458                                  CicUniv.empty_ugraph) with
 459                         C.InductiveDefinition (ind_type_list,_,nr_ind_params)  ->
 460 debug_print (lazy ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno))) ;
 461                          let _,_,_,constructor_list = (List.nth ind_type_list typeno) in
 462 debug_print (lazy ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2'))) ;
 463                           let false_constr_id,_ = List.nth constructor_list (consno2' - 1) in
 464 debug_print (lazy "XXXX nth funzionano ") ;
 465                            List.map
 466                             (function (id,cty) ->
 467                               let red_ty = CicReduction.whd context cty in (* dubbio: e' corretto ridurre in questo context ??? *)
 468                                let rec aux t k =
 469                                 match t with
 470                                    C.Prod (_,_,target) when (k <= nr_ind_params) ->
 471                                     aux target (k+1)
 472                                  | C.Prod (binder,source,target) when (k > nr_ind_params) ->
 473                                     C.Lambda (binder,source,(aux target (k+1)))
 474                                  | _ ->
 475                                     if (id = false_constr_id)
 476                                      then (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [])
 477                                      else (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/True.ind") 0 [])
 478                                in aux red_ty 1
 479                             )
 480                             constructor_list
 481                       | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible")
 482                    in
 483
 484                     let (proof',goals') =
 485                      EliminationTactics.elim_type_tac
 486                       ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] )
 487                       status
 488                     in
 489                      (match goals' with
 490                          [goal'] ->
 491                           let _,metasenv',_,_ = proof' in
 492                            let _,context',gty' =
 493                              CicUtil.lookup_meta goal' metasenv'
 494                            in
 495                             T.then_
 496                              ~start:
 497                               (P.change_tac
 498                                ~what:gty'
 499                                ~with_what:
 500                                 (C.Appl [
 501                                   C.Lambda (
 502                                    C.Name "x", tty,
 503                                    C.MutCase (
 504                                     turi, typeno,
 505                                     (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))),
 506                                     (C.Rel 1), pattern
 507                                    )
 508                                   );
 509                                   t2']
 510                                 )
 511                               )
 512                              ~continuation:
 513                               (
 514 debug_print (lazy ("XXXX rewrite<-: " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))));
 515 debug_print (lazy ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1' ; t2']))) ;
 516 debug_print (lazy ("XXXX equri: " ^ U.string_of_uri equri)) ;
 517 debug_print (lazy ("XXXX tty : " ^ CicPp.ppterm tty)) ;
 518 debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1'))) ;
 519 debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ;
 520 if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> tty then debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t1'))) ;
 521 if (CicTypeChecker.type_of_aux' metasenv' context' t2') <> tty then debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ;
 522 if (CicTypeChecker.type_of_aux' metasenv' context' t1') <> (CicTypeChecker.type_of_aux' metasenv' context' t2')
 523  then debug_print (lazy ("XXXX tt1': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux'
 524  metasenv' context' t1'))) ; debug_print (lazy ("XXXX tt2': " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' t2'))) ;
 525
 526                                let termty' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t1 ~with_what:t1' ~where:termty in
 527                                 let termty'' = ProofEngineReduction.replace_lifting ~equality:(==) ~what:t2 ~with_what:t2' ~where:termty' in
 528
 529 debug_print (lazy ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv' context' term)));
 530                                  T.then_
 531                                    ~start:(EqualityTactics.rewrite_back_simpl_tac ~term:term)
 532                                    ~continuation:(IntroductionTactics.constructor_tac ~n:1)
 533                               )
 534                              (proof',goal')
 535                        | _ -> raise (ProofEngineTypes.Fail "Discriminate: ElimType False left more (or less) than one goal")
 536                      )
 537             | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality")
 538            )
 539        | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality")
 540 ;;
 541
 542 *)
 543
 544
 545