From d63758972bf5b168f9826a4c6b9cd065b6f48f30 Mon Sep 17 00:00:00 2001 From: jlh <48520973+Jlh18@users.noreply.github.com> Date: Sun, 17 Apr 2022 10:28:26 +0100 Subject: [PATCH] Delete 0Trinitarianism/bin directory --- 0Trinitarianism/bin/AsProps/Quest0.agda | 216 ----------------- .../bin/AsProps/Quest0Preamble.agda | 12 - .../bin/AsProps/Quest0Solutions.agda | 43 ---- .../bin/AsProps/Quest0Solutions.lagda.md | 39 --- 0Trinitarianism/bin/AsProps/Quest1.agda | 13 - 0Trinitarianism/bin/AsTypes/Quest0.agda | 227 ------------------ 6 files changed, 550 deletions(-) delete mode 100644 0Trinitarianism/bin/AsProps/Quest0.agda delete mode 100644 0Trinitarianism/bin/AsProps/Quest0Preamble.agda delete mode 100644 0Trinitarianism/bin/AsProps/Quest0Solutions.agda delete mode 100644 0Trinitarianism/bin/AsProps/Quest0Solutions.lagda.md delete mode 100644 0Trinitarianism/bin/AsProps/Quest1.agda delete mode 100644 0Trinitarianism/bin/AsTypes/Quest0.agda diff --git a/0Trinitarianism/bin/AsProps/Quest0.agda b/0Trinitarianism/bin/AsProps/Quest0.agda deleted file mode 100644 index d0ecb38..0000000 --- a/0Trinitarianism/bin/AsProps/Quest0.agda +++ /dev/null @@ -1,216 +0,0 @@ -module Trinitarianism.AsProps.Quest0 where -open import Trinitarianism.AsProps.Quest0Preamble - -{- - Here are some things that we could like to have in a logical framework - * Propositions (with the data of proofs) - * Objects to reason about with propositions - - To make propositions we want - * False ⊥ - * True ⊤ - * Or ∨ - * And ∧ - * Implication → - - but propositions are useless if they're not talking about anything, - so we also want - * Predicates - * Exists ∃ - * For all ∀ - * Equality ≡ (of objects) --} - --- Here is how we define 'true' -data ⊤ : Prop where - trivial : ⊤ - -{- It reads '⊤ is a proposition and there is a proof of it, called "trivial"'. -} - --- Here is how we define 'false' -data ⊥ : Prop where - -{- This says that ⊥ is the proposition where there are no proofs of it. -} - -{- -Given two propositions P and Q, we can form a new proposition 'P implies Q' -written P → Q -To introduce a proof of P → Q we assume a proof x of P and give a proof y of Q - -Here is an example demonstrating → in action --} - -TrueToTrue : ⊤ → ⊤ -TrueToTrue = ? - -{- - * press C-c C-l (this means Ctrl-c Ctrl-l) to load the document, - and now you can fill the holes - * navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward) - * press C-c C-r and agda will try to help you (r for refine) - * you should see λ x → { } - * navigate to the new hole - * C-c C-, to check what agda wants in the hole (C-c C-comma) - * the Goal area should look like - - Goal: ⊤ - ———————————————————————————————————————————————————————————— - x : ⊤ - - * this means you have a proof of ⊤ 'x : ⊤' and you need to give a proof of ⊤ - * you can now give it a proof of ⊤ and press C-c C-SPC to fill the hole - - There is more than one proof (see solutions) - are they the same? --} - -{- -Let's assume we have the following the naturals ℕ -and try to define the 'predicate on ℕ' given by 'x is 0' --} -isZero : ℕ → Prop -isZero zero = ? -isZero (suc n) = ? - -{- -Here's how: - * when x is zero, we give the proposition ⊤ - (try typing it in by writing \top then pressing C-c C-SPC) - * when x is suc n (i.e. 'n + 1', suc for successor) we give ⊥ (\bot) -This is technically using induction - see AsTypes. - -In general a 'predicate on ℕ' is just a 'function' P : ℕ → Prop --} - -{- -You can check if zero is indeed zero by clicking C-c C-n, -which brings up a thing on the bottom saying 'Expression', -and you can type the following -isZero zero -isZero (suc zero) -isZero (suc (suc zero)) -... --} - -{- -We can prove that 'there exists a natural number that isZero' -in set theory we might write - ∃ x ∈ ℕ, x = 0 -which in agda noation is - Σ ℕ isZero - -In general if we have predicate P : ℕ → Prop we would write - Σ ℕ P -for - ∃ x ∈ ℕ, P x - -To formulate the result Σ ℕ isZero we need to define -a proof of it --} -ExistsZero : Σ ℕ isZero -ExistsZero = ? - -{- -To fill the hole, we need to give a natural and a proof that it is zero. -Agda will give the syntax you need: - * navigate to the correct hole then refine using C-c C-r - * there are now two holes - but which is which? - * navigate to the first holes and type C-c C-, - - for the first hole it will ask you to give it a natural 'Goal: ℕ' - - for the second hole it will ask you for a proof that - whatever you put in the first hole is zero 'Goal: isZero ?0' for example - * try to fill both holes, using C-c C-SPC as before - * for the second hole you can try also C-c C-r, - Agda knows there is an obvious proof! --} - -{- -Let's show 'if all natural numbers are zero then we have a contradiction', -where 'a contradiction' is a proof of ⊥. -In maths we would write - (∀ x ∈ ℕ, x = 0) → ⊥ -and the agda notation for this is - ((x : ℕ) → isZero x) → ⊥ - -In general if we have a predicate P : ℕ → Prop then we write - (x : ℕ) → P x -to mean - ∀ x ∈ ℕ, P x --} - -AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥ -AllZero→⊥ = ? - -{- -Here is how we prove it in maths - * assume hypothesis h, a proof of (x : ℕ) → isZero x - * apply the hypothesis h to 1, deducing isZero 1, i.e. we get a proof of isZero 1 - * notice isZero 1 IS ⊥ - -Here is how you can prove it here - * navigate to the hole and check the goal - * to assume the hypothesis (x : ℕ) → isZero x, - type an h in front like so - AllZero→⊥ h = { } - * now do - * C-c C-l to load the file - * navigate to the new hole and check the new goal - * type h in the hole, type C-c C-r - * this should give h { } - * navigate to the new hole and check the Goal - * Explanation - * (h x) is a proof of isZero x for each x - * it's now asking for a natural x such that isZero x is ⊥ - * Try filling the hole with 0 and 1 and see what Agda says --} - -{- -Let's try to show the mathematical statement -'any natural n is 0 or not' -but we need a definition of 'or' --} -data OR (P Q : Prop) : Prop where - left : P → OR P Q - right : Q → OR P Q -{- -This reads - * Given propositions P and Q we have another proposition P or Q - * There are two ways of proving P or Q - * given a proof of P, left sends this to a proof of P or Q - * given a proof of Q, right sends this to a proof of P or Q - -Agda supports nice notation using underscores. --} - -data _∨_ (P Q : Prop) : Prop where - left : P → P ∨ Q - right : Q → P ∨ Q - -{- -[Important note] -Agda is sensitive to spaces so these are bad - -data _ ∨ _ (P Q : Prop) : Prop where - left : P → P ∨ Q - right : Q → P ∨ Q - -data _∨_ (P Q : Prop) : Prop where - left : P → P∨Q - right : Q → P∨Q - -it is also sensitive to indentation so these are also bad - -data _∨_ (P Q : Prop) : Prop where -left : P → P ∨ Q -right : Q → P ∨ Q - --} - -{- -Now we can prove it! -This technically uses induction - see AsTypes. -Fill the missing part of the theorem statement. -You need to first uncomment this by getting rid of the -- in front (C-x C-;) --} --- DecidableIsZero : (n : ℕ) → {!!} --- DecidableIsZero zero = {!!} --- DecidableIsZero (suc n) = {!!} diff --git a/0Trinitarianism/bin/AsProps/Quest0Preamble.agda b/0Trinitarianism/bin/AsProps/Quest0Preamble.agda deleted file mode 100644 index 6a0a871..0000000 --- a/0Trinitarianism/bin/AsProps/Quest0Preamble.agda +++ /dev/null @@ -1,12 +0,0 @@ - -module Trinitarianism.AsProps.Quest0Preamble where - -open import Cubical.Core.Everything hiding (_∨_) public -open import Cubical.Data.Nat public - -private - postulate - u : Level - -Prop = Type u - diff --git a/0Trinitarianism/bin/AsProps/Quest0Solutions.agda b/0Trinitarianism/bin/AsProps/Quest0Solutions.agda deleted file mode 100644 index f283373..0000000 --- a/0Trinitarianism/bin/AsProps/Quest0Solutions.agda +++ /dev/null @@ -1,43 +0,0 @@ -module Trinitarianism.Quest0Solutions where -open import Trinitarianism.Quest0Preamble - -private - postulate - u : Level - -data ⊤ : Type u where - trivial : ⊤ - -data ⊥ : Type u where - -TrueToTrue : ⊤ → ⊤ -TrueToTrue = λ x → x - -TrueToTrue' : ⊤ → ⊤ -TrueToTrue' x = x - -TrueToTrue'' : ⊤ → ⊤ -TrueToTrue'' trivial = trivial - -TrueToTrue''' : ⊤ → ⊤ -TrueToTrue''' x = trivial - -isZero : ℕ → Type u -isZero zero = ⊤ -isZero (suc n) = ⊥ - -ExistsZero : Σ ℕ isZero -ExistsZero = zero , trivial - -AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥ -AllZero→⊥ h = h 1 - -data _∨_ (P Q : Type u) : Type u where - left : P → P ∨ Q - right : Q → P ∨ Q - -DecidableIsZero : (n : ℕ) → (isZero n) ∨ (isZero n → ⊥) -DecidableIsZero zero = left trivial -DecidableIsZero (suc n) = right (λ x → x) - - diff --git a/0Trinitarianism/bin/AsProps/Quest0Solutions.lagda.md b/0Trinitarianism/bin/AsProps/Quest0Solutions.lagda.md deleted file mode 100644 index 64b410e..0000000 --- a/0Trinitarianism/bin/AsProps/Quest0Solutions.lagda.md +++ /dev/null @@ -1,39 +0,0 @@ -```agda -module Trinitarianism.AsProps.Quest0Solutions where -open import Trinitarianism.AsProps.Quest0Preamble - -data ⊤ : Prop where - trivial : ⊤ - -data ⊥ : Prop where - -TrueToTrue : ⊤ → ⊤ -TrueToTrue = λ x → x - -TrueToTrue' : ⊤ → ⊤ -TrueToTrue' x = x - -TrueToTrue'' : ⊤ → ⊤ -TrueToTrue'' trivial = trivial - -TrueToTrue''' : ⊤ → ⊤ -TrueToTrue''' x = trivial - -isZero : ℕ → Prop -isZero zero = ⊤ -isZero (suc n) = ⊥ - -ExistsZero : Σ ℕ isZero -ExistsZero = zero , trivial - -AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥ -AllZero→⊥ h = h 1 - -data _∨_ (P Q : Prop) : Prop where - left : P → P ∨ Q - right : Q → P ∨ Q - -DecidableIsZero : (n : ℕ) → (isZero n) ∨ (isZero n → ⊥) -DecidableIsZero zero = left trivial -DecidableIsZero (suc n) = right (λ x → x) -``` diff --git a/0Trinitarianism/bin/AsProps/Quest1.agda b/0Trinitarianism/bin/AsProps/Quest1.agda deleted file mode 100644 index dc3632b..0000000 --- a/0Trinitarianism/bin/AsProps/Quest1.agda +++ /dev/null @@ -1,13 +0,0 @@ -{- -Two things being equal is also a proposition - --} - - - - --- FalseToTrue : ⊥ → ⊤ --- FalseToTrue = λ x → trivial - --- FalseToTrue' : ⊥ → ⊤ --- FalseToTrue' () diff --git a/0Trinitarianism/bin/AsTypes/Quest0.agda b/0Trinitarianism/bin/AsTypes/Quest0.agda deleted file mode 100644 index 774efe7..0000000 --- a/0Trinitarianism/bin/AsTypes/Quest0.agda +++ /dev/null @@ -1,227 +0,0 @@ -module Trinitarianism.AsTypes.Quest0 where - -open import Cubical.Core.Everything hiding (_∨_) --- ------------------------------ - -{- - In this branch, - we develop the point of view of types as constructions / programs. - - Here is our first construction. --} -data Unit : Type where - trivial : Unit -{- - This reads 'Unit is a type of construction and - there is a recipe for it, called "trivial"'. - - Here is another construction. --} - -data Empty : Type where - -{- - This says that Empty is a construction and - there are no recipes for it. --} - -{- - Given two constructions A and B, - 'converting recipes of A into recipes of B' is itself a type of construction, - written A → B. - To give a recipe of A → B, - we assume a recipe x of A and give a recipe y of B. - - Here is an example demonstrating → in action --} - -UnitToUnit : Unit → Unit -UnitToUnit = {!!} - -{- - * press C-c C-l (this means Ctrl-c Ctrl-l) to load the document, - and now you can fill the holes - * navigate to the hole { } using C-c C-f (forward) or C-c C-b (backward) - * press C-c C-r and agda will try to help you (r for refine) - * you should see λ x → { } - * navigate to the new hole - * C-c C-, to check what agda wants in the hole (C-c C-comma) - * the Goal area should look like - - Goal: Unit - ———————————————————————————————————————————————————————————— - x : Unit - - * this means you have a proof of Unit 'x : Unit' and you need to give a proof of Unit - * you can now give it a proof of Unit and press C-c C-SPC to fill the hole - - There is more than one proof (see solutions) - are they the same? --} - -{- - We can also encode "natural numbers" as a type of construction. --} -data ℕ : Type where - zero : ℕ - suc : ℕ → ℕ -{- - This reads ' - - ℕ is a type of construction - - "zero" is a recipe for ℕ - - "suc" takes an existing recipe for ℕ and gives - another recipe for ℕ. - ' --} -{- - Let's write a program that - "given a recipe n of ℕ, tells us whether it is zero". - - TODO finish this. --} -isZero : ℕ → Type -isZero zero = {!!} -isZero (suc n) = {!!} - -{- -Here's how: - * when x is zero, we give the proposition Unit - (try typing it in by writing \top then pressing C-c C-SPC) - * when x is suc n (i.e. 'n + 1', suc for successor) we give Empty (\bot) -This is technically using induction - see AsTypes. - -In general a 'predicate on ℕ' is just a 'function' P : ℕ → Type --} - -{- -You can check if zero is indeed zero by clicking C-c C-n, -which brings up a thing on the bottom saying 'Expression', -and you can type the following -isZero zero -isZero (suc zero) -isZero (suc (suc zero)) -... --} - -{- -We can prove that 'there exists a natural number that isZero' -in set theory we might write - ∃ x ∈ ℕ, x = 0 -which in agda noation is - Σ ℕ isZero - -In general if we have predicate P : ℕ → Type we would write - Σ ℕ P -for - ∃ x ∈ ℕ, P x - -To formulate the result Σ ℕ isZero we need to define -a proof of it --} -ExistsZero : Σ ℕ isZero -ExistsZero = {!!} - -{- -To fill the hole, we need to give a natural and a proof that it is zero. -Agda will give the syntax you need: - * navigate to the correct hole then refine using C-c C-r - * there are now two holes - but which is which? - * navigate to the first holes and type C-c C-, - - for the first hole it will ask you to give it a natural 'Goal: ℕ' - - for the second hole it will ask you for a proof that - whatever you put in the first hole is zero 'Goal: isZero ?0' for example - * try to fill both holes, using C-c C-SPC as before - * for the second hole you can try also C-c C-r, - Agda knows there is an obvious proof! --} - -{- -Let's show 'if all natural numbers are zero then we have a contradiction', -where 'a contradiction' is a proof of Empty. -In maths we would write - (∀ x ∈ ℕ, x = 0) → Empty -and the agda notation for this is - ((x : ℕ) → isZero x) → Empty - -In general if we have a predicate P : ℕ → Type then we write - (x : ℕ) → P x -to mean - ∀ x ∈ ℕ, P x --} - -AllZero→Empty : ((x : ℕ) → isZero x) → Empty -AllZero→Empty = {!!} - -{- -Here is how we prove it in maths - * assume hypothesis h, a proof of (x : ℕ) → isZero x - * apply the hypothesis h to 1, deducing isZero 1, i.e. we get a proof of isZero 1 - * notice isZero 1 IS Empty - -Here is how you can prove it here - * navigate to the hole and check the goal - * to assume the hypothesis (x : ℕ) → isZero x, - type an h in front like so - AllZero→Empty h = { } - * now do - * C-c C-l to load the file - * navigate to the new hole and check the new goal - * type h in the hole, type C-c C-r - * this should give h { } - * navigate to the new hole and check the Goal - * Explanation - * (h x) is a proof of isZero x for each x - * it's now asking for a natural x such that isZero x is Empty - * Try filling the hole with 0 and 1 and see what Agda says --} - -{- -Let's try to show the mathematical statement -'any natural n is 0 or not' -but we need a definition of 'or' --} -data OR (P Q : Type) : Type where - left : P → OR P Q - right : Q → OR P Q -{- -This reads - * Given propositions P and Q we have another proposition P or Q - * There are two ways of proving P or Q - * given a proof of P, left sends this to a proof of P or Q - * given a proof of Q, right sends this to a proof of P or Q - -Agda supports nice notation using underscores. --} - -data _∨_ (P Q : Type) : Type where - left : P → P ∨ Q - right : Q → P ∨ Q - -{- -[Important note] -Agda is sensitive to spaces so these are bad - -data _ ∨ _ (P Q : Type) : Type where - left : P → P ∨ Q - right : Q → P ∨ Q - -data _∨_ (P Q : Type) : Type where - left : P → P∨Q - right : Q → P∨Q - -it is also sensitive to indentation so these are also bad - -data _∨_ (P Q : Type) : Type where -left : P → P ∨ Q -right : Q → P ∨ Q - --} - -{- -Now we can prove it! -This technically uses induction - see AsTypes. -Fill the missing part of the theorem statement. -You need to first uncomment this by getting rid of the -- in front (C-x C-;) --} --- DecidableIsZero : (n : ℕ) → {!!} --- DecidableIsZero zero = {!!} --- DecidableIsZero (suc n) = {!!}