From ab16e7b1f7976674e6a4cb1043cd05f2c7f5ad20 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 14 Sep 2006 13:55:57 +0000
Subject: [PATCH] 1. Stricter controls implemented in injection. 2.
 tests/injection.ma now contains a description of why the tactic sometimes   
 fail and there is nothing really cute we can do with it. It also hints to   
 an alternative solution implemented in Coq.

---
 components/tactics/discriminationTactics.ml | 21 ++++++++++++++-------
 matita/tests/injection.ma                   | 13 +++++++++----
 2 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml
index 4f959965a..42da52bd6 100644
--- a/components/tactics/discriminationTactics.ml
+++ b/components/tactics/discriminationTactics.ml
@@ -83,8 +83,8 @@ let rec injection_tac ~term =
                     | ((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 "Injection: not a projectable equality but a discriminable one") ; *) T.id_tac
-                    | _ -> (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality") ; *) T.id_tac
+                       raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality but a discriminable one"))
+                    | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
                    )
             | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality"))
            )
@@ -144,7 +144,7 @@ and injection1_tac ~term ~i ~liftno =
                             | C.Prod (binder,source,target) when k > paramsno ->
  		               let binder' =
                                 match binder with
-                                   C.Name b -> C.Name b
+                                   C.Name _ -> binder
                                  | C.Anonymous ->
                                     C.Name
                                      (incr seed; "y" ^ string_of_int !seed)
@@ -164,10 +164,17 @@ prerr_endline ("rel= " ^ string_of_int (k - i));
                           in aux reduced_cty 1
                        ) constructor_list in
                      let outtype =
+                      let seed = ref 0 in
                       let rec to_lambdas te head =
                        match CicReduction.whd context te with
-                        | C.Prod (name,so,ta) ->
-                           C.Lambda (name,so,to_lambdas ta head)
+                        | C.Prod (binder,so,ta) ->
+                           let binder' =
+                            match binder with
+                               C.Name _ -> binder
+                             | C.Anonymous ->
+                                C.Name (incr seed; "d" ^ string_of_int !seed)
+                           in
+                            C.Lambda (binder',so,to_lambdas ta head)
                         | _ -> head in
                       let rec skip_prods n te =
                        match n, CicReduction.whd context te with
@@ -204,7 +211,7 @@ prerr_endline ("rel= " ^ string_of_int (k - i));
                   ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2']))
                   ~continuations:[
                     T.then_ 
-                     ~start:(injection_tac ~term:(C.Rel 1))
+                     ~start:T.id_tac (*(injection_tac ~term:(C.Rel 1))*)
                      ~continuation:T.id_tac (* !!! qui devo anche fare clear di term tranne al primo passaggio *) 
                     ;
                     T.then_ 
@@ -263,7 +270,7 @@ aaa
                   status
             | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type"))
            )
-        | _ -> ProofEngineTypes.apply_tactic T.id_tac status (*XXXraise (ProofEngineTypes.Fail (lazy "Injection: not an equality"))*)
+        | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equality"))
  in
   ProofEngineTypes.mk_tactic (injection1_tac ~term ~i)
 ;;
diff --git a/matita/tests/injection.ma b/matita/tests/injection.ma
index 149a39e81..7f79ef386 100644
--- a/matita/tests/injection.ma
+++ b/matita/tests/injection.ma
@@ -54,6 +54,13 @@ inductive ttree : Type → Type :=
    tempty: ttree nat
  | tnode : ∀A. ttree A → ttree A → ttree A.
 
+(* CSC: there is an undecidable unification problem here:
+    consider a constructor k : \forall x. f x -> i (g x)
+    The head of the outtype of the injection MutCase should be (f ?1)
+    such that (f ?1) unifies with (g d) [ where d is the Rel that binds
+    the corresponding right parameter in the outtype ]
+    Coq dodges the problem by generating an equality between sigma-types
+    (that state the existence of a ?1 such that ...)
 theorem injection_test3:
  ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'.
  intros;
@@ -67,13 +74,11 @@ theorem injection_test3:
    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.
-
-
+qed.
\ No newline at end of file
-- 
2.39.2