wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

infix operators!

Browse source
This commit is contained in:
William Ball 2024-12-10 20:31:53 -08:00
parent 7dce99e1f8
commit f9e0ec40bd
7 changed files with 363 additions and 289 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

121
examples/algebra.pg
View file

@ -15,42 +15,44 @@ section BasicDefinitions
-- I'd always strongly recommend including the type ascriptions for theorems
-- Fix some set A
variable (A : *);
variable (A : ★);
-- a unary operation is a function `A -> A`
def unop := A -> A;
-- a unary operation is a function `A → A`
def unop := A → A;
-- a binary operation is a function `A -> A -> A`
def binop := A -> A -> A;
-- a binary operation is a function `A → A → A`
def binop := A → A → A;
-- fix some binary operation `op`
variable (op : binop);
variable (* : binop);
infixl 20 *;
-- it is associative if ...
def assoc := forall (a b c : A), eq A (op a (op b c)) (op (op a b) c);
def assoc := forall (a b c : A), eq A (a * (b * c)) ((a * b) * c);
-- fix some element `e`
variable (e : A);
-- it is a left identity with respect to binop `op` if `∀ a, e * a = a`
def id_l := forall (a : A), eq A (op e a) a;
def id_l := forall (a : A), eq A (e * a) a;
-- likewise for right identity
def id_r := forall (a : A), eq A (op a e) a;
def id_r := forall (a : A), eq A (a * e) a;
-- an element is an identity element if it is both a left and right identity
def id := and id_l id_r;
def id := id_l ∧ id_r;
-- b is a left inverse for a if `b * a = e`
-- NOTE: we don't require `e` to be an identity in this definition.
-- this definition is purely for convenience's sake
def inv_l (a b : A) := eq A (op b a) e;
def inv_l (a b : A) := eq A (b * a) e;
-- likewise for right inverse
def inv_r (a b : A) := eq A (op a b) e;
def inv_r (a b : A) := eq A (a * b) e;
-- and full-on inverse
def inv (a b : A) := and (inv_l a b) (inv_r a b);
def inv (a b : A) := inv_l a b ∧ inv_r a b;
end BasicDefinitions
@ -59,15 +61,21 @@ end BasicDefinitions
-- --------------------------------------------------------------------------------------------------------------
-- a set `S` with binary operation `op` is a semigroup if its operation is associative
def semigroup (S : *) (op : binop S) : * := assoc S op;
def semigroup (S : ★) (op : binop S) : ★ := assoc S op;
section Monoid
variable (M : *) (op : binop M) (e : M);
-- Let `M` be a set with binary operation `op` and element `e`.
variable (M : ★) (op : binop M) (e : M);
-- We'll use `*` as an infix shorthand for `op`
def * (a b : M) := op a b;
infixl 50 *;
-- a set `M` with binary operation `op` and element `e` is a monoid
def monoid : * := and (semigroup M op) (id M op e);
def monoid : ★ := (semigroup M op) ∧ (id M op e);
-- Suppose `(M, *, e)` is a monoid
hypothesis (Hmonoid : monoid);
-- some "getters" for `monoid` so we don't have to do a bunch of very verbose
@ -87,10 +95,10 @@ section Monoid
def monoid_id_l_implies_identity (a : M) (H : id_l M op a) : eq M a e :=
-- WTS a = a * e = e
-- we can use `eq_trans` to glue proofs of `a = a * e` and `a * e = e` together
eq_trans M a (op a e) e
eq_trans M a (a * e) e
-- first, `a = a * e`, but we'll use `eq_sym` to flip it around
(eq_sym M (op a e) a
(eq_sym M (a * e) a
-- now the goal is to show `a * e = a`, which follows immediately from `id_r`
(id_rm a))
@ -100,10 +108,10 @@ section Monoid
-- the analogous result for right identities
def monoid_id_r_implies_identity (a : M) (H : id_r M op a) : eq M a e :=
-- this time, we'll show `a = e * a = e`
eq_trans M a (op e a) e
eq_trans M a (e * a) e
-- first, `a = e * a`
(eq_sym M (op e a) a
(eq_sym M (e * a) a
-- this time, it immediately follows from `id_l`
(id_lm a))
@ -114,12 +122,15 @@ end Monoid
section Group
variable (G : *) (op : binop G) (e : G) (i : unop G);
variable (G : ★) (op : binop G) (e : G) (i : unop G);
def * (a b : G) := op a b;
infixl 50 *;
-- groups are just monoids with inverses
def has_inverses : * := forall (a : G), inv G op e a (i a);
def has_inverses : ★ := forall (a : G), inv G op e a (i a);
def group : * := and (monoid G op e) has_inverses;
def group : ★ := (monoid G op e) ∧ has_inverses;
hypothesis (Hgroup : group);
@ -141,23 +152,23 @@ section Group
-- = (b * a) * a^-1
-- = e * a^-1
-- = a^-1
eq_trans G b (op b e) (i a)
eq_trans G b (b * e) (i a)
-- b = b * e
(eq_sym G (op b e) b (id_rg b))
(eq_sym G (b * e) b (id_rg b))
-- b * e = a^-1
(eq_trans G (op b e) (op b (op a (i a))) (i a)
(eq_trans G (b * e) (b * (a * i a)) (i a)
--b * e = b * (a * a^-1)
(eq_cong G G e (op a (i a)) (op b)
(eq_cong G G e (a * i a) (op b)
-- e = a * a^-1
(eq_sym G (op a (i a)) e (inv_rg a)))
(eq_sym G (a * i a) e (inv_rg a)))
-- b * (a * a^-1) = a^-1
(eq_trans G (op b (op a (i a))) (op (op b a) (i a)) (i a)
(eq_trans G (b * (a * i a)) (b * a * i a) (i a)
-- b * (a * a^-1) = (b * a) * a^-1
(assoc_g b a (i a))
-- (b * a) * a^-1 = a^-1
(eq_trans G (op (op b a) (i a)) (op e (i a)) (i a)
(eq_trans G (b * a * i a) (e * i a) (i a)
-- (b * a) * a^-1 = e * a^-1
(eq_cong G G (op b a) e (fun (x : G) => op x (i a)) h)
(eq_cong G G (b * a) e (fun (x : G) => x * i a) h)
-- e * a^-1 = a^-1
(id_lg (i a)))));
@ -168,66 +179,60 @@ section Group
-- = a^-1 * (a * b)
-- = a^-1 * e
-- = a^-1
eq_trans G b (op e b) (i a)
eq_trans G b (e * b) (i a)
-- b = e * b
(eq_sym G (op e b) b (id_lg b))
(eq_sym G (e * b) b (id_lg b))
-- e * b = a^-1
(eq_trans G (op e b) (op (op (i a) a) b) (i a)
(eq_trans G (e * b) (i a * a * b) (i a)
-- e * b = (a^-1 * a) * b
(eq_cong G G e (op (i a) a) (fun (x : G) => op x b)
(eq_cong G G e (i a * a) (fun (x : G) => x * b)
-- e = (a^-1 * a)
(eq_sym G (op (i a) a) e (inv_lg a)))
(eq_sym G (i a * a) e (inv_lg a)))
-- (a^-1 * a) * b = a^-1
(eq_trans G (op (op (i a) a) b) (op (i a) (op a b)) (i a)
(eq_trans G (i a * a * b) (i a * (a * b)) (i a)
-- (a^-1 * a) * b = a^-1 * (a * b)
(eq_sym G (op (i a) (op a b)) (op (op (i a) a) b) (assoc_g (i a) a b))
(eq_sym G (i a * (a * b)) (i a * a * b) (assoc_g (i a) a b))
-- a^-1 * (a * b) = a^-1
(eq_trans G (op (i a) (op a b)) (op (i a) e) (i a)
(eq_trans G (i a * (a * b)) (i a * e) (i a)
-- a^-1 * (a * b) = a^-1 * e
(eq_cong G G (op a b) e (op (i a)) h)
(eq_cong G G (a * b) e (op (i a)) h)
-- a^-1 * e = a^-1
(id_rg (i a)))));
-- the classic shoes and socks theorem, namely that (a * b)^-1 = b^-1 * a^-1
def shoes_and_socks (a b : G) : eq G (i (op a b)) (op (i b) (i a)) :=
eq_sym G (op (i b) (i a)) (i (op a b))
(right_inv_unique (op a b) (op (i b) (i a))
def shoes_and_socks (a b : G) : eq G (i (a * b)) (i b * i a) :=
eq_sym G (i b * i a) (i (a * b))
(right_inv_unique (a * b) (i b * i a)
-- WTS: (a * b) * (b^-1 * a^-1) = e
(let
-- some abbreviations for common terms
(ab := op a b)
(biai := op (i b) (i a))
(ab_bi := op (op a b) (i b))
(a_bbi := op a (op b (i b)))
-- helper function to prove that x * a^-1 = y * a^-1 given x = y
(under_ai (x y : G) (h : eq G x y) := eq_cong G G x y (fun (z : G) => op z (i a)) h)
(under_ai (x y : G) (h : eq G x y) := eq_cong G G x y (fun (z : G) => z * (i a)) h)
in
-- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
-- = (a * (b * b^-1)) * a^-1
-- = (a * e) * a^-1
-- = a * a^-1
-- = e
eq_trans G (op ab biai) (op ab_bi (i a)) e
eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e
-- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
(assoc_g ab (i b) (i a))
(assoc_g (a * b) (i b) (i a))
-- ((a * b) * b^-1) * a^-1 = e
(eq_trans G (op ab_bi (i a)) (op a_bbi (i a)) e
(eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e
-- ((a * b) * b^-1) * a^-1 = (a * (b * b^-1)) * a^-1
(under_ai ab_bi a_bbi (eq_sym G a_bbi ab_bi (assoc_g a b (i b))))
(under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (assoc_g a b (i b))))
-- (a * (b * b^-1)) * a^-1 = e
(eq_trans G (op a_bbi (i a)) (op (op a e) (i a)) e
(eq_trans G (a * (b * i b) * i a) (a * e * i a) e
-- (a * (b * b^-1)) * a^-1 = (a * e) * a^-1
(eq_cong G G (op b (i b)) e (fun (x : G) => (op (op a x) (i a))) (inv_rg b))
(eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (inv_rg b))
-- (a * e) * a^-1 = e
(eq_trans G (op (op a e) (i a)) (op a (i a)) e
(eq_trans G (a * e * i a) (a * i a) e
-- (a * e) * a^-1 = a * a^-1
(under_ai (op a e) a (id_rg a))
(under_ai (a * e) a (id_rg a))
-- a * a^-1 = e
(inv_rg a))))

96
examples/category.pg
View file

@ -2,71 +2,77 @@
section Category
variable
(Obj : *)
(Hom : Obj -> Obj -> *)
(id : forall (A : Obj), Hom A A)
(comp : forall (A B C : Obj), Hom A B -> Hom B C -> Hom A C);
(Obj : ★)
(~> : Obj -> Obj -> ★);
infixr 10 ~>;
variable
(id : forall (A : Obj), A ~> A)
(comp : forall (A B C : Obj), A ~> B -> B ~> C -> A ~> C);
hypothesis
(id_l : forall (A B : Obj) (f : Hom A B), eq (Hom A B) (comp A A B (id A) f) f)
(id_r : forall (A B : Obj) (f : Hom B A), eq (Hom A B) (comp B A A f (id A)) f)
(assoc : forall (A B C D : Obj) (f : Hom A B) (g : Hom B C) (h : Hom C D),
eq (Hom A D)
(id_l : forall (A B : Obj) (f : A ~> B), eq (A ~> B) (comp A A B (id A) f) f)
(id_r : forall (A B : Obj) (f : B ~> A), eq (A ~> B) (comp B A A f (id A)) f)
(assoc : forall (A B C D : Obj) (f : A ~> B) (g : B ~> C) (h : C ~> D),
eq (A ~> D)
(comp A B D f (comp B C D g h))
(comp A C D (comp A B C f g) h));
def initial (A : Obj) := forall (B : Obj), exists_uniq_t (Hom A B);
def terminal (A : Obj) := forall (B : Obj), exists_uniq_t (Hom B A);
def initial (A : Obj) := forall (B : Obj), exists_uniq_t (A ~> B);
def terminal (A : Obj) := forall (B : Obj), exists_uniq_t (B ~> A);
def product (A B C : Obj) (piA : Hom C A) (piB : Hom C B) :=
forall (D : Obj) (f : Hom D A) (g : Hom D B),
exists_uniq (Hom D C) (fun (fxg : Hom D C) =>
and (eq (Hom D A) (comp D C A fxg piA) f)
(eq (Hom D B) (comp D C B fxg piB) g));
def × (A B C : Obj) (piA : C ~> A) (piB : C ~> B) :=
forall (D : Obj) (f : D ~> A) (g : D ~> B),
exists_uniq (D ~> C) (fun (fxg : D ~> C) =>
(eq (D ~> A) (comp D C A fxg piA) f)
∧ (eq (D ~> B) (comp D C B fxg piB) g));
section Inverses
variable
(A B : Obj)
(f : Hom A B)
(g : Hom B A);
(f : A ~> B)
(g : B ~> A);
def inv_l := eq (Hom A A) (comp A B A f g) (id A);
def inv_r := eq (Hom B B) (comp B A B g f) (id B);
def inv_l := eq (A ~> A) (comp A B A f g) (id A);
def inv_r := eq (B ~> B) (comp B A B g f) (id B);
def inv := and inv_l inv_r;
def inv := inv_l ∧ inv_r;
end Inverses
def isomorphic (A B : Obj) :=
exists (Hom A B) (fun (f : Hom A B) =>
exists (Hom B A) (inv A B f));
def ≅ (A B : Obj) :=
exists (A ~> B) (fun (f : A ~> B) =>
exists (B ~> A) (inv A B f));
def initial_uniq (A B : Obj) (hA : initial A) (hB : initial B) : isomorphic A B :=
exists_uniq_t_elim (Hom A B) (isomorphic A B) (hA B) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) =>
exists_uniq_t_elim (Hom B A) (isomorphic A B) (hB A) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) =>
exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) =>
exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) =>
exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f
(exists_intro (Hom B A) (inv A B f) g
infixl 20 ≅;
def initial_uniq (A B : Obj) (hA : initial A) (hB : initial B) : A ≅ B :=
exists_uniq_t_elim (A ~> B) (A ≅ B) (hA B) (fun (f : A ~> B) (f_uniq : forall (y : A ~> B), eq (A ~> B) f y) =>
exists_uniq_t_elim (B ~> A) (A ≅ B) (hB A) (fun (g : B ~> A) (g_uniq : forall (y : B ~> A), eq (B ~> A) g y) =>
exists_uniq_t_elim (A ~> A) (A ≅ B) (hA A) (fun (a : A ~> A) (a_uniq : forall (y : A ~> A), eq (A ~> A) a y) =>
exists_uniq_t_elim (B ~> B) (A ≅ B) (hB B) (fun (b : B ~> B) (b_uniq : forall (y : B ~> B), eq (B ~> B) b y) =>
exists_intro (A ~> B) (fun (f : A ~> B) => exists (B ~> A) (inv A B f)) f
(exists_intro (B ~> A) (inv A B f) g
(and_intro (inv_l A B f g) (inv_r A B f g)
(eq_trans (Hom A A) (comp A B A f g) a (id A)
(eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g)))
(eq_trans (A ~> A) (comp A B A f g) a (id A)
(eq_sym (A ~> A) a (comp A B A f g) (a_uniq (comp A B A f g)))
(a_uniq (id A)))
(eq_trans (Hom B B) (comp B A B g f) b (id B)
(eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f)))
(eq_trans (B ~> B) (comp B A B g f) b (id B)
(eq_sym (B ~> B) b (comp B A B g f) (b_uniq (comp B A B g f)))
(b_uniq (id B)))))))));
def terminal_uniq (A B : Obj) (hA : terminal A) (hB : terminal B) : isomorphic A B :=
exists_uniq_t_elim (Hom A B) (isomorphic A B) (hB A) (fun (f : Hom A B) (f_uniq : forall (y : Hom A B), eq (Hom A B) f y) =>
exists_uniq_t_elim (Hom B A) (isomorphic A B) (hA B) (fun (g : Hom B A) (g_uniq : forall (y : Hom B A), eq (Hom B A) g y) =>
exists_uniq_t_elim (Hom A A) (isomorphic A B) (hA A) (fun (a : Hom A A) (a_uniq : forall (y : Hom A A), eq (Hom A A) a y) =>
exists_uniq_t_elim (Hom B B) (isomorphic A B) (hB B) (fun (b : Hom B B) (b_uniq : forall (y : Hom B B), eq (Hom B B) b y) =>
exists_intro (Hom A B) (fun (f : Hom A B) => exists (Hom B A) (inv A B f)) f
(exists_intro (Hom B A) (inv A B f) g
def terminal_uniq (A B : Obj) (hA : terminal A) (hB : terminal B) : A ≅ B :=
exists_uniq_t_elim (A ~> B) (A ≅ B) (hB A) (fun (f : A ~> B) (f_uniq : forall (y : A ~> B), eq (A ~> B) f y) =>
exists_uniq_t_elim (B ~> A) (A ≅ B) (hA B) (fun (g : B ~> A) (g_uniq : forall (y : B ~> A), eq (B ~> A) g y) =>
exists_uniq_t_elim (A ~> A) (A ≅ B) (hA A) (fun (a : A ~> A) (a_uniq : forall (y : A ~> A), eq (A ~> A) a y) =>
exists_uniq_t_elim (B ~> B) (A ≅ B) (hB B) (fun (b : B ~> B) (b_uniq : forall (y : B ~> B), eq (B ~> B) b y) =>
exists_intro (A ~> B) (fun (f : A ~> B) => exists (B ~> A) (inv A B f)) f
(exists_intro (B ~> A) (inv A B f) g
(and_intro (inv_l A B f g) (inv_r A B f g)
(eq_trans (Hom A A) (comp A B A f g) a (id A)
(eq_sym (Hom A A) a (comp A B A f g) (a_uniq (comp A B A f g)))
(eq_trans (A ~> A) (comp A B A f g) a (id A)
(eq_sym (A ~> A) a (comp A B A f g) (a_uniq (comp A B A f g)))
(a_uniq (id A)))
(eq_trans (Hom B B) (comp B A B g f) b (id B)
(eq_sym (Hom B B) b (comp B A B g f) (b_uniq (comp B A B g f)))
(eq_trans (B ~> B) (comp B A B g f) b (id B)
(eq_sym (B ~> B) b (comp B A B g f) (b_uniq (comp B A B g f)))
(b_uniq (id B)))))))));
end Category

14
examples/classical.pg
View file

@ -2,26 +2,26 @@
-- excluded middle!
-- P ∨ ~P
axiom em (P : *) : or P (not P);
axiom em (P : ★) : P ∨ not P;
-- ~~P => P
def dne (P : *) (nnp : not (not P)) : P :=
def dne (P : ★) (nnp : not (not P)) : P :=
or_elim P (not P) P (em P)
(fun (p : P) => p)
(fun (np : not P) => nnp np P);
-- ((P => Q) => P) => P
def peirce (P Q : *) (h : (P -> Q) -> P) : P :=
def peirce (P Q : ★) (h : (P -> Q) -> P) : P :=
or_elim P (not P) P (em P)
(fun (p : P) => p)
(fun (np : not P) => h (fun (p : P) => np p Q));
-- ~(A ∧ B) => ~A ∨ ~B
def de_morgan4 (A B : *) (h : not (and A B)) : or (not A) (not B) :=
or_elim A (not A) (or (not A) (not B)) (em A)
def de_morgan4 (A B : ★) (h : not (A ∧ B)) : not A ∨ not B :=
or_elim A (not A) (not A ∨ not B) (em A)
(fun (a : A) =>
or_elim B (not B) (or (not A) (not B)) (em B)
(fun (b : B) => h (and_intro A B a b) (or (not A) (not B)))
or_elim B (not B) (not A ∨ not B) (em B)
(fun (b : B) => h (and_intro A B a b) (not A ∨ not B))
(fun (nb : not B) => or_intro_r (not A) (not B) nb))
(fun (na : not A) => or_intro_l (not A) (not B) na);

26
examples/computation.pg
View file

@ -6,19 +6,21 @@
-- the natural number `n` is encoded as the function taking any function
-- `A -> A` and repeating it `n` times
def nat : * := forall (A : *), (A -> A) -> A -> A;
def nat : ★ := forall (A : ★), (A -> A) -> A -> A;
-- zero is the constant function
def zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
def zero : nat := fun (A : ★) (f : A -> A) (x : A) => x;
-- `suc n` composes one more `f` than `n`
def suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
def suc : nat -> nat := fun (n : nat) (A : ★) (f : A -> A) (x : A) => f ((n A f) x);
-- addition can be encoded as usual
def plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
def + : nat -> nat -> nat := fun (n m : nat) (A : ★) (f : A -> A) (x : A) => (m A f) (n A f x);
infixl 20 +;
-- likewise for multiplication
def times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
def * : nat -> nat -> nat := fun (n m : nat) (A : ★) (f : A -> A) (x : A) => (m A (n A f)) x;
infixl 30 *;
-- unforunately, it is impossible to prove induction on Church numerals,
-- which makes it really hard to prove standard theorems, or do anything really.
@ -37,19 +39,25 @@ def eight : nat := suc seven;
def nine : nat := suc eight;
def ten : nat := suc nine;
def = (n m : nat) := eq nat n m;
infixl 1 =;
-- now we can do a bunch of computations, even at the type level
-- the way we can do this is by defining equality (see <examples/logic.pg> for
-- more details on how this works) and proving a bunch of theorems like
-- `plus one one = two` (how exciting!)
-- `one + one = two` (how exciting!)
-- then perga will only accept our proof if `plus one one` and `two` are beta
-- equivalent
-- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a
-- proof that `1 + 1 = 2`
def one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;
def one_plus_one_is_two : one + one = two := eq_refl nat two;
-- we can likewise compute 2 + 2
def two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four;
def two_plus_two_is_four : two + two = four := eq_refl nat four;
-- even multiplication works
def two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten;
def two_times_five_is_ten : two * five = ten := eq_refl nat ten;
-- this is just to kind of show off the parser
def mixed : two + four * two = ten := eq_refl nat ten;

172
examples/logic.pg
View file

@ -1,52 +1,53 @@
-- False
def false : * := forall (A : *), A;
def false : ★ := forall (A : ★), A;
-- no introduction rule
-- elimination rule
def false_elim (A : *) (contra : false) : A := contra A;
def false_elim (A : ★) (contra : false) : A := contra A;
-- --------------------------------------------------------------------------------------------------------------
-- True
def true : * := forall (A : *), A -> A;
def true : ★ := forall (A : ★), A → A;
def true_intro : true := fun (A : *) (x : A) => x;
def true_intro : true := fun (A : ★) (x : A) => x;
-- --------------------------------------------------------------------------------------------------------------
-- Negation
def not (A : *) : * := A -> false;
def not (A : ★) : ★ := A → false;
-- introduction rule (kinda just the definition)
def not_intro (A : *) (h : A -> false) : not A := h;
def not_intro (A : ★) (h : A → false) : not A := h;
-- elimination rule
def not_elim (A B : *) (a : A) (na : not A) : B := na a B;
def not_elim (A B : ★) (a : A) (na : not A) : B := na a B;
-- can introduce double negation (can't eliminate it as that isn't constructive)
def double_neg_intro (A : *) (a : A) : not (not A) :=
def double_neg_intro (A : ★) (a : A) : not (not A) :=
fun (notA : not A) => notA a;
-- --------------------------------------------------------------------------------------------------------------
-- Conjunction
def and (A B : *) : * := forall (C : *), (A -> B -> C) -> C;
def ∧ (A B : ★) : ★ := forall (C : ★), (A → B → C) → C;
infixl 10 ∧;
-- introduction rule
def and_intro (A B : *) (a : A) (b : B) : and A B :=
fun (C : *) (H : A -> B -> C) => H a b;
def and_intro (A B : ★) (a : A) (b : B) : A ∧ B :=
fun (C : ★) (H : A → B → C) => H a b;
-- left elimination rule
def and_elim_l (A B : *) (ab : and A B) : A :=
def and_elim_l (A B : ★) (ab : A ∧ B) : A :=
ab A (fun (a : A) (b : B) => a);
-- right elimination rule
def and_elim_r (A B : *) (ab : and A B) : B :=
def and_elim_r (A B : ★) (ab : A ∧ B) : B :=
ab B (fun (a : A) (b : B) => b);
-- --------------------------------------------------------------------------------------------------------------
@ -54,18 +55,19 @@ def and_elim_r (A B : *) (ab : and A B) : B :=
-- Disjunction
-- 2nd order disjunction
def or (A B : *) : * := forall (C : *), (A -> C) -> (B -> C) -> C;
def ∨ (A B : ★) : ★ := forall (C : ★), (A → C) → (B → C) → C;
infixl 5 ∨;
-- left introduction rule
def or_intro_l (A B : *) (a : A) : or A B :=
fun (C : *) (ha : A -> C) (hb : B -> C) => ha a;
def or_intro_l (A B : ★) (a : A) : A ∨ B :=
fun (C : ★) (ha : A → C) (hb : B → C) => ha a;
-- right introduction rule
def or_intro_r (A B : *) (b : B) : or A B :=
fun (C : *) (ha : A -> C) (hb : B -> C) => hb b;
def or_intro_r (A B : ★) (b : B) : A ∨ B :=
fun (C : ★) (ha : A → C) (hb : B → C) => hb b;
-- elimination rule (kinda just the definition)
def or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
def or_elim (A B C : ★) (ab : A ∨ B) (ha : A → C) (hb : B → C) : C :=
ab C ha hb;
-- --------------------------------------------------------------------------------------------------------------
@ -73,14 +75,14 @@ def or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
-- Existential
-- 2nd order existential
def exists (A : *) (P : A -> *) : * := forall (C : *), (forall (x : A), P x -> C) -> C;
def exists (A : ★) (P : A → ★) : ★ := forall (C : ★), (forall (x : A), P x → C) → C;
-- introduction rule
def exists_intro (A : *) (P : A -> *) (a : A) (h : P a) : exists A P :=
fun (C : *) (g : forall (x : A), P x -> C) => g a h;
def exists_intro (A : ★) (P : A → ★) (a : A) (h : P a) : exists A P :=
fun (C : ★) (g : forall (x : A), P x → C) => g a h;
-- elimination rule (kinda just the definition)
def exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A), P a -> B) : B :=
def exists_elim (A B : ★) (P : A → ★) (ex_a : exists A P) (h : forall (a : A), P a → B) : B :=
ex_a B h;
-- --------------------------------------------------------------------------------------------------------------
@ -88,53 +90,53 @@ def exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A),
-- Universal
-- 2nd order universal (just ∏, including it for completeness)
def all (A : *) (P : A -> *) : * := forall (a : A), P a;
def all (A : ★) (P : A → ★) : ★ := forall (a : A), P a;
-- introduction rule
def all_intro (A : *) (P : A -> *) (h : forall (a : A), P a) : all A P := h;
def all_intro (A : ★) (P : A → ★) (h : forall (a : A), P a) : all A P := h;
-- elimination rule
def all_elim (A : *) (P : A -> *) (h_all : all A P) (a : A) : P a := h_all a;
def all_elim (A : ★) (P : A → ★) (h_all : all A P) (a : A) : P a := h_all a;
-- --------------------------------------------------------------------------------------------------------------
-- Equality
-- 2nd order Leibniz equality
def eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
def eq (A : ★) (x y : A) := forall (P : A → ★), P x → P y;
-- equality is reflexive
def eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
def eq_refl (A : ★) (x : A) : eq A x x := fun (P : A → ★) (Hx : P x) => Hx;
-- equality is symmetric
def eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
def eq_sym (A : ★) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A → ★) (Hy : P y) =>
Hxy (fun (z : A) => P z → P x) (fun (Hx : P x) => Hx) Hy;
-- equality is transitive
def eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
def eq_trans (A : ★) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A → ★) (Hx : P x) =>
Hyz P (Hxy P Hx);
-- equality is a universal congruence
def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
fun (P : B -> *) (Hfx : P (f x)) =>
def eq_cong (A B : ★) (x y : A) (f : A → B) (H : eq A x y) : eq B (f x) (f y) :=
fun (P : B → ★) (Hfx : P (f x)) =>
H (fun (a : A) => P (f a)) Hfx;
-- --------------------------------------------------------------------------------------------------------------
-- unique existence
def exists_uniq (A : *) (P : A -> *) : * :=
exists A (fun (x : A) => and (P x) (forall (y : A), P y -> eq A x y));
def exists_uniq (A : ★) (P : A → ★) : ★ :=
exists A (fun (x : A) => P x ∧ (forall (y : A), P y → eq A x y));
def exists_uniq_elim (A B : *) (P : A -> *) (ex_a : exists_uniq A P) (h : forall (a : A), P a -> (forall (y : A), P y -> eq A a y) -> B) : B :=
exists_elim A B (fun (x : A) => and (P x) (forall (y : A), P y -> eq A x y)) ex_a
(fun (a : A) (h2 : and (P a) (forall (y : A), P y -> eq A a y)) =>
h a (and_elim_l (P a) (forall (y : A), P y -> eq A a y) h2)
(and_elim_r (P a) (forall (y : A), P y -> eq A a y) h2));
def exists_uniq_elim (A B : ★) (P : A → ★) (ex_a : exists_uniq A P) (h : forall (a : A), P a → (forall (y : A), P y → eq A a y) → B) : B :=
exists_elim A B (fun (x : A) => P x ∧ (forall (y : A), P y → eq A x y)) ex_a
(fun (a : A) (h2 : P a ∧ (forall (y : A), P y → eq A a y)) =>
h a (and_elim_l (P a) (forall (y : A), P y → eq A a y) h2)
(and_elim_r (P a) (forall (y : A), P y → eq A a y) h2));
def exists_uniq_t (A : *) : * :=
def exists_uniq_t (A : ★) : ★ :=
exists A (fun (x : A) => forall (y : A), eq A x y);
def exists_uniq_t_elim (A B : *) (ex_a : exists_uniq_t A) (h : forall (a : A), (forall (y : A), eq A a y) -> B) : B :=
def exists_uniq_t_elim (A B : ★) (ex_a : exists_uniq_t A) (h : forall (a : A), (forall (y : A), eq A a y) → B) : B :=
exists_elim A B (fun (x : A) => forall (y : A), eq A x y) ex_a (fun (a : A) (h2 : forall (y : A), eq A a y) => h a h2);
-- --------------------------------------------------------------------------------------------------------------
@ -143,24 +145,24 @@ def exists_uniq_t_elim (A B : *) (ex_a : exists_uniq_t A) (h : forall (a : A), (
section Theorems
variable (A B C : *);
variable (A B C : ★);
-- ~(A ∨ B) => ~A ∧ ~B
def de_morgan1 (h : not (or A B)) : and (not A) (not B) :=
def de_morgan1 (h : not (A ∨ B)) : not A ∧ not B :=
and_intro (not A) (not B)
(fun (a : A) => h (or_intro_l A B a))
(fun (b : B) => h (or_intro_r A B b));
-- ~A ∧ ~B => ~(A ∨ B)
def de_morgan2 (h : and (not A) (not B)) : not (or A B) :=
fun (contra : or A B) =>
def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) :=
fun (contra : A ∨ B) =>
or_elim A B false contra
(and_elim_l (not A) (not B) h)
(and_elim_r (not A) (not B) h);
-- ~A ∨ ~B => ~(A ∧ B)
def de_morgan3 (h : or (not A) (not B)) : not (and A B) :=
fun (contra : and A B) =>
def de_morgan3 (h : not A ∨ not B) : not (A ∧ B) :=
fun (contra : A ∧ B) =>
or_elim (not A) (not B) false h
(fun (na : not A) => na (and_elim_l A B contra))
(fun (nb : not B) => nb (and_elim_r A B contra));
@ -168,80 +170,80 @@ section Theorems
-- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
-- A ∧ B => B ∧ A
def and_comm (h : and A B) : and B A :=
def and_comm (h : A ∧ B) : B ∧ A :=
and_intro B A
(and_elim_r A B h)
(and_elim_l A B h);
-- A ∨ B => B ∨ A
def or_comm (h : or A B) : or B A :=
or_elim A B (or B A) h
def or_comm (h : A ∨ B) : B ∨ A :=
or_elim A B (B ∨ A) h
(fun (a : A) => or_intro_r B A a)
(fun (b : B) => or_intro_l B A b);
-- A ∧ (B ∧ C) => (A ∧ B) ∧ C
def and_assoc_l (h : and A (and B C)) : and (and A B) C :=
let (a := (and_elim_l A (and B C) h))
(bc := (and_elim_r A (and B C) h))
def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C :=
let (a := (and_elim_l A (B ∧ C) h))
(bc := (and_elim_r A (B ∧ C) h))
(b := (and_elim_l B C bc))
(c := (and_elim_r B C bc))
in
and_intro (and A B) C (and_intro A B a b) c
and_intro (A ∧ B) C (and_intro A B a b) c
end;
-- (A ∧ B) ∧ C => A ∧ (B ∧ C)
def and_assoc_r (h : and (and A B) C) : and A (and B C) :=
let (ab := and_elim_l (and A B) C h)
def and_assoc_r (h : (A ∧ B) ∧ C) : A ∧ (B ∧ C) :=
let (ab := and_elim_l (A ∧ B) C h)
(a := and_elim_l A B ab)
(b := and_elim_r A B ab)
(c := and_elim_r (and A B) C h)
(c := and_elim_r (A ∧ B) C h)
in
and_intro A (and B C) a (and_intro B C b c)
and_intro A (B ∧ C) a (and_intro B C b c)
end;
-- A ∨ (B ∨ C) => (A ∨ B) ∨ C
def or_assoc_l (h : or A (or B C)) : or (or A B) C :=
or_elim A (or B C) (or (or A B) C) h
(fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a))
(fun (g : or B C) =>
or_elim B C (or (or A B) C) g
(fun (b : B) => or_intro_l (or A B) C (or_intro_r A B b))
(fun (c : C) => or_intro_r (or A B) C c));
def or_assoc_l (h : A ∨ (B ∨ C)) : (A ∨ B) ∨ C :=
or_elim A (B ∨ C) (A ∨ B ∨ C) h
(fun (a : A) => or_intro_l (A ∨ B) C (or_intro_l A B a))
(fun (g : B ∨ C) =>
or_elim B C (A ∨ B ∨ C) g
(fun (b : B) => or_intro_l (A ∨ B) C (or_intro_r A B b))
(fun (c : C) => or_intro_r (A ∨ B) C c));
-- (A ∨ B) ∨ C => A ∨ (B ∨ C)
def or_assoc_r (h : or (or A B) C) : or A (or B C) :=
or_elim (or A B) C (or A (or B C)) h
(fun (g : or A B) =>
or_elim A B (or A (or B C)) g
(fun (a : A) => or_intro_l A (or B C) a)
(fun (b : B) => or_intro_r A (or B C) (or_intro_l B C b)))
(fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c));
def or_assoc_r (h : (A ∨ B) ∨ C) : A ∨ (B ∨ C) :=
or_elim (A ∨ B) C (A ∨ (B ∨ C)) h
(fun (g : A ∨ B) =>
or_elim A B (A ∨ (B ∨ C)) g
(fun (a : A) => or_intro_l A (B ∨ C) a)
(fun (b : B) => or_intro_r A (B ∨ C) (or_intro_l B C b)))
(fun (c : C) => or_intro_r A (B ∨ C) (or_intro_r B C c));
-- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
def and_distrib_l_or (h : and A (or B C)) : or (and A B) (and A C) :=
or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h)
(fun (b : B) => or_intro_l (and A B) (and A C)
(and_intro A B (and_elim_l A (or B C) h) b))
(fun (c : C) => or_intro_r (and A B) (and A C)
(and_intro A C (and_elim_l A (or B C) h) c));
def and_distrib_l_or (h : A ∧ (B ∨ C)) : A ∧ B ∨ A ∧ C :=
or_elim B C (A ∧ B ∨ A ∧ C) (and_elim_r A (B ∨ C) h)
(fun (b : B) => or_intro_l (A ∧ B) (A ∧ C)
(and_intro A B (and_elim_l A (B ∨ C) h) b))
(fun (c : C) => or_intro_r (A ∧ B) (A ∧ C)
(and_intro A C (and_elim_l A (B ∨ C) h) c));
-- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
def and_factor_l_or (h : or (and A B) (and A C)) : and A (or B C) :=
or_elim (and A B) (and A C) (and A (or B C)) h
(fun (ab : and A B) => and_intro A (or B C)
def and_factor_l_or (h : A ∧ B ∨ A ∧ C) : A ∧ (B ∨ C) :=
or_elim (A ∧ B) (A ∧ C) (A ∧ (B ∨ C)) h
(fun (ab : A ∧ B) => and_intro A (B ∨ C)
(and_elim_l A B ab)
(or_intro_l B C (and_elim_r A B ab)))
(fun (ac : and A C) => and_intro A (or B C)
(fun (ac : A ∧ C) => and_intro A (B ∨ C)
(and_elim_l A C ac)
(or_intro_r B C (and_elim_r A C ac)));
-- Thanks Quinn!
-- A ∨ B => ~B => A
def disj_syllog (nb : not B) (hor : or A B) : A :=
def disj_syllog (nb : not B) (hor : A ∨ B) : A :=
or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
-- (A => B) => ~B => ~A
def contrapositive (f : A -> B) (nb : not B) : not A :=
def contrapositive (f : A → B) (nb : not B) : not A :=
fun (a : A) => nb (f a);
end Theorems

134
examples/peano.pg
View file

@ -12,7 +12,7 @@
-- powerful enough to construct the natural numbers (or at least to prove the
-- Peano axioms as theorems from a definition constructible in perga). However,
-- working with axioms is extremely common in math. As such, perga has a system
-- for doing just that, namely the *axiom* system.
-- for doing just that, namely the ★axiom★ system.
--
-- In a definition, rather than give a value for the term, we can give it the
-- value axiom, in which case a type ascription is mandatory. Perga will then
@ -20,7 +20,7 @@
-- defined is a value of the asserted type. For example, we will use the axiom
-- system to assert the existence of a type of natural numbers
axiom nat : *;
axiom nat : ★;
-- As you can imagine, this can be risky. For instance, there's nothing stopping
-- us from saying
@ -56,7 +56,7 @@ axiom suc_nonzero : forall (n : nat), not (eq nat (suc n) zero);
-- axiom 9: Induction! For any proposition P on natural numbers, if P(0) holds,
-- and if for every natural number n, P(n) ⇒ P(S n), then P holds for all n.
axiom nat_ind : forall (P : nat -> *), P zero -> (forall (n : nat), P n -> P (suc n))
axiom nat_ind : forall (P : nat -> ★), P zero -> (forall (n : nat), P n -> P (suc n))
-> forall (n : nat), P n;
-- }}}
@ -80,7 +80,7 @@ def four : nat := suc three;
def five : nat := suc four;
-- First, the predecessor of n is m if n = suc m.
def pred (n m : nat) : * := eq nat n (suc m);
def pred (n m : nat) : ★ := eq nat n (suc m);
-- Our claim is a disjunction, whose first option is that n = 0.
def szc_l (n : nat) := eq nat n zero;
@ -90,7 +90,7 @@ def szc_r (n : nat) := exists nat (pred n);
-- So the claim we are trying to prove is that either one of the above options
-- holds for every n.
def szc (n : nat) := or (szc_l n) (szc_r n);
def szc (n : nat) := szc_l n ∨ szc_r n;
-- And here's our proof!
def suc_or_zero : forall (n : nat), szc n :=
@ -142,8 +142,8 @@ def suc_or_zero : forall (n : nat), szc n :=
-- more used to perga. As such, I will go into a lot less detail on each of
-- these proofs than in the later sections.
--
-- Here's our game plan. We will define a relation R : nat -> A -> * such that
-- R x y iff for every relation Q : nat -> A -> * satisfying
-- Here's our game plan. We will define a relation R : nat -> A -> ★ such that
-- R x y iff for every relation Q : nat -> A -> ★ satisfying
-- 1) Q 0 z and
-- 2) forall (x : nat) (y : A), Q x y -> Q (suc x) (fS x y),
-- Q x y.
@ -154,30 +154,30 @@ def suc_or_zero : forall (n : nat), szc n :=
section RecursiveDefs
-- First, fix an A, z : A, and fS : nat -> A -> A
variable (A : *) (z : A) (fS : nat -> A -> A);
variable (A : ★) (z : A) (fS : nat -> A -> A);
-- {{{ Defining R
-- Here is condition 1 formally expressed in perga.
def cond1 (Q : nat -> A -> *) := Q zero z;
def cond1 (Q : nat -> A -> ★) := Q zero z;
-- Likewise for condition 2.
def cond2 (Q : nat -> A -> *) :=
def cond2 (Q : nat -> A -> ★) :=
forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
-- From here we can define R.
def rec_rel (x : nat) (y : A) :=
forall (Q : nat -> A -> *), cond1 Q -> cond2 Q -> Q x y;
forall (Q : nat -> A -> ★), cond1 Q -> cond2 Q -> Q x y;
-- }}}
-- {{{ R is total
def total (A B : *) (R : A -> B -> *) := forall (a : A), exists B (R a);
def total (A B : ★) (R : A -> B -> ★) := forall (a : A), exists B (R a);
def rec_rel_cond1 : cond1 rec_rel :=
fun (Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
fun (Q : nat -> A -> ★) (h1 : cond1 Q) (h2 : cond2 Q) => h1;
def rec_rel_cond2 : cond2 rec_rel :=
fun (n : nat) (y : A) (h : rec_rel n y)
(Q : nat -> A -> *) (h1 : cond1 Q) (h2 : cond2 Q) =>
(Q : nat -> A -> ★) (h1 : cond1 Q) (h2 : cond2 Q) =>
h2 n y (h Q h1 h2);
def rec_rel_total : total nat A rec_rel :=
@ -194,18 +194,18 @@ def rec_rel_total : total nat A rec_rel :=
-- {{{ Defining R2
def alt_cond1 (x : nat) (y : A) :=
and (eq nat x zero) (eq A y z);
eq nat x zero ∧ eq A y z;
def cond_y2 (x : nat) (y : A)
(x2 : nat) (y2 : A) :=
and (eq A y (fS x2 y2)) (rec_rel x2 y2);
(eq A y (fS x2 y2)) ∧ (rec_rel x2 y2);
def cond_x2 (x : nat) (y : A) (x2 : nat) :=
and (pred x x2) (exists A (cond_y2 x y x2));
pred x x2 ∧ exists A (cond_y2 x y x2);
def alt_cond2 (x : nat) (y : A) := exists nat (cond_x2 x y);
def rec_rel_alt (x : nat) (y : A) := or (alt_cond1 x y) (alt_cond2 x y);
def rec_rel_alt (x : nat) (y : A) := alt_cond1 x y ∨ alt_cond2 x y;
-- }}}
-- {{{ R = R2
@ -282,10 +282,10 @@ def R_sub_R2 (x : nat) (y : A) : rec_rel x y -> rec_rel_alt x y :=
-- {{{ R2 (hence R) is functional
def fl_in (A B : *) (R : A -> B -> *) (x : A) := forall (y1 y2 : B),
def fl_in (A B : ★) (R : A -> B -> ★) (x : A) := forall (y1 y2 : B),
R x y1 -> R x y2 -> eq B y1 y2;
def fl (A B : *) (R : A -> B -> *) := forall (x : A), fl_in A B R x;
def fl (A B : ★) (R : A -> B -> ★) := forall (x : A), fl_in A B R x;
def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
let (cx2 := cond_x2 zero y)
@ -382,7 +382,7 @@ def rec_def (x : nat) : A :=
-- existential, it still satisfies the property it definitionally is supposed
-- to satisfy. This annoying problem would be subverted with proper Σ-types,
-- provided they had η-equality.
axiom definite_description (A : *) (P : A -> *) (h : exists A P) :
axiom definite_description (A : ★) (P : A -> ★) (h : exists A P) :
P (exists_elim A A P h (fun (x : A) (_ : P x) => x));
-- Now we can use this axiom to prove that R n (rec_def n).
@ -440,27 +440,31 @@ def psuc (_ r : nat) := suc r;
-- And here's plus!
def plus (n : nat) : nat -> nat := rec_def nat n psuc;
-- And here's an infix version of it
def + (n m : nat) : nat := plus n m;
infixl 20 +;
-- The first equation manifests itself as the familiar
-- n + 0 = 0.
def plus_0_r (n : nat) : eq nat (plus n zero) n :=
def plus_0_r (n : nat) : eq nat (n + zero) n :=
rec_def_sat_zero nat n psuc;
-- The second equation, after a bit of massaging, manifests itself as the
-- likewise familiar
-- n + suc m = suc (n + m).
def plus_s_r (n m : nat) : eq nat (plus n (suc m)) (suc (plus n m)) :=
def plus_s_r (n m : nat) : eq nat (n + suc m) (suc (n + m)) :=
rec_def_sat_suc nat n psuc m;
-- -- We can now prove 1 + 1 = 2!
def one_plus_one_two : eq nat (plus one one) two :=
def one_plus_one_two : eq nat (one + one) two :=
-- 1 + (suc zero) = suc (1 + zero) = suc one
eq_trans nat (plus one one) (suc (plus one zero)) two
eq_trans nat (one + one) (suc (one + zero)) two
-- 1 + (suc zero) = suc (1 + zero)
(plus_s_r one zero)
-- suc (1 + zero) = suc one
(eq_cong nat nat (plus one zero) one suc (plus_0_r one));
(eq_cong nat nat (one + zero) one suc (plus_0_r one));
-- We have successfully defined addition! Note that evaluating 1 + 1 to 2
-- requires a proof, unfortunately, since this computation isn't visible to
@ -469,133 +473,133 @@ def one_plus_one_two : eq nat (plus one one) two :=
-- We will now prove a couple standard properties of addition.
-- First, associativity, namely that n + (m + p) = (n + m) + p.
def plus_assoc : forall (n m p : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)
def plus_assoc : forall (n m p : nat), eq nat (n + (m + p)) (n + m + p)
:= fun (n m : nat) =>
-- We prove this via induction on p for any fixed n and m.
nat_ind
(fun (p : nat) => eq nat (plus n (plus m p)) (plus (plus n m) p))
(fun (p : nat) => eq nat (n + (m + p)) (n + m + p))
-- Base case: p = 0
-- WTS n + (m + 0) = (n + m) + 0
-- n + (m + 0) = n + m = (n + m) + 0
(eq_trans nat (plus n (plus m zero)) (plus n m) (plus (plus n m) zero)
(eq_trans nat (n + (m + zero)) (n + m) (n + m + zero)
-- n + (m + 0) = n + m
(eq_cong nat nat (plus m zero) m (fun (p : nat) => plus n p) (plus_0_r m))
(eq_cong nat nat (m + zero) m (fun (p : nat) => n + p) (plus_0_r m))
-- n + m = (n + m) + 0
(eq_sym nat (plus (plus n m) zero) (plus n m) (plus_0_r (plus n m))))
(eq_sym nat (n + m + zero) (n + m) (plus_0_r (n + m))))
-- Inductive step: IH = n + (m + p) = (n + m) + p
(fun (p : nat) (IH : eq nat (plus n (plus m p)) (plus (plus n m) p)) =>
(fun (p : nat) (IH : eq nat (n + (m + p)) (n + m + p)) =>
-- WTS n + (m + suc p) = (n + m) + suc p
-- n + (m + suc p) = n + suc (m + p)
-- = suc (n + (m + p))
-- = suc ((n + m) + p)
-- = (n + m) + suc p
eq_trans nat (plus n (plus m (suc p))) (plus n (suc (plus m p))) (plus (plus n m) (suc p))
eq_trans nat (n + (m + suc p)) (n + (suc (m + p))) (n + m + suc p)
-- n + (m + suc p) = n + suc (m + p)
(eq_cong nat nat (plus m (suc p)) (suc (plus m p)) (fun (a : nat) => (plus n a)) (plus_s_r m p))
(eq_cong nat nat (m + suc p) (suc (m + p)) (fun (a : nat) => (n + a)) (plus_s_r m p))
-- n + suc (m + p) = (n + m) + suc p
(eq_trans nat (plus n (suc (plus m p))) (suc (plus n (plus m p))) (plus (plus n m) (suc p))
(eq_trans nat (n + suc (m + p)) (suc (n + (m + p))) (n + m + suc p)
-- n + suc (m + p) = suc (n + (m + p))
(plus_s_r n (plus m p))
(plus_s_r n (m + p))
-- suc (n + (m + p)) = (n + m) + suc p
(eq_trans nat (suc (plus n (plus m p))) (suc (plus (plus n m) p)) (plus (plus n m) (suc p))
(eq_trans nat (suc (n + (m + p))) (suc (n + m + p)) (n + m + suc p)
-- suc (n + (m + p)) = suc ((n + m) + p)
(eq_cong nat nat (plus n (plus m p)) (plus (plus n m) p) suc IH)
(eq_cong nat nat (n + (m + p)) (n + m + p) suc IH)
-- suc ((n + m) + p) = (n + m) + suc p
(eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p))
(plus_s_r (plus n m) p)))));
(eq_sym nat (n + m + suc p) (suc (n + m + p))
(plus_s_r (n + m) p)))));
-- Up next is commutativity, but we will need a couple lemmas first.
-- First, we will show that 0 + n = n.
def plus_0_l : forall (n : nat), eq nat (plus zero n) n :=
def plus_0_l : forall (n : nat), eq nat (zero + n) n :=
-- We prove this by induction on n.
nat_ind (fun (n : nat) => eq nat (plus zero n) n)
nat_ind (fun (n : nat) => eq nat (zero + n) n)
-- base case: WTS 0 + 0 = 0
-- This is just plus_0_r 0
(plus_0_r zero)
-- inductive case
(fun (n : nat) (IH : eq nat (plus zero n) n) =>
(fun (n : nat) (IH : eq nat (zero + n) n) =>
-- WTS 0 + (suc n) = suc n
-- 0 + (suc n) = suc (0 + n) = suc n
eq_trans nat (plus zero (suc n)) (suc (plus zero n)) (suc n)
eq_trans nat (zero + suc n) (suc (zero + n)) (suc n)
-- 0 + (suc n) = suc (0 + n)
(plus_s_r zero n)
-- suc (0 + n) = suc n
(eq_cong nat nat (plus zero n) n suc IH));
(eq_cong nat nat (zero + n) n suc IH));
-- Next, we will show that (suc n) + m = suc (n + m).
def plus_s_l (n : nat) : forall (m : nat), eq nat (plus (suc n) m) (suc (plus n m)) :=
def plus_s_l (n : nat) : forall (m : nat), eq nat (suc n + m) (suc (n + m)) :=
-- We proceed by induction on m.
nat_ind (fun (m : nat) => eq nat (plus (suc n) m) (suc (plus n m)))
nat_ind (fun (m : nat) => eq nat (suc n + m) (suc (n + m)))
-- base case: (suc n) + 0 = suc (n + 0)
-- (suc n) + 0 = suc n = suc (n + 0)
(eq_trans nat (plus (suc n) zero) (suc n) (suc (plus n zero))
(eq_trans nat (suc n + zero) (suc n) (suc (n + zero))
-- (suc n) + 0 = suc n
(plus_0_r (suc n))
-- suc n = suc (n + 0)
(eq_cong nat nat n (plus n zero) suc
(eq_cong nat nat n (n + zero) suc
-- n = n + 0
(eq_sym nat (plus n zero) n (plus_0_r n))))
(eq_sym nat (n + zero) n (plus_0_r n))))
-- inductive case
-- IH = suc n + m = suc (n + m)
(fun (m : nat) (IH : eq nat (plus (suc n) m) (suc (plus n m))) =>
(fun (m : nat) (IH : eq nat (suc n + m) (suc (n + m))) =>
-- WTS suc n + suc m = suc (n + suc m)
-- suc n + suc m = suc (suc n + m)
-- = suc (suc (n + m))
-- = suc (n + suc m)
(eq_trans nat (plus (suc n) (suc m)) (suc (plus (suc n) m)) (suc (plus n (suc m)))
(eq_trans nat (suc n + suc m) (suc (suc n + m)) (suc (n + suc m))
-- suc n + suc m = suc (suc n + m)
(plus_s_r (suc n) m)
-- suc (suc n + m) = suc (n + suc m)
(eq_trans nat (suc (plus (suc n) m)) (suc (suc (plus n m))) (suc (plus n (suc m)))
(eq_trans nat (suc (suc n + m)) (suc (suc (n + m))) (suc (n + suc m))
-- suc (suc n + m) = suc (suc (n + m))
(eq_cong nat nat (plus (suc n) m) (suc (plus n m)) suc IH)
(eq_cong nat nat (suc n + m) (suc (n + m)) suc IH)
-- suc (suc (n + m)) = suc (n + suc m)
(eq_cong nat nat (suc (plus n m)) (plus n (suc m)) suc
(eq_cong nat nat (suc (n + m)) (n + suc m) suc
-- suc (n + m) = n + suc m
(eq_sym nat (plus n (suc m)) (suc (plus n m)) (plus_s_r n m))))));
(eq_sym nat (n + suc m) (suc (n + m)) (plus_s_r n m))))));
-- Finally, we can prove commutativity.
def plus_comm (n : nat) : forall (m : nat), eq nat (plus n m) (plus m n) :=
def plus_comm (n : nat) : forall (m : nat), eq nat (n + m) (m + n) :=
-- As usual, we proceed by induction.
nat_ind (fun (m : nat) => eq nat (plus n m) (plus m n))
nat_ind (fun (m : nat) => eq nat (n + m) (m + n))
-- Base case: WTS n + 0 = 0 + n
-- n + 0 = n = 0 + n
(eq_trans nat (plus n zero) n (plus zero n)
(eq_trans nat (n + zero) n (zero + n)
-- n + 0 = n
(plus_0_r n)
-- n = 0 + n
(eq_sym nat (plus zero n) n (plus_0_l n)))
(eq_sym nat (zero + n) n (plus_0_l n)))
-- Inductive step:
(fun (m : nat) (IH : eq nat (plus n m) (plus m n)) =>
(fun (m : nat) (IH : eq nat (n + m) (m + n)) =>
-- WTS n + suc m = suc m + n
-- n + suc m = suc (n + m)
-- = suc (m + n)
-- = suc m + n
(eq_trans nat (plus n (suc m)) (suc (plus n m)) (plus (suc m) n)
(eq_trans nat (n + suc m) (suc (n + m)) (suc m + n)
-- n + suc m = suc (n + m)
(plus_s_r n m)
-- suc (n + m) = suc m + n
(eq_trans nat (suc (plus n m)) (suc (plus m n)) (plus (suc m) n)
(eq_trans nat (suc (n + m)) (suc (m + n)) (suc m + n)
-- suc (n + m) = suc (m + n)
(eq_cong nat nat (plus n m) (plus m n) suc IH)
(eq_cong nat nat (n + m) (m + n) suc IH)
-- suc (m + n) = suc m + n
(eq_sym nat (plus (suc m) n) (suc (plus m n)) (plus_s_l m n)))));
(eq_sym nat (suc m + n) (suc (m + n)) (plus_s_l m n)))));

89
lib/Parser.hs
View file

@ -5,18 +5,26 @@ module Parser where
import Control.Monad.Combinators (option)
import Control.Monad.Except
import Data.List (foldl, foldl1)
import qualified Data.Map.Strict as M
import qualified Data.Text as T
import Errors (Error (..))
import IR
import Preprocessor
import Text.Megaparsec (MonadParsec (..), Parsec, ShowErrorComponent (..), between, choice, errorBundlePretty, label, runParser, try)
import Text.Megaparsec (MonadParsec (..), ParsecT, ShowErrorComponent (..), between, choice, errorBundlePretty, label, runParserT, try)
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
newtype TypeError = TE Error
deriving (Eq, Ord)
type Parser = Parsec TypeError Text
data Fixity
= InfixL Int
| InfixR Int
deriving (Eq, Show)
type Operators = Map Text Fixity
type Parser = ParsecT TypeError Text (State Operators)
instance ShowErrorComponent TypeError where
showErrorComponent (TE e) = toString e
@ -34,6 +42,9 @@ lexeme = L.lexeme skipSpace
symbol :: Text -> Parser ()
symbol = void . L.symbol skipSpace
symbols :: String
symbols = "!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅"
pKeyword :: Text -> Parser ()
pKeyword keyword = void $ lexeme (string keyword <* notFollowedBy alphaNumChar)
@ -46,21 +57,24 @@ pIdentifier = try $ label "identifier" $ lexeme $ do
guard $ ident `notElem` keywords
pure ident
pSymbol :: Parser Text
pSymbol = lexeme $ takeWhile1P (Just "symbol") (`elem` symbols)
pVar :: Parser IRExpr
pVar = label "variable" $ lexeme $ Var <$> pIdentifier
pParamGroup :: Parser [Param]
pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
idents <- some pIdentifier
pParamGroup :: Parser Text -> Parser [Param]
pParamGroup ident = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
idents <- some ident
symbol ":"
ty <- pIRExpr
pure $ map (,ty) idents
pSomeParams :: Parser [Param]
pSomeParams = lexeme $ concat <$> some pParamGroup
pSomeParams :: Parser Text -> Parser [Param]
pSomeParams ident = lexeme $ concat <$> some (pParamGroup ident)
pManyParams :: Parser [Param]
pManyParams = lexeme $ concat <$> many pParamGroup
pManyParams :: Parser Text -> Parser [Param]
pManyParams ident = lexeme $ concat <$> many (pParamGroup ident)
mkAbs :: Maybe IRExpr -> (Text, IRExpr) -> IRExpr -> IRExpr
mkAbs ascription (param, typ) = Abs param typ ascription
@ -71,7 +85,7 @@ mkPi ascription (param, typ) = Pi param typ ascription
pLAbs :: Parser IRExpr
pLAbs = lexeme $ label "λ-abstraction" $ do
_ <- pKeyword "fun" <|> symbol "λ"
params <- pSomeParams
params <- pSomeParams pIdentifier
ascription <- optional pAscription
_ <- symbol "=>" <|> symbol "⇒"
body <- pIRExpr
@ -80,7 +94,7 @@ pLAbs = lexeme $ label "λ-abstraction" $ do
pPAbs :: Parser IRExpr
pPAbs = lexeme $ label "Π-abstraction" $ do
_ <- pKeyword "forall" <|> symbol "∏" <|> symbol "∀"
params <- pSomeParams
params <- pSomeParams pIdentifier
ascription <- optional pAscription
symbol ","
body <- pIRExpr
@ -90,7 +104,7 @@ pBinding :: Parser (Text, Maybe IRExpr, IRExpr)
pBinding = lexeme $ label "binding" $ do
symbol "("
ident <- pIdentifier
params <- pManyParams
params <- pManyParams pIdentifier
ascription <- optional pAscription
symbol ":="
value <- pIRExpr
@ -117,7 +131,7 @@ pApp :: Parser IRExpr
pApp = lexeme $ foldl1 App <$> some pTerm
pStar :: Parser IRExpr
pStar = lexeme $ Star <$ symbol "*"
pStar = lexeme $ Star <$ symbol "★"
subscriptDigit :: Parser Integer
subscriptDigit =
@ -146,8 +160,31 @@ pSort = lexeme $ pStar <|> pSquare
pTerm :: Parser IRExpr
pTerm = lexeme $ label "term" $ choice [pSort, pVar, between (char '(') (char ')') pIRExpr]
pInfix :: Parser IRExpr
pInfix = parseWithPrec 0
where
parseWithPrec :: Int -> Parser IRExpr
parseWithPrec prec = pApp >>= continue prec
continue :: Int -> IRExpr -> Parser IRExpr
continue prec lhs = option lhs $ do
op <- lookAhead pSymbol
operators <- get
case M.lookup op operators of
Just fixity -> do
let (opPrec, nextPrec) = case fixity of
InfixL p -> (p, p)
InfixR p -> (p, p + 1)
if opPrec <= prec
then pure lhs
else do
_ <- pSymbol
rhs <- parseWithPrec nextPrec
continue prec (App (App (Var op) lhs) rhs)
Nothing -> fail $ "unknown operator '" ++ toString op ++ "'"
pAppTerm :: Parser IRExpr
pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp]
pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pInfix]
pIRExpr :: Parser IRExpr
pIRExpr = lexeme $ do
@ -161,7 +198,7 @@ pAxiom :: Parser IRDef
pAxiom = lexeme $ label "axiom" $ do
pKeyword "axiom"
ident <- pIdentifier
params <- pManyParams
params <- pManyParams (pIdentifier <|> pSymbol)
ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
symbol ";"
pure $ Axiom ident ascription
@ -169,21 +206,33 @@ pAxiom = lexeme $ label "axiom" $ do
pVariable :: Parser [IRSectionDef]
pVariable = lexeme $ label "variable declaration" $ do
pKeyword "variable" <|> pKeyword "hypothesis"
vars <- pManyParams
vars <- pManyParams (pIdentifier <|> pSymbol)
symbol ";"
pure $ uncurry Variable <$> vars
pDef :: Parser IRDef
pDef = lexeme $ label "definition" $ do
pKeyword "def"
ident <- pIdentifier
params <- pManyParams
ident <- pIdentifier <|> pSymbol
params <- pManyParams pIdentifier
ascription <- fmap (flip (foldr (mkPi Nothing)) params) <$> optional pAscription
symbol ":="
body <- pIRExpr
symbol ";"
pure $ Def ident ascription $ foldr (mkAbs Nothing) body params
pFixityDec :: Parser ()
pFixityDec = do
_ <- string "infix"
fixity <-
choice
[ InfixL <$> (lexeme (char 'l') >> lexeme L.decimal)
, InfixR <$> (lexeme (char 'r') >> lexeme L.decimal)
]
ident <- pSymbol
modify (M.insert ident fixity)
symbol ";"
pSection :: Parser IRSectionDef
pSection = lexeme $ label "section" $ do
pKeyword "section"
@ -194,13 +243,13 @@ pSection = lexeme $ label "section" $ do
pure $ Section secLabel body
pIRDef :: Parser [IRSectionDef]
pIRDef = (pure . IRDef <$> pAxiom) <|> (pure . IRDef <$> pDef) <|> pVariable <|> (pure <$> pSection)
pIRDef = (pure . IRDef <$> pAxiom) <|> (pure . IRDef <$> pDef) <|> pVariable <|> (pure <$> pSection) <|> ([] <$ pFixityDec)
pIRProgram :: Parser IRProgram
pIRProgram = skipSpace >> concat <$> some pIRDef
parserWrapper :: Parser a -> String -> Text -> Either String a
parserWrapper p filename input = first errorBundlePretty $ runParser p filename input
parserWrapper p filename input = first errorBundlePretty $ evalState (runParserT p filename input) M.empty
parseProgram :: String -> Text -> Either String IRProgram
parseProgram = parserWrapper pIRProgram