From d38484e586188871d25ff9d582b1264fa58350d8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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. --- .../tactics/discriminationTactics.ml | 21 ++++++++++++------- helm/software/matita/tests/injection.ma | 13 ++++++++---- 2 files changed, 23 insertions(+), 11 deletions(-) diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index 4f959965a..42da52bd6 100644 --- a/helm/software/components/tactics/discriminationTactics.ml +++ b/helm/software/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/helm/software/matita/tests/injection.ma b/helm/software/matita/tests/injection.ma index 149a39e81..7f79ef386 100644 --- a/helm/software/matita/tests/injection.ma +++ b/helm/software/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