#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists test1 (P,Q::Prop) :: And P Q > Or P Q = external "fol"If you typecheck the above code, you obtain the following message in the buffer "* External Info *":
Proved by FOL And P Q > Or P QThis means that Gandalf proved that for all propositions P and Q, it is the case that P ∧ Q → P ∨ Q. Observe how this formula is represented as a type. The type
Prop
is assumed to contain all propositions.
The above occurrence of the expression external "fol"
can be regarded as a proof term.
\(h :: And P Q) > introOr_lft P Q (elimAnd_fst P Q h)
where introOr_lft
and elimAnd_fst
are constants defined in the library LogicSet.alfa
.
Should you get the message
"Plugin error: FOL could not prove
" instead of the above message,
at least one of Gandalf, Santa, and the Agda's plugin feature
is not installed correctly. If you have installed Agda using the
Windows binary installer, it is likely that you have not yet installed cygwin.
Exists P
.
Here, P
must be a predicate on a set A,
that is, a function of the type A > Prop
which sends each element of the set A
to a proposition.
#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists test2 (A::Set) (P::A > Prop) (a::A) :: P a > Exists P = external "fol"If you typecheck the above code, you obtain the following message:
Proved by FOL P a > Exists A PThis means that Gandalf proved that for any set A, any predicate P on A, and any element a of A, it is the case that P(a) → ∃x. P(x).
(x :: A) > P x
to express a universally quantified formula.
Here, P
must have the type A > Prop
.
#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists test3 (A::Set) (P::A > Prop) :: (a::A) > ((x::A) > P x) > P a = external "fol"
Proved by FOL (a::A) > ((x::A) > P x) > P a
(a::A)
to the `telescope' position
as follows
since a
is not
a proposition used as an assumption in the proof:
#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists test3b (A::Set) (P::A > Prop) (a::A) :: ((x::A) > P x) > P a = external "fol"In this case, we are to prove that (∀x. P(x)) → P(a), knowing that
a
is an element of A
.
Proved by FOL ((x::A) > P x) > P aThe difference is not important since they essentially prove the same thing.
#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists test4 (A::Set) (P::A > Prop) :: Exists A P = external "fol"You will get the following message because ∃x. P(x) is not provable for arbitrary
A
and P
.
Plugin error: FOL could not prove Exists A PIn this case, the message "Type correct" will not be displayed in the info bar of the Emacs buffer. This means that some proofs have not been found.
#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists test5 :: (P::Prop) > Or P (Not P) = external "fol"
Proved by FOL (P::Set) > Or P (Not P)
#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists test6 (A::Set) (P::A > Prop) :: Not ((x::A) > P x) > Exists (\(x::A) > Not (P x)) = external "fol"
Proved by FOL Not ((x::A) > P x) > Exists X (\(x::A) > Not (P x))
#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists test7 (X::Set) (P::X > Prop) :: ((x::X) > P x) > Exists P = external "fol"
Proved by FOL ((x::X) > P x) > Exists X PSince the prover has assumed that
X
is nonempty,
you should never give
the empty datatype Absurd
to test7
, which would
result in a proof of contradiction:
proof_of_contradiction :: Absurd = (test7 Absurd (\(x::Absurd) > Absurd) (\(x::Absurd) > x)).sndThe selector
.snd
extracts the proof part of
the dependent pair representing the bogus witness.
Proposition  Agda Representation 

¬ P  Not P

P ∧ Q  And P Q

P ∨ Q  Or P Q

P → Q  P > Q

T  Taut

⊥  Absurd

∀x∈P. Q  (x :: P) > Q

∃x∈P. Q  Exists (\(x :: P) > Q)

Set
:
postulate Man :: Set
postulate IsFatherOf :: Man > Man > Prop  a predicate symbol postulate fatherOf :: Man > Man  a function symbol
external "fol"
expressions
so that the plugin can use them. These extra arguments
can be supplied as many as you want.
postulate fatherLaw :: (x::Man) > IsFatherOf x (fatherOf x) hasFather :: (x::Man) > Exists (IsFatherOf x) = external "fol" fatherLaw
hasFather
defined above expresses a lemma.
Lemmas can be passed as extra arguments
to the external "fol"
expressions
so that the plugin can use them.
In fact, the plugin does not distinguish between lemmas and axioms
in the extra arguments; it just looks at their types.
#include "LogicSet.alfa" open LogicSet use Prop,Not,And,Or,Taut,Absurd,Exists postulate Man :: Set  Man is a set of human beings in this village postulate Shaves :: Man > Man > Prop  Shaves x y means that x shaves the beard of y postulate Barber :: Man > Prop  Barber x means that x is a barber postulate barberLaw1 :: (x::Man) > Barber x > (y::Man) > Not (Shaves y y) > Shaves x y postulate barberLaw2 :: (x::Man) > Barber x > (y::Man) > Shaves y y > Not (Shaves x y) noBarbers :: Not (Exists Barber) noBarbers = external "fol" barberLaw1 barberLaw2
Proved by FOL Not (Exists Man Barber)