The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,

How wrong am I if I say that the problem is not the termination checker,
it is this weird thing that is Prop.

I mean : No one would pretend that
(fun (x : Empty) => match x with end) = (fun (x : Empty) => x)
does she ?

So yes maybe, the termination checker has to be obfuscated by Prop as
case analysis typing rule is. Anyway, I would like a way to say that
impossible branches are subterms in a proof relevant setting and I still
don't see a reason to forbid myself to have one. Am I still half
asleep ?

Pierre B.


Le vendredi 13 décembre 2013 à 08:21 +0100, Christine Paulin a écrit :
> 
> On 12/13/2013 02:01 AM, Daniel Schepler wrote:
> 
> > I'd have to agree: the problem here would seem to be that it's
> > highly suspect for
> > 
> > match Heq ... with | eq_refl => fun f => match f with end end
> > 
> > to be considered a subterm of any u:True.
> > 
> I agree with that, it looks like a serious bug in the guard condition 
> 
> The principle is the recursive call in the definition of f x should be
> of the form 
>     f t 
> with t a strict recursive subterm of x
> 
> there is a rule to accept a term t of the form (match u with t1 .. tn
> end)
> whenever all ti are recursive subterms of x 
>     in particular when u has type False (match u with end) is
> accepted 
> 
> the justification for this rule is that (f (match u with t1 .. tn
> end)) behaves like (match u with (f t1) .. (f tn) end) which is
> correct
> 
> However in that case we end up with something of the form (f   (fun x
> => match x with end)) that will definitely not commute.
> So some check needs to be added. A simple idea would be that a
> recursive subterm could never be an abstraction, or to add some finer
> analysis in which context u should be typable.
> 
> Christine
> 
> 
> 
> 
> > 
> > 
> > (In fact, it was my unease over my hlength example from yesterday
> > being accepted with the second version of hcons_fin_inv, that led me
> > to experiment with it until I morphed it into the example from this
> > morning.)
> > -- 
> > 
> > Daniel Schepler
> > 
> > 
> > 
> > On Thu, Dec 12, 2013 at 4:08 PM, Abhishek Anand
> > <abhishek.anand.iitg AT gmail.com>
> >  wrote:
> >         It seems that Propositional Extensionality is implied by the
> >         proof-irrelevant semantics(of Prop) given in  
> >         
> > http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.55.1709&rep=rep1&type=pdf
> >         
> >         
> >         
> >         I quote:
> >         " Propositions  are  interpreted  either  by  the  empty
> >          set  or  by  a  canonical  sin- 
> >         gleton,  depending  upon  their  validity  in  the  model.
> >          As  a  consequence  all 
> >         proof-terms  are  identified.  In  the  same  way,  tile
> >          interpretation  of  Prop  is 
> >         {0,1}. "
> >         
> >         
> >         So, all true propositions have the same
> >         denotation(interpretation). I would guess this means
> >         Propositional Extensionality is indeed consistent with Coq's
> >         theory.
> >         
> >         
> >         I hope it is just a fixable bug in the
> >         implementation(termination analysis?) of Coq.
> >         
> >         
> >         
> >         -- Abhishek
> >         http://www.cs.cornell.edu/~aa755/
> >         
> >         
> >         On Thu, Dec 12, 2013 at 6:45 PM, Guillaume Melquiond
> >         
> > <guillaume.melquiond AT inria.fr>
> >  wrote:
> >                 On 13/12/2013 00:30, Daniel Schepler wrote:
> >                         The Extensionality_Ensembles axiom in
> >                         
> > http://coq.inria.fr/distrib/current/stdlib/Coq.Sets.Ensembles.html
> >                         easily implies propositional extensionality
> >                 
> >                 
> >                 In a similar way, propositional extensionality was
> >                 used to prove the consistency of the set theory of
> >                 Why3. And my email would be incomplete if I didn't
> >                 quote the comment accompanying that Coq proof: "it
> >                 is folklore that the two together are consistent".
> >                 Famous last words...
> >                 
> >                 Best regards,
> >                 
> >                 Guillaume
> >         
> >         
> > 
> > 
>