diff --git a/examples/and.mdln b/examples/and.mdln
deleted file mode 100644
index d1b9a0d2db51fc63aef58fcee53af97a748dfa5f..0000000000000000000000000000000000000000
--- a/examples/and.mdln
+++ /dev/null
@@ -1,9 +0,0 @@
-def And: Prop -> Prop -> Prop := fun A B: Prop => (C: Prop) -> (A -> B -> C) -> C
-
-def And_intro := (A B: Prop) -> A -> B -> And A B
-def And_elim_g := (A B: Prop) -> And A B -> A
-def And_elim_d := (A B: Prop) -> And A B -> B
-
-def and_intro_lemma: And_intro := fun A B: Prop, a: A, b: B, C: Prop, f: A -> B -> C => f a b
-def and_elim_g_lemma: And_elim_g := fun A B: Prop, f: And A B => f A (fun a: A, b: B => a)
-def and_elim_d_lemma: And_elim_d := fun A B: Prop, f: And A B => f B (fun a: A, b: B => b)
diff --git a/examples/contraposition.mdln b/examples/contraposition.mdln
deleted file mode 100644
index f6a7aeefaaeec003b5cd415fe951ded0fdcea230..0000000000000000000000000000000000000000
--- a/examples/contraposition.mdln
+++ /dev/null
@@ -1,4 +0,0 @@
-def not: Prop -> Prop := fun P: Prop => P -> False
-
-def Contrapose := (A B: Prop) -> (A -> B) -> (not B -> not A)
-def contrapose_lemma: Contrapose := fun A B: Prop, f: A -> B, nB: not B, a: A => nB (f a)
diff --git a/examples/eq.mdln b/examples/eq.mdln
index b9558aa43d58a9473c90cb7bc27af1a3a7dc2cfc..661c18226a1cee6e7da366845ab5497444a662d7 100644
--- a/examples/eq.mdln
+++ b/examples/eq.mdln
@@ -1,22 +1,3 @@
-def transport_type.{u,v} := (A : Sort u) -> (P : A -> Sort v) -> (x y : A) -> Eq.{u} A x y -> P x -> P y
+import ../std/eq.mdln
-def transport.{u,v} : transport_type.{u,v} :=
- fun A:Sort u,P:A -> Sort v,x y:A, p: Eq.{u} A x y,h:P x =>
- Eq_rec.{u,v} A x (fun y:A,p:Eq.{u} A x y => P y) h y p
-
-def transport_id.{u} := fun A:Sort u,x:A => transport.{u,u} A (fun x:A => A) x x (Refl.{u} A x) x
-
-def symm.{u} : (A : Sort u) -> (x y : A) -> Eq.{u} A x y -> Eq.{u} A y x :=
- fun A:Sort u,
- x y: A,
- e : Eq.{u} A x y =>
- Eq_rec.{u,0} A x (fun y:A, e:Eq.{u} A x y => Eq.{u} A y x) (Refl.{u} A x) y e
-
-def trans.{u} : (A : Sort u) -> (x y z : A) -> Eq.{u} A x y -> Eq.{u} A y z -> Eq.{u} A x z :=
- fun A: Sort u,
- x y z : A,
- e1 : Eq.{u} A x y,
- e2 : Eq.{u} A y z =>
- Eq_rec.{u,0} A y (fun x:A,e:Eq.{u} A y x => Eq.{u} A x z) e2 x (symm.{u} A x y e1)
-
-check Refl.{1} Nat Zero : Eq.{1} Nat Zero (transport_id.{1} Nat Zero)
\ No newline at end of file
+check Refl.{1} Nat Zero : Eq.{1} Nat Zero (transport_id.{1} Nat Zero)
diff --git a/examples/irrelevance.mdln b/examples/irrelevance.mdln
index 56d399eab8caaf414f78bc6d3c5459b829766d00..0eca694e6cd50e6fd5944395eb83bb9f43d25792 100644
--- a/examples/irrelevance.mdln
+++ b/examples/irrelevance.mdln
@@ -1,9 +1,9 @@
-def True := False -> False
+def myTrue := False -> False
-def id.{u} := fun A:Sort u,x:A => x
+def id.{u} := fun A: Sort u, x: A => x
-def tt1 : True := id.{0} False
+def tt1: myTrue := id.{0} False
-def tt2 : True := fun h:False => False_rec.{0} (fun h:False => False) h
+def tt2: myTrue := fun h: False => False_rec.{0} (fun h: False => False) h
-check Refl.{0} True tt1 : Eq.{0} True tt1 tt2
\ No newline at end of file
+check Refl.{0} myTrue tt1: Eq.{0} myTrue tt1 tt2
diff --git a/examples/nat_eq.mdln b/examples/nat_eq.mdln
deleted file mode 100644
index 42ce6392e301232b06ebbe3e48964058b1a1b244..0000000000000000000000000000000000000000
--- a/examples/nat_eq.mdln
+++ /dev/null
@@ -1,28 +0,0 @@
-def id.{u} := fun A :Sort u,x:A => x
-
-def Not := fun A : Prop => A -> False
-def True := False -> False
-def tt : True := id.{0} False
-
-def transport_type.{u,v} := (A : Sort u) -> (P : A -> Sort v) -> (x y : A) -> Eq.{u} A x y -> P x -> P y
-
-def transport.{u,v} : transport_type.{u,v} :=
- fun A:Sort u,
- P:A -> Sort v,
- x y:A,
- p: Eq.{u} A x y,
- h:P x =>
- Eq_rec.{u,v} A x (fun y:A,p:Eq.{u} A x y => P y) h y p
-
-def cast.{u} : (A B : Sort u) -> Eq.{u+1} (Sort u) A B -> A -> B :=
- fun A B : Sort u,
- e : Eq.{u+1} (Sort u) A B,
- a : A =>
- transport.{u+1,u} (Sort u) (fun A:Sort u => A) A B e a
-
-def is_zero := Nat_rec.{1} (fun n:Nat => Prop) True (fun n:Nat, p:Prop => False)
-
-def z_neq_s : (n: Nat) -> Not (Eq.{1} Nat Zero (Succ n)):=
- fun n: Nat,
- e : Eq.{1} Nat Zero (Succ n) =>
- transport.{1,0} Nat is_zero Zero (Succ n) e tt
\ No newline at end of file
diff --git a/proost/src/main.rs b/proost/src/main.rs
index 02641c3ed26116e6c35cb749ee087d5e16463785..b9213f5abd932b51a58561ae389f52a5a2a38f71 100644
--- a/proost/src/main.rs
+++ b/proost/src/main.rs
@@ -104,7 +104,7 @@ fn main() -> Result<'static, 'static, ()> {
// check if files are provided as command-line arguments
if !args.files.is_empty() {
- return kernel::memory::arena::use_arena(|arena| {
+ return kernel::memory::arena::use_arena_with_axioms(|arena| {
let command = Command::Import(args.files.iter().map(|file| (Location::default(), file.as_str())).collect());
display(evaluator.process_line(arena, &command), false);
diff --git a/std/eq.mdln b/std/eq.mdln
new file mode 100644
index 0000000000000000000000000000000000000000..73452b99c46b31988c2dfbf92f5822df38622e0d
--- /dev/null
+++ b/std/eq.mdln
@@ -0,0 +1,30 @@
+def transport_type.{u, v} := (A: Sort u) -> (P: A -> Sort v) -> (x y: A) -> Eq.{u} A x y -> P x -> P y
+
+def transport.{u, v}: transport_type.{u, v} :=
+ fun A: Sort u,
+ P: A -> Sort v,
+ x y: A,
+ p: Eq.{u} A x y,
+ h: P x =>
+ Eq_rec.{u, v} A x (fun y: A, p: Eq.{u} A x y => P y) h y p
+
+def transport_id.{u} := fun A: Sort u, x:A => transport.{u, u} A (fun x: A => A) x x (Refl.{u} A x) x
+
+def cast.{u}: (A B: Sort u) -> Eq.{u + 1} (Sort u) A B -> A -> B :=
+ fun A B: Sort u,
+ e: Eq.{u + 1} (Sort u) A B,
+ a: A =>
+ transport.{u + 1,u} (Sort u) (fun A: Sort u => A) A B e a
+
+def symm.{u}: (A: Sort u) -> (x y: A) -> Eq.{u} A x y -> Eq.{u} A y x :=
+ fun A: Sort u,
+ x y: A,
+ e: Eq.{u} A x y =>
+ Eq_rec.{u, 0} A x (fun y: A, e: Eq.{u} A x y => Eq.{u} A y x) (Refl.{u} A x) y e
+
+def trans.{u}: (A: Sort u) -> (x y z: A) -> Eq.{u} A x y -> Eq.{u} A y z -> Eq.{u} A x z :=
+ fun A: Sort u,
+ x y z: A,
+ e1: Eq.{u} A x y,
+ e2: Eq.{u} A y z =>
+ Eq_rec.{u, 0} A y (fun x:A, e:Eq.{u} A y x => Eq.{u} A x z) e2 x (symm.{u} A x y e1)
diff --git a/std/nat.mdln b/std/nat.mdln
new file mode 100644
index 0000000000000000000000000000000000000000..630f23ab51f8e0ea89e2949bcb6b508ec8bf5920
--- /dev/null
+++ b/std/nat.mdln
@@ -0,0 +1,9 @@
+import eq.mdln
+import prop/connectives.mdln
+
+def is_zero := Nat_rec.{1} (fun n: Nat => Prop) True (fun n: Nat, p: Prop => False)
+
+def z_neq_s: (n: Nat) -> Not (Eq.{1} Nat Zero (Succ n)) :=
+ fun n: Nat,
+ e: Eq.{1} Nat Zero (Succ n) =>
+ transport.{1, 0} Nat is_zero Zero (Succ n) e Tt
diff --git a/std/prop/classical.mdln b/std/prop/classical.mdln
new file mode 100644
index 0000000000000000000000000000000000000000..4139c388b621d33cd09ef6a4f23b35c73de95782
--- /dev/null
+++ b/std/prop/classical.mdln
@@ -0,0 +1,106 @@
+// This file proves some lemmas on classical logic.
+
+import connectives.mdln
+import false.mdln
+
+// The law of excluded middle. Note, this is a definition, not an
+// assumption! If you want to prove a theorem in classical logic,
+// formulate it as "Excluded_middle -> <what you want>".
+
+def Excluded_middle: Prop := (P: Prop) -> Or P (Not P)
+
+// The following proves that the following axioms are equivalent:
+// Excluded_middle: (1) ∀P, P ∨ ¬P
+// Double_negation_elimination: (2) ∀P, ¬¬P → P
+// Implication_as_or: (3) ∀P,Q, (P → Q) → (¬P ∨ Q)
+// Peirce: (4) ∀P,Q, ((P → Q) → P) → P
+// Proof by:
+// (1) => (2), (2) => (3), (3) => (1)
+// (1) => (4), (4) => (1)
+
+def Double_negation_elimination: Prop := (P : Prop) -> ((Not (Not P)) -> P)
+
+def Implication_as_or: Prop := (P Q : Prop) -> (P -> Q) -> Or (Not P) Q
+
+def Peirce: Prop := (P Q: Prop) -> ((P -> Q) -> P) -> P
+
+// Lemmas (TODO: put in namespace when that works)
+def excluded_middle_implies_double_negation_elimination: (Excluded_middle -> Double_negation_elimination) :=
+ fun excl : Excluded_middle, P: Prop, notnotP : (Not (Not P)) =>
+ (excl P) // Apply P \/ ~P
+ P // ... to prove P
+ (fun p: P => p) // P case: P -> P is trivial
+ // ~P case by contradiction with ~~P
+ (fun notP: (Not P) =>
+ (exfalso P (notnotP notP)))
+
+def double_negation_elimination_implies_implication_as_or: (Double_negation_elimination -> Implication_as_or) :=
+ (fun elim: Double_negation_elimination, P Q: Prop, PtoQ : (P -> Q) =>
+ elim (Or (Not P) Q) // Prove ~P \/ Q by ~~(~P \/ Q)
+ (fun H: Not (Or (Not P) Q) => // Assume ~(~P \/ Q) and prove False
+ (fun p : P, qf: Not Q => qf (PtoQ p)) // From lemmas P and ~Q, prove False by P, P -> Q, Q -> False
+ (elim P // Prove P by ~~P
+ (fun HP: (Not P) => // Assume ~P, prove False
+ H (or_intro_l (Not P) Q HP))) // Deduce False from ~(~P \/ Q)
+ (fun q : Q => // Assume Q, prove False.
+ H (or_intro_r (Not P) Q q)))) // Deduce False from ~(~P \/ Q)
+
+def implication_as_or_implies_excluded_middle: Implication_as_or -> Excluded_middle :=
+ (fun imp2or : Implication_as_or, P: Prop => // Let's prove ~P \/ P
+ or_comm (Not P) P // Trivially follows from P \/ ~P
+ (imp2or P P (fun p: P => p))) // P -> P, therefore ~P \/ P
+
+// Boilerplate: deduce (1) <=> (2) from (1) => (2) => (3) => (1)
+def excluded_middle_iff_double_negation_elimination: Iff Excluded_middle Double_negation_elimination :=
+ (iff_intro
+ Excluded_middle
+ Double_negation_elimination
+ excluded_middle_implies_double_negation_elimination
+ (fun elim: Double_negation_elimination =>
+ implication_as_or_implies_excluded_middle
+ (double_negation_elimination_implies_implication_as_or elim)))
+
+// Boilerplate: deduce (1) <=> (3) from (1) => (2) => (3) => (1)
+def excluded_middle_iff_implication_as_or: Iff Excluded_middle Implication_as_or :=
+ (iff_intro
+ Excluded_middle
+ Implication_as_or
+ (fun excl: Excluded_middle =>
+ double_negation_elimination_implies_implication_as_or
+ (excluded_middle_implies_double_negation_elimination excl))
+ implication_as_or_implies_excluded_middle)
+
+def excluded_middle_implies_peirce: Excluded_middle -> Peirce :=
+ (fun excl: Excluded_middle, P Q: Prop, H: ((P -> Q) -> P) =>
+ (excl P) // Eliminate from P \/ ~P
+ P // To prove P
+ (fun p: P => p) // P -> P is trivial
+ // ~P -> P
+ (fun nP: Not P =>
+ H // Prove P by H
+ // Need to prove P -> Q
+ (fun p: P =>
+ // We have P and ~P, we can prove anything.
+ exfalso Q (nP p))))
+
+def peirce_implies_excluded_middle: Peirce -> Excluded_middle :=
+ (fun peirce: Peirce, P: Prop =>
+ // Specialize Peirce's law:
+ // (((P \/ ~P) -> False) -> (P \/ ~P)) -> (P \/ ~P)
+ // Thus we can prove P \/ ~P by
+ // ((P \/ ~P) -> False) -> (P \/ ~P)
+ (peirce (Or P (Not P)) False)
+ (fun H: ((Or P (Not P)) -> False) => // assume (P \/ ~P) -> False
+ // We want to prove P \/ ~P. It suffices to prove ~P.
+ or_intro_r P (Not P)
+ // Prove ~P.
+ (fun p: P => // Assume P, deduce False
+ // We know P \/ ~P -> False, and we can prove
+ // P \/ ~P with P.
+ H (or_intro_l P (Not P) p))))
+
+// Boilerplate: deduce (1) <=> (4) from (1) => (4) => (1)
+def excluded_middle_iff_peirce: Iff Excluded_middle Peirce :=
+ (iff_intro Excluded_middle Peirce
+ excluded_middle_implies_peirce
+ peirce_implies_excluded_middle)
diff --git a/std/prop/connectives.mdln b/std/prop/connectives.mdln
new file mode 100644
index 0000000000000000000000000000000000000000..088b576979614d9f19e82e7153ce1ed0c1c8c4f3
--- /dev/null
+++ b/std/prop/connectives.mdln
@@ -0,0 +1,38 @@
+// Basic logical connectives in Prop: and, or, not, iff
+
+// === And ===
+def And: Prop -> Prop -> Prop := fun A B: Prop => (C: Prop) -> (A -> B -> C) -> C
+
+def and_intro: (A B: Prop) -> A -> B -> And A B :=
+ fun A B: Prop, a: A, b: B, C: Prop, f: A -> B -> C => f a b
+
+def and_elim_l: (A B: Prop) -> And A B -> A :=
+ fun A B: Prop, f: And A B => f A (fun a: A, b: B => a)
+
+def and_elim_r: (A B: Prop) -> And A B -> B :=
+ fun A B: Prop, f: And A B => f B (fun a: A, b: B => b)
+
+def and_comm: (A B: Prop) -> (And A B) -> (And B A) :=
+ fun A B: Prop, f: (And A B), C: Prop, bac: (B -> A -> C) => f C (fun a:A, b:B => bac b a)
+
+// === Or ===
+def Or: Prop -> Prop -> Prop := fun A B : Prop => (C: Prop) -> (A -> C) -> (B -> C) -> C
+
+def or_intro_l : (A B : Prop) -> A -> Or A B :=
+ fun A B: Prop, a: A, C: Prop, fAC: A -> C, fBC: B -> C => fAC a
+
+def or_intro_r : (A B : Prop) -> B -> Or A B :=
+ fun A B: Prop, b: B, C: Prop, fAC: A -> C, fBC: B -> C => fBC b
+
+def or_comm: (A B : Prop) -> (Or A B) -> Or B A :=
+ (fun A B: Prop, orAB: (Or A B), C: Prop, fBC: B -> C, fAC: A -> C =>
+ orAB C fAC fBC)
+
+// === Not ===
+def Not: Prop -> Prop := fun P: Prop => P -> False
+
+// === Iff ===
+def Iff: Prop -> Prop -> Prop := fun P Q: Prop => And (P -> Q) (Q -> P)
+
+def iff_intro: (P Q: Prop) -> (P -> Q) -> (Q -> P) -> Iff P Q :=
+ fun P Q: Prop, PQ: P -> Q, QP: Q -> P => and_intro (P -> Q) (Q -> P) PQ QP
diff --git a/std/prop/contraposition.mdln b/std/prop/contraposition.mdln
new file mode 100644
index 0000000000000000000000000000000000000000..bc4d63a97a5f22260577bf6c2aedaf06a7bba4e7
--- /dev/null
+++ b/std/prop/contraposition.mdln
@@ -0,0 +1,6 @@
+// Contraposition
+
+import connectives.mdln
+
+def contrapose: (A B: Prop) -> (A -> B) -> (Not B -> Not A) :=
+ fun A B: Prop, f: A -> B, nB: (Not B), a: A => nB (f a)
diff --git a/std/prop/false.mdln b/std/prop/false.mdln
new file mode 100644
index 0000000000000000000000000000000000000000..678111e33eed864466ba565a54f38be082bfc491
--- /dev/null
+++ b/std/prop/false.mdln
@@ -0,0 +1,2 @@
+def exfalso: (P: Prop) -> False -> P := fun P: Prop, f: False =>
+ False_rec.{0} (fun _: False => P) f