Library CR
Require Import ARS LC_Basis.
Instance red_PreOrder : PreOrder (star step).
Proof.
constructor; hnf.
- apply starR.
- apply star_trans.
Qed.
Instance red_app_proper :
Proper (star step ==> star step ==> star step) App.
Proof.
cbv. intros s s' A t t' B. transitivity (s' t).
- induction A; eauto using star, step.
- induction B; eauto using star, step.
Qed.
Instance red_lam_proper :
Proper (star step ==> star step) Lam.
Proof.
cbv. intros s s' A. induction A; eauto using star, step.
Qed.
Fixpoint rho (s : term) : term :=
match s with
| Var n => Var n
| App (Lam s) t => beta (rho t) ! rho s
| App s t => App (rho s) (rho t)
| Lam s => Lam (rho s)
end.
Inductive pstep : term -> term -> Prop :=
| pstepV n :
pstep (Var n) (Var n)
| pstepA s s' t t' :
pstep s s' ->
pstep t t' ->
pstep (App s t) (App s' t')
| pstepL s s' :
pstep s s' ->
pstep (Lam s) (Lam s')
| pstepB s s' t t' :
pstep s s' ->
pstep t t' ->
pstep (App (Lam s) t) (beta t' ! s').
Lemma pstep_refl :
reflexive pstep.
Proof.
intros s. induction s ; auto using pstep.
Qed.
Lemma step_pstep :
step <=2 pstep.
Proof.
induction 1; auto using pstep, pstep_refl.
Qed.
Lemma pstep_step :
pstep <=2 star step.
Proof.
intros s t A. induction A.
- reflexivity.
- rewrite IHA1, IHA2. constructor.
- rewrite IHA. constructor.
- rewrite IHA1, IHA2. eauto using star, step.
Qed.
Lemma red_agrees :
star step =2 star pstep.
Proof.
apply interpolation.
- apply step_pstep.
- apply pstep_step.
Qed.
Lemma pstep_substitutive sigma s t :
pstep s t -> pstep (sigma ! s) (sigma ! t).
Proof.
intros A. revert sigma.
induction A as [n | s s' t t' _ IHs _ IHt | s s' _ IHs
| s s' t t' _ IHs _ IHt ];
simpl ; intros sigma.
- apply pstep_refl.
- constructor; auto.
- constructor; auto.
- rewrite subst_beta_com. constructor; auto.
Qed.
Definition psstep (sigma tau : substitution) : Prop :=
forall n, pstep (sigma n) (tau n).
Lemma pstep_up sigma tau :
psstep sigma tau -> psstep (up sigma) (up tau).
Proof.
intros A [|n] ; simpl.
- constructor.
- do 2 rewrite subst_ren. apply pstep_substitutive, A.
Qed.
Lemma pstep_compatible sigma tau s s' :
psstep sigma tau -> pstep s s' -> pstep (sigma ! s) (tau ! s').
Proof.
intros A B. revert sigma tau A.
induction B as [n | s s' t t' _ IHs _ IHt | s s' _ IHs
| s s' t t' _ IHs _ IHt ];
simpl ; intros sigma tau A.
- apply A.
- constructor; auto.
- constructor. apply IHs. apply pstep_up, A.
- rewrite subst_beta_com. constructor.
+ apply IHs. apply pstep_up, A.
+ auto.
Qed.
Lemma triangle_pstep_rho :
triangle pstep rho.
Proof.
intros s s' A.
induction A as [n | s s' t t' As IHs _ IHt | s s' _ IHs
| s s' t t' _ IHs _ IHt ].
- constructor.
- destruct s as [n |u v|u].
+ constructor; assumption.
+ constructor; assumption.
+ inv As. simpl. inv IHs. constructor; assumption.
- constructor; assumption.
- simpl. apply pstep_compatible.
+ intros [|n] ; simpl. exact IHt. constructor.
+ exact IHs.
Qed.
Lemma rho_sound :
sound step rho.
Proof.
apply sound_stable with (S := pstep).
exact red_agrees.
apply triangle_to_sound.
exact triangle_pstep_rho.
exact pstep_refl.
Qed.
Lemma rho_cofinal :
cofinal step rho.
Proof.
apply cofinal_stable with (S := pstep).
exact red_agrees.
apply triangle_to_cofinal.
exact triangle_pstep_rho.
Qed.
Theorem CR :
church_rosser step.
Proof.
apply confluent_CR.
eapply rho_to_confluent.
exact rho_sound.
exact rho_cofinal.
Qed.
Alternatively, CR follows directly from the triangle property, but cofinality of rho
is a useful property in its own right.