BD.v

  Definition beta_delta_rule := (union_basic_rule beta_rule delta_rule).

  Definition beta_delta := (Rule beta_delta_rule).

  Hints Unfold beta_delta : pts.

Section BD_Whnf.

  Fixpoint whnf_bd [e:env; t:term]: Prop :=
     Cases t of
       (Ref n) => Cases (delta_reduce n e) of
                    (inleft _) => False
                  | _ => True
                  end
     | (App u v) => (whnf_bd e u) /\ (T,t:term)~u=(Abs T t)
     | _ => True
     end.

  Hints Unfold whnf_bd delta_reduce : pts.

  Lemma bd_red_whnf: (e:env)(t,u:term)(red beta_delta e t u)->(whnf_bd e t)
                          ->(whnf_bd e u).
(Induction 1; Simpl; Intros; Auto with arith pts).
Generalize H1 .
(Elim H0; Simpl; Auto with arith pts).
Destruct 1.
(Induction 1; Simpl; Intros).
Inversion_clear H4.
(Elim H6 with T M; Auto with arith pts).

(Induction 1; Simpl).
Do 5 Intro.
(Elim (delta_reduce n e1); Intros).
Elim H5.

Elim y1 with (lift (S n) d).
(Apply delta_intro with T; Auto with arith pts).

Intros.
Inversion_clear H4.
(Split; Auto with arith pts).
(Red; Intros).
Clear H3.
Inversion_clear H4 in H2.
Generalize H5 H6 .
Clear H5 H6.
(Inversion_clear H2; Simpl).
Inversion_clear H3.
(Inversion_clear H2; Simpl; Intros).
Inversion_clear H5.
(Elim H3 with T0 M; Auto with arith pts).

Inversion_clear H2.
Simpl.
(Elim (delta_reduce n e0); Intros).
Auto with arith pts.

Elim y0 with (lift (S n) d).
(Apply delta_intro with T0; Auto with arith pts).

Intros.
(Elim H6 with M t0; Auto with arith pts).

Intros.
(Elim H6 with T M; Auto with arith pts).
Save.

  Lemma whnf_bd_head_normal: (e:env)(t:term)(whnf_bd e t)
                            ->(head_normal beta_delta e t).
(Red; Intros).
Generalize H .
Elim H0.
Induction 1.
Destruct 1.
(Induction 1; Simpl; Intros).
Inversion_clear H4.
(Elim H6 with T M; Auto with arith pts).

Destruct 1.
Simpl.
Do 5 Intro.
(Elim (delta_reduce n e1); Intros).
Elim H5.

Elim y1 with (lift (S n) d).
(Apply delta_intro with T; Auto with arith pts).

(Red; Red; Intros).
Inversion_clear H5.
Inversion_clear H6.

Inversion_clear H6.

(Red; Red; Intros).
(Inversion_clear H5; Inversion_clear H6).

(Red; Red; Intros).
Generalize H2 .
(Inversion_clear H5; Inversion_clear H6).
Intros.
Generalize H4 .
(Inversion_clear H5; Simpl; Intros).
Inversion_clear H5.
Generalize H7 .
Inversion_clear H6.
Inversion_clear H5.
(Simpl; Intros).
Inversion_clear H5.
(Elim H9 with T0 M0; Auto with arith pts).

Inversion_clear H5.
Simpl.
(Elim (delta_reduce n e0); Intros).
Auto with arith pts.

Elim y0 with (lift (S n) d).
(Apply delta_intro with T0; Auto with arith pts).

Inversion H5.
(Elim H8 with M0 M; Auto with arith pts).

Inversion H5.
(Elim H8 with T M0; Auto with arith pts).

(Red; Red; Intros).
Generalize H4 .
(Inversion_clear H5; Inversion_clear H6; Simpl; Intros).
Inversion_clear H5.
(Elim H7 with T M; Auto with arith pts).

(Red; Red; Intros).
(Inversion_clear H5; Inversion_clear H6).

