Metatheory.v

  Record PTS_sub_spec: Type := {
    pts_axiom: (relation sort);
    pts_rules: sort->sort->sort->Prop;
    pts_le_type: Subtyping_rule
  }.

  Load PTS_spec.

  Mutual Inductive wf: env->Prop :=
      wf_nil: (wf (nil decl))
    | wf_var: (e:env)(T:term)(s:sort)
                  (typ e T (Srt s))
                ->(wf (cons (Ax T) e))
    | wf_cst: (e:env)(t,T:term)(s:sort)
                  (typ e t T)
                ->(typ e T (Srt s))
                ->(wf (cons (Def t T) e))

  with typ: env->term->term->Prop :=
      type_ax: (e:env)(s1,s2:sort)
                  (wf e)
                ->(axiom s1 s2)
                ->(typ e (Srt s1) (Srt s2))
    | type_var: (e:env)(v:nat)(t:term)
                  (wf e)
                ->(item_lift t e v)
                ->(typ e (Ref v) t)
    | type_abs: (e:env)(T,U,M:term)(s:sort)
                  (typ e (Prod T U) (Srt s))
                ->(typ (cons (Ax T) e) M U)
                ->(typ e (Abs T M) (Prod T U))
    | type_app: (e:env)(u,v,V,Ur:term)
                  (typ e v V)
                ->(typ e u (Prod V Ur))
                ->(typ e (App u v) (subst v Ur))
    | type_prod: (e:env)(T,U:term)(s1,s2,s3:sort)
                  (typ e T (Srt s1))
                ->(typ (cons (Ax T) e) U (Srt s2))
                ->(rule s1 s2 s3)
                ->(typ e (Prod T U) (Srt s3))
    | type_conv: (e:env)(t,U,V:term)(s:sort)
                  (typ e t U)
                ->(le_type e U V)
                ->(typ e V (Srt s))
                ->(typ e t V)
(* sert uniquement quand il y a des sortes non typees: *)
    | type_conv_srt: (e:env)(t,U:term)(s:sort)
                  (typ e t U)
                ->(le_type e U (Srt s))
                ->(typ e t (Srt s)).

  Hints Resolve wf_nil type_ax type_var : pts.

  Definition rule_sat: sort->sort->sort->Prop :=
    [s1,s2,s3](EX x1 | (le_sort s1 x1)
                     & (EX x2 | (le_sort s2 x2) & (rule x1 x2 s3))).

  Lemma type_prod_sat: (e:env)(T,U:term)(s1,s2,s3:sort)
          (typ e T (Srt s1))
        ->(typ (cons (Ax T) e) U (Srt s2))
        ->(rule_sat s1 s2 s3)
        ->(typ e (Prod T U) (Srt s3)).
Intros.
Inversion_clear H1.
Inversion_clear H3.
(Apply type_prod with x x0; Trivial with arith pts).
(Apply type_conv_srt with (Srt s1); Auto with arith pts).

(Apply type_conv_srt with (Srt s2); Auto with arith pts).
Save.

  Theorem typ_wf: (e:env)(t,T:term)(typ e t T)->(wf e).
Induction 1;Auto with arith pts.
Save.

  Theorem inv_wf: (e:env)(d:decl)(wf (cons d e)) -> (wf e).
Intros.
Inversion_clear H.
(Apply typ_wf with T (Srt s); Auto with arith pts).

(Apply typ_wf with T (Srt s); Auto with arith pts).
Save.

  Lemma inv_wf_sort: (e:env)(d:decl)(wf (cons d e))
        -> (EX s:sort | (typ e (typ_of_decl d) (Srt s))).
Intros.
(Inversion_clear H; Exists s; Auto with arith pts).
Save.

  Theorem wf_sort: (e:env)(n:nat)(d:decl)
          (item d e n)
        ->(wf e)
        ->(f:env)(trunc (S n) e f)
        ->(EX s | (typ f (typ_of_decl d) (Srt s))).
