From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 14 Sep 2009 08:45:55 +0000 (+0000)
Subject: New tactics ncut and nlapply.
X-Git-Tag: make_still_working~3469
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b91d9e60b0a5f450d2725d4b9bb3ed7f81ef6d3a;p=helm.git

New tactics ncut and nlapply.
---

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 8d0679230..5c8f461c1 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -56,10 +56,12 @@ type ntactic =
    | 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
diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index e21f98c27..3d6b86492 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -96,6 +96,11 @@ let rec pp_ntactic ~map_unicode_to_tex =
   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) -> "@ " ^
@@ -105,18 +110,15 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | 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 _ -> "##;"
diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 7e314670b..f7df56315 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -656,6 +656,7 @@ let eval_ng_tac tac =
   | 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 
@@ -666,6 +667,7 @@ let eval_ng_tac 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
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 6b80c32cf..c9ece6dba 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -256,10 +256,12 @@ EXTEND
     | 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)
diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 037c5c6e2..7d5d0101a 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -46,13 +46,11 @@ class status =
 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)
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index b3f05293f..0ba8e4b44 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -402,6 +402,19 @@ let generalize_tac ~where =
    ) 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
diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 4e21cbb45..9afd918ea 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -32,6 +32,7 @@ val assumption_tac: 's NTacStatus.tactic
 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
@@ -40,6 +41,7 @@ val cases_tac:
    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 -> 
diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma
index e83175f18..e33ddfa1d 100644
--- a/helm/software/matita/nlibrary/sets/partitions.ma
+++ b/helm/software/matita/nlibrary/sets/partitions.ma
@@ -22,11 +22,6 @@ include "datatypes/pairs.ma".
 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;
@@ -63,7 +58,6 @@ naxiom ad_hoc15: ∀a,a',b,c. a=a' → b < c → a + b < c + a'.
 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:
@@ -81,8 +75,8 @@ ntheorem iso_nat_nat_union_char:
     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
@@ -91,10 +85,10 @@ ntheorem iso_nat_nat_union_char:
         | 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 ⊢ (????(?(??%)?));
@@ -135,17 +129,16 @@ nlemma partition_splits_card:
  ∀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
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 89650db96..f3bd3b889 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -52,13 +52,13 @@ nqed.
 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".
 
@@ -83,10 +83,9 @@ nrecord qpowerclass (A: setoid) : Type[1] ≝
  }.
 
 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; @
@@ -108,7 +107,7 @@ unification hint 0 ≔ 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;##]
      ##]
@@ -121,7 +120,7 @@ unification hint 0 ≔
 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')
@@ -132,7 +131,7 @@ nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_
  #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
@@ -182,7 +181,7 @@ nqed.
 
 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]