Conv.v

Section Conversion_Decidability.

  Variable the_Rule: Basic_rule.

  Local R := (Rule the_Rule).

  Local stable_ctxt: (R_stable_env (ctxt R)).
Proof (ctxt_stable R (R_stable the_Rule)).

  Hints Resolve stable_ctxt : pts.

  Hypothesis CR: (church_rosser (ctxt R)).

  Hypothesis whnf: (e:env)(t:term)(sn (ctxt R) e t)
                      -> { u:term | (red R e t u) & (head_normal R e u) }.

Section Inversion_Conv.

  Local stable_conv: (R_stable_env (conv R)).
Proof (R_rst_stable (ctxt R) stable_ctxt).

  Inductive conv_hn_inv: env->term->term->Prop :=
    chi_srt: (e:env)(s:sort)(conv_hn_inv e (Srt s) (Srt s))
  | chi_ref: (e:env)(n:nat)(conv_hn_inv e (Ref n) (Ref n))
  | chi_abs: (e:env)(A,A',M,M':term)(conv R e A A')
                  ->(conv R (cons (Ax A') e) M M')
                  ->(conv_hn_inv e (Abs A M) (Abs A' M'))
  | chi_app: (e:env)(u,u',v,v':term)(conv R e u u')
                  ->(conv R e v v')
                  ->(conv_hn_inv e (App u v) (App u' v'))
  | chi_prod: (e:env)(A,A',B,B':term)(conv R e A A')
                  ->(conv R (cons (Ax A') e) B B')
                  ->(conv_hn_inv e (Prod A B) (Prod A' B')).

  Hints Resolve chi_srt chi_ref chi_abs chi_app chi_prod : pts.

  Lemma conv_hn_inv_sym: (e:env)(x,y:term)(conv_hn_inv e x y)
                              ->(conv_hn_inv e y x).
(Induction 1; Intros; Auto with arith pts).
(Apply chi_abs; Auto with arith pts).
(Apply stable_conv with [_:env][_,x:term]x=A (cons (Ax A') e0);
Auto with arith pts).

(Apply chi_prod; Auto with arith pts).
(Apply stable_conv with [_:env][_,x:term]x=A (cons (Ax A') e0);
Auto with arith pts).
Save.

  Lemma conv_hn_inv_trans: (e:env)(x,y,z:term)(conv_hn_inv e x y)
          ->(conv_hn_inv e y z)->(conv_hn_inv e x z).
(Induction 1; Intros; Auto with arith pts).
Inversion_clear H2.
Apply chi_abs.
(Apply conv_trans with A'; Auto with arith pts).

(Apply conv_trans with M'; Auto with arith pts).
(Apply stable_conv with [_:env][_,x:term]x=A'0 (cons (Ax A') e0); Auto with arith pts).

Inversion_clear H2.
Apply chi_app.
(Apply conv_trans with u'; Auto with arith pts).

(Apply conv_trans with v'; Auto with arith pts).

Inversion_clear H2.
Apply chi_prod.
(Apply conv_trans with A'; Auto with arith pts).

(Apply conv_trans with B'; Auto with arith pts).
(Apply stable_conv with [_:env][_,x:term]x=A'0 (cons (Ax A') e0); Auto with arith pts).
Save.

  Lemma inv_red_hn: (e:env)(x,y:term)(red R e x y)->(head_normal R e x)
                          ->(conv_hn_inv e x y).
Induction 1.
(Induction 1; Intros; Auto with arith pts).
(Elim H2 with x1 y1; Auto with arith pts).

(Destruct x; Auto with arith pts).

Intros.
(Apply conv_hn_inv_trans with y0; Auto with arith pts).
Apply H3.
(Apply hn_red_hn with x0; Auto with arith pts).
Save.

  Hints Resolve inv_red_hn : pts.

  Lemma inv_conv_hn: (e:env)(x,y:term)(conv R e x y)
          ->(x',y':term)(red R e x x')->(head_normal R e x')
          ->(red R e y y')->(head_normal R e y')
          ->(conv_hn_inv e x' y').
Intros.
(Elim CR with e x' y'; Intros).
(Apply conv_hn_inv_trans with x0; Auto with arith pts).
(Apply conv_hn_inv_sym; Auto with arith pts).

Change (conv R e x' y').
(Apply conv_trans with x; Auto with arith pts).
(Apply conv_trans with y; Auto with arith pts).
Save.

  Lemma inv_conv_conv: (e:env)(x,y:term)(conv_hn_inv e x y)->(conv R e x y).
(Induction 1; Intros; Auto with arith pts).
Save.

End Inversion_Conv.

  Hints Resolve chi_srt chi_ref chi_abs chi_app chi_prod : pts.
  Hints Resolve inv_conv_conv : pts.

Section Head_Normal_Sorts.

  Hypothesis sort_norm: (e:env)(s:sort)(normal R e (Srt s)).

  Definition is_sort := [t:term]
    Cases t of
      (Srt _) => True
    | _ => False
    end.

  Lemma red_is_sort: (e:env)(t,u:term)(red R e t u) -> (is_sort t)
                          -> (is_sort u).
(Induction 1; Auto with arith pts).
(Destruct x; Simpl; Intros).
(Inversion_clear H0; Simpl; Auto with arith pts).
(Elim sort_norm with e s y; Auto with arith pts).

Elim H1.

Elim H1.

Elim H1.

Elim H1.
Save.

  Lemma sort_is_norm: (e:env)(t:term)(is_sort t) -> (normal R e t).
(Destruct t; Simpl; Auto with arith pts; Intros; Elim H).
Save.

  Lemma hn_sort: (e:env)(s:sort)(head_normal R e (Srt s)).
(Red; Intros).
Apply sort_is_norm.
(Apply red_is_sort with e (Srt s); Simpl; Auto with arith pts).
Save.

End Head_Normal_Sorts.

Section Head_Normal_Products.

  Hypothesis prod_norm: (e:env)(A,B:term)(normal R e (Prod A B)).

  Definition is_prod := [t:term]
    Cases t of
      (Prod _ _) => True
    | _ => False
    end.

  Lemma red_is_prod: (e:env)(t,u:term)(red R e t u) -> (is_prod t)
                          -> (is_prod u).
(Induction 1; Auto with arith pts).
(Destruct x; Simpl; Intros).
(Inversion_clear H0; Simpl; Auto with arith pts).
Elim H1.

Elim H1.

Elim H1.

Elim H1.

(Inversion_clear H0; Simpl; Auto with arith pts).
(Elim prod_norm with e t0 t1 y; Auto with arith pts).
Save.

  Lemma prod_is_norm: (e:env)(t:term)(is_prod t) -> (normal R e t).
(Destruct t; Simpl; Auto with arith pts; Intros; Elim H).
Save.

  Lemma hn_prod: (e:env)(A,B:term)(head_normal R e (Prod A B)).
(Red; Intros).
Apply prod_is_norm.
(Apply red_is_prod with e (Prod A B); Simpl; Auto with arith pts).
Save.

  Lemma inv_R_prod: (e:env)(A,B,C,D:term)(conv R e (Prod A B) (Prod C D))
                ->((conv R e C A)/\ (conv R (cons (Ax C) e) B D)).
Intros.
(Cut (conv_hn_inv e (Prod A B) (Prod C D)); Intros).
(Inversion_clear H0; Auto with arith pts).

(Apply inv_conv_hn with (Prod A B) (Prod C D); Auto with arith pts).
Apply hn_prod.

Apply hn_prod.
Save.

  Lemma inv_prod: (product_inversion (conv R)).
(Apply Build_product_inversion; Intros).
(Elim inv_R_prod with e A B C D; Auto with arith pts).

(Elim inv_R_prod with e A B C D; Auto with arith pts).
Save.

End Head_Normal_Products.

Section Algo_Conversion.

  Local f := [tr:env*term*term]
    Cases tr of (e,(t1,t2)) => ((e,t1),(e,t2)) end.

  Theorem CR_WHNF_convert_hn: (e:env)(x,y:term)
            (sn (ctxt R) e x)
          ->(sn (ctxt R) e y)
          ->(decide (conv_hn_inv e x y)).
Intros e x y sn0 sn1.
Generalize sn0 sn1 .
Pattern e x y .
Apply Acc3_rec with R:=[x,y:env*term*term](ord_conv R (f x) (f y)).
Unfold f .
Clear sn0 sn1 e x y.
Intros e u v.
Case u.
(Case v; Intros).
(Elim eq_sort_dec with s0 s; Intros).
Left.
(Elim y; Auto with arith pts).

(Right; Red; Intros).
Apply y.
(Inversion_clear H0; Auto with arith pts).

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

(Case v; Intros).
(Right; Red; Intros).
Inversion_clear H0.

(Elim eq_nat_dec with n0 n; Intros).
Left.
(Elim y; Auto with arith pts).

(Right; Red; Intros).
Apply y.
(Inversion_clear H0; Auto with arith pts).

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

Intros A M.
(Case v; Intros).
(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

Cut (sn (ctxt R) e A).
Cut (sn (ctxt R) e t).
Intros sn2 sn3.
(Elim whnf with e A; Intros; Auto with arith pts).
(Elim whnf with e t; Intros; Auto with arith pts).
(Elim H with e x x0; Intros).
Cut (sn (ctxt R) (cons (Ax t) e) M).
Cut (sn (ctxt R) (cons (Ax t) e) t0).
Intros sn4 sn5.
(Elim whnf with (cons (Ax t) e) M; Intros; Auto with arith pts).
(Elim whnf with (cons (Ax t) e) t0; Intros; Auto with arith pts).
(Elim H with (cons (Ax t) e) x1 x2; Intros).
Left.
Apply chi_abs.
(Apply conv_trans with x; Auto with arith pts).
(Apply conv_trans with x0; Auto with arith pts).

(Apply conv_trans with x1; Auto with arith pts).
(Apply conv_trans with x2; Auto with arith pts).

(Right; Red; Intros).
Apply y8.
Inversion_clear H0.
(Apply inv_conv_hn with M t0; Auto with arith pts).

(Apply ord_cv_no_swap with M t0; Auto with arith pts).

(Apply sn_red_sn with M; Auto with arith pts).

(Apply sn_red_sn with t0; Auto with arith pts).

(Apply subterm_sn with e (Abs t t0); Auto with arith pts).

(Apply subterm_sn with e (Abs A M); Auto with arith pts).

(Right; Red; Intros).
Apply y3.
Inversion_clear H0.
(Apply inv_conv_hn with A t; Auto with arith pts).

(Apply ord_cv_no_swap with A t; Auto with arith pts).

(Apply sn_red_sn with A; Auto with arith pts).

(Apply sn_red_sn with t; Auto with arith pts).

(Apply subterm_sn with e (Abs t t0); Auto with arith pts).

(Apply subterm_sn with e (Abs A M); Auto with arith pts).

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

Intros u0 v0.
(Case v; Intros).
(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

Cut (sn (ctxt R) e u0).
Cut (sn (ctxt R) e t).
Intros sn2 sn3.
(Elim whnf with e u0; Intros; Auto with arith pts).
(Elim whnf with e t; Intros; Auto with arith pts).
(Elim H with e x x0; Intros).
Cut (sn (ctxt R) e v0).
Cut (sn (ctxt R) e t0).
Intros sn4 sn5.
(Elim whnf with e v0; Intros; Auto with arith pts).
(Elim whnf with e t0; Intros; Auto with arith pts).
(Elim H with e x1 x2; Intros).
Left.
Apply chi_app.
(Apply conv_trans with x; Auto with arith pts).
(Apply conv_trans with x0; Auto with arith pts).

(Apply conv_trans with x1; Auto with arith pts).
(Apply conv_trans with x2; Auto with arith pts).

(Right; Red; Intros).
Apply y8.
Inversion_clear H0.
(Apply inv_conv_hn with v0 t0; Auto with arith pts).

(Apply ord_cv_no_swap with v0 t0; Auto with arith pts).

(Apply sn_red_sn with v0; Auto with arith pts).

(Apply sn_red_sn with t0; Auto with arith pts).

(Apply subterm_sn with e (App t t0); Auto with arith pts).

(Apply subterm_sn with e (App u0 v0); Auto with arith pts).

(Right; Red; Intros).
Apply y3.
Inversion_clear H0.
(Apply inv_conv_hn with u0 t; Auto with arith pts).

(Apply ord_cv_no_swap with u0 t; Auto with arith pts).

(Apply sn_red_sn with u0; Auto with arith pts).

(Apply sn_red_sn with t; Auto with arith pts).

(Apply subterm_sn with e (App t t0); Auto with arith pts).

(Apply subterm_sn with e (App u0 v0); Auto with arith pts).

(Right; Red; Intros).
Inversion_clear H0.

Intros A B.
(Case v; Intros).
(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

(Right; Red; Intros).
Inversion_clear H0.

Cut (sn (ctxt R) e A).
Cut (sn (ctxt R) e t).
Intros sn2 sn3.
(Elim whnf with e A; Intros; Auto with arith pts).
(Elim whnf with e t; Intros; Auto with arith pts).
(Elim H with e x x0; Intros).
Cut (conv R e A t).
Intros cv.
Cut (sn (ctxt R) (cons (Ax t) e) B).
Cut (sn (ctxt R) (cons (Ax t) e) t0).
Intros sn4 sn5.
(Elim whnf with (cons (Ax t) e) B; Intros; Auto with arith pts).
(Elim whnf with (cons (Ax t) e) t0; Intros; Auto with arith pts).
(Elim H with (cons (Ax t) e) x1 x2; Intros).
Left.
Apply chi_prod.
Auto with arith pts.

(Apply conv_trans with x1; Auto with arith pts).
(Apply conv_trans with x2; Auto with arith pts).

(Right; Red; Intros).
Apply y8.
Inversion_clear H0.
(Apply inv_conv_hn with B t0; Auto with arith pts).

(Apply ord_cv_no_swap with B t0; Auto with arith pts).

(Apply sn_red_sn with B; Auto with arith pts).

(Apply sn_red_sn with t0; Auto with arith pts).

(Apply subterm_sn with e (Prod t t0); Auto with arith pts).

(Apply subterm_sn with e (Prod A B); Auto with arith pts).

(Apply conv_trans with x; Auto with arith pts).
(Apply conv_trans with x0; Auto with arith pts).

(Right; Red; Intros).
Apply y3.
Inversion_clear H0.
(Apply inv_conv_hn with A t; Auto with arith pts).

(Apply ord_cv_no_swap with A t; Auto with arith pts).

(Apply sn_red_sn with A; Auto with arith pts).

(Apply sn_red_sn with t; Auto with arith pts).

(Apply subterm_sn with e (Prod t t0); Auto with arith pts).

(Apply subterm_sn with e (Prod A B); Auto with arith pts).

Apply Acc_Acc3.
Apply (Acc_inverse_image env*term*term value*value).
Unfold ord_conv f .
Apply Acc_clos_trans.
Apply Acc_swapprod.
(Apply sn_acc_ord_norm1; Auto with arith pts).

(Apply sn_acc_ord_norm1; Auto with arith pts).
Save.

  Theorem CR_WHNF_conv_dec: (e:env)(x,y:term)
            (sn (ctxt R) e x)
          ->(sn (ctxt R) e y)
          ->(decide (conv R e x y)).
Intros.
(Elim whnf with e x; Intros; Auto with arith pts).
(Elim whnf with e y; Intros; Auto with arith pts).
(Elim CR_WHNF_convert_hn with e x0 x1; Intros).
Left.
(Apply conv_trans with x0; Auto with arith pts).
(Apply conv_trans with x1; Auto with arith pts).

(Right; Red; Intros).
Apply y4.
(Apply inv_conv_hn with x y; Auto with arith pts).

(Apply sn_red_sn with x; Auto with arith pts).

(Apply sn_red_sn with y; Auto with arith pts).
Save.

End Algo_Conversion.

End Conversion_Decidability.

  Hints Resolve chi_srt chi_ref chi_abs chi_app chi_prod : pts.

23/12/98, 14:29