[Agda] Fin n -> Fin n extensional?

[Andreas Abel]

On 19.02.2015 09:41, Peter Selinger wrote:
> even the statement "Functions with different names are different even
> if their code is the same" seems to be only conditionally true.

Indeed, this applies only to functions defined by pattern matching. 
Your examples below are simple aliases/abbreviations (as they do not 
match on data constructors), which are always expanded during equality 
checking. --Andreas

> For example,
>
>    open import Relation.Binary.PropositionalEquality
>
>    id : {a : Set} -> a -> a
>    id = λ x -> x
>
>    id2 : {a : Set} -> a -> a
>    id2 x = x
>
>    test : {a : Set} -> id {a} ≡ id2
>    test = refl
>
> works without a hitch. Actually, even this works:
>
>    app : {a b : Set} -> (a -> b) -> (a -> b)
>    app f x = f x
>
>    test2 : {a b : Set} -> app {a} {b} ≡ id {a -> b}
>    test2 = refl
>
> So the reality seems to be more complicated than you suggest. Even
> named functions seem to be compared up to beta-eta equality, provided
> that they are not pattern-matching.
>
> -- Peter
>
> Andreas Abel wrote:
>>
>> 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/
>>
>

-- 
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/