Proof.
(Induction 1; Intros).
Apply inv_wf_sort.
(Replace f with l; Trivial with arith pts).
Inversion_clear H1.
(Inversion_clear H2; Trivial with arith pts).

Inversion_clear H3.
(Apply H1; Trivial with arith pts).
Apply inv_wf with 1:=H2.
Save.

  Theorem wf_definition: (n:nat)(e:env)(m,t:term)
        (item (Def m t) e n)
      ->(wf e)
      ->(f:env)(trunc (S n) e f)
      ->(typ f m t).
Proof.
(Induction 1; Intros).
Inversion_clear H0.
(Replace f with l; Trivial with arith pts).
Inversion_clear H1.
(Inversion_clear H0; Trivial with arith pts).

Inversion_clear H3.
(Apply H1; Trivial with arith pts).
Apply inv_wf with 1:=H2.
Save.

  Inductive wf_type [e:env]: term->Prop :=
    wft_typed: (T:term)(s:sort)(typ e T (Srt s))->(wf_type e T)
  | wft_top: (s:sort)(wf_type e (Srt s)).

  Hints Resolve wft_top : pts.

  Definition le_type_wf: red_rule :=
    [e](clos_refl_trans ? [x,y](le_type e x y) /\ (wf_type e y)).
(*   Lemma le_type_wf_le: (e:env)(x,y:term)(le_type_wf e x y)->(le_type e x y). *)

  Definition inv_typ: env->term->term->Prop->Prop :=
    [e:env][t:term][T:term][P:Prop]Cases t of
       (Srt s1) => (s2:sort)(axiom s1 s2)->(le_type e (Srt s2) T)->P
     | (Ref n) => (x:decl)(item x e n)
                      ->(le_type e (lift (S n) (typ_of_decl x)) T)->P
     | (Abs A M) => (s:sort)(U:term)(typ (cons (Ax A) e) M U)
                      ->(typ e (Prod A U) (Srt s))
                      ->(le_type e (Prod A U) T)->P
     | (App u v) => (Ur,V:term)(typ e v V)->(typ e u (Prod V Ur))
                      ->(le_type e (subst v Ur) T)->P
     | (Prod A B) => (s1,s2,s3:sort)(rule s1 s2 s3)->(typ e A (Srt s1))
                      ->(typ (cons (Ax A) e) B (Srt s2))
                      ->(le_type e (Srt s3) T)->P
     end.

  Theorem inv_typ_conv: (e:env)(t,U,V:term)(le_type e U V)
      ->(P:Prop)(inv_typ e t V P)->(inv_typ e t U P).
Do 5 Intro.
Cut (x:term)(le_type e x U)->(le_type e x V).
(Case t; Simpl; Intros).
(Apply H1 with s2; Auto with arith pts).

(Apply H1 with x; Auto with arith pts).

(Apply H1 with s U0; Auto with arith pts).

(Apply H1 with Ur V0; Auto with arith pts).

(Apply H1 with s1 s2 s3; Auto with arith pts).

Intros.
(Apply le_type_trans with U; Auto with arith pts).
Save.

  Theorem inversion_lemma: (e:env)(t,T:term)(P:Prop)
        (inv_typ e t T P)->(typ e t T)->P.
Intros e t T P inv_P j.
(Generalize P inv_P; Clear inv_P P).
(Elim j; Simpl; Intros).
(Apply inv_P with s2; Trivial with arith pts).

Decompose [item_lift] H0.
(Apply inv_P with x; Trivial with arith pts).
(Elim H2; Trivial with arith pts).

(Apply inv_P with s U; Auto with arith pts).

(Apply inv_P with Ur V; Auto with arith pts).

(Apply inv_P with s1 s2 s3; Auto with arith pts).

Apply H0.
(Apply inv_typ_conv with V; Auto with arith pts).

