...
 
Commits (3)
type : Type.
def term : type -> Type.
eq : A : type -> term A -> term A -> type.
def Eq (A : type) (a : term A) (b : term A) : Type := term (eq A a b).
refl : A : type -> a : term A -> Eq A a a.
sym : A : type -> a : term A -> b : term A -> Eq A a b -> Eq A b a.
def trans : A : type -> a : term A -> b : term A -> c : term A ->
Eq A a b -> Eq A b c -> Eq A a c.
[A,a,b,h] trans A a b a h (sym A a b h) --> refl A a
[A,a,b,h] trans A b a b (sym A a b h) h --> refl A b
[A,a,b,h] trans A a b b h (refl A b) --> h
[A,a,b,h] trans A a a b (refl A a) h --> h
[A,w,x,y,z,h,h',h''] trans A w x z h (trans A x y z h' h'') -->
trans A w y z (trans A w x y h h') h''.
def bpi : X : type -> x : term X -> y : term X -> h : Eq X x y ->
P : (z : term X -> Eq X x z -> type) ->
term (P x (refl X x)) -> term (P y h).
(; The left-hand side ;)
def bpi_trans_1 (X : type) (x : term X) (y : term X) (z : term X)
(P : t : term X -> Eq X y t -> type)
(h : Eq X x y) (h' : Eq X y z)
(p : term (P x (sym X x y h))) :
term (P z h') :=
bpi X y z h' (t : term X => h' : Eq X y t => P t h')
(bpi X x y h
(t : term X => h'' : Eq X x t => P t (trans X y x t (sym X x y h) h''))
p).
(; The right-hand side ;)
def bpi_trans_2 (X : type) (x : term X) (y : term X) (z : term X)
(P : t : term X -> Eq X y t -> type)
(h : Eq X x y) (h' : Eq X y z)
(p : term (P x (sym X x y h))) : term (P z h') :=
bpi X x z (trans X x y z h h')
(t : term X => h'' : Eq X x t => P t (trans X y x t (sym X x y h) h'')) p.
(; The following rule is rejected by Dedukti with the error message
"The type could not be infered." ;)
[X,x,y,z,P,h,h',p]
bpi X y z h' P
(bpi X x y h
(t => h'' => P t (trans X y x t (sym X x y h) h''))
p)
-->
bpi X x z (trans X x y z h h')
(t => h'' => P t (trans X y x t (sym X x y h) h'')) p.
type : Type.
def term : type -> Type.
eq : A : type -> term A -> term A -> type.
def Eq (A : type) (a : term A) (b : term A) : Type := term (eq A a b).
refl : A : type -> a : term A -> Eq A a a.
sym : A : type -> a : term A -> b : term A -> Eq A a b -> Eq A b a.
def trans : A : type -> a : term A -> b : term A -> c : term A ->
Eq A a b -> Eq A b c -> Eq A a c.
[A,a,b,h] trans A a b a h (sym A a b h) --> refl A a
[A,a,b,h] trans A b a b (sym A a b h) h --> refl A b
[A,a,b,h] trans A a b b h (refl A b) --> h
[A,a,b,h] trans A a a b (refl A a) h --> h
[A,w,x,y,z,h,h',h''] trans A w x z h (trans A x y z h' h'') -->
trans A w y z (trans A w x y h h') h''.
def bpi : X : type -> x : term X -> y : term X -> h : Eq X x y ->
P : (z : term X -> Eq X x z -> type) ->
term (P x (refl X x)) -> term (P y h).
(; The left-hand side ;)
def bpi_trans_1 (X : type) (x : term X) (y : term X) (z : term X)
(P : t : term X -> Eq X y t -> type)
(h : Eq X x y) (h' : Eq X y z)
(p : term (P x (sym X x y h))) :
term (P z h') :=
bpi X y z h' (t : term X => h' : Eq X y t => P t h')
(bpi X x y h
(t : term X => h'' : Eq X x t => P t (trans X y x t (sym X x y h) h''))
p).
(; The right-hand side ;)
def bpi_trans_2 (X : type) (x : term X) (y : term X) (z : term X)
(P : t : term X -> Eq X y t -> type)
(h : Eq X x y) (h' : Eq X y z)
(p : term (P x (sym X x y h))) : term (P z h') :=
bpi X x z (trans X x y z h h')
(t : term X => h'' : Eq X x t => P t (trans X y x t (sym X x y h) h'')) p.
(; The following rule is rejected by Dedukti with the error message
"The type could not be infered." ;)
[X,x,y,z,P,h,h',p]
bpi X y z h' P
(bpi X x y h
(t => h'' => P t (trans X y x t (sym X x y h) h''))
p)
-->
bpi X x z (trans X x y z h h')
(t => h'' => P t (trans X y x t (sym X x y h) h'')) p.
#NAME essai.
A : Type.
B : Type.
C : ((A -> B) -> B) -> A.
def e : A -> B.
[f] e (C f) --> f e.
\ No newline at end of file
......@@ -15,7 +15,7 @@ def D : fun -> fun.
[] D id --> 1.
[] D 0 --> 0.
[] D 1 --> 1.
[] D 1 --> 0.
[x,y] D (plus x y) --> plus (D x) (D y).
[x,y] D (mult x y) --> plus (mult y (D x)) (mult x (D y)).
[x,y] D (minus x y) --> minus (D x) (D y).
......
Prop : Type.
def not : Prop -> Prop.
def and : Prop -> Prop -> Prop.
or : Prop -> Prop.
[x] not (not x) --> x.
[x,y] not (or x y) --> and (not x) (not y).
[x,y] not (and x y) --> or (not x) (not y).
[x,y,z] and x (or y z) --> or (and x y) (and x z).
[x,y,z] and (or y z) x --> or (and x y) (and x z).
......@@ -6,7 +6,8 @@ def minus : Nat -> Nat -> Nat.
[x] minus x 0 --> x.
[x,y] minus (S x) (S y) --> minus x y.
(; Caution, this division is the upper integer part which is not the usual one;)
(; Caution, this division is the upper integer part which is not the usual one
(if we make minus total);)
def div : Nat -> Nat -> Nat.
[y] div 0 (S y) --> 0.
[x,y] div (S x) (S y) --> S (div (minus x y) (S y)).
......
......@@ -12,21 +12,30 @@ False : Bool.
Nil : List 0.
Cons : (n: Nat) -> A -> List n -> List (S n).
def taut : A -> Bool.
[] taut _ --> True.
(;
def ifthensucc : Bool -> Nat -> Nat.
[n] ifthensucc True n --> S n.
[n] ifthensucc False n --> n.
(; ;)
def compute_length : (A -> Bool) -> (n: Nat) -> List n -> Nat.
def aux_length : Bool -> (A -> Bool) -> (n: Nat) -> List n -> Nat.
[] compute_length _ _ Nil --> 0.
[f,n,x,l] compute_length f _ (Cons n x l) --> aux_length (f x) f n l.
[n,l] compute_length taut n l --> n.
[f,n,l] aux_length True f n l --> S (compute_length f n l).
[f,n,l] aux_length False f n l --> compute_length f n l.
def filter : f: (A -> Bool) -> (n: Nat) -> l: List n -> List (compute_length f n l).
def bis : b: Bool -> f: (A -> Bool) -> x: A -> (n: Nat) -> l: List n -> List (aux_length b f n l).
[] filter _ _ Nil --> Nil.
[f,n,x,l] filter f _ (Cons n x l) --> bis (f x) f x n l.
[l] filter taut _ l --> l.
[f,n,x,l] bis True f x n l --> Cons (compute_length f n l) x (filter f n l).
[f,x,n,l] bis False f x n l --> filter f n l.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def plus : Nat -> Nat -> Nat.
[y] plus 0 y --> y.
[x,y] plus (S x) y --> S (plus x y).
def 1 := S 0.
def 2 := S 1.
def 3 := S 2.
def 5 := plus 2 3.
def T : Nat -> Type.
[] T 0 --> Nat.
[k] T (S k) --> (n : Nat) -> T n.
def f : (n : Nat) -> T n.
[] f 0 --> 0.
[k] f (S k) 0 --> S k.
[k,l] f (S k) (S l) --> f (plus (S k) (S l)).
#EVAL f 3 1 5 0.
\ No newline at end of file
......@@ -263,5 +263,5 @@ def 0_right_neutral : n : Nat ->
[] 0_right_neutral 0 --> tt
[n] 0_right_neutral (S n) --> 0_right_neutral n.
#CHECK factorielle 14 == mult 95 95. (; Answer is of course NO ;)
#CHECKNOT factorielle 14 == mult 95 95. (; Answer is of course YES ;)
#NAME tuto.
(; Les Types ;)
Nat : Type.
Bool : Type.
NatList : Type.
(; Constructeurs ;)
0 : Nat.
S : Nat -> Nat.
True : Bool.
False : Bool.
Vide : NatList.
Cons : Nat -> NatList -> NatList.
(; Plein de fonctions ;)
def pred : Nat -> Nat.
[n] pred (S n) --> n.
def plus : Nat -> Nat -> Nat.
[n] plus 0 n --> n
[m, n] plus (S m) n --> S (plus m n).
def plus_rec_term : Nat -> Nat -> Nat.
[n] plus_rec_term 0 n --> n
[m, n] plus_rec_term (S m) n --> plus_rec_term m (S n).
def mult : Nat -> Nat -> Nat.
[] mult 0 _ --> 0
[m, n] mult (S m) n --> plus n (mult m n).
def not : Bool -> Bool.
[] not True --> False.
[] not False --> True.
def even : Nat -> Bool.
[] even 0 --> True.
[n] even (S n) --> not (even n).
def leq : Nat -> Nat -> Bool.
[] leq 0 _ --> True
[m] leq (S m) 0 --> False
[m, n] leq (S m) (S n) --> leq m n.
def moitie : Nat -> Nat.
[] moitie 0 --> 0
[n] moitie (S (S n)) --> S (moitie n).
def double_add : Nat -> Nat.
[n] double_add n --> plus n n.
def double_mult : Nat -> Nat.
[n] double_mult n --> mult (S (S 0)) n.
def double_constr : Nat -> Nat.
[] double_constr 0 --> 0
[n] double_constr (S n) --> S (S (double_constr n)).
def Ackermann : Nat -> Nat -> Nat.
[n] Ackermann 0 n --> S n
[m] Ackermann (S m) 0 --> Ackermann m (S 0)
[m, n] Ackermann (S m) (S n) --> Ackermann m (Ackermann (S m) n).
def hd : NatList -> Nat.
[n] hd (Cons n _) --> n.
def tl : NatList -> NatList.
[l] tl (Cons _ l) --> l.
def append : NatList -> NatList -> NatList.
[l] append Vide l --> l
[n,l1,l2] append (Cons n l1) l2 --> Cons n (append l1 l2).
def length : NatList -> Nat.
[] length Vide --> 0
[l] length (Cons _ l) --> S (length l).
[x,y,z] plus x (plus y z) --> plus (plus x y) z.
\ No newline at end of file
#NAME test.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def plus : Nat -> Nat -> Nat.
[n] plus 0 n --> n
[m, n] plus (S m) n --> S (plus m n).
def mult : Nat -> Nat -> Nat.
[] mult 0 _ --> 0
[m, n] mult (S m) n --> plus n (mult m n).
def double : Nat -> Nat := mult (S (S 0)).
def ddouble : Nat -> Nat.
[] ddouble --> mult (S (S 0)).
def plus1 : Nat -> Nat.
[n] plus1 n --> S n.
def moitie : Nat -> Nat.
[] moitie 0 --> 0.
[n] moitie (S (S n)) --> moitie (S n)
[] moitie (S 0) --> 0.
#put the path of your dkcheck binary
DKCHECK ?= dkcheck
#put the path of your dkdep binary
DKDEP ?= dkdep
DKOPTIONS = -nl -errors-in-snf
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
.PHONY: all clean
all: $(DKOS)
%.dko: %.dk .depend
@echo "FILE: $<"
#time --format "TIME: %U" --output /dev/stdout $(DKCHECK) $(DKOPTIONS) -e $<
$(DKCHECK) $(DKOPTIONS) -e $<
# standard .depend file generation
.depend: $(DKS)
@echo "Producing .depend"
@$(DKDEP) $^ -o $@
clean:
@rm -f *.dko .depend tmp.dk
ifneq ($(MAKECMDGOALS), clean)
-include .depend
endif
This diff is collapsed.
This diff is collapsed.
#NAME russel_paradox.
(; An expression of Russell Paradox.
This uses three inductive types: Leibnitz equality, Sigma types and
sets represented as trees with arbitrary branching (indexed by a type).
Based on https://people.cs.kuleuven.be/~bart.jacobs/coq-essence.pdf, but with
a simpler definition of sets. ;)
(; usual encoding of polymorphism ;)
type : Type.
def term : type -> Type.
(; We do not need Type : Type here, just the ability to define the
inductive type for Set in an impredicative way. ;)
(; Remark: we do not need universal quantification ;)
false : Type.
Not : type -> type.
[A] term (Not A) --> term A -> false.
(; Equality ;)
Eq : A : type -> term A -> term A -> type.
eq : A : type -> term A -> term A -> Type.
[A,a,b] term (Eq A a b) --> eq A a b.
refl : A : type -> a : term A -> eq A a a.
(; To eliminate equalities, we need only Leibnitz's principle. ;)
def leibnitz : A : type -> a : term A -> b : term A -> eq A a b ->
P : (term A -> type) -> term (P a) -> term (P b).
(; This rewrite rule is not needed for deriving the Paradox but only to make the final term of type false diverge. ;)
[A,a,P,H] leibnitz _ _ _ (refl A a) P H --> H.
(; Sigma types ;)
Ex : A : type -> (term A -> type) -> type.
ex : A : type -> (term A -> type) -> Type.
[A,B] term (Ex A B) --> ex A B.
pair : A : type -> B : (term A -> type) -> a : term A -> term (B a) -> ex A B.
def fst : A : type -> B : (term A -> type) -> ex A B -> term A.
def snd : A : type -> B : (term A -> type) -> e : ex A B -> term (B (fst A B e)).
[a] fst _ _ (pair _ _ a _) --> a.
[b] snd _ _ (pair _ _ _ b) --> b.
(; Sets ;)
(; A set is an arbitrary-branching tree. We write "C" the constructor for sets. ;)
Set : type.
set : Type.
[] term Set --> set.
C : A : type -> (term A -> set) -> set.
(; We do not need a full elimination principle for sets, it is enough
to define membership in the case of sets constructed with C. ;)
def In : set -> set -> type.
[x,A,f] In x (C A f) --> Ex A (a => Eq Set (f a) x).
(; From now on, we have only definitions and we culminate with one
inhabiting false. ;)
def in (A : set) (B : set) := term (In A B).
def NotIn (A : set) (B : set) := Not (In A B).
def Notinself (A : set) := NotIn A A.
(; Notinselfs is the type of all sets satisifying Notinself ;)
def Notinselfs := Ex Set Notinself.
(; Russell set, Coq rejects this definition due to an universe inconsistency. ;)
def R : set := C Notinselfs (fst Set Notinself).
def eqR (a : term Notinselfs) := Eq Set (fst Set Notinself a) R.
def r1 (H : in R R) : false :=
(; By definition of "In",
H : ex Notinselfs eqR
snd Notinselfs eqR H : eqR (fst Notinselfs eqR H)
== Eq Set (fst Set Notinself (fst Notinselfs eqR H)) R
snd Set Notinself (fst Notinselfs eqR H) : Notinself (fst Set Notinself (fst Notinselfs eqR H)
so by the Leibnitz property, H2 : Notinself R
hence H2 H : false.
;)
leibnitz Set (fst Set Notinself (fst Notinselfs eqR H)) R (snd Notinselfs eqR H) Notinself (snd Set Notinself (fst Notinselfs eqR H)) H.
def r2 : in R R :=
pair Notinselfs eqR (pair Set Notinself R r1) (refl Set R).
def r3 : false := r1 r2.
#NAME bug.
type : Type.
def term : type -> Type.
......@@ -15,12 +13,12 @@ B : type.
def e : f : (term A -> term B) ->
(x : term A -> term (E B (f x))) ->
term (E (arr A B) f).
[f] e f (x => r B (f x)) --> r (arr A B) f.
[f] e (x => f x) (x => r B (f x)) --> r (arr A B) f.
f : term (arr A B).
#EVAL e f (x : term A => r B (f x)).
#EVAL e (x => f x) (x : term A => r B (f x)).
#ASSERT (f : term (arr A B) => e (x => f x) (x : term A => r B (f x))) ==
#CHECK (f : term (arr A B) => e (x => f x) (x : term A => r B (f x))) ==
(f : term (arr A B) => r (arr A B) f).
\ No newline at end of file
......@@ -6,7 +6,7 @@ S : nat -> nat.
def A : (nat -> nat) -> (nat -> nat) -> nat -> nat.
[f] A f (x => f x) --> f.
[f] A f f --> f.
#EVAL A (x : nat => 0) (x : nat => 0).
......
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def T : Nat-> Type.
[] T 0 --> Nat.
[x] T (S x) --> T x -> Nat.
def f : x : Nat -> T x -> Nat.
[x,y] f x (z => y z) --> 0.