X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=a26895e6221fe003849d6597c038e37afd6263a1;hb=d1126c6b78a3333bbf415daf027004496b77c2f4;hp=24ab511f05d71c77f08e83e186b8be41f67f27d2;hpb=ab0954eab207a70e6ad5f2991cc117608deff55b;p=helm.git diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 24ab511f0..a26895e62 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -23,8 +23,6 @@ * http://cs.unibo.it/helm/. *) -open HelmLibraryObjects - let debug_print = fun _ -> () let rec injection_tac ~term = @@ -41,7 +39,7 @@ let rec injection_tac ~term = ProofEngineTypes.apply_tactic (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> ( @@ -97,7 +95,7 @@ and injection1_tac ~term ~i = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in match termty with (* an equality *) (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -163,29 +161,28 @@ and injection1_tac ~term ~i = | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct") in ProofEngineTypes.apply_tactic - (P.change_tac - ~what:new_t1' - ~pattern:([],None) - ~with_what: - (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ( - (C.Name "x"), - (S.lift 1 tty), - (S.lift 2 tty'))), - (C.Rel 1), pattern - ) - ); - t1] - )) + (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, + (C.Lambda ((C.Name "x"), + (S.lift 1 tty), + (S.lift 2 tty'))), + (C.Rel 1), pattern + ) + ); + t1], m, u)) status )) ~continuation: (T.then_ - ~start:(EqualityTactics.rewrite_simpl_tac ~term ()) + ~start: + (EqualityTactics.rewrite_simpl_tac + ~direction:`LeftToRight + ~pattern:(ProofEngineTypes.conclusion_pattern None) + term) ~continuation:EqualityTactics.reflexivity_tac ) ]) @@ -217,7 +214,7 @@ let discriminate'_tac ~term = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) - when (U.eq equri Logic.eq_URI) -> ( + when LibraryObjects.is_eq_URI equri -> ( match tty with (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> @@ -276,8 +273,8 @@ let discriminate'_tac ~term = C.Lambda (binder,source,(aux target (k+1))) | _ -> if (id = false_constr_id) - then (C.MutInd(Logic.false_URI,0,[])) - else (C.MutInd(Logic.true_URI,0,[])) + then (C.MutInd(LibraryObjects.false_URI (),0,[])) + else (C.MutInd(LibraryObjects.true_URI (),0,[])) in aux red_ty 1 ) constructor_list @@ -287,7 +284,7 @@ let discriminate'_tac ~term = let (proof',goals') = ProofEngineTypes.apply_tactic (EliminationTactics.elim_type_tac - ~term:(C.MutInd(Logic.false_URI,0,[]))) + (C.MutInd(LibraryObjects.false_URI (),0,[]))) status in (match goals' with @@ -299,27 +296,27 @@ let discriminate'_tac ~term = ProofEngineTypes.apply_tactic (T.then_ ~start: - (P.change_tac - ~what:gty' - ~pattern:([],None) - ~with_what: - (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), - (C.Rel 1), pattern - ) - ); - t2] - ) - ) + (ReductionTactics.change_tac + ~pattern:(ProofEngineTypes.conclusion_pattern + (Some gty')) + (fun _ m u -> C.Appl [ + C.Lambda ( + C.Name "x", tty, + C.MutCase ( + turi, typeno, + (C.Lambda ((C.Name "x"),tty,(C.Sort C.Prop))), + (C.Rel 1), pattern + ) + ); + t2], m, u)) ~continuation: ( T.then_ - ~start:(EqualityTactics.rewrite_back_simpl_tac - ~term ()) + ~start: + (EqualityTactics.rewrite_simpl_tac + ~direction:`RightToLeft + ~pattern:(ProofEngineTypes.conclusion_pattern None) + term) ~continuation:(IntroductionTactics.constructor_tac ~n:1) )) (proof',goal')