[Agda] Fin n -> Fin n extensional?

Mon Feb 23 23:29:34 CET 2015

Jon,

Yeah, I was going to add that eta expanding Id[X](e,e') to refl is
only type preserving when e and e' are judgementally equal, and in an
open context they might not be.

Best,
Andrea

On Mon, Feb 23, 2015 at 9:05 PM, Jon Sterling <jon at jonmsterling.com> wrote:
> Andrea,
>
> Out of curiosity, is the reason that Agda does not do eta expansion at
> the identity type because it would cause false identifications to become
> true judgementally in an open term?
>
> Kind regards,
> Jon
>
>
> On Mon, Feb 23, 2015, at 10:50 AM, Andrea Vezzosi wrote:
>> As a side note, Agda doesn't actually do any eta expansion at the Id
>> type, e.g. two postulated equalities won't be judgementally equal.
>>
>> However without postulates (or primTrustMe) it is still the case that
>> every proof of equality in a closed context will evaluate to refl.
>> Axiom K actually computes away as soon as the proof becomes refl, so
>> it's not making this any harder.
>>
>>
>> Cheers,
>> Andrea
>>
>> On Mon, Feb 23, 2015 at 4:38 PM, Neelakantan Krishnaswami
>> <n.krishnaswami at cs.bham.ac.uk> wrote:
>> > -----BEGIN PGP SIGNED MESSAGE-----
>> > Hash: SHA1
>> >
>> > Hello,
>> >
>> > Definitional equality including Axiom K (uniqueness of identity proofs)
>> > remains decidable.
>> >
>> > The reason is that you can split the implementation of judgemental
>> > into two alternating phases -- weak-head normalization and
>> > type-directed eta-expansion. Just as with eta for unit, this means
>> > that when you compare terms at equality type, you can simply succeed.
>> >
>> > Concretely, if you have proofs p and q at type Id[X](e,e') such that
>> > p,q :  Id[X](e,e'), then you can eta-expand to p ==> refl and
>> > q ==> refl, and then refl will be judged to be equal to itself.
>> >
>> > If you restrict "computation" to mean beta-reduction, then equality
>> > proofs do not all have to *reduce* to refl. However, they all can
>> > *eta-expand* to refl.
>> >
>> > IMO, a very good reference on this is Andreas Abel's habilitation
>> > thesis. If you're in a hurry, then his FOSSACS 2011 paper with Gabriel
>> > Scherer "On Irrelevance and Algorithmic Equality in Predicative Type
>> > Theory" was a relatively accessible introduction to this approach.
>> >
>> >
>> > Best,
>> > Neel
>> >
>> > On 19/02/15 20:54, Abhishek Anand wrote:
>> >> Thanks Jason. Your argument is convincing. Already at the second
>> >> line,  (\_ → 0) and (\_ → 1)  being definitionally equal
>> >> contradicts my understanding of Coq's definitional equality. Are
>> >> your assumptions valid in Agda with K? In other words, is it true
>> >> that in Agda with K, any proof of equality (Id) of closed terms
>> >> computes down to refl?
>> >>
>> >>
>> >> Thanks, -- Abhishek http://www.cs.cornell.edu/~aa755/
>> >>
>> >> On Wed, Feb 18, 2015 at 12:06 PM, Jason Gross
>> >> <jasongross9 at gmail.com> wrote:
>> >>
>> >>> Here's one, I think, for showing impossibility of inhabiting the
>> >>> type (f g : Void → ℕ) → Id f g: Assuming the type theory is
>> >>> strongly normalizing on terms of identity type, the only closed
>> >>> proof of equality of two closed functions must be refl.  Thus, if
>> >>> (\_ → 0) and (\_ → 1) are equal, they must be definitionally
>> >>> equal in a strongly normalizing type theory.  From (Id f g), we
>> >>> can obtain (x : Void) → Id (f x) (g x); it's behavior is to send
>> >>> refl to refl.  Thus, when we plug in refl : Id (\_ → 0) (\_ → 1),
>> >>> we get a proof of Void → Id 0 1 which reduces to \_ → refl.  But
>> >>> this is a contradiction, for refl does not prove Id 0 1.
>> >>>
>> >>> On Wed, Feb 18, 2015 at 11:37 AM, Abhishek Anand <
>> >>> abhishek.anand.iitg at gmail.com> wrote:
>> >>>
>> >>>> Unprovability of void-ext has been known to be the reason why
>> >>>> one cannot (in Coq) code up natural numbers as W Types.
>> >>>>
>> >>>> Here is a quote : "This is because one cannot prove that there
>> >>>> is only a unique function from the empty set to the set of
>> >>>> natural numbers without using extensional equality." from
>> >>>> https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes
>> >>>>
>> >>>> However, I don't know a formal (meta-theoretical) proof of
>> >>>> unprovability of void-ext. I'd be grateful if someone can point
>> >>>> us to such a  proof.
>> >>>>
>> >>>>
>> >>>> -- Abhishek http://www.cs.cornell.edu/~aa755/
>> >>>>
>> >>>> On Wed, Feb 18, 2015 at 11:20 AM, Dan Licata <drl at cs.cmu.edu>
>> >>>> wrote:
>> >>>>
>> >>>>> Can you even do this (without otherwise assuming function
>> >>>>> extensionality)?
>> >>>>>
>> >>>>> For example, for Fin 0, isn't it the same as saying "any
>> >>>>> function from 0 to A is abort":
>> >>>>>
>> >>>>> data Id {A : Set} (a : A) : A → Set where refl : Id a a
>> >>>>>
>> >>>>> data Void : Set where
>> >>>>>
>> >>>>> abort : {A : Set} → Void → A abort ()
>> >>>>>
>> >>>>> void-ext : {A : Set} → (f : Void → A) → Id f abort void-ext f
>> >>>>> = {!!}
>> >>>>>
>> >>>>> (void-ext is sufficient; is it necessary?) and if so, can you
>> >>>>> prove that?  I don't see how off the top of my head.
>> >>>>>
>> >>>>> -Dan
>> >>>>>
>> >>>>> On Feb 18, 2015, at 10:47 AM, João Paulo Pizani Flor <
>> >>>>> J.P.PizaniFlor at uu.nl> wrote:
>> >>>>>
>> >>>>> Not yet (couldn't find it anywhere), but I will probably need
>> >>>>> it for my Ph.D project, so maybe it will come in some
>> >>>>> time...
>> >>>>>
>> >>>>> Cheers,
>> >>>>>
>> >>>>> João Pizani, M.Sc <j.p.pizaniflor at uu.nl> Promovendus -
>> >>>>> Departement Informatica Faculteit Bètawetenschappen -
>> >>>>> Universiteit Utrecht
>> >>>>>
>> >>>>> On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette
>> >>>>> <carette at mcmaster.ca> wrote:
>> >>>>>
>> >>>>>> Does anyone have a proof in Agda that functions at type
>> >>>>>> (Fin n -> Fin n) are extensional? Jacques
>> >>>>>> _______________________________________________ Agda
>> >>>>>> mailing list Agda at lists.chalmers.se
>> >>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>> >>>>>>
>> >>>>>
>> >>>>> _______________________________________________ Agda mailing
>> >>>>> list Agda at lists.chalmers.se
>> >>>>> https://lists.chalmers.se/mailman/listinfo/agda
>> >>>>>
>> >>>>>
>> >>>>>
>> >>>>> _______________________________________________ Agda mailing
>> >>>>> list Agda at lists.chalmers.se
>> >>>>> https://lists.chalmers.se/mailman/listinfo/agda
>> >>>>>
>> >>>>>
>> >>>>
>> >>>> _______________________________________________ Agda mailing
>> >>>> list Agda at lists.chalmers.se
>> >>>> https://lists.chalmers.se/mailman/listinfo/agda
>> >>>>
>> >>>>
>> >>>
>> >>
>> >>
>> >>
>> >> _______________________________________________ Agda mailing list
>> >> Agda at lists.chalmers.se
>> >> https://lists.chalmers.se/mailman/listinfo/agda
>> >>
>> > -----BEGIN PGP SIGNATURE-----
>> > Version: GnuPG v2.0.14 (GNU/Linux)
>> >
>> > iQIbBAEBAgAGBQJU60laAAoJEFHmop5RZGmSfJcP91HMj9P8+iiF344OtyF+Pfv1
>> > IUk+w4IndUMQcDPFys0GCX9VyMeg5W3ezwV1eYYLNlSghtR/rWAVtKRlDH/PQ8Hp
>> > Q9RJhpEo3gNMW1cBSHWTM7HpmcI2z8ttualtE/1+yK4XPRC0vXw6V6mOHv4KmDES
>> > xjhsKy4ut8Ah4pTXvb0+MkTvI46F7dpBlkpQmAFygpfOtNz7ahZ4+bQjlmdPMu6B
>> > DG9jwtA9HuEBoxR84Fni0w9gA5da+Ew7cF0mcuG777RK3M6NnuB+jnyk18w7qUKv
>> > bQ9s4Is0YZ4KHkDmNe6tVnTbDaivzQfN6rBTFPfrRPHCo0b4cU3Dpos7dQdOf56a
>> > qvlmC8hoB60KGaLYx+SqjAHfEudHsTPzpDQUHZE0T+zlqLBI1g8y9my20rd5PN3t
>> > S4sapKOVsVibd+XnNbGDhoRDA4Uy1KccO0O9Yt8w1/yTpJqik4DfB8g7tEIzsgc+
>> > 137F+WnUfNiilpukOWrhzSRmxpmOgGZaA96o4tsq6eZjf8w9OSZeYFzEqn+pCtci
>> > gClqrFGIdbBXHEcOMnJ5K+Y1y+1himsvfM8XavdE0tTfv2+aGknpwm9qRs6SG7+w
>> > gNV18wNhkL6BqdDTnEIJ6y1PvK/IDmi6D9Ar9eL8nvcELzzsEbDFLFWkm/ElSzZ6
>> > OC285Dst5uKeClsp238=
>> > =qT5j
>> > -----END PGP SIGNATURE-----
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda