Commit 25bbfedd authored by Francois THIRE's avatar Francois THIRE

Add more theories

parent 6d41e673
#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.
[i : Nat] next (type i) --> type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1 : Sort] rule s1 prop --> prop.
[s2 : Sort] rule prop s2 --> s2.
[i : Nat, j : Nat] rule (type i) (type j) --> type (m i j).
def max : Sort -> Sort -> Sort.
[s1 : Sort] max s1 prop --> s1.
[s2 : Sort] max prop s2 --> s2.
[i : Nat, j : Nat] max (type i) (type j) --> type (m i j).
(; Types and terms ;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (succ s).
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (max s1 s2).
def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).
[s : Sort] Term _ (univ s) --> Univ s.
[s1 : Sort, s2 : Sort, a : Univ s1] Term _ (lift s1 s2 a) --> Term s1 a.
[s1 : Sort, s2 : Sort, a : Univ s1, b : (Term s1 a -> Univ s2)]
Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
[s : Sort] max s s --> s.
[s1 : Sort, s2 : Sort, s3 : Sort] max (max s1 s2) s3 --> max s1 (max s2 s3).
[s1 : Sort, s2 : Sort, s3 : Sort] rule (max s1 s3) s2 --> max (rule s1 s2) (rule s3 s2).
[s1 : Sort, s2 : Sort, s3 : Sort] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).
[s : Sort, a : Univ s] lift s s a --> a.
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1]
lift _ s3 (lift s1 s2 a) -->
lift s1 (max s2 s3) a.
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1, b : Term s1 a -> Univ s2]
prod _ s2 (lift s1 s3 a) b -->
lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1, b : Term s1 a -> Univ s2]
prod s1 _ a (x => lift s2 s3 (b x)) -->
lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
#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 hol.
(;-----------;)
(; HOL Types ;)
(;-----------;)
type : Type.
bool : type.
ind : type.
arr : type -> type -> type.
(;-----------;)
(; HOL Terms ;)
(;-----------;)
def term : type -> Type.
[a,b] term (arr a b) --> term a -> term b.
eq : a : type -> term (arr a (arr a bool)).
select : a : type -> term (arr (arr a bool) a).
(;------------;)
(; HOL Proofs ;)
(;------------;)
proof : term bool -> Type.
REFL : a : type -> t : term a ->
proof (eq a t t).
ABS_THM : a : type -> b : type -> f : (term a -> term b) -> g : (term a -> term b) ->
(x : term a -> proof (eq b (f x) (g x))) ->
proof (eq (arr a b) f g).
APP_THM : a : type -> b : type -> f : term (arr a b) -> g : term (arr a b) -> x : term a -> y : term a ->
proof (eq (arr a b) f g) ->
proof (eq a x y) ->
proof (eq b (f x) (g y)).
PROP_EXT : p : term bool -> q : term bool ->
(proof q -> proof p) ->
(proof p -> proof q) ->
proof (eq bool p q).
EQ_MP : p : term bool -> q : term bool ->
proof (eq bool p q) ->
proof p ->
proof q.
def BETA_CONV : a : type -> b : type -> f : (term a -> term b) -> u : term a ->
proof (eq b (f u) (f u)) :=
a : type => b : type => f : (term a -> term b) => u : term a =>
REFL b (f u).
def SYM (a : type) (t : term a) (u : term a) (H : proof (eq a t u)) : proof (eq a u t)
:=
EQ_MP
(eq a t t)
(eq a u t)
(APP_THM
a
bool
(eq a t)
(eq a u)
t
t
(APP_THM
a
(arr a bool)
(eq a)
(eq a)
t
u
(REFL (arr a (arr a bool)) (eq a))
H)
(REFL a t))
(REFL a t).
def TRANS (a : type) (t : term a) (u : term a) (v : term a) (H1 : proof (eq a t u)) (H2 : proof (eq a u v)) : proof (eq a t v)
:=
EQ_MP
(eq a u v)
(eq a t v)
(APP_THM
a
bool
(eq a u)
(eq a t)
v
v
(APP_THM a (arr a bool) (eq a) (eq a) u t (REFL (arr a (arr a bool)) (eq a)) (SYM a t u H1))
(REFL a v))
H2.
def PROVE_HYP (x : term bool) (y : term bool) (H1 : proof x) (H2 : proof x -> proof y) : proof y := H2 H1.
(;---------------------;)
(; Derived Connectives ;)
(;---------------------;)
def true : term bool :=
eq (arr bool bool) (p : term bool => p) (p : term bool => p).
def forall : a : type -> p : term (arr a bool) -> term bool :=
a : type => p : term (arr a bool) =>
eq (arr a bool) p (x : term a => true).
def false : term bool :=
forall bool (p : term bool => p).
def and : term (arr bool (arr bool bool)) :=
p : term bool => q : term bool =>
eq (arr (arr bool (arr bool bool)) bool)
(f : term (arr bool (arr bool bool)) => f p q)
(f : term (arr bool (arr bool bool)) => f true true).
def imp : term (arr bool (arr bool bool)) :=
p : term bool => q : term bool =>
eq bool (and p q) p.
def or : term (arr bool (arr bool bool)) :=
p : term bool => q : term bool =>
forall bool (r : term bool => imp (imp p r) (imp (imp q r) r)).
def cond : a : type -> term (arr bool (arr a (arr a a))) :=
a : type => t : term bool => t1 : term a => t2 : term a =>
select a (x : term a =>
and
(imp (eq bool t true) (eq a x t1))
(imp (eq bool t false) (eq a x t2))).
def not (p : term bool) :=
imp p false.
witness : a : type -> term a.
(; := a : type => select a (x : term a => true). ;)
def true_intro : proof true :=
REFL (arr bool bool) (p : term bool => p).
def eq_sym (a : type) (x : term a) (y : term a) (h : proof (eq a x y)) : proof (eq a y x) :=
EQ_MP (eq a x x) (eq a y x)
(APP_THM a bool (eq a x) (eq a y) x x
(APP_THM a (arr a bool) (eq a) (eq a) x y
(REFL (arr a (arr a bool)) (eq a))
(h))
(REFL a x))
(REFL a x).
def eq_true_intro (p : term bool) (h : proof p) : proof (eq bool p true) :=
PROP_EXT p true (h2 : proof true => h) (h : proof p => true_intro).
def eq_true_elim (p : term bool) (h : proof (eq bool p true)) : proof p :=
EQ_MP true p (eq_sym bool p true h) true_intro.
def forall_intro (a : type) (p : term (arr a bool))
(h : (x : term a -> proof (p x))) : proof (forall a p) :=
ABS_THM a bool p (x : term a => true) (x : term a =>
eq_true_intro (p x) (h x)).
def forall_elim (a : type) (p : term (arr a bool))
(h : proof (forall a p)) (x : term a) : proof (p x) :=
eq_true_elim (p x)
(APP_THM a bool p (x : term a => true) x x h (REFL a x)).
def false_elim (p : term bool) (h : proof false) : proof p :=
forall_elim bool (p : term bool => p) h p.
def and_intro (p : term bool)
(q : term bool)
(Hp : proof p)
(Hq : proof q)
: proof (and p q)
:=
ABS_THM
(arr bool (arr bool bool))
bool
(f : term (arr bool (arr bool bool)) => f p q)
(f : term (arr bool (arr bool bool)) => f true true)
(f : term (arr bool (arr bool bool)) =>
APP_THM
bool
bool
(f p)
(f true)
q
true
(APP_THM
bool
(arr bool bool)
f
f
p
true
(REFL (arr bool (arr bool bool)) f)
(eq_true_intro p Hp))
(eq_true_intro q Hq)).
def and_elim1 (p : term bool)
(q : term bool)
(Hpq : proof (and p q))
: proof p
:=
eq_true_elim p
(APP_THM
(arr bool (arr bool bool))
bool
(f : (term bool -> term bool -> term bool) => f p q)
(f : (term bool -> term bool -> term bool) => f true true)
(x : term bool => y : term bool => x)
(x : term bool => y : term bool => x)
Hpq
(REFL (arr bool (arr bool bool)) (x : term bool => y : term bool => x))).
def and_elim2 (p : term bool)
(q : term bool)
(Hpq : proof (and p q))
: proof q
:=
eq_true_elim q
(APP_THM
(arr bool (arr bool bool))
bool
(f : (term bool -> term bool -> term bool) => f p q)
(f : (term bool -> term bool -> term bool) => f true true)
(x : term bool => y : term bool => y)
(x : term bool => y : term bool => y)
Hpq
(REFL (arr bool (arr bool bool)) (x : term bool => y : term bool => y))).
def imp_intro (p : term bool)
(q : term bool)
(Hpq : proof p -> proof q)
: proof (imp p q)
:=
PROP_EXT (and p q) p
(Hp : proof p =>
and_intro p q Hp (Hpq Hp))
(and_elim1 p q).
def imp_elim (p : term bool)
(q : term bool)
(Hpq : proof (imp p q))
(Hp : proof p)
: proof q
:=
and_elim2 p q (EQ_MP p (and p q) (eq_sym bool (and p q) p Hpq) Hp).
def or_intro1 (p : term bool)
(q : term bool)
(Hp : proof p)
: proof (or p q)
:=
forall_intro
bool
(r : term bool => imp (imp p r) (imp (imp q r) r))
(r : term bool =>
imp_intro
(imp p r)
(imp (imp q r) r)
(H : proof (imp p r) =>
imp_intro
(imp q r)
r
(__ : proof (imp q r) =>
imp_elim p r H Hp))).
def or_intro2 (p : term bool)
(q : term bool)
(Hq : proof q)
: proof (or p q)
:=
forall_intro
bool
(r : term bool => imp (imp p r) (imp (imp q r) r))
(r : term bool =>
imp_intro
(imp p r)
(imp (imp q r) r)
(__ : proof (imp p r) =>
imp_intro
(imp q r)
r
(H : proof (imp q r) =>
imp_elim q r H Hq))).
def or_elim (p : term bool)
(q : term bool)
(r : term bool)
(Hpq : proof (or p q))
(Hpr : proof p -> proof r)
(Hqr : proof q -> proof r) : proof r
:=
imp_elim
(imp q r)
r
(imp_elim
(imp p r)
(imp (imp q r) r)
(forall_elim
bool
(r : term bool => imp (imp p r) (imp (imp q r) r))
Hpq
r)
(imp_intro p r Hpr))
(imp_intro q r Hqr).
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