# Church-Rosser theorem for CComega

Require Import base ord ars data.fintype ccomega.sorts ccomega.syntax ccomega.reduction.

Inductive pstep {n} : tm n -> tm n -> Prop :=
| pstep_beta s1 s2 t1 t2 u :
u = inst (t2 .: @var _) s2 ->
@pstep n.+1 s1 s2 -> pstep t1 t2 -> pstep (app (lam s1) t1) u
| pstep_var x : pstep (var x) (var x)
| pstep_sort u : pstep (univ _ u) (univ _ u)
| pstep_app s1 s2 t1 t2 :
pstep s1 s2 -> pstep t1 t2 -> pstep (app s1 t1) (app s2 t2)
| pstep_lam s1 s2 :
@pstep n.+1 s1 s2 -> pstep (lam s1) (lam s2)
| pstep_prod s1 s2 t1 t2 :
pstep s1 s2 -> @pstep n.+1 t1 t2 -> pstep (prod s1 t1) (prod s2 t2).

Definition psstep {m n} (sigma tau : subst m n) :=
forall x, pstep (sigma x) (tau x).

Fixpoint rho {n} (s : tm n) : tm n :=
match s with
| app (lam s) t => inst (rho t .: @var _) (rho s)
| app s t => app (rho s) (rho t)
| lam s => lam (rho s)
| prod A B => prod (rho A) (rho B)
| x => x
end.

Lemma pstep_refl n (s : tm n) : pstep s s.
Proof. elim: s; eauto using @pstep. Qed.
Hint Resolve @pstep_refl.

Lemma step_pstep n (s t : tm n) : step s t -> pstep s t.
Proof. elim; eauto using @pstep. Qed.

Lemma pstep_red n (s t : tm n) : pstep s t -> red s t.
Proof.
elim=> {n s t} //=; eauto with red_congr.
move=> n s1 s2 t1 t2 u -> {u} _ A _ B. eapply starES. by econstructor.
apply: (star_trans (inst (t1.:@var _) s2)). exact: red_subst.
by apply: red_compat => -[|].
Qed.

Lemma pstep_subst m n (sigma : subst m n) s t :
pstep s t -> pstep (inst sigma s) (inst sigma t).
Proof.
move=> A. elim: A n sigma => /={m s t}; eauto using @pstep.
move=> m s1 s2 t1 t2 u -> _ A _ B n sigma. eapply pstep_beta; eauto.
rewrite !inst_comp; f_equal; fext=>/=; case=> //=i.
rewrite ren_inst_comp; fsimpl. by rewrite inst_ids.
Qed.

Lemma psstep_up m n (sigma tau : subst m n) :
psstep sigma tau -> psstep (upi sigma) (upi tau).
Proof.
move=> A. hnf=>/=-[i|]//=. rewrite !ren_inst. apply: pstep_subst. exact: A.
Qed.

Lemma pstep_compat m n (sigma tau : subst m n) s t :
psstep sigma tau -> pstep s t -> pstep (inst sigma s) (inst tau t).
Proof with eauto using @pstep, @psstep_up.
move=> A B. elim: B n sigma tau A => //={m s t}...
move=> m s1 s2 t1 t2 u -> _ A _ B n sigma tau C.
apply: (@pstep_beta _ _ (inst (upi tau) s2) _ (inst tau t2))...
rewrite !inst_comp; f_equal; fext=>/=; case=> //=i.
rewrite ren_inst_comp; fsimpl. by rewrite inst_ids.
Qed.

Lemma pstep_compat_beta n (s1 s2 : tm n.+1) t1 t2 :
pstep s1 s2 -> pstep t1 t2 -> pstep (inst (t1 .: @var _) s1) (inst (t2 .: @var _) s2).
Proof.
move=> A B. by apply: pstep_compat A => -[|].
Qed.

Ltac inv H := inversion H; clear H; subst.

Lemma rho_triangle n : triangle (@pstep n) rho.
Proof with eauto using @pstep.
move=> s t. elim=> {n s t} //=...
- move=> n s1 s2 t1 t2 u -> {u} _ A _ B. exact: pstep_compat_beta.
- move=> n s1 s2 t1 t2 A ih1 _ ih2. case: s1 A ih1 => //=...
move=> s A ih1. inv A; inv ih1...
Qed.

Theorem church_rosser n :
CR (@step n).
Proof.
apply: (cr_method (e2 := pstep) (rho := rho)).
exact: step_pstep. exact: pstep_red. exact: rho_triangle.
Qed.
Hint Resolve church_rosser.

## Reduction behaviour

Lemma normal_step_sort n u : normal (@step n) (univ n u).
Proof. move=> [s st]. inversion st. Qed.
Hint Resolve normal_step_sort.

CoInductive RedProdSpec {n} A1 B1 : tm n -> Prop :=
| RedProdSpecI A2 B2 : red A1 A2 -> red B1 B2 -> RedProdSpec A1 B1 (prod A2 B2).

Lemma red_prod_inv n (A1 : tm n) B1 C :
red (prod A1 B1) C -> RedProdSpec A1 B1 C.
Proof.
elim=> {C} [|C D _ [A2 B2]].
- by constructor.
- move=> ra12 rb12 st. inv st; constructor; eauto using star.
Qed.

Lemma inj_sort n u v : univ n u === univ n v -> u = v.
Proof.
move=> A. suff: (univ n u = univ n v) => [[//]|].
eapply cr_conv_normal => //; done.
Qed.

Lemma inj_prod n (A1 A2 : tm n) B1 B2 :
prod A1 B1 === prod A2 B2 -> A1 === A2 /\ B1 === B2.
Proof.
move=>/church_rosser[z /red_prod_inv s1 /red_prod_inv s2].
inv s1; inv s2; split; eauto using join_conv.
Qed.

Lemma conv_prod_sort n A B u :
~(prod A B === univ n u).
Proof.
move=> h. apply cr_star_normal in h => //. apply red_prod_inv in h. inv h.
Qed.