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

minor edits

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

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

@ -1014,15 +1014,25 @@ 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′
``` ```
So the inversion principle for functions can be stated as
v ↦ w ⊑ u
---------------
→ factor u u′ v w
We prove the inversion principle for functions by induction on the We prove the inversion principle for functions by induction on the
derivation of the less-than relation. To make the induction hypothesis derivation of the less-than relation. To make the induction hypothesis
stronger, we broaden the premise to `u₁ ⊑ u₂` (instead of `v ↦ w ⊑ stronger, we broaden the premise `v ↦ w ⊑ u` to `u₁ ⊑ u₂`, and
u`), and strengthen the conclusion to say that for _every_ function strengthen the conclusion to say that for _every_ function value
value `v ↦ w ∈ u₁`, we have that `v ↦ w` factors `u₂` into some `v ↦ w ∈ u₁`, we have that `v ↦ w` factors `u₂` into some value `u₃`.
value `u₃`.
→ u₁ ⊑ u₂
------------------------------------------------------
→ ∀{v w} → v ↦ w ∈ u₁ → Σ[ u₃ ∈ Value ] factor u₂ u₃ v w
### Inversion of less-than for functions, the case for ⊑-trans ### Inversion of less-than for functions, the case for ⊑-trans