Commit 80698ccb authored by Raphael Cauderlier's avatar Raphael Cauderlier

Example: drinker paradox

parent 74e50ed9
......@@ -119,7 +119,7 @@ echo > .config_vars &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5" &&
find_and_check_binary "dkdep" ".native" "DKDEP" "" "" &&
#find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.6" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Dedukti v2.5" &&
#find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.6" &&
#find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Sukerujo v2.6" &&
......
include ../.config_vars
# Dedukti files
DKMS = $(wildcard *.dkm)
DKS = $(DKMS:.dkm=.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol
DKMETA_OPTIONS = -I ../fol -I ../meta -nl
all: $(DKOS)
%.dk: %.dkm
$(DKMETA) $(DKMETA_OPTIONS) $< > $@
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
# For each dependency foo.dko in the ../fol directory, the previous
# rule will try to create foo.dko here by calling "dkcheck -e" without
# file argument. This actually succeeds but does not produce any file.
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dkm
$(DKDEP) $< | sed "s/\.dkm/\.dk/" > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
depend: $(DKDEPENDS)
clean:
rm -f *.dko *.dk *.depend
install: all
mkdir -p $(INSTALL_LIB_DIR)
install -t $(INSTALL_LIB_DIR) $(DKOS)
uninstall:
for f in $(DKOS); do \
rm -f $(INSTALL_LIB_DIR)/$$f; \
done
rmdir $(INSTALL_LIB_DIR)
.PHONY: clean depend install uninstall all
#NAME drinker.
BAR : fol.type.
JOE : fol.function.
[] fol.fun_arity (JOE) --> fol.nil_type.
[] fol.fun_codomain (JOE) --> BAR.
def Joe : fol.term BAR := fol.apply_fun JOE fol.nil_term.
DRINK : fol.predicate.
[] fol.pred_arity (DRINK) --> fol.read_types (nat.S nat.O) BAR.
def drink :
x:(fol.term BAR) -> fol.prop
:=
x:(fol.term BAR) =>
fol.apply_pred DRINK (fol.cons_term BAR x fol.nil_type fol.nil_term).
def drinker_statement :
fol.prop
:=
fol.ex BAR
(x:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK (fol.cons_term BAR x fol.nil_type fol.nil_term))
(fol.all BAR
(x0:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term)))).
def ndrink :=
x:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK (fol.cons_term BAR x fol.nil_type fol.nil_term))
fol.false.
def drinker_paradox :
c:fol.prop ->
(a:(fol.term BAR) ->
((fol.proof
(fol.apply_pred DRINK (fol.cons_term BAR a fol.nil_type fol.nil_term))) ->
a0:(fol.term BAR) ->
fol.proof
(fol.apply_pred DRINK (fol.cons_term BAR a0 fol.nil_type fol.nil_term))) ->
fol.proof c) ->
fol.proof c
:=
classical.excluded_middle
(fol.all BAR
(x:(fol.term BAR) =>
fol.apply_pred DRINK (fol.cons_term BAR x fol.nil_type fol.nil_term)))
(fol.ex BAR
(x:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x fol.nil_type fol.nil_term))
(fol.all BAR
(x0:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term)))))
(x:
(a:(fol.term BAR) ->
fol.proof
(fol.apply_pred DRINK (fol.cons_term BAR a fol.nil_type fol.nil_term))) =>
fol.ex_intro BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))
(fol.all BAR
(x1:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))))
(fol.apply_fun JOE fol.nil_term)
(x0:
(fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR (fol.apply_fun JOE fol.nil_term)
fol.nil_type fol.nil_term))) =>
x))
(x:
((a:(fol.term BAR) ->
fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR a fol.nil_type fol.nil_term))) ->
c:fol.prop -> fol.proof c) =>
fol.ex_elim BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term)) fol.false)
(fol.ex BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))
(fol.all BAR
(x1:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term)))))
(classical.excluded_middle
(fol.ex BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))
fol.false))
(fol.ex BAR
(x0:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))
fol.false))
(x0:
(c:fol.prop ->
(a:(fol.term BAR) ->
((fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR a fol.nil_type fol.nil_term))) ->
c0:fol.prop -> fol.proof c0) ->
fol.proof c) ->
fol.proof c) =>
x0)
(x0:
((c:fol.prop ->
(a:(fol.term BAR) ->
((fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR a fol.nil_type fol.nil_term))) ->
c0:fol.prop -> fol.proof c0) ->
fol.proof c) ->
fol.proof c) ->
c:fol.prop -> fol.proof c) =>
fol.false_elim
(fol.ex BAR
(x1:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))
fol.false))
(x
(x1:(fol.term BAR) =>
classical.excluded_middle
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))
(x2:
(fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))) =>
x2)
(x2:
((fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))) ->
c:fol.prop -> fol.proof c) =>
fol.false_elim
(fol.apply_pred DRINK
(fol.cons_term BAR x1 fol.nil_type fol.nil_term))
(x0
(fol.ex_intro BAR
(x3 =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x3 fol.nil_type
fol.nil_term)) fol.false) x1 x2)))))))
(x0:(fol.term BAR) =>
x1:
((fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))) ->
c:fol.prop -> fol.proof c) =>
fol.ex_intro BAR
(x2:(fol.term BAR) =>
fol.imp
(fol.apply_pred DRINK
(fol.cons_term BAR x2 fol.nil_type fol.nil_term))
(fol.all BAR
(x3:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x3 fol.nil_type fol.nil_term)))) x0
(x2:
(fol.proof
(fol.apply_pred DRINK
(fol.cons_term BAR x0 fol.nil_type fol.nil_term))) =>
fol.false_elim
(fol.all BAR
(x3:(fol.term BAR) =>
fol.apply_pred DRINK
(fol.cons_term BAR x3 fol.nil_type fol.nil_term))) (
x1 x2)))).
#NAME drinker.
(; Customization of Emacs mode for Dedukti: this file is not linear
and requires a path extended with "../fol" and "../meta.
(setq-local dedukti-check-options '("-nc" "-nl" "-I" "../fol" "-I" "../meta"))
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol" "-I" "../meta"))
;)
BAR : fol.type.
(; We have to assume that the bar is not empty, that is we have a term
of type BAR. Let's call it Joe. ;)
JOE : fol.function.
[] fol.fun_arity JOE --> fol.nil_type.
[] fol.fun_codomain JOE --> BAR.
def Joe : fol.term BAR := fol.fun_apply JOE.
(; The "drink" predicate. ;)
DRINK : fol.predicate.
[] fol.pred_arity DRINK --> fol.read_types (nat.S nat.O) BAR.
def drink (x : fol.term BAR) : fol.prop := fol.pred_apply DRINK x.
def drinker_statement : fol.prop :=
fol.ex BAR (x : fol.term BAR =>
fol.imp
(drink x)
(fol.all BAR drink)).
def ndrink (x : fol.term BAR) := fol.not (drink x).
def drinker_paradox : fol.proof drinker_statement :=
tac.run drinker_statement (
cert.run drinker_statement cert.nil_ctx
(classical_cert.prop_case (fol.all BAR drink)
(; ∀ ⊢ ∃x. drink x → ∀ ;)
(cert.exists BAR Joe (cert.intro cert.assumption))
(; ¬∀ ⊢ ∃x. drink x → ∀ ;)
(cert.destruct_imp
(fol.not (fol.all BAR drink))
(fol.ex BAR ndrink)
(; ¬∀ ⊢ ¬∀ → ∃¬ ;)
(cert.exact
(fol.imp (fol.not (fol.all BAR drink))
(fol.ex BAR ndrink))
(classical_cert.not_all_is_ex_not BAR drink))
(; ¬∀ ⊢ ¬∀ ;)
cert.assumption
(; ¬∀, ∃¬ ⊢ ∃x. drink x → ∀ ;)
(cert.with_assumption (E => e =>
cert.destruct_ex BAR ndrink (cert.exact E e)
(; ¬∀, ∃¬, John, ¬drink John ⊢ ∃x. drink x → ∀ ;)
(cert.with_variable (B : fol.type => John : fol.term B =>
cert.exists B John
(; ¬∀, ∃¬, John, ¬drink John ⊢ drink John → ∀ ;)
(cert.intro cert.absurd)))))))).
......@@ -616,9 +616,56 @@ A a a' c1 c2= proves =B= if =c1= proves =eq.eq A a a'= and =c2= proves
=B= in which each occurrence of =a= has been replaced by =a'= (see [[* Substitution and unification][the
section on substitution]]).
* TODO Examples
** Classical Reasoning
The file [[./fol/classical.dk][fol/classical.dk]] declares the axiom scheme of excluded middle:
=classical.excluded_middle : P : fol.prop -> fol.proof (fol.or P (fol.not P))=
The file [[./meta/classical_cert.dk][meta/classical_cert.dk]] contains certificate combinators to ease reasoning in classical logic:
- =classical_cert.prop_case : fol.prop -> cert.certificate -> cert.certificate -> cert.certificate=
- =classical_cert.contradict : cert.certificate -> cert.certificate=
=classical_cert.prop_case= is used to reason by case on a the truth of
a formula using excluded middle; =classical_cert.prop_case A c1 c2=
proves the current goal =B= in context =G= if =c1= proves =B= in
context =G= with extra assumption =A= and =c2= proves =B= in context
=G= with extra assumption =fol.not A=.
=classical_cert.contradict= is used to prove by contradiction using
double-negation elimination. =classical_cert.contradict c= proves the
current goal =A= in context =G= if =c= proves =fol.false= in context
=G= with extra assumption =fol.not A=.
These combinators are used to prove the following classical facts:
- =classical_cert.nnpp : P : fol.prop -> fol.proof (fol.imp (fol.not (fol.not P)) P)=
- =classical_cert.not_and_is_or_not : A : fol.prop -> B : fol.prop -> fol.proof (fol.imp (fol.not (fol.and A B)) (fol.or (fol.not A) (fol.not B)))=
- =classical_cert.not_all_is_ex_not (A : fol.type) (P : fol.term A -> fol.prop) : fol.proof (fol.imp (fol.not (fol.all A (x => P x)))=
* Examples
** Drinker paradox
** Decision procedures
The file [[./example/drinker.dkm][example/drinker.dkm]] is an example of classical reasoning. It
shows how to prove Smullyan's famous "drinker paradox": in an
non-empty bar, there is somebody such that, if he is drinking then
everyone in the bar is drinking.
The =.dkm= extension indicates that this file is intended to be
normalized by Meta Dedukti to produce the file =example/drinker.dk= to
be checked in the safe encoding of classical first-order logic.
This problem uses a single sort representing the person present in the
bar that we write =drinker.BAR=. Since the bar is assumed non-empty,
we know that somedy, call it Joe, is in the bar hence we declare a
constant =drinker.JOE= of codomain =drinker.BAR=. Finally the
signature is achieved with the unary predicate =drinker.DRINK=
representing drinking.
The proof of the theorem uses classical features twice: it starts with
a classical reasoning by case (using the =classical_cert.prop_case=
combinator) and then uses the classical lemma
=classical_cert.not_all_is_ex_not= in the second branch.
** TODO Decision procedures
*** Minimal logic
*** Presburger arithmetic
* TODO Interactive proof development
......
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