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

Inductive step {m} : tm m -> tm m -> Prop :=
| step_beta s t u :
    u = inst (t .: @var m) s -> step (app (lam s) t) u
| step_appL s1 s2 t :
    step s1 s2 -> step (app s1 t) (app s2 t)
| step_appR s t1 t2 :
    step t1 t2 -> step (app s t1) (app s t2)
| step_lam s1 s2 :
    @step m.+1 s1 s2 -> step (lam s1) (lam s2)
| step_prodL A1 A2 B :
    step A1 A2 -> step (prod A1 B) (prod A2 B)
| step_prodR A B1 B2 :
    @step m.+1 B1 B2 -> step (prod A B1) (prod A B2).

Notation red := (star (@step _)).
Notation "s === t" := (conv (@step _) s t) (at level 50).

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

Lemma step_subst m n (sigma : subst m n) s t :
  step s t -> step (inst sigma s) (inst sigma t).
Proof.
  move=> st. elim: st n sigma => //={m s t}; eauto using @step.
  move=> m s t u -> n f; apply: step_beta.
  rewrite !inst_comp; f_equal; fext=> /=; case=> //= i.
  rewrite ren_inst_comp. fsimpl. by rewrite inst_ids.
Qed.

Lemma red_app m (s1 s2 t1 t2 : tm m) :
  red s1 s2 -> red t1 t2 -> red (app s1 t1) (app s2 t2).
Proof.
  move=> A B. apply: (star_trans (app s2 t1)).
  - apply: (star_hom (@app _^~ t1)) A => x y. exact: step_appL.
  - apply: star_hom B => x y. exact: step_appR.
Qed.

Lemma red_lam m (s1 s2 : tm m.+1) :
  red s1 s2 -> red (lam s1) (lam s2).
Proof. apply: star_hom => x y. exact: step_lam. Qed.

Lemma red_prod m (s1 s2 : tm m) t1 t2 :
  red s1 s2 -> red t1 t2 -> red (prod s1 t1) (prod s2 t2).
Proof.
  move=> A B. apply: (star_trans (prod s2 t1)).
  - apply: (star_hom (@prod _^~ t1)) A => x y. exact: step_prodL.
  - apply: star_hom B => x y. exact: step_prodR.
Qed.

Lemma red_subst m n (f : subst m n) s t :
  red s t -> red (inst f s) (inst f t).
Proof. apply: star_hom. exact: step_subst. Qed.

Lemma sred_up m n (f g : subst m n) :
  sred f g -> sred (upi f) (upi g).
Proof.
  move=> A. hnf=>/=-[i|] //=. rewrite !ren_inst. apply: red_subst. exact: A.
Qed.

Hint Resolve @red_app @red_lam @red_prod @sred_up : red_congr.

Lemma red_compat m n (sigma tau : subst m n) s :
  sred sigma tau -> red (inst sigma s) (inst tau s).
Proof. elim: s n sigma tau =>/= *; eauto with red_congr. Qed.

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

Lemma conv_app m (s1 s2 t1 t2 : tm m) :
  s1 === s2 -> t1 === t2 -> app s1 t1 === app s2 t2.
Proof.
  move=> A B. apply: (conv_trans (app s2 t1)).
  - apply: (conv_hom (@app _^~ t1)) A => x y. exact: step_appL.
  - apply: conv_hom B => x y. exact: step_appR.
Qed.

Lemma conv_lam m (s1 s2 : tm m.+1) :
  s1 === s2 -> lam s1 === lam s2.
Proof. apply: conv_hom => x y. exact: step_lam. Qed.

Lemma conv_prod m (s1 s2 : tm m) t1 t2 :
  s1 === s2 -> t1 === t2 -> prod s1 t1 === prod s2 t2.
Proof.
  move=> A B. apply: (conv_trans (prod s2 t1)).
  - apply: (conv_hom (@prod _^~ t1)) A => x y. exact: step_prodL.
  - apply: conv_hom B => x y. exact: step_prodR.
Qed.

Lemma conv_subst m n (sigma : subst m n) s t :
  s === t -> inst sigma s === inst sigma t.
Proof. apply: conv_hom. exact: step_subst. Qed.

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

Lemma conv_compat m n (sigma tau : subst m n) s :
  sconv sigma tau -> inst sigma s === inst tau s.
Proof.
  elim: s n sigma tau => *; eauto using
    @conv_app, @conv_lam, @conv_prod, @sconv_up.
Qed.

Lemma conv_beta m (s : tm m.+1) t1 t2 :
  t1 === t2 -> inst (t1 .: @var _) s === inst (t2 .: @var _) s.
Proof. move=> c. by apply: conv_compat => -[]. Qed.