Commit 4a14869a authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

New files

parent d5870427
#NAME FO.
Term : Type.
Prop : Type.
def prf : Prop -> Type.
true : Prop.
false: Prop.
not : Prop -> Prop.
and : Prop -> Prop -> Prop.
or : Prop -> Prop -> Prop.
imp : Prop -> Prop -> Prop.
forall: (Term -> Prop) -> Prop.
exists: (Term -> Prop) -> Prop.
equals: Term -> Term -> Prop.
def equiv: Prop -> Prop -> Prop := A:Prop => B:Prop => and (imp A B) (imp B A).
tt: prf true.
[] prf false --> P:Prop -> prf P
[A] prf (not A) --> prf A -> prf false
[A,B] prf (and A B) --> P:Prop -> (prf A -> prf B -> prf P) -> prf P
[A,B] prf (or A B) --> P:Prop -> (prf A -> prf P) -> (prf B -> prf P) -> prf P
[A,B] prf (imp A B) --> prf A -> prf B
[A] prf (forall A) --> x:Term -> prf (A x)
[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 ;)
def imp_elim : A:Prop -> B:Prop -> prf (imp A B) -> prf A -> prf B
:= A:Prop => B:Prop => p:prf (imp A B) => p.
def imp_intro : A:Prop -> B:Prop -> (prf A -> prf B) -> prf (imp A B)
:= A:Prop => B:Prop => p:(prf A -> prf B) => p.
(; disjunction ;)
def or_intro_1 : A:Prop -> B:Prop -> prf A -> prf (or A B)
:= A:Prop => B:Prop => p:prf A =>
P:Prop => f:(prf A -> prf P) => g:(prf B -> prf P) => f p.
def or_intro_2 : A:Prop -> B:Prop -> prf B -> prf (or A B)
:= A:Prop => B:Prop => p:prf B =>
P:Prop => f:(prf A -> prf P) => g:(prf B -> prf P) => g p.
def or_elim : A:Prop -> B:Prop -> prf (or A B) -> C:Prop -> prf (imp A C) -> prf (imp B C) -> prf C
:= A:Prop => B:Prop => p:prf (or A B) => p.
(; conjunction ;)
def and_intro : A:Prop -> B:Prop -> prf A -> prf B -> prf (and A B)
:= A:Prop => B:Prop => a:prf A => b:prf B => P:Prop => f:(prf A -> prf B -> prf P) => f a b.
def and_elim_1 : A:Prop -> B:Prop -> prf (and A B) -> prf A
:= A:Prop => B:Prop => p:prf (and A B) => p A (a:prf A => b:prf B => a).
def and_elim_2 : A:Prop -> B:Prop -> prf (and A B) -> prf B
:= A:Prop => B:Prop => p:prf (and A B) => p B (a:prf A => b:prf B => b).
(; Universal quantificator ;)
def forall_intro: P:(Term->Prop) -> (t:Term -> prf (P t)) -> prf (forall P)
:= P:(Term->Prop) => p:(t:Term -> prf (P t)) => p.
def forall_elim: P:(Term->Prop) -> t:Term -> p:prf (forall P) -> prf (P t)
:= P:(Term->Prop) => t:Term => p:prf (forall P) => p t.
(; Existential quantificator ;)
def exists_intro: P:(Term->Prop) -> t:Term -> prf (P t) -> prf (exists P)
:= P:(Term -> Prop) => t:Term => p:prf (P t) =>
A:Prop => f:(x:Term -> prf (P x) -> prf A) => f t p.
def exists_elim: P:(Term->Prop) -> Q:Prop -> prf (exists P) -> prf (forall (x => imp (P x) Q)) -> prf Q
:= P:(Term->Prop) => Q:Prop => p1:prf (exists P) => p2:prf (forall (x => imp (P x) Q))
=> p1 Q p2.
(; Equality ;)
def eq_refl: prf (forall (x:Term => equals x x))
:= x:Term => P:(Term -> Prop) => p:prf (P x) => p.
def eq_sym: prf( forall (x:Term => forall (y:Term => (imp (equals x y) (equals y x)))) )
:= x:Term => y:Term => p:prf (equals x y) => p (z:Term => equals z x) (eq_refl x).
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).
#NAME NumberBases.
Figure : Type.
0 : Figure.
1 : Figure.
2 : Figure.
3 : Figure.
4 : Figure.
5 : Figure.
6 : Figure.
7 : Figure.
8 : Figure.
9 : Figure.
A : Figure.
B : Figure.
C : Figure.
D : Figure.
E : Figure.
F : Figure.
Number : Type.
Zero : Number.
Cons : Number -> Figure -> Number.
def decimal : Tuto.Nat -> Number.
def decimal_aux : Tuto.Nat -> Number -> Number.
[n] decimal n --> decimal_aux n Zero.
[N] decimal_aux Tuto.0 N --> N.
[n] decimal_aux (Tuto.S n) Zero --> decimal_aux n (Cons Zero 1).
[n,N] decimal_aux (Tuto.S n) (Cons N 0) --> decimal_aux n (Cons N 1).
[n,N] decimal_aux (Tuto.S n) (Cons N 1) --> decimal_aux n (Cons N 2).
[n,N] decimal_aux (Tuto.S n) (Cons N 2) --> decimal_aux n (Cons N 3).
[n,N] decimal_aux (Tuto.S n) (Cons N 3) --> decimal_aux n (Cons N 4).
[n,N] decimal_aux (Tuto.S n) (Cons N 4) --> decimal_aux n (Cons N 5).
[n,N] decimal_aux (Tuto.S n) (Cons N 5) --> decimal_aux n (Cons N 6).
[n,N] decimal_aux (Tuto.S n) (Cons N 6) --> decimal_aux n (Cons N 7).
[n,N] decimal_aux (Tuto.S n) (Cons N 7) --> decimal_aux n (Cons N 8).
[n,N] decimal_aux (Tuto.S n) (Cons N 8) --> decimal_aux n (Cons N 9).
[n,N] decimal_aux (Tuto.S n) (Cons N 9) --> decimal_aux n (Cons (decimal_aux (Tuto.S Tuto.0) N) 0).
def binary : Tuto.Nat -> Number.
def binary_aux : Tuto.Nat -> Number -> Number.
[n] binary n --> binary_aux n Zero.
[N] binary_aux Tuto.0 N --> N.
[n] binary_aux (Tuto.S n) Zero --> binary_aux n (Cons Zero 1).
[n,N] binary_aux (Tuto.S n) (Cons N 0) --> binary_aux n (Cons N 1).
[n,N] binary_aux (Tuto.S n) (Cons N 1) --> binary_aux n (Cons (decimal_aux (Tuto.S Tuto.0) N) 0).
def hexadecimal : Tuto.Nat -> Number.
def hexadecimal_aux : Tuto.Nat -> Number -> Number.
[n] hexadecimal n --> hexadecimal_aux n Zero.
[N] hexadecimal_aux Tuto.0 N --> N.
[n] hexadecimal_aux (Tuto.S n) Zero --> hexadecimal_aux n (Cons Zero 1).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 0) --> hexadecimal_aux n (Cons N 1).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 1) --> hexadecimal_aux n (Cons N 2).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 2) --> hexadecimal_aux n (Cons N 3).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 3) --> hexadecimal_aux n (Cons N 4).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 4) --> hexadecimal_aux n (Cons N 5).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 5) --> hexadecimal_aux n (Cons N 6).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 6) --> hexadecimal_aux n (Cons N 7).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 7) --> hexadecimal_aux n (Cons N 8).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 8) --> hexadecimal_aux n (Cons N 9).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 9) --> hexadecimal_aux n (Cons N A).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N A) --> hexadecimal_aux n (Cons N B).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N B) --> hexadecimal_aux n (Cons N C).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N C) --> hexadecimal_aux n (Cons N D).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N D) --> hexadecimal_aux n (Cons N E).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N E) --> hexadecimal_aux n (Cons N F).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N F) --> hexadecimal_aux n (Cons (hexadecimal_aux (Tuto.S Tuto.0) N) 0).
#NAME simple.
#NAME Tuto.
(; Les Types ;)
......
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