diff options
| -rw-r--r-- | tactics/contradiction.ml | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml new file mode 100644 index 0000000000..58b85297f0 --- /dev/null +++ b/tactics/contradiction.ml @@ -0,0 +1,34 @@ +open Util +open Term +open Proof_type +open Hipattern +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" + +(* Absurd *) +let absurd c gls = + (tclTHENS + (tclTHEN (elim_type (build_coq_False ())) (cut c)) + ([(tclTHENS + (cut (applist(build_coq_not (),[c]))) + ([(tclTHEN intros + ((fun gl -> + let ida = pf_nth_hyp_id gl 1 + and idna = pf_nth_hyp_id gl 2 in + exact_no_check (applist(mkVar idna,[mkVar ida])) gl))); + tclIDTAC])); + tclIDTAC])) gls + +let contradiction gls = + tclTHENLIST [ intros; elim_type (build_coq_False ()); assumption ] gls |