| Assumption of loc
| Auto of loc * (string * string) list
| Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
- | Clear of loc * 'ident
+ | Clear of loc * 'ident list
| ClearBody of loc * 'ident
| Constructor of loc * int
| Contradiction of loc
| Cut of loc * 'ident option * 'term
- | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list
+ | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
| Discriminate of loc * 'term
| Elim of loc * 'term * 'term option * int option * 'ident list
| ElimType of loc * 'term * 'term option * int option * 'ident list
let terms_pp ~term_pp terms = String.concat ", " (List.map term_pp terms)
+let opt_string_pp = function
+ | None -> ""
+ | Some what -> what ^ " "
+
let rec pp_tactic ~term_pp ~lazy_term_pp =
let pp_reduction_kind = pp_reduction_kind ~term_pp in
let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
| Assumption _ -> "assumption"
| Change (_, where, with_what) ->
sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
- | Clear (_,id) -> sprintf "clear %s" id
+ | Clear (_,ids) -> sprintf "clear %s" (pp_idents ids)
| ClearBody (_,id) -> sprintf "clearbody %s" id
| Constructor (_,n) -> "constructor " ^ string_of_int n
| Contradiction _ -> "contradiction"
"cut " ^ term_pp term ^
(match ident with None -> "" | Some id -> " as " ^ id)
| Decompose (_, [], what, names) ->
- sprintf "decompose %s%s" what (pp_intros_specs (None, names))
+ sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names))
| Decompose (_, types, what, names) ->
let to_ident = function
| Ident id -> id
| Type _ -> assert false
in
let types = List.rev_map to_ident types in
- sprintf "decompose %s %s%s" (pp_idents types) what (pp_intros_specs (None, names))
+ sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names))
| Discriminate (_, term) -> "discriminate " ^ term_pp term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^
let user_types = List.rev_map to_type types in
let dbd = LibraryDb.instance () in
let mk_fresh_name_callback = namer_of names in
- Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
+ Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
| GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
| GrafiteAst.Elim (_, what, using, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
string_of_int v | v = IDENT -> v ] -> i,v ] ->
GrafiteAst.Auto (loc,params)
- | IDENT "clear"; id = IDENT ->
- GrafiteAst.Clear (loc,id)
+ | IDENT "clear"; ids = LIST1 IDENT ->
+ GrafiteAst.Clear (loc, ids)
| IDENT "clearbody"; id = IDENT ->
GrafiteAst.ClearBody (loc,id)
| IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
GrafiteAst.Contradiction loc
| IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
GrafiteAst.Cut (loc, ident, t)
- | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
- (num, idents) = intros_spec ->
+ | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
+ idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
let types = match types with None -> [] | Some types -> types in
+ let idents = match idents with None -> [] | Some idents -> idents in
let to_spec id = GrafiteAst.Ident id in
GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
| IDENT "discriminate"; t = tactic_term ->
tactics.mli:
$(H)echo " OCAMLC -i $$(tactics_mli_deps) > $@"
$(H)echo "(* GENERATED FILE, DO NOT EDIT. STAMP:`date` *)" > $@
- $(H)$(OCAMLC) -I paramodulation -i $(tactics_mli_deps) >> $@
+ $(H)$(OCAMLC) -I paramodulation -i tactics.ml >> $@
+# FG: tactics.ml was (wrongly) $(tactics_mli_deps)
UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions)
STR=$(shell $(OCAMLFIND) query str)
module E = ProofEngineTypes
module H = ProofEngineHelpers
-(*
-let induction_tac ~term status =
- let (proof, goal) = status in
- let module C = Cic in
- let module R = CicReduction in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let module S = ProofEngineStructuralRules in
- let module U = UriManager in
- let (_,metasenv,_,_) = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let termty = CicTypeChecker.type_of_aux' metasenv context term in (* per ora non serve *)
-
- T.then_ ~start:(T.repeat_tactic
- ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *)
- ~continuation:(P.intros))
- ~continuation:(P.elim_intros_simpl ~term)
- status
-;;
-*)
-
(* unexported tactics *******************************************************)
let get_name context index =
let index, ty = H.lookup_type metasenv context what in
if check_inductive_types types ty then
let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
- ~continuation:(S.clear what)
+ ~continuation:(S.clear [what])
in
E.apply_tactic tac status
else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type"))
(* roba seria ------------------------------------------------------------- *)
let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
- ?(user_types=[]) ~dbd what =
+ ?(user_types=[]) ?what ~dbd =
let decompose_tac status =
let (proof, goal) = status in
let _, metasenv,_,_ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let types = List.rev_append user_types (FwdQueries.decomposables dbd) in
let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in
- let old_context_length = List.length context in
- let tac = T.then_ ~start:(tactic ~what)
- ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic)
+ let old_context_length = List.length context in
+ let tac = match what with
+ | Some what ->
+ T.then_ ~start:(tactic ~what)
+ ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic)
+ | None ->
+ scan_tac ~old_context_length ~index:old_context_length ~tactic
in
E.apply_tactic tac status
in
E.mk_tactic decompose_tac
-
-(*
-module R = CicReduction
-
- let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status =
- let (proof, goal) = status in
- warn (lazy ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)));
- if nr_of_hyp_still_to_elim <> 0 then
- let _,metasenv,_,_ = proof in
- let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let old_context_len = List.length context in
- let termty,_ =
- CicTypeChecker.type_of_aux' metasenv context term'
- CicUniv.empty_ugraph in
- warn (lazy ("elim_clear termty= " ^ CicPp.ppterm termty));
- match termty with
- C.MutInd (uri,typeno,exp_named_subst)
- | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_)
- when (List.mem (uri,typeno,exp_named_subst) urilist) ->
- warn (lazy ("elim " ^ CicPp.ppterm termty));
- ProofEngineTypes.apply_tactic
- (T.then_
- ~start:(P.elim_intros_simpl_tac term')
- ~continuation:(
- (* clear the hyp that has just been eliminated *)
- ProofEngineTypes.mk_tactic (fun status ->
- let (proof, goal) = status in
- let _,metasenv,_,_ = proof in
- let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let new_context_len = List.length context in
- warn (lazy ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)));
- let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in
- let hyp_name =
- match List.nth context new_nr_of_hyp_still_to_elim with
- None
- | Some (Cic.Anonymous,_) -> assert false
- | Some (Cic.Name name,_) -> name
- in
- ProofEngineTypes.apply_tactic
- (T.then_
- ~start:(
- if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *)
- then begin debug_print (lazy ("%%%%%%% no clear")); T.id_tac end
- else begin debug_print (lazy ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim)))); (S.clear ~hyp:hyp_name) end)
- ~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim)))
- status
- )))
- status
- | _ ->
- let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in
- warn (lazy ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)));
- elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status
- else (* no hyp to elim left in this goal *)
- ProofEngineTypes.apply_tactic T.id_tac status
-
- in
- elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status
-*)
val decompose_tac:
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?user_types:((UriManager.uri * int) list) ->
- dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic
+ ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
~pattern:
(None,[name,Cic.Implicit (Some `Hole)], None)
(ProofEngineTypes.const_lazy_term typ);
- ProofEngineStructuralRules.clear dummy
+ ProofEngineStructuralRules.clear [dummy]
]),
Some pat,gty
| _::_ -> assert false
(function ((proof,goal) as status) ->
let _,metasenv,_,_ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let hyp =
+ let hyps =
try
match List.hd context with
- Some (Cic.Name name,_) -> name
+ Some (Cic.Name name,_) -> [name]
| _ -> assert false
with (Failure "hd") -> assert false
in
ProofEngineTypes.apply_tactic
- (ProofEngineStructuralRules.clear ~hyp) status))
+ (ProofEngineStructuralRules.clear ~hyps) status))
~continuation:(aux_tac (n + 1) tl));
T.id_tac])
status
| uri :: _ ->
Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr;
let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in
- let tac = T.then_ ~start ~continuation:(PESR.clear hyp) in
+ let tac = T.then_ ~start ~continuation:(PESR.clear ~hyps:[hyp]) in
PET.apply_tactic tac status
in
PET.mk_tactic fwd_simpl_tac
in
mk_tactic (clearbody ~hyp)
-let clear ~hyp =
- let clear ~hyp (proof, goal) =
+let clear_one ~hyp =
+ let clear_one ~hyp (proof, goal) =
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty =
in
(curi,metasenv',pbo,pty), [goal]
in
- mk_tactic (clear ~hyp)
+ mk_tactic (clear_one ~hyp)
+
+let clear ~hyps =
+ let clear hyps status =
+ let aux status hyp =
+ match apply_tactic (clear_one ~hyp) status with
+ | proof, [g] -> proof, g
+ | _ -> raise (Fail (lazy "clear: internal error"))
+ in
+ let proof, g = List.fold_left aux status hyps in
+ proof, [g]
+ in
+ mk_tactic (clear hyps)
(* Warning: this tactic has no effect on the proof term.
It just changes the name of an hypothesis in the current sequent *)
*)
val clearbody: hyp:string -> ProofEngineTypes.tactic
-val clear: hyp:string -> ProofEngineTypes.tactic
+val clear: hyps:string list -> ProofEngineTypes.tactic
(* Warning: this tactic has no effect on the proof term.
It just changes the name of an hypothesis in the current sequent *)
in
aux (n-1) tl
(status_of_single_goal_tactic_result
- (ProofEngineTypes.apply_tactic (S.clear ~hyp:name_of_hyp) status))
+ (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status))
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
let (_, metasenv, _, _) = proof in
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr 12 11:46:23 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Jun 27 17:58:26 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 assumption : ProofEngineTypes.tactic
-val auto :
+val auto :
params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
val change :
pattern:ProofEngineTypes.lazy_pattern ->
Cic.lazy_term -> ProofEngineTypes.tactic
-val clear : hyp:string -> ProofEngineTypes.tactic
+val clear : hyps:string list -> ProofEngineTypes.tactic
val clearbody : hyp:string -> ProofEngineTypes.tactic
val constructor : n:int -> ProofEngineTypes.tactic
val contradiction : ProofEngineTypes.tactic
val decompose :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
?user_types:(UriManager.uri * int) list ->
- dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic
+ ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
val demodulate :
dbd:HMysql.dbd ->
pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
-(**************************************************************************)
+clear(**************************************************************************)
(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_gen".
+set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_fwd".
-include "nat_gen.ma".
+include "nat_fwd.ma".
include "add_defs.ma".
(* primitive generation lemmas proved by elimination and inversion *)
theorem add_gen_O_1: \forall q,r. add O q r \to q = r.
- intros. elim H; clear H; clear q; clear r; intros;
+ intros. elim H; clear H q r; intros;
[ reflexivity
| clear H1. auto
].
theorem add_gen_S_1: \forall p,q,r. add (S p) q r \to
\exists s. r = (S s) \land add p q s.
- intros. elim H; clear H; clear q; clear r; intros;
+ intros. elim H; clear H q r; intros;
[
- | clear H1.
- decompose H2.
- rewrite > H1. clear H1. clear n2
+ | clear H1.
+ decompose.
+ rewrite > H1. clear H1 n2
]; apply ex_intro; [| auto || auto ]. (**)
qed.
theorem add_gen_O_2: \forall p,r. add p O r \to p = r.
intros. inversion H; clear H; intros;
[ auto
- | clear H. clear H1.
+ | clear H H1.
lapply eq_gen_O_S to H2 as H0. apply H0
].
qed.
\exists s. r = (S s) \land add p q s.
intros. inversion H; clear H; intros;
[ lapply eq_gen_S_O to H as H0. apply H0
- | clear H1. clear H3. clear r.
+ | clear H1 H3 r.
lapply eq_gen_S_S to H2 as H0. clear H2.
- rewrite > H0. clear H0. clear q.
+ rewrite > H0. clear H0 q.
apply ex_intro; [| auto ] (**)
].
qed.
theorem add_gen_O_3: \forall p,q. add p q O \to p = O \land q = O.
intros. inversion H; clear H; intros;
- [ rewrite < H1. clear H1. clear p.
+ [ rewrite < H1. clear H1 p.
auto
- | clear H. clear H1.
+ | clear H H1.
lapply eq_gen_O_S to H3 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. inversion H; clear H; intros;
- [ rewrite < H1. clear H1. clear p
+ [ rewrite < H1. clear H1 p
| clear H1.
lapply eq_gen_S_S to H3 as H0. clear H3.
- rewrite > H0. clear H0. clear r.
+ 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.
- rewrite > H0. clear H0. clear p.
+ rewrite > H0. clear H0 p.
auto
| clear H.
lapply add_gen_S_2 to H1 as H0. clear H1.
- decompose H0.
+ decompose.
lapply eq_gen_O_S to H1 as H0. apply H0
].
qed.
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.
- rewrite > H0. clear H0. clear p
+ rewrite > H0. clear H0 p
| clear H.
lapply add_gen_S_2 to H1 as H0. clear H1.
- decompose H0.
+ decompose.
lapply eq_gen_S_S to H1 as H0. clear H1.
- rewrite > H0. clear H0. clear r.
+ 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.
- rewrite > H0. clear H0. clear p
+ rewrite > H0. clear H0 p
| lapply add_gen_S_2 to H1 as H0. clear H1.
- decompose H0.
+ decompose.
lapply eq_gen_S_S to H2 as H0. clear H2.
- rewrite < H0 in H3. clear H0. clear a
+ 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.
- rewrite > H0. clear H0. clear q
+ rewrite > H0. clear H0 q
| lapply add_gen_S_1 to H1 as H0. clear H1.
- decompose H0.
+ decompose.
lapply eq_gen_S_S to H2 as H0. clear H2.
- rewrite < H0 in H3. clear H0. clear a
+ rewrite < H0 in H3. clear H0 a
]; auto.
qed.
set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_props".
-include "add_gen.ma".
+include "add_fwd.ma".
theorem add_O_1: \forall q. add O q q.
intros. elim q; clear q; auto.
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.
- rewrite > H0. clear H0. clear p
+ rewrite > H0. clear H0 p
| lapply add_gen_S_2 to H1 as H0. clear H1.
- decompose H0.
- rewrite > H2. clear H2. clear r
+ decompose.
+ rewrite > H2. clear H2 r
]; auto.
qed.
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.
- rewrite > H0. clear H0. clear p
+ rewrite > H0. clear H0 p
| lapply add_gen_S_2 to H1 as H0. clear H1.
- decompose H0.
- rewrite > H2. clear H2. clear r
+ decompose.
+ rewrite > H2. clear H2 r
]; auto.
qed.
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.
- decompose H0.
- rewrite > H1. clear H1. clear r.
+ decompose.
+ rewrite > H1. clear H1 r.
auto.
qed.
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.
- decompose H0.
- rewrite > H1. clear H1. clear r.
+ decompose.
+ rewrite > H1. clear H1 r.
auto.
qed.
\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.
- rewrite > H0. clear H0. clear p
+ rewrite > H0. clear H0 p
| lapply add_gen_S_2 to H1 as H0. clear H1.
- decompose H0.
- rewrite > H3. rewrite > H3 in H2. clear H3. clear r1.
+ decompose.
+ rewrite > H3. rewrite > H3 in H2. clear H3 r1.
lapply add_gen_S_1 to H2 as H0. clear H2.
- decompose H0.
- rewrite > H2. clear H2. clear r2.
- lapply H to H4, H3 as H0. clear H. clear H4. clear H3.
- decompose H0.
+ decompose.
+ rewrite > H2. clear H2 r2.
+ lapply H to H4, H3 as H0. clear H H4 H3.
+ decompose.
]; apply ex_intro; [| auto || auto ]. (**)
qed.
\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.
- rewrite > H0. clear H0. clear p1
+ rewrite > H0. clear H0 p1
| lapply add_gen_S_2 to H1 as H0. clear H1.
- decompose H0.
- rewrite > H3. rewrite > H3 in H2. clear H3. clear r1.
+ decompose.
+ rewrite > H3. rewrite > H3 in H2. clear H3 r1.
lapply add_gen_S_2 to H2 as H0. clear H2.
- decompose H0.
- rewrite > H2. clear H2. clear r2.
- lapply H to H4, H3 as H0. clear H. clear H4. clear H3.
- decompose H0.
+ decompose.
+ rewrite > H2. clear H2 r2.
+ lapply H to H4, H3 as H0. clear H H4 H3.
+ decompose.
]; apply ex_intro; [| auto || auto ]. (**)
qed.
\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.
- rewrite > H0 in H1. clear H0. clear p
+ rewrite > H0 in H1. clear H0 p
| lapply add_gen_S_2 to H1 as H0. clear H1.
- decompose H0.
- rewrite > H3. clear H3. clear r1.
+ decompose.
+ rewrite > H3. clear H3 r1.
lapply add_gen_S_2 to H2 as H0. clear H2.
- decompose H0.
- rewrite > H2. clear H2. clear r2.
+ decompose.
+ rewrite > H2. clear H2 r2.
]; auto.
qed.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/nat_gen".
+set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/nat_fwd".
include "library/logic/equality.ma".
include "nat_defs.ma".
<sect1 id="tac_clear">
<title>clear</title>
<titleabbrev>clear</titleabbrev>
- <para><userinput>clear H</userinput></para>
+ <para><userinput>
+ clear H<subscript>1</subscript> ... H<subscript>m</subscript>
+ </userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">clear</emphasis> &id;</para>
+ <para>
+ <emphasis role="bold">clear</emphasis>
+ &id; [&id;…]
+ </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para><command>H</command> must be an hypothesis of the
- current sequent to prove.</para>
+ <para>
+ <command>
+ H<subscript>1</subscript> ... H<subscript>m</subscript>
+ </command> must be hypotheses of the
+ current sequent to prove.
+ </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>It hides the hypothesis <command>H</command> from the
- current sequent.</para>
+ <para>
+ It hides the hypotheses
+ <command>
+ H<subscript>1</subscript> ... H<subscript>m</subscript>
+ </command> from the current sequent.
+ </para>
</listitem>
</varlistentry>
<varlistentry>
<title>decompose</title>
<titleabbrev>decompose</titleabbrev>
<para><userinput>
- decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>) H hips
+ decompose (T<subscript>1</subscript> ... T<subscript>n</subscript>)
+ H as H<subscript>1</subscript> ... H<subscript>m</subscript>
</userinput></para>
<para>
<variablelist>
<listitem>
<para>
<emphasis role="bold">decompose</emphasis>
- [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
- &id; &intros-spec;
+ [<emphasis role="bold">(</emphasis>
+ &id;…
+ <emphasis role="bold">)</emphasis>]
+ [&id;]
+ [<emphasis role="bold">as</emphasis> &id;…]
</para>
</listitem>
</varlistentry>
<term>Action:</term>
<listitem>
<para>
- Runs <command>elim H hyps</command>, clears H and tries to run
- itself recursively on each new identifier introduced by
- <command>elim</command> in the opened sequents.
+ Runs <command>
+ elim H H<subscript>1</subscript> ... H<subscript>m</subscript>
+ </command>, clears <command>H</command> and tries to run itself
+ recursively on each new identifier introduced by
+ <command>elim</command> in the opened sequents.
+ If <command>H</command> is not provided tries this operation on
+ each premise in the current context.
</para>
</listitem>
</varlistentry>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">lapply</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] &sterm; [<emphasis role="bold">to</emphasis> &sterm; [&sterm;]…] [<emphasis role="bold">as</emphasis> &id;]</para>
+ <para>
+ <emphasis role="bold">lapply</emphasis>
+ [<emphasis role="bold">depth=</emphasis>&nat;]
+ &sterm;
+ [<emphasis role="bold">to</emphasis>
+ &sterm;
+ [<emphasis role="bold">,</emphasis>&sterm;…]
+ ]
+ [<emphasis role="bold">as</emphasis> &id;]
+ </para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
<para>
- It invokes <command>letin H ≝ (t ? ... ?)</command>
+ Invokes <command>letin H ≝ (t ? ... ?)</command>
with enough <command>?</command>'s to reach the
<command>d</command>-th independent premise of
<command>t</command>
(<command>d</command> is maximum if unspecified).
- Then it istantiates (by <command>apply</command>) with
+ Then istantiates (by <command>apply</command>) with
t<subscript>1</subscript>, ..., t<subscript>n</subscript>
the <command>?</command>'s corresponding to the first
<command>n</command> independent premises of
<para><link linkend="tac_change"><emphasis role="bold">change</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> <emphasis role="bold">with</emphasis> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
</listitem>
<listitem>
- <para><link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
+ <para>
+ <link linkend="tac_clear"><emphasis role="bold">clear</emphasis></link>
+ <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>…]
+ </para>
</listitem>
<listitem>
<para><link linkend="tac_clearbody"><emphasis role="bold">clearbody</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis></para>
<listitem>
<para>
<link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
- [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
- <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis>
+ [<emphasis role="bold">(</emphasis>
+ <emphasis><link linkend="grammar.id">id</link></emphasis>…
+ <emphasis role="bold">)</emphasis>]
+ [<emphasis><link linkend="grammar.id">id</link></emphasis>]
+ [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>…]
</para>
</listitem>
<listitem>
<para><link linkend="tac_inversion"><emphasis role="bold">inversion</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>
</listitem>
<listitem>
- <para><link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link> [<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> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis><link linkend="grammar.sterm">sterm</link></emphasis>]…] [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
+ <para>
+ <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link>
+ [<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>
+ <emphasis><link linkend="grammar.sterm">sterm</link></emphasis>
+ [<emphasis role="bold">,</emphasis><emphasis><link linkend="grammar.sterm">sterm</link></emphasis>…]
+ ]
+ [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]
+ </para>
</listitem>
<listitem>
<para>
projects / helm.git / commitdiff