Cumul.v

  Inductive cumul: env->term->term->Prop :=
     c_eq: (e:env)(x,y:term)(conv hdr e x y)->(cumul e x y)
   | c_rule: (e:env)(s1,s2:sort)(univ s1 s2)->(cumul e (Srt s1) (Srt s2))
   | c_prod: (e:env)(A,B,C,D:term)(cumul e C A)
                ->(cumul (cons (Ax C) e) B D)
                ->(cumul e (Prod A B) (Prod C D)).

  Local rt_univ := (clos_refl_trans ? univ).
  Local rt_cumul := (R_rt cumul).

  Local cumul_trans: (e:env)(x,y,z:term)(rt_cumul e x y)->(rt_cumul e y z)
                          ->(rt_cumul e x z).
Proof [e:env](rt_trans term (cumul e)).

  Hints Unfold rt_univ rt_cumul : pts.
  Hints Resolve c_eq c_rule c_prod : pts.

  Definition cumul_rule: Basic_rule.
Apply Build_Basic_rule with cumul.
Red.
(Induction 1; Simpl; Intros; Auto with arith pts).
Apply c_eq.
(Apply (conv_lift ? lifts) with 2:=H1; Auto with arith pts).

(Apply c_prod; Auto with arith pts).
Apply H3.
(Replace (Ax (lift_rec (S O) C k)) with (lift_decl (S O) (Ax C) k); Auto with arith pts).

Red.
(Induction 1; Simpl; Intros; Auto with arith pts).
Red.
Cut (R_rt (conv hdr) f (subst_rec s x n) (subst_rec s y n)).
(Induction 1; Intros; Auto with arith pts).
(Apply rt_trans with y0; Auto with arith pts).

(Apply (conv_subst ? substs) with 2:=H1; Auto with arith pts).

Red.
Apply rt_trans with (Prod (subst_rec s C n) (subst_rec s B (S n))).
(Elim H1 with n f; Intros; Auto with arith pts).
Auto 10 with arith pts.

(Apply rt_trans with (Prod y (subst_rec s B (S n))); Auto with arith pts).

(Elim H3 with (S n) (cons (subst_decl s (Ax C) n) f); Intros; Auto 10 with arith pts).
(Apply rt_trans with (Prod (subst_rec s C n) y); Auto with arith pts).

Red.
(Induction 1; Intros; Auto with arith pts).
Apply c_eq.
(Apply stable_conv with R' e0; Auto with arith pts).
Defined.

  Definition cts_pts_functor: PTS_sub_spec :=
        (Build_PTS_sub_spec axiom rule (canonical_subtyping cumul_rule)).

  (* other properties *)

  Local stable_rt_cumul: (R_stable_env rt_cumul).
Proof (R_rt_stable cumul (R_stable cumul_rule)).

  Lemma cumul_prod: (e:env)(T,A,B:term)(rt_cumul (cons (Ax T) e) A B)
                  ->(rt_cumul e (Prod T A) (Prod T B)).
(Induction 1; Intros; Auto 10 with arith pts).
(Apply cumul_trans with (Prod T y); Auto with arith pts).
Save.

  (* inversion de rt_cumul *)

  Inductive cumul_hn_inv: env->term->term->Prop :=
    cuhi_srt: (e:env)(s,s':sort)(rt_univ s s')
                      ->(cumul_hn_inv e (Srt s) (Srt s'))
  | cuhi_ref: (e:env)(n:nat)(cumul_hn_inv e (Ref n) (Ref n))
  | cuhi_abs: (e:env)(A,A',M,M':term)(conv hdr e A A')
                        ->(conv hdr (cons (Ax A') e) M M')
                        ->(cumul_hn_inv e (Abs A M) (Abs A' M'))
  | cuhi_app: (e:env)(u,u',v,v':term)(conv hdr e u u')
                        ->(conv hdr e v v')
                        ->(cumul_hn_inv e (App u v) (App u' v'))
  | cuhi_prod: (e:env)(A,A',B,B':term)(rt_cumul e A' A)
                        ->(rt_cumul (cons (Ax A') e) B B')
                        ->(cumul_hn_inv e (Prod A B) (Prod A' B')).

  Hints Resolve cuhi_srt cuhi_ref cuhi_abs cuhi_app cuhi_prod : pts.

  Lemma inv_cumul_trans: (e:env)(x,y,z:term)
      (cumul_hn_inv e x y)->(cumul_hn_inv e y z)
            ->(cumul_hn_inv e x z).
(Induction 1; Intros; Auto with arith pts).
Inversion_clear H1.
Apply cuhi_srt.
Red.
(Apply rt_trans with s'; Auto with arith pts).

Inversion_clear H2.
Apply cuhi_abs.
(Apply conv_trans with A'; Auto with arith pts).

(Apply conv_trans with M'; Auto with arith pts).
(Apply (stable_conv (conv hdr) (cons (Ax A') e0)); Auto 10 with arith pts).

Inversion_clear H2.
Apply cuhi_app.
(Apply conv_trans with u'; Auto with arith pts).

(Apply conv_trans with v'; Auto with arith pts).

Inversion_clear H2.
Apply cuhi_prod.
(Apply cumul_trans with A'; Auto with arith pts).

(Apply cumul_trans with B'; Auto with arith pts).
(Apply stable_rt_cumul
  with [e:env](transp ? (rt_cumul e)) (cons (Ax A') e0); Auto with arith pts).
Save.

23/12/98, 14:29