(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                                 Eqdep.v                                  *)
(****************************************************************************)


Section Dependent_Equality.

Variable U : Set.
Variable P : U->Set.

Inductive eq_dep [p:U;x:(P p)] : (q:U)(P q)->Prop :=
   eq_dep_intro : (eq_dep p x p x).
Hint constr_eq_dep : core v62 := Constructors eq_dep.

Lemma  eq_dep_sym 
	: (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep q y p x).
Proof.
Induction 1; Auto.
Qed.
Hints Immediate eq_dep_sym : core v62.

Lemma eq_dep_trans : (p,q,r:U)(x:(P p))(y:(P q))(z:(P r))
     (eq_dep p x q y)->(eq_dep q y r z)->(eq_dep p x r z).
Proof.
Induction 1; Auto.
Qed.

(* eq_dep x y implies equality of parameters *)

Lemma eq_dep_eq_param : (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->p=q.
Destruct 1; Trivial.
Save.

(* dependent functions are stable w.r.t eq_dep *)
Lemma eq_dep_map_eq : 
  (Q:Set)(F:(p:U)(P p)->Q)
	(p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(F p x)=(F q y).
Destruct 1; Trivial.
Save.

Lemma eqmap_eq_dep : 
  (F:(p:U)(P p))(p,q:U)p=q ->(eq_dep p (F p) q (F q)).
Destruct 1; Trivial.
Save.

(* when x,y:(P p) one would like to establish (eq_dep x y)->x=y 
   but requires an extra axiom. We choose to introduce a non computational 
   axiom on the substitution combinator.
This axiom is related to Streicher K axiom and is 
provable whenever the equality on U is decidable, see file 
Eqdep_dec.
*)
	
Axiom eq_rec_eq : (p:U)(Q:U->Set)(x:(Q p))(h:p=p)
                  x=(eq_rec U p Q x p h).


Definition Kaxiom := 
	(p:U)(Q:p=p->Prop)(Q (refl_equal ? p))->(h:p=p)(Q h).

Lemma K_eq_rec_eq : Kaxiom -> (p:U)(Q:U->Set)(x:(Q p))(h:p=p)
                  x=(eq_rec U p Q x p h).
Intros.
Pattern h; Apply H; Trivial.
Save.


(* 
	Another dependent equality 
	(eq_dep1 x y) if there exists h:q=p such that x is equal 
	to y seen as an object in (P x) using elimination on h (eq_rec)
*)

Inductive eq_dep1 [p:U;x:(P p);q:U;y:(P q)] : Prop :=
   eq_dep1_intro : (h:q=p)
                  (x=(eq_rec U q P y p h))->(eq_dep1 p x q y).



Lemma eq_dep1_dep :
      (p:U)(x:(P p))(q:U)(y:(P q))(eq_dep1 p x q y)->(eq_dep p x q y).
Proof.
Induction 1; Intros eq_qp.
Cut (h:q=p)(y0:(P q))
    (x=(eq_rec U q P y0 p h))->(eq_dep p x q y0).
Intros; Apply H0 with eq_qp; Auto.
Rewrite eq_qp; Intros h y0.
Elim eq_rec_eq.
Induction 1; Auto.
Qed.

Lemma eq_dep_dep1 
	: (p,q:U)(x:(P p))(y:(P q))(eq_dep p x q y)->(eq_dep1 p x q y).
Proof.
Induction 1; Intros.
Apply eq_dep1_intro with (refl_equal U p).
Elim eq_rec_eq; Trivial.
Qed.

Lemma eq_dep1_eq : (p:U)(x,y:(P p))(eq_dep1 p x p y)->x=y.
Proof.
Induction 1; Intro.
Elim eq_rec_eq; Auto.
Qed.

Lemma eq_dep_eq : (p:U)(x,y:(P p))(eq_dep p x p y)->x=y.
Proof.
Intros; Apply eq_dep1_eq; Apply eq_dep_dep1; Trivial.
Qed.

(* Elimination principles to rewrite with dependent equality *)
Lemma eq_dep_rew 
 :  (p:U)(x:(P p))(C:(P p)->Prop)(C x)->(y:(P p))(eq_dep p y p x)->(C y).
Intros.
Generalize H.
Elim eq_dep_eq with 1:=H0; Trivial.
Save.

Lemma eq_dep_rew_RL
 :  (p:U)(x:(P p))(C:(P p)->Prop)(C x)->(y:(P p))(eq_dep p x p y)->(C y).
Intros.
Elim eq_dep_eq with 1:=H0; Trivial.
Save.

(* The contraposition of eq_dep_eq to be used as an Immediate Hint *)
Lemma neq_neq_dep : (p:U)(x,y:(P p))(~(x=y))->~(eq_dep p x p y).
Proof.
Red; Intros. 
Apply H; Apply eq_dep_eq; Trivial.
Qed.

(* Another definition of dependent equality using dependent pairs *)

Lemma equiv_eqex_eqdep : (p,q:U)(x:(P p))(y:(P q)) 
    (existS U P p x)=(existS U P q y) <-> (eq_dep p x q y).
Proof.
Split. 
Intros.
Generalize (eq_ind (sigS U P) (existS U P q y)
      [pr:(sigS U P)] (eq_dep  (projS1 U P pr) (projS2 U P pr) q y)) .
Proof.
Simpl.
Intro.
Generalize (H0 (eq_dep_intro q y)) .
Intro.
Apply (H1 (existS U P p x)).
Auto.
Intros.
Elim H.
Auto.
Qed.


Lemma inj_pair2: (p:U)(x,y:(P p))
    (existS U P p x)=(existS U P p y)-> x=y.
Proof.
Intros.
Apply eq_dep_eq.
Generalize (equiv_eqex_eqdep p p x y) .
Induction 1.
Intros.
Auto.
Qed.

End Dependent_Equality.

Hints Resolve eq_dep_intro : core v62.
Hints Immediate eq_dep_sym eq_dep_eq neq_neq_dep : core v62.

Lemma eq_dep_map_eq_dep : 
  (U,V:Set)(f:U->V)(P:U->Set)(Q:V->Set)(F:(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)).
Destruct 1; Trivial.
Save.


(* $Id: Eqdep.v,v 1.6 1999/11/23 15:45:13 mohring Exp $ *)
