EqD.v

(* Some preliminaries on eq_dep *)

Implicit Arguments On.

Require Export Eqdep.

Grammar command command1 :=
  eqD_expl [ command0($c1) "==<" lcommand($l1) ">" command0($c2) ]
   -> [<<(eq_dep ? $l1 ? $c1 ? $c2)>>].

Transparent eq_rec.

Section My_Dependent_eq.

Variable U : Set.
Variable F : U->Set.

Lemma eq_dep_ind_l:
  (a:U; x:(F a); P:(b:U)(F b)->Prop)
    (P a x) -> (b:U; y:(F b))x ==<F> y -> (P b y).
  Intros a x P H1 b y H2; Case H2; Auto.
Qed.

Lemma eq_dep_ind_l2:
  (a:U; x1,x2:(F a); P:(b:U)(F b)->(F b)->Prop)
    (P a x1 x2) -> (b:U; y1,y2:(F b))x1 ==<F> y1 -> x2 ==<F> y2 -> (P b y1 y2).
  Intros a x1 x2 P H1 b y1 y2 H2; Generalize y2; Clear y2; Case H2.
  Intros y2 H3; Rewrite <- eq_dep_eq with P:=F x:=x2 y:=y2; Auto.
Qed.

Lemma f_eq_dep:
(a,b:U; fU:U->U; fF:(c:U)(F c)->(F (fU c));
   x:(F a); y:(F b)) x ==<F> y -> (fF a x) ==<F> (fF b y).
  Induction 1; Auto with core v62.
Qed.

Lemma eq_eq_dep : (a:U; x,y:(F a))x=y -> x ==<F> y.
Proof.
  Induction 1; Auto with core v62.
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: (a,b:U; H:a=b; x:(F a)) x==<F> (coerce H x).
  Intros a b H x; Pattern b H; Apply eq_indd; Simpl; Auto with core v62.
Qed.

Lemma eq_dep_coerce_eq:
  (a,b: U; x:(F a); y:(F b))
     x ==<F> y ->(c:U; H1: a=c; H2: b=c)(coerce H1 x)=(coerce H2 y).
  Intros a b x y H; Elim H.
    Intros c H1; Pattern c H1; Apply eq_indd; Simpl;
    Intros; Unfold coerce; Apply eq_rec_eq.
Qed.

End My_Dependent_eq.

Hints Resolve eq_dep_intro eq_dep_sym f_eq_dep eq_eq_dep coerce_eq_dep: eqD.

08/05/101, 16:43