(Red; Red; Intros).
(Inversion_clear H5; Inversion_clear H6).

(Red; Red; Intros).
Generalize H1 .
Inversion_clear H2.
(Inversion_clear H3; Simpl; Intros).
Inversion_clear H2.
(Elim H4 with T M; Auto with arith pts).

Inversion_clear H3.
Simpl.
(Elim (delta_reduce n e); Intros).
Auto with arith pts.

Elim y with (lift (S n) d).
(Apply delta_intro with T; Auto with arith pts).

Intros.
Apply H4.
(Apply bd_red_whnf with x; Auto with arith pts).
Save.

  Lemma whnf_bd_app_list: (args:(list term))(e:env)(t:term)
      (whnf_bd e t)->((A,M:term)~t=(Abs A M))
        ->(head_normal beta_delta e (app_list args t)).
(Induction args; Simpl; Intros; Auto with arith pts).
(Apply whnf_bd_head_normal; Auto with arith pts).

(Apply H; Intros).
Simpl;Auto with arith pts.

Discriminate.
Save.

  Local f1:= [a:approx]
    Cases a of
      (e,(t,args)) => (existS value [_]value (e,(app_list args t)) (e,t))
    end.

  Definition whnf_bd_ord := [x,y:approx](lexprod value [_:value]value
                     (R_exp beta_delta) [_:value]subterm (f1 x) (f1 y)).

  Lemma bd_app_list_ctxt: (l:(list term))(e:env)(u,v:term)
   (ctxt beta_delta e u v)
          ->(ctxt beta_delta e (app_list l u) (app_list l v)).
(Induction l; Simpl; Intros; Auto with arith pts).
Save.

  Hints Resolve bd_app_list_ctxt : pts.

  Lemma bd_whnf_rec: (e:env)(t:term)(args:(list term))
          (sn (ctxt beta_delta) e (app_list args t))
     -> { u:term | (red beta_delta e (app_list args t) u)
                  & (head_normal beta_delta e u) }.
Intros.
Pattern e t args .
Apply (Acc3_rec ? ? ? whnf_bd_ord).
Clear H e t args.
Intros e t args.
(Case t; Intros).
(Exists (app_list args (Srt s)); Auto with arith pts).
(Apply whnf_bd_app_list; Simpl; Intros; Auto with arith pts).
Discriminate.

(Elim delta_reduce with n e; Intros).
Inversion_clear y.
(Elim H with e x args; Intros; Auto with arith pts).
(Exists x0; Auto with arith pts).
(Apply red_trans with (app_list args x); Auto with arith pts).
(Red; Red).
Apply rt_step.
Apply bd_app_list_ctxt.
Apply ctx_rule.
(Right; Auto with arith pts).

(Red; Simpl).
Left.
Apply Rex_intro.
Apply bd_app_list_ctxt.
Apply ctx_rule.
(Right; Auto with arith pts).

(Exists (app_list args (Ref n)); Auto with arith pts).
(Apply whnf_bd_app_list; Simpl; Intros; Auto with arith pts).
(Elim delta_reduce with n e; Intros).
Inversion_clear y0.
(Elim y with x; Auto with arith pts).

Auto with arith pts.

Discriminate.

Generalize H .
(Case args; Simpl; Intros).
(Exists (Abs t0 t1); Simpl; Auto with arith pts).
(Apply whnf_bd_head_normal; Auto with arith pts).

(Simpl; Auto with arith pts).
(Elim H0 with e (subst t2 t1) l; Simpl; Intros; Auto with arith pts).
(Exists x; Auto with arith pts).
(Apply red_trans with (app_list l (subst t2 t1)); Auto with arith pts).
(Red; Red).
Apply rt_step.
Apply bd_app_list_ctxt.
(Apply ctx_rule; Left; Auto with arith pts).

(Red; Simpl).
Left.
Apply Rex_intro.
Apply bd_app_list_ctxt.
(Apply ctx_rule; Left; Auto with arith pts).

