Beta.v

Section Beta_Whnf.

  Fixpoint whnf_beta [t:term]: Prop :=
    Cases t of
      (App u v) => (whnf_beta u) /\ (T,t:term)~u=(Abs T t)
    | _ => True
    end.

  Hints Unfold whnf_beta : pts.

  Lemma beta_red_whnf: (e:env)(t,u:term)(red beta e t u)->(whnf_beta t)
                          ->(whnf_beta u).
(Induction 1; Simpl; Intros; Auto with arith pts).
Generalize H1 .
(Elim H0; Simpl; Auto with arith pts).
(Induction 1; Simpl; Intros).
Inversion_clear H3.
(Elim H5 with T M; Auto with arith pts).

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

(Elim H2 with M t0; Auto with arith pts).

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

  Lemma whnf_head_normal: (t:term)(whnf_beta t)->(e:env)(head_normal beta e t).
(Red; Intros).
Generalize H .
Elim H0.
Induction 1.
(Induction 1; Simpl; Intros).
Inversion_clear H3.
(Elim H5 with T M; Auto with arith pts).

(Red; Red; Intros).
Inversion_clear H5.

(Red; Red; Intros).
Inversion_clear H5.

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

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

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

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

(Red; Red; Intros).
Inversion_clear H5.

(Red; Red; Intros).
Inversion_clear H5.

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

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

  Lemma whnf_app_list: (args:(list term))(e:env)(t:term)
      (whnf_beta t)->((A,M:term)~t=(Abs A M))
        ->(head_normal beta e (app_list args t)).