Apply H0.
(Apply inv_typ_conv with (Srt s); Auto with arith pts).
Save.

  Tactic Definition Inversion_typ [$T] :=
    [<:tactic:< Generalize $T; Intro INVTYP;
                Inversion INVTYP using inversion_lemma;
                Unfold inv_typ; Clear INVTYP; Intros >>].

  (* Thinning lemma *)
  Theorem typ_weak: (g:env)(d:decl)(e:env)(t,T:term)
                   (typ e t T)
                 ->(n:nat)(f:env)(ins_in_env g d n e f)
                 ->(wf f)
                 ->(typ f (lift_rec (S O) t n) (lift_rec (S O) T n)).
(Induction 1; Simpl; Intros; Auto with arith pts).
(Elim (le_gt_dec n v); Intros; Apply type_var; Auto with arith pts).
(Elim H1; Intros).
Rewrite -> H4.
Unfold lift .
(Rewrite -> simpl_lift_rec; Simpl; Auto with arith pts).
(Exists x; Auto with arith pts).
(Apply ins_item_ge with 1:=H2; Auto with arith pts).

(Apply ins_item_lift_lt with 1:=H2; Auto with arith pts).

Cut (wf (cons (Ax (lift_rec (S O) T0 n)) f)).
Intro.
(Apply type_abs with s; Auto with arith pts).
(Fold (lift_decl (S O) (Ax T0) n); Auto with arith pts).

Inversion_typ (H1 ? ? H4 H5).
(Apply wf_var with s1; Auto with arith pts).

Rewrite -> distr_lift_subst.
(Apply type_app with (lift_rec (S O) V n); Auto with arith pts).

Cut (wf (cons (Ax (lift_rec (S O) T0 n)) f)).
Intro.
(Apply type_prod with s1 s2; Auto with arith pts).
(Fold (lift_decl (S O) (Ax T0) n); Auto with arith pts).

(Apply wf_var with s1; Auto with arith pts).

(Apply type_conv with (lift_rec (S O) U n) s; Auto with arith pts).
(Apply le_type_lift with 2:=H5; Trivial with arith pts).

(Apply type_conv_srt with (lift_rec (S O) U n); Auto with arith pts).
Fold (lift_rec (S O) (Srt s) n).
(Apply le_type_lift with 2:=H3; Auto with arith pts).
Save.

  Theorem thinning: (e:env)(t,T:term)(d:decl)
                  (typ e t T)
                ->(wf (cons d e))
                ->(typ (cons d e) (lift (S O) t) (lift (S O) T)).
Unfold lift .
Intros.
(Apply typ_weak with e d e; Auto with arith pts).
Save.

  Theorem thinning_n: (n:nat)(e,f:env)(trunc n e f)->(t,T:term)(typ f t T)
                      ->(wf e)->(typ e (lift n t) (lift n T)).
Induction n.
Intros.
Rewrite -> lift0.
Rewrite -> lift0.
(Replace e with f; Auto with arith pts).
(Inversion_clear H; Auto with arith pts).

Do 8 Intro.
Inversion_clear H0.
Intro.
(Rewrite -> simpl_lift; Auto with arith pts).
Pattern (lift (S n0) T) .
(Rewrite -> simpl_lift; Auto with arith pts).
Inversion_clear H0.
Change (typ (cons (Ax T0) e0) (lift (S O) (lift n0 t))
         (lift (S O) (lift n0 T))).
(Apply thinning; Auto with arith pts).
(Apply H with f; Auto with arith pts).
(Apply typ_wf with T0 (Srt s); Auto with arith pts).

(Apply wf_var with s; Auto with arith pts).

Change (typ (cons (Def t0 T0) e0) (lift (S O) (lift n0 t))
         (lift (S O) (lift n0 T))).
(Apply thinning; Auto with arith pts).
(Apply H with f; Auto with arith pts).
(Apply typ_wf with t0 T0; Auto with arith pts).

(Apply wf_cst with s; Auto with arith pts).
Save.

  Theorem wf_sort_lift: (n:nat)(e:env)(t:term)(wf e)->(item_lift t e n)
         ->(EX s:sort | (typ e t (Srt s))).
Induction n.
(Destruct e; Intros).
(Elim H0; Intros).
Inversion_clear H2.

