[Agda] Fin n -> Fin n extensional?

[Andreas Abel]

Peter,

your analysis is correct.  Equality is not structural in Agda, but 
generative.  Functions with different names are different even if their 
code is the same.

   not : Bool -> Bool
   not true = false
   not false = true

is intensionally different from

   neg : Bool -> Bool
   neg true = false
   neg false = true

Each pattern matching lambda (pml) is a new named function, so pattern 
matching lambdas are different even though they share the same code. 
This is certainly a sort of confusion and owed to the light-weight 
implementation of pmls.

Ordinary lambdas are just terms which are compared via beta-eta.

--Andreas

On 18.02.2015 23:57, Peter Selinger wrote:
> This discussion reminds me that I have basically very little idea what
> equality of functions means in Agda. It may be one of the places where
> Agda differs from Coq. Unfortunately, the reference manual is mostly
> silent on this point, except for an obscure reference on the page on
> functions:
>
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Functions
>
> In the subsection on pattern matching lambdas, the manual states that
> "pattern matching functions are generative. For instance, refl will
> not be accepted as an inhabitant of the type
>
>    (λ { true → true ; false → false }) ≡
>    (λ { true → true ; false → false }),
>
> because this is equivalent to extlam1 ≡ extlam2 for some distinct
> fresh names extlam1 and extlam2."
>
>>From this, I inferred that function equality in Agda is definitional
> equality, i.e., two functions are equal if and only if they are
> internally represented as pointers to the same closure.
>
> However, this does not seem to be the case in general. For most
> functions, Agda seems quite happy to accept refl as an inhabitant as
> long as the two functions are beta-eta equivalent. For example,
>
> test : {a : Set} -> (λ(x : a -> a) -> λ(y : a) -> x y) ≡ (λ(x : a -> a) -> x)
> test = refl
>
> Apparently it is only for pattern-matching functions that definitional
> equality is used. So the correct answer for most purposes seems to be:
> Agda equality at function types is a random, but fixed, relation that
> is contained in beta-eta equality and that contains definitional
> equality.
>
> In particular, one cannot prove extensionality for any function whose
> domain is a datatype (such as Void or Fin n), because one can just
> write down two identical copies of some pattern-matching function, and
> they won't be equal.
>
> -- Peter
>
> Abhishek Anand 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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/