Subtyping_rule.v
(* reduction *)
Definition
red_rule := env->term->term->Prop.
Section RuleOper.
Variable R: red_rule.
(* fermetures refl. trans. *)
Definition
R_rt : red_rule := [e:env](clos_refl_trans term (R e)).
(* reduction dans l'environnement *)
Inductive
red_decl: env->decl->decl->Prop :=
rd_ax: (e:env)(T,U:term)(R e T U)->(red_decl e (Ax T) (Ax U))
| rd_def: (e:env)(d,T,U:term)(R e T U)->(red_decl e (Def d T) (Def d U)).
Inductive
R_in_env: env->env->Prop :=
R_env_hd: (e:env)(t,u:decl)(red_decl e t u)
->(R_in_env (cons t e) (cons u e))
| R_env_tl: (e,f:env)(t:decl)(R_in_env e f)
->(R_in_env (cons t e) (cons t f)).
Lemma
red_item:
(n:nat)(t:decl)(e:env)(item t e n)
->(f:env)(R_in_env e f)
->(item t f n)
\/( (g:env)(trunc (S n) e g)
-> (Ex2 [u:decl](red_decl g t u) [u:decl](item u f n))
/\ (trunc (S n) f g) ).
(Induction 1; Intros).
(Inversion_clear H0; Auto with arith pts).
(Right; Split).
(Exists u; Auto with arith pts).
Inversion_clear H0.
Generalize H1 .
(Inversion_clear H2; Auto with arith pts).
(Inversion_clear H0; Auto with arith pts).
(Inversion_clear H2; Auto with arith pts).
(Elim H1 with f0; Auto with arith pts; Intros).
(Right; Intros).
Inversion_clear H4.
(Elim H2 with g; Auto with arith pts).
(Induction 1; Split; Auto with arith pts; Intros).
(Exists x; Auto with arith pts).
Save.
End RuleOper.
Hints Unfold R_rt : pts.
Hints Resolve rd_ax rd_def R_env_hd R_env_tl : pts.
Section Rule_Props.
Variable R: red_rule.
Definition
R_lift :=
(d1:decl)(g,e:env)(t,u:term)(R e t u)->
(k:nat)(f:env)(ins_in_env g d1 k e f)
->(R f (lift_rec (S O) t k) (lift_rec (S O) u k)).
Definition
R_subst :=
(s:term)(d1:decl)(g,e:env)(t,u:term)(R e t u)->
(n:nat)(f:env)(sub_in_env g d1 s n e f)
->(R_rt R f (subst_rec s t n) (subst_rec s u n)).
Definition
R_stable_env :=
(R':red_rule)(e:env)(x,y:term)(R e x y)
-> (f:env)(R_in_env R' e f)
-> (R f x y).
Record
product_inversion: Prop := {
inv_prod_l: (e:env)(A,B,C,D:term)(R e (Prod A B) (Prod C D))
-> (R e C A);
inv_prod_r: (e:env)(A,B,C,D:term)(R e (Prod A B) (Prod C D))
-> (R (cons (Ax C) e) B D) }.
End Rule_Props.
Record
Basic_rule: Type := {
Rule: red_rule;
R_lifts: (R_lift Rule);
R_substs: (R_subst Rule);
R_stable: (R_stable_env Rule)
}.
(* A subtyping rule is a relation which is a Basic_rule and a preorder
*)
Record
Subtyping_rule: Type := {
Le_type: Basic_rule;
preord: (e:env)(preorder term (Rule Le_type e))
}.
Lemma
iter_R_lift: (R:red_rule)(R_lift R)
->(n:nat)(e,f:env)(trunc n f e)
->(t,u:term)(R e t u)
->(R f (lift n t) (lift n u)).
(Induction 2; Intros).
(Repeat (Rewrite -> lift0); Trivial with arith pts).
Rewrite -> simpl_lift.
Rewrite -> (simpl_lift u).
Unfold 1 3 lift.
(Apply H with x e0 e0; Auto with arith pts).
Save.
Lemma
sub_sort_env_indep: (R:Subtyping_rule)
(e:env)(s1,s2:sort)(Rule (Le_type R) e (Srt s1) (Srt s2))
->(f:env)(Rule (Le_type R) f (Srt s1) (Srt s2)).
Proof.
Intros.
(Cut (Rule (Le_type R) (nil ?) (Srt s1) (Srt s2)); Intros).
(Elim f; Intros; Auto with arith pts).
Fold (lift_rec (1) (Srt s1) O) (lift_rec (1) (Srt s2) O).
(Apply (R_lifts (Le_type R)) with a l l; Auto with arith pts).
(Cut (e:env)
(x,y:term)
(R_rt (Rule (Le_type R)) e x y)->(Rule (Le_type R) e x y);
Intros).
Generalize H.
Clear H.
(Elim e; Trivial with arith pts).
Intros.
Apply H.
(ElimType (EX t:? | (val_ok a t)); Intros).
Fold (subst_rec x (Srt s1) O) (subst_rec x (Srt s2) O).
Apply H0.
(Apply (R_substs (Le_type R)) with a l (cons a l); Auto with arith pts).
(Case a; Intros).
(Split with t; Trivial with arith pts).
(Compute; Trivial with arith pts).
(Split with t; Compute; Trivial with arith pts).
(Elim H0; Intros; Auto with arith pts).
Generalize (preord_refl ? ? (preord R e0)).
Trivial with arith pts.
Generalize (preord_trans ? ? (preord R e0)).
(Unfold transitive; Intros).
(Apply H5 with y0; Auto with arith pts).
Save.
23/12/98, 14:30