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

updates to examples

Browse source
This commit is contained in:
William Ball 2024-11-22 11:52:30 -08:00
parent 75ab0a1a41
commit 91157dd2aa
3 changed files with 103 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
examples/algebra.pg
View file

@ -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)))));

27
examples/classical.pg Normal file
View file

@ -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);

19
examples/logic.pg
View file

@ -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);