From ea42753758afead48455446d056514a51144f8b8 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Sat, 18 Jan 2020 21:38:42 -0500 Subject: [PATCH] added hints to Bin-isomorphism exercise --- src/plfa/part1/Quantifiers.lagda.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index 545626d9..559560ce 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -463,6 +463,24 @@ And to establish the following properties: Using the above, establish that there is an isomorphism between `ℕ` and `∃[ b ](Can b)`. +We recommend proving following lemmas which show that, for a given +binary number `b`, there is only one proof of `One b` and similarly +for `Can b`. + + ≡One : ∀{b : Bin} (o o' : One b) → o ≡ o' + + ≡Can : ∀{b : Bin} (cb : Can b) (cb' : Can b) → cb ≡ cb' + +The proof of `to∘from` is tricky. We recommend proving the following lemma + + to∘from-aux : ∀ (b : Bin) (cb : Can b) → to (from b) ≡ b + → _≡_ {_} {∃[ b ](Can b)} ⟨ to (from b) , canon-to (from b) ⟩ ⟨ b , cb ⟩ + +You cannot immediately use `≡Can` to equate `canon-to (from b)` and +`cb` because they have different types: `Can (to (from b))` and `Can b` +respectively. You must first get their types to be equal, which +can be done by changing the type of `cb` using `rewrite`. + ``` -- Your code goes here ```