From c61fbff7b7296b56aa5313823bc2df4d344c9ce6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Sep 2006 16:47:13 +0000 Subject: [PATCH] Injection now clears all intermediate results introduced. Injection code reindented. Baseuri in injection.ma fixed. --- components/tactics/discriminationTactics.ml | 233 ++++++++++++-------- matita/tests/injection.ma | 2 +- 2 files changed, 139 insertions(+), 96 deletions(-) diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index e6682709c..7c5df0d82 100644 --- a/components/tactics/discriminationTactics.ml +++ b/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/matita/tests/injection.ma b/matita/tests/injection.ma index 7f79ef386..7d9586fd1 100644 --- a/matita/tests/injection.ma +++ b/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. -- 2.39.2