Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
tree: 9ca9644e35
Fetching contributors…

Cannot retrieve contributors at this time

90 lines (80 sloc) 2.861 kB
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Errors
open Term
open Hipattern
open Tacmach
open Tacticals
open Tactics
open Coqlib
open Reductionops
open Misctypes
(* Absurd *)
let absurd c gls =
let env = pf_env gls and sigma = project gls in
let _,j = Coercion.inh_coerce_to_sort Loc.ghost env
(Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in
let c = j.Environ.utj_val in
(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
(* 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 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,lbind as cl) gl =
let env = pf_env gl in
let sigma = project gl in
let typ = pf_type_of gl c in
let _, ccl = splay_prod env sigma typ in
if is_empty_type ccl then
tclTHEN (elim false cl None) (tclTRY assumption) gl
else
try
if lbind = NoBindings then
filter_hyp (is_negation_of env sigma typ)
(fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) gl
else
raise Not_found
with Not_found -> error "Not a contradiction."
let contradiction = function
| None -> tclTHEN intros contradiction_context
| Some c -> contradiction_term c
Jump to Line
Something went wrong with that request. Please try again.