Tel_coerce2.v

Implicit Arguments On.
Require Export Tel.

Mutual Inductive subtel: tel -> tel ->Type :=
     subtel_T0: (t:tel)(subtel T0 t)
    | subtel_Tc:
        (T, T':Type) (identityT ? T T') ->
        (f:T ->tel)
        (g:T' ->tel)
        ((x:T)
         (x':T')
         (identityT
            ? (existT Type [T0:Type]T0 T x) (existT Type [T0:Type]T0 T' x')) ->
         (subtel (f x) (g x'))) ->(subtel (Tc f) (Tc g))
    | subtel_tel_Tc:
        (t:tel) (T:Type) (f:T ->tel) ((x:T)(subtel t (f x))) ->(subtel t (Tc f)) .
Hints Resolve subtel_T0 subtel_Tc subtel_tel_Tc :core.

Definition coerce_type:
  (T, T':Type) (identityT ? T' T) ->
  (x:T)
  (sigT
     ?
     [x':T']
     (identityT ? (existT Type [T0:Type]T0 T x) (existT Type [T0:Type]T0 T' x'))).
Intros T T' H'; Try Assumption.
Case H'.
Intros x; Try Assumption.
Exists x.
Auto with core.
Defined.

Definition coerce_tel: (t, t':tel) (subtel t t') -> (el_tel t') ->(el_tel t).
Fix 3.
Intros t t' H'; Try Assumption.
Case H'.
Intros T H'0; Try Assumption.
Exact el_T0.
Intros T T' H'0 f g H'1 H'2.
Case (coerce_type H'0 (el_fst H'2)).
Intros x H'3; Try Assumption.
Apply el_Tc with x := x.
Apply coerce_tel with t' := (g (el_fst H'2)).
Apply H'1.
Simpl in H'3; Auto with core.
Exact (el_rem H'2).
Intros t0 T f H'0 H'1; Try Assumption.
Apply coerce_tel with t' := (tel_fun (el_fst H'1)).
Apply H'0.
Exact (el_rem H'1).
Defined.
Parameter subtel_refl:(t:tel)(subtel t t).
Hints Resolve subtel_refl :core.

Definition concat_tel: tel -> tel ->tel.
Fix 1.
Intros t1.
Case t1.
Exact [t2:tel]t2.
Intros T f.
Exact [t2:tel](Tc [x:T](concat_tel (f x) t2)).
Defined.

Mutual Inductive sumT[A, B:Type]: Type :=
     leftT: A ->(sumT A B)
    | rightT: B ->(sumT A B) .

Record prodT[A, B:Type]: Type := {
   prodT1: A;
   prodT2: B }.

Axiom depidT_idT:
      (T:Type)
      (x, y:T)
      (identityT
         (sigT Type [T0:Type]T0) (existT Type [T0:Type]T0 T x)
         (existT Type [T0:Type]T0 T y)) ->(identityT T x y).
Hints Resolve depidT_idT :core.

Axiom depidT_idTfun:
      (T, A:Type)
      (f, g:T ->A)
      (identityT
         (sigT Type [T:Type] T ->A) (existT Type [T:Type] T ->A T f)
         (existT Type [T:Type] T ->A T g)) ->(identityT ? f g).

Axiom depidT_idTtype:
      (T, T':Type)
      (P:Type ->Type)
      (f:(P T))
      (g:(P T')) (identityT ? (existT Type P T f) (existT Type P T' g)) ->
      (identityT ? T T').

Definition identityT_fun:
  (T, T', A:Type)
  (f:T ->A)
  (g:T' ->A)
  (identityT
     (sigT Type [T:Type] T ->A) (existT Type [T:Type] T ->A T f)
     (existT Type [T:Type] T ->A T' g)) ->
  (x:T)
  (x':T')
  (identityT
     (sigT Type [T0:Type]T0) (existT Type [T0:Type]T0 T x)
     (existT Type [T0:Type]T0 T' x')) ->(identityT ? (f x) (g x')).
Intros T T' A f g H'; Try Assumption.
Cut (identityT ? T T').
Intros H'0; Try Assumption.
Generalize H'; Clear H'.
Generalize g; Clear g.
Generalize f; Clear f.
Rewrite <- H'0.
Intros f g H' x x' H'1; Try Assumption.
Rewrite (depidT_idT H'1).
Rewrite (depidT_idTfun H').
Auto with core.
Rewrite (depidT_idTtype H').
Auto with core.
Defined.

Definition subtel_Tc_Tc:
  (t, t':tel) (subtel t t') ->
  (T:Type) (f:T ->tel) (identityT ? t (Tc f)) ->
  (T':Type) (g:T' ->tel) (identityT ? t' (Tc g)) ->
  (sumT
     (prodT
        (identityT ? T T')
        (x:T)
        (x':T')
        (identityT
           ? (existT Type [T0:Type]T0 T x) (existT Type [T0:Type]T0 T' x')) ->
        (subtel (f x) (g x'))) (x:T')(subtel (Tc f) (g x))).
Intros t t' H'; Try Assumption.
Case H'.
Intros H'0 T f H'1; Try Assumption.
Inversion H'1.
Intros T T' H'0 f g H'1 T0 f0 H'2 T'0 g0 H'3; Try Assumption.
Left.
Split.
Apply trans_idT with T.
Injection H'2.
Auto with core.
Apply trans_idT with T'.
Auto with core.
Injection H'3.
Auto with core.
Intros x x' H'4; Try Assumption.
Injection H'2.
Intros H'5 H'6; Try Assumption.
Case (coerce_type H'6 x).
Intros x0 H'7; Try Assumption.
Cut (identityT ? (f0 x) (f x0)).
Intros H'8; Try Assumption.
Rewrite H'8.
Injection H'3.
Intros H'9 H'10; Try Assumption.
Case (coerce_type H'10 x').
Intros x1 H'11; Try Assumption.
Cut (identityT ? (g0 x') (g x1)).
Intros H'12; Try Assumption.
Rewrite H'12.
Apply H'1.
Apply trans_idT with (existT Type [T0:Type]T0 T1 x).
Auto with core.
Apply trans_idT with (existT Type [T0:Type]T0 T'0 x').
Auto with core.
Auto with core.
Apply identityT_fun with T := T'0 T' := T'.
Auto with core.
Auto with core.
Apply identityT_fun with T := T1 T' := T.
Auto with core.
Auto with core.
Intros t0 T f H'0 T0 f0 H'1 T' g H'2; Try Assumption.
Right.
Intros x; Try Assumption.
Rewrite <- H'1.
Injection H'2.
Intros H'3 H'4; Try Assumption.
Case (coerce_type H'4 x).
Intros x0 H'5; Try Assumption.
Cut (identityT ? (g x) (f x0)).
Intros H'6; Try Assumption.
Rewrite H'6.
Apply H'0.
Apply identityT_fun with T := T' T' := T.
Auto with core.
Auto with core.
Defined.

Definition mixtel: (t1, t2:tel) (subtel t1 t2) ->(t3:tel) (subtel t1 t3) ->tel.
Fix 1.
Intros t1.
Case t1.
Intros t2 H' t3 H'0.
Exact (concat_tel t2 t3).
Intros T f.
Fix mixtel2 1.
Intros t2.
Case t2.
Intros H' t3 H'0.
Inversion H'.
Intros T0 g.
Intros H'.
Case (!subtel_Tc_Tc
        (Tc f) (Tc g) H' T f (refl_identityT ? (Tc f)) T1 g
        (refl_identityT ? (Tc g))).
Intros H'0.
Case H'0; Clear H'0.
Intros H'0 H'1.
Fix mixtel3 1.
Intros t3.
Case t3.
Intros H'2.
Inversion H'2.
Intros T0 h H'2.
Case (!subtel_Tc_Tc
        (Tc f) (Tc h) H'2 T f (refl_identityT ? (Tc f)) T2 h
        (refl_identityT ? (Tc h))).
Intros H'3.
Case H'3; Clear H'3.
Intros H'3 H'4.
Apply (!Tc T).
Intros x.
Case (coerce_type (sym_idT ? ? ? H'3) x).
Intros x0 H'5.
Case (coerce_type (sym_idT ? ? ? H'0) x).
Intros x1 H'6.
Exact (mixtel ? ? (H'1 x x1 H'6) ? (H'4 x x0 H'5)).
Intros H'3.
Apply (!Tc T2).
Intros x.
Exact (mixtel3 ? (H'3 x)).
Intros H'0 t3 H'1.
Apply (!Tc T1).
Intros x.
Exact (mixtel2 ? (H'0 x) t3 H'1).
Defined.

Axiom extT:
      (T, T':Type) (f, g:T ->T') ((x:T)(identityT ? (f x) (g x))) ->
      (identityT ? f g).
Hints Resolve extT :core.

Lemma concat_tel_T0: (t:tel)(identityT ? (concat_tel t T0) t).
Induction t.
Simpl.
Auto with core.
Simpl.
Intros T t0 H'; Try Assumption.
Cut (identityT ? [x:T](concat_tel (t0 x) T0) t0).
Intros H'0; Try Assumption.
Rewrite H'0.
Auto with core.
Auto with core.
Qed.
Hints Resolve concat_tel_T0 :core.

Lemma subtel_concat: (t1, t2:tel)(subtel t1 (concat_tel t1 t2)).
Induction t1.
Simpl.
Auto with core.
Simpl.
Intros T t H' t2; Try Assumption.
Apply subtel_Tc.
Auto with core.
Intros x x' H'0; Try Assumption.
Rewrite (depidT_idT H'0).
Apply (H' x' t2).
Qed.
Hints Resolve subtel_concat :core.(*                                   Lemma mixtel1:                                     (t1, t2:tel) (s2:(subtel t1 t2)) (t3:tel) (s3:(subtel t1 t3))                                     (subtel t2 (mixtel s2 s3)).                                   Induction t1.                                   Simpl; Auto with core.                                   Induction t2.                                   Auto with core.                                   Intros T0 t0 H' s2; Try Assumption.                                   Case s2.                                   Simpl.                                   Auto with core.                                   Simpl.                                   Intros T0 T' i f g s; Try Assumption.                                   Induction t3.                                   Intros s3; Try Assumption.                                   Inversion s3.                                   Intros T0 t4 H'0 s3; Try Assumption.                                   Simpl.                                   Inversion s3; Try Assumption.                                   Case (subtel_Tc_Tc s3 (refl_identityT tel (Tc f)) (refl_identityT tel (Tc t4))).                                   Intros p; Try Assumption.                                   Case p.                                   Intros prodT1 prodT2; Try Assumption.                                   Case (coerce_type (sym_idT Type T2 T3 prodT3) x).                                   Apply extT.                                   Auto with core.                                   Intros T0 t0 H' H'0; Try Assumption.                                   Simpl.                                   Intros x; Try Assumption. .......                                   *)

22/01/99, 13:46