From da2c7f7bb1d9f27d998e54e09218be2245a00805 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Sep 2009 12:33:22 +0000 Subject: [PATCH] constructor accepts the arguments of the constructor... --- .../software/components/grafite/grafiteAst.ml | 2 +- .../components/grafite/grafiteAstPp.ml | 6 ++- .../grafite_engine/grafiteEngine.ml | 4 +- .../grafite_parser/grafiteParser.ml | 4 +- .../components/ng_tactics/nTactics.ml | 11 +++-- .../components/ng_tactics/nTactics.mli | 3 +- helm/software/matita/nlibrary/sets/sets.ma | 42 +++++++++---------- .../software/matita/nlibrary/topology/igft.ma | 34 ++++----------- 8 files changed, 46 insertions(+), 60 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 1d3b21392..8d0679230 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -55,7 +55,7 @@ type ntactic = | 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 diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 0ec8b9175..e21f98c27 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -98,8 +98,10 @@ let rec pp_ntactic ~map_unicode_to_tex = | 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 diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 2a04b7470..7e314670b 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -653,7 +653,9 @@ let eval_ng_tac tac = | 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 diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 8232aa672..6b80c32cf 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -253,9 +253,9 @@ EXTEND 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 -> diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index d8a9fba5e..b3f05293f 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -573,15 +573,20 @@ let case1_tac name = 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 diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index b282b04ca..4e21cbb45 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -60,4 +60,5 @@ val auto_tac: 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 diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 68a281500..89650db96 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -54,18 +54,16 @@ include "properties/relations1.ma". 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". @@ -85,13 +83,13 @@ nrecord qpowerclass (A: setoid) : Type[1] ≝ }. 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)) @@ -99,7 +97,7 @@ ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A). nqed. ndefinition qpowerclass_setoid: setoid → setoid1. - #A; napply mk_setoid1 + #A; @ [ napply (qpowerclass A) | napply (qseteq A) ] nqed. @@ -108,7 +106,7 @@ unification hint 0 ≔ A ⊢ 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;##] @@ -121,7 +119,7 @@ unification hint 0 ≔ 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) @@ -131,13 +129,13 @@ nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_s 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. @@ -177,9 +175,7 @@ nrecord compatible_equivalence_relation (A: setoid) : Type[1] ≝ }. 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 **********************) @@ -187,21 +183,21 @@ nqed. 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. @@ -222,8 +218,8 @@ ndefinition injective ≝ 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: diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index b7818372b..04f4be9c7 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -1,27 +1,5 @@ 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]; @@ -31,8 +9,9 @@ nrecord axiom_set : Type[1] ≝ { 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). @@ -49,8 +28,9 @@ ndefinition fish_set ≝ λf:∀A:axiom_set.Ω^A → A → CProp[0]. λ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). @@ -68,8 +48,8 @@ nlet corec fish_rec (A:axiom_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. @@ -97,7 +77,7 @@ alias symbol "covers" = "covers". 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; -- 2.39.2