1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: JMeq.v 9849 2007-05-22 20:40:04Z herbelin $ i*)
11
(** John Major's Equality as proposed by Conor McBride
15
[McBride] Elimination with a Motive, Proceedings of TYPES 2000,
16
LNCS 2277, pp 197-216, 2002.
20
Set Implicit Arguments.
22
Unset Elimination Schemes.
24
Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
27
Set Elimination Schemes.
29
Hint Resolve JMeq_refl.
31
Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
35
Hint Immediate sym_JMeq.
38
forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
42
Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
44
Lemma JMeq_ind : forall (A:Type) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y.
45
intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
48
Lemma JMeq_rec : forall (A:Type) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y.
49
intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
52
Lemma JMeq_rect : forall (A:Type) (x y:A) (P:A->Type), P x -> JMeq x y -> P y.
53
intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
57
forall (A:Type) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x.
58
intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
62
forall (A:Type) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x.
63
intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
67
forall (A:Type) (x y:A) (P:A -> Type), P y -> JMeq x y -> P x.
68
intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
71
(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)
75
Lemma JMeq_eq_dep_id :
76
forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y.
82
Lemma eq_dep_id_JMeq :
83
forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y.
89
(** [eq_dep U P p x q y] is strictly finer than [JMeq (P p) x (P q) y] *)
92
forall U P p x q y, eq_dep U P p x q y -> JMeq x y.
98
Lemma eq_dep_strictly_stronger_JMeq :
99
exists U, exists P, exists p, exists q, exists x, exists y,
100
JMeq x y /\ ~ eq_dep U P p x q y.
102
exists bool. exists (fun _ => True). exists true. exists false.
107
assert (true=false) by (destruct H; reflexivity).