[Agda] How to validate eta-reduction in equational reasoning proofs?

[James Wood]

The bidirectional type checker often needs a bit of help with non-normal 
forms. In this case, we can see that `(λ { C→A⇒D (C , A) → C→A⇒D C · A 
})` has some type of the form (x : X) → Y[x] where
Y[(λ C₁ → ƛ (λ A₁ → C×A→D (C₁ , A₁)))] is known. However, we don't know 
much about Y[x] for general x.

To help out the type checker, you need to give a (possibly partial) type 
annotation to the first λ-expression. This can be done using stdlib's 
`Function.Base._∋_` or a local definition with a type signature. 
Alternatively (and this is probably what I would do), you could 
normalise away all the redexes, and then you probably won't need any 
annotations. In fact, because the whole proof should be by definitional 
equality, I'd probably turn all of the equational reasoning into `refl` 
and move on.

All the best,
James

On 14/01/2021 19:46, David Banas wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> Thanks, Ulf!
> After changing my product type definition to match yours, I am unstuck. :)
> 
> Originally, I’d written:
> 
>     data _×_ (A : Set) (B : Set) : Set where
>        _,_ : A → B → (A × B)
> 
> 
> I guess there was something more I needed to do, in order to have this 
> type play nicely with the rest of the system?
> 
> Now (using your product type), I’m able to complete the proof in a 
> single step and without invoking extensionality:
> 
>     117 begin
>     118 (λ { C→A⇒D (C , A) → C→A⇒D C · A })
>     119   (λ C₁ → ƛ (λ A₁ → C×A→D (C₁ , A₁)))
>     120 ≡⟨⟩
>     121   C×A→D
>     122 ∎
> 
> 
> However, I’m getting the following warning, related to the highlighted 
> code above (line 118):
> (Note that /column/ numbers below are inaccurate.)
> 
>     Sort _78  [ at ###.agda:118,31-64 ]
>     _79 : _78  [ at ###.agda:118,31-64 ]
>     _81 : _79  [ at ###.agda:118,31-64 ]
> 
> 
> Do you know why?
> 
> Thanks,
> -db
> 
> 
>> On Jan 14, 2021, at 6:02 AM, Ulf Norell <ulf.norell at gmail.com 
>> <mailto:ulf.norell at gmail.com>> wrote:
>>
>> FWIW this works:
>>
>> open import Agda.Builtin.Sigma
>> open import Agda.Builtin.Equality
>>
>> _×_ : Set → Set → Set
>> A × B = Σ A λ _ → B
>>
>> postulate
>>   A B C : Set
>>   f     : A × B → C
>>   ext   : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
>>
>> prf : (λ { (x , y) → f (x , y) }) ≡ (λ { p → f p })
>> prf = ext λ _ → refl
>>
>> Have you made sure that the pair type you are using has eta equality?
>>
>> / Ulf
>>
>> On Thu, Jan 14, 2021 at 2:09 PM James Wood 
>> <james.wood.100 at strath.ac.uk <mailto:james.wood.100 at strath.ac.uk>> wrote:
>>
>>     It might not hold definitionally as written because extended λs are
>>     generative. The first thing I'd try, assuming sufficiently new
>>     Agda, is
>>     to remove all the curly braces.
>>
>>     James
>>
>>     On 14/01/2021 01:22, Jason -Zhong Sheng- Hu wrote:
>>     > CAUTION: This email originated outside the University. Check before
>>     > clicking links or attachments.
>>     >
>>     > That’s very strange. I would expect this equality to hold
>>     > definitionally. You shouldn’t even need extensionality.
>>     >
>>     > Does agda complain anything if you remove the first two lines
>>     entirely?
>>     >
>>     > Thanks,
>>     >
>>     > Jason Hu
>>     >
>>     > *From: *David Banas <mailto:capn.freako at gmail.com
>>     <mailto:capn.freako at gmail.com>>
>>     > *Sent: *Wednesday, January 13, 2021 8:20 PM
>>     > *To: *Agda mailing list <mailto:agda at lists.chalmers.se
>>     <mailto:agda at lists.chalmers.se>>
>>     > *Subject: *[Agda] How to validate eta-reduction in equational
>>     reasoning
>>     > proofs?
>>     >
>>     > Hi all,
>>     >
>>     > Does anyone know how I can get this to work?
>>     >
>>     >                               (λ { (C , A) → (C×A→D (C , A)) })
>>     >                             ≡⟨extensionality (λ C×A → refl) ⟩
>>     >                               (λ { x → (C×A→D x) })
>>     >
>>     > Agda is telling me:
>>     >
>>     >     (λ { (C , A) → C×A→D (C , A) }) C×A != C×A→D C×A of type D
>>     >
>>     >     when checking that the expression refl has type
>>     >
>>     >     (λ { (C , A) → C×A→D (C , A) }) C×A ≡ C×A→D C×A
>>     >
>>     > Thanks,
>>     >
>>     > -db
>>     >
>>     >
>>     > _______________________________________________
>>     > Agda mailing list
>>     > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>     > https://lists.chalmers.se/mailman/listinfo/agda
>>     <https://lists.chalmers.se/mailman/listinfo/agda>>>     >
>>
>>     _______________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>     https://lists.chalmers.se/mailman/listinfo/agda
>>     <https://lists.chalmers.se/mailman/listinfo/agda>>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
>