From 91157dd2aa5a785620459673bc968891b2676ff2 Mon Sep 17 00:00:00 2001 From: William Ball Date: Fri, 22 Nov 2024 11:52:30 -0800 Subject: [PATCH] updates to examples --- examples/algebra.pg | 59 +++++++++++++++++++++++++++++++++++++++++-- examples/classical.pg | 27 ++++++++++++++++++++ examples/logic.pg | 19 ++++++++++++++ 3 files changed, 103 insertions(+), 2 deletions(-) create mode 100644 examples/classical.pg diff --git a/examples/algebra.pg b/examples/algebra.pg index 7ee1e81..258b9b3 100644 --- a/examples/algebra.pg +++ b/examples/algebra.pg @@ -20,7 +20,7 @@ binop (A : *) := A -> A -> A; -- a binary operation is associative if ... assoc (A : *) (op : binop A) := - forall (a b c : A), eq A (op (op a b) c) (op a (op b c)); + forall (a b c : A), eq A (op a (op b c)) (op (op a b) c); -- an element `e : A` is a left identity with respect to binop `op` if `∀ a, e * a = a` id_l (A : *) (op : binop A) (e : A) := @@ -65,6 +65,9 @@ id_rm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : id_r M op e := and_elim_r (id_l M op e) (id_r M op e) (and_elim_r (semigroup M op) (id M op e) Hmonoid); +assoc_m (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : assoc M op := + and_elim_l (semigroup M op) (id M op e) Hmonoid; + -- now we can prove that, for any monoid, if `a` is a left identity, then it -- must be "the" identity monoid_id_l_implies_identity @@ -99,6 +102,58 @@ monoid_id_r_implies_identity -- groups are just monoids with inverses +has_inverses (G : *) (op : binop G) (e : G) (i : unop G) : * := + forall (a : G), inv G op e a (i a); + group (G : *) (op : binop G) (e : G) (i : unop G) : * := and (monoid G op e) - (forall (a : G), inv G op e a (i a)); + (has_inverses G op e i); + +-- more "getters" +monoid_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : monoid G op e := + and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup; + +assoc_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : assoc G op := + assoc_m G op e (monoid_g G op e i Hgroup); + +id_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_l G op e := + id_lm G op e (and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup); + +id_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_r G op e := + id_rm G op e (and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup); + +inv_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : forall (a : G), inv G op e a (i a) := + and_elim_r (monoid G op e) (has_inverses G op e i) Hgroup; + +inv_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_l G op e a (i a) := + and_elim_l (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a); + +inv_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_r G op e a (i a) := + and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a); + +left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a b : G) (h : inv_l G op e a b) : eq G b (i a) := + -- b = b * e + -- = b * (a * a^-1) + -- = (b * a) * a^-1 + -- = e * a^-1 + -- = a^-1 + eq_trans G b (op b e) (i a) + -- b = b * e + (eq_sym G (op b e) b (id_rg G op e i Hgroup b)) + -- b * e = a^-1 + (eq_trans G (op b e) (op b (op a (i a))) (i a) + --b * e = b * (a * a^-1) + (eq_cong G G e (op a (i a)) (op b) + -- e = a * a^-1 + (eq_sym G (op a (i a)) e (inv_rg G op e i Hgroup a))) + -- b * (a * a^-1) = a^-1 + (eq_trans G (op b (op a (i a))) (op (op b a) (i a)) (i a) + -- b * (a * a^-1) = (b * a) * a^-1 + (assoc_g G op e i Hgroup 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) + -- (b * a) * a^-1 = e * a^-1 + (eq_cong G G (op b a) e (fun (x : G) => op x (i a)) h) + -- e * a^-1 = a^-1 + (id_lg G op e i Hgroup (i a))))); + diff --git a/examples/classical.pg b/examples/classical.pg new file mode 100644 index 0000000..18aaa5e --- /dev/null +++ b/examples/classical.pg @@ -0,0 +1,27 @@ +@include logic.pg + +-- excluded middle! +-- P ∨ ~P +em (P : *) : or (P) (not P) := axiom; + +-- ~~P => P +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 +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 +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) + (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))) + (fun (nb : not B) => or_intro_r (not A) (not B) nb)) + (fun (na : not A) => or_intro_l (not A) (not B) na); diff --git a/examples/logic.pg b/examples/logic.pg index adc537b..df715ce 100644 --- a/examples/logic.pg +++ b/examples/logic.pg @@ -190,3 +190,22 @@ and_distrib_l_or (A B C : *) (h : and A (or B C)) : or (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)); + +-- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C) +and_factor_l_or (A B C : *) (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) + (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) + (and_elim_l A C ac) + (or_intro_r B C (and_elim_r A C ac))); + +-- Thanks Quinn! +-- A ∨ B => ~B => A +disj_syllog (A B : *) (nb : not B) (hor : or A B) : A := + or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A); + +-- (A => B) => ~B => ~A +contrapositive (A B : *) (f : A -> B) (nb : not B) : not A := + fun (a : A) => nb (f a);