Cablage en dur de inversion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4566 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 159 insertions, 63 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 6c8ad0c1b0..47977b69b6 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -224,6 +224,10 @@ GEXTEND Gram
     [ [ "in"; idl = LIST1 hypident -> idl
       | -> [] ] ]
   ;
+  simple_clause:
+    [ [ "in"; idl = LIST1 id_or_meta -> idl
+      | -> [] ] ]
+  ;
   fixdecl:
     [ [ id = base_ident; "/"; n = natural; ":"; c = constr -> (id,n,c) ] ]
   ;
@@ -252,7 +256,7 @@ GEXTEND Gram
 	  TacIntroMove (Some id, Some id2)
       | IDENT "Intro"; IDENT "after"; id2 = identref ->
 	  TacIntroMove (None, Some id2)
-      | IDENT "Intro"; id = base_ident -> TacIntroMove (Some id, None)
+      | IDENT "Intro"; id = base_ident -> TacIntroMove (Some id,None)
       | IDENT "Intro" -> TacIntroMove (None, None)
 
       | IDENT "Assumption" -> TacAssumption
@@ -344,14 +348,32 @@ GEXTEND Gram
 	  TacSymmetry ido
       | IDENT "Transitivity"; c = constr -> TacTransitivity c
 
+      (* Equality and inversion *)
+      | IDENT "Dependent"; k =
+	  [ IDENT "Simple"; IDENT "Inversion" -> SimpleInversion
+	  | IDENT "Inversion" -> FullInversion
+	  | IDENT "Inversion_clear" -> FullInversionClear ];
+	  hyp = quantified_hypothesis; 
+	  ids = with_names; co = OPT ["with"; c = constr -> c] ->
+	    TacInversion (DepInversion (k,co,ids),hyp)
+      | IDENT "Simple"; IDENT "Inversion";
+	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	    TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
+      | IDENT "Inversion"; 
+	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	    TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
+      | IDENT "Inversion_clear"; 
+	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	    TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
+      | IDENT "Inversion"; hyp = quantified_hypothesis; 
+	  "using"; c = constr; cl = simple_clause ->
+	    TacInversion (InversionUsing (c,cl), hyp)
+
       (* Conversion *)
       | r = red_tactic; cl = clause -> TacReduce (r, cl)
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "Change"; (oc,c) = conversion; cl = clause -> TacChange (oc,c,cl)
 
-(* Unused ??
-      | IDENT "ML"; s = string -> ExtraTactic<:ast< (MLTACTIC $s) >>
-*)
     ] ]
   ;
 END;;
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index b17907844e..b03aaf8680 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -257,6 +257,10 @@ GEXTEND Gram
     [ [ "in"; idl = LIST1 hypident -> idl
       | -> [] ] ]
   ;
+  simple_clause:
+    [ [ "in"; idl = LIST1 id_or_meta -> idl
+      | -> [] ] ]
+  ;
   fixdecl:
     [ [ id = base_ident; bl=LIST0 Constr.binder; ann=fixannot;
         ":"; ty=lconstr -> (loc,id,bl,ann,ty) ] ]
@@ -381,6 +385,27 @@ GEXTEND Gram
 	  TacSymmetry ido
       | IDENT "transitivity"; c = constr -> TacTransitivity c
 
+      (* Equality and inversion *)
+      | IDENT "dependent"; k =
+	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
+	  | IDENT "inversion" -> FullInversion
+	  | IDENT "inversion_clear" -> FullInversionClear ];
+	  hyp = quantified_hypothesis; 
+	  ids = with_names; co = OPT ["with"; c = constr -> c] ->
+	    TacInversion (DepInversion (k,co,ids),hyp)
+      | IDENT "simple"; IDENT "inversion";
+	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	    TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)
+      | IDENT "inversion"; 
+	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	    TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)
+      | IDENT "inversion_clear"; 
+	  hyp = quantified_hypothesis; ids = with_names; cl = simple_clause ->
+	    TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)
+      | IDENT "inversion"; hyp = quantified_hypothesis; 
+	  "using"; c = constr; cl = simple_clause ->
+	    TacInversion (InversionUsing (c,cl), hyp)
+
       (* Conversion *)
       | r = red_tactic; cl = clause -> TacReduce (r, cl)
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 166db86758..0d72304536 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -117,19 +117,23 @@ let pr_bindings prc prlc = function
 let pr_with_bindings prc prlc (c,bl) = 
   prc c ++ hv 0 (pr_bindings prc prlc bl)
 
