Extension de Contradiction au cas d'hypotheses ~A et A dans le contexte

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

1 files changed, 63 insertions, 11 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 58b85297f0..ab7f0c550a 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
 open Util
 open Term
 open Proof_type
@@ -6,17 +16,10 @@ open Tacmach
 open Tacticals
 open Tactics
 open Coqlib
-
-(* Contradiction *)
-
-let contradiction_on_hyp id gl =
-  let hyp = pf_get_hyp_typ gl id in
-  if is_empty_type hyp then
-    simplest_elim (mkVar id) gl
-  else 
-    error "Not a contradiction"
+open Reductionops
 
 (* Absurd *)
+
 let absurd c gls =
   (tclTHENS
      (tclTHEN (elim_type (build_coq_False ())) (cut c)) 
@@ -30,5 +33,54 @@ let absurd c gls =
             tclIDTAC]));
        tclIDTAC])) gls
 
-let contradiction gls = 
-  tclTHENLIST [ intros; elim_type (build_coq_False ()); assumption ] gls
+(* Contradiction *)
+
+let filter_hyp f tac gl =
+  let rec seek = function
+    | [] -> raise Not_found
+    | (id,_,t)::rest when f t -> tac id gl
+    | _::rest -> seek rest in
+  seek (pf_hyps gl)
+
+let contradiction_context gl =
+  let env = pf_env gl in
+  let sigma = project gl in
+  let rec seek_neg l gl = match l with
+    | [] ->  error "No such contradiction"
+    | (id,_,typ)::rest ->
+	let typ = whd_betadeltaiota env sigma typ in
+	if is_empty_type typ then
+	  simplest_elim (mkVar id) gl
+	else match kind_of_term typ with
+	  | Prod (na,t,u) when is_empty_type u ->
+	      (try
+		filter_hyp (fun typ -> pf_conv_x_leq gl typ t) 
+		  (fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
+		  gl
+	      with Not_found -> seek_neg rest gl)
+	  | _ -> seek_neg rest gl in
+  seek_neg (pf_hyps gl) gl
+
+let contradiction = tclTHEN intros contradiction_context
+
+let is_negation_of env sigma typ t =
+  match kind_of_term (whd_betadeltaiota env sigma t) with
+    | Prod (na,t,u) -> is_empty_type u & is_conv_leq env sigma typ t
+    | _ -> false
+
+let contradiction_term c gl =
+  let env = pf_env gl in
+  let sigma = project gl in
+  let typ = pf_type_of gl c in
+  if is_empty_type typ then
+    simplest_elim c gl
+  else
+    try
+      (match kind_of_term (whd_betadeltaiota env sigma typ) with
+	| Prod (na,t,u) when is_empty_type u ->
+	    filter_hyp (fun typ -> pf_conv_x_leq gl typ t)
+	    (fun id -> simplest_elim (mkApp (c,[|mkVar id|]))) gl
+	| _ ->
+	    filter_hyp (is_negation_of env sigma typ)
+	    (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) gl)
+    with Not_found -> error "Not a contradiction"