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

renamed dom and cod

Browse source
This commit is contained in:
Jeremy Siek 2020-03-11 15:55:44 -04:00
parent 6b595851d6
commit 08508f9e36
1 changed files with 47 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

93
src/plfa/part3/Denotational.lagda.md
View file

@ -953,59 +953,59 @@ function, we want to show that `v ↦ w ⊑ u` implies that `u` includes
a set of function values such that the join of their domains is less a set of function values such that the join of their domains is less
than `v` and the join of their codomains is greater than `w`. than `v` and the join of their codomains is greater than `w`.
To this end we define the following dom and cod functions. Given some To this end we define the following `⨆dom` and `⨆cod` functions. Given some
value `u` (that represents a set of entries), `dom u` returns the join of value `u` (that represents a set of entries), `⨆dom u` returns the join of
their domains and `cod u` returns the join of their codomains. their domains and `⨆cod u` returns the join of their codomains.
``` ```
dom : (u : Value) → Value ⨆dom : (u : Value) → Value
dom ⊥ = ⊥ ⨆dom ⊥ = ⊥
dom (v ↦ w) = v ⨆dom (v ↦ w) = v
dom (u ⊔ u′) = dom u ⊔ dom u′ ⨆dom (u ⊔ u′) = ⨆dom u ⊔ ⨆dom u′
cod : (u : Value) → Value ⨆cod : (u : Value) → Value
cod ⊥ = ⊥ ⨆cod ⊥ = ⊥
cod (v ↦ w) = w ⨆cod (v ↦ w) = w
cod (u ⊔ u′) = cod u ⊔ cod u′ ⨆cod (u ⊔ u′) = ⨆cod u ⊔ ⨆cod u′
``` ```
We need just one property each for `dom` and `cod`. Given a collection of We need just one property each for `⨆dom` and `⨆cod`. Given a collection of
functions represented by value `u`, and an entry `v ↦ w ∈ u`, we know functions represented by value `u`, and an entry `v ↦ w ∈ u`, we know
that `v` is included in the domain of `v`. that `v` is included in the domain of `v`.
``` ```
↦∈→⊆dom : ∀{u v w : Value} ↦∈→⊆⨆dom : ∀{u v w : Value}
→ all-funs u → (v ↦ w) ∈ u → all-funs u → (v ↦ w) ∈ u
---------------------- ----------------------
→ v ⊆ dom u → v ⊆ ⨆dom u
↦∈→⊆dom {⊥} fg () u∈v ↦∈→⊆⨆dom {⊥} fg () u∈v
↦∈→⊆dom {v ↦ w} fg refl u∈v = u∈v ↦∈→⊆⨆dom {v ↦ w} fg refl u∈v = u∈v
↦∈→⊆dom {u ⊔ u′} fg (inj₁ v↦w∈u) u∈v = ↦∈→⊆⨆dom {u ⊔ u′} fg (inj₁ v↦w∈u) u∈v =
let ih = ↦∈→⊆dom (λ z → fg (inj₁ z)) v↦w∈u in let ih = ↦∈→⊆⨆dom (λ z → fg (inj₁ z)) v↦w∈u in
inj₁ (ih u∈v) inj₁ (ih u∈v)
↦∈→⊆dom {u ⊔ u′} fg (inj₂ v↦w∈u′) u∈v = ↦∈→⊆⨆dom {u ⊔ u′} fg (inj₂ v↦w∈u′) u∈v =
let ih = ↦∈→⊆dom (λ z → fg (inj₂ z)) v↦w∈u′ in let ih = ↦∈→⊆⨆dom (λ z → fg (inj₂ z)) v↦w∈u′ in
inj₂ (ih u∈v) inj₂ (ih u∈v)
``` ```
Regarding `cod`, suppose we have a collection of functions represented Regarding `⨆cod`, suppose we have a collection of functions represented
by `u`, but all of them are just copies of `v ↦ w`. Then the `cod u` is by `u`, but all of them are just copies of `v ↦ w`. Then the `⨆cod u` is
included in `w`. included in `w`.
``` ```
⊆↦→cod⊆ : ∀{u v w : Value} ⊆↦→⨆cod⊆ : ∀{u v w : Value}
→ u ⊆ v ↦ w → u ⊆ v ↦ w
--------- ---------
→ cod u ⊆ w → ⨆cod u ⊆ w
⊆↦→cod⊆ {⊥} s refl with s {⊥} refl ⊆↦→⨆cod⊆ {⊥} s refl with s {⊥} refl
... | () ... | ()
⊆↦→cod⊆ {C ↦ C′} s m with s {C ↦ C′} refl ⊆↦→⨆cod⊆ {C ↦ C′} s m with s {C ↦ C′} refl
... | refl = m ... | refl = m
⊆↦→cod⊆ {u ⊔ u′} s (inj₁ x) = ⊆↦→cod⊆ (λ {C} z → s (inj₁ z)) x ⊆↦→⨆cod⊆ {u ⊔ u′} s (inj₁ x) = ⊆↦→⨆cod⊆ (λ {C} z → s (inj₁ z)) x
⊆↦→cod⊆ {u ⊔ u′} s (inj₂ y) = ⊆↦→cod⊆ (λ {C} z → s (inj₂ z)) y ⊆↦→⨆cod⊆ {u ⊔ u′} s (inj₂ y) = ⊆↦→⨆cod⊆ (λ {C} z → s (inj₂ z)) y
``` ```
With the `dom` and `cod` functions in hand, we can make precise the With the `⨆dom` and `⨆cod` functions in hand, we can make precise the
conclusion of the inversion principle for functions, which we package conclusion of the inversion principle for functions, which we package
into the following predicate named `factor`. We say that `v ↦ w` into the following predicate named `factor`. We say that `v ↦ w`
_factors_ `u` into `u′` if `u′` is a included in `u`, if `u′` contains only _factors_ `u` into `u′` if `u′` is a included in `u`, if `u′` contains only
@ -1014,7 +1014,7 @@ than `w`.
``` ```
factor : (u : Value) → (u′ : Value) → (v : Value) → (w : Value) → Set factor : (u : Value) → (u′ : Value) → (v : Value) → (w : Value) → Set
factor u u′ v w = all-funs u′ × u′ ⊆ u × dom u′ ⊑ v × w ⊑ cod u′ factor u u′ v w = all-funs u′ × u′ ⊆ u × ⨆dom u′ ⊑ v × w ⊑ ⨆cod u′
``` ```
We prove the inversion principle for functions by induction on the We prove the inversion principle for functions by induction on the
@ -1038,7 +1038,7 @@ so we have `all-funs u′` and `u′ ⊆ u`.
By the induction hypothesis for `u ⊑ u₂`, we know By the induction hypothesis for `u ⊑ u₂`, we know
that for any `v′ ↦ w′ ∈ u`, `v′ ↦ w′` factors `u₂` into `u₃`. that for any `v′ ↦ w′ ∈ u`, `v′ ↦ w′` factors `u₂` into `u₃`.
With these facts in hand, we proceed by induction on `u′` With these facts in hand, we proceed by induction on `u′`
to prove that `(dom u′) ↦ (cod u′)` factors `u₂` into `u₃`. to prove that `(⨆dom u′) ↦ (⨆cod u′)` factors `u₂` into `u₃`.
We discuss each case of the proof in the text below. We discuss each case of the proof in the text below.
``` ```
@ -1046,7 +1046,7 @@ sub-inv-trans : ∀{u′ u₂ u : Value}
→ all-funs u′ → u′ ⊆ u → all-funs u′ → u′ ⊆ u
→ (∀{v′ w′} → v′ ↦ w′ ∈ u → Σ[ u₃ ∈ Value ] factor u₂ u₃ v′ w′) → (∀{v′ w′} → v′ ↦ w′ ∈ u → Σ[ u₃ ∈ Value ] factor u₂ u₃ v′ w′)
--------------------------------------------------------------- ---------------------------------------------------------------
→ Σ[ u₃ ∈ Value ] factor u₂ u₃ (dom u′) (cod u′) → Σ[ u₃ ∈ Value ] factor u₂ u₃ (⨆dom u′) (⨆cod u′)
sub-inv-trans {⊥} {u₂} {u} fu′ u′⊆u IH = sub-inv-trans {⊥} {u₂} {u} fu′ u′⊆u IH =
⊥-elim (contradiction (fu′ refl) ¬Fun⊥) ⊥-elim (contradiction (fu′ refl) ¬Fun⊥)
sub-inv-trans {u₁′ ↦ u₂′} {u₂} {u} fg u′⊆u IH = IH (↦⊆→∈ u′⊆u) sub-inv-trans {u₁′ ↦ u₂′} {u₂} {u} fg u′⊆u IH = IH (↦⊆→∈ u′⊆u)
@ -1074,18 +1074,18 @@ sub-inv-trans {u₁′ ⊔ u₂′} {u₂} {u} fg u′⊆u IH
* Suppose `u′ ≡ u₁′ ↦ u₂′`. Then `u₁′ ↦ u₂′ ∈ u` and we can apply the * Suppose `u′ ≡ u₁′ ↦ u₂′`. Then `u₁′ ↦ u₂′ ∈ u` and we can apply the
premise (the induction hypothesis from `u ⊑ u₂`) to obtain that premise (the induction hypothesis from `u ⊑ u₂`) to obtain that
`u₁′ ↦ u₂′` factors of `u₂ into u₂′`. This case is complete because `u₁′ ↦ u₂′` factors of `u₂ into u₂′`. This case is complete because
`dom u′ ≡ u₁′` and `cod u′ ≡ u₂′`. `⨆dom u′ ≡ u₁′` and `⨆cod u′ ≡ u₂′`.
* Suppose `u′ ≡ u₁′ ⊔ u₂′`. Then we have `u₁′ ⊆ u` and `u₂′ ⊆ u`. We also * Suppose `u′ ≡ u₁′ ⊔ u₂′`. Then we have `u₁′ ⊆ u` and `u₂′ ⊆ u`. We also
have `all-funs u₁′` and `all-funs u₂′`, so we can apply the induction hypothesis have `all-funs u₁′` and `all-funs u₂′`, so we can apply the induction hypothesis
for both `u₁′` and `u₂′`. So there exists values `u₃₁` and `u₃₂` such that for both `u₁′` and `u₂′`. So there exists values `u₃₁` and `u₃₂` such that
`(dom u₁′) ↦ (cod u₁′)` factors `u` into `u₃₁` and `(⨆dom u₁′) ↦ (⨆cod u₁′)` factors `u` into `u₃₁` and
`(dom u₂′) ↦ (cod u₂′)` factors `u` into `u₃₂`. `(⨆dom u₂′) ↦ (⨆cod u₂′)` factors `u` into `u₃₂`.
We will show that `(dom u) ↦ (cod u)` factors `u` into `u₃₁ ⊔ u₃₂`. We will show that `(⨆dom u) ↦ (⨆cod u)` factors `u` into `u₃₁ ⊔ u₃₂`.
So we need to show that So we need to show that
dom (u₃₁ ⊔ u₃₂) ⊑ dom (u₁′ ⊔ u₂′) ⨆dom (u₃₁ ⊔ u₃₂) ⊑ ⨆dom (u₁′ ⊔ u₂′)
cod (u₁′ ⊔ u₂′) ⊑ cod (u₃₁ ⊔ u₃₂) ⨆cod (u₁′ ⊔ u₂′) ⊑ ⨆cod (u₃₁ ⊔ u₃₂)
But those both follow directly from the factoring of But those both follow directly from the factoring of
`u` into `u₃₁` and `u₃₂`, using the monotonicity of `⊔` with respect to `⊑`. `u` into `u₃₁` and `u₃₂`, using the monotonicity of `⊔` with respect to `⊑`.
@ -1183,10 +1183,10 @@ Let `v` and `w` be arbitrary values.
By the induction hypothesis for `u ⊑ u₂`, we know By the induction hypothesis for `u ⊑ u₂`, we know
that for any `v′ ↦ w′ ∈ u`, `v′ ↦ w′` factors `u₂`. that for any `v′ ↦ w′ ∈ u`, `v′ ↦ w′` factors `u₂`.
Now we apply the lemma sub-inv-trans, which gives us Now we apply the lemma sub-inv-trans, which gives us
some `u₃` such that `(dom u′) ↦ (cod u′)` factors `u₂` into `u₃`. some `u₃` such that `(⨆dom u′) ↦ (⨆cod u′)` factors `u₂` into `u₃`.
We show that `v ↦ w` also factors `u₂` into `u₃`. We show that `v ↦ w` also factors `u₂` into `u₃`.
From `dom u₃ ⊑ dom u′` and `dom u′ ⊑ v`, we have `dom u₃ ⊑ v`. From `⨆dom u₃ ⊑ ⨆dom u′` and `⨆dom u′ ⊑ v`, we have `⨆dom u₃ ⊑ v`.
From `w ⊑ cod u′` and `cod u′ ⊑ cod u₃`, we have `w ⊑ cod u₃`, From `w ⊑ ⨆cod u′` and `⨆cod u′ ⊑ ⨆cod u₃`, we have `w ⊑ ⨆cod u₃`,
and this case is complete. and this case is complete.
* Case `⊑-fun`. * Case `⊑-fun`.
@ -1197,7 +1197,7 @@ Let `v` and `w` be arbitrary values.
Given that `v ↦ w ∈ u₁₁ ↦ u₁₂`, we have `v ≡ u₁₁` and `w ≡ u₁₂`. Given that `v ↦ w ∈ u₁₁ ↦ u₁₂`, we have `v ≡ u₁₁` and `w ≡ u₁₂`.
We show that `u₁₁ ↦ u₁₂` factors `u₂₁ ↦ u₂₂` into itself. We show that `u₁₁ ↦ u₁₂` factors `u₂₁ ↦ u₂₂` into itself.
We need to show that `dom (u₂₁ ↦ u₂₂) ⊑ u₁₁` and `u₁₂ ⊑ cod (u₂₁ ↦ u₂₂)`, We need to show that `⨆dom (u₂₁ ↦ u₂₂) ⊑ u₁₁` and `u₁₂ ⊑ ⨆cod (u₂₁ ↦ u₂₂)`,
but that is equivalent to our premises `u₂₁ ⊑ u₁₁` and `u₁₂ ⊑ u₂₂`. but that is equivalent to our premises `u₂₁ ⊑ u₁₁` and `u₁₂ ⊑ u₂₂`.
* Case `⊑-dist`. * Case `⊑-dist`.
@ -1223,13 +1223,13 @@ sub-inv-fun : ∀{v w u₁ : Value}
→ (v ↦ w) ⊑ u₁ → (v ↦ w) ⊑ u₁
----------------------------------------------------- -----------------------------------------------------
→ Σ[ u₂ ∈ Value ] all-funs u₂ × u₂ ⊆ u₁ → Σ[ u₂ ∈ Value ] all-funs u₂ × u₂ ⊆ u₁
× (∀{v′ w′} → (v′ ↦ w′) ∈ u₂ → v′ ⊑ v) × w ⊑ cod u₂ × (∀{v′ w′} → (v′ ↦ w′) ∈ u₂ → v′ ⊑ v) × w ⊑ ⨆cod u₂
sub-inv-fun{v}{w}{u₁} abc sub-inv-fun{v}{w}{u₁} abc
with sub-inv abc {v}{w} refl with sub-inv abc {v}{w} refl
... | ⟨ u₂ , ⟨ f , ⟨ u₂⊆u₁ , ⟨ db , cc ⟩ ⟩ ⟩ ⟩ = ... | ⟨ u₂ , ⟨ f , ⟨ u₂⊆u₁ , ⟨ db , cc ⟩ ⟩ ⟩ ⟩ =
⟨ u₂ , ⟨ f , ⟨ u₂⊆u₁ , ⟨ G , cc ⟩ ⟩ ⟩ ⟩ ⟨ u₂ , ⟨ f , ⟨ u₂⊆u₁ , ⟨ G , cc ⟩ ⟩ ⟩ ⟩
where G : ∀{D E} → (D ↦ E) ∈ u₂ → D ⊑ v where G : ∀{D E} → (D ↦ E) ∈ u₂ → D ⊑ v
G{D}{E} m = ⊑-trans (⊆→⊑ (↦∈→⊆dom f m)) db G{D}{E} m = ⊑-trans (⊆→⊑ (↦∈→⊆⨆dom f m)) db
``` ```
The second corollary is the inversion rule that one would expect for The second corollary is the inversion rule that one would expect for
@ -1247,8 +1247,8 @@ less-than with functions on the left and right-hand sides.
... | ⟨ u , ⟨ u′ , u↦u′∈Γ ⟩ ⟩ ... | ⟨ u , ⟨ u′ , u↦u′∈Γ ⟩ ⟩
with Γ⊆v34 u↦u′∈Γ with Γ⊆v34 u↦u′∈Γ
... | refl = ... | refl =
let codΓ⊆w′ = ⊆↦→cod⊆ Γ⊆v34 in let ⨆codΓ⊆w′ = ⊆↦→⨆cod⊆ Γ⊆v34 in
⟨ lt1 u↦u′∈Γ , ⊑-trans lt2 (⊆→⊑ codΓ⊆w′) ⟩ ⟨ lt1 u↦u′∈Γ , ⊑-trans lt2 (⊆→⊑ ⨆codΓ⊆w′) ⟩
``` ```
@ -1356,6 +1356,7 @@ This chapter uses the following unicode:
↦ U+21A6 RIGHTWARDS ARROW FROM BAR (\mapsto) ↦ U+21A6 RIGHTWARDS ARROW FROM BAR (\mapsto)
⊔ U+2294 SQUARE CUP (\lub) ⊔ U+2294 SQUARE CUP (\lub)
⊑ U+2291 SQUARE IMAGE OF OR EQUAL TO (\sqsubseteq) ⊑ U+2291 SQUARE IMAGE OF OR EQUAL TO (\sqsubseteq)
⨆ U+2A06 N-ARY SQUARE UNION OPERATOR (\Lub)
⊢ U+22A2 RIGHT TACK (\|- or \vdash) ⊢ U+22A2 RIGHT TACK (\|- or \vdash)
↓ U+2193 DOWNWARDS ARROW (\d) ↓ U+2193 DOWNWARDS ARROW (\d)
ᶜ U+1D9C MODIFIER LETTER SMALL C (\^c) ᶜ U+1D9C MODIFIER LETTER SMALL C (\^c)