| NCase1 of loc * string
| NChange of loc * npattern * CicNotationPt.term
| NConstructor of loc * int option * CicNotationPt.term list
+ | NCut of loc * CicNotationPt.term
| NElim of loc * CicNotationPt.term * npattern
| NGeneralize of loc * npattern
| NId of loc
| NIntro of loc * string
+ | NLApply of loc * CicNotationPt.term
| NLetIn of loc * npattern * CicNotationPt.term * string
| NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern
| NRewrite of loc * direction * CicNotationPt.term * npattern
pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+ | NAuto (_,(l,flgs)) ->
+ "nauto" ^
+ (if l <> [] then (" by " ^
+ (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
+ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NConstructor (_,None,l) -> "@ " ^
| NCase1 (_,n) -> "*" ^ n ^ ":"
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
+ | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
+ | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t
| NRewrite (_,dir,n,where) -> "nrewrite " ^
(match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
" " ^ CicNotationPp.pp_term n ^ " " ^ pp_tactic_pattern where
- | NAuto (_,(l,flgs)) ->
- "nauto" ^
- (if l <> [] then (" by " ^
- (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^
- String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED"
| NDot _ -> "##."
| NSemicolon _ -> "##;"
| GrafiteAst.NConstructor (_loc,num,args) ->
NTactics.constructor_tac
?num ~args:(List.map (fun x -> text,prefix_len,x) args)
+ | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
NTactics.elim_tac
NTactics.generalize_tac ~where:(text,prefix_len,where)
| GrafiteAst.NId _ -> (fun x -> x)
| GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+ | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t)
| GrafiteAst.NLetIn (_loc,where,what,name) ->
NTactics.letin_tac ~where:(text,prefix_len,where)
~what:(text,prefix_len,what) name
| SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
G.NConstructor (loc,
(match num with None -> None | Some x -> Some (int_of_string x)),l)
+ | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
G.NElim (loc, what, where)
| IDENT "ngeneralize"; p=pattern_spec ->
G.NGeneralize (loc, p)
+ | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
| IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
where = pattern_spec ->
G.NLetIn (loc,where,t,name)
let index_coercion status name c src tgt arity arg =
let db_src,db_tgt = status#coerc_db in
let data = (name,c,arity,arg,src,tgt) in
-
debug (lazy ("INDEX:" ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^
string_of_int arg ^ " " ^ string_of_int arity));
-
let db_src = DB.index db_src src data in
let db_tgt = DB.index db_tgt tgt data in
status#set_coerc_db (db_src, db_tgt)
) s) ]
;;
+let cut_tac t =
+ block_tac [
+ exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]);
+ branch_tac;
+ pos_tac [2]; exact_tac t;
+ shift_tac; pos_tac [1]; skip_tac;
+ merge_tac ]
+;;
+
+let lapply_tac (s,n,t) =
+ exact_tac (s,n, Ast.Appl [Ast.Implicit `JustOne; t])
+;;
+
let reduce_tac ~reduction ~where =
let change status t =
match reduction with
val change_tac:
where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term ->
's NTacStatus.tactic
+val cut_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
val elim_tac:
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
's NTacStatus.tactic
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
's NTacStatus.tactic
val case1_tac: string -> 's NTacStatus.tactic
+val lapply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
val rewrite_tac:
dir:[ `LeftToRight | `RightToLeft ] ->
what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
alias symbol "eq" = "setoid eq".
alias symbol "eq" = "setoid1 eq".
alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: qpowerclass support;
naxiom ad_hoc16: ∀a,b,c. a < c → a < b + c.
naxiom not_lt_to_le: ∀a,b. ¬ (a < b) → b ≤ a.
naxiom le_to_le_S_S: ∀a,b. a ≤ b → S a ≤ S b.
-naxiom minus_S_S: ∀a,b. S a - S b = a - b.
naxiom minus_S: ∀n. S n - n = S O.
naxiom ad_hoc17: ∀a,b,c,d,d'. a+c+d=b+c+d' → a+d=b+d'.
naxiom split_big_plus:
fst … p ≤ n ∧ snd … p < s (fst … p).
#n; #s; nelim n
[ #m; nwhd in ⊢ (??% → let p ≝ % in ?); nwhd in ⊢ (??(??%) → ?);
- nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize;
- napply conj [ napply conj [ napply refl | napply le_n ] ##| nassumption ]
+ nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize; @
+ [ @ [ napply refl | napply le_n ] ##| nassumption ]
##| #n'; #Hrec; #m; nwhd in ⊢ (??% → let p ≝ % in ?); #H;
ncases (ltb_cases m (s (S n'))); *; #H1; #H2; nrewrite > H2;
nwhd in ⊢ (let p ≝ % in ?); nwhd
| nnormalize; napply le_n]
##| nnormalize; nassumption ]
##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i));
- ngeneralize in match (Hrec (m - s (S n')) ?) in ⊢ ?
- [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj
+ nlapply (Hrec (m - s (S n')) ?)
+ [ napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; @
[##2: nassumption
- |napply conj
+ |@
[nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip]
nrewrite > (ad_hoc12 …); ##[##2: nassumption]
nwhd in ⊢ (????(?(??%)?));
∀A. ∀P:partition A. ∀n,s.
∀f:isomorphism ?? (Nat_ n) (indexes ? P).
(∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) →
- (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)).
- STOP #A; #P; #Sn; ncases Sn
- [ #s; #f; #fi;
- ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H;
+ (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) A).
+ #A; #P; #Sn; ncases Sn
+ [ #s; #f; #fi; nlapply (covers ? P); *; #_; #H;
(*
- ngeneralize in match
- (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f) in ⊢ ?;
+ nlapply
+ (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f);
*; #K; #_; nwhd in K: (? → ? → %);*)
nelim daemon (* impossibile *)
- | #n; #s; #f; #fi; napply mk_isomorphism
- [ napply mk_unary_morphism
+ | #n; #s; #f; #fi; @
+ [ @
[ napply (λm.let p ≝ iso_nat_nat_union s m n in iso_f ???? (fi (fst … p)) (snd … p))
| #a; #a'; #H; nrewrite < H; napply refl ]
##| #x; #Hx; nwhd; napply I
include "properties/relations1.ma".
ndefinition seteq: ∀A. equivalence_relation1 (Ω^A).
- #A; napply mk_equivalence_relation1
+ #A; @
[ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S)
| #S; @; napply subseteq_refl
| #S; #S'; *; #H1; #H2; @; nassumption
| #S; #T; #U; *; #H1; #H2; *; #H3; #H4; @; napply subseteq_trans;
##[##2,5: nassumption |##1,4: ##skip |##*: nassumption]##]
-nqed.
+nqed.
include "sets/setoids1.ma".
}.
ndefinition Full_set: ∀A. qpowerclass A.
- #A; @
- [ napply (full_set A)
- | #x; #x'; #H; napply refl1; ##]
+ #A; @[ napply A | #x; #x'; #H; napply refl1]
nqed.
+ncoercion Full_set: ∀A. qpowerclass A ≝ Full_set on A: setoid to qpowerclass ?.
ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A).
#A; @
nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
#A; @
[ napply (λx,S. x ∈ S)
- | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; napply mk_iff; #H;
+ | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H;
##[ napply Hb1; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha^-1;##]
##| napply Hb2; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha;##]
##]
nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
#A; @
[ napply (λS,S'. S ⊆ S')
- | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; napply mk_iff; #H
+ | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #H
[ napply (subseteq_trans … a)
[ nassumption | napply (subseteq_trans … b); nassumption ]
##| napply (subseteq_trans … a')
#A; @
[ #S; #S'; @
[ napply (S ∩ S')
- | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); napply mk_iff; *; #H1; #H2; @
+ | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); @; *; #H1; #H2; @
[##1,2: napply (. (mem_ok' …)^-1) [##3,6: nassumption |##2,5: nassumption |##*: ##skip]
##|##3,4: napply (. (mem_ok' …)) [##1,3,4,6: nassumption |##*: ##skip]##]##]
##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; @; #x; nwhd in ⊢ (% → %); #H
ndefinition eqrel_of_morphism:
∀A,B. unary_morphism A B → compatible_equivalence_relation A.
- #A; #B; #f; napply mk_compatible_equivalence_relation
+ #A; #B; #f; @
[ @
[ napply (λx,y. f x = f y)
| #x; napply refl | #x; #y; napply sym | #x; #y; #z; napply trans]
projects / helm.git / commitdiff