-let constructor_tac ~n ~status:(proof, goal) =
- let module C = Cic in
- let module R = CicReduction in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- match (R.whd context ty) with
- (C.MutInd (uri,typeno,exp_named_subst))
- | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::_)) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
- ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
- | _ -> raise (ProofEngineTypes.Fail "Constructor failed")
-;;
-
-
-let exists_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let split_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let left_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let right_tac ~status =
- constructor_tac ~n:2 ~status
-;;
-
-
-let reflexivity_tac =
- constructor_tac ~n:1
-;;
-
-
-let symmetry_tac ~status:(proof, goal) =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- match (R.whd context ty) with
- (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/sym_eq.con", []))
-
- | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con", []))
-
- | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
-;;
-
-
-let transitivity_tac ~term ~status:((proof, goal) as status) =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let module Tl = Tacticals in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- match (R.whd context ty) with
- (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) ->
- Tl.thens
- ~start:(PrimitiveTactics.apply_tac
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/trans_eq.con", [])))
- ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac]
- ~status
-
- | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
- Tl.thens
- ~start:(PrimitiveTactics.apply_tac
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/trans_eqT.con", [])))
- ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac]
- ~status
-
- | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
-;;
-
-