Soundness.v



Section Soundness.

  Load PTS_spec.

  Syntactic Definition typ2 := (typ the_PTS).
  Syntactic Definition
wf_type2 := (wf_type the_PTS).


Section SoundnessDef.

  Variable R: red_rule.

  Definition
rule_sound :=
    (e:env)(x,y:term)(R e x y)
      ->(T:term)(
typ2 e x T)->(typ2 e y T).

End SoundnessDef.


Section Sound_context.


  Variable the_rule: Basic_rule.

  Local R := (Rule the_rule).
  Local Rlifts: (R_lift R) := (R_lifts the_rule).

  Hints Resolve Rlifts : pts.


  Hypothesis incl_R_le_type: (e:env)(x,y:term)(ctxt R e x y)
                                 -> (le_type e y x).



  Theorem red_incl_le_type: (e:env)(x,y:term)(red R e x y)
                               -> (le_type e y x).
(Induction 1; Intros; Auto with arith pts).
(Apply le_type_trans with y0; Auto with arith pts).
Save.


  Theorem
red_in_env: (e:env)(u,v,t,T:term)(typ2 (cons (Ax u) e) t T)
                ->(s:sort)(typ2 e v (Srt s))->(red R e u v)
                  ->(typ2 (cons (Ax v) e) t T).
Intros.
Apply subtype_in_env with 1:=H.
Constructor.
Constructor.
Red.
Auto with arith pts.
Apply red_incl_le_type.
Trivial with arith pts.

(Apply wf_var with s; Trivial with arith pts).
Save.


  Theorem ctxt_sound: (rule_sound R)->(rule_sound (ctxt R)).
Red.
(Induction 2; Auto with arith pts; Intros).
Inversion_typ H3.
(Apply typ_conv_wf with (Prod M U); Auto with arith pts).
(Apply type_conv with (Prod M' U) s; Auto with arith pts).
Inversion_typ H5.
(Apply type_abs with s3; Auto with arith pts).
(Apply type_prod with s1 s2; Auto with arith pts).
(Apply red_in_env with M s1; Auto with arith pts).

(Apply red_in_env with M s1; Auto with arith pts).

Apply incl_R_le_type.
Auto with arith pts.

(Apply type_correctness with (Abs M N); Auto with arith pts).

Inversion_typ H3.
(Apply typ_conv_wf with (Prod N U); Auto with arith pts).
(Apply type_abs with s; Auto with arith pts).

(Apply type_correctness with (Abs N M); Auto with arith pts).

Inversion_typ H3.
(Apply typ_conv_wf with (subst M2 Ur); Auto with arith pts).
(Apply type_app with V; Auto with arith pts).

(Apply type_correctness with (App M1 M2); Auto with arith pts).

Inversion_typ H3.
(Apply typ_conv_wf with (subst M2 Ur); Auto with arith pts).
(Cut (wf_type2 e0 (Prod V Ur)); Intros).
Inversion_clear H7.
Inversion_typ H8.
(Apply type_conv with (subst N2 Ur) s2; Auto with arith pts).
(Apply type_app with V; Auto with arith pts).

Apply red_incl_le_type.
Unfold subst.
(Apply red_subst_l with e0; Auto with arith pts).

(Replace (Srt s2) with (subst M2 (Srt s2)); Auto with arith pts).
(Apply substitution with V; Auto with arith pts).

(Apply type_correctness with M1; Auto with arith pts).

(Apply type_correctness with (App M1 M2); Auto with arith pts).

Inversion_typ H3.
(Apply typ_conv_wf with (Srt s3); Auto with arith pts).
(Apply type_prod with s1 s2; Auto with arith pts).
(Apply red_in_env with M1 s1; Auto with arith pts).

(Apply type_correctness with (Prod M1 M2); Auto with arith pts).

Inversion_typ H3.
(Apply typ_conv_wf with (Srt s3); Auto with arith pts).
(Apply type_prod with s1 s2; Auto with arith pts).

(Apply type_correctness with (Prod M1 M2); Auto with arith pts).
Save.


End Sound_context.


  Theorem incl_sound: (P,Q: red_rule)
                     ((e:env)(x,y:term)(P e x y)->(Q e x y))
                      ->(
rule_sound Q)->(rule_sound P).
Unfold rule_sound .
Intros.
(Apply H0 with x; Auto with arith pts).
Save.

  Theorem union_sound: (P,Q: red_rule)
                      (
rule_sound P)->(rule_sound Q)
                       ->(rule_sound (reunion P Q)).
Red.
(Induction 3; Intros).
(Apply H with x; Auto with arith pts).

(Apply H0 with x; Auto with arith pts).
Save.


  Theorem clos_trans_sound: (P: red_rule)
                      (
rule_sound P)
                       ->(rule_sound [e:env](clos_trans term (P e))).
Red.
(Induction 2; Intros;Auto with arith pts).
(Apply H with x0; Auto with arith pts).
Save.


  Theorem clos_refl_trans_sound: (P: red_rule)
                      (
rule_sound P)->(rule_sound (R_rt P)).
Red.
(Induction 2; Intros; Auto with arith pts).
(Apply H with x0; Auto with arith pts).
Save.


End Soundness.

23/12/98, 14:30