Cablage en dur de inversion

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

2 files changed, 55 insertions, 49 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 47c8319f1..f783b17d5 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 7f1a0943a..460d0bc38 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)