Commit 962629f4 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Initialization

parents
*~
\#*\#
#NAME test.
nat : Type.
0 : nat.
S : nat -> nat.
def 1 := S 0.
def 2 := S 1.
def 3 := S 2.
def 4 := S 3.
def 5 := S 4.
defac mset [nat].
#CONV mset 1 0, mset 0 1.
#CONV mset 0 1, mset 1 0.
#CONV mset 1 0, mset 0 0.
#WHNF mset (mset 2 0) (mset 1 ( (x : nat => mset x (mset (S x) x)) 4)).
#SNF mset (mset 2 0) (mset 1 ( (x : nat => mset x (mset (S x) x)) 4)).
#CONV mset (mset 3 4) (mset 0 1), mset (mset (mset 1 4) 0) 3.
defac min [nat].
[] min 0 --> (x : nat => 0)
[x] min 0 x --> 0
[x,y] min (S x) (S y) --> S (min x y).
#GDT min.
#SNF min (S (S 0)) (min 0 (S 0)).
#PRINT "".
#PRINT "----------- plus ------------".
defacu plus [nat,0].
[x,y] plus (S x) y --> S (plus x y).
#GDT plus.
#SNF plus (plus 2 0) (plus 1 ( (x : nat => plus x (plus (S x) x)) 4)).
#PRINT "".
#PRINT "----------- time ------------".
defacu time [nat,S 0].
[] time 0 _ --> 0.
[x,y] time (S x) y --> plus y (time x y).
#GDT time.
#WHNF time 1 2.
#SNF time 1 2.
#SNF time 5 5.
#PRINT "----------- square ------------".
def square := (x : nat => time x x).
#CONV plus (square 3) (square 4), square 5.
#PRINT "----------- tricky ------------".
defac tricky [nat].
[x,y,z] tricky (tricky x z) (tricky y x) --> 0.
#GDT tricky.
#SNF tricky (tricky 1 (tricky 2 3)) (tricky 5 1).
#SNF tricky (tricky 1 (tricky 2 1)) (tricky 5 2).
#SNF tricky (tricky 1 (tricky 2 3)) (tricky 5 4).
#PRINT "------------ vector -------------".
Vect : nat -> Type.
def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
[n1,n2,n3,l1,l2,l3] concat (plus n1 n2) (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3).
[l] concat 0 _ _ l --> l.
\ No newline at end of file
File added
#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 pouet.
id:Type
#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
#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 MillerPatternWithLambda.
A : Type.
f : A -> A -> A.
def g : (A -> A) -> A.
def h : (A -> A) -> A.
a : A.
[]
h (x => g (y => f x y))
-->
a.
[]
g (x => g (y => f x y))
-->
a.
#CONV g (x => g (y => f x y)), a.
#CONV h (x => g (y => f x y)), a.
#NAME dot.
N: Type.
Z: N.
S: N->N.
def plus: N->N->N.
[y] plus Z y --> y
[x,y] plus (S x) y --> S (plus x y).
V: N->Type.
Nil: V Z.
Con: n:N -> V n -> N -> V (S n).
def hd: n:N -> V (S n) -> N.
[m] hd _ (Con _ _ m) --> m.
def app: n:N -> m:N -> V n -> V m -> V (plus n m).
[y] app _ _ Nil y --> y
[n,m,x,y,k] app _ m (Con n x k) y --> Con (plus n m) (app n m x y) k.
#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 Prop.
Prop: Type.
def prf : Prop -> Type.
Term: Type.
(; *** Declarations ;)
true : Prop.
false : Prop.
imp : Prop -> Prop -> Prop.
forall: (Term -> Prop) -> Prop.
(; *** Definitions ;)
def not : Prop -> Prop := A:Prop => imp A false.
def or : Prop -> Prop -> Prop := A:Prop => B:Prop => imp (not A) B.
def and : Prop -> Prop -> Prop := A:Prop => B:Prop => not (imp A (not B)).
def exists: (Term -> Prop) -> Prop := P:(Term -> Prop) => not (forall (t:Term => not (P t))).
(; *** Axioms ;)
true_intro : prf true.
false_elim : A:Prop -> prf false -> prf A.
[A,B] prf (imp A B) --> prf A -> prf B.
[P] prf (forall P) --> t:Term -> prf (P t).
lem: A:Prop -> B:Prop -> prf (imp A B) -> prf (imp (not A) B) -> prf B.
(; *** 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 => q:prf (not A) => false_elim B (q p).
def or_intro_2 : A:Prop -> B:Prop -> prf B -> prf (or A B)
:= A:Prop => B:Prop => p:prf B => q:prf (not A) => p.
def or_elim : A:Prop -> B:Prop -> C:Prop -> prf (imp A C) -> prf (imp B C) -> prf (or A B) -> prf C
:= A:Prop => B:Prop => C:Prop => p1:prf (imp A C) => p2:prf (imp B C) => q:prf (or A B) =>
lem A C p1 (x:prf (not A) => p2 (q x)).
(; 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:prf (imp A (not B)) => p 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) =>
lem A A (q:prf A => q) (q:prf (not A) => false_elim A (p (x:prf A => false_elim (not B) (q x)))).
def and_elim_2 : A:Prop -> B:Prop -> prf (and A B) -> prf B
:= A:Prop => B:Prop => p:prf (and A B) =>
lem B B (q:prf B => q) (q:prf (not B) => false_elim B (p (x:prf A => q))).
(; 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) => q:prf (forall (u:Term => not (P u))) => q t p.
e: (Term -> Prop) -> Term. (;Hilbert operator;)
exists_elim: P:(Term->Prop) -> prf (exists P) -> prf (P (e P)).
#NAME zen.
A : Type.
def e0 : A -> A.
i1 : (A -> A) -> A.
def e1 : A -> A -> A.
i2 : (A -> A) -> A.
def e2 : A -> A -> A.
def e3 : A -> A.
[a] e0 (e1 _ a) --> a.
[a,b] e1 (i1 a) b --> a b.
[a,b] e2 (e0 a) b --> e0 a
[a,b] e2 (i2 a) b --> a b.
[b] e3 (i1 (a => e1 a b)) --> b.
b : A.
def f (x : A -> A -> A) := i2 (a => e3 (i1 (x a))).
def pr1 (a : A) (c : A) :=
e1
(i1
(g =>
e1
g
(i2
(__ =>
e0
(e1
(i1
(d =>
e1 g
(i2 (__ => d)))) b)))))
(i1
(e => e1 c (e2 e a))).
(; pr2 is the normal form of pr1. ;)
def pr2 (__ : A) (c : A) := e1 c b.
#CONV pr1, pr2. (; Answer must be YES ;)
#CONV f pr1, f pr2. (; Answer must be YES ;)
#NAME bug.
A : Type.
def F : (A -> A) -> A -> A.
a : A.
[f] F (x => f x) _ --> a.
g : A -> A.
def test (b : A) := F (x => g x) b.
#SNF test.
#CONV test, b : A => a. (; Answer must be YES ;)
#NAME rule_name.
nat : Type.
0 : nat.
def plus : nat -> nat -> nat.
{plus_0_n} [n] plus 0 n --> n.
#NAME subst.
A : Type.
x : A.
t : (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => (x : A => A) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x.
#NAME test.
Term : Type.
Prop: Type.
def prf: Prop -> Type.
anyterm: Term.
not: Prop -> Prop.
def notc: Prop -> Prop :=
A:Prop => not (not (not (not (not A)))).
True: Prop.
def Truec: Prop := not (not (True)).
False: Prop.
def Falsec: Prop := not (not (False)).
and: Prop -> Prop -> Prop.
def andc: Prop -> Prop -> Prop :=
A:Prop => B:Prop => not (not (and (not (not A)) (not (not B)))).
or: Prop -> Prop -> Prop.
def orc: Prop -> Prop -> Prop :=
A:Prop => B:Prop => not (not (or (not (not A)) (not (not B)))).
imply: Prop -> Prop -> Prop.
def implyc: Prop -> Prop -> Prop :=
A:Prop => B:Prop => not (not (imply (not (not A)) (not (not B)))).
forall: (Term -> Prop) -> Prop.
def forallc: (Term -> Prop) -> Prop :=
P:(Term -> Prop) =>
not (not (forall (x:Term => not (not (P x))))).
exists: (Term -> Prop) -> Prop.
def existsc: (Term -> Prop) -> Prop :=
P:(Term -> Prop) =>
not (not (exists (x:Term => not (not (P x))))).
equal: Term -> Term -> Prop.
def equalc: Term -> Term -> Prop :=
a:Term => b:Term => not (not (equal a b)).
def equiv: Prop -> Prop -> Prop :=
A:Prop => B:Prop => and (imply A B) (imply B A).
[] prf True --> P:Prop -> (prf P -> prf P)
[] prf False --> P:Prop -> prf P
[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 (imply A B) --> prf A -> prf B
[A] prf (not A) --> prf A -> prf False
[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 (equal x y) --> P:(Term -> Prop) -> prf (imply (P x) (P y)).
def leq : Term -> Term -> Prop.
one : Term.
c : Term -> Term.
def test : Term -> Prop.
def complement : Term -> Term -> Prop.
def addition : Term -> Term -> Term.
zero : Term.
def multiplication : Term -> Term -> Term.
[B, A] leq A B --> (equal (addition A B) B).
[X0] test X0 --> (exists (X1:Term => (complement X1 X0))).
[X0, X1] complement X1 X0 --> (and (equal (multiplication X0 X1) zero) (and (equal (multiplication X1 X0) zero) (equal (addition X0 X1) one))).
[C, B, A] addition A (addition B C) --> (addition (addition A B) C)
[A] addition A zero --> A.
[C, B, A] multiplication A (multiplication B C) --> (multiplication (multiplication A B) C)
[A] multiplication A one --> A
[A] multiplication one A --> A
[C, B, A] multiplication A (addition B C) --> (addition (multiplication A B) (multiplication A C))
[C, B, A] multiplication (addition A B) C --> (addition (multiplication A C) (multiplication B C))
[A] multiplication A zero --> zero
[A] multiplication zero A --> zero.
def conjecture_proof : prf (imply (forall (A:Term => (forall (B:Term => (equal (addition A B) (addition B A)))))) (imply (forall (X0:Term => (forall (X1:Term => (imply (exists (X1:Term => (and (equal (multiplication X0 X1) zero) (and (equal (multiplication X1 X0) zero) (equal (addition X0 X1) one))))) (equiv (equal (c X0) X1) (and (equal (multiplication X1 X0) zero) (and (equal (multiplication X0 X1) zero) (equal (addition X1 X0) one))))))))) (imply (forall (X0:Term => (imply (not (exists (X1:Term => (and (equal (multiplication X0 X1) zero) (and (equal (multiplication X1 X0) zero) (equal (addition X0 X1) one)))))) (equal (c X0) zero)))) (equalc (c one) zero)))) :=
(H0 : prf (forall (A:Term => (forall (B:Term => (equal (addition A B) (addition B A)))))) => (H1 : prf (forall (X0:Term => (forall (X1:Term => (imply (exists (X1:Term => (and (equal (multiplication X0 X1) zero) (and (equal (multiplication X1 X0) zero) (equal (addition X0 X1) one))))) (equiv (equal (c X0) X1) (and (equal (multiplication X1 X0) zero) (and (equal (multiplication X0 X1) zero) (equal (addition X1 X0) one))))))))) => (H2 : prf (forall (X0:Term => (imply (not (exists (X1:Term => (and (equal (multiplication X0 X1) zero) (and (equal (multiplication X1 X0) zero) (equal (addition X0 X1) one)))))) (equal (c X0) zero)))) => (H3 : prf (not (equal (c one) zero)) => (H3 ((H2 one) (H4 : prf (exists (X1:Term => (and (equal X1 zero) (and (equal X1 zero) (equal (addition one X1) one))))) => ((((H1 one) (c one)) H4) False (H5 : prf (imply (equal (c one) (c one)) (and (equal (c one) zero) (and (equal (c one) zero) (equal (addition (c one) one) one)))) => H6 : prf (imply (and (equal (c one) zero) (and (equal (c one) zero) (equal (addition (c one) one) one))) (equal (c one) (c one))) => ((H5 (P9 : (Term -> Prop) => (H10 : prf (P9 (c one)) => H10))) False (H7 : prf (equal (c one) zero) => H8 : prf (and (equal (c one) zero) (equal (addition (c one) one) one)) => (H8 False (H11 : prf (equal (c one) zero) => H12 : prf (equal (addition (c one) one) one) => (H3 H11)))))))))))))).
#NAME tr.
def A : Type.
B : Type.
def x : A.
y : B.
[] A --> B.
[] x --> y.
#NAME hott.
Nat: Type.
Fin : Nat -> Type.
type:Type.
e: type -> Type.
def Finm: Nat -> Nat -> Type
:= i:Nat => j:Nat => (Fin i -> Fin j).
def comp := i:Nat => j:Nat => k:Nat => f:Finm i j => g:Finm j k => x:Fin i => g (f x).
Sn1: Type.
Bn: Sn1 -> Nat -> Type.
def mapBn: Ln1:Sn1 -> i:Nat -> ip:Nat -> Finm i ip -> Bn Ln1 ip -> Bn Ln1 i.
[Ln1,i,j,k,f,g,p]
mapBn Ln1 i j f (mapBn _ _ k g p) --> mapBn Ln1 i k (comp i j k f g) p.
n:Nat.
Sn: Type.
Ln1: Sn -> Sn1.
Xn : Ln:Sn -> Bn (Ln1 Ln) n -> Type.
Bsn: Sn -> Nat -> Type.
def bn : Ln:Sn -> i:Nat -> Bsn Ln i -> Bn (Ln1 Ln) i.
def bsn: Ln:Sn -> i:Nat -> p:Bsn Ln i -> f:Finm n i -> Xn Ln (mapBn (Ln1 Ln) n i f (bn Ln i p)).
mkBsn: Ln:Sn -> i:Nat -> bn:Bn (Ln1 Ln) i
-> bsn:(f:Finm n i -> Xn Ln (mapBn (Ln1 Ln) n i f bn)) -> Bsn Ln i.
[bn2] bn _ _ (mkBsn _ _ bn2 _) --> bn2.
[bsn2] bsn _ _ (mkBsn _ _ _ bsn2) --> bsn2.
#NAME Abstraction.
A : Type.
f: A -> A -> A.
def g: A -> (A -> A).
[x] g x --> (y => f y x).
#NAME AndPoly.
Bool : Type.
Nat : Type.
True : Bool.
False : Bool.
0 : Nat.
S : Nat -> Nat.
def Bool_ : Nat -> Type.
[] Bool_ 0 --> Bool.
[n] Bool_ (S n) --> Bool -> Bool_ n.
def and : Bool -> Bool -> Bool.
[] and False _ --> False.
[x] and True x --> x.
(; Une façon de définir and d'arité variable qui est rejetée avec un message d'erreur clair :
All the rewrite rules for the symbol 'and_' should have the same arity ;)
(;
def and_ : n : Nat -> Bool_ n.
[] and_ 0 --> True.
[x] and_ (S 0) x --> x.
[x,y,n] and_ (S (S n)) x y --> and_ (S n) (and x y).
(; ;)
(; Ici un and acceptant un nombre variable d'arguments qui type-check bien ;)
def and_ : n : Nat -> Bool_ n.
[] and_ 0 --> True.
[x] and_ (S 0) --> (x => x).
[x,y,n] and_ (S (S n)) --> (x : Bool => y : Bool => (and_ (S n) (and x y))).
(; ;)
(; Quand les patterns d'arités différentes sont imbriqués dans un sous-pattern, on obtient :
Assertion failed lors de la construction de l'arbre de décision
def e : n : Nat -> Bool_ n -> Bool_ n.
def andb : n : Nat -> Bool_ n.
[] e 0 (andb 0 ) --> True.
[x] e 0 (andb (S 0) x ) --> x.
[x,y,n] e n (andb _ x y) --> andb (S n) (and x y).
(; ;)
\ No newline at end of file
#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).
#NAME Associativity.
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).
(; The associativity of plus is needed to type the associativity of concat ;)
[x,y,z] plus (plus x y) z --> plus x (plus y z).
(; ;)
Vect : nat -> Type.
(; The non-linear version
def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
[n1,n2,n3,l1,l2,l3] concat (plus n1 n2) (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3).
(; ;)
(; Th linear version ;)
def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
[n1,n2,n3,l1,l2,l3] concat _ (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3).
(; ;)
\ No newline at end of file
#NAME binaire.
NatBin : Type.
1 : NatBin.
x2 : NatBin -> NatBin.
x2plus1 : NatBin -> NatBin.
def 3 := x2plus1 1.
def plus : NatBin -> NatBin -> NatBin.
[] plus 1 1 --> x2 1.
[y] plus 1 (x2 y) --> x2plus1 y.
[y] plus 1 (x2plus1 y) --> x2 (plus 1 y).
[x] plus (x2 x) 1 --> x2plus1 x.
[x,y] plus (x2 x) (x2 y) --> x2 (plus x y).
[x,y] plus (x2 x) (x2plus1 y) --> x2plus1 (plus x y).
[x] plus (x2plus1 x) 1 --> x2 (plus x 1).
[x,y] plus (x2plus1 x) (x2 y) --> x2plus1 (plus x y).
[x,y] plus (x2plus1 x) (x2plus1 y) --> x2 (plus 1 (plus x y)).
def mult : NatBin -> NatBin -> NatBin.
[x] mult x 1 --> x.
[y] mult 1 y --> y.
[x,y] mult (x2 x) (x2 y) --> x2 (x2 (mult x y)).
[x,y] mult (x2 x) (x2plus1 y) --> plus (x2 x) (x2 (x2 (mult x y))).
[x,y] mult (x2plus1 x) (x2 y) --> plus (x2 y) (x2 (x2 (mult x y))).
[x,y] mult (x2plus1 x) (x2plus1 y) --> plus (x2 (x2 (mult x y))) (plus (x2 x) (x2plus1 y)).
(;
#SNF mult (x2plus1 (x2plus1 1)) (x2plus1 (x2 1)).
(; ;)
def Syracuse : NatBin -> NatBin.
[] Syracuse 1 --> 1.
[x] Syracuse (x2 x) --> Syracuse x.
[x] Syracuse (x2plus1 x) --> Syracuse (plus 1 (mult 3 (x2plus1 x))).
(;
#SNF Syracuse (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2 (x2 (x2plus1 (x2 (x2 (x2 (x2 (x2plus1 (x2 (x2plus1 1))))))))))))))))).
(; ;)
\ No newline at end of file
#NAME bool.
Bool : Type.
def boucle : Bool -> Bool.
[x] boucle x --> boucle x.
#NAME church.
type : Type.
arr : type -> type -> type.
def e : type -> Type.
[a,b] e (arr a b) --> e a -> e b.
N : type.
z : e N.
s : e N -> e N.
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) => f.
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 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 four : numeral := plus two two.
def five : numeral := plus two three.
#CONV ( power two (times four five) ),
( power two (times five four) ).
#NAME cic.
Nat : Type.
z : Nat.
s : Nat -> Nat.
def m : Nat -> Nat -> Nat.
[i : Nat] m i z --> i.
[j : Nat] m z j --> j.
[i : Nat, j : Nat] m (s i) (s j) --> s (m i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
(; Universe successors ;)
def succ : Sort -> Sort.
[] succ prop --> type z.
[i : Nat] succ (type i) --> type (s i).
(; Universe cumulativity ;)
def next : Sort -> Sort.
[] next prop --> type z.