JMeq.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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.

Set Implicit Arguments.

Unset Elimination Schemes.

Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
    JMeq_refl : JMeq x x.

Set Elimination Schemes.

Arguments JMeq_refl {A x} , [A] x.

Register JMeq as core.JMeq.type.
Register JMeq_refl as core.JMeq.refl.

Hint Resolve JMeq_refl : core.

Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.

Register JMeq_hom as core.JMeq.hom.

Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.forall (A B : Type) (x : A) (y : B),
JMeq x y -> JMeq y x
Proof.forall (A B : Type) (x : A) (y : B),
JMeq x y -> JMeq y x 
intros; destruct H; trivial.
Qed.

Hint Immediate JMeq_sym : core.

Register JMeq_sym as core.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.forall (A B C : Type) (x : A) (y : B) (z : C),
JMeq x y -> JMeq y z -> JMeq x z
Proof.forall (A B C : Type) (x : A) (y : B) (z : C),
JMeq x y -> JMeq y z -> JMeq x z
destruct 2; trivial.
Qed.

Register JMeq_trans as core.JMeq.trans.

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.forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, JMeq x y -> P y
Proof.forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, JMeq x y -> P y
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.

Register JMeq_ind as core.JMeq.ind.

Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set),
  P x -> forall y, JMeq x y -> P y.forall (A : Type) (x : A) (P : A -> Set),
P x -> forall y : A, JMeq x y -> P y
Proof.forall (A : Type) (x : A) (P : A -> Set),
P x -> forall y : A, JMeq x y -> P y
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.

Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type),
  P x -> forall y, JMeq x y -> P y.forall (A : Type) (x : A) (P : A -> Type),
P x -> forall y : A, JMeq x y -> P y
Proof.forall (A : Type) (x : A) (P : A -> Type),
P x -> forall y : A, JMeq x y -> P y
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.

Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
   P x -> forall y, JMeq y x -> P y.forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, JMeq y x -> P y
Proof.forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, JMeq y x -> P y
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set),
   P x -> forall y, JMeq y x -> P y.forall (A : Type) (x : A) (P : A -> Set),
P x -> forall y : A, JMeq y x -> P y
Proof.forall (A : Type) (x : A) (P : A -> Set),
P x -> forall y : A, JMeq y x -> P y
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type),
   P x -> forall y, JMeq y x -> P y.forall (A : Type) (x : A) (P : A -> Type),
P x -> forall y : A, JMeq y x -> P y
Proof.forall (A : Type) (x : A) (P : A -> Type),
P x -> forall y : A, JMeq y x -> P y
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.

Lemma JMeq_congr :
 forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y.forall (A : Type) (x : A) (B : Type) (f : A -> B)
  (y : A), JMeq x y -> f x = f y
Proof.forall (A : Type) (x : A) (B : Type) (f : A -> B)
  (y : A), JMeq x y -> f x = f y
intros A x B f y H; case JMeq_eq with (1 := H); trivial.
Qed.

Register JMeq_congr as core.JMeq.congr.

JMeq is equivalent to eq_dep Type (fun X ⇒ X)

Require Import Eqdep.

Lemma JMeq_eq_dep_id :
 forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y.forall (A B : Type) (x : A) (y : B),
JMeq x y -> eq_dep Type (fun X : Type => X) A x B y
Proof.forall (A B : Type) (x : A) (y : B),
JMeq x y -> eq_dep Type (fun X : Type => X) A x B y
destruct 1.A:Type
x:A
eq_dep Type (fun X : Type => X) A x A x
apply eq_dep_intro.
Qed.

Lemma eq_dep_id_JMeq :
 forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y.forall (A B : Type) (x : A) (y : B),
eq_dep Type (fun X : Type => X) A x B y -> JMeq x y
Proof.forall (A B : Type) (x : A) (y : B),
eq_dep Type (fun X : Type => X) A x B y -> JMeq x y
destruct 1.A:Type
x:A
JMeq x x
apply JMeq_refl.
Qed.

eq_dep U P p x q y is strictly finer than JMeq (P p) x (P q) y

Lemma eq_dep_JMeq :
 forall U P p x q y, eq_dep U P p x q y -> JMeq x y.forall (U : Type) (P : U -> Type) (p : U) (x : P p)
  (q : U) (y : P q), eq_dep U P p x q y -> JMeq x y
Proof.forall (U : Type) (P : U -> Type) (p : U) (x : P p)
  (q : U) (y : P q), eq_dep U P p x q y -> JMeq x y
destruct 1.U:Type
P:U -> Type
p:U
x:P p
JMeq x x
apply JMeq_refl.
Qed.

Lemma eq_dep_strictly_stronger_JMeq :
 exists U P p q x y, JMeq x y /\ ~ eq_dep U P p x q y.exists
  (U : Type) (P : U -> Type) (p q : U) (x : P p) (y : 
                                                 P q),
  JMeq x y /\ ~ eq_dep U P p x q y
Proof.exists
  (U : Type) (P : U -> Type) (p q : U) (x : P p) (y : 
                                                 P q),
  JMeq x y /\ ~ eq_dep U P p x q y
exists bool.exists
  (P : bool -> Type) (p q : bool) (x : P p) (y : P q),
  JMeq x y /\ ~ eq_dep bool P p x q y exists (fun _ => True).exists (p q : bool) (x y : True),
  JMeq x y /\
  ~ eq_dep bool (fun _ : bool => True) p x q y exists true.exists (q : bool) (x y : True),
  JMeq x y /\
  ~ eq_dep bool (fun _ : bool => True) true x q y exists false.exists x y : True,
  JMeq x y /\
  ~ eq_dep bool (fun _ : bool => True) true x false y
exists I.exists y : True,
  JMeq I y /\
  ~ eq_dep bool (fun _ : bool => True) true I false y exists I.JMeq I I /\
~ eq_dep bool (fun _ : bool => True) true I false I
split.JMeq I I
~ eq_dep bool (fun _ : bool => True) true I false I
-JMeq I I trivial.
-~ eq_dep bool (fun _ : bool => True) true I false I intro H.H:eq_dep bool (fun _ : bool => True) true I false I
False
  assert (true=false) by (destruct H; reflexivity).H:eq_dep bool (fun _ : bool => True) true I false I
H0:true = false
False
  discriminate.
Qed.

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)

Lemma JMeq_eq_dep : 
  forall U (P:U->Type) p q (x:P p) (y:P q), 
  p = q -> JMeq x y -> eq_dep U P p x q y.forall (U : Type) (P : U -> Type) (p q : U) (x : P p)
  (y : P q), p = q -> JMeq x y -> eq_dep U P p x q y
Proof.forall (U : Type) (P : U -> Type) (p q : U) (x : P p)
  (y : P q), p = q -> JMeq x y -> eq_dep U P p x q y
intros.U:Type
P:U -> Type
p, q:U
x:P p
y:P q
H:p = q
H0:JMeq x y
eq_dep U P p x q y
destruct H.U:Type
P:U -> Type
p:U
x, y:P p
H0:JMeq x y
eq_dep U P p x p y
apply JMeq_eq in H0 as ->.U:Type
P:U -> Type
p:U
y:P p
eq_dep U P p y p y
reflexivity.
Qed.


(* Compatibility *)
Notation sym_JMeq := JMeq_sym (only parsing).
Notation trans_JMeq := JMeq_trans (only parsing).