module plfa.part2.ConfluenceZ4 where

{- Confluence by Z of De Bruijn's λ-calculus with nameless dummies in Agda, based on PLFA 
   Vincent van Oostrom. oostrom@javakade.nl. www.javakade.nl. 

   Developed with emacs in Agda 2.6.1.1 on MAC OS X for PLFA version 20.07. 
   October 2021. Lightly commented version. Comments welcome.

   Constructive confluence is derived from the Z-property (vO, FSCD 2021)
   for the rewrite system having as objects De Bruin's λ-terms with nameless 
   dummies, and beta steps defined using the notion of substitution (and 
   its properties such as self-distributivity of substitution) as defined 
   in the modules Untyped and Substitution of the book
   Programming Language Foundations in Agda,
   Wadler & Kokke & Siek, version 20.07.

   This module may replace the module plfa.part2.Confluence of
   that book (found at https://plfa.inf.ed.ac.uk/20.07/).

   This work is licensed under the Creative Commons Attribution 4.0 
   International License. To view a copy of this license, visit
   http://creativecommons.org/licenses/by/4.0/.
-}

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; cong₂)
open import Function using (_∘_)
open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
  renaming (_,_ to ⟨_,_⟩)
open import plfa.part2.Substitution using (Rename; Subst; rename-subst-commute; subst-commute; ren; cong-sub; extensionality)
open import plfa.part2.Untyped
  using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; begin_; _—→⟨_⟩_; _—↠⟨_⟩_; _∎;
  abs-cong; appL-cong; appR-cong; —↠-trans;
  _⊢_; _∋_; `_; #_; _,_; ★; ƛ_; _·_; _[_];
  rename; ext; exts; Z; S_; subst; subst-zero)

{- Part I -}

{- basic facts on rewriting and substitution, in particular 
   we show that beta is apart from being `closed under contexts'
   as established in plfa, also closed under substitutions, 
   i.e. that we are in a (higher-order) term rewriting setting.
   (these results only depend on Untyped section of plfa)

   φ ranges over steps; Ψ,Χ over many-steps; R over substitution many-steps
-}

{- rewriting is a quasi-congruence for application -}
app-cong : ∀{Γ} {K L M N : Γ ⊢ ★} → K —↠ L → M —↠ N → K · M —↠ L · N
app-cong Ψ Χ = —↠-trans (appL-cong Ψ) (appR-cong Χ)

{- steps are closed under renaming -}
stp-rename : ∀{Γ Δ A} {ρ : Rename Γ Δ} (M : Γ ⊢ A) {N : Γ ⊢ A}
  → M —→ N
    ------------------------
  → rename ρ M —→ rename ρ N
stp-rename (ƛ M) (ζ φ) = ζ (stp-rename M φ)
stp-rename (M · _) (ξ₁ φ) = ξ₁ (stp-rename M φ) 
stp-rename (_ · M) (ξ₂ φ) = ξ₂ (stp-rename M φ)  
stp-rename {ρ = ρ} ((ƛ L) · M) β with β {_} {rename (ext ρ) L} {rename ρ M}
... | G rewrite rename-subst-commute {_}{_}{L}{M}{ρ} = G

{- steps are closed under substitution -}
stp-subst : ∀{Γ Δ A} {σ : Subst Γ Δ} {M M′ : Γ ⊢ A}
  → M —→ M′
    -----------------------
  → subst σ M —→ subst σ M′
stp-subst (ξ₁ φ) = ξ₁ (stp-subst φ) 
stp-subst (ξ₂ φ) = ξ₂ (stp-subst φ)
stp-subst {σ = σ} (β {_} {L} {M}) with β {_} {subst (exts σ) L} {subst σ M}
... | G rewrite subst-commute {_}{_}{L}{M}{σ} = G 
stp-subst {σ = σ} (ζ φ) = ζ (stp-subst  {σ = exts σ} φ)

{- parallel substitution many-step -}
_—↠s_ : ∀{Γ Δ} → Subst Γ Δ → Subst Γ Δ → Set
_—↠s_ {Γ}{Δ} σ τ = ∀{A} → (x : Γ ∋ A) → σ x —↠ τ x

{- applying parallel substitution many-step to term yields many-step -}
trm-subst : ∀{Γ Δ A} {σ τ : Subst Γ Δ}
  → σ —↠s τ
  → (M : Γ ⊢ A)
    -----------------------
  → subst σ M —↠ subst τ M
trm-subst R (` x) = R x
trm-subst {σ = σ} {τ = τ} R (ƛ M) = abs-cong (trm-subst exts-rews M) where
  {- many-step closed under renaming -}
  rew-rename : ∀{Γ Δ A} {ρ : Rename Γ Δ} {M N : Γ ⊢ A}
    → M —↠ N
    ------------------------
    → rename ρ M  —↠ rename ρ N
  rew-rename {ρ = ρ} (M ∎) = (rename ρ M) ∎
  rew-rename {ρ = ρ} (M —→⟨ φ ⟩ Ψ) =  rename ρ M —→⟨ stp-rename _ φ ⟩ rew-rename Ψ
  {- extension lemma for parallel substitution many-steps -}
  exts-rews : ∀{B} → exts σ {B = B} —↠s exts τ 
  exts-rews Z = (` Z) ∎ 
  exts-rews (S x) = rew-rename (R x)
