The Coq mailing list

[Christine Paulin <christine.paulin AT lri.fr>]

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