From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Sep 2009 12:33:22 +0000 (+0000)
Subject: constructor accepts the arguments of the constructor...
X-Git-Tag: make_still_working~3473
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da2c7f7bb1d9f27d998e54e09218be2245a00805;p=helm.git

constructor accepts the arguments of the constructor...
---

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;