(Elim H0; Intros).
Rewrite -> H1.
Inversion_clear H2.
(Elim inv_wf_sort with l d; Intros; Auto with arith pts).
Exists x0.
(Replace (Srt x0) with (lift (S O) (Srt x0)); Auto with arith pts).
(Apply thinning; Auto with arith pts).

Intros.
(Elim H1; Intros).
Rewrite -> H2.
Generalize H0 .
(Inversion_clear H3; Intros).
(Rewrite -> simpl_lift; Auto with arith pts).
(Elim H with l (lift (S n0) (typ_of_decl x)); Intros; Auto with arith pts).
Exists x0.
(Replace (Srt x0) with (lift (S O) (Srt x0)); Auto with arith pts).
(Apply thinning; Auto with arith pts).

(Apply inv_wf with y; Auto with arith pts).

(Exists x; Auto with arith pts).
Save.

  Theorem definition_lift: (e:env)(n:nat)(t,T:term)(item (Def t T) e n)
             -> (wf e) -> (typ e (lift (S n) t) (lift (S n) T)).
Intros.
(Elim item_trunc with 1:=H; Intros).
(Apply thinning_n with x; Auto with arith pts).
(Apply wf_definition with 1:=H; Trivial with arith pts).
Save.

  Theorem typ_sub: (g:env)(x:term)(d:decl)(typ g x (typ_of_decl d))
                   ->(e:env)(u,U:term)(typ e u U)
                   ->(f:env)(n:nat)(sub_in_env g d x n e f)
                   ->(wf f)
                   ->(typ f (subst_rec x u n) (subst_rec x U n)).
(Induction 2; Simpl; Intros; Auto with arith pts).
(Elim (lt_eq_lt_dec n v); Intros).
Elim H2.
Elim y.
(Case v; Intros).
Inversion_clear y0.

Simpl.
Rewrite -> H5.
(Rewrite -> simpl_subst; Auto with arith pts).
(Apply type_var; Auto with arith pts).
(Exists x0; Auto with arith pts).
(Apply nth_sub_sup with 1:=H3; Auto with arith pts).

Intros.
Rewrite H5.
Elim y0.
(Rewrite simpl_subst; Auto with arith pts).
(Apply thinning_n with g; Auto with arith pts).
(Elim H3; Intros; Auto with arith pts).

Rewrite <- y0 in H6.
Elim nth_sub_eq with 1:=H3 2:=H6.
Trivial with arith pts.

(Apply type_var; Auto with arith pts).
(Apply nth_sub_item_inf with 1:=H3; Auto with arith pts).

(Cut (wf (cons (subst_decl x (Ax T) n) f)); Intros).
(Apply type_abs with s; Auto with arith pts).
(Replace (Ax (subst_rec x T n)) with (subst_decl x (Ax T) n); Auto with arith pts).

(Apply inversion_lemma with f (Prod (subst_rec x T n)
                                  (subst_rec x U0 (S n))) (Srt s);
Simpl; Intros; Auto with arith pts).
(Apply wf_var with s1; Auto with arith pts).

Rewrite -> distr_subst.
(Apply type_app with (subst_rec x V n); Auto with arith pts).

(Cut (wf (cons (Ax (subst_rec x T n)) f)); Intros; Auto with arith pts).
(Apply type_prod with s1 s2; Auto with arith pts).
(Replace (Ax (subst_rec x T n)) with (subst_decl x (Ax T) n); Auto with arith pts).

(Apply wf_var with s1; Auto with arith pts).

(Apply type_conv with (subst_rec x U0 n) s; Auto with arith pts).
(Apply le_type_subst with g d e0; Auto with arith pts).

(Apply type_conv_srt with (subst_rec x U0 n); Auto with arith pts).
Fold (subst_rec x (Srt s) n).
(Apply le_type_subst with g d e0; Auto with arith pts).
Save.

  Theorem substitution: (e:env)(d,t,u,U:term)
                (typ (cons (Ax t) e) u U)
              ->(typ e d t)
              ->(typ e (subst d u) (subst d U)).
