[Agda] Question, re: x-dual-U exercise in Negation chapter of PLFA.

[James Wood]

Hi David,

I don't want to give the answer to the exercise away, but I will try to
explain mechanically what's going on.

You should notice, before writing `to∘from`, that the underscore in the
`to` field is highlighted yellow. This means that, by writing the
underscore, you have asked Agda's type checker to fill this expression
in, but the type checker has not been able to. However, you are free to
fill in more holes in the file, in case filling in any of them holes
gives it enough of a clue to work it out.

Then, when you go to write `from∘to`, your proof does give enough of a
clue to solve the previous underscore: it should be solved to
`snd(.patternInTele0)`, i.e, the underscore in `λ (a , _) → refl`, which
is of type `B`. But then we hit a problem: whereas the `a` in `from∘to`
an the `a` in `to` basically line up, there is no equivalent to
`snd(.patternInTele0)` in scope within `to`. Indeed, if you put a hole
in place of the underscore in `to`, you'll notice that you're never
going to find a `B` to put there, unless you swap `inj₁` for `inj₂`,
losing your `A`. The “Cannot instantiate the metavariable [...] since it
contains the variable [...] which is not in scope of the metavariable”
error basically means that you're requiring something earlier in a proof
to know something later, where the thing later has assumptions not made
earlier. `to` can't be implemented purely by virtue of `from∘to` being
provable – that would be cyclic.

As for tackling this problem, I would first focus on whether you can
implement `to` and `from` independent of their proofs and without any
yellow. This should be instructive as to what the full solution will be.
It looks like `from` is already fine.

I hope this helps,
James

On 22/08/2020 22:48, David Banas wrote:
> Hi all,
> 
> In trying to answer the following question from the /Negation/ chapter
> of PLFA:
> 
> Do we also have the following?
> 
> |¬ (A × B) ≃ (¬ A) ⊎ (¬ B) |
> 
> If so, prove; if not, can you give a relation weaker than isomorphism
> that relates the two sides?
> 
> It seems to me that I ought to be able to define an /embedding/. That
> is, I should /not/ have to settle for just an /equivalence/:
> 
>     ×-dual-⊎ : ∀ {A B : Set}
>         -------------------------
>       → ¬ (A × B) ≲ (¬ A) ⊎ (¬ B)
>     ×-dual-⊎ =
>       record
>         { to      = λ ¬A×B → inj₁ (λ a → ¬A×B (a , _))
>         ; from    = λ { (inj₁ ¬A) → λ (a , _) → ¬A a
>                       ; (inj₂ ¬B) → λ (_ , b) → ¬B b
>                       }
>         ; from∘to = λ ¬A×B → extensionality (λ (a , _) → refl
>         -- ; to∘from = λ { (inj₁ ¬A) → -- We could write this one.
>         --               ; (inj₂ ¬B) →
>         --               -- Can't write this, due to choice of `inj₁`
>     for `to`, above.
>         --               }
>         }
> 
> 
> However, when I try the code above, I get:
> 
>     Cannot instantiate the metavariable _140 to solution
>     snd(.patternInTele0) since it contains the variable
>     snd(.patternInTele0) which is not in scope of the metavariable
>     when checking that the expression refl has type
>     (λ { (inj₁ ¬A)
>            → λ .patternInTele0 → ¬A (Data.Product.proj₁ .patternInTele0)
>        ; (inj₂ ¬B)
>            → λ .patternInTele0 → ¬B (Data.Product.proj₂ .patternInTele0)
>        })
>     (inj₁ (λ a → ¬A×B (a , _snd_140 (¬A×B = ¬A×B) (a = a))))
>     .patternInTele0
>     ≡ ¬A×B .patternInTele0
> 
> 
> Any thoughts?
> 
> Thanks,
> -db
> :)
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>