New tactic "case1_tac" that make "intro" followed by case of the first

argument.

It is now possible to write things like:

napply t; ## [ #H | *W; #K1 #K2 ]

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 4f86ff6eb06e24a74948926f906ee1a7e378fdcf..2deacf2ac48bf5cde54bb68b3075889371a08788 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -51,6 +51,7 @@ type 'term just =
 
 type ntactic =
    | NApply of loc * CicNotationPt.term
+   | NCase1 of loc * string
    | NChange of loc * npattern * CicNotationPt.term
    | NElim of loc * CicNotationPt.term * npattern  
    | NId of loc

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 6a493f834a1fe24b6d866c1421741dfa1cc9c809..347eab2dabee8871f938172b44b6da856fc3ef3b 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -91,12 +91,13 @@ let pp_just ~term_pp =
 
 let pp_ntactic ~map_unicode_to_tex = function
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
+  | NCase1 (_,n) -> "*" ^ n ^ ":"
   | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
       " with " ^ CicNotationPp.pp_term wwhat
   | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
-  | NIntro (_,n) -> n
+  | NIntro (_,n) -> "#" ^ n
 ;;
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b3560150e0c9931496a5b087dd6fd4241b94e680..634ccc769129e5157564d49fd96fda33be3f88ce 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -586,6 +586,7 @@ let eval_ng_punct (_text, _prefix_len, punct) =
 let eval_ng_tac (text, prefix_len, tac) =
   match tac with
   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
+  | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 
        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index b3bbaf3f8d94d68d3a6cfe6c8b4b90597273f744..fa2680811c38e7bfebeb014a80cb4d028189dc26 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -187,6 +187,9 @@ EXTEND
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         GrafiteAst.NElim (loc, what, where)
     | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
+    | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
+    | SYMBOL "*"; n=IDENT ->
+        GrafiteAst.NCase1 (loc,n)
     ]
   ];
   tactic: [

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 40a490d6bb5941bf736edbd61532e769f49acf7e..87be3279f18ade3f1f49ad8bbebb443e94251d9c 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -288,6 +288,14 @@ let typeof status where t =
   None, ctx, ty
 ;;
   
+let whd status ?delta where t =
+  let _,_,metasenv,subst,_ = status.pstatus in
+  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
+  let _,_,t = relocate ctx t in
+  let t = NCicReduction.whd ~subst ?delta ctx t in
+  None, ctx, t
+;;
+  
 let unify status where a b =
   let n,h,metasenv,subst,o = status.pstatus in
   let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
@@ -521,4 +529,28 @@ let intro_tac name =
  exact_tac
   ("",0,(CicNotationPt.Binder (`Lambda,
    (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
-;; 
+;;
+
+let case status goal =
+ let _,ctx,_ = get_goal status goal in
+ let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in
+ let ref =
+  match whd status (`Ctx ctx) ty with
+     _,_,NCic.Const ref
+   | _,_,NCic.Appl (NCic.Const ref :: _) -> ref
+   | _,_,_ -> fail (lazy ("not an inductive type")) in
+ let _,_,tl,_,i = NCicEnvironment.get_checked_indtys ref in
+ let _,_,_,cl = List.nth tl i in
+ let consno = List.length cl in
+ let t =
+  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,HExtlib.mk_list (NCic.Implicit `Term) consno)
+ in
+ let status,t,ty = refine status (`Ctx ctx) ("",ctx,t) None in
+ instantiate status goal t
+;;
+
+let case_tac = distribute_tac case;;
+
+let case1_tac name =
+ block_tac [ intro_tac name; case_tac ]
+;;

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index de8c24738b1e3d177073961a7672f16e9532ac89..fbebd4cbbfc9bc8661d6a89d7d5dfcb0407c1197 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -47,5 +47,6 @@ val apply_tac: tactic_term -> tactic
 val change_tac: where:tactic_pattern -> with_what:tactic_term -> tactic
 val elim_tac: what:tactic_term -> where:tactic_pattern -> tactic
 val intro_tac: string -> tactic
+val case1_tac: string -> tactic
 
 val pp_tac_status: tac_status -> unit

diff --git a/helm/software/matita/tests/a.ma b/helm/software/matita/tests/a.ma
index 8ca9e669aa06681de53c3cfb98a4d3ce1883317b..29432d2d3a36afadcfe34507cae8d03f7ce92377 100644 (file)
--- a/helm/software/matita/tests/a.ma
+++ b/helm/software/matita/tests/a.ma
@@ -18,13 +18,14 @@ axiom C : Prop.
 axiom a: A.
 axiom b: B.
 
+include "logic/connectives.ma".
 
 notation "#" non associative with precedence 90 for @{ 'sharp }.
 interpretation "a" 'sharp = a.
 interpretation "b" 'sharp = b. 
 
-ntheorem prova : ((A â\86\92 A → B) → (A → B) → C) → C.
+ntheorem prova : ((A â\88§ A → B) → (A → B) → C) → C.
 # H;
-napply (H ? ?) [#L | #K1; #K2]
+napply (H ? ?) [#L | *w; #K1; #K2]
 napply #.
 nqed. 
\ No newline at end of file