1. added a test for injection

2. injection now works also on inductive types with left parameters

As the test shows, there are still bugs even in the case of an inductive
case with right parameters only.

diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml
index 97e9597c6dbbe433727d958fbc0c07856f3a68cf..9ec2d76221e19ffd3dc48f44374c7c1c085517fb 100644 (file)
--- a/helm/software/components/tactics/discriminationTactics.ml
+++ b/helm/software/components/tactics/discriminationTactics.ml
@@ -55,17 +55,25 @@ let rec injection_tac ~term =
                     | ((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 =
+                       let rec traverse_list i liftno l1 l2 =
                          match l1,l2 with
                             [],[] -> T.id_tac
                           | hd1::tl1,hd2::tl2 -> 
-                             T.then_ 
-                              ~start:
-                                (injection1_tac ~i
-                                  ~term:(CicSubstitution.lift (i-1) term))
-                              ~continuation:(traverse_list (i+1) tl1 tl2)
+                             if
+                              fst
+                               (CicReduction.are_convertible ~metasenv
+                                 context hd1 hd2 CicUniv.empty_ugraph)
+                             then
+                              traverse_list (i+1) liftno tl1 tl2
+                             else
+                              T.then_ 
+                               ~start:
+                                 (injection1_tac ~i ~liftno
+                                   ~term:(CicSubstitution.lift liftno term))
+                               ~continuation:
+                                 (traverse_list (i+1) (liftno+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
+                       in traverse_list 1 0 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)),
@@ -85,7 +93,7 @@ let rec injection_tac ~term =
  in 
   ProofEngineTypes.mk_tactic (injection_tac ~term)
 
-and injection1_tac ~term ~i = 
+and injection1_tac ~term ~i ~liftno = 
  let injection1_tac ~term ~i status =
   let (proof, goal) = status in
   (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma differiscono (o potrebbero differire?) nell'i-esimo parametro del costruttore *)
@@ -142,7 +150,7 @@ and injection1_tac ~term ~i =
                             | _ ->
                                let nr_param_constr = k - 1 - paramsno in
                                 if id = i_constr_id
-                                 then C.Rel (nr_param_constr - i + 1)
+                                 then C.Rel (nr_param_constr - liftno)
                                  else S.lift (nr_param_constr + 1) t1' (* + 1 per liftare anche il lambda aggiunto esternamente al case *)
                           in aux reduced_cty 1
                        ) constructor_list in
@@ -195,13 +203,20 @@ and injection1_tac ~term ~i =
                        (fun status ->    
                          let (proof, goal) = status in
                          let _,metasenv,_,_ = proof in
-                          let _,context,gty = CicUtil.lookup_meta goal metasenv 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"))
+                             | _ ->
+                               raise
+                                (ProofEngineTypes.Fail
+                                  (lazy
+                                    "Injection: goal after cut is not correct"))
                            in
+let aaa =
                             ProofEngineTypes.apply_tactic 
                             (ReductionTactics.change_tac
                                ~pattern:(ProofEngineTypes.conclusion_pattern
@@ -216,10 +231,14 @@ let xxx =
                                       (turi,typeno,outtype,C.Rel 1,patterns)) ;
                                   t1]
 in
-(*prerr_endline ("XXX: " ^ CicPp.ppterm xxx);*)
+prerr_endline ("XXX: " ^ CicPp.ppterm xxx);
+prerr_endline ("WITH: " ^ CicPp.ppterm new_t1');
 xxx,
                                  m, u))
                         status
+in
+prerr_endline "OK";
+aaa
                        ))
                      ~continuation:
                        (T.then_
@@ -232,9 +251,9 @@ xxx,
                        )
                    ])     
                   status
-            | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not a discriminable equality"))
+            | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type"))
            )
-        | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not an equality"))
+        | _ -> ProofEngineTypes.apply_tactic T.id_tac status (*XXXraise (ProofEngineTypes.Fail (lazy "Injection: not an equality"))*)
  in
   ProofEngineTypes.mk_tactic (injection1_tac ~term ~i)
 ;;

diff --git a/helm/software/matita/tests/injection.ma b/helm/software/matita/tests/injection.ma
new file mode 100644 (file)
index 0000000..149a39e
--- /dev/null
+++ b/helm/software/matita/tests/injection.ma
@@ -0,0 +1,79 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/test/injection/".
+
+include "legacy/coq.ma".
+
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
+alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
+
+inductive t0 : Type :=
+   k0 : nat → nat → t0
+ | k0' : bool → bool → t0.
+
+theorem injection_test0: ∀n,n',m,m'. k0 n m = k0 n' m' → m = m'.
+ intros;
+ injection H;
+ assumption.
+qed.
+
+inductive t : Type → Type :=
+   k : nat → t nat
+ | k': bool → t bool.
+ 
+theorem injection_test1: ∀n,n'. k n = k n' → n = n'.
+ intros;
+ injection H;
+ assumption.
+qed.
+
+inductive tt (A:Type) : Type -> Type :=
+   k1: nat → nat → tt A nat
+ | k2: bool → bool → tt A bool.
+ 
+theorem injection_test2: ∀n,n',m,m'. k1 bool n n' = k1 bool m m' → n' = m'.
+ intros;
+ injection H;
+ assumption.
+qed.
+
+inductive ttree : Type → Type :=
+   tempty: ttree nat
+ | tnode : ∀A. ttree A → ttree A → ttree A.
+
+theorem injection_test3:
+ ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'.
+ intros;
+ injection H;
+ assumption.
+qed.
+
+theorem injection_test3:
+ ∀t,t'.
+  tnode nat (tnode nat t t') tempty = tnode nat (tnode nat t' tempty) tempty →
+   t = t'.
+ intros;
+ injection H;
+ 
+
+theorem injection_test4:
+ ∀n,n',m,m'. k1 bool (S n) (S m) = k1 bool (S n') (S (S m')) → m = S m'.
+ intros;
+ injection H;
+ assumption.
+qed.
+
+