(****************************************************************************)
(*                 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 : Type.
Variable P : U->Type.

Inductive eqT_dep [p:U;x:(P p)] : (q:U)(P q)->Prop :=
   eqT_dep_intro : (eqT_dep p x p x).
Hint constr_eqT_dep : core v62 := Constructors eqT_dep.

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

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

(* eqT_dep x y implies equality of parameters *)

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

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

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

(* when x,y:(P p) one would like to establish (eqT_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 eqT_rec_eq : (p:U)(Q:U->Type)(x:(Q p))(h:p==p)
                  x==(eqT_rec U p Q x p h).


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

(*
Lemma K_eqT_rec_eq : Kaxiom -> (p:U)(Q:U->Type)(x:(Q p))(h:p==p)
                  x==(eqT_rec U p Q x p h).
Intros.
Pattern h; Apply H; Trivial.
Save.
*)


(* 
	Another dependent equality 
	(eqT_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 (eqT_rec)
*)

Inductive eqT_dep1 [p:U;x:(P p);q:U;y:(P q)] : Prop :=
   eqT_dep1_intro : (h:q==p)
                  (x==(eqT_rec U q P y p h))->(eqT_dep1 p x q y).



Lemma eqT_dep1_dep :
      (p:U)(x:(P p))(q:U)(y:(P q))(eqT_dep1 p x q y)->(eqT_dep p x q y).
Proof.
Induction 1; Intros eq_qp.
Cut (h:q==p)(y0:(P q))
    (x==(eqT_rec U q P y0 p h))->(eqT_dep p x q y0).
Intros; Apply H0 with eq_qp; Auto.
Rewrite eq_qp; Intros h y0.
Elim eqT_rec_eq.
Induction 1; Auto.
Qed.

Lemma eqT_dep_dep1 
	: (p,q:U)(x:(P p))(y:(P q))(eqT_dep p x q y)->(eqT_dep1 p x q y).
Proof.
Induction 1; Intros.
Apply eqT_dep1_intro with (refl_eqT U p).
Elim eqT_rec_eq; Trivial.
Qed.

Lemma eqT_dep1_eq : (p:U)(x,y:(P p))(eqT_dep1 p x p y)->x==y.
Proof.
Induction 1; Intro.
Elim eqT_rec_eq; Auto.
Qed.

Lemma eqT_dep_eq : (p:U)(x,y:(P p))(eqT_dep p x p y)->x==y.
Proof.
Intros; Apply eqT_dep1_eq; Apply eqT_dep_dep1; Trivial.
Qed.

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

Lemma eqT_dep_rew_RL
 :  (p:U)(x:(P p))(C:(P p)->Prop)(C x)->(y:(P p))(eqT_dep p x p y)->(C y).
Intros.
Elim eqT_dep_eq with 1:=H0; Trivial.
Save.

(* The contraposition of eqT_dep_eq to be used as an Immediate Hint *)
Lemma neq_neqT_dep : (p:U)(x,y:(P p))(~(x==y))->~(eqT_dep p x p y).
Proof.
Red; Intros. 
Apply H; Apply eqT_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) <-> (eqT_dep p x q y).
Proof.
Split. 
Intros.
Generalize (eq_ind (sigS U P) (existS U P q y)
      [pr:(sigS U P)] (eqT_dep  (projS1 U P pr) (projS2 U P pr) q y)) .
Proof.
Simpl.
Intro.
Generalize (H0 (eqT_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 eqT_dep_eq.
Generalize (equiv_eqex_eqdep p p x y) .
Induction 1.
Intros.
Auto.
Qed.

*)

End Dependent_Equality.

Hints Resolve eqT_dep_intro : core v62.
Hints Immediate eqT_dep_sym eqT_dep_eq neq_neqT_dep : core v62.

Lemma eqT_dep_map_eqT_dep : 
  (U,V:Type)(f:U->V)(P:U->Type)(Q:V->Type)(F:(p:U)(P p)->(Q (f p)))
	(p,q:U)(x:(P p))(y:(P q))
	(eqT_dep U P p x q y)->(eqT_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 $ *)