Set Implicit Arguments.
Require Export Eqdep.
Notation "
c1 '==<<'
l1 '>>'
c2" := (
eq_dep _ l1 _ c1 _ c2) (
at level 100).
Transparent eq_rec.
Section My_Dependent_eq.
Variable U :
Set.
Variable F :
U->
Set.
Lemma eq_dep_ind_l :
forall (
a:
U) (
x:
F a) (
P:
forall (
b:
U),
F b ->
Prop),
(
P a x) ->
forall (
b:
U) (
y:
F b), (
x ==<<
F>>
y) ->
P b y.
Proof.
intros a x P H1 b y H2.
case H2.
auto.
Qed.
Lemma eq_dep_ind_l2 :
forall (
a:
U) (
x1 x2:
F a) (
P:
forall (
b:
U),
F b ->
F b ->
Prop),
P a x1 x2 ->
forall (
b:
U) (
y1 y2:
F b),
(
x1 ==<<
F>>
y1) -> (
x2 ==<<
F>>
y2) ->
P b y1 y2.
Proof.
intros a x1 x2 P H1 b y1 y2 H2;
generalize y2;
clear y2;
case H2;
intros y2 H3;
rewrite <- (
eq_dep_eq _ F _ x2 y2);
auto;
exact H3.
Qed.
Lemma f_eq_dep :
forall (
a b:
U) (
fU:
U ->
U) (
fF:
forall (
c:
U), (
F c) -> (
F (
fU c)))
(
x:
F a) (
y:
F b), (
x ==<<
F>>
y) -> ((
fF a x) ==<<
F>> (
fF b y)).
Proof.
induction 1;
auto.
Qed.
Lemma eq_eq_dep :
forall (
a:
U) (
x y:
F a),
x =
y -> (
x ==<<
F>>
y).
Proof.
induction 1;
auto.
Qed.
Scheme eq_indd:=
Induction for eq Sort Prop.
Definition coerce (
a b:
U) (
H:
a=
b) (
x:
F a) :=
eq_rec _ _ x _ H.
Lemma coerce_eq_dep :
forall (
a b:
U) (
H:
a=
b) (
x:
F a),
x ==<<
F>> (
coerce H x).
Proof.
intros a b H x;
apply (
eq_indd (
fun (
c:
U) (
H':
a=
c) => (
x ==<<
F>>
coerce H'
x)));
simpl;
auto.
Qed.
Lemma eq_dep_coerce_eq :
forall (
a b:
U) (
x:
F a) (
y:
F b),
(
x ==<<
F>>
y) ->
forall (
c:
U) (
H1:
a=
c) (
H2:
b=
c),
(
coerce H1 x) = (
coerce H2 y).
Proof.
intros a b x y H;
elim H;
intros c H1;
apply (
eq_indd (
fun (
u:
U) (
H':
a =
u) =>
forall (
H2:
a =
u),
coerce H'
x =
coerce H2 x));
simpl;
intro H2;
unfold coerce;
apply eq_rec_eq.
Qed.
End My_Dependent_eq.
Hint Resolve eq_dep_intro eq_dep_sym f_eq_dep eq_eq_dep coerce_eq_dep :
eqD.
Section Eq_dep_lemmas.
Section Eq_dep_eq_param.
Variable U:
Set.
Variable P:
U ->
Set.
Lemma eq_dep_eq_param :
forall (
p q:
U) (
x:
P p) (
y:
P q),
eq_dep _ _ p x q y ->
p =
q.
Proof.
intros p q x y h;
case h;
auto.
Qed.
End Eq_dep_eq_param.
Section Eq_dep_map_eq_dep.
Lemma eq_dep_map_eq_dep :
forall (
U V:
Set) (
f:
U ->
V) (
P:
U ->
Set) (
Q:
V ->
Set)
(
F:
forall (
p:
U),
P p ->
Q (
f p)) (
p q:
U) (
x:
P p) (
y:
P q),
eq_dep U P p x q y ->
eq_dep V Q (
f p) (
F p x) (
f q) (
F q y).
Proof.
intros U V f P Q F p q x y h.
apply eq_dep_ind_l with (
x :=
x) (
y :=
y) (
P :=
fun (
b:
U) (
z:
P b) =>
F p x ==<<
Q >>
F b z);
auto.
Qed.
End Eq_dep_map_eq_dep.
End Eq_dep_lemmas.