Library Coq.Logic.JMeq
John Major's Equality as proposed by Conor McBride
Reference:
McBride Elimination with a Motive, Proceedings of TYPES 2000,
LNCS 2277, pp 197-216, 2002.
Inductive JMeq (
A:
Type) (
x:
A) :
forall B:
Type,
B ->
Prop :=
JMeq_refl :
JMeq x x.
Hint Resolve JMeq_refl.
Lemma JMeq_sym :
forall (
A B:
Type) (
x:
A) (
y:
B),
JMeq x y ->
JMeq y x.
Hint Immediate JMeq_sym.
Lemma JMeq_trans :
forall (
A B C:
Type) (
x:
A) (
y:
B) (
z:
C),
JMeq x y ->
JMeq y z ->
JMeq x z.
Axiom JMeq_eq :
forall (
A:
Type) (
x y:
A),
JMeq x y ->
x = y.
Lemma JMeq_ind :
forall (
A:
Type) (
x:
A) (
P:
A ->
Prop),
P x ->
forall y,
JMeq x y ->
P y.
Lemma JMeq_rec :
forall (
A:
Type) (
x:
A) (
P:
A ->
Set),
P x ->
forall y,
JMeq x y ->
P y.
Lemma JMeq_rect :
forall (
A:
Type) (
x:
A) (
P:
A->
Type),
P x ->
forall y,
JMeq x y ->
P y.
Lemma JMeq_ind_r :
forall (
A:
Type) (
x:
A) (
P:
A ->
Prop),
P x ->
forall y,
JMeq y x ->
P y.
Lemma JMeq_rec_r :
forall (
A:
Type) (
x:
A) (
P:
A ->
Set),
P x ->
forall y,
JMeq y x ->
P y.
Lemma JMeq_rect_r :
forall (
A:
Type) (
x:
A) (
P:
A ->
Type),
P x ->
forall y,
JMeq y x ->
P y.
Lemma JMeq_congr :
forall (
A:
Type) (
x:
A) (
B:
Type) (
f:
A->
B) (
y:
A),
JMeq x y ->
f x = f y.
JMeq is equivalent to eq_dep Type (fun X => X)
eq_dep U P p x q y is strictly finer than JMeq (P p) x (P q) y
However, when the dependencies are equal, JMeq (P p) x (P q) y
is as strong as eq_dep U P p x q y (this uses JMeq_eq)