Injection now clears all intermediate results introduced.

Injection code reindented.
Baseuri in injection.ma fixed.

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index e6682709c1b75edff7bda053889a19bde01f9238..7c5df0d82eafbbf9bfc7da73ddf573e405e72b12 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -27,7 +27,7 @@
 
 let debug_print = fun _ -> ()
 
-let rec injection_tac ~term ~liftno ~continuation =
+let rec injection_tac ~first_time ~term ~liftno ~continuation =
  let injection_tac ~term status = 
   let (proof, goal) = status in
   let module C = Cic in
@@ -41,52 +41,91 @@ let rec injection_tac ~term ~liftno ~continuation =
     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
   in
     ProofEngineTypes.apply_tactic
-      (match termty with
-          (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
-             when LibraryObjects.is_eq_URI equri -> (
+     (match termty with
+         (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
+            when LibraryObjects.is_eq_URI equri ->
+          begin
            match tty with
               (C.MutInd (turi,typeno,exp_named_subst))
-            | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
-                   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) ->
-                       (* raise (ProofEngineTypes.Fail "Injection: nothing to do") ; *) continuation ~liftno
-                    | ((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 i l1 l2 =
-                         match l1,l2 with
-                            [],[] -> continuation
-                          | hd1::tl1,hd2::tl2 -> 
-                             if
-                              fst
-                               (CicReduction.are_convertible ~metasenv
-                                 context hd1 hd2 CicUniv.empty_ugraph)
-                             then
-                              traverse_list (i+1) tl1 tl2
-                             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???"))
-                       in traverse_list 1 applist1 applist2 ~liftno
-                    | ((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 (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one"))
-                    | _ -> continuation ~liftno (*raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))*)
-                   )
-            | _ -> continuation ~liftno (*raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))*)
-           )
-        | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation"))
-      ) status
+            | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
+               begin
+                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)
+                   ->
+                    if first_time then
+                     raise
+                      (ProofEngineTypes.Fail (lazy "Injection: nothing to do"))
+                    else
+                     continuation ~liftno
+                 | 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 i l1 l2 =
+                       match l1,l2 with
+                          [],[] ->
+                           if first_time then
+                            continuation
+                           else
+                            (match term with
+                                C.Rel n ->
+                                 (match List.nth context (n-1) with
+                                     Some (C.Name id,_) ->
+                                      fun ~liftno ->
+                                       T.then_
+                                        ~start:
+                                          (ProofEngineStructuralRules.clear
+                                            ~hyps:[id])
+                                        ~continuation:(continuation ~liftno)
+                                   | _ -> assert false)
+                              | _ -> assert false)
+                        | hd1::tl1,hd2::tl2 -> 
+                           if
+                            fst
+                             (CicReduction.are_convertible ~metasenv
+                               context hd1 hd2 CicUniv.empty_ugraph)
+                           then
+                            traverse_list (i+1) tl1 tl2
+                           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???"))
+                     in
+                      traverse_list 1 applist1 applist2 ~liftno
+                 | ((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 (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"))
+                   else
+                    continuation ~liftno 
+               end
+            | _ ->
+              if first_time then
+               raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
+              else
+               continuation ~liftno 
+           end
+       | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation"))
+     ) status
  in 
   ProofEngineTypes.mk_tactic (injection_tac ~term)
 
@@ -201,55 +240,59 @@ and injection1_tac ~term ~i ~liftno ~continuation =
                 in
                 ProofEngineTypes.apply_tactic   
                  (T.thens 
-                  ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2']))
-                  ~continuations:[
-                    T.then_ 
-                     ~start:(injection_tac ~liftno:0 ~term:(C.Rel 1)
-                       ~continuation:(fun ~liftno:x -> continuation ~liftno:(liftno + 1 + x)))
-                     ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) 
-                    ;
-                    T.then_ 
-                     ~start:(ProofEngineTypes.mk_tactic 
-                       (fun status ->    
-                         let (proof, goal) = status in
-                         let _,metasenv,_,_ = proof in
-                          let _,context,gty =
-                           CicUtil.lookup_meta goal metasenv
-                          in
-                           let new_t1' = 
-                            match gty with 
-                               (C.Appl (C.MutInd (_,_,_)::arglist)) -> 
-                                List.nth arglist 1
-                             | _ ->
-                               raise
-                                (ProofEngineTypes.Fail
-                                  (lazy
-                                    "Injection: goal after cut is not correct"))
-                           in
-                            ProofEngineTypes.apply_tactic 
-                            (ReductionTactics.change_tac
-                               ~pattern:(ProofEngineTypes.conclusion_pattern
-                                (Some new_t1'))
-                               (fun _ m u ->
-                                 C.Appl [
-                                  C.Lambda
-                                   (C.Name "x",
-                                     tty,
-                                     C.MutCase
-                                      (turi,typeno,outtype,C.Rel 1,patterns)) ;
-                                  t1],
-                                 m, u))
-                        status
-                       ))
-                     ~continuation:
-                       (T.then_
-                         ~start:
-                           (EqualityTactics.rewrite_simpl_tac
-                             ~direction:`LeftToRight
-                             ~pattern:(ProofEngineTypes.conclusion_pattern None)
-                             term)
-                         ~continuation:EqualityTactics.reflexivity_tac
-                       )
+                  ~start:
+                    (P.cut_tac
+                     (C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2']))
+                  ~continuations:
+                    [ injection_tac ~first_time:false ~liftno:0
+                       ~term:(C.Rel 1)
+                       (* here I need to lift all the continuations by 1;
+                          since I am setting back liftno to 0, I actually
+                          need to lift all the continuations by liftno + 1 *)
+                       ~continuation:
+                         (fun ~liftno:x ->
+                           continuation ~liftno:(liftno + 1 + x)) ;
+                      T.then_ 
+                       ~start:(ProofEngineTypes.mk_tactic 
+                         (fun status ->    
+                           let (proof, goal) = status in
+                           let _,metasenv,_,_ = proof in
+                            let _,context,gty =
+                             CicUtil.lookup_meta goal metasenv
+                            in
+                             let new_t1' = 
+                              match gty with 
+                                 (C.Appl (C.MutInd (_,_,_)::arglist)) -> 
+                                  List.nth arglist 1
+                               | _ ->
+                                 raise
+                                  (ProofEngineTypes.Fail
+                                    (lazy
+                                      "Injection: goal after cut is not correct"))
+                             in
+                              ProofEngineTypes.apply_tactic 
+                              (ReductionTactics.change_tac
+                                 ~pattern:(ProofEngineTypes.conclusion_pattern
+                                  (Some new_t1'))
+                                 (fun _ m u ->
+                                   C.Appl [
+                                    C.Lambda
+                                     (C.Name "x",
+                                       tty,
+                                       C.MutCase
+                                        (turi,typeno,outtype,C.Rel 1,patterns)) ;
+                                    t1],
+                                   m, u))
+                          status
+                         ))
+                       ~continuation:
+                         (T.then_
+                           ~start:
+                             (EqualityTactics.rewrite_simpl_tac
+                               ~direction:`LeftToRight
+                               ~pattern:(ProofEngineTypes.conclusion_pattern None)
+                               term)
+                           ~continuation:EqualityTactics.reflexivity_tac)
                    ])     
                   status
             | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type"))
@@ -260,7 +303,7 @@ and injection1_tac ~term ~i ~liftno ~continuation =
 ;;
 
 let injection_tac =
- injection_tac ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)
+ injection_tac ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)
 ;;
 
 exception TwoDifferentSubtermsFound of int 

diff --git a/helm/software/matita/tests/injection.ma b/helm/software/matita/tests/injection.ma
index 7f79ef3867146f4e77bd5513811178a5d09551d4..7d9586fd1badd4482f9dc88667cb01e755f42b89 100644 (file)
--- a/helm/software/matita/tests/injection.ma
+++ b/helm/software/matita/tests/injection.ma
@@ -77,7 +77,7 @@ theorem injection_test3:
 *) 
 
 theorem injection_test4:
- ∀n,n',m,m'. k1 bool (S n) (S m) = k1 bool (S n') (S (S m')) → m = S m'.
+ ∀n,n',m,m'. k1 bool (S n) (S (S m)) = k1 bool (S n') (S (S (S m'))) → m = S m'.
  intros;
  injection H;
  assumption.