From 3a0c3a4275ba88babc9d5717a019fe277d947fa6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 14 Sep 2006 11:58:21 +0000 Subject: [PATCH 1/1] 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. --- .../tactics/discriminationTactics.ml | 47 +++++++---- helm/software/matita/tests/injection.ma | 79 +++++++++++++++++++ 2 files changed, 112 insertions(+), 14 deletions(-) create mode 100644 helm/software/matita/tests/injection.ma diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index 97e9597c6..9ec2d7622 100644 --- 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 index 000000000..149a39e81 --- /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. + + -- 2.39.2