Mechanized proof of the Church-Rosser theorem

church-rosser.v

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
Require Import Arith.
Import Nat.
Require Import Lia.

(** * Reflexive transitive closure of a relation *)
Definition relation (X : Type) := X -> X -> Prop.
Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : forall (x : X), multi R x x
  | multi_step : forall (x y z : X),
                    R x y ->
                    multi R y z ->
                    multi R x z.

Hint Constructors multi : core.

Theorem multi_R : forall (X : Type) (R : relation X) (x y : X),
    R x y -> (multi R) x y.
Proof.
  econstructor; eauto.
Qed.

Theorem multi_trans :
  forall (X : Type) (R : relation X) (x y z : X),
      multi R x y  ->
      multi R y z ->
      multi R x z.
Proof.
  intros X R x y z G H.
  induction G; auto; econstructor; eauto.
Qed.


(* Reference: Types and Programming Languages, Benjamin Pierce, Chapter 6 *)

(** * Untyped lambda calculus with de Bruijn indices *)
Inductive dexp : Type :=
 | d_var  : nat -> dexp
 | d_abs  : dexp -> dexp
 | d_app  : dexp -> dexp -> dexp.

(** ** Custom syntax *)
Declare Custom Entry dexp.
Notation "<{ e }>" := e (e custom dexp at level 99).
Notation "( x )" := x (in custom dexp, x at level 99).
Notation "x" := x (in custom dexp at level 0, x constr at level 0).
Notation "x y" := (d_app x y) (in custom dexp at level 1, left associativity).
Notation "\, y" :=
  (d_abs y) (in custom dexp at level 90, y custom dexp at level 99,
                     left associativity).
Coercion d_var : nat >-> dexp.

(** ** Identity function *)
Check <{\, 0}>.

Inductive nterm : nat -> dexp -> Prop :=
| nterm_var : forall n k, k < n -> nterm n k
| nterm_abs : forall n t1, nterm (S n) t1 -> nterm n <{\, t1 }>
| nterm_app : forall n t1 t2, nterm n t1 -> nterm n t2 -> nterm n <{t1 t2}>.

(** ** Shifting *)

(* d-place shift of a term t above cutoff c *)
Fixpoint shift (d c : nat) (t : dexp) : dexp :=
  match t with
  | d_var k => match compare c k with
              | Lt => k + d
              | Eq => k + d
              | Gt => k
              end
  | <{\, t1}> => d_abs (shift d (S c) t1)
  | <{t1 t2}> => d_app (shift d c t1) (shift d c t2)
  end.


Eval compute in shift 0 2 <{\, \, 1 (0 2) }>.
Eval compute in shift 0 2 <{\, 0 1 (\, 0 1 2) }>.

Ltac solve_compare :=
  repeat match goal with
         | [ |- context [ match ?x ?= ?y with _ => _ end ] ] =>
           destruct (compare_spec x y); simpl; auto; try lia
         end.

Theorem ex_6_2_3 :
  forall t n d c, nterm n t -> nterm (n + d) (shift d c t).
Proof.
  intros t n d c H.
  generalize dependent d.
  generalize dependent c.
  induction H; intros c d; simpl.
  - solve_compare; constructor; try lia.
  - simpl in IHnterm.
    constructor; auto.
  - constructor; auto.
Qed.



(** ** Lifting *)
(* However, lifting works better in Coq. *)
(* lift shifts all the free variables over by 1 *)

Fixpoint lift (k : nat) (t : dexp) :=
  match t with
  | d_var i => match compare k i with
              | Lt => d_var (S i)
              | Eq => d_var (S i)
              | Gt => d_var i
              end
  | d_abs t' => d_abs (lift (S k) t')
  | d_app t1 t2 => d_app (lift k t1) (lift k t2)
  end.

(* Showing that lift k and shift 1 k are equivalent *)
Theorem lift_shift_1 : forall k t, lift k t = shift 1 k t.
Proof.
  intros k t0.
  generalize dependent k.
  induction t0; intros k; simpl.
  - solve_compare; rewrite add_1_r; auto.
  - congruence.
  - congruence.
Qed.

(** ** Substitution *)
Reserved Notation "'[' j '/' s ']' t" (in custom dexp at level 20, j constr).