+let pr_with_constr prc = function
+  | None -> mt ()
+  | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c)
+
 let rec pr_intro_pattern = function
-  | IntroOrAndPattern pll ->
-      str "[" ++
-      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
-      ++ str "]"
+  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
 
+and pr_case_intro_pattern pll =
+  str "[" ++
+  hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+  ++ str "]"
+
 let pr_with_names = function
   | [] -> mt ()
-  | ids -> spc () ++ str "as [" ++
-      hv 0 (prlist_with_sep (fun () -> spc () ++ str "| ")
-              (prlist_with_sep spc pr_intro_pattern) ids ++ str "]")
+  | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
 
 let pr_hyp_location pr_id = function
   | InHyp id -> spc () ++ pr_id id
@@ -139,6 +143,11 @@ let pr_clause pr_id = function
   | [] -> mt ()
   | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
 
+let pr_simple_clause pr_id = function
+  | [] -> mt ()
+  | l -> spc () ++
+      hov 0 (str "in" ++ spc () ++ prlist_with_sep spc pr_id l)
+
 let pr_clause_pattern pr_id = function
   | (None, []) -> mt ()
   | (glopt,l) ->
@@ -156,6 +165,11 @@ let pr_induction_arg prc = function
   | ElimOnIdent (_,id) -> pr_id id
   | ElimOnAnonHyp n -> int n
 
+let pr_induction_kind = function
+  | SimpleInversion -> str "Simple Inversion"
+  | FullInversion -> str "Inversion"
+  | FullInversionClear -> str "Inversion_clear"
+
 let pr_match_pattern pr_pat = function
   | Term a -> pr_pat a
   | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]"
@@ -526,6 +540,20 @@ and pr_atom1 = function
   | TacSymmetry (Some id) -> str "Symmetry " ++ pr_ident id
   | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c
 
+  (* Equality and inversion *)
+  | TacInversion (DepInversion (k,c,ids),hyp) ->
+      hov 1 (str "Dependent " ++ pr_induction_kind k ++ 
+      pr_quantified_hypothesis hyp ++
+      pr_with_names ids ++ pr_with_constr pr_constr c)
+  | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+      hov 1 (pr_induction_kind k ++ spc () ++
+      pr_quantified_hypothesis hyp ++
+      pr_with_names ids ++ pr_simple_clause pr_ident cl)
+  | TacInversion (InversionUsing (c,cl),hyp) ->
+      hov 1 (str "Inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ 
+      str "using" ++ spc () ++ pr_constr c ++ 
+      pr_simple_clause pr_ident cl)
+
 and pr_tactic_seq_body tl = 
   hv 0 (str "[ " ++
         prlist_with_sep (fun () -> spc () ++ str "| ") prtac tl ++ str " ]")
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index c6453f076c..4435d57ab0 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -60,12 +60,24 @@ type 'a induction_arg =
   | ElimOnAnonHyp of int
 
 type intro_pattern_expr =
-  | IntroOrAndPattern of intro_pattern_expr list list
+  | IntroOrAndPattern of case_intro_pattern_expr
   | IntroWildcard
   | IntroIdentifier of identifier
 
+and case_intro_pattern_expr = intro_pattern_expr list list
+
 type 'id clause_pattern = int list option * ('id * int list) list
 
+type inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear
+
+type ('c,'id) inversion_strength =
+  | NonDepInversion of inversion_kind * 'id list * case_intro_pattern_expr
+  | DepInversion of inversion_kind * 'c option * case_intro_pattern_expr
+  | InversionUsing of 'c * 'id list
+
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
 
 type pattern_expr = constr_expr
@@ -111,10 +123,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Derived basic tactics *)
   | TacSimpleInduction of quantified_hypothesis
   | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
-      * intro_pattern_expr list list
+      * case_intro_pattern_expr
   | TacSimpleDestruct of quantified_hypothesis
   | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
