Commit 323146ea authored by g.genestier's avatar g.genestier

Merge branch 'master' of https://git.lsv.fr/genestier/PleinDeDk

parents a1c8c900 fbd1a896

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.

......@@ -13,6 +13,11 @@ iProverModulo_dk/*
iProverModulo/*
dklib-master/*
TermChecker/*.txt
bench-constr/*
Bible_examples/*
JFLA/*
tests/*
example/*
temp/*
*.tmp
*.tar*
\ No newline at end of file
DKS=$(wildcard *.dk)
# DKOS need not have the same name that the corresponding Dedukti
# files (modulogic.dk becomes zen.dko) but for each file f.dk, dkdep
# f.dk outputs the name of the produced dko file before the ':'
# character.
DKOS=$(shell cut -d ':' -f 1 .depend)
DKDEP=dkdep
DKCHECK=dkcheck
all: $(DKOS)
%.dko:
$(DKCHECK) -e -nl $<
clean:
rm -f *.dko .depend
depend: .depend
.depend:
$(DKDEP) *.dk > ./.depend
-include .depend
#NAME part3.
nat : Type.
0 : nat.
S : nat -> nat.
def plus : nat -> nat -> nat.
[n] plus 0 n --> n.
[n1, n2] plus (S n1) n2 --> S (plus n1 n2).
[n] plus 0 n --> n
[n1, n2] plus (S n1) n2 --> S (plus n1 n2).
[n1, n2, n3] plus n1 (plus n2 n3) --> plus (plus n1 n2) n3.
def two := S (S 0).
def K2 := x:nat => two.
A: Type.
vector: nat -> Type.
Nil : vector 0.
Cons : n : nat -> A -> vector n -> vector (S n).
def tail: n:nat -> vector (S n) -> vector n.
[n, m, a, l] tail n (Cons m a l) --> l.
[n, a, l] tail n (Cons _ a l) --> l.
[l] tail _ (Cons _ _ l) --> l.
[n, a, l] tail n (Cons {n} a l) --> l.
#NAME part41.
s : Type.
P : s -> Type.
def Thm : x:s -> (P x) -> (P x) := x:s => a:(P x) => a.
#NAME part42.
o : Type.
s : Type.
P : s -> o.
imp : o -> o -> o.
def eps : o -> Type.
[x, y] eps (imp x y) --> (eps x) -> (eps y).
and: o -> o -> o.
[x, y] eps (and x y) --> z:o -> (eps x -> eps y -> eps z) -> eps z.
def top : o.
[ ] eps top --> z:o -> (eps z) -> (eps z).
def bot : o.
[ ] eps bot --> z:o -> (eps z).
def not : o -> o := x:o => imp x bot.
def or : o -> o -> o.
[x, y] eps (or x y)
--> z:o -> (eps x -> eps z) -> (eps y -> eps z) -> eps z.
def fa_s : (s -> o) -> o.
[y] eps (fa_s y) --> x:s -> eps (y x).
def ex_s : (s -> o) -> o.
[y] eps (ex_s y) --> z:o -> (x:s -> eps (y x) -> (eps z)) -> eps z.
#NAME part43.
nat : Type.
o : Type.
imp : o -> o -> o.
def eps : o -> Type.
[x, y] eps (imp x y) --> (eps x) -> (eps y).
and: o -> o -> o.
[x, y] eps (and x y) --> z:o -> (eps x -> eps y -> eps z) -> eps z.
def top : o.
[ ] eps top --> z:o -> (eps z) -> (eps z).
def bot : o.
[ ] eps bot --> z:o -> (eps z).
def not : o -> o := x:o => imp x bot.
def or : o -> o -> o.
[x, y] eps (or x y)
--> z:o -> (eps x -> eps z) -> (eps y -> eps z) -> eps z.
def fa_nat : (nat -> o) -> o.
[y] eps (fa_nat y) --> x:nat -> eps (y x).
def ex_nat : (nat -> o) -> o.
[y] eps (ex_nat y) --> z:o -> (x:nat -> eps (y x) -> (eps z)) -> eps z.
0 : nat.
S : nat -> nat.
def plus : nat -> nat -> nat.
def times : nat -> nat -> nat.
def equal : nat -> nat -> o.
N : nat -> o.
[y] plus 0 y --> y
[x, y] plus (S x) y --> S (plus x y).
[y] times 0 y --> 0
[x, y] times (S x) y --> plus (times x y) y.
[ ] equal 0 0 --> top
[x] equal (S x) 0 --> bot
[y] equal 0 (S y) --> bot
[x, y] equal (S x) (S y) --> equal x y.
[n] eps (N n) -->
k:(nat->o) -> eps (k 0) ->
eps ( fa_nat (y:nat => imp (N y) (imp (k y) (k (S y))) ) ) ->
eps (k n).
def tt : eps top := z:o => p:eps z => p.
def k := x:nat => equal (plus x 0) x.
def z_r_neutral : eps ( fa_nat ( x => imp (N x) (k x)))
:= x:nat => p:eps (N x) =>
p k tt (y:nat => q: eps (N y) => r:eps (k y) => r).
#NAME part44.
o : Type.
def eps : o -> Type.
i : Type.
imp : o -> o -> o.
[x, y] eps (imp x y) --> (eps x) -> (eps y).
def bot : o.
[ ] eps bot --> z:o -> (eps z).
def not : o -> o := x:o => imp x bot.
def or : o -> o -> o.
[x, y] eps (or x y)
--> z:o -> (eps x -> eps z) -> (eps y -> eps z) -> eps z.
def fa_i : (i -> o) -> o.
[y] eps (fa_i y) --> x:i -> eps (y x).
P: i -> i -> o.
a : i.
b : i.
d1: eps (fa_i (x => fa_i (y => or (P a x) (or (P y b) (P y x))))).
d2: eps (fa_i (x => fa_i (y => or (not (P a x)) (not (P y b))))).
def c1 : x : i -> y : i -> (eps (P a x) -> eps bot) ->
(eps (P y b) -> eps bot) ->
(eps (P y x) -> eps bot) -> eps bot
:= x => y => l1 => l2 => l3 => z =>
d1 x y z (l1' => l1 l1' z)
(sb1 => sb1 z (l2' => l2 l2' z) (l3' => l3 l3' z)).
def c2 : x : i -> y : i -> ((eps (P a x) -> eps bot) -> eps bot) ->
((eps (P y b) -> eps bot) -> eps bot) -> eps bot
:= x => y => l1 => l2 => z =>
d2 x y z (l1' => l1 l1' z) (l2' => l2 l2' z).
def c3 : (eps (P a b) -> eps bot) -> eps bot
:= l1 => c1 b a l1 l1 l1.
def c4 : x : i -> ((eps (P a x) -> eps bot) -> eps bot) -> eps bot
:= x => l1 => c3 (tp => c2 x a l1 (tnp => tnp tp)).
def c5 : eps bot := c3 (tp => c4 b (tnp => tnp tp)).
eq : i -> i -> o.
0 : i.
S : i -> i.
def plus : i -> i -> i.
[x] plus 0 x --> x.
[x, y] plus (S x) y --> S (plus x y).
def one : i := S 0.
def two : i := S one.
d'1 : eps(eq 0 0).
d'2 : eps(fa_i (x => fa_i (y => or (eq (S x) (S y)) (not (eq x y))))).
d'3 : eps(fa_i (x => not (eq (plus x one) two))).
def c'1 : (eps(eq 0 0) -> eps bot) -> eps bot := l1 => l1 d'1.
def c'2 : x : i -> y : i -> (eps (eq (S x) (S y)) -> eps bot) ->
(eps (not (eq x y)) -> eps bot) -> eps bot
:= x => y => l1 => l2 => z => d'2 x y z (l1' => l1 l1' z)
(l2' => l2 l2' z).
def c'3 : x : i -> (eps (not (eq (plus x one) two)) -> eps bot) ->
eps bot
:= x => l1 => l1 (d'3 x).
def c'4 : y : i -> (eps (not (eq (S (plus y one)) two)) -> eps bot) ->
eps bot
:= y => l1 => c'3 (S y) l1.
def c'5 : y : i -> (eps (not (eq (plus y one) one)) -> eps bot) ->
eps bot
:= y => l1 => c'2 (plus y one) one
(tp => c'4 y (tnp => tnp tp)) l1.
def c'6 : (eps (not (eq one one)) -> eps bot) -> eps bot
:= l1 => c'5 0 l1.
def c'7 : (eps (not (eq 0 0)) -> eps bot) -> eps bot
:= l1 => c'2 0 0 (tp => c'6 (tnp => tnp tp)) l1.
def c'8 : eps bot := c'1 (tp => c'7 (tnp => tnp tp)).
#NAME part5.
o : Type.
s : Type.
imp : o -> o -> o.
def eps : o -> Type.
[x, y] eps (imp x y) --> (eps x) -> (eps y).
and: o -> o -> o.
[x, y] eps (and x y) --> z:o -> (eps x -> eps y -> eps z) -> eps z.
def top : o.
[ ] eps top --> z:o -> (eps z) -> (eps z).
def bot : o.