| Injection of loc * 'term
| Intros of loc * int option * 'ident list
| Inversion of loc * 'term
- | LApply of loc * int option * 'term list * 'term * 'ident option
+ | LApply of loc * bool * int option * 'term list * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
| Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern
sprintf "intros%s%s"
(match num with None -> "" | Some num -> " " ^ string_of_int num)
(match idents with [] -> "" | idents -> " " ^ pp_idents idents)
- | LApply (_, level_opt, terms, term, ident_opt) ->
- sprintf "lapply %s%s%s%s"
- (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")
+ | LApply (_, linear, level_opt, terms, term, ident_opt) ->
+ sprintf "lapply %s%s%s%s%s"
+ (if linear then " linear " else "")
+ (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")
(term_pp term)
(match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
(match ident_opt with None -> "" | Some ident -> " as " ^ ident)
~mk_fresh_name_callback:(namer_of names) ()
| GrafiteAst.Inversion (_, term) ->
Tactics.inversion term
- | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+ | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
let names = match ident with None -> [] | Some id -> [id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
- ~to_what what
+ Tactics.lapply ~mk_fresh_name_callback:(namer_of names)
+ ~linear ?how_many ~to_what what
| GrafiteAst.Left _ -> Tactics.left
| GrafiteAst.LetIn (loc,term,name) ->
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
| GrafiteAst.Inversion (loc, term) ->
let metasenv,term = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Inversion (loc, term)
- | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+ | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
let f term to_what =
let metasenv,term = disambiguate_term context metasenv term in
term :: to_what
in
let to_what = List.fold_right f to_what [] in
let metasenv,what = disambiguate_term context metasenv what in
- metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
| GrafiteAst.Left loc ->
metasenv,GrafiteAst.Left loc
| GrafiteAst.LetIn (loc, term, name) ->
| IDENT "inversion"; t = tactic_term ->
GrafiteAst.Inversion (loc, t)
| IDENT "lapply";
+ linear = OPT [ IDENT "linear" ];
depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
what = tactic_term;
to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
ident = OPT [ "as" ; ident = IDENT -> ident ] ->
- let to_what = match to_what with None -> [] | Some to_what -> to_what in
- GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ let linear = match linear with None -> false | Some _ -> true in
+ let to_what = match to_what with None -> [] | Some to_what -> to_what in
+ GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
| IDENT "left" -> GrafiteAst.Left loc
| IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
GrafiteAst.LetIn (loc, t, where)
(* unexported tactics *******************************************************)
-let get_name context index =
- try match List.nth context (pred index) with
- | Some (Cic.Name name, _) -> Some name
- | _ -> None
- with Invalid_argument "List.nth" -> None
-
let rec scan_tac ~old_context_length ~index ~tactic =
let scan_tac status =
let (proof, goal) = status in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let context_length = List.length context in
let rec aux index =
- match get_name context index with
+ match H.get_name context index with
| _ when index <= 0 -> (proof, [goal])
| None -> aux (pred index)
| Some what ->
| _, t -> metasenv, metas, conts
in
aux metasenv [] [] to_what (how_many, term)
-
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+
+let get_clearables context terms =
+ let aux = function
+ | Cic.Rel i
+ | Cic.Appl (Cic.Rel i :: _) -> PEH.get_name context i
+ | _ -> None
+ in
+ PEH.list_rev_map_filter aux terms
+
+let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
(* ?(substs = []) *) ?how_many ?(to_what = []) what =
let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in
let lapply_tac (proof, goal) =
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
- let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
+ let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
let conclusion =
match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas)
in
- let tac = T.then_ ~start:(letin_tac conclusion)
- ~continuation:(clearbody ~index:1)
+ let tac =
+ T.then_ ~start:(letin_tac conclusion)
+ ~continuation:(clearbody ~index:1)
in
let proof = (xuri, metasenv, u, t) in
let aux (proof, goals) (tac, goal) =
List.fold_left aux (proof, []) ((tac, goal) :: conts)
in
PET.mk_tactic lapply_tac
-
+
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
+ (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
+ let lapply_tac status =
+ let proof, goal = status in
+ let _, metasenv, _, _ = proof in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
+ let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
+ let tac =
+ if linear then
+ let hyps = get_clearables context (what :: to_what) in
+ T.then_ ~start:lapply
+ ~continuation:(PESR.clear ~hyps) (* T.try_tactic ~tactic: *)
+ else
+ lapply
+ in
+ PET.apply_tactic tac status
+ in
+ PET.mk_tactic lapply_tac
+
(* fwd **********************************************************************)
let fwd_simpl_tac
val lapply_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
+ ?linear:bool -> ?how_many:int -> ?to_what:Cic.term list -> Cic.term ->
+ ProofEngineTypes.tactic
val fwd_simpl_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
| [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
in
aux 1 context
+
+(* FG: **********************************************************************)
+
+let list_rev_map_filter f l =
+ let rec aux a = function
+ | [] -> a
+ | hd :: tl ->
+ begin match f hd with
+ | None -> aux a tl
+ | Some b -> aux (b :: a) tl
+ end
+ in
+ aux [] l
+
+let get_name context index =
+ try match List.nth context (pred index) with
+ | Some (Cic.Name name, _) -> Some name
+ | _ -> None
+ with Invalid_argument "List.nth" -> None
(* returns the index and the type of a premise in a context *)
val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
+(* FG: some helper functions ************************************************)
+
+val list_rev_map_filter: ('a -> 'b option) -> 'a list -> 'b list
+
+val get_name: Cic.context -> int -> string option
+
-(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Jun 27 17:58:26 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jun 28 17:27: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 inversion : term:Cic.term -> ProofEngineTypes.tactic
val lapply :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+ ?linear:bool ->
?how_many:int ->
?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
val left : ProofEngineTypes.tactic
-clear(**************************************************************************)
+(**************************************************************************)
(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
intros. inversion H; clear H; intros;
[ lapply eq_gen_S_O to H as H0. apply H0
| clear H1 H3 r.
- lapply eq_gen_S_S to H2 as H0. clear H2.
+ lapply linear eq_gen_S_S to H2 as H0.
rewrite > H0. clear H0 q.
apply ex_intro; [| auto ] (**)
].
intros. inversion H; clear H; intros;
[ rewrite < H1. clear H1 p
| clear H1.
- lapply eq_gen_S_S to H3 as H0. clear H3.
+ lapply linear eq_gen_S_S to H3 as H0.
rewrite > H0. clear H0 r.
]; apply ex_intro; [| auto || auto ] (**)
qed.
variant add_gen_O_3_alt: \forall p,q. add p q O \to p = O \land q = O.
intros 2. elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
rewrite > H0. clear H0 p.
auto
| clear H.
- lapply add_gen_S_2 to H1 as H0. clear H1.
+ lapply linear add_gen_S_2 to H1 as H0.
decompose.
- lapply eq_gen_O_S to H1 as H0. apply H0
+ lapply linear eq_gen_O_S to H1 as H0. apply H0
].
qed.
\exists s. p = S s \land add s q r \lor
q = S s \land add p s r.
intros 2. elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
rewrite > H0. clear H0 p
| clear H.
- lapply add_gen_S_2 to H1 as H0. clear H1.
+ lapply linear add_gen_S_2 to H1 as H0.
decompose.
- lapply eq_gen_S_S to H1 as H0. clear H1.
+ lapply linear eq_gen_S_S to H1 as H0.
rewrite > H0. clear H0 r.
]; apply ex_intro; [| auto || auto ]. (**)
qed.
theorem add_gen_eq_2_3: \forall p,q. add p q q \to p = O.
intros 2. elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
rewrite > H0. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
decompose.
- lapply eq_gen_S_S to H2 as H0. clear H2.
+ lapply linear eq_gen_S_S to H2 as H0.
rewrite < H0 in H3. clear H0 a
]; auto.
qed.
theorem add_gen_eq_1_3: \forall p,q. add p q p \to q = O.
intros 1. elim p; clear p; intros;
- [ lapply add_gen_O_1 to H as H0. clear H.
+ [ lapply linear add_gen_O_1 to H as H0.
rewrite > H0. clear H0 q
- | lapply add_gen_S_1 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_1 to H1 as H0.
decompose.
- lapply eq_gen_S_S to H2 as H0. clear H2.
+ lapply linear eq_gen_S_S to H2 as H0.
rewrite < H0 in H3. clear H0 a
]; auto.
qed.
theorem add_S_1: \forall p,q,r. add p q r \to add (S p) q (S r).
intros 2. elim q; clear q;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
rewrite > H0. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
decompose.
rewrite > H2. clear H2 r
]; auto.
theorem add_sym: \forall p,q,r. add p q r \to add q p r.
intros 2. elim q; clear q;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
rewrite > H0. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
decompose.
rewrite > H2. clear H2 r
]; auto.
theorem add_shift_S_sx: \forall p,q,r. add p (S q) r \to add (S p) q r.
intros.
- lapply add_gen_S_2 to H as H0. clear H.
+ lapply linear add_gen_S_2 to H as H0.
decompose.
rewrite > H1. clear H1 r.
auto.
theorem add_shift_S_dx: \forall p,q,r. add (S p) q r \to add p (S q) r.
intros.
- lapply add_gen_S_1 to H as H0. clear H.
+ lapply linear add_gen_S_1 to H as H0.
decompose.
rewrite > H1. clear H1 r.
auto.
\forall q2,r2. add r1 q2 r2 \to
\exists q. add q1 q2 q \land add p q r2.
intros 2; elim q1; clear q1; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
rewrite > H0. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
decompose.
rewrite > H3. rewrite > H3 in H2. clear H3 r1.
- lapply add_gen_S_1 to H2 as H0. clear H2.
+ lapply linear add_gen_S_1 to H2 as H0.
decompose.
rewrite > H2. clear H2 r2.
- lapply H to H4, H3 as H0. clear H H4 H3.
+ lapply linear H to H4, H3 as H0.
decompose.
]; apply ex_intro; [| auto || auto ]. (**)
qed.
\forall p2,r2. add p2 r1 r2 \to
\exists p. add p1 p2 p \land add p q r2.
intros 2; elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
rewrite > H0. clear H0 p1
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
decompose.
rewrite > H3. rewrite > H3 in H2. clear H3 r1.
- lapply add_gen_S_2 to H2 as H0. clear H2.
+ lapply linear add_gen_S_2 to H2 as H0.
decompose.
rewrite > H2. clear H2 r2.
- lapply H to H4, H3 as H0. clear H H4 H3.
+ lapply linear H to H4, H3 as H0.
decompose.
]; apply ex_intro; [| auto || auto ]. (**)
qed.
theorem add_conf: \forall p,q,r1. add p q r1 \to
\forall r2. add p q r2 \to r1 = r2.
intros 2. elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
rewrite > H0 in H1. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
decompose.
rewrite > H3. clear H3 r1.
- lapply add_gen_S_2 to H2 as H0. clear H2.
+ lapply linear add_gen_S_2 to H2 as H0.
decompose.
rewrite > H2. clear H2 r2.
]; auto.
<title>lapply</title>
<titleabbrev>lapply</titleabbrev>
<para><userinput>
- lapply depth=d t
+ lapply linear depth=d t
to t<subscript>1</subscript>, ..., t<subscript>n</subscript> as H
</userinput></para>
<para>
<listitem>
<para>
<emphasis role="bold">lapply</emphasis>
+ [<emphasis role="bold">linear</emphasis>]
[<emphasis role="bold">depth=</emphasis>&nat;]
&sterm;
[<emphasis role="bold">to</emphasis>
Usually the other <command>?</command>'s preceding the
<command>n</command>-th independent premise of
<command>t</command> are istantiated as a consequence.
+ If the <command>linear</command> flag is specified and if
+ <command>t, t<subscript>1</subscript>, ..., t<subscript>n</subscript></command>
+ are (applications of) premises in the current context, they are
+ <command>clear</command>ed.
</para>
</listitem>
</varlistentry>
<listitem>
<para>
<link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
+ [<emphasis role="bold">linear</emphasis>]
[<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>]
<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
[<emphasis role="bold">to</emphasis>
projects / helm.git / commitdiff