trm-subst R (L · M) = app-cong (trm-subst R L) (trm-subst R M)

{- applying singleton substition many-step to many-step yields many-step -}
rew-rew :  ∀{Γ} {M N : Γ , ★ ⊢ ★ } {K L : Γ ⊢ ★ }
  → M —↠ N
  → K —↠ L
    --------------------
  → M [ K ] —↠ N [ L ]
rew-rew {Γ} {K = K} {L} Ψ Χ = rews-subst Ψ where
  {- lifting many-step to a singleton substitution many-step -}
  rews-zero : subst-zero K —↠s subst-zero L
  rews-zero Z = Χ
  rews-zero (S x) = (` x) ∎
  {- applying parallel substition many-step to many-step yields many-step -}
  rews-subst : ∀{A} {M N : Γ , ★ ⊢ A} → M —↠ N
    → subst (subst-zero K) M —↠ subst (subst-zero L) N
  rews-subst (M ∎) = trm-subst rews-zero M
  rews-subst (_ —→⟨ φ ⟩ Ψ) = _ —→⟨ stp-subst φ ⟩ (rews-subst Ψ)

{- Part II -}

{- beta is shown to have the Z property, taking the function
   mapping a term to the result of its maximal multi-step,
   i.e. full development, as bullet and showing that 
   satisfies upperbound (condition 1) and monotonic (condition 2) 
   for beta steps. based on Loader 97 and van Oostrom 21.
   (these results may replace the Confluence section of plfa) -}

{- take full developments for bullet map; gross/takahashi/loader -}
_• : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A
(` x)• =  ` x
(ƛ M)• = ƛ (M •)
((ƛ M) · N)• =  M • [ N • ]
(M · N)• = (M •) ·(N •)

{- bullet is extensive -}
extensive :  ∀ {Γ A} → (M : Γ ⊢ A) → M —↠ M •
extensive (` _) = _ ∎
extensive (ƛ M) = abs-cong (extensive M)
extensive ((ƛ M) · N) = _  —→⟨ β ⟩ rew-rew (extensive M) (extensive N)
extensive (` _ · N) = appR-cong (extensive N) 
extensive (L · M · N) = app-cong (extensive (L · M)) (extensive N)

{- bullet gives upper bound to co-initial steps (first condition of Z) -}
upperbound : ∀ {Γ} → {M N : Γ ⊢ ★}
  → M —→ N
    --------
  → N —↠ M •
upperbound {_} {ƛ _} (ζ φ) = abs-cong (upperbound φ)
upperbound {_} {(` _) · _} {_} (ξ₂ φ) = appR-cong (upperbound φ)
upperbound {_} {(ƛ _) · M} {((ƛ _) · M)} (ξ₁ (ζ φ)) = _ —→⟨ β ⟩ rew-rew (upperbound φ) (extensive M) 
upperbound {_} {(ƛ L) · _} {.((ƛ L) · _)} (ξ₂ φ) = _ —→⟨ β ⟩ rew-rew (extensive L) (upperbound φ) 
upperbound {_} {(ƛ L) · M} {.(subst (subst-zero M) L)} β = rew-rew (extensive L) (extensive M)
upperbound {_} {_ · _ · M} {.(_ · M)} (ξ₁ φ) = app-cong (upperbound φ) (extensive M)
upperbound {_} {K · L · _} {.(_ · _ · _)} (ξ₂ φ) = app-cong (extensive (K · L)) (upperbound φ)

{- bullet commutes with renaming -}
rename-bullet : ∀{Γ Δ} (ρ : Rename Γ Δ) {A} (M : Γ ⊢ A) → rename ρ (M •) ≡ rename ρ M •
rename-bullet _ (` x) = refl
rename-bullet ρ (ƛ M) = cong ƛ_ (rename-bullet (ext ρ) M)
rename-bullet ρ ((` x) · M) rewrite rename-bullet ρ M = refl
rename-bullet ρ ((ƛ L) · M) rewrite sym (rename-subst-commute {_} {_} {L •} {M •} {ρ}) 
  rewrite rename-bullet ρ M rewrite rename-bullet (ext ρ) L = refl
rename-bullet ρ (K · L · M) = cong₂ _·_ (rename-bullet ρ (K · L)) (rename-bullet ρ M) 

{- bullet commutes with extension -}
exts-bullet : ∀{Γ Δ} {σ τ : Subst Γ Δ}
  → ((x : Γ ∋ ★) → τ x ≡ σ x •)
    ----------------------------------------
  → (x : Γ , ★ ∋ ★) → exts τ x ≡ exts σ x •