Fixpoint substX (j : nat) (s : dexp) (t : dexp) : dexp  :=
  match t with
  | d_var k => match compare k j with
              | Eq => s
              | Lt => t
              | Gt => d_var (pred k)
              end
  | d_abs t1 => d_abs (substX (S j) (lift 0 s) t1)
  | d_app t1 t2 => d_app (substX j s t1) (substX j s t2)
  end

where "'[' j '/' s ']' t" := (substX j s t) (in custom dexp).

Example ex1 : substX 0 <{\, 0}> <{1 0 2}> = <{ 0 (\, 0) 1 }>.
Proof.
  simpl. reflexivity.
Qed.

Theorem ex_6_2_6 :
  forall (n j : nat) (s t : dexp),
    nterm n s -> nterm n t -> j <= n -> nterm n (substX j s t).
Proof.
  intros n j s t H H0 H1.
  generalize dependent j.
  generalize dependent s.
  induction H0; intros s Hs j Hj; simpl.
  - destruct (k ?= j); try constructor; auto.
    lia.
  - constructor.
    apply IHnterm; try lia.
    rewrite lift_shift_1.
    replace (S n) with (n + 1) by lia.
    apply ex_6_2_3; auto.
  - constructor; auto.
Qed.

(** ** Values **)
Inductive value : dexp -> Prop :=
  | v_abs : forall t1, value <{\, t1}>.

Hint Constructors value : core.

(** ** Reduction **)
Reserved Notation "t '-->' t'" (at level 40).