Intros.
Unfold subst .
(Apply typ_sub with e (Ax t) (cons (Ax t) e); Auto with arith pts).
(Apply typ_wf with d t; Auto with arith pts).
Save.

  Theorem subtype_in_env: (e:env)(t,T:term)
                  (typ e t T)
                ->(f:env)(R_in_env ge_type e f)
                ->(wf f)
                ->(typ f t T).
(Induction 1; Auto with arith pts; Intros).
Inversion_clear H1.
Rewrite -> H4.
(Elim red_item with ge_type v x e0 f; Intros; Auto with arith pts).
(Apply type_var; Auto with arith pts).
(Exists x; Auto with arith pts).

(Elim item_trunc with decl v e0 x; Auto with arith pts; Intros).
(Elim H1 with x0; Auto with arith pts; Intros).
Inversion_clear H7.
(Elim wf_sort with 1:=H5 3:=H6; Auto with arith pts; Intros).
(Apply type_conv with (lift (S v) (typ_of_decl x1)) x2; Auto with arith pts).
(Apply type_var; Auto with arith pts).
(Exists x1; Auto with arith pts).

(Apply iter_R_lift with x0; Auto with arith pts).
(Elim H9; Auto with arith pts).

(Replace (Srt x2) with (lift (S v) (Srt x2)); Auto with arith pts).
(Apply thinning_n with x0; Auto with arith pts).

(Apply type_abs with s; Auto with arith pts).
(Apply H3; Auto with arith pts).
Inversion_typ (H1 ? H4 H5).
(Apply wf_var with s1; Auto with arith pts).

(Apply type_app with V; Auto with arith pts).

(Apply type_prod with s1 s2; Auto with arith pts).
(Apply H3; Auto with arith pts).
(Apply wf_var with s1; Auto with arith pts).

(Apply type_conv with U s; Auto with arith pts).
(Apply (le_type_stable ge_type e0); Auto with arith pts).

(Apply type_conv_srt with U; Auto with arith pts).
(Apply le_type_stable with ge_type e0; Auto with arith pts).
Save.

  Theorem typ_conv_wf: (e:env)(t,T,U:term)(typ e t T)->(wf_type e U)
            ->(le_type e T U)->(typ e t U).
(Induction 2; Intros).
(Apply type_conv with T s; Auto with arith pts).

(Apply type_conv_srt with T; Auto with arith pts).
Save.

  Theorem wf_type_prod_l: (e:env)(A,B:term)(wf_type e (Prod A B))
                              -> (wf_type e A).
Intros.
Inversion_clear H.
Inversion_typ H0.
(Left with s1; Trivial with arith pts).
Save.

  Theorem wf_type_prod_r: (e:env)(A,B:term)(wf_type e (Prod A B))
                    ->(wf_type (cons (Ax A) e) B).
Intros.
Inversion_clear H.
Inversion_typ H0.
(Left with s2; Trivial with arith pts).
Save.

  Theorem wf_type_subst: (e:env)(v,V,T:term)(wf_type (cons (Ax V) e) T)
            ->(typ e v V)->(wf_type e (subst v T)).
(Induction 1; Intros).
Apply wft_typed with s.
Change (typ e (subst v T0) (subst v (Srt s))).
(Apply substitution with V; Auto with arith pts).

Unfold subst .
(Simpl; Auto with arith pts).
Save.

  Theorem type_correctness: (e:env)(t,T:term)(typ e t T)->(wf_type e T).
(Induction 1; Intros; Auto with arith pts).
(Elim wf_sort_lift with v e0 t0; Intros; Auto with arith pts).
(Apply wft_typed with x; Auto with arith pts).

(Apply wft_typed with s; Auto with arith pts).

(Apply wf_type_subst with V; Auto with arith pts).
(Apply wf_type_prod_r; Auto with arith pts).

(Apply wft_typed with s; Auto with arith pts).
Save.

23/12/98, 14:30