Skip to content
Snippets Groups Projects
Verified Commit 5936b90f authored by ColinRothgang's avatar ColinRothgang
Browse files

Replace tabs with spaces 

This makes the examples look better when viewed from a web browser
parent 96501657
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
source/casestudies/2023-cade/BasicExample/predicate_exam.mmt
+ 1
− 1
View file @ 5936b90f
......@@ -9,7 +9,7 @@ theory PredicateExample : latin:/?DHOL =
// The type (a true) is a singleton.❙
ax0: ⊦ ∀ͭ[x:tm (a true)] x =ͭ c_0 ❙
// The type (a false) has at least two elements that are distinguished by p.❙
p: tm Πͭ [x: tm (a false)] bool ❙
ax1: ⊦ p @ c_1 ❙
......
source/casestudies/2023-cade/Category Theory/cat.mmt
+ 135
− 135
View file @ 5936b90f
......@@ -6,10 +6,10 @@ theory Cat : latin:/?DHOL =
mor : tm obj ⟶ tm obj ⟶ tp ❙
id: tm Πͭ [x] mor x x ❙
comp: tm Πͭ [x] Πͭ [y] Πͭ [z] Πͭ [f:tm mor x y] Πͭ [g:tm mor y z] mor x z ❘# 5 ◦ 4 prec 50 ❙
ax1: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] ((((comp @ x) @ y) @ y) @ m) @ (id @ y) =ͭ m ❙
ax1: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] ((((comp @ x) @ y) @ y) @ m) @ (id @ y) =ͭ m ❙
ax2: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] ((((comp @ x) @ x) @ y) @ (id @ x)) @ m =ͭ m ❙
// we omit the associativity axiom for brevity
// An example conjecture that with non-trivial well-typedness.
The type checker generates the proof obligation x =ͭ y ⇒ͩ [p] y =ͭ x ❙
conj: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] x =ͭ y ⇒ͩ [p] (id @ x) =ͭ (id @ y) ❘ = PROVE ❙
......@@ -21,81 +21,81 @@ theory CatExtended : latin:/?DPHOL =
mor : {x:tm obj,y:tm obj} tp ❙
id: {x: tm obj} tm mor x x ❙
comp: {x, y, z, f:tm mor x y, g:tm mor y z} tm mor x z ❘ # 5 ◦ 4 prec 50 ❙
ax1: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] (id y) ◦ m =ͭ m ❙
ax1: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] (id y) ◦ m =ͭ m ❙
ax2: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[m: tm (mor x y)] m ◦ (id x) =ͭ m ❙
isIsomorphism : {x, y} tm mor x y ⟶ prop ❘ = [x, y, m]
∃ͭ [i: tm mor y x] i ◦ m =ͭ id x ∧ m ◦ i =ͭ id y ❙
areIsomorphic : tm obj ⟶ tm obj ⟶ prop ❘ = [x, y] ∃ͭ [i: tm mor x y] isIsomorphism x y i ❙
// Lemma 1: transitivity of isomorphic ❙
transitiveIsomorphic: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] areIsomorphic x y⇒ areIsomorphic y z ⇒ areIsomorphic y z ❙
// an example of predicate subtypes: the endo-isomorphisms of an object❙
isomorphisms = [u: tm obj] mor u u | ( [m: mor u u] isIsomorphism u u m ) ❙
// a particular categorical product and projections❙
prod: tm obj ⟶ tm obj ⟶ tm obj ❙
proj1: {x:tm obj, y:tm obj} tm mor (prod x y) x ❙
proj2: {x:tm obj, y:tm obj} tm mor (prod x y) y ❙
// A few abbreviations towards stating the universal property.
Note that "# ..." introduces compact notations for these abbreviations.
The definitions abstract over an arbitrary potential arbitrary product (xy, projX, projY) of two objects x and y.❙
// f and g factorize through projX and projY using universal morphism u❙
factorizesProjections:
{x,y,z, f:tm mor z x, g:tm mor z y, xy, projX: tm mor xy x, projY: tm mor xy y, u:tm mor z xy} prop❘
= [x, y, z, f, g, xy, projX, projY, u] projX ◦ u =ͭ f ∧ projY ◦ u =ͭ g ❘
# factorizesProjs 4 5 7 8 9 ❙
isIsomorphism : {x, y} tm mor x y ⟶ prop ❘ = [x, y, m]
∃ͭ [i: tm mor y x] i ◦ m =ͭ id x ∧ m ◦ i =ͭ id y ❙
areIsomorphic : tm obj ⟶ tm obj ⟶ prop ❘ = [x, y] ∃ͭ [i: tm mor x y] isIsomorphism x y i ❙
// Lemma 1: transitivity of isomorphic ❙
transitiveIsomorphic: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] areIsomorphic x y⇒ areIsomorphic y z ⇒ areIsomorphic y z ❙
// an example of predicate subtypes: the endo-isomorphisms of an object❙
isomorphisms = [u: tm obj] mor u u | ( [m: mor u u] isIsomorphism u u m ) ❙
// a particular categorical product and projections❙
prod: tm obj ⟶ tm obj ⟶ tm obj ❙
proj1: {x:tm obj, y:tm obj} tm mor (prod x y) x ❙
proj2: {x:tm obj, y:tm obj} tm mor (prod x y) y ❙
// A few abbreviations towards stating the universal property.
Note that "# ..." introduces compact notations for these abbreviations.
The definitions abstract over an arbitrary potential arbitrary product (xy, projX, projY) of two objects x and y.❙
// f and g factorize through projX and projY using universal morphism u❙
factorizesProjections:
{x,y,z, f:tm mor z x, g:tm mor z y, xy, projX: tm mor xy x, projY: tm mor xy y, u:tm mor z xy} prop❘
= [x, y, z, f, g, xy, projX, projY, u] projX ◦ u =ͭ f ∧ projY ◦ u =ͭ g ❘
# factorizesProjs 4 5 7 8 9 ❙
// m is the unique morphism with property p❙
isUniqueMorphismWith: {x, y, p: tm (mor x y) ⟶ prop, m:tm mor x y} prop ❘
= [x, y, p, m]
p m ∧ ∀ͭ[u:tm mor x y] p u ⇒ m =ͭ u ❘
# 4 isUniqueMorWith 3 ❙
// the uniqueness of the universal morphism❙
isUniversalMorphismOfAProduct:
{x, y, z, f:tm mor z x, g:tm mor z y,
xy, projX: tm mor xy x, projY: tm mor xy y, u:tm mor z xy} prop ❘
= [x, y, z, f, g, xy, projX, projY, u]
u isUniqueMorWith ([m] factorizesProjs f g projX projY m) ❘
# isUnivMorProd 4 5 7 8 9 ❙
// the property of (xy, projX, projY) being a product: the universal morphism must exist uniquely❙
isProduct: {x, y, xy, projX: tm mor xy x, projY: tm mor xy y} prop ❘
= [x, y, xy, projX, projY] ∀ͭ[z] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y]
∃ͭ [u] isUnivMorProd f g projX projY u ❘
# isProd 3 4 5 ❙
isUniqueMorphismWith: {x, y, p: tm (mor x y) ⟶ prop, m:tm mor x y} prop ❘
= [x, y, p, m]
p m ∧ ∀ͭ[u:tm mor x y] p u ⇒ m =ͭ u ❘
# 4 isUniqueMorWith 3 ❙
// the uniqueness of the universal morphism❙
isUniversalMorphismOfAProduct:
{x, y, z, f:tm mor z x, g:tm mor z y,
xy, projX: tm mor xy x, projY: tm mor xy y, u:tm mor z xy} prop ❘
= [x, y, z, f, g, xy, projX, projY, u]
u isUniqueMorWith ([m] factorizesProjs f g projX projY m) ❘
# isUnivMorProd 4 5 7 8 9 ❙
// the property of (xy, projX, projY) being a product: the universal morphism must exist uniquely❙
isProduct: {x, y, xy, projX: tm mor xy x, projY: tm mor xy y} prop ❘
= [x, y, xy, projX, projY] ∀ͭ[z] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y]
∃ͭ [u] isUnivMorProd f g projX projY u ❘
# isProd 3 4 5 ❙
// finally the axiom that (prod, proj1, proj2) indeed returns a product for all arguments❙
prodUnivMorph_ax: ⊦ ∀ͭ[x] ∀ͭ[y] isProduct x y (prod x y) (proj1 x y) (proj2 x y)❙
// We (try to) prove some non-trivial properties of the product.❙
// Lemma 2: Uniqueness of the product.
This cannot be proven by any HOL prover even in the native HOL version below.❙
uniquenessProd: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y]
isProduct x y z f g ⇒ areIsomorphic z (prod x y) ❙
// Lemma 3: a simpler version and the first step towards proving the Lemma 5 below❙
symmetricIsProd: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y]
isProduct x y z f g ⇒ isProduct y x z g f ❙
// Lemma 4: another stepping stone❙
isProdUnique: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y]
∀ͭ[xy] ∀ͭ[projX: tm mor xy x] ∀ͭ[projY: tm mor xy y]
isProduct x y z f g ⇒ isProduct x y xy projX projY ⇒ areIsomorphic z xy ❙
// Lemma 5: products are commutative up to isomorphism.
This rather hard to prove on its own (even in the native version below, only E can prove it),
but it becomes provable if the previous lemmas are included in the formalization.❙
symmetricProd: ⊦ ∀ͭ[x] ∀ͭ[y] areIsomorphic (prod x y) (prod y x) ❙
// Lemma 6: associativity up to isomorphism.
Without stepping stone lemmas, this cannot be proved although some provers can prove it in the native HOL version below.❙
assocProd: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] areIsomorphic (prod x (prod y z)) (prod (prod x y) z) ❘ = PROVE ❙
prodUnivMorph_ax: ⊦ ∀ͭ[x] ∀ͭ[y] isProduct x y (prod x y) (proj1 x y) (proj2 x y)❙
// We (try to) prove some non-trivial properties of the product.❙
// Lemma 2: Uniqueness of the product.
This cannot be proven by any HOL prover even in the native HOL version below.❙
uniquenessProd: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y]
isProduct x y z f g ⇒ areIsomorphic z (prod x y) ❙
// Lemma 3: a simpler version and the first step towards proving the Lemma 5 below❙
symmetricIsProd: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y]
isProduct x y z f g ⇒ isProduct y x z g f ❙
// Lemma 4: another stepping stone❙
isProdUnique: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] ∀ͭ[f: tm mor z x] ∀ͭ[g: tm mor z y]
∀ͭ[xy] ∀ͭ[projX: tm mor xy x] ∀ͭ[projY: tm mor xy y]
isProduct x y z f g ⇒ isProduct x y xy projX projY ⇒ areIsomorphic z xy ❙
// Lemma 5: products are commutative up to isomorphism.
This rather hard to prove on its own (even in the native version below, only E can prove it),
but it becomes provable if the previous lemmas are included in the formalization.❙
symmetricProd: ⊦ ∀ͭ[x] ∀ͭ[y] areIsomorphic (prod x y) (prod y x) ❙
// Lemma 6: associativity up to isomorphism.
Without stepping stone lemmas, this cannot be proved although some provers can prove it in the native HOL version below.❙
assocProd: ⊦ ∀ͭ[x] ∀ͭ[y] ∀ͭ[z] areIsomorphic (prod x (prod y z)) (prod (prod x y) z) ❘ = PROVE ❙
❚
// An alternative formalization that uses only HOL instead of DHOL.
......@@ -105,71 +105,71 @@ theory CatExtended : latin:/?DPHOL =
theory CatExtendedHOL : latin:/?HOL =
obj : tp❙
mor : tp❙
id: tm obj ⟶ tm mor❙
// This makes all morphisms composable.
So all domain/codomain information of morphisms must be provided
by assumptions rather than types.❙
comp : tm mor ⟶ tm mor ⟶ tm mor❘ # 2 ◦ 1 prec 50 ❙
dom: tm mor ⟶ tm obj❙ // (co)domain of a morphism❙
cod: tm mor ⟶ tm obj❙
// (co)domain axioms for identity and composition❙
id_dom: ⊦ ∀ͭ[a: tm obj] dom (id a) =ͭ a❙
id_cod: ⊦ ∀ͭ[a: tm obj] cod (id a) =ͭ a❙
comp_dom: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[f: tm mor] ∀ͭ[g: tm mor] cod f =ͭ dom g ⇒ dom (g ◦ f) =ͭ dom f ❙
comp_cod: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[f: tm mor] ∀ͭ[g: tm mor] cod f =ͭ dom g ⇒ cod (g ◦ f) =ͭ cod g❙
// abbreviations for isomorphism❙
isIsomorphism : tm obj ⟶ tm obj ⟶ tm mor ⟶ prop ❘ = [a,b, f] ∃ͭ [inv: tm mor]
dom f =ͭ a ∧ cod f =ͭ b ∧ dom inv =ͭ b ∧ cod inv =ͭ a ∧ f ◦ inv =ͭ id b ∧ inv ◦ f =ͭ id a ❙
areIsomorphic : tm obj ⟶ tm obj ⟶ prop ❘ = [a,b] ∃ͭ [f: tm mor] dom f =ͭ a ∧ cod f =ͭ b ∧ isIsomorphism a b f ❙
// transitivity of isomorphism❙
transitiveIsomorphic: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj]
areIsomorphic x y ⇒ areIsomorphic y z ⇒ areIsomorphic y z ❙
// a product operator❙
prod: tm obj ⟶ tm obj ⟶ tm obj ❙
proj1: tm obj ⟶ tm obj ⟶ tm mor ❙
proj1_dom: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] dom (proj1 x y) =ͭ prod x y ❙
proj1_cod: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] cod (proj1 x y) =ͭ x ❙
proj2: tm obj ⟶ tm obj ⟶ tm mor ❙
proj2_dom: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] dom (proj2 x y) =ͭ prod x y ❙
proj2_cod: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] cod (proj2 x y) =ͭ y ❙
// abbreviations corresponding to the above❙
factorizesProjections: tm obj ⟶ tm obj ⟶ tm obj ⟶ tm mor ⟶ tm mor ⟶ tm obj ⟶ tm mor ⟶ tm mor ⟶ tm mor ⟶ prop ❘
= [x: tm obj, y: tm obj, z: tm obj, f: tm mor, g: tm mor, xy: tm obj, projX: tm mor, projY: tm mor, u:tm mor]
dom f =ͭ z ∧ cod f =ͭ x ∧ dom g =ͭ z ∧ cod g =ͭ y ∧ dom projX =ͭ xy ∧ cod projX =ͭ x ∧ dom projY =ͭ xy ∧ cod projY =ͭ y
∧ dom u =ͭ z ∧ cod u =ͭ xy ∧ projX ◦ u =ͭ f ∧ projY ◦ u =ͭ g ❙
id: tm obj ⟶ tm mor❙
// This makes all morphisms composable.
So all domain/codomain information of morphisms must be provided
by assumptions rather than types.❙
comp : tm mor ⟶ tm mor ⟶ tm mor❘ # 2 ◦ 1 prec 50 ❙
dom: tm mor ⟶ tm obj❙ // (co)domain of a morphism❙
cod: tm mor ⟶ tm obj❙
// (co)domain axioms for identity and composition❙
id_dom: ⊦ ∀ͭ[a: tm obj] dom (id a) =ͭ a❙
id_cod: ⊦ ∀ͭ[a: tm obj] cod (id a) =ͭ a❙
comp_dom: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[f: tm mor] ∀ͭ[g: tm mor] cod f =ͭ dom g ⇒ dom (g ◦ f) =ͭ dom f ❙
comp_cod: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[f: tm mor] ∀ͭ[g: tm mor] cod f =ͭ dom g ⇒ cod (g ◦ f) =ͭ cod g❙
// abbreviations for isomorphism❙
isIsomorphism : tm obj ⟶ tm obj ⟶ tm mor ⟶ prop ❘ = [a,b, f] ∃ͭ [inv: tm mor]
dom f =ͭ a ∧ cod f =ͭ b ∧ dom inv =ͭ b ∧ cod inv =ͭ a ∧ f ◦ inv =ͭ id b ∧ inv ◦ f =ͭ id a ❙
areIsomorphic : tm obj ⟶ tm obj ⟶ prop ❘ = [a,b] ∃ͭ [f: tm mor] dom f =ͭ a ∧ cod f =ͭ b ∧ isIsomorphism a b f ❙
// transitivity of isomorphism❙
transitiveIsomorphic: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj]
areIsomorphic x y ⇒ areIsomorphic y z ⇒ areIsomorphic y z ❙
// a product operator❙
prod: tm obj ⟶ tm obj ⟶ tm obj ❙
proj1: tm obj ⟶ tm obj ⟶ tm mor ❙
proj1_dom: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] dom (proj1 x y) =ͭ prod x y ❙
proj1_cod: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] cod (proj1 x y) =ͭ x ❙
proj2: tm obj ⟶ tm obj ⟶ tm mor ❙
proj2_dom: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] dom (proj2 x y) =ͭ prod x y ❙
proj2_cod: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] cod (proj2 x y) =ͭ y ❙
// abbreviations corresponding to the above❙
factorizesProjections: tm obj ⟶ tm obj ⟶ tm obj ⟶ tm mor ⟶ tm mor ⟶ tm obj ⟶ tm mor ⟶ tm mor ⟶ tm mor ⟶ prop ❘
= [x: tm obj, y: tm obj, z: tm obj, f: tm mor, g: tm mor, xy: tm obj, projX: tm mor, projY: tm mor, u:tm mor]
dom f =ͭ z ∧ cod f =ͭ x ∧ dom g =ͭ z ∧ cod g =ͭ y ∧ dom projX =ͭ xy ∧ cod projX =ͭ x ∧ dom projY =ͭ xy ∧ cod projY =ͭ y
∧ dom u =ͭ z ∧ cod u =ͭ xy ∧ projX ◦ u =ͭ f ∧ projY ◦ u =ͭ g ❙
isUniqueMorphismWith: tm obj ⟶ tm obj ⟶ (tm mor ⟶ prop) ⟶ tm mor ⟶ prop ❘
= [x: tm obj, y: tm obj, p: tm mor ⟶ prop, m: tm mor]
dom m =ͭ x ∧ cod m =ͭ y ∧ p m ∧ ∀ͭ[u:tm mor] dom u =ͭ x ∧ cod u =ͭ y ∧ p u ⇒ m =ͭ u ❙
dom m =ͭ x ∧ cod m =ͭ y ∧ p m ∧ ∀ͭ[u:tm mor] dom u =ͭ x ∧ cod u =ͭ y ∧ p u ⇒ m =ͭ u ❙
isUniversalMorphismOfAProduct: tm obj ⟶ tm obj ⟶ tm obj ⟶ tm mor ⟶ tm mor ⟶ tm obj ⟶ tm mor ⟶ tm mor ⟶ tm mor ⟶ prop ❘
= [x: tm obj, y: tm obj, z: tm obj, f: tm mor, g: tm mor, xy: tm obj, projX: tm mor, projY: tm mor, u:tm mor]
dom f =ͭ z ∧ cod f =ͭ x ∧ dom g =ͭ z ∧ cod g =ͭ y ∧ dom projX =ͭ xy ∧ cod projX =ͭ x ∧ dom projY =ͭ xy ∧ cod projY =ͭ y
∧ dom u =ͭ z ∧ cod u =ͭ xy ∧
isUniqueMorphismWith x y ([m:tm mor] dom m =ͭ x ∧ cod m =ͭ y ∧ factorizesProjections x y z f g xy projX projY m) u ❘# isUnivMorProd 4 5 7 8 9 ❙
isProduct: tm obj ⟶ tm obj ⟶ tm obj ⟶ tm mor ⟶ tm mor ⟶ prop ❘ =
[x: tm obj, y: tm obj, xy: tm obj, projX: tm mor, projY: tm mor] dom projX =ͭ xy ∧ cod projX =ͭ x ∧ dom projY =ͭ xy ∧ cod projY =ͭ y ∧
∀ͭ[z: tm obj] ∀ͭ[f: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒ ∀ͭ[g: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒
∃ͭ [u: tm mor] dom u =ͭ z ∧ cod u =ͭ xy ∧ isUniversalMorphismOfAProduct x y z f g xy projX projY u ❘# isProd 3 4 5 ❙
prodUnivMorph_ax: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] isProduct x y (prod x y) (proj1 x y) (proj2 x y) ❙
uniquenessProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj] ∀ͭ[f: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒ ∀ͭ[g: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒
isProduct x y z f g ⇒ areIsomorphic z (prod x y) ❙
symmetricIsProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj] ∀ͭ[f: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒ ∀ͭ[g: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒
isProduct x y z f g ⇒ isProduct y x z g f ❙
isProdUnique: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj] ∀ͭ[f: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒ ∀ͭ[g: tm mor] dom g =ͭ z ∧ cod g =ͭ y ⇒
∀ͭ[xy: tm obj] ∀ͭ[projX: tm mor] dom projX =ͭ xy ∧ cod projX =ͭ x ⇒ ∀ͭ[projY: tm mor] dom projY =ͭ xy ∧ cod projY =ͭ y ⇒
isProduct x y z f g ⇒ isProduct x y xy projX projY ⇒ areIsomorphic z xy ❙
// commutativity up to isomorphism❙
symmetricProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] areIsomorphic (prod x y) (prod y x) ❙
// associativity up to isomorphism❙
assocProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj] areIsomorphic (prod x (prod y z)) (prod (prod x y) z) ❙
dom f =ͭ z ∧ cod f =ͭ x ∧ dom g =ͭ z ∧ cod g =ͭ y ∧ dom projX =ͭ xy ∧ cod projX =ͭ x ∧ dom projY =ͭ xy ∧ cod projY =ͭ y
∧ dom u =ͭ z ∧ cod u =ͭ xy ∧
isUniqueMorphismWith x y ([m:tm mor] dom m =ͭ x ∧ cod m =ͭ y ∧ factorizesProjections x y z f g xy projX projY m) u ❘# isUnivMorProd 4 5 7 8 9 ❙
isProduct: tm obj ⟶ tm obj ⟶ tm obj ⟶ tm mor ⟶ tm mor ⟶ prop ❘ =
[x: tm obj, y: tm obj, xy: tm obj, projX: tm mor, projY: tm mor] dom projX =ͭ xy ∧ cod projX =ͭ x ∧ dom projY =ͭ xy ∧ cod projY =ͭ y ∧
∀ͭ[z: tm obj] ∀ͭ[f: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒ ∀ͭ[g: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒
∃ͭ [u: tm mor] dom u =ͭ z ∧ cod u =ͭ xy ∧ isUniversalMorphismOfAProduct x y z f g xy projX projY u ❘# isProd 3 4 5 ❙
prodUnivMorph_ax: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] isProduct x y (prod x y) (proj1 x y) (proj2 x y) ❙
uniquenessProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj] ∀ͭ[f: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒ ∀ͭ[g: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒
isProduct x y z f g ⇒ areIsomorphic z (prod x y) ❙
symmetricIsProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj] ∀ͭ[f: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒ ∀ͭ[g: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒
isProduct x y z f g ⇒ isProduct y x z g f ❙
isProdUnique: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj] ∀ͭ[f: tm mor] dom f =ͭ z ∧ cod f =ͭ x ⇒ ∀ͭ[g: tm mor] dom g =ͭ z ∧ cod g =ͭ y ⇒
∀ͭ[xy: tm obj] ∀ͭ[projX: tm mor] dom projX =ͭ xy ∧ cod projX =ͭ x ⇒ ∀ͭ[projY: tm mor] dom projY =ͭ xy ∧ cod projY =ͭ y ⇒
isProduct x y z f g ⇒ isProduct x y xy projX projY ⇒ areIsomorphic z xy ❙
// commutativity up to isomorphism❙
symmetricProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] areIsomorphic (prod x y) (prod y x) ❙
// associativity up to isomorphism❙
assocProd: ⊦ ∀ͭ[x: tm obj] ∀ͭ[y: tm obj] ∀ͭ[z: tm obj] areIsomorphic (prod x (prod y z)) (prod (prod x y) z) ❙
❚
source/casestudies/2023-cade/FunctionsOnSets/functions.mmt
+ 52
− 52
View file @ 5936b90f
......@@ -3,63 +3,63 @@ namespace latin:/casestudies/_2023-cade❚
// a fragment of a formalization of set theory❚
theory FunctionExample : latin:/?DHOL =
// the type of sets❙
set: tp ❙
// the set of function from a to b❙
set: tp ❙
// the set of function from a to b❙
functType : tm Πͭ [a: tm set] Πͭ [b: tm set] set ❙
// function application❙
funcAppl : tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] Πͭ [x: tm set] set ❙
// the property of being a function❙
functionHood_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[x:tm set] ∀ͭ[y:tm set] x =ͭ y ⇒ (funcAppl @ a @ b @ f @ x) =ͭ (funcAppl @ a @ b @ f @ y) ❙
// functional extensionality❙
functExt_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ((∀ͭ[x:tm set] (funcAppl @ a @ b @ f @ x) =ͭ (funcAppl @ a @ b @ g @ x)) ⇒ f =ͭ g) ❙
// composition of functions❙
concat : tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [c: tm set] Πͭ [f: tm set] Πͭ [g: tm set] set ❙
concatAppl_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[c:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ∀ͭ[x:tm set]
(funcAppl @ a @ c @ (concat @ a @ b @ c @ f @ g) @ x) =ͭ (funcAppl @ b @ c @ f @ (funcAppl @ a @ b @ g @ x)) ❙
funcAppl : tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] Πͭ [x: tm set] set ❙
// the property of being a function❙
functionHood_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[x:tm set] ∀ͭ[y:tm set] x =ͭ y ⇒ (funcAppl @ a @ b @ f @ x) =ͭ (funcAppl @ a @ b @ f @ y) ❙
// functional extensionality❙
functExt_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ((∀ͭ[x:tm set] (funcAppl @ a @ b @ f @ x) =ͭ (funcAppl @ a @ b @ g @ x)) ⇒ f =ͭ g) ❙
// composition of functions❙
concat : tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [c: tm set] Πͭ [f: tm set] Πͭ [g: tm set] set ❙
concatAppl_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[c:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ∀ͭ[x:tm set]
(funcAppl @ a @ c @ (concat @ a @ b @ c @ f @ g) @ x) =ͭ (funcAppl @ b @ c @ f @ (funcAppl @ a @ b @ g @ x)) ❙
// Lemma 1: associativity of compositions a -f-> b -g-> c -h-> d when applied to an argument x❙
concatAssocAppl: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[c:tm set] ∀ͭ[d:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ∀ͭ[h:tm set] ∀ͭ[x:tm set]
(funcAppl @ a @ d @ (funcAppl @ a @ c @ (concat @ a @ b @ c @ f @ g) @ x) @ x) =ͭ (funcAppl @ a @ d @ (funcAppl @ b @ c @ f @ (funcAppl @ a @ b @ g @ x)) @ x) ❘ = PROVE❙
(funcAppl @ a @ d @ (funcAppl @ a @ c @ (concat @ a @ b @ c @ f @ g) @ x) @ x) =ͭ (funcAppl @ a @ d @ (funcAppl @ b @ c @ f @ (funcAppl @ a @ b @ g @ x)) @ x) ❘ = PROVE❙
// Lemma 2: as Lemma 1, but without the argument x❙
concatAssoc: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[c:tm set] ∀ͭ[d:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ∀ͭ[h:tm set]
((((concat @ a) @ c) @ d) @ f) @ (((((concat @ a) @ b) @ c) @ g) @ h) =ͭ ((((concat @ a) @ b) @ d) @ (((((concat @ b) @ c) @ d) @ f) @ g)) @ h ❘ = PROVE❙
// basic definitions on functions (all stated as a primitive constant with a defining axiom)❙
injective: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] bool ❙
injective_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (injective @ a @ b @ f) ⇔ (∀ͭ[x:tm set] ∀ͭ[y:tm set] (funcAppl @ a @ b @ f @ x) =ͭ (funcAppl @ a @ b @ f @ y) ⇒ (x =ͭ y)) ❙
surjective: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] bool ❙
surjective_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (surjective @ a @ b @ f) ⇔ (∀ͭ[y:tm set] ∃ͭ[x:tm set] (funcAppl @ a @ b @ f @ x) =ͭ y) ❙
bijective: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] bool ❙
bijective_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (bijective @ a @ b @ f) ⇔ ((injective @ a @ b @ f) ∧ (surjective @ a @ b @ f)) ❙
left_inverse: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] Πͭ [g: tm set] bool ❙
left_inverse_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] (left_inverse @ a @ b @ f @ g) ⇔ (∀ͭ[x:tm set] ( (funcAppl @ a @ a @ (concat @ a @ b @ a @ g @ f) @ x) =ͭ x) ) ❙
right_inverse: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] Πͭ [g: tm set] bool ❙
right_inverse_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ((right_inverse @ a @ b @ f @ g) ⇔ (∀ͭ[x:tm set] ( (funcAppl @ b @ b @ (concat @ b @ a @ b @ f @ g) @ x) =ͭ x) )) ❙
// f and g are inverse❙
inverse: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] Πͭ [g: tm set] bool ❙
inverse_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] (inverse @ a @ b @ f @ g) ⇔ ((left_inverse @ a @ b @ f @ g) ∧ (right_inverse @ a @ b @ f @ g)) ❙
// properties of the above❙
// Lemma 3: g is a left inverse of f iff f is a right inverse of g❙
left_right_inverses: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] (left_inverse @ a @ b @ f @ g) ⇔ (right_inverse @ b @ a @ g @ f) ❘ = PROVE ❙
// Lemma 4: functions with left-inverses are injective❙
left_inverse_injective: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (∃ͭ[g:tm set] left_inverse @ a @ b @ f @ g) ⇒ injective @ a @ b @ f ❘ = PROVE ❙
// Lemma 5: functions with right-inverses are surjective❙
right_inverse_surjective: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (∃ͭ[g:tm set] right_inverse @ a @ b @ f @ g) ⇒ surjective @ a @ b @ f ❘ = PROVE ❙
// Lemma 6: functions with inverses are bijections❙
inverses_bijective: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (∃ͭ[g:tm set] inverse @ a @ b @ f @ g) ⇒ bijective @ a @ b @ f ❘ = PROVE ❙
concatAssoc: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[c:tm set] ∀ͭ[d:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ∀ͭ[h:tm set]
((((concat @ a) @ c) @ d) @ f) @ (((((concat @ a) @ b) @ c) @ g) @ h) =ͭ ((((concat @ a) @ b) @ d) @ (((((concat @ b) @ c) @ d) @ f) @ g)) @ h ❘ = PROVE❙
// basic definitions on functions (all stated as a primitive constant with a defining axiom)❙
injective: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] bool ❙
injective_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (injective @ a @ b @ f) ⇔ (∀ͭ[x:tm set] ∀ͭ[y:tm set] (funcAppl @ a @ b @ f @ x) =ͭ (funcAppl @ a @ b @ f @ y) ⇒ (x =ͭ y)) ❙
surjective: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] bool ❙
surjective_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (surjective @ a @ b @ f) ⇔ (∀ͭ[y:tm set] ∃ͭ[x:tm set] (funcAppl @ a @ b @ f @ x) =ͭ y) ❙
bijective: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] bool ❙
bijective_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (bijective @ a @ b @ f) ⇔ ((injective @ a @ b @ f) ∧ (surjective @ a @ b @ f)) ❙
left_inverse: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] Πͭ [g: tm set] bool ❙
left_inverse_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] (left_inverse @ a @ b @ f @ g) ⇔ (∀ͭ[x:tm set] ( (funcAppl @ a @ a @ (concat @ a @ b @ a @ g @ f) @ x) =ͭ x) ) ❙
right_inverse: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] Πͭ [g: tm set] bool ❙
right_inverse_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] ((right_inverse @ a @ b @ f @ g) ⇔ (∀ͭ[x:tm set] ( (funcAppl @ b @ b @ (concat @ b @ a @ b @ f @ g) @ x) =ͭ x) )) ❙
// f and g are inverse❙
inverse: tm Πͭ [a: tm set] Πͭ [b: tm set] Πͭ [f: tm set] Πͭ [g: tm set] bool ❙
inverse_ax: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] (inverse @ a @ b @ f @ g) ⇔ ((left_inverse @ a @ b @ f @ g) ∧ (right_inverse @ a @ b @ f @ g)) ❙
// properties of the above❙
// Lemma 3: g is a left inverse of f iff f is a right inverse of g❙
left_right_inverses: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] ∀ͭ[g:tm set] (left_inverse @ a @ b @ f @ g) ⇔ (right_inverse @ b @ a @ g @ f) ❘ = PROVE ❙
// Lemma 4: functions with left-inverses are injective❙
left_inverse_injective: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (∃ͭ[g:tm set] left_inverse @ a @ b @ f @ g) ⇒ injective @ a @ b @ f ❘ = PROVE ❙
// Lemma 5: functions with right-inverses are surjective❙
right_inverse_surjective: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (∃ͭ[g:tm set] right_inverse @ a @ b @ f @ g) ⇒ surjective @ a @ b @ f ❘ = PROVE ❙
// Lemma 6: functions with inverses are bijections❙
inverses_bijective: ⊦ ∀ͭ[a:tm set] ∀ͭ[b:tm set] ∀ͭ[f:tm set] (∃ͭ[g:tm set] inverse @ a @ b @ f @ g) ⇒ bijective @ a @ b @ f ❘ = PROVE ❙
❚
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment