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 -- I'd always strongly recommend including the type ascriptions for theorems
-- Fix some set A -- Fix some set A
variable (A : *); variable (A : ★);
-- a unary operation is a function `A -> A` -- a unary operation is a function `A → A`
def unop := A -> A; def unop := A → A;
-- a binary operation is a function `A -> A -> A` -- a binary operation is a function `A → A → A`
def binop := A -> A -> A; def binop := A → A → A;
-- fix some binary operation `op` -- fix some binary operation `op`
variable (op : binop); variable (* : binop);
infixl 20 *;
-- it is associative if ... -- 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` -- fix some element `e`
variable (e : A); variable (e : A);
-- it is a left identity with respect to binop `op` if `∀ a, e * a = 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 -- 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 -- 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` -- b is a left inverse for a if `b * a = e`
-- NOTE: we don't require `e` to be an identity in this definition. -- NOTE: we don't require `e` to be an identity in this definition.
-- this definition is purely for convenience's sake -- 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 -- 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 -- 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 end BasicDefinitions
@ -59,15 +61,21 @@ end BasicDefinitions
-- -------------------------------------------------------------------------------------------------------------- -- --------------------------------------------------------------------------------------------------------------
-- a set `S` with binary operation `op` is a semigroup if its operation is associative -- 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 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 -- 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); hypothesis (Hmonoid : monoid);
-- some "getters" for `monoid` so we don't have to do a bunch of very verbose -- 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 := def monoid_id_l_implies_identity (a : M) (H : id_l M op a) : eq M a e :=
-- WTS a = a * e = e -- WTS a = a * e = e
-- we can use `eq_trans` to glue proofs of `a = a * e` and `a * e = e` together -- 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 -- 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` -- now the goal is to show `a * e = a`, which follows immediately from `id_r`
(id_rm a)) (id_rm a))
@ -100,10 +108,10 @@ section Monoid
-- the analogous result for right identities -- the analogous result for right identities
def monoid_id_r_implies_identity (a : M) (H : id_r M op a) : eq M a e := 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` -- 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` -- 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` -- this time, it immediately follows from `id_l`
(id_lm a)) (id_lm a))
@ -114,12 +122,15 @@ end Monoid
section Group 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 -- 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); hypothesis (Hgroup : group);
@ -141,23 +152,23 @@ section Group
-- = (b * a) * a^-1 -- = (b * a) * a^-1
-- = e * a^-1 -- = e * a^-1
-- = a^-1 -- = a^-1
eq_trans G b (op b e) (i a) eq_trans G b (b * e) (i a)
-- b = b * e -- 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 -- 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) --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 -- 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 -- 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 -- b * (a * a^-1) = (b * a) * a^-1
(assoc_g b a (i a)) (assoc_g b a (i a))
-- (b * a) * a^-1 = a^-1 -- (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 -- (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 -- e * a^-1 = a^-1
(id_lg (i a))))); (id_lg (i a)))));
@ -168,66 +179,60 @@ section Group
-- = a^-1 * (a * b) -- = a^-1 * (a * b)
-- = a^-1 * e -- = a^-1 * e
-- = a^-1 -- = a^-1
eq_trans G b (op e b) (i a) eq_trans G b (e * b) (i a)
-- b = e * b -- 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 -- 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 -- 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) -- 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 -- (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) -- (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 -- 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 -- 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 -- a^-1 * e = a^-1
(id_rg (i a))))); (id_rg (i a)))));
-- the classic shoes and socks theorem, namely that (a * b)^-1 = b^-1 * a^-1 -- 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)) := def shoes_and_socks (a b : G) : eq G (i (a * b)) (i b * i a) :=
eq_sym G (op (i b) (i a)) (i (op a b)) eq_sym G (i b * i a) (i (a * b))
(right_inv_unique (op a b) (op (i b) (i a)) (right_inv_unique (a * b) (i b * i a)
-- WTS: (a * b) * (b^-1 * a^-1) = e -- WTS: (a * b) * (b^-1 * a^-1) = e
(let (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 -- 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 in
-- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1 -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
-- = (a * (b * b^-1)) * a^-1 -- = (a * (b * b^-1)) * a^-1
-- = (a * e) * a^-1 -- = (a * e) * a^-1
-- = a * a^-1 -- = a * a^-1
-- = e -- = 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 -- (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 -- ((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 -- ((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 -- (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 -- (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 -- (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 -- (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 -- a * a^-1 = e
(inv_rg a)))) (inv_rg a))))

96
examples/category.pg
View file

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

14
examples/classical.pg
View file

@ -2,26 +2,26 @@
-- excluded middle! -- excluded middle!
-- P ∨ ~P -- P ∨ ~P
axiom em (P : *) : or P (not P); axiom em (P : ★) : P ∨ not P;
-- ~~P => 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) or_elim P (not P) P (em P)
(fun (p : P) => p) (fun (p : P) => p)
(fun (np : not P) => nnp np P); (fun (np : not P) => nnp np P);
-- ((P => Q) => P) => 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) or_elim P (not P) P (em P)
(fun (p : P) => p) (fun (p : P) => p)
(fun (np : not P) => h (fun (p : P) => np p Q)); (fun (np : not P) => h (fun (p : P) => np p Q));
-- ~(A ∧ B) => ~A ∨ ~B -- ~(A ∧ B) => ~A ∨ ~B
def de_morgan4 (A B : *) (h : not (and A B)) : or (not A) (not B) := def de_morgan4 (A B : ★) (h : not (A ∧ B)) : not A ∨ not B :=
or_elim A (not A) (or (not A) (not B)) (em A) or_elim A (not A) (not A ∨ not B) (em A)
(fun (a : A) => (fun (a : A) =>
or_elim B (not B) (or (not A) (not B)) (em B) or_elim B (not B) (not A ∨ not B) (em B)
(fun (b : B) => h (and_intro A B a b) (or (not A) (not 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 (nb : not B) => or_intro_r (not A) (not B) nb))
(fun (na : not A) => or_intro_l (not A) (not B) na); (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 -- the natural number `n` is encoded as the function taking any function
-- `A -> A` and repeating it `n` times -- `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 -- 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` -- `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 -- 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 -- 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, -- unforunately, it is impossible to prove induction on Church numerals,
-- which makes it really hard to prove standard theorems, or do anything really. -- 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 nine : nat := suc eight;
def ten : nat := suc nine; 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 -- 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 -- 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 -- 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 -- then perga will only accept our proof if `plus one one` and `two` are beta
-- equivalent -- equivalent
-- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a -- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a
-- proof that `1 + 1 = 2` -- 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 -- 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 -- 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 -- False
def false : * := forall (A : *), A; def false : ★ := forall (A : ★), A;
-- no introduction rule -- no introduction rule
-- elimination rule -- elimination rule
def false_elim (A : *) (contra : false) : A := contra A; def false_elim (A : ★) (contra : false) : A := contra A;
-- -------------------------------------------------------------------------------------------------------------- -- --------------------------------------------------------------------------------------------------------------
-- True -- 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 -- Negation
def not (A : *) : * := A -> false; def not (A : ★) : ★ := A → false;
-- introduction rule (kinda just the definition) -- 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 -- 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) -- 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; fun (notA : not A) => notA a;
-- -------------------------------------------------------------------------------------------------------------- -- --------------------------------------------------------------------------------------------------------------
-- Conjunction -- Conjunction
def and (A B : *) : * := forall (C : *), (A -> B -> C) -> C; def ∧ (A B : ★) : ★ := forall (C : ★), (A → B → C) → C;
infixl 10 ∧;
-- introduction rule -- introduction rule
def and_intro (A B : *) (a : A) (b : B) : and A B := def and_intro (A B : ★) (a : A) (b : B) : A ∧ B :=
fun (C : *) (H : A -> B -> C) => H a b; fun (C : ★) (H : A → B → C) => H a b;
-- left elimination rule -- 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); ab A (fun (a : A) (b : B) => a);
-- right elimination rule -- 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); ab B (fun (a : A) (b : B) => b);
-- -------------------------------------------------------------------------------------------------------------- -- --------------------------------------------------------------------------------------------------------------
@ -54,18 +55,19 @@ def and_elim_r (A B : *) (ab : and A B) : B :=
-- Disjunction -- Disjunction
-- 2nd order 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 -- left introduction rule
def or_intro_l (A B : *) (a : A) : or A B := def or_intro_l (A B : ★) (a : A) : A ∨ B :=
fun (C : *) (ha : A -> C) (hb : B -> C) => ha a; fun (C : ★) (ha : A → C) (hb : B → C) => ha a;
-- right introduction rule -- right introduction rule
def or_intro_r (A B : *) (b : B) : or A B := def or_intro_r (A B : ★) (b : B) : A ∨ B :=
fun (C : *) (ha : A -> C) (hb : B -> C) => hb b; fun (C : ★) (ha : A → C) (hb : B → C) => hb b;
-- elimination rule (kinda just the definition) -- 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; 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 -- Existential
-- 2nd order 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 -- introduction rule
def exists_intro (A : *) (P : A -> *) (a : A) (h : P a) : exists A P := 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; fun (C : ★) (g : forall (x : A), P x → C) => g a h;
-- elimination rule (kinda just the definition) -- 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; 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 -- Universal
-- 2nd order universal (just ∏, including it for completeness) -- 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 -- 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 -- 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 -- Equality
-- 2nd order Leibniz 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 -- 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 -- 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) => 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; Hxy (fun (z : A) => P z → P x) (fun (Hx : P x) => Hx) Hy;
-- equality is transitive -- 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); Hyz P (Hxy P Hx);
-- equality is a universal congruence -- 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) := 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)) => fun (P : B → ★) (Hfx : P (f x)) =>
H (fun (a : A) => P (f a)) Hfx; H (fun (a : A) => P (f a)) Hfx;
-- -------------------------------------------------------------------------------------------------------------- -- --------------------------------------------------------------------------------------------------------------
-- unique existence -- unique existence
def exists_uniq (A : *) (P : A -> *) : * := def exists_uniq (A : ★) (P : A → ★) : ★ :=
exists A (fun (x : A) => and (P x) (forall (y : A), P y -> eq A x y)); 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 := 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 exists_elim A B (fun (x : A) => 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)) => (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) 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)); (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); 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); 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 section Theorems
variable (A B C : *); variable (A B C : ★);
-- ~(A ∨ B) => ~A ∧ ~B -- ~(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) and_intro (not A) (not B)
(fun (a : A) => h (or_intro_l A B a)) (fun (a : A) => h (or_intro_l A B a))
(fun (b : B) => h (or_intro_r A B b)); (fun (b : B) => h (or_intro_r A B b));
-- ~A ∧ ~B => ~(A ∨ B) -- ~A ∧ ~B => ~(A ∨ B)
def de_morgan2 (h : and (not A) (not B)) : not (or A B) := def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) :=
fun (contra : or A B) => fun (contra : A ∨ B) =>
or_elim A B false contra or_elim A B false contra
(and_elim_l (not A) (not B) h) (and_elim_l (not A) (not B) h)
(and_elim_r (not A) (not B) h); (and_elim_r (not A) (not B) h);
-- ~A ∨ ~B => ~(A ∧ B) -- ~A ∨ ~B => ~(A ∧ B)
def de_morgan3 (h : or (not A) (not B)) : not (and A B) := def de_morgan3 (h : not A ∨ not B) : not (A ∧ B) :=
fun (contra : and A B) => fun (contra : A ∧ B) =>
or_elim (not A) (not B) false h or_elim (not A) (not B) false h
(fun (na : not A) => na (and_elim_l A B contra)) (fun (na : not A) => na (and_elim_l A B contra))
(fun (nb : not B) => nb (and_elim_r 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 -- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively
-- A ∧ B => B ∧ A -- 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_intro B A
(and_elim_r A B h) (and_elim_r A B h)
(and_elim_l A B h); (and_elim_l A B h);
-- A ∨ B => B ∨ A -- A ∨ B => B ∨ A
def or_comm (h : or A B) : or B A := def or_comm (h : A ∨ B) : B ∨ A :=
or_elim A B (or B A) h or_elim A B (B ∨ A) h
(fun (a : A) => or_intro_r B A a) (fun (a : A) => or_intro_r B A a)
(fun (b : B) => or_intro_l B A b); (fun (b : B) => or_intro_l B A b);
-- A ∧ (B ∧ C) => (A ∧ B) ∧ C -- A ∧ (B ∧ C) => (A ∧ B) ∧ C
def and_assoc_l (h : and A (and B C)) : and (and A B) C := def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C :=
let (a := (and_elim_l A (and B C) h)) let (a := (and_elim_l A (B ∧ C) h))
(bc := (and_elim_r A (and B C) h)) (bc := (and_elim_r A (B ∧ C) h))
(b := (and_elim_l B C bc)) (b := (and_elim_l B C bc))
(c := (and_elim_r B C bc)) (c := (and_elim_r B C bc))
in 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; end;
-- (A ∧ B) ∧ C => A ∧ (B ∧ C) -- (A ∧ B) ∧ C => A ∧ (B ∧ C)
def and_assoc_r (h : and (and A B) C) : and A (and B C) := def and_assoc_r (h : (A ∧ B) ∧ C) : A ∧ (B ∧ C) :=
let (ab := and_elim_l (and A B) C h) let (ab := and_elim_l (A ∧ B) C h)
(a := and_elim_l A B ab) (a := and_elim_l A B ab)
(b := and_elim_r 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 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; end;
-- A ∨ (B ∨ C) => (A ∨ B) ∨ C -- A ∨ (B ∨ C) => (A ∨ B) ∨ C
def or_assoc_l (h : or A (or B C)) : or (or A B) C := def or_assoc_l (h : A ∨ (B ∨ C)) : (A ∨ B) ∨ C :=
or_elim A (or B C) (or (or A B) C) h or_elim A (B ∨ C) (A ∨ B ∨ C) h
(fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a)) (fun (a : A) => or_intro_l (A ∨ B) C (or_intro_l A B a))
(fun (g : or B C) => (fun (g : B ∨ C) =>
or_elim B C (or (or A B) C) g or_elim B C (A ∨ B ∨ C) g
(fun (b : B) => or_intro_l (or A B) C (or_intro_r A B b)) (fun (b : B) => or_intro_l (A ∨ B) C (or_intro_r A B b))
(fun (c : C) => or_intro_r (or A B) C c)); (fun (c : C) => or_intro_r (A ∨ B) C c));
-- (A ∨ B) ∨ C => A ∨ (B ∨ C) -- (A ∨ B) ∨ C => A ∨ (B ∨ C)
def or_assoc_r (h : or (or A B) C) : or A (or B C) := def or_assoc_r (h : (A ∨ B) ∨ C) : A ∨ (B ∨ C) :=
or_elim (or A B) C (or A (or B C)) h or_elim (A ∨ B) C (A ∨ (B ∨ C)) h
(fun (g : or A B) => (fun (g : A ∨ B) =>
or_elim A B (or A (or B C)) g or_elim A B (A ∨ (B ∨ C)) g
(fun (a : A) => or_intro_l A (or B C) a) (fun (a : A) => or_intro_l A (B ∨ C) a)
(fun (b : B) => or_intro_r A (or B C) (or_intro_l B C b))) (fun (b : B) => or_intro_r A (B ∨ C) (or_intro_l B C b)))
(fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c)); (fun (c : C) => or_intro_r A (B ∨ C) (or_intro_r B C c));
-- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ 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) := def and_distrib_l_or (h : A ∧ (B ∨ C)) : A ∧ B ∨ A ∧ C :=
or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h) or_elim B C (A ∧ B ∨ A ∧ C) (and_elim_r A (B ∨ C) h)
(fun (b : B) => or_intro_l (and A B) (and A C) (fun (b : B) => or_intro_l (A ∧ B) (A ∧ C)
(and_intro A B (and_elim_l A (or B C) h) b)) (and_intro A B (and_elim_l A (B ∨ C) h) b))
(fun (c : C) => or_intro_r (and A B) (and A C) (fun (c : C) => or_intro_r (A ∧ B) (A ∧ C)
(and_intro A C (and_elim_l A (or B C) h) c)); (and_intro A C (and_elim_l A (B ∨ C) h) c));
-- A ∧ B ∨ A ∧ C => A ∧ (B ∨ 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) := def and_factor_l_or (h : A ∧ B ∨ A ∧ C) : A ∧ (B ∨ C) :=
or_elim (and A B) (and A C) (and A (or B C)) h or_elim (A ∧ B) (A ∧ C) (A ∧ (B ∨ C)) h
(fun (ab : and A B) => and_intro A (or B C) (fun (ab : A ∧ B) => and_intro A (B ∨ C)
(and_elim_l A B ab) (and_elim_l A B ab)
(or_intro_l B C (and_elim_r 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) (and_elim_l A C ac)
(or_intro_r B C (and_elim_r A C ac))); (or_intro_r B C (and_elim_r A C ac)));
-- Thanks Quinn! -- Thanks Quinn!
-- A ∨ B => ~B => A -- 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); or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);
-- (A => B) => ~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); fun (a : A) => nb (f a);
end Theorems 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 -- powerful enough to construct the natural numbers (or at least to prove the
-- Peano axioms as theorems from a definition constructible in perga). However, -- 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 -- 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 -- 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 -- 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 -- 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 -- 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 -- As you can imagine, this can be risky. For instance, there's nothing stopping
-- us from saying -- 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, -- 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. -- 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; -> forall (n : nat), P n;
-- }}} -- }}}
@ -80,7 +80,7 @@ def four : nat := suc three;
def five : nat := suc four; def five : nat := suc four;
-- First, the predecessor of n is m if n = suc m. -- 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. -- Our claim is a disjunction, whose first option is that n = 0.
def szc_l (n : nat) := eq nat n zero; 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 -- So the claim we are trying to prove is that either one of the above options
-- holds for every n. -- 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! -- And here's our proof!
def suc_or_zero : forall (n : nat), szc n := 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 -- more used to perga. As such, I will go into a lot less detail on each of
-- these proofs than in the later sections. -- these proofs than in the later sections.
-- --
-- Here's our game plan. We will define a relation R : nat -> A -> * such that -- 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 -- R x y iff for every relation Q : nat -> A -> ★ satisfying
-- 1) Q 0 z and -- 1) Q 0 z and
-- 2) forall (x : nat) (y : A), Q x y -> Q (suc x) (fS x y), -- 2) forall (x : nat) (y : A), Q x y -> Q (suc x) (fS x y),
-- Q x y. -- Q x y.
@ -154,30 +154,30 @@ def suc_or_zero : forall (n : nat), szc n :=
section RecursiveDefs section RecursiveDefs
-- First, fix an A, z : A, and fS : nat -> A -> A -- 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 -- {{{ Defining R
-- Here is condition 1 formally expressed in perga. -- 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. -- 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); forall (n : nat) (y : A), Q n y -> Q (suc n) (fS n y);
-- From here we can define R. -- From here we can define R.
def rec_rel (x : nat) (y : A) := 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 -- {{{ 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 := 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 := def rec_rel_cond2 : cond2 rec_rel :=
fun (n : nat) (y : A) (h : rec_rel n y) 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); h2 n y (h Q h1 h2);
def rec_rel_total : total nat A rec_rel := def rec_rel_total : total nat A rec_rel :=
@ -194,18 +194,18 @@ def rec_rel_total : total nat A rec_rel :=
-- {{{ Defining R2 -- {{{ Defining R2
def alt_cond1 (x : nat) (y : A) := 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) def cond_y2 (x : nat) (y : A)
(x2 : nat) (y2 : 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) := 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 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 -- {{{ 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 -- {{{ 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; 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 := def R2_zero (y : A) : rec_rel_alt zero y -> eq A y z :=
let (cx2 := cond_x2 zero y) 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 -- existential, it still satisfies the property it definitionally is supposed
-- to satisfy. This annoying problem would be subverted with proper Σ-types, -- to satisfy. This annoying problem would be subverted with proper Σ-types,
-- provided they had η-equality. -- 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)); 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). -- 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! -- And here's plus!
def plus (n : nat) : nat -> nat := rec_def nat n psuc; 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 -- The first equation manifests itself as the familiar
-- n + 0 = 0. -- 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; rec_def_sat_zero nat n psuc;
-- The second equation, after a bit of massaging, manifests itself as the -- The second equation, after a bit of massaging, manifests itself as the
-- likewise familiar -- likewise familiar
-- n + suc m = suc (n + m). -- 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; rec_def_sat_suc nat n psuc m;
-- -- We can now prove 1 + 1 = 2! -- -- 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 -- 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) -- 1 + (suc zero) = suc (1 + zero)
(plus_s_r one zero) (plus_s_r one zero)
-- suc (1 + zero) = suc one -- 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 -- We have successfully defined addition! Note that evaluating 1 + 1 to 2
-- requires a proof, unfortunately, since this computation isn't visible to -- 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. -- We will now prove a couple standard properties of addition.
-- First, associativity, namely that n + (m + p) = (n + m) + p. -- 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) => := fun (n m : nat) =>
-- We prove this via induction on p for any fixed n and m. -- We prove this via induction on p for any fixed n and m.
nat_ind 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 -- Base case: p = 0
-- WTS n + (m + 0) = (n + m) + 0 -- WTS n + (m + 0) = (n + m) + 0
-- n + (m + 0) = n + m = (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 -- 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 -- 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 -- 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 -- WTS n + (m + suc p) = (n + m) + suc p
-- n + (m + suc p) = n + suc (m + p) -- n + (m + suc p) = n + suc (m + p)
-- = suc (n + (m + p)) -- = suc (n + (m + p))
-- = suc ((n + m) + p) -- = suc ((n + m) + p)
-- = (n + m) + suc 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) -- 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 -- 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)) -- 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 -- 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) -- 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 -- suc ((n + m) + p) = (n + m) + suc p
(eq_sym nat (plus (plus n m) (suc p)) (suc (plus (plus n m) p)) (eq_sym nat (n + m + suc p) (suc (n + m + p))
(plus_s_r (plus n m) p))))); (plus_s_r (n + m) p)))));
-- Up next is commutativity, but we will need a couple lemmas first. -- Up next is commutativity, but we will need a couple lemmas first.
-- First, we will show that 0 + n = n. -- 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. -- 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 -- base case: WTS 0 + 0 = 0
-- This is just plus_0_r 0 -- This is just plus_0_r 0
(plus_0_r zero) (plus_0_r zero)
-- inductive case -- 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 -- WTS 0 + (suc n) = suc n
-- 0 + (suc n) = suc (0 + 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) -- 0 + (suc n) = suc (0 + n)
(plus_s_r zero n) (plus_s_r zero n)
-- suc (0 + n) = suc 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). -- 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. -- 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) -- base case: (suc n) + 0 = suc (n + 0)
-- (suc n) + 0 = suc n = 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 -- (suc n) + 0 = suc n
(plus_0_r (suc n)) (plus_0_r (suc n))
-- suc n = suc (n + 0) -- 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 -- 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 -- inductive case
-- IH = suc n + m = suc (n + m) -- 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) -- WTS suc n + suc m = suc (n + suc m)
-- suc n + suc m = suc (suc n + m) -- suc n + suc m = suc (suc n + m)
-- = suc (suc (n + m)) -- = suc (suc (n + m))
-- = suc (n + suc 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) -- suc n + suc m = suc (suc n + m)
(plus_s_r (suc n) m) (plus_s_r (suc n) m)
-- suc (suc n + m) = suc (n + suc 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)) -- 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) -- 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 -- 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. -- 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. -- 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 -- Base case: WTS n + 0 = 0 + n
-- n + 0 = n = 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 -- n + 0 = n
(plus_0_r n) (plus_0_r n)
-- n = 0 + 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: -- 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 -- WTS n + suc m = suc m + n
-- n + suc m = suc (n + m) -- n + suc m = suc (n + m)
-- = suc (m + n) -- = suc (m + n)
-- = 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) -- n + suc m = suc (n + m)
(plus_s_r n m) (plus_s_r n m)
-- suc (n + m) = suc m + n -- 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) -- 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 -- 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.Combinators (option)
import Control.Monad.Except import Control.Monad.Except
import Data.List (foldl, foldl1) import Data.List (foldl, foldl1)
import qualified Data.Map.Strict as M
import qualified Data.Text as T import qualified Data.Text as T
import Errors (Error (..)) import Errors (Error (..))
import IR import IR
import Preprocessor 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 Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L import qualified Text.Megaparsec.Char.Lexer as L
newtype TypeError = TE Error newtype TypeError = TE Error
deriving (Eq, Ord) 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 instance ShowErrorComponent TypeError where
showErrorComponent (TE e) = toString e showErrorComponent (TE e) = toString e
@ -34,6 +42,9 @@ lexeme = L.lexeme skipSpace
symbol :: Text -> Parser () symbol :: Text -> Parser ()
symbol = void . L.symbol skipSpace symbol = void . L.symbol skipSpace
symbols :: String
symbols = "!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅"
pKeyword :: Text -> Parser () pKeyword :: Text -> Parser ()
pKeyword keyword = void $ lexeme (string keyword <* notFollowedBy alphaNumChar) pKeyword keyword = void $ lexeme (string keyword <* notFollowedBy alphaNumChar)
@ -46,21 +57,24 @@ pIdentifier = try $ label "identifier" $ lexeme $ do
guard $ ident `notElem` keywords guard $ ident `notElem` keywords
pure ident pure ident
pSymbol :: Parser Text
pSymbol = lexeme $ takeWhile1P (Just "symbol") (`elem` symbols)
pVar :: Parser IRExpr pVar :: Parser IRExpr
pVar = label "variable" $ lexeme $ Var <$> pIdentifier pVar = label "variable" $ lexeme $ Var <$> pIdentifier
pParamGroup :: Parser [Param] pParamGroup :: Parser Text -> Parser [Param]
pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do pParamGroup ident = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do
idents <- some pIdentifier idents <- some ident
symbol ":" symbol ":"
ty <- pIRExpr ty <- pIRExpr
pure $ map (,ty) idents pure $ map (,ty) idents
pSomeParams :: Parser [Param] pSomeParams :: Parser Text -> Parser [Param]
pSomeParams = lexeme $ concat <$> some pParamGroup pSomeParams ident = lexeme $ concat <$> some (pParamGroup ident)
pManyParams :: Parser [Param] pManyParams :: Parser Text -> Parser [Param]
pManyParams = lexeme $ concat <$> many pParamGroup pManyParams ident = lexeme $ concat <$> many (pParamGroup ident)
mkAbs :: Maybe IRExpr -> (Text, IRExpr) -> IRExpr -> IRExpr mkAbs :: Maybe IRExpr -> (Text, IRExpr) -> IRExpr -> IRExpr
mkAbs ascription (param, typ) = Abs param typ ascription mkAbs ascription (param, typ) = Abs param typ ascription
@ -71,7 +85,7 @@ mkPi ascription (param, typ) = Pi param typ ascription
pLAbs :: Parser IRExpr pLAbs :: Parser IRExpr
pLAbs = lexeme $ label "λ-abstraction" $ do pLAbs = lexeme $ label "λ-abstraction" $ do
_ <- pKeyword "fun" <|> symbol "λ" _ <- pKeyword "fun" <|> symbol "λ"
params <- pSomeParams params <- pSomeParams pIdentifier
ascription <- optional pAscription ascription <- optional pAscription
_ <- symbol "=>" <|> symbol "⇒" _ <- symbol "=>" <|> symbol "⇒"
body <- pIRExpr body <- pIRExpr
@ -80,7 +94,7 @@ pLAbs = lexeme $ label "λ-abstraction" $ do
pPAbs :: Parser IRExpr pPAbs :: Parser IRExpr
pPAbs = lexeme $ label "Π-abstraction" $ do pPAbs = lexeme $ label "Π-abstraction" $ do
_ <- pKeyword "forall" <|> symbol "∏" <|> symbol "∀" _ <- pKeyword "forall" <|> symbol "∏" <|> symbol "∀"
params <- pSomeParams params <- pSomeParams pIdentifier
ascription <- optional pAscription ascription <- optional pAscription
symbol "," symbol ","
body <- pIRExpr body <- pIRExpr
@ -90,7 +104,7 @@ pBinding :: Parser (Text, Maybe IRExpr, IRExpr)
pBinding = lexeme $ label "binding" $ do pBinding = lexeme $ label "binding" $ do
symbol "(" symbol "("
ident <- pIdentifier ident <- pIdentifier
params <- pManyParams params <- pManyParams pIdentifier
ascription <- optional pAscription ascription <- optional pAscription
symbol ":=" symbol ":="
value <- pIRExpr value <- pIRExpr
@ -117,7 +131,7 @@ pApp :: Parser IRExpr
pApp = lexeme $ foldl1 App <$> some pTerm pApp = lexeme $ foldl1 App <$> some pTerm
pStar :: Parser IRExpr pStar :: Parser IRExpr
pStar = lexeme $ Star <$ symbol "*" pStar = lexeme $ Star <$ symbol "★"
subscriptDigit :: Parser Integer subscriptDigit :: Parser Integer
subscriptDigit = subscriptDigit =
@ -146,8 +160,31 @@ pSort = lexeme $ pStar <|> pSquare
pTerm :: Parser IRExpr pTerm :: Parser IRExpr
pTerm = lexeme $ label "term" $ choice [pSort, pVar, between (char '(') (char ')') pIRExpr] 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 :: Parser IRExpr
pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp] pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pInfix]
pIRExpr :: Parser IRExpr pIRExpr :: Parser IRExpr
pIRExpr = lexeme $ do pIRExpr = lexeme $ do
@ -161,7 +198,7 @@ pAxiom :: Parser IRDef
pAxiom = lexeme $ label "axiom" $ do pAxiom = lexeme $ label "axiom" $ do
pKeyword "axiom" pKeyword "axiom"
ident <- pIdentifier ident <- pIdentifier
params <- pManyParams params <- pManyParams (pIdentifier <|> pSymbol)
ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription
symbol ";" symbol ";"
pure $ Axiom ident ascription pure $ Axiom ident ascription
@ -169,21 +206,33 @@ pAxiom = lexeme $ label "axiom" $ do
pVariable :: Parser [IRSectionDef] pVariable :: Parser [IRSectionDef]
pVariable = lexeme $ label "variable declaration" $ do pVariable = lexeme $ label "variable declaration" $ do
pKeyword "variable" <|> pKeyword "hypothesis" pKeyword "variable" <|> pKeyword "hypothesis"
vars <- pManyParams vars <- pManyParams (pIdentifier <|> pSymbol)
symbol ";" symbol ";"
pure $ uncurry Variable <$> vars pure $ uncurry Variable <$> vars
pDef :: Parser IRDef pDef :: Parser IRDef
pDef = lexeme $ label "definition" $ do pDef = lexeme $ label "definition" $ do
pKeyword "def" pKeyword "def"
ident <- pIdentifier ident <- pIdentifier <|> pSymbol
params <- pManyParams params <- pManyParams pIdentifier
ascription <- fmap (flip (foldr (mkPi Nothing)) params) <$> optional pAscription ascription <- fmap (flip (foldr (mkPi Nothing)) params) <$> optional pAscription
symbol ":=" symbol ":="
body <- pIRExpr body <- pIRExpr
symbol ";" symbol ";"
pure $ Def ident ascription $ foldr (mkAbs Nothing) body params 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 :: Parser IRSectionDef
pSection = lexeme $ label "section" $ do pSection = lexeme $ label "section" $ do
pKeyword "section" pKeyword "section"
@ -194,13 +243,13 @@ pSection = lexeme $ label "section" $ do
pure $ Section secLabel body pure $ Section secLabel body
pIRDef :: Parser [IRSectionDef] 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 :: Parser IRProgram
pIRProgram = skipSpace >> concat <$> some pIRDef pIRProgram = skipSpace >> concat <$> some pIRDef
parserWrapper :: Parser a -> String -> Text -> Either String a 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 :: String -> Text -> Either String IRProgram
parseProgram = parserWrapper pIRProgram parseProgram = parserWrapper pIRProgram