KO/ExplRaphIllTyped.dk

+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.

KO/nonMillerPattern.dk

+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.

Miscellaneous/CallCC.dk

+#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

Miscellaneous/Dershowitz33/Expl11.dk

@@ -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).

Miscellaneous/Dershowitz33/Expl12.dk

+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).

Miscellaneous/IntegerDivision.dk

@@ -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)).

Miscellaneous/filter.dk

@@ -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.

Miscellaneous/productProperty.dk

+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

Miscellaneous/tuto.dk

@@ -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 ;)
 

Miscellaneous/tuto_inde.dk

+#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

Miscellaneous/unaireDouble.dk

+#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.

Paradoxes/Makefile

-#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

Paradoxes/russel_paradox.dk

-#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.

ToStudy/bugRaphael.dk

-#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

ToStudy/explFrc.dk

@@ -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).
 

ToStudy/explFrc2.dk

+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.