michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #588 from lorenzo-lipparini/patch-2

Browse source 
Fixing minor coding style inconsistencies in part1/Quantifiers
This commit is contained in:
Philip Wadler 2021-08-29 18:22:36 +01:00 committed by GitHub
commit cdcc12f4cc
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/plfa/part1/Quantifiers.lagda.md
View file

@ -105,7 +105,7 @@ Show that a disjunction of universals implies a universal of disjunctions:
``` ```
postulate postulate
⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} → ⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
``` ```
Does the converse hold? If so, prove; if not, explain why. Does the converse hold? If so, prove; if not, explain why.
@ -463,21 +463,21 @@ And to establish the following properties:
to (from b) ≡ b to (from b) ≡ b
Using the above, establish that there is an isomorphism between `ℕ` and Using the above, establish that there is an isomorphism between `ℕ` and
`∃[ b ](Can b)`. `∃[ b ] Can b`.
We recommend proving the following lemmas which show that, for a given We recommend proving the following lemmas which show that, for a given
binary number `b`, there is only one proof of `One b` and similarly binary number `b`, there is only one proof of `One b` and similarly
for `Can b`. for `Can b`.
≡One : ∀{b : Bin} (o o' : One b) → o ≡ o' ≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′
≡Can : ∀{b : Bin} (cb : Can b) (cb' : Can b) → cb ≡ cb' ≡Can : ∀ {b : Bin} (cb cb′ : Can b) → cb ≡ cb′
Many of the alternatives for proving `to∘from` turn out to be tricky. Many of the alternatives for proving `to∘from` turn out to be tricky.
However, the proof can be straightforward if you use the following lemma, However, the proof can be straightforward if you use the following lemma,
which is a corollary of `≡Can`. which is a corollary of `≡Can`.
proj₁≡→Can≡ : {cb cb′ : ∃[ b ](Can b)} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′ proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
``` ```
-- Your code goes here -- Your code goes here