exts-bullet eq Z = refl
exts-bullet {σ = σ} eq (S x) rewrite (eq x) = rename-bullet S_ (σ x)

{- rhs lemma for parallel substitution -}
rhss : ∀{Γ Δ} (M : Γ ⊢ ★) {σ  τ : Subst Γ Δ} → ((x : Γ ∋ ★) → τ x ≡ σ x •)
    -----------------------------
  → subst τ (M •) —↠ (subst σ M)•
rhss (` x) eq rewrite (eq x) = _ ∎
rhss (ƛ M) eq = abs-cong (rhss M (exts-bullet eq))
rhss ((` x) · M) {σ} eq rewrite (eq x) = —↠-trans
  (appR-cong (rhss M eq)) (app-bullet (σ x) (subst σ M)) where
  {- auxiliary rhs/monotonicity lemma for application -}
    app-bullet : ∀{Γ} (L M : Γ ⊢ ★) → L • · M • —↠ (L · M)•
    app-bullet (` _) _ = _ ∎
    app-bullet (ƛ _) _ = (_ —→⟨ β ⟩ _ ∎)
    app-bullet (_ · _) _ = _ ∎
rhss ((ƛ L) · M) {τ = τ} eq rewrite (sym (subst-commute {N = L •} {M •} {τ})) = 
  rew-rew (rhss L (exts-bullet eq)) (rhss M eq)
rhss (K · L · M) eq = app-cong (rhss (K · L) eq) (rhss M eq)

{- bullet monotonic for steps (second condition of Z) -}
monotonic : ∀{Γ} → {M N : Γ ⊢ ★}
  → M —→ N
    ----------
  → M • —↠ N •
monotonic (ζ φ) = abs-cong (monotonic φ)
monotonic {_} {(` _) · _} {(` _) · _} (ξ₂ φ) = appR-cong (monotonic φ)
monotonic {Γ} {(ƛ M) · N} {.(subst (subst-zero N) M)} β = rhss M bullet-zero where
  {- bullet commutes with lifting terms to substitutions -} 
  bullet-zero : (x : Γ , ★ ∋ ★) → subst-zero (N •) x ≡ subst-zero N x •
  bullet-zero Z = refl
  bullet-zero (S x) = refl 
monotonic {_} {(ƛ _) · _} {(ƛ _) · _} (ξ₁ (ζ φ)) = rew-rew (monotonic φ) (_ ∎)
monotonic {_} {(ƛ M) · _} {.((ƛ M) · _)} (ξ₂ φ) = rew-rew (M • ∎) (monotonic φ)
monotonic {_} {_ · _ · _} {(ƛ _) · _} (ξ₁ φ) = —↠-trans (appL-cong (monotonic φ)) (_ —→⟨ β ⟩ _ ∎)
monotonic {_} {_ · _ · _} {(` _) · _} (ξ₁ φ) = appL-cong (monotonic φ)
monotonic {_} {_ · _ · _} {_ · _ · _} (ξ₁ φ) = appL-cong (monotonic φ)
monotonic {_} {_ · _ · _} {_ · _ · _} (ξ₂ φ) = appR-cong (monotonic φ)

{- bullet is monotonic for rewrites (abstract from Z)  -}
rew-monotonic : ∀{Γ} → {M N : Γ ⊢ ★}
  → M —↠ N
    ----------
  → M • —↠ N •
rew-monotonic (_ ∎) = _ ∎
rew-monotonic (_ —→⟨ φ ⟩ Ψ) = —↠-trans (monotonic φ) (rew-monotonic Ψ)

{- Barendregt's Strip Lemma for beta (abstract from Z) -}
strip : ∀{Γ} {L M N : Γ ⊢ ★}
  → L —→ M
  → L —↠ N
    -----------------------------------
  → Σ[ K ∈ Γ ⊢ ★ ] (M —↠ K) × (N —↠ K)
strip {L = L} {N = N} φ Ψ = ⟨ N • ,
  ⟨ —↠-trans (upperbound φ) (rew-monotonic Ψ) , extensive N ⟩ ⟩
  
{- confluence of beta (abstract from Z) -}
confluence : ∀{Γ} {L M N : Γ ⊢ ★}
  → L —↠ M
  → L —↠ N
    ------------------------------------
  → Σ[ K ∈ Γ ⊢  ★ ] (M —↠ K) × (N —↠ K)
confluence (_ ∎) Χ = ⟨ _ , ⟨ Χ , _ ∎ ⟩ ⟩
confluence (_ —→⟨ φ ⟩ Ψ) Χ =
  ⟨ _ , ⟨ proj₁ d2 , —↠-trans (proj₂ d1) (proj₂ d2) ⟩ ⟩ where
  d1 = proj₂ (strip φ Χ) 
  d2 = proj₂ (confluence Ψ (proj₁ d1))