The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

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.

The fact that the implementation is behind the theoretical capabilities 
is just that, an implementation problem.

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