Tel_coerce.v
Implicit Arguments On.
Require Export Tel.
(*
Inclusion de télescopes.
idées:
- le télescope vide est minimal.
- si pour tout x, f(x) <= g(x), alors (x:T)f(x) <= (x:T)g(x)
- si pour tout x, t <= f(x), alors t <= (x:T)f(x)
- si pour tous x et y f(x,y) <= g(y,x), alors (x:A)(y:B)f(x,y) <= (y:B)(x:A)g(y,x).
- <= est transitive.
*)
Inductive
subtel: tel -> tel ->Type :=
subtel_T0: (t:tel)(subtel T0 t)
| subtel_Tc:
(T:Type) (f, g:T ->tel) ((x:T)(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))
| subtel_transpose_Tc:
(A, B:Type)
(f:A -> B ->tel)
(g:B -> A ->tel) ((x:A) (y:B)(subtel (f x y) (g y x))) ->
(subtel (Tc [x:A](Tc (f x))) (Tc [x:B](Tc (g x))))
| subtel_trans:
(t, t', t'':tel) (subtel t t') -> (subtel t' t'') ->(subtel t t'') .
Hints Resolve subtel_T0 subtel_Tc subtel_tel_Tc subtel_transpose_Tc : core.
(*
Coercions d'un télescope vers un autre plus petit.
*)
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 f g H'0 H'1; Try Assumption.
Apply el_Tc with x := (el_fst H'1).
Apply coerce_tel with t' := (g (el_fst H'1)).
Apply H'0.
Exact (el_rem H'1).
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).
Intros A B f g H'0 H'1; Try Assumption.
Apply el_Tc with x := (el_fst (el_rem H'1)).
Apply el_Tc with x := (el_fst H'1).
Apply coerce_tel with t' := (g (el_fst H'1) (el_fst (el_rem H'1))).
Apply H'0.
Exact (el_rem (el_rem H'1)).
Intros t0 t'0 t'' H'0 H'1 H'2; Try Assumption.
Apply coerce_tel with t' := t'0; Auto with core.
Apply coerce_tel with t' := t''; Auto with core.
Defined.
Lemma
subtel_refl: (t:tel)(subtel t t).
Intros t; Try Assumption.
Elim t; Auto with core.
Qed.
Hints Resolve subtel_refl : core.
22/01/99, 13:45