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.

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.