(Elim H with e t0 (cons t1 args); Intros; Auto with arith pts).
(Exists x; Auto with arith pts).

(Red; Simpl; Right; Auto with arith pts).

(Exists (app_list args (Prod t0 t1)); Simpl; Auto with arith pts).
(Apply whnf_bd_app_list; Simpl; Intros; Auto with arith pts).
Discriminate.

Apply Acc_Acc3.
Unfold whnf_bd_ord.
Apply (Acc_inverse_image approx {_:value & value}).
Simpl.
(Apply acc_A_B_lexprod; Intros).
(Elim H; Intros).
(Apply Acc_intro; Intros; Auto with arith pts).
(Inversion_clear H2; Auto with arith pts).

Exact wf_subterm.

Apply wf_subterm.
Save.

  Theorem beta_delta_whnf: (e:env)(t:term)(sn (ctxt beta_delta) e t)
     -> { u:term | (red beta_delta e t u) & (head_normal beta_delta e u) }.
Realizer [e:env][t:term](bd_whnf_rec e t (nil term)).
Program_all.
Save.

End BD_Whnf.

Section Confluence_Beta_Delta.

  Inductive bd_par_red1: env->term->term->Prop :=
    par_betad : (e:env)(M,M',T:term)(bd_par_red1 (cons (Ax T) e) M M')
                     -> (N,N':term)(bd_par_red1 e N N')
                     -> (bd_par_red1 e (App (Abs T M) N) (subst N' M'))
  | par_delta : (e:env)(d,T,N: term)(n:nat)(bd_par_red1 e (lift (S n) d) N)
                     -> (item (Def d T) e n)
                     ->(bd_par_red1 e (Ref n) N)
  | sort_par_red: (e:env)(s:sort)(bd_par_red1 e (Srt s) (Srt s))
  | ref_par_red : (e:env)(n:nat)(bd_par_red1 e (Ref n) (Ref n))
  | abs_par_red : (e:env)(M,M',T,T':term)(bd_par_red1 (cons (Ax T') e) M M')
                       -> (bd_par_red1 e T T')
                       -> (bd_par_red1 e (Abs T M) (Abs T' M'))
  | app_par_red : (e:env)(M,M':term)(bd_par_red1 e M M')
                       -> (N,N':term)(bd_par_red1 e N N')
                       -> (bd_par_red1 e (App M N) (App M' N'))
  | prod_par_red : (e:env)(M,M':term)(bd_par_red1 e M M')
                        -> (N,N':term)(bd_par_red1 (cons (Ax M') e) N N')
                        -> (bd_par_red1 e (Prod M N) (Prod M' N')).

  Hints Resolve par_betad sort_par_red ref_par_red abs_par_red app_par_red prod_par_red : pts.

  Lemma refl_bd_par_red1 : (M:term)(e:env)(bd_par_red1 e M M).
Induction M; Auto with arith pts.
Save.

  Hints Resolve refl_bd_par_red1 : pts.

  Lemma incl_bd_par_red1: (e:env)(M,N:term)(ctxt beta_delta e M N)
                               ->(bd_par_red1 e M N).
(Induction 1; Auto with arith pts; Intros).
(Elim H0; Intros; Auto with arith pts).
(Elim H1; Auto with arith pts).

(Elim H1; Intros).
(Apply par_delta with d T; Auto with arith pts).
Save.

  Lemma bd_par_red1_red: (e:env)(M,N:term)(bd_par_red1 e M N)
        ->(red beta_delta e M N).
(Induction 1; Intros; Auto with arith pts).
(Apply red_trans with (App (Abs T M') N'); Auto 10 with arith pts).
(Red; Red).
Apply rt_step.
Apply ctx_rule.
(Left; Auto with arith pts).

(Apply red_trans with (lift (S n) d); Auto with arith pts).
(Red; Red).
Apply rt_step.
Apply ctx_rule.
Right.
(Apply delta_intro with T; Auto with arith pts).
Save.

  Lemma bd_par_red1_stable_env: (R_stable_env bd_par_red1).
Red.
(Induction 1; Intros; Auto with arith pts).
(Elim red_item with R' n (Def d T) e0 f; Intros; Auto with arith pts).
(Apply par_delta with d T; Auto with arith pts).

(Elim item_trunc with decl n e0 (Def d T); Intros; Auto with arith pts).
(Elim H4 with x0; Intros; Auto with arith pts).
Inversion_clear H6.
Generalize H9 .
(Inversion_clear H8; Intros).
(Apply par_delta with d U; Auto with arith pts).
Save.

  Lemma bd_par_red1_lift: (R_lift bd_par_red1).
Red.
(Induction 1; Simpl; Intros; Auto with arith pts).
(Rewrite -> distr_lift_subst; Auto with arith pts).
(Apply par_betad; Auto with arith pts).
(Replace (Ax (lift_rec (S O) T k)) with (lift_decl (S O) (Ax T) k); Auto with arith pts).

(Elim (le_gt_dec k n); Intros).
(Apply par_delta with d T; Auto with arith pts).
Unfold lift .
(Replace (S (S n)) with (plus (S O) (S n)); Auto with arith pts).
(Elim simpl_lift_rec with d (S n) O (S O) k; Auto with arith pts).
(Simpl; Auto with arith pts).

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

(Apply par_delta
  with (lift_rec (S O) d (minus k (S n)))
       (lift_rec (S O) T (minus k (S n)));
Auto with arith pts).
Unfold lift .
(Rewrite -> permute_lift_rec; Auto with arith pts).
(Replace (plus (S n) (minus k (S n))) with k; Auto with arith pts).

Change (item (lift_decl (S O) (Def d T) (minus k (S n))) f n).
(Apply ins_item_lt with 1:=H3; Auto with arith pts).

(Apply abs_par_red; Auto with arith pts).
(Replace (Ax (lift_rec (S O) T' k)) with (lift_decl (S O) (Ax T') k);
Auto with arith pts).

(Apply prod_par_red; Auto with arith pts).
(Replace (Ax (lift_rec (S O) M' k)) with (lift_decl (S O) (Ax M') k);
Auto with arith pts).
Save.

  Hints Resolve bd_par_red1_lift : pts.

  Lemma bd_par_red1_subst_l: (t,u:term)(g:env)(bd_par_red1 g t u)
        ->(v:term)(n:nat)(e:env)(trunc n e g)
        ->(bd_par_red1 e (subst_rec t v n) (subst_rec u v n)).
(Induction v; Simpl; Intros; Auto with arith pts).
(Elim (lt_eq_lt_dec n0 n); Intros; Auto with arith pts).
(Elim y; Intros; Auto with arith pts).
(Apply iter_R_lift with g; Auto with arith pts).
Save.

  Lemma bd_par_red1_subst_rec: (d:decl)(x,y,t,u:term)(e,g:env)
              (bd_par_red1 g x y)
            ->(bd_par_red1 e t u)
            ->(n:nat)(f:env)(sub_in_env g d x n e f)
            ->(bd_par_red1 f (subst_rec x t n) (subst_rec y u n)).
(Induction 2; Simpl; Intros; Auto with arith pts).
(Rewrite -> distr_subst; Auto with arith pts).
(Apply par_betad; Auto with arith pts).
(Replace (Ax (subst_rec x T n)) with (subst_decl x (Ax T) n); Auto with arith pts).

(Elim (lt_eq_lt_dec n0 n); Intros).
Elim y0.
Generalize H1 H2 H3 .
Clear H1 H2 H3.
(Case n; Intros).
Inversion y1.

(Apply par_delta with d0 T; Auto with arith pts).
Simpl.
(Elim simpl_subst with x d0 (S n1) n0; Auto with arith pts).

Simpl.
(Apply nth_sub_sup with 1:=H4; Auto with arith pts).

Intro.
Rewrite -> y1.
(Elim simpl_subst with x x n n; Auto with arith pts).
Pattern 2 x .
Replace x with d0.
(Apply H2; Auto with arith pts).
(Elim y1; Auto with arith pts).

Rewrite y1 in H4.
Generalize H4.
Rewrite nth_sub_eq with 1:=H4 2:=H3.
Intro.
Elim sub_decl_eq_def with 1:=H5.
Trivial with arith pts.

(Apply par_delta
  with (subst_rec x d0 (minus n0 (S n)))
       (subst_rec x T (minus n0 (S n))); Auto with arith pts).
Unfold lift .
(Rewrite -> commut_lift_subst_rec; Auto with arith pts).
(Replace (plus (S n) (minus n0 (S n))) with n0; Auto with arith pts).

Change (item (subst_decl x (Def d0 T) (minus n0 (S n))) f n).
(Apply nth_sub_inf with 1:=H4; Auto with arith pts).

(Elim (lt_eq_lt_dec n0 n); Intros; Auto with arith pts).
(Elim y0; Auto with arith pts).
Intros.
(Apply iter_R_lift with g; Auto with arith pts).

(Elim H1; Auto with arith pts).

(Apply abs_par_red; Auto with arith pts).
(Apply (bd_par_red1_stable_env bd_par_red1
         (cons (subst_decl x (Ax T') n) f));
Auto with arith pts).
Apply R_env_hd.
Simpl.
Apply rd_ax.
(Apply bd_par_red1_subst_l with g; Auto with arith pts).

(Elim H5; Auto with arith pts).

(Apply prod_par_red; Auto with arith pts).
(Apply (bd_par_red1_stable_env bd_par_red1
         (cons (subst_decl x (Ax M') n) f));
Auto with arith pts).
Apply R_env_hd.
Simpl.
Apply rd_ax.
(Apply bd_par_red1_subst_l with g; Auto with arith pts).

(Elim H5; Auto with arith pts).
Save.

  Lemma bd_par_red1_subst: (e:env)(x,y,t,u,T:term)
                  (bd_par_red1 (cons (Ax T) e) t u)->(bd_par_red1 e x y)
                ->(bd_par_red1 e (subst x t) (subst y u)).
Intros.
Unfold subst .
(Apply bd_par_red1_subst_rec with d:=(Ax T) 1:=H0 2:=H; Auto with arith pts).
Save.

  Lemma confluence_bd_par_red1: (confluent bd_par_red1).
Unfold confluent commut transp .
(Induction 1; Intros).
Inversion_clear H4.
(Elim H1 with M'0; Auto with arith pts; Intros).
(Elim H3 with N'0; Auto with arith pts; Intros).
(Exists (subst x1 x0); Apply bd_par_red1_subst with T; Auto with arith pts).

Inversion_clear H5.
(Elim H1 with M'1; Auto with arith pts; Intros).
(Elim H3 with N'0; Auto with arith pts; Intros).
Exists (subst x1 x0).
(Apply bd_par_red1_subst with T; Auto with arith pts).

(Apply par_betad; Auto with arith pts).
(Apply (bd_par_red1_stable_env bd_par_red1 (cons (Ax T) e0)); Auto with arith pts).

(Apply (bd_par_red1_stable_env [e:env][x,y:term](bd_par_red1 e y x)
         (cons (Ax T') e0));
Auto with arith pts).

Inversion_clear H3.
Apply H1.
(Cut (eq ? (Def d T) (Def d0 T0)); Intros).
Injection H3.
Intros.
(Rewrite -> H7; Auto with arith pts).

(Apply fun_item with e0 n; Auto with arith pts).

(Exists N; Auto with arith pts).
(Apply par_delta with d T; Auto with arith pts).

Inversion_clear H0.
(Exists (Srt s); Auto with arith pts).

Inversion_clear H0.
(Exists z; Auto with arith pts).
(Apply par_delta with d T; Auto with arith pts).

(Exists (Ref n); Auto with arith pts).

Inversion_clear H4.
(Elim H1 with M'0; Auto with arith pts; Intros).
(Elim H3 with T'0; Auto with arith pts; Intros).
(Exists (Abs x1 x0); Auto with arith pts).
(Apply abs_par_red; Auto with arith pts).
(Apply (bd_par_red1_stable_env bd_par_red1 (cons (Ax T') e0)); Auto with arith pts).

(Apply abs_par_red; Auto with arith pts).
(Apply (bd_par_red1_stable_env bd_par_red1 (cons (Ax T') e0)); Auto with arith pts).

(Apply (bd_par_red1_stable_env bd_par_red1 (cons (Ax T) e0)); Auto with arith pts).
(Apply (bd_par_red1_stable_env [e:env][x,y:term](bd_par_red1 e y x)
         (cons (Ax T'0) e0));
Auto with arith pts).

Generalize H0 H1 .
Clear H0 H1.
Inversion_clear H4.
Intro.
Inversion_clear H4.
Intros.
(Elim H4 with (Abs T M'0); Auto with arith pts; Intros).
(Elim H3 with N'0; Auto with arith pts; Intros).
Generalize H8 .
Inversion_clear H7.
(Clear H8; Intro).
Inversion_clear H8.
(Exists (subst x1 M'2); Auto with arith pts).
(Apply par_betad; Auto with arith pts).
(Apply (bd_par_red1_stable_env [e:env][x,y:term](bd_par_red1 e y x)
         (cons (Ax T'0) e0));
Auto with arith pts).

(Apply bd_par_red1_subst with T'0; Auto with arith pts).

Intros.
(Elim H5 with M'0; Auto with arith pts; Intros).
(Elim H3 with N'0; Auto with arith pts; Intros).
(Exists (App x0 x1); Auto with arith pts).

Intros.
Inversion_clear H4.
(Elim H1 with M'0; Auto with arith pts; Intros).
(Elim H3 with N'0; Auto with arith pts; Intros).
(Exists (Prod x0 x1); Auto with arith pts).
(Apply prod_par_red; Auto with arith pts).
(Apply (bd_par_red1_stable_env bd_par_red1 (cons (Ax M') e0)); Auto with arith pts).

(Apply prod_par_red; Auto with arith pts).
(Apply (bd_par_red1_stable_env bd_par_red1 (cons (Ax M') e0)); Auto with arith pts).

(Apply (bd_par_red1_stable_env [e:env][x,y:term](bd_par_red1 e y x)
         (cons (Ax x0) e0));
Auto with arith pts).
(Apply (bd_par_red1_stable_env bd_par_red1 (cons (Ax M'0) e0)); Auto with arith pts).
Save.

  Theorem church_rosser_beta_delta: (church_rosser (ctxt beta_delta)).
Proof (TML_Church_rosser (ctxt beta_delta) bd_par_red1
                 confluence_bd_par_red1 incl_bd_par_red1 bd_par_red1_red).

End Confluence_Beta_Delta.

  Lemma norm_bd_srt: (e:env)(s:sort)(normal beta_delta e (Srt s)).
Intros.
Unfold beta_delta .
Simpl.
(Apply normal_union; Auto with arith pts).
Apply sort_beta_norm.

Apply sort_delta_norm.
Save.

  Lemma norm_bd_prd: (e:env)(A,B:term)(normal beta_delta e (Prod A B)).
Intros.
Unfold beta_delta .
Simpl.
(Apply normal_union; Auto with arith pts).
Apply prod_beta_norm.

Apply prod_delta_norm.
Save.

  Lemma bd_hn_sort: (e:env)(s:sort)(head_normal beta_delta e (Srt s)).
Proof (hn_sort beta_delta_rule norm_bd_srt).

  Lemma bd_hn_prod: (e:env)(A,B:term)(head_normal beta_delta e (Prod A B)).
Proof (hn_prod beta_delta_rule norm_bd_prd).

  Lemma inv_prod_bd_conv: (product_inversion (conv beta_delta)).
Proof (inv_prod beta_delta_rule church_rosser_beta_delta norm_bd_prd).

23/12/98, 14:29