Inductive step : dexp -> dexp -> Prop :=
  | E_app1 : forall t1 t1' t2,
         t1 --> t1' ->
         <{t1 t2}> --> <{t1' t2}>
  | E_app2 : forall t1 t2 t2',
         t2 --> t2' ->
         <{t1 t2}> --> <{t1 t2'}>
  | E_AppAbs : forall t2 t1,
         <{(\, t2) t1}> --> substX 0 t1 t2
  | E_abs : forall t1 t1',
      t1 --> t1' ->
      <{\, t1 }> --> <{\, t1'}>

where "t '-->' t'" := (step t t').


Hint Constructors step : core.

Notation multistep := (multi step).
Notation "t1 '-->>' t2" := (multistep t1 t2) (at level 40).
Hint Resolve multi_refl : core.

Theorem multistep_cong1 :
  forall M M' N, M -->> M' -> <{M N}> -->> <{M' N}>.
Proof.
  intros M M' N H.
  generalize dependent N.
  induction H; intros N.
  - econstructor.
  - eapply multi_trans; eauto with nocore.
    econstructor; econstructor; eauto.
Qed.

Theorem multistep_cong2 :
  forall M N N', N -->> N' -> <{M N}> -->> <{M N'}>.
Proof.
  intros M N N' H.
  generalize dependent M.
  induction H; intros M.
  - econstructor.
  - eapply multi_trans; eauto with nocore.
    eapply multi_step; eauto.
Qed.

Theorem multistep_abs :
  forall M M', M -->> M' -> <{\, M}> -->> <{\, M'}>.
Proof.
  intros M M' H.
  induction H.
  - econstructor.
  - eapply multi_trans; eauto with nocore.
    eapply multi_step; eauto.
Qed.

Hint Resolve multistep_cong1 : core.
Hint Resolve multistep_cong2 : core.
Hint Resolve multistep_abs : core.

(* https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-Lambda-Calculus-Notes.pdf *)
Definition confluence {X} (R : relation X) :=
  forall M N P, (multi R) M N ->
           (multi R) M P ->
           exists Z, (multi R) N Z /\ (multi R) P Z.

Definition church_rosser_stmt := confluence step.

(* property b *)
Definition property_b {X} (R : relation X) :=
  forall M N P, R M N -> R M P -> exists Z, (multi R) N Z /\ (multi R) P Z.

(* diamond property of a relation *)
Definition diamond_property {X} (R : relation X) :=
  forall M N P, R M N -> R M P -> exists Z, R N Z /\ R P Z.

Lemma prop_c_1 {X} :
  forall (R : relation X), diamond_property R ->
  forall M N P, (multi R) M N -> R M P -> exists Z, (multi R) N Z /\ (multi R) P Z.
Proof.
  intros R H M N P H0 H1.
  generalize dependent P.
  induction H0; intros P MP.
  - exists P; eauto.
  - rename z into G.
    pose proof (H _ _ _ H0 MP).
    destruct H2 as [z [Hz Hz1]].
    apply IHmulti in Hz.
    destruct Hz as [Z [GZ zZ]].
    exists Z; eauto.
Qed.

Lemma diamond_property_implies_confluence {X} :
  forall (R : relation X), diamond_property R -> confluence R.
Proof.
  intros R H. unfold diamond_property, confluence.
  intros M N P MN NP.
  generalize dependent P.
  induction MN; intros P HP.
  - exists P; auto.
  - rename z into g.
    pose proof (prop_c_1 R H _ _ _ HP H0).
    destruct H1 as [Z [PZ yZ]].
    apply IHMN in yZ.
    destruct yZ as [Z0 [gZ0 ZZ0]].
    exists Z0; split.
    + assumption.
    + eapply multi_trans; eauto.
Qed.

Lemma diamond_property_implies_church_rosser :
  diamond_property step -> church_rosser_stmt.
Proof.
  apply diamond_property_implies_confluence.
Qed.


Reserved Notation "t '|>' t'" (at level 40).


(** *Parallel one-step reduction **)

Inductive Pstep : dexp -> dexp -> Prop :=
| PE_var : forall (x : nat), x |> x
| PE_app : forall P P' N N',
    P |> P' ->
    N |> N' ->
    <{P N}> |> <{P' N'}>
| PE_abs : forall N N',
    N |> N' ->
    <{\, N }> |> <{\, N' }>
| PE_AppAbs : forall Q Q' N N',
    Q |> Q' ->
    N |> N' ->
    <{(\, Q) N}> |> substX 0 N' Q'

where "t '|>' t'" := (Pstep t t').

Hint Constructors Pstep : core.

Lemma Pstep_refl : forall (P : dexp), P |> P.
Proof.
  induction P; auto.
Qed.

Hint Resolve Pstep_refl : core.

Lemma lem_4_6_a : forall M M', M --> M' -> M |> M'.
Proof.
  intros M M' H.
  induction H; auto.
Qed.

Lemma lem_4_6_b : forall (M M' : dexp), M |> M' -> M -->> M'.
Proof.
  intros M M' H.
  induction H; auto.
  - eapply multi_trans.
    eauto using multistep_cong1 with nocore.
    eauto using multistep_cong2 with nocore.
  - apply multi_trans with (y := <{(\, Q) N'}>).
    + eapply multistep_cong2; eauto.
    + apply multi_trans with (y := <{ (\, Q') N' }>).
      * eapply multistep_cong1; eauto.
      * eapply multi_step; eauto.
Qed.

Lemma lem_4_6_c : forall (M M' : dexp), M -->> M' <-> (multi Pstep) M M'.
Proof.
  intros M M'; split; intros H.
  - induction H; auto.
    econstructor.
    apply lem_4_6_a.
    apply H.
    assumption.
  - induction H; auto.
    eapply lem_4_6_b in H.
    eapply multi_trans; eauto.
Qed.

Lemma lift_lift : forall M n m,
  n <= m -> lift n (lift m M) = lift (S m) (lift n M).
Proof.
  induction M; intros n' m H; simpl.
  - solve_compare; try lia.
    destruct n; solve_compare; auto.
  - rewrite IHM; try lia; auto.
  - rewrite IHM1, IHM2; try lia; auto.
Qed.

Lemma lift_subst : forall M N n m,
  lift (n + m) (substX n N M) = substX n (lift (n + m) N) (lift (n + S m) M).
Proof with auto.
  induction M; intros N n' m; simpl.
  - solve_compare; destruct n, n'; solve_compare; try lia; auto.
  - change (S (n' + m)) with (S n' + m).
    rewrite IHM.
    rewrite (lift_lift _ 0 (n' + m)); auto with arith.
  - congruence.
Qed.

Lemma subst_skip : forall M N m, M = substX m N (lift m M).
Proof.
  intros M.
  induction M; intros N m; simpl.
  - solve_compare; destruct m; auto; solve_compare.
  - congruence.
  - congruence.
Qed.

Lemma subst_avoid : forall M N m n,
  n >= m ->
  substX (S n) (lift m M) (lift m N) = lift m (substX n M N).
Proof with auto.
  intros M N m n H.
  revert m n H M.
  induction N; intros m n' H M; simpl.
  - solve_compare; destruct n; try lia...
  - rewrite <- IHN by lia.
    rewrite lift_lift by lia...
  - rewrite IHN1, IHN2...
Qed.

Lemma subst_subst : forall N1 N2 M n m,
    substX (n + m) N1 (substX m N2 M)
  = substX m (substX (n + m) N1 N2) (substX (n + S m) (lift m N1) M).
Proof with auto.
  intros N1 N2 M n m.
  revert n m N1 N2.
  induction M; intros n' m N1 N2; simpl.
  - solve_compare; apply subst_skip.
  - replace (S (n' + m)) with (n' + S m)...
    replace (S (n' + S m)) with (n' + S (S m))...
    rewrite lift_lift by lia.
    rewrite <- subst_avoid by lia.
    rewrite plus_n_Sm.
    rewrite IHM...
  - congruence.
Qed.

Lemma lift_par :
  forall M M', M |> M' -> forall m, lift m M |> lift m M'.
Proof.
  intros M M' H.
  induction H; intros m; simpl; auto.
  - change (S m) with (0 + S m).
    change m with (0 + m) at 3.
    rewrite lift_subst.
    auto.
Qed.

Lemma subst_par1 :
  forall M M' N, M |> M' -> forall n, substX n M N |> substX n M' N.
Proof with auto.
  intros M M' N H.
  generalize dependent M.
  generalize dependent M'.
  induction N; intros M' M H n'; simpl...
  - destruct (_ ?= _)...
  - pose proof lift_par...
Qed.

Lemma subst_par :
  forall M M' N N' n, M |> M' -> N |> N' -> substX n M N |> substX n M' N'.
Proof with auto.
  intros M M' N N' n HM HN.
  generalize dependent M.
  generalize dependent M'.
  generalize dependent n.
  induction HN; intros n M' M HM; simpl...
  - destruct (_ ?= _)...
  - auto using lift_par.
  - epose proof (subst_subst _ _ _ n 0).
    rewrite add_0_r, add_1_r in H.
    rewrite H.
    constructor; auto using lift_par.
Qed.

(* Lemma 4.7: Substitution lemma *)
Lemma lem_4_7 :
  forall M M' U U' n, M |> M' -> U |> U' -> substX n U M |> substX n U' M'.
Proof.
  intros M M' U U' n H H0.
  apply subst_par; auto.
Qed.

(* Maximum parallel one-step reduct M* of term M *)

Fixpoint max_par_redex t : dexp :=
  match t with
    | d_var _ => t
    | d_app (d_abs t1) t2 =>
      substX 0 (max_par_redex t2) (max_par_redex t1)
    | d_app t1 t2 => d_app (max_par_redex t1) (max_par_redex t2)
    | d_abs t' => d_abs (max_par_redex t')
  end.

Lemma lem_4_8 : forall M M', M |> M' -> M' |> max_par_redex M.
Proof.
  intros M M' H.
  induction H; simpl; auto.
  - destruct P; auto.
    inversion H; subst.
    inversion IHPstep1; auto.
  - apply lem_4_7; auto.
Qed.

Lemma diamond_property_of_pstep : diamond_property Pstep.
Proof.
  intros M N P MN MP.
  exists (max_par_redex M).
  split; apply lem_4_8; auto.
Qed.

Theorem church_rosser : church_rosser_stmt.
Proof.
  assert (diamond_property (multi Pstep)).
  {
    pose proof (diamond_property_implies_confluence _ diamond_property_of_pstep).
    assumption.
  }
  assert (diamond_property (multi step)).
  {
    intros M N P MN MP.
    rewrite lem_4_6_c in *.
    pose proof (H _ _ _ MN MP).
    destruct H0 as [Z [NZ PZ]].
    exists Z; split; rewrite lem_4_6_c; assumption.
  }
  assumption.
Qed.