| Right of loc
| Ring of loc
| Split of loc
- | Subst of loc * string
+ | Subst of loc
| Symmetry of loc
| Transitivity of loc * 'term
(* Costruttori Aggiunti *)
| Right _ -> "right"
| Ring _ -> "ring"
| Split _ -> "split"
- | Subst (_, s) -> "subst " ^ s
+ | Subst _ -> "subst"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
(* Tattiche Aggiunte *)
| GrafiteAst.Right _ -> Tactics.right
| GrafiteAst.Ring _ -> Tactics.ring
| GrafiteAst.Split _ -> Tactics.split
- | GrafiteAst.Subst (_, hyp) -> Tactics.subst ~hyp
+ | GrafiteAst.Subst _ -> Tactics.subst
| GrafiteAst.Symmetry _ -> Tactics.symmetry
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
(* Implementazioni Aggiunte *)
metasenv,GrafiteAst.Ring loc
| GrafiteAst.Split loc ->
metasenv,GrafiteAst.Split loc
- | GrafiteAst.Subst (loc, hyp) ->
- metasenv, GrafiteAst.Subst (loc, hyp)
+ | GrafiteAst.Subst loc ->
+ metasenv, GrafiteAst.Subst loc
| GrafiteAst.Symmetry loc ->
metasenv,GrafiteAst.Symmetry loc
| GrafiteAst.Transitivity (loc, term) ->
GrafiteAst.Ring loc
| IDENT "split" ->
GrafiteAst.Split loc
- | IDENT "subst"; id = IDENT ->
- GrafiteAst.Subst (loc, id)
+ | IDENT "subst" ->
+ GrafiteAst.Subst loc
| IDENT "symmetry" ->
GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->
in
(proof',goals)
with (* FG: this should be PET.Fail _ *)
- TC.TypeCheckerFailure _ -> PET.apply_tactic (P.letout_tac ()) status
+ TC.TypeCheckerFailure _ -> PET.apply_tactic P.letout_tac status
in
ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
ProofEngineTypes.mk_tactic (transitivity_tac ~term)
;;
-(* FG *)
+(* FG: subst tactic *********************************************************)
let msg0 = lazy "Subst: not found in context"
let msg1 = lazy "Subst: not a simple equality"
PET.apply_tactic tac status
in
PET.mk_tactic subst_tac
+
+(* FG: This should be replaced by T.try_tactic *)
+let try_tactic ~tactic =
+ let try_tactic status =
+ try PET.apply_tactic tactic status with
+ | PET.Fail _ -> PET.apply_tactic T.id_tac status
+ in
+ PET.mk_tactic try_tactic
+
+let subst_tac =
+ let subst hyp = try_tactic ~tactic:(subst_tac hyp) in
+ let map = function
+ | Some (C.Name s, _) -> Some (subst s)
+ | _ -> None
+ in
+ let subst_tac status =
+ let (proof, goal) = status in
+ let (_, metasenv, _, _) = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let tactics = PEH.list_rev_map_filter map context in
+ PET.apply_tactic (T.seq ~tactics) status
+ in
+ PET.mk_tactic subst_tac
(* FG *)
-val subst_tac: hyp:string -> ProofEngineTypes.tactic
+(* rewrites and clears all simple equalities in the context *)
+val subst_tac: ProofEngineTypes.tactic
module C = Cic
-let letout_tac () =
+let letout_tac =
let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =
(* inserts a hole in the context *)
val letout_tac:
- unit -> ProofEngineTypes.tactic
+ ProofEngineTypes.tactic
(* This applies tactic and catches its possible failure *)
let try_tactic ~tactic =
- let rec try_tactic ~tactic status =
+ let try_tactic status =
info (lazy "in Tacticals.try_tactic");
try
S.apply_tactic tactic status
"Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
S.apply_tactic S.id_tactic status
in
- S.mk_tactic (try_tactic ~tactic)
+ S.mk_tactic try_tactic
(* This tries tactics until one of them doesn't _solve_ the goal *)
(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Aug 28 17:29:50 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Aug 29 11:37:38 CEST 2006 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
val set_goal : int -> ProofEngineTypes.tactic
val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val split : ProofEngineTypes.tactic
-val subst : hyp:string -> ProofEngineTypes.tactic
+val subst : ProofEngineTypes.tactic
val symmetry : ProofEngineTypes.tactic
val transitivity : term:Cic.term -> ProofEngineTypes.tactic
val unfold :
[ auto
| decompose;
[ lapply linear nle_gen_succ_1 to H1. decompose.
- rewrite > H1. clear H1 n. auto
+ subst. auto
| lapply linear nle_lt_or_eq to H1; decompose;
- [ auto
- | rewrite > H. clear H n. auto
- ]
+ subst; auto
]
].
qed.
intros. inversion H; clear H; intros;
[ apply (eq_gen_succ_zero ? ? H)
| lapply linear eq_gen_succ_succ to H2 as H0.
- rewrite > H0. clear H0.
+ subst.
apply ex_intro; [|auto] (**)
].
qed.
[ apply (eq_gen_succ_zero ? ? H)
| lapply linear eq_gen_succ_succ to H2 as H0.
lapply linear eq_gen_succ_succ to H3 as H2.
- rewrite > H0. rewrite > H2. clear H0 H2.
- auto
+ subst. auto
].
qed.
intros 1. elim y; clear y; intros;
[ lapply linear nle_gen_zero_2 to H. auto
| lapply linear nle_gen_succ_2 to H1. decompose;
- [ rewrite > H1. clear H1. auto
+ [ subst. auto
| lapply linear H to H3 as H0. decompose;
- [ rewrite > H1. clear H1 x. auto
- | rewrite < H. clear H n. auto
- ]
+ subst; auto
]
].
qed.
[
| clear H1.
decompose.
- rewrite > H1. clear H1 n2
+ subst.
]; apply ex_intro; [| auto || auto ]. (**)
qed.
[ lapply eq_gen_succ_zero to H as H0. apply H0
| clear H1 H3 r.
lapply linear eq_gen_succ_succ to H2 as H0.
- rewrite > H0. clear H0 q.
+ subst.
apply ex_intro; [| auto ] (**)
].
qed.
theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to
p = zero \land q = zero.
intros. inversion H; clear H; intros;
- [ rewrite < H1. clear H1 p.
- auto
+ [ subst. auto
| clear H H1.
lapply eq_gen_zero_succ to H3 as H0. apply H0
].
\exists s. p = succ s \land (s + q == r) \lor
q = succ s \land p + s == r.
intros. inversion H; clear H; intros;
- [ rewrite < H1. clear H1 p
+ [ subst.
| clear H1.
lapply linear eq_gen_succ_succ to H3 as H0.
- rewrite > H0. clear H0 r.
+ subst.
]; apply ex_intro; [| auto || auto ] (**)
qed.
(*
p = zero \land q = zero.
intros 2. elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
- rewrite > H0. clear H0 p.
- auto
+ subst. auto
| clear H.
lapply linear nplus_gen_succ_2 to H1 as H0.
decompose.
q = succ s \land p + s == r.
intros 2. elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
- rewrite > H0. clear H0 p
+ subst
| clear H.
lapply linear nplus_gen_succ_2 to H1 as H0.
decompose.
lapply linear eq_gen_succ_succ to H1 as H0.
- rewrite > H0. clear H0 r.
+ subst
]; apply ex_intro; [| auto || auto ]. (**)
qed.
*)
theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
intros 2. elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
- rewrite > H0. clear H0 p
+ subst
| lapply linear nplus_gen_succ_2 to H1 as H0.
decompose.
lapply linear eq_gen_succ_succ to H2 as H0.
- rewrite < H0 in H3. clear H0 a
+ subst
]; auto.
qed.
theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
intros 1. elim p; clear p; intros;
[ lapply linear nplus_gen_zero_1 to H as H0.
- rewrite > H0. clear H0 q
+ subst
| lapply linear nplus_gen_succ_1 to H1 as H0.
decompose.
lapply linear eq_gen_succ_succ to H2 as H0.
- rewrite < H0 in H3. clear H0 a
+ subst
]; auto.
qed.
(succ p) + q == (succ r).
intros 2. elim q; clear q;
[ lapply linear nplus_gen_zero_2 to H as H0.
- rewrite > H0. clear H0 p
+ subst
| lapply linear nplus_gen_succ_2 to H1 as H0.
decompose.
- rewrite > H2. clear H2 r
+ subst
]; auto.
qed.
theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
intros 2. elim q; clear q;
[ lapply linear nplus_gen_zero_2 to H as H0.
- rewrite > H0. clear H0 p
+ subst
| lapply linear nplus_gen_succ_2 to H1 as H0.
decompose.
- rewrite > H2. clear H2 r
+ subst
]; auto.
qed.
(p + (succ q) == r) \to (succ p) + q == r.
intros.
lapply linear nplus_gen_succ_2 to H as H0.
- decompose.
- rewrite > H1. clear H1 r.
- auto.
+ decompose. subst. auto.
qed.
theorem nplus_shift_succ_dx: \forall p,q,r.
((succ p) + q == r) \to p + (succ q) == r.
intros.
lapply linear nplus_gen_succ_1 to H as H0.
- decompose.
- rewrite > H1. clear H1 r.
- auto.
+ decompose. subst. auto.
qed.
theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
\exists q. (q1 + q2 == q) \land p + q == r2.
intros 2; elim q1; clear q1; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
- rewrite > H0. clear H0 p
+ subst.
| lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose.
- rewrite > H3. rewrite > H3 in H2. clear H3 r1.
+ decompose. subst.
lapply linear nplus_gen_succ_1 to H2 as H0.
- decompose.
- rewrite > H2. clear H2 r2.
+ decompose. subst.
lapply linear H to H4, H3 as H0.
decompose.
]; apply ex_intro; [| auto || auto ]. (**)
\exists p. (p1 + p2 == p) \land p + q == r2.
intros 2; elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
- rewrite > H0. clear H0 p1
+ subst
| lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose.
- rewrite > H3. rewrite > H3 in H2. clear H3 r1.
+ decompose. subst.
lapply linear nplus_gen_succ_2 to H2 as H0.
- decompose.
- rewrite > H2. clear H2 r2.
+ decompose. subst.
lapply linear H to H4, H3 as H0.
decompose.
]; apply ex_intro; [| auto || auto ]. (**)
\forall r2. (p + q == r2) \to r1 = r2.
intros 2. elim q; clear q; intros;
[ lapply linear nplus_gen_zero_2 to H as H0.
- rewrite > H0 in H1. clear H0 p
+ subst
| lapply linear nplus_gen_succ_2 to H1 as H0.
- decompose.
- rewrite > H3. clear H3 r1.
+ decompose. subst.
lapply linear nplus_gen_succ_2 to H2 as H0.
- decompose.
- rewrite > H2. clear H2 r2.
+ decompose. subst.
]; auto.
qed.
theorem pippo: \forall (P,Q,R:nat \to Prop).
\forall x,y. x=y \to P x \to Q x \to R x.
intros.
- try rewrite > P in Q.
+ rewrite > P in Q.
(*
-theorem pippo2: \forall (P,Q,R:nat \to Prop).
- \forall x,y. x=y \to P x \to Q x \to R x.
- intros. rewrite > H in y.
-*)
+theorem pippo: \forall (P,Q,R:nat \to Prop).
+ \forall x,y. x=y \to P x \to Q x \to R x.
+ intros. rewrite > H in y.
+*)
\ No newline at end of file
</variablelist>
</para>
</sect1>
+
+ <sect1 id="tac_subst">
+ <title>subst</title>
+ <titleabbrev>subst</titleabbrev>
+ <para><userinput>subst</userinput></para>
+ <para>
+ <variablelist>
+ <varlistentry role="tactic.synopsis">
+ <term>Synopsis:</term>
+ <listitem>
+ <para><emphasis role="bold">subst</emphasis></para>
+ </listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Pre-conditions:</term>
+ <listitem><para>
+ None.
+ </para></listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>Action:</term>
+ <listitem><para>
+ For each premise of the form
+ <command>H: x = t</command> or <command>H: t = x</command>
+ where <command>x</command> is a local variable and
+ <command>t</command> does not depend on <command>x</command>,
+ the tactic rewrites <command>H</command> wherever
+ <command>x</command> appears clearing <command>H</command> and
+ <command>x</command> afterwards.
+ </para></listitem>
+ </varlistentry>
+ <varlistentry>
+ <term>New sequents to prove:</term>
+ <listitem><para>
+ The one opened by the applied tactics.
+ </para></listitem>
+ </varlistentry>
+ </variablelist>
+ </para>
+ </sect1>
<sect1 id="tac_symmetry">
<title>symmetry</title>
<titleabbrev>symmetry</titleabbrev>
</link>
</entry>
</row>
+ <row>
+ <entry/>
+ <entry>|</entry>
+ <entry>
+ <link linkend="tac_subst">
+ <emphasis role="bold">subst</emphasis>
+ </link>
+ </entry>
+ </row>
<row>
<entry/>
<entry>|</entry>
<keyword>symmetry</keyword>
<keyword>simplify</keyword>
<keyword>split</keyword>
+ <keyword>subst</keyword>
<keyword>to</keyword>
<keyword>transitivity</keyword>
<keyword>unfold</keyword>
projects / helm.git / commitdiff