Commit d5870427 authored by Gaspard FEREY's avatar Gaspard FEREY

Reorganized Misc folder.

parent eafcab14
#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 need not have the same name that the corresponding Dedukti
......@@ -6,13 +13,10 @@ DKS=$(wildcard *.dk)
# character.
DKOS=$(shell cut -d ':' -f 1 .depend)
DKDEP=dkdep
DKCHECK=dkcheck
all: $(DKOS)
%.dko:
$(DKCHECK) -e -nl $<
$(DKCHECK) -e $(DKOPTIONS) $<
clean:
rm -f *.dko .depend
......
#NAME append.
A : Type.
Nat: Type.
Z : Nat.
S : Nat -> Nat.
def plus: Nat -> Nat -> Nat.
[m] plus Z m --> m
[n,m] plus (S n) m --> S (plus n m).
Listn : Nat -> Type.
nil : Listn Z.
cons : n : Nat -> A -> Listn n -> Listn (S n).
def append: n : Nat -> Listn n -> m : Nat -> Listn m -> Listn (plus n m).
[l2] append _ nil _ l2 --> l2
[n,l1,m,l2,a]
append _ (cons n a l1) m l2 --> cons (plus n m) a (append n l1 m l2).
......@@ -29,6 +29,8 @@ tt: prf true.
[A] prf (exists A) --> P:Prop -> (x:Term -> prf (A x) -> prf P) -> prf P
[x,y] prf (equals x y) --> P:(Term -> Prop) -> prf (P x) -> prf (P y).
lem: A:Prop -> prf (or A (not A)).
(; *** Theorems ;)
(; implication ;)
......@@ -88,13 +90,3 @@ def eq_sym: prf( forall (x:Term => forall (y:Term => (imp (equals x y) (equals y
def eq_trans: prf ( forall (x:Term => forall (y:Term => (forall (z:Term => imp (and (equals x y) (equals y z)) (equals x z))))) )
:= x:Term => y:Term => z:Term => p:prf (and (equals x y) (equals y z)) => P:(Term -> Prop) => q:prf (P x) =>
and_elim_2 (equals x y) (equals y z) p P (and_elim_1 (equals x y) (equals y z) p P q).
(; *** Classical logic ;)
lem: A:Prop -> prf (or A (not A)).
def double_neg_elim : A:Prop -> prf (not (not A)) -> prf A
:= A:Prop => p:prf (not (not A)) => or_elim A (not A) (lem A) A (imp_intro A A (a:prf A => a)) (imp_intro (not A) A (q:prf (not A) => (imp_elim (not A) false p q) A)).
def Pierce_law : A:Prop -> B:Prop -> prf (imp (imp (imp A B) A) A)
:= A:Prop => B:Prop => (p:prf (imp (imp A B) A) => or_elim A (not A) (lem A) A (imp_intro A A (a:prf A => a)) (imp_intro (not A) A (q:prf (not A) => p (imp_intro A B (a:prf A =>(q a) B))))).
#NAME stlc.
type:Type.
o:type.
arrow: type -> type -> type.
term:type -> Type.
def App: a:type -> b:type -> term (arrow a b) -> term a -> term b.
Lam: a:type -> b:type -> (term a -> term b) -> term (arrow a b).
[f,arg] App _ _ (Lam _ _ (x => f x)) arg --> f arg.
c:term o.
#STEP App o o (Lam o o (x=> x)) c.
#NAME Church.
type : Type.
arr : type -> type -> type.
def e : type -> Type.
[a : type, b : type] e (arr a b) --> e a -> e b.
def numeral : Type := A : type -> (e A -> e A) -> (e A -> e A).
def zero : numeral := A : type => f : (e A -> e A) => x : e A => x.
def one : numeral := A : type => f : (e A -> e A) => x : e A => f x.
def two : numeral := A : type => f : (e A -> e A) => x : e A => f (f x).
def three : numeral := A : type => f : (e A -> e A) => x : e A => f (f (f x)).
def four : numeral := A : type => f : (e A -> e A) => x : e A => f (f (f (f x))).
def plus : numeral -> numeral -> numeral :=
m : numeral => n : numeral => A : type => f : (e A -> e A) => x : e A => m A f (n A f x).
def times : numeral -> numeral -> numeral :=
m : numeral => n : numeral => A : type => f : (e A -> e A) => x : e A => m A (n A f) x.
def power : numeral -> numeral -> numeral :=
m : numeral => n : numeral => A : type => n (arr A A) (m A).
def test : numeral := power two (plus one (times three four)).
def test_ : numeral := power two (plus (times four four) one).
P : numeral -> Type.
P2: n:numeral -> P n -> Type.
y : P test_.
z: P2 test y.
#NORMALIZE zero.
#NORMALIZE one.
#NORMALIZE two.
#NORMALIZE three.
#NORMALIZE four.
#NORMALIZE plus one (times three four).
#NAME def.
A:Type.
P:A->Type.
def magic (a1:A) (a2:A) (H:P a1) : P a2 := H.
#NAME pouet.
karaté:Type.
#NAME NonInjectivity.
Nat : Type.
Vect : Nat -> Type.
def non_inject : Nat -> Nat.
Cons : n : Nat -> Vect n -> Vect (non_inject n).
def Tail : n : Nat -> Vect (non_inject n) -> Vect n.
[n, l] Tail n (Cons _ l) --> l.
#NAME pouet.
id:Type
#NAME var.
A:Type.
a:A.
[x:A] x --> a.
#NAME scope.
id:toto.tata.
#NAME abs.
A:Type.
y:A.
P:A->Type.
p:P y.
id: x:A -> P x -> P x.
def T: P y.
(; [ ] T --> (z => id z p) y. ;)
[ ] T --> (z:A => id z p) y.
#NAME omega.
A : Type.
B : A -> Type.
C : B ( (x => x x)(x => x x) ).
#NAME pi.
T:Type.
x:T.
f:x->Type.
#NAME sort.
nat : Type.
x : nat.
y : x.
#NAME FOL.
Prop : Type.
prf : Prop -> Type.
True : Prop.
True_intro : prf True.
False : Prop.
False_elim : A:Prop -> prf False -> prf A.
and : Prop -> Prop -> Prop.
and_intro : A:Prop -> B:Prop -> prf A -> prf B -> prf (and A B).
and_elim1 : A:Prop -> B:Prop -> prf (and A B) -> prf A.
and_elim2 : A:Prop -> B:Prop -> prf (and A B) -> prf B.
imp : Prop -> Prop -> Prop.
imp_elim : A:Prop -> B:Prop -> prf (imp A B) -> prf A -> prf B.
imp_intro : A:Prop -> B:Prop -> (prf A -> prf B) -> prf (imp A B).
or : Prop -> Prop -> Prop.
or_elim : A:Prop -> B:Prop -> C:Prop -> prf (or A B) -> prf (imp A C) -> prf (imp B C) -> prf C.
or_intro1 : A:Prop -> B:Prop -> prf A -> prf (or A B).
or_intro2 : A:Prop -> B:Prop -> prf B -> prf (or A B).
def not : Prop -> Prop := p:Prop => imp p False.
def equiv : Prop -> Prop -> Prop := A:Prop => B:Prop => and (imp A B) (imp B A).
(; De Morgan Laws ;)
def DeMorgan1 : A:Prop -> B:Prop -> prf (imp (and A B) (not (or (not A) (not B)))) :=
A:Prop => B:Prop =>
imp_intro (and A B) (not (or (not A) (not B)))
( A_and_B :(prf (and A B)) => imp_intro (or (not A) (not B)) False (
( not_A_or_not_B:(prf (or (not A) (not B))) =>
or_elim (not A) (not B) False not_A_or_not_B
(imp_intro (not A) False (not_A:(prf (not A)) => imp_elim A False not_A (and_elim1 A B A_and_B) ) )
(imp_intro (not B) False (not_B:(prf (not B)) => imp_elim B False not_B (and_elim2 A B A_and_B) ) )
) ) ).
DeMorgan2 : A:Prop -> B:Prop -> prf (imp (or A B) (not (and (not A) (not B)))). (; TODO ;)
(; Quantifiers ;)
U:Type.
forall : (U->Prop) -> Prop.
forall_intro : P:(U->Prop) -> (x:U -> prf (P x)) -> prf (forall P).
forall_elim : P:(U->Prop) -> prf (forall P) -> x:U -> prf (P x).
#NAME rule_name.
nat : Type.
0 : nat.
def plus : nat -> nat -> nat.
{rule_name.plus_0_n} [n] plus 0 n --> n.
\ No newline at end of file
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