CODEWITHSUNDEEP
coqdependent-type
Bob
Bob

Reputation: 1743

Rewriting with John Major's equality

John Major's equality comes with the following lemma for rewriting:

Check JMeq_ind_r.
(*
JMeq_ind_r
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, JMeq y x -> P y
*)

It is easy to generalize it like that:

Lemma JMeq_ind2_r
     : forall (A:Type)(x:A)(P:forall C,C->Prop),
       P A x -> forall (B:Type)(y:B), @JMeq B y A x -> P B y.
Proof.
intros.
destruct H0.
assumption.
Qed.

However I need something a bit different:

Lemma JMeq_ind3_r
     : forall (A:Type)(x:A*A) (P:forall C,C*C->Prop),
       P A x -> forall (B:Type)(y:B*B), @JMeq (B*B) y (A*A) x -> P B y.
Proof.
intros.
Fail destruct H0.
Abort.

Is JMeq_ind3_r provable?

If not:

Upvotes: 3

Views: 486

Answers (1)

András Kovács
András Kovács

Reputation: 30113

It's not provable. JMeq is essentially two equality proofs bundled together, one for the types and one for the values. In this case, we get from the hypothesis that A * A = B * B. From this, it is not provable that A = B, so we cannot convert a P A x into P B y.

If A * A = B * B implies A = B, that means that the pair type constructor is injective. Type constructor injectivity in general (i.e. for all types) is inconsistent with classical logic and also with univalence. For some type constructors, injectivity is provable, but not for pairs.

Is it safe to assume it as an axiom?

If you use classical logic or univalence then it isn't. Otherwise, it probably is, but I would instead try to rephrase the problem so that type constructor injectivity does not come up.

Upvotes: 4

Related Questions