Commit 7eb85198 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Départ en vacances

parent 8d1ea65b
......@@ -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
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.
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