casting convertible types in coq

Question

In the following:

Lemma test:
  forall n j  (jn : j < n)  (ln : j + 0 < n) (P:  forall {x} {y}, (x<y) -> nat),
    P ln = P jn.

Types ln an jn seems to be convertible to each other (from arithmetics point of view). How can I use that fact to prove the lemma above? I can easily prove assert(JL: j < n -> j + 0 < n) by auto. but I fail to see how to apply this to types.

score 2 · Accepted Answer · edited May 23 '17 at 12:03

2

The types are not convertible to each other, because of the way addition on the natural numbers is defined in Coq (i.e., by recursion on the first argument). As a matter of fact, the only reason your lemma can be typed in Coq at all is that the first implicit argument of P is instantiated to j + 0 on the right-hand side.

Unfortunately, even if these types were convertible, it would not be possible to prove this lemma without additional assumptions, because it requires the axiom of propositional extensionality (see here, for instance).

edited May 23 '17 at 12:03

Community

1
1

answered Nov 05 '15 at 05:34

Arthur Azevedo De Amorim

23,012
3
33
39

thanks. I understand it is not provable in general, but I was able to prove it for particular P. – krokodil Nov 05 '15 at 06:02
I am sorry, but I still do not understand. Even if I make 'x' and 'y' non-implicit, 'P' takes natural number so 'j' and 'j+0' are of type 'nat' and I can prove they are equivalent. From common sense, from proof 'j+0 – krokodil Nov 05 '15 at 17:22
3

Aren't all proofs of "m < n" provably equal? – gallais Nov 06 '15 at 14:01
Yes, that's actually true: proofs of "m < n" _are_ proof irrelevant... I should edit this. – Arthur Azevedo De Amorim Nov 08 '15 at 00:42

larsr · Answer 2 · 2015-11-06T09:18:48.370

The lemma is not provable. Try intros. remember (j+0) as Q. rewrite <- plus_n_O in HeqQ. subst Q. It will get rid of the + 0. Your goal is now

P j n ln = P j n jn

Both sides are of type nat. But now you need to prove that these two nats are equal, without knowing anything else about them...

EDIT:

Actually I was a little too quick... The value of the function P cannot depend on ln and jn since they are Props, . But to prove that, you need proof irrelevance.

If you do Require Import ProofIrrelevance. you get the axiom

Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.

It is not a consequence of Coq's logic, but it is consistent with it (and often is just what we mean with a proof - two formally correct arguments are equally true even if they differ in the details).

Now you just do

rewrite (proof_irrelevance _ ln jn). reflexivity. Qed.

I added some comments about using *proof irrelevance* to finish the proof. — larsr, Nov 06 '15 at 09:19

casting convertible types in coq

2 Answers2