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