LambdaSound.v
Section Sound_Rules.
Load PTS_spec.
Section Beta_Reduction_Sound.
Hypothesis inv_prod: (product_inversion le_type).
Local le_type_prod_l := (inv_prod_l le_type inv_prod).
Local le_type_prod_r := (inv_prod_r le_type inv_prod).
Theorem
beta_sound: (rule_sound the_PTS beta).
Red.
(Induction 1; Intros).
Inversion_typ H0.
Inversion_typ H2.
(Apply typ_conv_wf with (subst N Ur); Auto with arith pts).
(Apply substitution with V; Auto with arith pts).
(Cut (wf_type the_PTS e0 (Prod V Ur)); Intros).
Inversion_clear H7.
Inversion_typ H8.
(Apply type_conv with U s2; Auto with arith pts).
(Apply subtype_in_env with (cons (Ax T) e0); Auto with arith pts).
Apply R_env_hd.
Apply rd_ax.
Red.
(Apply le_type_prod_l with U Ur; Auto with arith pts).
(Apply wf_var with s1; Auto with arith pts).
(Apply le_type_prod_r with T; Auto with arith pts).
(Apply type_correctness with (Abs T M); Auto with arith pts).
(Apply type_correctness with (App (Abs T M) N); Auto with arith pts).
Save.
End Beta_Reduction_Sound.
Section Delta_Reduction_Sound.
Theorem
delta_sound: (rule_sound the_PTS delta).
Red.
(Destruct 1; Intros).
Inversion_typ H1.
(Apply typ_conv_wf with (lift (S n) (typ_of_decl x0)); Simpl; Auto with arith pts).
(Replace x0 with (Def d T); Simpl).
(Apply definition_lift; Auto with arith pts).
(Apply typ_wf with (Ref n) T0; Auto with arith pts).
(Apply fun_item with e0 n; Auto with arith pts).
(Apply type_correctness with (Ref n); Auto with arith pts).
Save.
End Delta_Reduction_Sound.
End Sound_Rules.
23/12/98, 14:30