Lambda_Rules.v
Section General_Definitions.
Definition
approx := env*term*(list term).
Fixpoint
app_list [args:(list term)] : term->term :=
[t]Cases args of
nil => t
| (cons hd tl) => (app_list tl (App t hd))
end.
End General_Definitions.
Section Beta_Reduction.
Inductive
beta: env->term->term->Prop :=
beta_intro: (e:env)(M,N,T:term)
(beta e (App (Abs T M) N) (subst N M)).
Hints Resolve beta_intro : pts.
Lemma
beta_rule: Basic_rule.
Apply Build_Basic_rule with beta.
Red.
(Induction 1; Simpl; Intros).
(Rewrite -> distr_lift_subst; Auto with arith pts).
Red.
(Induction 1; Simpl; Intros).
(Rewrite -> distr_subst; Auto with arith pts).
(Red; Intros).
(Elim H; Auto with arith pts).
Defined.
Lemma
sort_beta_norm: (e:env)(s:sort)(normal beta e (Srt s)).
(Red; Red; Intros).
Inversion_clear H.
Save.
Lemma
prod_beta_norm: (e:env)(A,B:term)(normal beta e (Prod A B)).
(Red; Red; Intros).
Inversion_clear H.
Save.
End Beta_Reduction.
Hints Resolve beta_intro : pts.
Section Delta_Reduction.
Inductive
delta: env->term->term->Prop :=
delta_intro: (e:env)(n:nat)(d,T:term)(item (Def d T) e n)
->(delta e (Ref n) (lift (S n) d)).
Lemma
delta_rule: Basic_rule.
Apply Build_Basic_rule with delta.
Red.
(Induction 1; Simpl; Intros).
(Elim (le_gt_dec k n); Intros).
Unfold lift .
(Rewrite -> simpl_lift_rec; Simpl; Auto with arith pts).
Change (delta f (Ref (S n)) (lift (S (S n)) d)).
(Apply delta_intro with T; Auto with arith pts).
(Apply ins_item_ge with 1:=H1; Auto with arith pts).
Unfold lift .
(Replace k with (plus (S n) (minus k (S n))); Auto with arith pts).
(Elim permute_lift_rec with d (S O) (minus k (S n)) (S n) O; Auto with arith pts).
Change (delta f (Ref n) (lift (S n) (lift_rec (S O) d (minus k (S n))))).
Apply delta_intro with (lift_rec (S O) T (minus k (S n))).
Change (item (lift_decl (S O) (Def d T) (minus k (S n))) f n).
(Apply ins_item_lt with 1:=H1; Auto with arith pts).
Red.
(Induction 1; Simpl; Intros).
(Elim (lt_eq_lt_dec n0 n); Intros).
Red.
Elim y.
Generalize H0 .
Clear H0.
(Case n; Simpl; Intros).
Inversion_clear y0.
(Rewrite -> simpl_subst; Auto with arith pts).
Apply rt_step.
Apply delta_intro with T.
(Apply nth_sub_sup with 1:=H1; Auto with arith pts).
Intro.
Rewrite -> y0.
Rewrite -> simpl_subst.
Rewrite y0 in H1.
Generalize H1.
Rewrite nth_sub_eq with 1:=H1 2:=H0.
Intro.
Elim sub_decl_eq_def with 1:=H2.
Auto with arith pts.
Auto with arith pts.
(Red; Apply rt_step).
(Replace n0 with (plus (S n) (minus n0 (S n))); Auto with arith pts).
Unfold lift .
(Elim commut_lift_subst_rec with d s (S n) (minus n0 (S n)) O; Auto with arith pts).
Change (delta f (Ref n) (lift (S n) (subst_rec s d (minus n0 (S n))))).
Apply delta_intro with (subst_rec s T (minus n0 (S n))).
Change (item (subst_decl s (Def d T) (minus n0 (S n))) f n).
(Apply nth_sub_inf with 1:=H1; Auto with arith pts).
(Red; Intros).
Inversion_clear H.
(Elim red_item with R' n (Def d T) e f; Intros; Auto with arith pts).
(Apply delta_intro with T; Auto with arith pts).
(Elim item_trunc with decl n e (Def d T); Intros; Auto with arith pts).
(Elim H with x0; Intros; Auto with arith pts).
Inversion_clear H3.
Generalize H6 .
(Inversion_clear H5; Intros).
(Apply delta_intro with U; Auto with arith pts).
Defined.
Lemma
delta_reduce: (n:nat)(e:env)
{def:term| (delta e (Ref n) def)} + {(x:term)~(delta e (Ref n) x)}.
Realizer [n:nat][e:env]Cases (list_item ? e n) of
(inleft (Ax T)) => (inright term)
| (inleft (Def d T)) => (inleft term (lift (S n) d))
| _ => (inright term)
end.
Program_all.
(Red; Intros).
Inversion_clear H.
Absurd (Ax T)=(Def d T0).
Discriminate.
(Apply fun_item with e n; Auto with arith pts).
Change (delta e (Ref n) (lift (S n) d)).
(Apply delta_intro with T; Auto with arith pts).
(Red; Intros).
Inversion_clear H.
(Elim n0 with (Def d T); Auto with arith pts).
Save.
Lemma
sort_delta_norm: (e:env)(s:sort)(normal delta e (Srt s)).
(Red; Red; Intros).
Inversion_clear H.
Save.
Lemma
prod_delta_norm: (e:env)(A,B:term)(normal delta e (Prod A B)).
(Red; Red; Intros).
Inversion_clear H.
Save.
End Delta_Reduction.
23/12/98, 14:32