Commit bd560f72 authored by Raphael Cauderlier's avatar Raphael Cauderlier

New certificate: absurd

parent bae98fea
...@@ -565,6 +565,7 @@ A B= if =c= proves =B a=. ...@@ -565,6 +565,7 @@ A B= if =c= proves =B a=.
The following certificates are used to reason from assumptions: The following certificates are used to reason from assumptions:
- =cert.exfalso : cert.certificate -> cert.certificate= - =cert.exfalso : cert.certificate -> cert.certificate=
- =cert.absurd : cert.certificate=
- =cert.destruct_and : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate= - =cert.destruct_and : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.destruct_or : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate -> cert.certificate= - =cert.destruct_or : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate -> cert.certificate=
- =cert.destruct_imp : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate -> cert.certificate= - =cert.destruct_imp : fol.prop -> fol.prop -> cert.certificate -> cert.certificate -> cert.certificate -> cert.certificate=
...@@ -572,20 +573,22 @@ The following certificates are used to reason from assumptions: ...@@ -572,20 +573,22 @@ The following certificates are used to reason from assumptions:
- =cert.destruct_ex : A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate -> cert.certificate -> cert.certificate= - =cert.destruct_ex : A : fol.type -> (fol.term A -> fol.prop) -> cert.certificate -> cert.certificate -> cert.certificate=
The certificate =cert.exfalso c= proves the current goal if =c= proves The certificate =cert.exfalso c= proves the current goal if =c= proves
=fol.false=. The certificate =cert.destruct_and A B c1 c2= proves the =fol.false=. The certificate =cert.absurd= proves the current goal if
current goal =C= in context =G= if =c1= proves =fol.and A B= in the context contains a pair of contradictory assumptions (an
context =G= and =c2= proves =C= in context =G= with extra assumptions assumption together with its negation). The certificate
=A= and =B=. The certificate =cert.destruct_or A B c1 c2 c3= proves =cert.destruct_and A B c1 c2= proves the current goal =C= in context
the current goal =C= in context =G= if =c1= proves =fol.or A B= in =G= if =c1= proves =fol.and A B= in context =G= and =c2= proves =C= in
context =G=, =c2= proves =C= in context =G= with extra assumption =A=, context =G= with extra assumptions =A= and =B=. The certificate
and =c3= proves =C= in context =G= with extra assumption =B=. The =cert.destruct_or A B c1 c2 c3= proves the current goal =C= in context
certificate =cert.destruct_imp A B c1 c2 c3= proves the current goal =G= if =c1= proves =fol.or A B= in context =G=, =c2= proves =C= in
=C= in context =G= if =c1= proves =fol.imp A B= in context =G=, =c2= context =G= with extra assumption =A=, and =c3= proves =C= in context
proves =A= in context =G= and =c3= proves =C= in context =G= with =G= with extra assumption =B=. The certificate =cert.destruct_imp A B
extra assumption =B=. The certificate =cert.destruct_ex A B c1 c2= c1 c2 c3= proves the current goal =C= in context =G= if =c1= proves
proves the current goal =C= in context =G= if =c1= proves =fol.ex A B= =fol.imp A B= in context =G=, =c2= proves =A= in context =G= and =c3=
and =c2= proves =C= in context =G= with an extra variable =x= of type proves =C= in context =G= with extra assumption =B=. The certificate
=A= and an extra assumption =B x=. =cert.destruct_ex A B c1 c2= proves the current goal =C= in context
=G= if =c1= proves =fol.ex A B= and =c2= proves =C= in context =G=
with an extra variable =x= of type =A= and an extra assumption =B x=.
** Equality Certificates ** Equality Certificates
......
...@@ -200,6 +200,12 @@ def exfalso (c : certificate) : certificate := ...@@ -200,6 +200,12 @@ def exfalso (c : certificate) : certificate :=
with_goal (A => with_goal (A =>
refine fol.false A (fol.false_elim A) c). 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 ;) (; trivial proves true ;)
def trivial : certificate := def trivial : certificate :=
exact fol.true fol.true_intro. exact fol.true fol.true_intro.
......
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