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