(Induction args; Simpl; Intros; Auto with arith pts).
(Apply whnf_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_ord := [x,y:approx]
      (lexprod value [_]value (R_exp beta) [_]subterm (f1 x) (f1 y)).

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

  Hints Resolve beta_app_list_ctxt : pts.

  Lemma beta_whnf_rec: (e:env)(t:term)(args:(list term))
          (sn (ctxt beta) e (app_list args t))
     -> { u:term | (red beta e (app_list args t) u) & (head_normal beta e u) }.
Intros.
Pattern e t args .
Apply (Acc3_rec ? ? ? whnf_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_app_list; Simpl; Intros; Auto with arith pts).
Discriminate.

(Exists (app_list args (Ref n)); Auto with arith pts).
(Apply whnf_app_list; Simpl; Intros; Auto with arith pts).
Discriminate.

Generalize H .
(Case args; Simpl; Intros).
(Exists (Abs t0 t1); Simpl; Auto with arith pts).
(Apply whnf_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.
Auto with arith pts.

(Red; Simpl).
Left.
Apply Rex_intro.
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_app_list; Simpl; Intros; Auto with arith pts).
Discriminate.

Apply Acc_Acc3.
Unfold whnf_ord .
Apply (Acc_inverse_image approx (sigS 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_whnf: (e:env)(t:term)(sn (ctxt beta) e t)
     -> { u:term | (red beta e t u) & (head_normal beta e u) }.
Realizer [e:env][t:term](beta_whnf_rec e t (nil term)).
Program_all.
Save.

End Beta_Whnf.

Section Confluence_Beta.

  Inductive beta_par_red1: env->term->term->Prop :=
    par_beta : (e:env)(M,M',T:term)(beta_par_red1 (cons (Ax T) e) M M')
                      -> (N,N':term)(beta_par_red1 e N N')
                      -> (beta_par_red1 e (App (Abs T M) N) (subst N' M'))
  | sort_par_red_b: (e:env)(s:sort)(beta_par_red1 e (Srt s) (Srt s))
  | ref_par_red_b : (e:env)(n:nat)(beta_par_red1 e (Ref n) (Ref n))
  | abs_par_red_b : (e:env)(M,M',T,T':term)
                         (beta_par_red1 (cons (Ax T') e) M M')
                      -> (beta_par_red1 e T T')
                      -> (beta_par_red1 e (Abs T M) (Abs T' M'))
  | app_par_red_b : (e:env)(M,M':term)(beta_par_red1 e M M')
                      -> (N,N':term)(beta_par_red1 e N N')
                      -> (beta_par_red1 e (App M N) (App M' N'))
  | prod_par_red_b : (e:env)(M,M':term)(beta_par_red1 e M M')
                      -> (N,N':term)(beta_par_red1 (cons (Ax M') e) N N')
                      -> (beta_par_red1 e (Prod M N) (Prod M' N')).

  Hints Resolve par_beta sort_par_red_b ref_par_red_b abs_par_red_b
       app_par_red_b prod_par_red_b : pts.

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

  Hints Resolve refl_beta_par_red1 : pts.

  Lemma beta_red_par_red1: (e:env)(M,N:term)(ctxt beta e M N)
                               ->(beta_par_red1 e M N).
(Induction 1; Auto with arith pts; Intros).
(Elim H0; Auto with arith pts).
Save.

  Lemma beta_par_red1_red: (e:env)(M,N:term)(beta_par_red1 e M N)->(red beta e M N).
(Induction 1; Intros; Auto with arith pts).
(Red; Red).
(Apply rt_trans with (App (Abs T M') N'); Auto with arith pts).
Change (red beta e0 (App (Abs T M0) N0) (App (Abs T M') N')).
Auto with arith pts.
Save.

  Lemma beta_par_red1_stable_env: (R_stable_env beta_par_red1).
Red.
(Induction 1; Auto with arith pts).
Save.

  Lemma beta_par_red1_lift: (R_lift beta_par_red1).
Red.
(Induction 1; Simpl; Intros; Auto with arith pts).
(Rewrite -> distr_lift_subst; Auto with arith pts).
(Apply par_beta; 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 abs_par_red_b; 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_b; 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 beta_par_red1_lift : pts.

  Lemma beta_par_red1_subst_l: (t,u:term)(g:env)(beta_par_red1 g t u)
        ->(v:term)(n:nat)(e:env)(trunc n e g)
        ->(beta_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 beta_par_red1_subst_rec: (d:decl)(x,y,t,u:term)(e,g:env)
              (beta_par_red1 g x y)
            ->(beta_par_red1 e t u)
            ->(n:nat)(f:env)(sub_in_env g d x n e f)
            ->(beta_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_beta; Auto with arith pts).
(Fold (subst_decl x (Ax T) n); Auto with arith pts).

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

(Apply abs_par_red_b; Auto with arith pts).
(Apply (beta_par_red1_stable_env beta_par_red1
         (cons (subst_decl x (Ax T') n) f)); Auto with arith pts).
Apply R_env_hd.
Simpl.
Apply rd_ax.
(Apply beta_par_red1_subst_l with g; Auto with arith pts).
(Elim H5; Auto with arith pts).

(Apply prod_par_red_b; Auto with arith pts).
(Apply (beta_par_red1_stable_env beta_par_red1
         (cons (subst_decl x (Ax M') n) f)); Auto with arith pts).
Apply R_env_hd.
Simpl.
Apply rd_ax.
(Apply beta_par_red1_subst_l with g; Auto with arith pts).
(Elim H5; Auto with arith pts).
Save.

  Lemma beta_par_red1_subst: (e:env)(x,y,t,u,T:term)
                  (beta_par_red1 (cons (Ax T) e) t u)->(beta_par_red1 e x y)
                              ->(beta_par_red1 e (subst x t) (subst y u)).
Intros.
Unfold subst .
(Apply beta_par_red1_subst_rec with (Ax T) (cons (Ax T) e) e; Auto with arith pts).
Save.

  Lemma confluence_beta_par_red1: (confluent beta_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 beta_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 beta_par_red1_subst with T; Auto with arith pts).

(Apply par_beta; Auto with arith pts).
(Apply (beta_par_red1_stable_env beta_par_red1 (cons (Ax T) e0)); Auto with arith pts).

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

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

Inversion_clear H0.
(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_b; Auto with arith pts).
(Apply (beta_par_red1_stable_env beta_par_red1 (cons (Ax T') e0)); Auto with arith pts).

(Apply abs_par_red_b; Auto with arith pts).
(Apply (beta_par_red1_stable_env beta_par_red1 (cons (Ax T') e0)); Auto with arith pts).

(Apply (beta_par_red1_stable_env beta_par_red1 (cons (Ax T) e0)); Auto with arith pts).
(Apply (beta_par_red1_stable_env [e:env][x,y:term](beta_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_beta; Auto with arith pts).
(Apply (beta_par_red1_stable_env [e:env][x,y:term](beta_par_red1 e y x)
         (cons (Ax T'0) e0));
Auto with arith pts).

(Apply beta_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_b; Auto with arith pts).
(Apply (beta_par_red1_stable_env beta_par_red1 (cons (Ax M') e0)); Auto with arith pts).

(Apply prod_par_red_b; Auto with arith pts).
(Apply (beta_par_red1_stable_env beta_par_red1 (cons (Ax M') e0)); Auto with arith pts).

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

  Theorem church_rosser_red: (church_rosser (ctxt beta)).
Proof (TML_Church_rosser (ctxt beta) beta_par_red1
                 confluence_beta_par_red1 beta_red_par_red1 beta_par_red1_red).

End Confluence_Beta.

  Lemma beta_hn_sort: (e:env)(s:sort)(head_normal beta e (Srt s)).
Proof (hn_sort beta_rule sort_beta_norm).

  Lemma beta_hn_prod: (e:env)(A,B:term)(head_normal beta e (Prod A B)).
Proof (hn_prod beta_rule prod_beta_norm).

  Lemma inv_prod_beta_conv: (product_inversion (conv beta)).
Proof (inv_prod beta_rule church_rosser_red prod_beta_norm).

23/12/98, 14:29