# Reduction and Substitutivity in CComega

## Single-step reduction

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.

## Many-Step Reduction

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.

## Conversion

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.