[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

Tue Jan 7 11:01:48 CET 2014

Hello Thorsten.

Le 07/01/2014 10:19, Altenkirch Thorsten a ¨¦crit :
>
> On 06/01/2014 23:45, "Cody Roux" <cody.roux at andrew.cmu.edu> wrote:
>
>> On 01/06/2014 06:36 PM, Vladimir Voevodsky wrote:
>>> In my opinion only those constructions which can be expressed through
>>> eliminators are trustworthy. There is really no other way to supply
>>> rigorousness to inductive types with  pseudo-parameters (or whatever
>>> they are now called) such as Id-types.
>> This is simply not true, there are whole PhDs dedicated to describing
>> systems which can do better than eliminators. Andreas mentioned
>> sized-types, which are IMO the most mature candidate.
> A convincing way to justify those systems would be to provide a
> translation into eliminators. I suggested this to Andreas a while ago.
>> The fact that the implementation is behind the theoretical capabilities
>> is just that, an implementation problem.
> The eliminators are like axioms in set theory and it is worthwhile to
> translate any extension by reducing them to the axiom instead of adding
> new ones even though they may be semantically justified.

Nowadays, one can automatically certify in proof assistants like Coq or
Isabelle/HOL quite complex termination proofs (see the website of the
termination competition http://termcomp.uibk.ac.at/termcomp/home.seam).
So, it would be a pity not to take advantage of this for making the life
of proof assistants users easier, and allow them to define functions (or
enrich the equivalence on types) in ways that can hardly (or cannot) be
translated into eliminators. This is for instance the case of function
definitions based on general rewriting theory. This of course may raise
problems for making sure that such definitions are consistent, but it is
another (interesting) problem.

Regards,

Fr¨¦d¨¦ric.

> Thorsten
>
>
>> Best,
>>
>> Cody
>>
>>
>>> V.
>>>
>>>
>>> On Jan 6, 2014, at 6:27 PM, Cody Roux <cody.roux at andrew.cmu.edu> wrote:
>>>
>>>> The thing about Coq is that it's very disturbing not to have a
>>>> Set-theoretic interpretation where Prop is the set of Booleans {True,
>>>> False}. Agda of course doesn't have these qualms, but the fact that
>>>> this
>>>> issue appears in Coq without use of anything fancy (impredicativity,
>>>> etc) makes me still a bit worried. In particular there should be a
>>>> Set-theoretic model for Agda where Empty -> Box and Box -are- equal:
>>>> with a sufficiently clever interpretation of inductives, I believe I
>>>> can
>>>> get [[Empty -> Box ]] = [[Box]] = { {} } (where {} is just the empty
>>>> set). Can someone with more Agda knowledge try to type the original
>>>> problematic term?
>>>>
>>>>
>>>> Hypothesis Heq : (False -> False) = True.
>>>>
>>>> Fixpoint contradiction (u : True) : False :=
>>>> contradiction (
>>>> match Heq in (_ = T) return T with
>>>> | eq_refl => fun f:False => match f with end
>>>> end
>>>> ).
>>>>
>>>>
>>>>
>>>> On 01/06/2014 06:12 PM, Altenkirch Thorsten wrote:
>>>>> Hi Maxime,
>>>>>
>>>>> your postulate seems correct since certainly Empty ¡ú Box and Box are
>>>>> isomorphic and hence equal as a consequence of univalence.
>>>>>
>>>>> However, I think the definition of loop looks suspicious in the
>>>>> presence
>>>>> of proof-relevant equality: if we replace rewrite by an explicit use
>>>>> of
>>>>> subst, loop isn't structural recursive anymore. Hence my diagnosis
>>>>> would
>>>>> be that rewrite is simply incompatible with univalence.
>>>>>
>>>>> Cheers,
>>>>> Thorsten
>>>>>
>>>>> On 06/01/2014 20:42, "Maxime D¨¦n¨¨s" <mail at maximedenes.fr> wrote:
>>>>>
>>>>>> Bingo, Agda seems to have the same problem:
>>>>>>
>>>>>> module Termination where
>>>>>>
>>>>>> open import Relation.Binary.Core
>>>>>>
>>>>>> data Empty : Set where
>>>>>>
>>>>>> data Box : Set where
>>>>>> wrap : (Empty ¡ú Box) ¡ú Box
>>>>>>
>>>>>> postulate
>>>>>> iso : (Empty ¡ú Box) ¡Ô Box
>>>>>>
>>>>>> loop : Box -> Empty
>>>>>> loop (wrap x) rewrite iso = loop x
>>>>>>
>>>>>> gift : Empty ¡ú Box
>>>>>> gift ()
>>>>>>
>>>>>> bug : Empty
>>>>>> bug = loop (wrap gift)
>>>>>>
>>>>>> However, I may be missing something due to my ignorance of Agda. It
>>>>>> may
>>>>>> be well known that the axiom I introduced is inconsistent. Forgive
>>>>>> me if
>>>>>> it is the case.
>>>>>>
>>>>>> Maxime.
>>>>>>
>>>>>> On 01/06/2014 01:15 PM, Maxime D¨¦n¨¨s wrote:
>>>>>>> The anti-extensionality bug is indeed related to termination. More
>>>>>>> precisely, it is the subterm relation used by the guard checker
>>>>>>> which
>>>>>>> is not defined quite the right way on dependent pattern matching.
>>>>>>>
>>>>>>> It is not too hard to fix (we have a patch), but doing so without
>>>>>>> ruling out any interesting legitimate example (dealing with
>>>>>>> recursion
>>>>>>> on dependently typed data structures) is more challenging.
>>>>>>>
>>>>>>> I am also curious as to whether Agda is impacted. Let's try it :)
>>>>>>>
>>>>>>> Maxime.
>>>>>>>
>>>>>>> On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
>>>>>>>> Which bug was this?
>>>>>>>>
>>>>>>>> I only saw the one which allowed you to prove anti-extensionality?
>>>>>>>> But
>>>>>>>> this wasn't related to termination, or?
>>>>>>>>
>>>>>>>> Thorsten
>>>>>>>>
>>>>>>>> On 06/01/2014 16:54, "Cody Roux" <cody.roux at andrew.cmu.edu> wrote:
>>>>>>>>
>>>>>>>>> Nice summary!
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
>>>>>>>>>> Agda enforces termination via a termination checker which is more
>>>>>>>>>> flexible but I think less principled than Coq's approach.
>>>>>>>>> That's a bit scary given that there was an inconsistency found in
>>>>>>>>> the Coq termination checker just a couple of weeks ago :)
>>>>>>>>>
>>>>>>>>> BTW, has anyone tried reproducing the bug in Agda?
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Cody
>>>>>>>> This message and any attachment are intended solely for the
>>>>>>>> addressee
>>>>>>>> and may contain confidential information. If you have received this
>>>>>>>> message in error, please send it back to me, and immediately delete
>>>>>>>> it. Please do not use, copy or disclose the information contained
>>>>>>>> in
>>>>>>>> this message or in any attachment. Any views or opinions expressed
>>>>>>>> by
>>>>>>>> the author of this email do not necessarily reflect the views of
>>>>>>>> the
>>>>>>>> University of Nottingham.
>>>>>>>>
>>>>>>>> This message has been checked for viruses but the contents of an
>>>>>>>> attachment
>>>>>>>> may still contain software viruses which could damage your computer
>>>>>>>> system, you are advised to perform your own checks. Email
>>>>>>>> communications with the University of Nottingham may be monitored
>>>>>>>> as
>>>>>>>> permitted by UK legislation.
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>> _______________________________________________
>>>>>>> Agda mailing list
>>>>>>> Agda at lists.chalmers.se
>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda