| Split of loc
| Symmetry of loc
| Transitivity of loc * 'term
+ (* Costruttori Aggiunti *)
+ | Assume of loc * 'ident * 'term
+ | Suppose of loc * 'term *'ident
+ | By_term_we_proved of loc * 'term * 'term * 'ident
+ | We_need_to_prove of loc * 'term * 'ident
+ | Bydone of loc * 'term
type search_kind = [ `Locate | `Hint | `Match | `Elim ]
| Split _ -> "split"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
-
-let pp_search_kind = function
+
+ let pp_search_kind = function
| `Locate -> "locate"
| `Hint -> "hint"
| `Match -> "match"
| GrafiteAst.Split _ -> Tactics.split
| GrafiteAst.Symmetry _ -> Tactics.symmetry
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
+ (* Implementazioni Aggiunte *)
+ | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
+ | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id
+ | GrafiteAst.By_term_we_proved (_, t, ty, id) ->
+ Declarative.by_term_we_proved t ty id
+ | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id
+ | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
(* maybe we only need special cases for apply and goal *)
let classify_tactic tactic =
| GrafiteAst.Transitivity (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Transitivity (loc, cic)
+ (* Nuovi casi *)
+ | GrafiteAst.Assume (loc, id, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Assume (loc, id, cic)
+ | GrafiteAst.Suppose (loc, term, id) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Suppose (loc, cic, id)
+ | GrafiteAst.Bydone (loc,term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Bydone (loc, cic)
+ | GrafiteAst.We_need_to_prove (loc,term,id) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.We_need_to_prove (loc,cic,id)
+ | GrafiteAst.By_term_we_proved (loc,term,term',id) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic' = disambiguate_term context metasenv term' in
+ metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id)
let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
let uri =
GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->
GrafiteAst.Transitivity (loc, t)
+ (* Produzioni Aggiunte *)
+ | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
+ GrafiteAst.Assume (loc, id, t)
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.Suppose (loc, t, id)
+ | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.By_term_we_proved (loc, t, ty, id)
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.We_need_to_prove (loc, t, id)
+ | IDENT "by" ; t = tactic_term ; IDENT "done" ->
+ GrafiteAst.Bydone (loc, t)
]
];
atomic_tactical:
discriminationTactics.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
ring.cmi: proofEngineTypes.cmi
+setoids.cmi: proofEngineTypes.cmi
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
statefulProofEngine.cmi: proofEngineTypes.cmi
tactics.cmi: proofEngineTypes.cmi
+declarative.cmi: proofEngineTypes.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi
paramodulation/subst.cmo: paramodulation/subst.cmi
paramodulation/subst.cmx: paramodulation/subst.cmi
paramodulation/equality.cmo: paramodulation/utils.cmi \
- paramodulation/subst.cmi proofEngineReduction.cmi \
+ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
paramodulation/equality.cmi
paramodulation/equality.cmx: paramodulation/utils.cmx \
- paramodulation/subst.cmx proofEngineReduction.cmx \
+ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
paramodulation/equality.cmi
paramodulation/inference.cmo: paramodulation/utils.cmi \
- paramodulation/subst.cmi proofEngineHelpers.cmi metadataQuery.cmi \
- paramodulation/equality.cmi paramodulation/inference.cmi
+ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
+ metadataQuery.cmi paramodulation/equality.cmi \
+ paramodulation/inference.cmi
paramodulation/inference.cmx: paramodulation/utils.cmx \
- paramodulation/subst.cmx proofEngineHelpers.cmx metadataQuery.cmx \
- paramodulation/equality.cmx paramodulation/inference.cmi
+ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
+ metadataQuery.cmx paramodulation/equality.cmx \
+ paramodulation/inference.cmi
paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
paramodulation/equality.cmi paramodulation/equality_indexing.cmi
paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
autoTactic.cmx tactics.cmi
+declarative.cmo: tactics.cmi tacticals.cmi declarative.cmi
+declarative.cmx: tactics.cmx tacticals.cmx declarative.cmi
equalityTactics.mli autoTactic.mli discriminationTactics.mli \
inversion.mli inversion_principle.mli ring.mli setoids.mli \
fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \
- statefulProofEngine.mli tactics.mli
+ statefulProofEngine.mli tactics.mli declarative.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
--- /dev/null
+let assume id t =
+ Tacticals.then_
+ ~start:
+ (Tactics.intros ~howmany:1
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
+ ~continuation:
+ (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> t,metasenv,ugraph))
+;;
+
+let suppose t id =
+ Tacticals.then_
+ ~start:
+ (Tactics.intros ~howmany:1
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
+ ~continuation:
+ (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+ (fun _ metasenv ugraph -> t,metasenv,ugraph))
+;;
+
+let by_term_we_proved t ty id =
+ Tacticals.thens
+ ~start:
+ (Tactics.cut ty
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
+ ~continuations:
+ [ Tacticals.id_tac ; Tactics.apply t ]
+;;
+
+let bydone t =
+ (Tactics.apply ~term:t)
+
+;;
+
+let we_need_to_prove t id =
+ let aux status =
+ let proof,goals =
+ ProofEngineTypes.apply_tactic
+ (Tactics.cut t
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id))
+ status
+ in
+ let goals' =
+ match goals with
+ [fst; snd] -> [snd; fst]
+ | _ -> assert false
+ in
+ proof,goals'
+ in
+ ProofEngineTypes.mk_tactic aux
+;;
--- /dev/null
+val assume : string -> Cic.term -> ProofEngineTypes.tactic
+val suppose : Cic.term -> string -> ProofEngineTypes.tactic
+val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic
+val bydone : Cic.term -> ProofEngineTypes.tactic
+val we_need_to_prove : Cic.term -> string -> ProofEngineTypes.tactic
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/decl".
+
+include "nat/times.ma".
+include "nat/orders.ma".
+
+theorem easy: ∀n,m. n * m = O → n = O ∨ m = O.
+ assume n: nat.
+ assume m: nat.
+ (* base case *)
+ by (refl_eq ? O) we proved (O = O) (trivial).
+ by (or_introl ? ? trivial) we proved (O = O ∨ m = O) (trivial2).
+ by (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case).
+ (* inductive case *)
+ we need to prove
+ (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
+ (inductive_case).
+ assume n1: nat.
+ suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
+ (* base case *)
+ by (or_intror ? ? trivial) we proved (S n1 = O ∨ O = O) (pre_base_case2).
+ by (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
+ (* inductive case *)
+ we need to prove
+ (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
+ (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
+ assume m1: nat.
+ suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
+ suppose (S n1 * S m1 = O) (absurd_hyp).
+ simplify in absurd_hyp.
+ by (sym_eq ? ? ? absurd_hyp) we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+ by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
+ by (False_ind ? the_absurd)
+ done.
+ (* the induction *)
+ by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
+ done.
+ (* the induction *)
+ by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
+done.
+qed.
+
+theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O.
+ intros 2.
+ elim n 0
+ [ intro;
+ left;
+ reflexivity
+ | intro;
+ elim m 0
+ [ intros;
+ right;
+ reflexivity
+ | intros;
+ simplify in H2;
+ lapply (sym_eq ? ? ? H2);
+ elim (not_eq_O_S ? Hletin)
+ ]
+ ]
+qed.
+
\ No newline at end of file
projects / helm.git / commitdiff