Commit c4b8ac15 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Fix the absurd certificate.

parent a4095ae5
......@@ -202,12 +202,6 @@ def exfalso (c : certificate) : certificate :=
with_goal (A =>
refine fol.false A (fol.false_elim A) c).
(; absurd proves anything if the current context contains an
assumption and its negation. ;)
def absurd : cert.certificate :=
cert.with_assumption (P => p =>
cert.destruct_imp P fol.false cert.assumption (cert.exact P p) cert.assumption).
(; trivial proves true ;)
def trivial : certificate :=
exact fol.true fol.true_intro.
......@@ -367,6 +361,12 @@ def destruct_imp (A : prop) (B : prop) (c1 : certificate) (c2 : certificate) (c3
:=
with_goal (G => refinen (nat.S (nat.S (nat.S nat.O))) (imp A B) A (imp B G) G (ab => a => bg => bg (ab a)) c1 c2 (intro c3)).
(; absurd proves anything if the current context contains an
assumption and its negation. ;)
def absurd : cert.certificate :=
with_assumption (P => p =>
destruct_imp P fol.false assumption (exact P p) (exfalso assumption)).
(; apply A B a c proves (B a) if c proves all A B ;)
def apply (A : type) (B : term A -> prop) (a : term A) : certificate -> certificate :=
refine (all A B) (B a) (ab => ab a).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment