The Coq mailing list

[Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>]

On 07/01/2014 10:01, "Frédéric Blanqui" 
<frederic.blanqui AT inria.fr>
 wrote:

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

What termination arguments are not provable in Type Theory?

Ok, I buy the argument that we want to make conversion stronger. There is
your work with Jean-Pierre and more recently Conor's proposal how to add
equations to conversion.

However, the equations we add are on elements of Sets (= 0-truncated types
in the sense of HoTT) and provable using the eliminators. Hence I would
guess that there should be a way to reduce the enriched theory to the
basic theory. That is for any theorem you can prove in the enriched theory
there is a corresponding one in the basic theory which uses some
additional equality coercions. I am thinking of a result similar to
Martin-Hofmann's conservativity result for extensional type theory.

Hence, I do think that such extensions can be justified by a translation
into basic recursors.

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

Yes, and one way to them consistent is by translating them to basic
recursors.

Thorsten

>
>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
>
>--
>You received this message because you are subscribed to the Google Groups
>"Homotopy Type Theory" group.
>To unsubscribe from this group and stop receiving emails from it, send an
>email to 
>HomotopyTypeTheory+unsubscribe AT googlegroups.com.
>For more options, visit https://groups.google.com/groups/opt_out.