-      * intro_pattern_expr list list
+      * case_intro_pattern_expr 
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
@@ -155,6 +167,9 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacSymmetry of 'id option
   | TacTransitivity of 'constr 
 
+  (* Equality and inversion *)
+  | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
+      
   (* For ML extensions *)
   | TacExtend of loc * string * ('constr,'tac) generic_argument list
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 47c8319f1b..f783b17d5d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -110,43 +110,6 @@ TACTIC EXTEND Contradiction
  [ "Contradiction" ] -> [ contradiction ]
 END
 
-(* Inversion *)
-
-open Inv
-open Leminv
-
-TACTIC EXTEND SimpleInversion
-| [ "Simple" "Inversion" quantified_hypothesis(id) ] -> [ inv None id ]
-| [ "Simple" "Inversion" quantified_hypothesis(id) "in" ne_ident_list(l) ]
-  -> [ invIn_gen None id l]
-| [ "Dependent" "Simple" "Inversion" quantified_hypothesis(id) with_constr(c) ]
-  -> [ dinv None c id ]
-END
-
-TACTIC EXTEND Inversion
-| [ "Inversion" quantified_hypothesis(id) ] -> [ inv (Some false) id ]
-| [ "Inversion" quantified_hypothesis(id) "in" ne_ident_list(l) ]
-      -> [ invIn_gen (Some false) id l]
-| [ "Dependent" "Inversion" quantified_hypothesis(id) with_constr(c) ]
-    -> [ dinv (Some false) c id ]
-END
-
-TACTIC EXTEND InversionClear
-| [ "Inversion_clear" quantified_hypothesis(id) ] -> [ inv (Some true) id ]
-| [ "Inversion_clear" quantified_hypothesis(id) "in" ne_ident_list(l) ]
-      -> [ invIn_gen (Some true) id l]
-| [ "Dependent" "Inversion_clear" quantified_hypothesis(id) with_constr(c) ]
-    -> [ dinv (Some true) c id ]
-END
-
-TACTIC EXTEND InversionUsing
-| [ "Inversion" quantified_hypothesis(id) "using" constr(c) ]
-     -> [ lemInv_gen id c ]
-| [ "Inversion" quantified_hypothesis(id) "using" constr(c)
-    "in" ne_ident_list(l) ]
-     -> [ lemInvIn_gen id c l ]
-END        
-
 (* AutoRewrite *)
 
 open Autorewrite
@@ -200,6 +163,9 @@ END
 
 (* Inversion lemmas (Leminv) *)
 
+open Inv
+open Leminv
+
 VERNAC COMMAND EXTEND DeriveInversionClear
   [ "Derive" "Inversion_clear" ident(na) ident(id) ]
   -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_clear_tac ]
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7f1a0943ab..460d0bc380 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -393,12 +393,15 @@ let intern_reference strict ist r =
 
 let rec intern_intro_pattern lf ist = function
   | IntroOrAndPattern l ->
-      IntroOrAndPattern (List.map (List.map (intern_intro_pattern lf ist)) l)
+      IntroOrAndPattern (intern_case_intro_pattern lf ist l)
   | IntroWildcard ->
       IntroWildcard
   | IntroIdentifier id ->
       IntroIdentifier (intern_ident lf ist id)
 
+and intern_case_intro_pattern lf ist =
+  List.map (List.map (intern_intro_pattern lf ist))
+
 let intern_quantified_hypothesis ist x =
   (* We use identifier both for variables and quantified hyps (no way to
      statically check the existence of a quantified hyp); thus nothing to do *)
@@ -486,6 +489,16 @@ let intern_redexp ist = function
   | (Red _ | Hnf as r) -> r
   | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c)
 
+let intern_inversion_strength lf ist = function
+  | NonDepInversion (k,idl,ids) ->
+      NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
+      intern_case_intro_pattern lf ist ids)
+  | DepInversion (k,copt,ids) ->
+      DepInversion (k, option_app (intern_constr ist) copt,
+      intern_case_intro_pattern lf ist ids)
+  | InversionUsing (c,idl) ->
+      InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
+
 (* Interprets an hypothesis name *)
 let intern_hyp_location ist = function
   | InHyp id -> InHyp (intern_hyp ist (skip_metaid id))
@@ -592,13 +605,13 @@ let rec intern_atomic lf ist x =
   | TacNewInduction (c,cbo,ids) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               List.map (List.map (intern_intro_pattern lf ist)) ids)
+               intern_case_intro_pattern lf ist ids)
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               List.map (List.map (intern_intro_pattern lf ist)) ids)
+	       intern_case_intro_pattern lf ist ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -637,6 +650,11 @@ let rec intern_atomic lf ist x =
       TacSymmetry (option_app (intern_hyp_or_metaid ist) idopt)
   | TacTransitivity c -> TacTransitivity (intern_constr ist c)
 
+  (* Equality and inversion *)
+  | TacInversion (inv,hyp) ->
+      TacInversion (intern_inversion_strength lf ist inv,
+        intern_quantified_hypothesis ist hyp)
+
   (* For extensions *)
   | TacExtend (loc,opn,l) ->
       let _ = lookup_tactic opn in
@@ -1149,12 +1167,12 @@ let interp_constr_may_eval ist gl c =
   end
 
 let rec interp_intro_pattern ist = function
-  | IntroOrAndPattern l ->
-      IntroOrAndPattern (List.map (List.map (interp_intro_pattern ist)) l)
-  | IntroWildcard ->
-      IntroWildcard
-  | IntroIdentifier id ->
-      IntroIdentifier (eval_ident ist id)
+  | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist l)
+  | IntroWildcard -> IntroWildcard
+  | IntroIdentifier id -> IntroIdentifier (eval_ident ist id)
+
+and interp_case_intro_pattern ist =
+  List.map (List.map (interp_intro_pattern ist))
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
@@ -1564,7 +1582,7 @@ and interp_atomic ist gl = function
       h_intros_until (interp_quantified_hypothesis ist gl hyp)
   | TacIntroMove (ido,ido') ->
       h_intro_move (option_app (eval_ident ist) ido)
-        (option_app (interp_hyp ist gl) ido')
+      (option_app (interp_hyp ist gl) ido')
   | TacAssumption -> h_assumption
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
   | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
@@ -1609,13 +1627,13 @@ and interp_atomic ist gl = function
   | TacNewInduction (c,cbo,ids) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (List.map (List.map (interp_intro_pattern ist)) ids)
+        (interp_case_intro_pattern ist ids)
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist gl h)
   | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (List.map (List.map (interp_intro_pattern ist)) ids)
+        (interp_case_intro_pattern ist ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist gl h1 in
       let h2 = interp_quantified_hypothesis ist gl h2 in
@@ -1660,6 +1678,21 @@ and interp_atomic ist gl = function
   | TacSymmetry c -> h_symmetry (option_app (interp_hyp ist gl) c)
   | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
 
+  (* Equality and inversion *)
+  | TacInversion (DepInversion (k,c,ids),hyp) ->
+      Inv.dinv k (option_app (pf_interp_constr ist gl) c)
+        (interp_case_intro_pattern ist ids)
+        (interp_quantified_hypothesis ist gl hyp)
+  | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
+      Inv.inv_clause k 
+        (interp_case_intro_pattern ist ids)
+        (List.map (interp_hyp ist gl) idl)
+        (interp_quantified_hypothesis ist gl hyp)
+  | TacInversion (InversionUsing (c,idl),hyp) ->
+      Leminv.lemInv_clause (interp_quantified_hypothesis ist gl hyp)
+        (pf_interp_constr ist gl c)
+        (List.map (interp_hyp ist gl) idl)
+
   (* For extensions *)
   | TacExtend (loc,opn,l) ->
       fun gl -> vernac_tactic (opn,List.map (interp_genarg ist gl) l) gl
@@ -1874,6 +1907,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacReflexivity | TacSymmetry _ as x -> x
   | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
 
+  (* Equality and inversion *)
+  | TacInversion (DepInversion (k,c,l),hyp) ->
+     TacInversion (DepInversion (k,option_app (subst_rawconstr subst) c,l),hyp)
+  | TacInversion (NonDepInversion _,_) as x -> x
+  | TacInversion (InversionUsing (c,cl),hyp) ->
+      TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp)
+
   (* For extensions *)
   | TacExtend (_loc,opn,l) ->
       TacExtend (loc,opn,List.map (subst_genarg subst) l)