diff options
| -rw-r--r-- | tactics/contradiction.ml | 74 |
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" |