| NCases of loc * CicNotationPt.term * npattern
| NCase1 of loc * string
| NChange of loc * npattern * CicNotationPt.term
- | NConstructor of loc * int option
+ | NConstructor of loc * int option * CicNotationPt.term list
| NElim of loc * CicNotationPt.term * npattern
| NGeneralize of loc * npattern
| NId of loc
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
- | NConstructor (_,None) -> "@"
- | NConstructor (_,Some x) -> "@" ^ string_of_int x
+ | NConstructor (_,None,l) -> "@ " ^
+ String.concat " " (List.map CicNotationPp.pp_term l)
+ | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
+ String.concat " " (List.map CicNotationPp.pp_term l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
| GrafiteAst.NChange (_loc, pat, ww) ->
NTactics.change_tac
~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww)
- | GrafiteAst.NConstructor (_loc,num) -> NTactics.constructor_tac ?num
+ | GrafiteAst.NConstructor (_loc,num,args) ->
+ NTactics.constructor_tac
+ ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
| GrafiteAst.NDot _ -> NTactics.dot_tac
| GrafiteAst.NElim (_loc, what, where) ->
NTactics.elim_tac
G.NCases (loc, what, where)
| IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
G.NChange (loc, what, with_what)
- | SYMBOL "@"; num = OPT NUMBER ->
+ | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
G.NConstructor (loc,
- match num with None -> None | Some x -> Some (int_of_string x))
+ (match num with None -> None | Some x -> Some (int_of_string x)),l)
| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
G.NElim (loc, what, where)
| IDENT "ngeneralize"; p=pattern_spec ->
if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
;;
-let constructor ?(num=1) status goal =
+let constructor ?(num=1) ~args status goal =
if num < 1 then fail (lazy "constructor numbers begin with 1");
let gty = get_goalty status goal in
let status, (r,_,_,_) = analyse_indty status gty in
let ref = NReference.mk_constructor num r in
- exec (apply_tac ("",0,Ast.NRef ref)) status goal
+ let t =
+ if args = [] then Ast.NRef ref else
+ Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
+ ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
+ in
+ exec (apply_tac ("",0,t)) status goal
;;
-let constructor_tac ?num = distribute_tac (constructor ?num);;
+let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);;
let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
let gty = get_goalty status goal in
params:(NTacStatus.tactic_term list * (string * string) list) ->
's NTacStatus.tactic
-val constructor_tac : ?num:int -> 's NTacStatus.tactic
+val constructor_tac :
+ ?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic
ndefinition seteq: ∀A. equivalence_relation1 (Ω^A).
#A; napply mk_equivalence_relation1
[ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S)
- | #S; napply conj; napply subseteq_refl
- | #S; #S'; *; #H1; #H2; napply conj; nassumption
- | #S; #T; #U; *; #H1; #H2; *; #H3; #H4; napply conj; napply subseteq_trans;
+ | #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.
include "sets/setoids1.ma".
ndefinition powerclass_setoid: Type[0] → setoid1.
- #A; napply mk_setoid1
- [ napply (Ω^A)
- | napply seteq ]
+ #A; @[ napply (Ω^A)| napply seteq ]
nqed.
include "hints_declaration.ma".
}.
ndefinition Full_set: ∀A. qpowerclass A.
- #A; napply mk_qpowerclass
+ #A; @
[ napply (full_set A)
| #x; #x'; #H; napply refl1; ##]
nqed.
ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A).
- #A; napply mk_equivalence_relation1
+ #A; @
[ napply (λS,S'. S = S')
| #S; napply (refl1 ? (seteq A))
| #S; #S'; napply (sym1 ? (seteq A))
nqed.
ndefinition qpowerclass_setoid: setoid → setoid1.
- #A; napply mk_setoid1
+ #A; @
[ napply (qpowerclass A)
| napply (qseteq A) ]
nqed.
carr1 (qpowerclass_setoid A) ≡ qpowerclass A.
nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP.
- #A; napply mk_binary_morphism1
+ #A; @
[ napply (λx,S. x ∈ S)
| #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; napply mk_iff; #H;
##[ napply Hb1; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha^-1;##]
A : setoid, x, S ⊢ (mem_ok A) x S ≡ mem A S x.
nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP.
- #A; napply mk_binary_morphism1
+ #A; @
[ napply (λS,S'. S ⊆ S')
| #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; napply mk_iff; #H
[ napply (subseteq_trans … a)
nqed.
nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A).
- #A; napply mk_binary_morphism1
- [ #S; #S'; napply mk_qpowerclass
+ #A; @
+ [ #S; #S'; @
[ napply (S ∩ S')
- | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); napply mk_iff; *; #H1; #H2; napply conj
+ | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); napply mk_iff; *; #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; napply conj; #x; nwhd in ⊢ (% → %); #H
+ ##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; @; #x; nwhd in ⊢ (% → %); #H
[ napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption
| napply (. ((#‡Ha)‡(#‡Hb))); nassumption ]##]
nqed.
}.
ndefinition quotient: ∀A. compatible_equivalence_relation A → setoid.
- #A; #R; napply mk_setoid
- [ napply A
- | napply R]
+ #A; #R; @ A R;
nqed.
(******************* first omomorphism theorem for sets **********************)
ndefinition eqrel_of_morphism:
∀A,B. unary_morphism A B → compatible_equivalence_relation A.
#A; #B; #f; napply mk_compatible_equivalence_relation
- [ napply mk_equivalence_relation
+ [ @
[ napply (λx,y. f x = f y)
| #x; napply refl | #x; #y; napply sym | #x; #y; #z; napply trans]
##| #x; #x'; #H; nwhd; napply (.= (†H)); napply refl ]
nqed.
ndefinition canonical_proj: ∀A,R. unary_morphism A (quotient A R).
- #A; #R; napply mk_unary_morphism
+ #A; #R; @
[ napply (λx.x) | #a; #a'; #H; napply (compatibility … R … H) ]
nqed.
ndefinition quotiented_mor:
∀A,B.∀f:unary_morphism A B.
unary_morphism (quotient … (eqrel_of_morphism … f)) B.
- #A; #B; #f; napply mk_unary_morphism
+ #A; #B; #f; @
[ napply f | #a; #a'; #H; nassumption]
nqed.
nlemma first_omomorphism_theorem_functions2:
∀A,B.∀f: unary_morphism A B.
surjective … (Full_set ?) (Full_set ?) (canonical_proj ? (eqrel_of_morphism … f)).
- #A; #B; #f; nwhd; #y; #Hy; napply (ex_intro … y); napply conj
- [ napply I | napply refl]
+ #A; #B; #f; nwhd; #y; #Hy; @ y; @ [ napply I | napply refl]
+ (* bug, prova @ I refl *)
nqed.
nlemma first_omomorphism_theorem_functions3:
include "sets/sets.ma".
-nrecord powerset (X : Type[0]) : Type[1] ≝ { char : X → CProp[0] }.
-
-interpretation "char" 'subset p = (mk_powerset ? p).
-
-interpretation "pwset" 'powerset a = (powerset a).
-
-interpretation "in" 'mem a X = (char ? X a).
-
-ndefinition subseteq ≝ λA.λU,V : Ω^A.
- ∀x.x ∈ U → x ∈ V.
-
-interpretation "subseteq" 'subseteq u v = (subseteq ? u v).
-
-ndefinition overlaps ≝ λA.λU,V : Ω^A.
- ∃x.x ∈ U ∧ x ∈ V.
-
-interpretation "overlaps" 'overlaps u v = (overlaps ? u v).
-(*
-ndefinition intersect ≝ λA.λu,v:Ω\sup A.{ y | y ∈ u ∧ y ∈ v }.
-
-interpretation "intersect" 'intersects u v = (intersect ? u v).
-*)
nrecord axiom_set : Type[1] ≝ {
S:> Type[0];
I: S → Type[0];
ndefinition cover_set ≝ λc:∀A:axiom_set.Ω^A → A → CProp[0].λA,C,U.
∀y.y ∈ C → c A U y.
+(* a \ltri b *)
notation "hvbox(a break ◃ b)" non associative with precedence 45
-for @{ 'covers $a $b }. (* a \ltri b *)
+for @{ 'covers $a $b }.
interpretation "covers set temp" 'covers C U = (cover_set ?? C U).
λA,U,V.
∃a.a ∈ V ∧ f A U a.
+(* a \ltimes b *)
notation "hvbox(a break ⋉ b)" non associative with precedence 45
-for @{ 'fish $a $b }. (* a \ltimes b *)
+for @{ 'fish $a $b }.
interpretation "fish set temp" 'fish A U = (fish_set ?? U A).
∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
#a; #p; napply cfish;
##[ napply H1; napply p;
-##| #i; ncases (H2 a p i); #x; *; #xC; #xP; napply ex_intro; ##[napply x]
- napply conj; ##[ napply xC ] napply (fish_rec ? U P); nassumption;
+##| #i; ncases (H2 a p i); #x; *; #xC; #xP; @; ##[napply x]
+ @; ##[ napply xC ] napply (fish_rec ? U P); nassumption;
##]
nqed.
ntheorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
#A; #a; #U; #V; #aV; #aU; ngeneralize in match aV; (* clear aV *)
nelim aU;
-##[ #b; #bU; #bV; napply ex_intro; ##[ napply b] napply conj; nassumption;
+##[ #b; #bU; #bV; @; ##[ napply b] @; nassumption;
##| #b; #i; #CaiU; #H; #bV; ncases bV in i CaiU H;
#c; #cV; #CciV; #i; #CciU; #H; ncases (CciV i); #x; *; #xCci; #xV;
napply H; nassumption;
projects / helm.git / commitdiff