CumulDec.v
(* on part d'un CTS confluent, avec un algo de whnf, ... *)
Record
subtype_dec_CTS: Set := {
scts_cr: (church_rosser red_step);
scts_hn_sort: (e:env)(s:sort)(head_normal hdr e (Srt s));
scts_hn_prod: (e:env)(A,B:term)(head_normal hdr e (Prod A B));
scts_whnf: (e:env)(t:term)(sn red_step e t)
-> { u:term | (red hdr e t u) & (head_normal hdr e u) };
scts_convert_hn: (e:env)(x,y:term)(sn red_step e x)->(sn red_step e y)
->(decide (conv_hn_inv hd_rule e x y));
scts_rt_univ_dec: (s,s':sort)(decide (rt_univ s s'))
}.
Variable the_scts: subtype_dec_CTS.
(* open it step by step *)
Local CR: (church_rosser red_step) := (scts_cr the_scts).
Local shn_sort := (scts_hn_sort the_scts).
Local shn_prod := (scts_hn_prod the_scts).
Hints Resolve shn_sort shn_prod : pts.
Lemma
commut_red_hnf_rt_cumul: (e:env)(commut term (rt_cumul e)
[x,y:term](red hdr e y x)/\(head_normal hdr e x)).
Red.
Induction 1.
(Induction 1; Intros).
Inversion_clear H2.
(Elim CR with e0 y1 z; Intros; Auto with arith pts).
(Exists x2; Auto 10 with arith pts).
(Split; Auto with arith pts).
(Apply hn_red_hn with z; Auto with arith pts).
Change (conv hdr e0 y1 z).
(Apply conv_trans with x1; Auto with arith pts).
Inversion_clear H2.
(Exists (Srt s2); Auto with arith pts).
(Apply cumul_trans with (Srt s1); Auto 10 with arith pts).
Inversion_clear H5.
(Exists (Prod C D); Auto with arith pts).
(Apply cumul_trans with (Prod A B); Auto 10 with arith pts).
Intros.
(Exists z; Auto with arith pts).
Intros.
(Elim H1 with z0; Intros; Auto with arith pts).
(Elim H3 with x1; Intros; Auto with arith pts).
(Exists x2; Auto with arith pts).
(Apply cumul_trans with x1; Auto with arith pts).
Save.
Lemma
inv_cumul_conv: (e:env)(x,y:term)(conv_hn_inv hd_rule e x y)
->(cumul_hn_inv e x y).
(Induction 1; Intros; Auto 10 with arith pts).
Save.
Lemma
inv_cumul_hn: (e:env)(x,y:term)(rt_cumul e x y)
->(x',y':term)(red hdr e x x')->(head_normal hdr e x')
->(red hdr e y y')->(head_normal hdr e y')
->(cumul_hn_inv e x' y').
Induction 1.
(Induction 1; Intros).
(Apply inv_cumul_conv; Auto with arith pts).
(Apply inv_conv_hn with x1 y1; Auto with arith pts).
Exact CR.
(Cut (conv_hn_inv hd_rule e0 (Srt s1) x'); Intros).
(Cut (conv_hn_inv hd_rule e0 (Srt s2) y'); Intros).
Inversion_clear H6.
(Inversion_clear H7; Auto with arith pts).
(Apply inv_red_hn; Auto with arith pts).
(Apply inv_red_hn; Auto with arith pts).
(Cut (conv_hn_inv hd_rule e0 (Prod A B) x'); Intros).
(Cut (conv_hn_inv hd_rule e0 (Prod C D) y'); Intros).
Inversion_clear H9.
(Inversion_clear H10; Auto with arith pts).
Cut (rt_cumul e0 A'0 A').
Intro.
(Apply cuhi_prod; Auto with arith pts).
(Apply cumul_trans with B; Auto with arith pts).
(Apply stable_rt_cumul
with [e:env](transp ? (rt_cumul e)) (cons (Ax A') e0); Auto with arith pts).
(Apply cumul_trans with D; Auto with arith pts).
(Apply stable_rt_cumul
with [e:env](transp ? (rt_cumul e)) (cons (Ax C) e0); Auto 10 with arith pts).
(Apply cumul_trans with C; Auto with arith pts).
(Apply cumul_trans with A; Auto with arith pts).
(Apply inv_red_hn; Auto with arith pts).
(Apply inv_red_hn; Auto with arith pts).
Intros.
Apply inv_cumul_conv.
(Apply inv_conv_hn with x0 x0; Auto with arith pts).
Exact CR.
Intros.
(Elim commut_red_hnf_rt_cumul with e y0 x0 x'; Intros; Auto with arith pts).
Inversion_clear H8.
(Apply inv_cumul_trans with x1; Auto with arith pts).
Save.
Lemma
inv_cumul_cumul: (e:env)(x,y:term)(cumul_hn_inv e x y)
->(rt_cumul e x y).
(Induction 1; Intros; Auto 10 with arith pts).
(Elim H0; Intros; Auto with arith pts).
(Apply cumul_trans with (Srt y0); Auto with arith pts).
Apply cumul_trans with (Prod A' B).
(Elim H0; Intros; Auto 10 with arith pts).
(Apply cumul_trans with (Prod y0 B); Auto with arith pts).
(Elim H1; Intros; Auto 10 with arith pts).
(Apply cumul_trans with (Prod A' y0); Auto with arith pts).
Save.
Hints Resolve inv_cumul_cumul : pts.
(* open *)
Local conv_hn_dec: (e:env)(x,y:term)(sn red_step e x)->(sn red_step e y)
->(decide (conv_hn_inv hd_rule e x y)) :=
(scts_convert_hn the_scts).
Local rt_univ_dec: (s,s':sort)(decide (rt_univ s s')) :=
(scts_rt_univ_dec the_scts).
Local whnf: (e:env)(t:term)(sn red_step e t)
-> { u:term | (red hdr e t u) & (head_normal hdr e u) } :=
(scts_whnf the_scts).
Local f := [tr:env*term*term]
Cases tr of (e,(t1,t2)) => ((e,t1),(e,t2)) end.
Theorem
CR_WHNF_inv_cumul_dec: (e:env)(x,y:term)
(sn red_step e x)
->(sn red_step e y)
->(decide (cumul_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 hdr (f x) (f y)).
Unfold f .
Clear sn0 sn1 e x y.
Intros e u v.
Case u.
(Case v; Intros).
(Elim rt_univ_dec with s0 s; Intros).
Left.
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.
Intros.
(Elim conv_hn_dec with e (Ref n) v; Intros; Auto with arith pts).
Left.
(Inversion_clear y; Auto with arith pts).
(Right; Red; Intros).
Apply y.
(Inversion_clear H0; Auto with arith pts).
Intros.
(Elim conv_hn_dec with e (Abs t t0) v; Intros; Auto with arith pts).
Left.
(Inversion_clear y; Auto with arith pts).
(Right; Red; Intros).
Apply y.
(Inversion_clear H0; Auto with arith pts).
Intros.
(Elim conv_hn_dec with e (App t t0) v; Intros; Auto with arith pts).
Left.
(Inversion_clear y; Auto with arith pts).
(Right; Red; Intros).
Apply y.
(Inversion_clear H0; Auto with arith pts).
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 hdr) e A).
Cut (sn (ctxt hdr) 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 x0 x; Intros).
Cut (rt_cumul e t A).
Intros cv.
Cut (sn (ctxt hdr) (cons (Ax t) e) B).
Cut (sn (ctxt hdr) (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 cuhi_prod; Auto with arith pts).
(Red; Red).
(Apply rt_trans with x1; Auto with arith pts).
(Apply rt_trans with x2; Auto with arith pts).
Change (rt_cumul (cons (Ax t) e) x1 x2).
Auto with arith pts.
(Right; Red; Intros).
Apply y8.
Inversion_clear H0.
(Apply inv_cumul_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 cumul_trans with x0; Auto 10 with arith pts).
(Apply cumul_trans with x; Auto 10 with arith pts).
(Right; Red; Intros).
Inversion_clear H0.
Apply y3.
(Apply inv_cumul_hn with t A; Auto with arith pts).
(Apply ord_cv_swap with t A; Auto with arith pts).
(Apply sn_red_sn with t; Auto with arith pts).
(Apply sn_red_sn with A; 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_cumul_dec: (e:env)(x,y:term)
(sn red_step e x)
->(sn red_step e y)
->(decide (rt_cumul 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_inv_cumul_dec with e x0 x1; Intros).
Left.
Apply cumul_trans with x0;Auto 10 with arith pts.
Apply cumul_trans with x1;Auto 10 with arith pts.
(Right; Red; Intros).
Apply y4.
(Apply inv_cumul_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.
Lemma
cumul_inv_prod: (product_inversion rt_cumul).
Cut (e:env)(A,B,C,D:term)(rt_cumul e (Prod A B) (Prod C D))
-> (rt_cumul e C A) /\ (rt_cumul (cons (Ax C) e) B D).
(Split; Intros).
(Elim H with e A B C D; Auto with arith pts).
(Elim H with e A B C D; Auto with arith pts).
Intros.
(Cut (cumul_hn_inv e (Prod A B) (Prod C D)); Intros).
(Inversion_clear H0; Auto with arith pts).
(Apply inv_cumul_hn with (Prod A B) (Prod C D); Auto with arith pts).
Save.
23/12/98, 14:29