Tel_ex.v

Require Export Tel_coerce.

(* Quelques exemples montrant comment on peut récupérer avec les télescopes ce qu'on a avec les Record et les coercions de Coq. t1:=(E:Type)(a1:A1(E))(b1:(B1 E a1)) *)

Variables A1, A2:Type ->Type.
Variable B1:(E:Type) (a:(A1 E))Type.
Variable B2:(E:Type) (a:(A2 E))Type.

Definition t1 := (Tc [E:Type](Tc [a1:(A1 E)](Tc [b1:(B1 E a1)]T0))).

Definition T1 := (el_tel t1).

(* Les projections d'accès aux champs. *)

Definition g_E: T1 ->Type := (!el_nth t1 O).

Definition g_a1: (x:T1)(A1 (g_E x)) := (!el_nth t1 (S O)).

Definition g_b1: (x:T1)(B1 (g_E x) (g_a1 x)) := (!el_nth t1 (S (S O))).

(* Constructeur de T1. *)

Definition Build_T1: (E1:Type) (va1:(A1 E1)) (B1 E1 va1) ->T1 :=
   [E1:Type] [va1:(A1 E1)] [vb1:(B1 E1 va1)]
   (!el_Tc
      ? E1 (!tel_fun t1)
      (!el_Tc
         ? va1 (!tel_fun ((!tel_fun t1) E1))
         (!el_Tc ? vb1 (!tel_fun ((!tel_fun ((!tel_fun t1) E1)) va1)) el_T0))).

(* les élements de T1 comme  types. *)

Coercion g_E : T1 >-> SORTCLASS.

(* Un exemple d'élément de T1. *)
Variable E1:Type.
Variable va1:(A1 E1).
Variable vb1:(B1 E1 va1).

Definition vT1: T1 := (Build_T1 E1 va1 vb1).
Eval Compute in (!tel_nth t1 O vT1).
Eval Compute in (!tel_nth t1 (S O) vT1).
Eval Compute in (!tel_nth t1 (S (S O)) vT1).
Eval Compute in (!el_nth t1 O vT1).
Eval Compute in (!el_nth t1 (S O) vT1).
Eval Compute in (!el_nth t1 (S (S O)) vT1).
Eval Compute in (g_E vT1).
Eval Compute in (g_a1 vT1).
Eval Compute in (g_b1 vT1).

(* vT1 comme type. *)

Variable x1:vT1.

(* Un télescope qui étend t1. *)

Definition t0 :=
   (Tc
      [E:Type]
      (Tc [a1:(A1 E)](Tc [a2:(A2 E)](Tc [b1:(B1 E a1)](Tc [b2:(B2 E a2)]T0))))).

Lemma l1: (subtel t1 t0).
Unfold t1 t0; Auto with core.
Defined.
Hints Resolve l1 : core.

Lemma l2: (t:tel) (subtel t0 t) ->(subtel t1 t).
Intros t H'; Try Assumption.
Apply subtel_trans with t0; Auto with core.
Defined.
Hints Resolve l2 : core.
Variable va2:(A2 E1).
Variable vb2:(B2 E1 va2).

Definition T := (el_tel t0).

Definition vT: T :=
   (!el_Tc
      Type E1
      [E:Type]
      (Tc [a1:(A1 E)](Tc [a2:(A2 E)](Tc [b1:(B1 E a1)](Tc [b2:(B2 E a2)]T0))))
      (!el_Tc
         (A1 E1) va1
         [a1:(A1 E1)](Tc [a2:(A2 E1)](Tc [b1:(B1 E1 a1)](Tc [b2:(B2 E1 a2)]T0)))
         (!el_Tc
            (A2 E1) va2 [a2:(A2 E1)](Tc [b1:(B1 E1 va1)](Tc [b2:(B2 E1 a2)]T0))
            (!el_Tc
               (B1 E1 va1) vb1 [b1:(B1 E1 va1)](Tc [b2:(B2 E1 va2)]T0)
               (!el_Tc (B2 E1 va2) vb2 [b2:(B2 E1 va2)]T0 el_T0))))).
Check (coerce_tel l1 vT).

Definition T_T1: T ->T1 := (!coerce_tel ? ? l1).
Check (T_T1 vT).

(* Coercion de T vers T1. *)

Coercion T_T1 : T >-> T1.

Check (g_E vT).

Eval Compute in (g_E vT).
Eval Compute in (g_a1 vT).
Eval Compute in (g_b1 vT).

22/01/99, 13:46