-
Notifications
You must be signed in to change notification settings - Fork 0
/
file.coc
40 lines (30 loc) · 1.27 KB
/
file.coc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
constant sorry : Π α : Sort 0, α.
constant false : Sort 0.
constant false_elim : Π C : Sort 0, Π h : false, C.
constant true : Sort 0.
constant true_intro : true.
def implies : Π α : Sort 0, Π β : Sort 0, Sort 0 := λ α : Sort 0, λ β : Sort 0, Π a : α, β.
def not : Π α : Sort 0, Sort 0 := λ α : Sort 0, implies α false.
constant and : Π α : Sort 0, Π β : Sort 0, Sort 0.
constant and_intro : Π α : Sort 0, Π β : Sort 0, Π a : α, Π b : β, and α β.
constant and_elim_left : Π α : Sort 0, Π β : Sort 0, implies (and α β) α.
constant and_elim_right : Π α : Sort 0, Π β : Sort 0, implies (and α β) β.
-- Proof that ¬(P ∧ ¬P)
def consistency : Π P : Sort 0, not (and P (not P)) :=
λ P : Sort 0,
λ both : and P (not P),
and_elim_right P (not P) both (and_elim_left P (not P) both)
.
def eo1a :
Π P : Sort 0, Π Q : Sort 0, Π R : Sort 0,
implies (implies P Q) (implies (implies R P) (implies R Q)) :=
λ P : Sort 0, λ Q : Sort 0, λ R : Sort 0,
λ pq : (implies P Q),
λ rp : (implies R P),
λ r : R,
pq (rp r)
.
def idtype : Sort 0 := Π α : Sort 0, Π x : α, α.
def id : idtype := λ α : Sort 0, λ x : α, x.
def id_1 : idtype := id idtype id. -- Applying it to itself
def id_2 : idtype := sorry idtype. -- Proof by sorry