The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le lundi 26 novembre 2012 à 10:43 +0100, Arnaud Spiwack a écrit :

>         If you always need match or
>         fix, I am under the impression that propositional variables do
>         not
>         matter since their values cannot be matched upon.
> 
> Well, you seem to be missing Hugo's point here. By the lemma above, f1
> (Acc R x) p1 p2 and f2 (Acc R x) p1 p2 are convertible. Hence any two
> proofs of Acc R x are convertible, hence full proof-irrelevance.

Rather than proof-irrelevance, my concern was about having a
convertibility check that does terminate in all cases (that is, no
reduction to the halting problem). And I think that is what Hugo was
seeking too. My intuition still stands: I think you do not have to
exclude propositional variables from the algorithm. Now, the algorithm
might not give a sound answer due to proof irrelevance, but I am hardly
competent on such theoretical issues; I prefer to leave them to Andreas
and others.

Best regards,

Guillaume