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

[David Banas]

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> 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
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210114/57d7e833/attachment.html>