Proof of confluence of beta reduction + D reduction (a simple form of eta for pairs), for the untyped lambda calculus. See http://lambda-the-ultimate.org/node/4835 for a discussion.

2013-11-13-relations.agda

module 2013-11-13-relations where

open import Level hiding (zero;suc)
open import Function
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open import Data.Empty
open import Data.Product using (∃)
open import Induction.WellFounded

--------------------------------------------------------------------------------
-- Utility
--------------------------------------------------------------------------------

Rel₀ : Set → Set₁
Rel₀ A = Rel A Level.zero

Arrow : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
Arrow A B = A → B

Any : ∀ {a b r} {A : Set a} {B : Set b} → (A → Rel B r) → Rel B _
Any r u v = ∃ \x → r x u v

--------------------------------------------------------------------------------
-- Transitive closure
--------------------------------------------------------------------------------

module Star where
  open import Data.Star public renaming (map to map'; fold to foldr)
  
  map : ∀ {i j t u} {I : Set i} {T : Rel I t} {J : Set j} {U : Rel J u} →
        {f : I → J} → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
  map g xs = gmap _ g xs

  concatMap : ∀ {i j t u}
                {I : Set i} {J : Set j} {T : Rel I t} {U : Rel J u}
                {f : I → J} → T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
  concatMap g xs = kleisliStar _ g xs

  foldMap : ∀ {i j t p} {I : Set i} {J : Set j} {T : Rel I t}
          {f : I → J} (P : Rel J p) →
          Transitive P → Reflexive P → T =[ f ]⇒ P → Star T =[ f ]⇒ P
  foldMap {f = f} P t r g = gfold f P (\a b → t (g a) b) r

  fold : ∀ {a r} {A : Set a} {R : Rel A r} → {f : A → Set} → (R =[ f ]⇒ Arrow) → (Star R =[ f ]⇒ Arrow)
  --fold {f = f} g = Data.Star.gfold f Arrow (\a b → b ∘ g a) id
  fold {f = f} g = foldMap {f = f} Arrow (\f g x → g (f x)) id g

  zip : ∀ {la lb lc r s t} {A : Set la} {B : Set lb} {C : Set lc} {R : Rel A r} {S : Rel B s} {T : Rel C t}
      → {f : A → B → C}
      → Reflexive R
      → Reflexive S
      → (∀ {a b c d} → R a b → S c d → T (f a c) (f b d))
      → ∀ {a b c d} → Star R a b → Star S c d → Star T (f a c) (f b d)
  zip reflR reflS g xs ys = map (\x → g x reflS) xs ◅◅ map (\y → g reflR y) ys

open Star public using (Star;_◅_;_◅◅_;ε;_⋆)

--------------------------------------------------------------------------------
-- Non-Reflexive Transitive closure
--------------------------------------------------------------------------------

module Plus where
  data Plus {l r} {A : Set l} (R : Rel A r) (a : A) (c : A) : Set (l ⊔ r) where
    _◅_ : ∀ {b} → R a b → Star R b c → Plus R a c

  plus-acc : ∀ {l} {A : Set l} {R : Rel A l} {x} → Acc (flip R) x → Acc (flip (Plus R)) x
  plus-acc' : ∀ {l} {A : Set l} {R : Rel A l} {x y} → Acc (flip R) x → Plus R x y → Acc (flip (Plus R)) y
  star-acc' : ∀ {l} {A : Set l} {R : Rel A l} {x y} → Acc (flip R) x → Star R x y → Acc (flip (Plus R)) y
  plus-acc a = acc (\_ → plus-acc' a)
  plus-acc' (acc a) (ab ◅ bc) = star-acc' (a _ ab) bc
  star-acc' a ε = plus-acc a
  star-acc' (acc a) (ab ◅ bc) = star-acc' (a _ ab) bc
  
  well-founded : ∀ {l} {A : Set l} {R : Rel A l} → Well-founded (flip R) → Well-founded (flip (Plus R))
  well-founded wf = plus-acc ∘ wf

open Plus public using (Plus;_◅_)

--------------------------------------------------------------------------------
-- Reflexive closure
--------------------------------------------------------------------------------

-- reflexive closure
module Refl where
  data Refl {l r} {A : Set l} (R : Rel A r) (a : A) : A → Set (l ⊔ r) where
    ε : Refl R a a
    _◅ε : ∀ {b} → R a b → Refl R a b

  _?◅_ : ∀ {l r} {A : Set l} {R : Rel A r} {x y z : A} → Refl R x y → Star R y z → Star R x z
  ε ?◅ yz = yz
  xy ◅ε ?◅ yz = xy ◅ yz

  map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
      → {f : A → B}
      → (∀ {a b} → R a b → S (f a) (f b))
      → ∀ {a b} → Refl R a b → Refl S (f a) (f b)
  map g ε = ε
  map g (x ◅ε) = g x ◅ε

  fromRefl : ∀ {a A r} {R : Rel {a} A r} → Reflexive R → Refl R ⇒ R
  fromRefl refl ε = refl
  fromRefl refl (x ◅ε) = x

open Refl public hiding (module Refl;map)

--------------------------------------------------------------------------------
-- Symmetric closure
--------------------------------------------------------------------------------

module Sym where
  data CoSym {l r s} {A : Set l} (R : Rel A r) (S : Rel A s) (a : A) : A → Set (l ⊔ r ⊔ s) where
    fwd : ∀ {b} → R a b → CoSym R S a b
    bwd : ∀ {b} → S b a → CoSym R S a b
  
  Sym : ∀ {l r} {A : Set l} (R : Rel A r) (a : A) → A → Set (l ⊔ r)
  Sym R = CoSym R R

  sym : ∀ {l r} {A : Set l} {R : Rel A r} {a b : A} → Sym R a b → Sym R b a
  sym (fwd x) = bwd x
  sym (bwd x) = fwd x
  
  map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
      → {f : A → B}
      → (∀ {a b} → R a b → S (f a) (f b))
      → ∀ {a b} → Sym R a b → Sym S (f a) (f b)
  map g (fwd x) = fwd (g x)
  map g (bwd x) = bwd (g x)

open Sym public hiding (map;sym)

--------------------------------------------------------------------------------
-- Symmetric-transitive closure
--------------------------------------------------------------------------------

module StarSym where
  StarSym : ∀ {l r} {A : Set l} (R : Rel A r) → Rel A (l ⊔ r)
  StarSym R = Star (Sym R)

  map : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
      → {f : A → B}
      → (∀ {a b} → R a b → S (f a) (f b))
      → ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
  map g = Star.map (Sym.map g)

  zip : ∀ {la lb lc r s t} {A : Set la} {B : Set lb} {C : Set lc} {R : Rel A r} {S : Rel B s} {T : Rel C t}
      → {f : A → B → C}
      → Reflexive R
      → Reflexive S
      → (∀ {a b c d} → R a b → S c d → T (f a c) (f b d))
      → ∀ {a b c d} → StarSym R a b → StarSym S c d → StarSym T (f a c) (f b d)
  zip reflR reflS g xs ys = map (\x → g x reflS) xs ◅◅ map (\y → g reflR y) ys

  sym :  ∀ {l r A R} → StarSym {l} {r} {A} R ⇒ flip (StarSym R)
  sym = Star.reverse Sym.sym

  into :  ∀ {l r A R} → Sym (Star R) ⇒ StarSym {l} {r} {A} R
  into (fwd xs) = Star.map     fwd xs
  into (bwd xs) = Star.reverse bwd xs

  symInto :  ∀ {l r A R} → Sym (StarSym R) ⇒ StarSym {l} {r} {A} R
  symInto (fwd xs) = xs
  symInto (bwd xs) = sym xs

  concat : ∀ {l r A R} → StarSym (StarSym {l} {r} {A} R) ⇒ StarSym R
  concat = Star.concat ∘ Star.map symInto

  concatMap : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
            → {f : A → B}
            → (∀ {a b} → R a b → StarSym S (f a) (f b))
            → ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
  concatMap g = Star.concat ∘ Star.map (symInto ∘ Sym.map g)

  concatMap' : ∀ {la lb r s} {A : Set la} {B : Set lb} {R : Rel A r} {S : Rel B s}
             → {f : A → B}
             → (∀ {a b} → R a b → Star S (f a) (f b))
             → ∀ {a b} → StarSym R a b → StarSym S (f a) (f b)
  concatMap' g = Star.concat ∘ Star.map (into ∘ Sym.map g)

open StarSym public using (StarSym)

--------------------------------------------------------------------------------------------------
-- Relations
--------------------------------------------------------------------------------------------------

module Relations where
  -- Here are some lemmas about confluence
  -- First the generic stuff
  infix 3 _||_
  record CommonReduct' {la lb lc r s} {A : Set la} {B : Set lb} {C : Set lc}
                       (R : REL A C r) (S : REL B C s)
                       (a : A) (b : B) : Set (la ⊔ lb ⊔ lc ⊔ r ⊔ s) where
    constructor _||_
    field {c} : C
    field reduce₁ : R a c
    field reduce₂ : S b c

  module CommonReduct where
    CommonReduct : ∀ {a r} {A : Set a} (R : Rel A r) → Rel A (a ⊔ r)
    CommonReduct R = CommonReduct' R R
    
    maps : ∀ {a b c d e f r s t u} {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e} {F : Set f}
              {R : REL A C r} {S : REL B C s} {T : REL D F t} {U : REL E F u}
              {f : A → D} {g : B → E} {h : C → F}
         → (∀ {u v} → R u v → T (f u) (h v))
         → (∀ {u v} → S u v → U (g u) (h v))
         → (∀ {u v} → CommonReduct' R S u v → CommonReduct' T U (f u) (g v))
    maps f g (u || v) = f u || g v
    
    map : ∀ {a b r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
        → {f : A → B}
        → (R =[ f ]⇒ S) → (CommonReduct R =[ f ]⇒ CommonReduct S)
    map g (u || v) = g u || g v
  
    zips : ∀ {a b c d e f g h i r s t u v w}
              {A : Set a} {B : Set b} {C : Set c} {D : Set d} {E : Set e} {F : Set f} {G : Set g} {H : Set h} {I : Set i}
              {R : REL A C r} {S : REL B C s} {T : REL D F t} {U : REL E F u} {V : REL G I v} {W : REL H I w}
              {f : A → D → G} {g : B → E → H} {h : C → F → I}
         → (∀ {x y u v} → R x y → T u v → V (f x u) (h y v))
         → (∀ {x y u v} → S x y → U u v → W (g x u) (h y v))
         → (∀ {x y u v} → CommonReduct' R S x y → CommonReduct' T U u v → CommonReduct' V W (f x u) (g y v))
    zips f g (x || y) (u || v) = f x u || g y v
    
    zip : ∀ {a b c r s t} {A : Set a} {B : Set b} {C : Set c} {R : Rel A r} {S : Rel B s} {T : Rel C t}
        → {f : A → B → C}
        → (f Preserves₂ R ⟶ S ⟶ T)
        → (f Preserves₂ CommonReduct R ⟶ CommonReduct S ⟶ CommonReduct T)
    zip f (ac || bc) (df || ef) = f ac df || f bc ef

    swap : ∀ {a r} {A : Set a} {R S : Rel A r}
         → ∀ {x y} → CommonReduct' R S x y → CommonReduct' S R y x
    swap (u || v) = v || u

  open CommonReduct public using (CommonReduct)
  module CR = CommonReduct
  
  
  GenConfluent : ∀ {a r s t u} {A : Set a} (R : Rel A r) (S : Rel A s) (T : Rel A t) (U : Rel A u)
               → Set (a ⊔ r ⊔ s ⊔ t ⊔ u)
  GenConfluent R S T U = ∀ {a b c} → R a b → S a c → CommonReduct' T U b c
  
  -- With two relations
  CoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  CoConfluent R S = GenConfluent R S S R
  
  SemiCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  SemiCoConfluent R S = GenConfluent R (Star S) (Star S) (Star R)
  
  HalfCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  HalfCoConfluent R S = GenConfluent R S (Star S) R
  
  StrongCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  StrongCoConfluent R S = GenConfluent R (Star S) (Star S) (Refl R)
  
  StrongerCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  StrongerCoConfluent R S = GenConfluent R (Star S) (Star S) R
  
  ReflCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  ReflCoConfluent R S = GenConfluent R S (Refl S) (Refl R)
  
  GlobalCoConfluent : ∀ {a r s} {A : Set a} (R : Rel A r) (S : Rel A s) → Set (a ⊔ r ⊔ s)
  GlobalCoConfluent R S = CoConfluent (Star R) (Star S)
  
  -- Now with a single relation
  Confluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  Confluent R = GenConfluent R R R R
  
  LocalConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  LocalConfluent R = GenConfluent R R (Star R) (Star R)
  
  ReflConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  ReflConfluent R = GenConfluent R R (Refl R) (Refl R)
  
  SemiConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  SemiConfluent R = GenConfluent R (Star R) (Star R) (Star R)
  
  GlobalConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  GlobalConfluent R = Confluent (Star R)
  
  --StrongConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  --StrongConfluent R = GenConfluent R R (Star R) (MaybeRel R)
  
  -- semi confluence implies confluence for R*
  SemiConfluent-to-GlobalConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → SemiCoConfluent R S → GlobalCoConfluent R S
  SemiConfluent-to-GlobalConfluent conf ε ab = ab || ε
  SemiConfluent-to-GlobalConfluent conf ab ε = ε || ab
  SemiConfluent-to-GlobalConfluent conf (ab ◅ bc) ad with conf ab ad
  ... | be || de with SemiConfluent-to-GlobalConfluent conf bc be
  ...   | cf || ef = cf || (de ◅◅ ef)

  Confluent-to-StrongConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → StrongCoConfluent R S
  Confluent-to-StrongConfluent conf ab ε = ε || (ab ◅ε)
  Confluent-to-StrongConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ce with Confluent-to-StrongConfluent conf ce cd
  ...   | ef || df = be ◅ ef || df

  Confluent-to-StrongerConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → StrongerCoConfluent R S
  Confluent-to-StrongerConfluent conf ab ε = ε || ab
  Confluent-to-StrongerConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ce with Confluent-to-StrongerConfluent conf ce cd
  ...   | ef || df = be ◅ ef || df

  HalfConfluent-to-StrongerConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → HalfCoConfluent R S → StrongerCoConfluent R S
  HalfConfluent-to-StrongerConfluent conf ab ε = ε || ab
  HalfConfluent-to-StrongerConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ce with HalfConfluent-to-StrongerConfluent conf ce cd
  ...   | ef || df = be ◅◅ ef || df

  -- note: could be weakened to require StrongConfluent
  Confluent-to-SemiConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → SemiCoConfluent R S
  Confluent-to-SemiConfluent conf ab ε = ε || (ab ◅ ε)
  Confluent-to-SemiConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ce with Confluent-to-SemiConfluent conf ce cd
  ...   | ef || df = be ◅ ef || df
  
  ReflConfluent-to-SemiConfluent : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → ReflCoConfluent R S → SemiCoConfluent R S
  ReflConfluent-to-SemiConfluent conf ab ε = ε || (ab ◅ ε)
  ReflConfluent-to-SemiConfluent conf ab (ac ◅ cd) with conf ab ac
  ... | be || ε = be ?◅ cd || ε
  ... | be || ce ◅ε with ReflConfluent-to-SemiConfluent conf ce cd
  ...   | ef || df = be ?◅ ef || df

  Confluent-Star : ∀ {a r s A} {R : Rel {a} A r} {S : Rel {a} A s} → CoConfluent R S → GlobalCoConfluent R S
  Confluent-Star = SemiConfluent-to-GlobalConfluent ∘ Confluent-to-SemiConfluent
  
  from-StarSym : ∀ {a r A} {R : Rel {a} A r} → GlobalConfluent R → Star (Sym R) ⇒ CommonReduct (Star R)
  from-StarSym conf ε = ε || ε
  from-StarSym conf (fwd ab ◅ bc) with from-StarSym conf bc
  ... | bd || cd = ab ◅ bd || cd
  from-StarSym conf (bwd ba ◅ bc) with from-StarSym conf bc
  ... | bd || cd with conf (ba ◅ ε) bd
  ...   | be || de = be || cd ◅◅ de

  to-StarSym : ∀ {a r A} {R : Rel {a} A r} → CommonReduct (Star R) ⇒ Star (Sym R)
  to-StarSym (xs || ys) = Star.map fwd xs ◅◅ Star.reverse bwd ys

  -- strong normalization + local confluence implies global confluence
  -- we can write SN R as Well-founded (flip R)
  well-founded-confluent : ∀ {a A} {R : Rel {a} A a} → Well-founded (flip R) → LocalConfluent R → GlobalConfluent R
  well-founded-confluent wf conf = acc-confluent conf (Plus.well-founded wf _)
    where
    acc-confluent : ∀ {a A} {R : Rel {a} A a} → LocalConfluent R → ∀ {a b c} → Acc (flip (Plus R)) a → Star R a b → Star R a c → CommonReduct (Star R) b c
    acc-confluent conf _ ε ac = ac || ε
    acc-confluent conf _ ab ε = ε || ab
    acc-confluent conf (acc a) (ab ◅ bc) (ad ◅ de) with conf ab ad
    ... | bf || df with acc-confluent conf (a _ (ab ◅ ε)) bc bf
    ... | cg || fg with acc-confluent conf (a _ (ad ◅ ε)) de df
    ... | eh || fh with acc-confluent conf (a _ (ab ◅ bf)) fg fh
    ... | gi || hi = cg ◅◅ gi || eh ◅◅ hi

  confluent-by : ∀ {a A r s} {R : Rel {a} A r} {S : Rel A s}
               → (S ⇒ R) → (R ⇒ S)
               → Confluent R → Confluent S
  confluent-by toR fromR confR ab ac = CR.map fromR (confR (toR ab) (toR ac))
  
  concatCR : ∀ {a r A} {R : Rel {a} A r} → GlobalConfluent R → StarSym (CommonReduct (Star R)) ⇒ CommonReduct (Star R)
  concatCR conf ε = ε || ε
  concatCR conf (fwd (ad || bd) ◅ bc) with concatCR conf bc
  ... | be || ce with conf bd be
  ... | df || ef = ad ◅◅ df || ce ◅◅ ef
  concatCR conf (bwd (bd || ad) ◅ bc) with concatCR conf bc
  ... | be || ce with conf bd be
  ... | df || ef = ad ◅◅ df || ce ◅◅ ef

open Relations public

--------------------------------------------------------------------------------
-- Empty relation
--------------------------------------------------------------------------------

module Empty {a} {A : Set a} where
  Empty : Rel A Level.zero
  Empty _ _ = ⊥
  confluent : Confluent Empty
  confluent ()
  --gconfluent : GlobalConfluent Empty
  --gconfluent = {!!}

--------------------------------------------------------------------------------
-- Triple common reduction
--------------------------------------------------------------------------------

module CRPlus where
  infix 3 _|[_]|_
  record CommonReductPlus {l r A} (R : Rel {l} A r) a b c : Set (l ⊔ r) where
    constructor _|[_]|_
    field {d} : A
    field reduce₁ : R a d
    field reduce₂ : R b d
    field reduce₃ : R c d
    
    toCR : CommonReduct R a c
    toCR = reduce₁ || reduce₃
    
  --fromCR : {l r A} {R : Rel {l} A r} {a b} → CommonReduct a b → 
  
  ConfluentPlus : ∀ {a r A} (R : Rel {a} A r) → Set (a ⊔ r)
  ConfluentPlus R = ∀ {a b c} → R a b → R a c → CommonReductPlus R b a c
  

2013-12-21-confluence-beta-d.agda

module 2013-12-21-confluence-beta-d where

open import 2013-11-13-relations
open import Function
open import Relation.Binary hiding (Sym)
open import Relation.Binary.PropositionalEquality as PE hiding (subst;sym;trans;refl)
open ≡-Reasoning

--------------------------------------------------------------------------------
-- Lambda calculus
--------------------------------------------------------------------------------

module Var where
  -- The type (Var α) has one more element than the type α
  -- it is isomorphic to Maybe α
  data Var (α : Set) : Set where
    zero : Var α
    suc  : α → Var α
  
  -- Case analysis for Var
  unvar : ∀ {α} {β : Var α → Set}
        → β zero → ((x : α) → β (suc x)) → (x : Var α) → β x
  unvar z _ zero = z
  unvar _ s (suc x) = s x
  
  map : ∀ {α β} → (α → β) → Var α → Var β
  map f = unvar zero (suc ∘ f)

  one : ∀ {α} → Var (Var α)
  one = suc zero
  two : ∀ {α} → Var (Var (Var α))
  two = suc one
  
open Var public hiding (map;module Var)

module Term where
  data Term (A : Set) : Set where
    var : (a : A) → Term A
    lam : (a : Term (Var A)) → Term A
    app : (a : Term A) → (b : Term A) → Term A
    dup : (a : Term A) → (b : Term A) → Term A

  -- T forms a functor
  map : ∀ {A B} → (A → B) → Term A → Term B
  map f (var a) = var (f a)
  map f (lam x) = lam (map (Var.map f) x)
  map f (app x y) = app (map f x) (map f y)
  map f (dup x y) = dup (map f x) (map f y)
  
  map-Term : ∀ {A B} → (A → Term B) → Var A → Term (Var B)
  map-Term f = unvar (var zero) (map suc ∘ f)
  
  -- and a monad
  bind : ∀ {A B} → (A → Term B) → Term A → Term B
  bind f (var a) = f a
  bind f (lam x) = lam (bind (map-Term f) x)
  bind f (app x y) = app (bind f x) (bind f y)
  bind f (dup x y) = dup (bind f x) (bind f y)

  -- we can use the monad for substitution
  subst : ∀ {A} → Term (Var A) → Term A → Term A
  subst a b = bind (unvar b var) a
  
  -- We need these properties later on
  -- these are all just standard functor and monad laws
  module Properties where
    -- properties of map, i.e. the functor laws
    map-cong : ∀ {A B} {f g : A → B} → (f=g : ∀ x → f x ≡ g x) → (x : Term A) → map f x ≡ map g x
    map-cong f=g (var   x) = PE.cong var (f=g x)
    map-cong f=g (lam   x) = PE.cong lam (map-cong (unvar PE.refl (cong suc ∘ f=g)) x)
    map-cong f=g (app x y) = PE.cong₂ app (map-cong f=g x) (map-cong f=g y)
    map-cong f=g (dup x y) = PE.cong₂ dup (map-cong f=g x) (map-cong f=g y)
    
    map-id : ∀ {A} → (x : Term A) → map id x ≡ x
    map-id (var   x) = PE.refl
    map-id (lam   x) = PE.cong lam (map-cong (unvar PE.refl (\_ → PE.refl)) x ⟨ PE.trans ⟩ map-id x)
    map-id (app x y) = PE.cong₂ app (map-id x) (map-id y)
    map-id (dup x y) = PE.cong₂ dup (map-id x) (map-id y)
    
    map-map : ∀ {A B C} (f : B → C) (g : A → B) (x : Term A)
            → map f (map g x) ≡ map (f ∘ g) x
    map-map f g (var   x) = PE.refl
    map-map f g (lam   x) = PE.cong lam (map-map (Var.map f) (Var.map g) x
                          ⟨ PE.trans ⟩ map-cong (unvar PE.refl (\_ → PE.refl)) x)
    map-map f g (app x y) = PE.cong₂ app (map-map f g x) (map-map f g y)
    map-map f g (dup x y) = PE.cong₂ dup (map-map f g x) (map-map f g y)
    
    -- let's also prove some properties of the monad
    bind-cong : ∀ {A B} {f g : A → Term B}
              → (f=g : ∀ x → f x ≡ g x) → (x : Term A) → bind f x ≡ bind g x
    bind-cong f=g (var   x) = f=g x
    bind-cong f=g (lam   x) = PE.cong lam (bind-cong (unvar PE.refl (PE.cong (map suc) ∘ f=g)) x)
    bind-cong f=g (app x y) = PE.cong₂ app (bind-cong f=g x) (bind-cong f=g y)
    bind-cong f=g (dup x y) = PE.cong₂ dup (bind-cong f=g x) (bind-cong f=g y)
    
    bind-map : ∀ {A B} → (f : A → B) → (x : Term A) → bind (var ∘ f) x ≡ map f x
    bind-map f (var   x) = PE.refl
    bind-map f (lam   x) = PE.cong lam (bind-cong (unvar PE.refl (\_ → PE.refl)) x
                         ⟨ PE.trans ⟩ bind-map (Var.map f) x)
    bind-map f (app x y) = PE.cong₂ app (bind-map f x) (bind-map f y)
    bind-map f (dup x y) = PE.cong₂ dup (bind-map f x) (bind-map f y)
    
    bind-map₁ : ∀ {A B C} (f : B → Term C) (g : A → B) (x : Term A)
              → bind f (map g x) ≡ bind (f ∘ g) x
    bind-map₁ f g (var   x) = PE.refl
    bind-map₁ f g (lam   x) = PE.cong lam (bind-map₁ _ _ x
                            ⟨ PE.trans ⟩ bind-cong (unvar PE.refl (\_ → PE.refl)) x)
    bind-map₁ f g (app x y) = PE.cong₂ app (bind-map₁ f g x) (bind-map₁ f g y)
    bind-map₁ f g (dup x y) = PE.cong₂ dup (bind-map₁ f g x) (bind-map₁ f g y)
   
    bind-map₂ : ∀ {A B C} (f : B → C) (g : A → Term B) (x : Term A)
              → bind (map f ∘ g) x ≡ map f (bind g x)
    bind-map₂ f g (var   x) = PE.refl
    bind-map₂ f g (lam   x) = PE.cong lam (bind-cong (unvar PE.refl (lem ∘ g)) x
                         ⟨ PE.trans ⟩ bind-map₂ _ _ x)
      where
      lem : ∀ y → map suc (map f y) ≡ map (Var.map f) (map suc y)
      lem y = map-map _ _ y ⟨ PE.trans ⟩ PE.sym (map-map _ _ y)
    bind-map₂ f g (app x y) = PE.cong₂ app (bind-map₂ f g x) (bind-map₂ f g y)
    bind-map₂ f g (dup x y) = PE.cong₂ dup (bind-map₂ f g x) (bind-map₂ f g y)
    
    bind-bind : ∀ {A B C} (f : B → Term C) (g : A → Term B) (x : Term A)
              → bind f (bind g x) ≡ bind (bind f ∘ g) x
    bind-bind f g (var   x) = PE.refl
    bind-bind f g (lam   x) = PE.cong lam (bind-bind _ _ x
                            ⟨ PE.trans ⟩ bind-cong (unvar PE.refl (lem ∘ g)) x)
      where
      lem : ∀ y → bind (map-Term f) (map suc y) ≡ map suc (bind f y)
      lem y = bind-map₁ _ _ y ⟨ PE.trans ⟩ bind-map₂ _ _ y
    bind-bind f g (app x y) = PE.cong₂ app (bind-bind f g x) (bind-bind f g y) 
    bind-bind f g (dup x y) = PE.cong₂ dup (bind-bind f g x) (bind-bind f g y) 
    
    -- derived properties
    bind-return : ∀ {A} → (x : Term A) → bind var x ≡ x
    bind-return x = bind-map id x ⟨ PE.trans ⟩ map-id x
    
    map-subst : ∀ {A B} (f : A → B) (a : Term (Var A)) (b : Term A)
              → map f (subst a b) ≡ subst (map (Var.map f) a) (map f b)
    map-subst f a b
      = PE.sym (bind-map₂ _ _ a)
      ⟨ PE.trans ⟩ bind-cong (unvar PE.refl \_ → PE.refl) a
      ⟨ PE.trans ⟩ PE.sym (bind-map₁ _ _ a)

    bind-subst : ∀ {A B} (f : A → Term B) (a : Term (Var A)) (b : Term A)
               → bind f (subst a b) ≡ subst (bind (map-Term f) a) (bind f b)
    bind-subst f a b
      = bind-bind _ _ a ⟨ PE.trans ⟩
        bind-cong (unvar PE.refl
                         (\x' → PE.sym (bind-return (f x')) ⟨ PE.trans ⟩
                                PE.sym (bind-map₁ (unvar (bind f b) var) suc (f x')))) a ⟨ PE.trans ⟩
        PE.sym (bind-bind _ _ a)
  open Properties public

open Term public hiding (map;bind;subst;module Term)

--------------------------------------------------------------------------------
-- Reduction
--------------------------------------------------------------------------------

data Beta {A} : Rel₀ (Term A) where
  beta : ∀ {a b} → Beta (app (lam a) b) (Term.subst a b)
  dup₁ : ∀ {a b} → StarSym Beta a b → Beta (dup a b) a
  dup₂ : ∀ {a b} → StarSym Beta a b → Beta (dup a b) b
  under-lam : ∀ {a a'} → Beta a a' → Beta (lam a) (lam a')
  under-app₁ : ∀ {a a' b} → Beta a a' → Beta (app a b) (app a' b)
  under-app₂ : ∀ {a b b'} → Beta b b' → Beta (app a b) (app a b')
  under-dup₁ : ∀ {a a' b} → Beta a a' → Beta (dup a b) (dup a' b)
  under-dup₂ : ∀ {a b b'} → Beta b b' → Beta (dup a b) (dup a b')

-- we want to prove confluence of Beta

--------------------------------------------------------------------------------
-- Simple dup rule
--------------------------------------------------------------------------------

data IStep {A} : Rel₀ (Term A) where
  beta : ∀ {a b} → IStep (app (lam a) b) (Term.subst a b)
  dup : ∀ {a} → IStep (dup a a) a
  under-lam : ∀ {a a'} → IStep a a' → IStep (lam a) (lam a')
  under-app : ∀ {a a' b b'} → IStep a a' → IStep b b' → IStep (app a b) (app a' b')
  under-dup : ∀ {a a' b b'} → IStep a a' → IStep b b' → IStep (dup a b) (dup a' b')
  under-var : ∀ {a} → IStep (var a) (var a)

irefl : ∀ {A} → Reflexive (IStep {A})
irefl {A} {var a} = under-var
irefl {A} {lam x} = under-lam irefl
irefl {A} {app x y} = under-app irefl irefl
irefl {A} {dup x y} = under-dup irefl irefl

-- isteps are preserved under map,bind,subst
map-istep : ∀ {A B} → (f : A → B) → IStep =[ Term.map f ]⇒ IStep
map-istep f (beta {a} {b}) rewrite map-subst f a b = beta
map-istep f dup = dup
map-istep f (under-lam x) = under-lam (map-istep _ x)
map-istep f (under-app x y) = under-app (map-istep f x) (map-istep f y)
map-istep f (under-dup x y) = under-dup (map-istep f x) (map-istep f y)
map-istep f under-var = under-var

bind-istep : ∀ {A B} (f : A → Term B) → IStep =[ Term.bind f ]⇒ IStep
bind-istep f (beta {a} {b}) rewrite bind-subst f a b = beta
bind-istep f dup = dup
bind-istep f (under-lam x) = under-lam (bind-istep _ x)
bind-istep f (under-app x y) = under-app (bind-istep f x) (bind-istep f y)
bind-istep f (under-dup x y) = under-dup (bind-istep f x) (bind-istep f y)
bind-istep f under-var = irefl

-- conversion
beta-to-isteps : ∀ {A} → Beta {A} ⇒ StarSym IStep
betas-to-isteps : ∀ {A} → StarSym (Beta {A}) ⇒ StarSym IStep
beta-to-isteps beta = fwd beta ◅ ε
beta-to-isteps (dup₁ x) = StarSym.map (\u → under-dup irefl u) (StarSym.sym $ betas-to-isteps x) ◅◅ fwd dup ◅ ε
beta-to-isteps (dup₂ x) = StarSym.map (\u → under-dup u irefl) (betas-to-isteps x) ◅◅ fwd dup ◅ ε
beta-to-isteps (under-lam x) = StarSym.map under-lam (beta-to-isteps x)
beta-to-isteps (under-app₁ x) = StarSym.map (\u → under-app u irefl) (beta-to-isteps x)
beta-to-isteps (under-app₂ x) = StarSym.map (\u → under-app irefl u) (beta-to-isteps x)
beta-to-isteps (under-dup₁ x) = StarSym.map (\u → under-dup u irefl) (beta-to-isteps x)
beta-to-isteps (under-dup₂ x) = StarSym.map (\u → under-dup irefl u) (beta-to-isteps x)
betas-to-isteps ε = ε
betas-to-isteps (fwd x ◅ xs) = beta-to-isteps x ◅◅ betas-to-isteps xs
betas-to-isteps (bwd x ◅ xs) = StarSym.sym (beta-to-isteps x) ◅◅ betas-to-isteps xs

istep-to-betas : ∀ {A} → IStep {A} ⇒ StarSym Beta
istep-to-betas beta = fwd beta ◅ ε
istep-to-betas dup = fwd (dup₁ ε) ◅ ε
istep-to-betas (under-lam x) = StarSym.map under-lam (istep-to-betas x)
istep-to-betas (under-app x y) = StarSym.map under-app₁ (istep-to-betas x) ◅◅
                                 StarSym.map under-app₂ (istep-to-betas y)
istep-to-betas (under-dup x y) = StarSym.map under-dup₁ (istep-to-betas x) ◅◅
                                 StarSym.map under-dup₂ (istep-to-betas y)
istep-to-betas under-var = ε

--------------------------------------------------------------------------------
-- Step: parallel beta reduction, and dup reduction guarded by IStep
--------------------------------------------------------------------------------

data Step {A} : Rel₀ (Term A) where
  beta : ∀ {a a' b b'} → Step a a' → Step b b' → Step (app (lam a) b) (Term.subst a' b')
  dup₁ : ∀ {a a' b} → StarSym IStep a b → Step a a' → Step (dup a b) a'
  under-lam : ∀ {a a'} → Step a a' → Step (lam a) (lam a')
  under-app : ∀ {a a' b b'} → Step a a' → Step b b' → Step (app a b) (app a' b')
  under-dup : ∀ {a a' b b'} → Step a a' → Step b b' → Step (dup a b) (dup a' b')
  under-var : ∀ {a} → Step (var a) (var a)

srefl : ∀ {A} → Reflexive (Step {A})
srefl {A} {var a} = under-var
srefl {A} {lam x} = under-lam srefl
srefl {A} {app x y} = under-app srefl srefl
srefl {A} {dup x y} = under-dup srefl srefl

-- conversion
istep-to-step : ∀ {A} → IStep {A} ⇒ Step
istep-to-step beta = beta srefl srefl
istep-to-step dup = dup₁ ε srefl
istep-to-step (under-lam x) = under-lam (istep-to-step x)
istep-to-step (under-app x y) = under-app (istep-to-step x) (istep-to-step y)
istep-to-step (under-dup x y) = under-dup (istep-to-step x) (istep-to-step y)
istep-to-step under-var = srefl

step-to-betas : ∀ {A} → Step {A} ⇒ Star Beta
step-to-betas (beta x y) = Star.map (under-app₁ ∘ under-lam) (step-to-betas x) ◅◅
                           Star.map under-app₂ (step-to-betas y) ◅◅ beta ◅ ε
step-to-betas (dup₁ x y) = dup₁ (StarSym.concatMap istep-to-betas x) ◅ step-to-betas y ◅◅ ε
step-to-betas (under-lam x) = Star.map under-lam (step-to-betas x)
step-to-betas (under-app x y) = Star.map under-app₁ (step-to-betas x) ◅◅ Star.map under-app₂ (step-to-betas y)
step-to-betas (under-dup x y) = Star.map under-dup₁ (step-to-betas x) ◅◅ Star.map under-dup₂ (step-to-betas y)
step-to-betas under-var = ε

step-to-isteps : ∀ {A} → Step {A} ⇒ StarSym IStep
step-to-isteps = Star.concatMap beta-to-isteps ∘ step-to-betas

-- steps are preserved under map,bind,subst
map-step : ∀ {A B} → (f : A → B) → Step =[ Term.map f ]⇒ Step
map-step f (beta {a' = a'} {b' = b'} x y) rewrite map-subst f a' b' = beta (map-step _ x) (map-step f y)
map-step f (dup₁ x y) = dup₁ (StarSym.map (map-istep f) x) (map-step f y)
map-step f (under-lam x) = under-lam (map-step _ x)
map-step f (under-app x y) = under-app (map-step f x) (map-step f y)
map-step f (under-dup x y) = under-dup (map-step f x) (map-step f y)
map-step f under-var = under-var

bind-step : ∀ {A B} {f g : A → Term B} (fg : ∀ x → Step (f x) (g x))
           → ∀ {x y} → Step x y → Step (Term.bind f x) (Term.bind g y)
bind-step {g = g} fg (beta {a' = a'} {b' = b'} x y) rewrite bind-subst g a' b' =
  beta (bind-step (unvar srefl (map-step suc ∘ fg)) x) (bind-step fg y)
bind-step fg (dup₁ x y) = dup₁ (StarSym.map (bind-istep _) x) (bind-step fg y)
bind-step fg (under-lam x) = under-lam (bind-step (unvar srefl (map-step suc ∘ fg)) x)
bind-step fg (under-app x y) = under-app (bind-step fg x) (bind-step fg y)
bind-step fg (under-dup x y) = under-dup (bind-step fg x) (bind-step fg y)
bind-step fg under-var = fg _

subst-step : ∀ {A a a' b b'} → Step a a' → Step {A} b b' → Step (Term.subst a b) (Term.subst a' b')
subst-step aa bb = bind-step (unvar bb \_ → srefl) aa

-- confluence
sconfluent : ∀ {A} → Confluent (Step {A})
sconfluent under-var under-var = under-var || under-var
sconfluent (beta x y) (beta u v) = CR.zip subst-step (sconfluent x u) (sconfluent y v)
sconfluent (beta x y) (under-app (under-lam u) v) = CR.zips subst-step beta (sconfluent x u) (sconfluent y v)
sconfluent (under-app (under-lam x) y) (beta u v) = CR.zips beta subst-step (sconfluent x u) (sconfluent y v)
sconfluent (dup₁ x y) (dup₁ u v) = sconfluent y v
sconfluent (dup₁ x y) (under-dup u v) with sconfluent y u
... | y' || u' = y' || dup₁ (StarSym.sym (step-to-isteps u) ◅◅ x ◅◅ step-to-isteps v) u'
sconfluent (under-dup u v) (dup₁ x y) with sconfluent y u
... | y' || u' = dup₁ (StarSym.sym (step-to-isteps u) ◅◅ x ◅◅ step-to-isteps v) u' || y'
sconfluent (under-lam x) (under-lam u) = CR.map under-lam (sconfluent x u)
sconfluent (under-app x y) (under-app u v) = CR.zip under-app (sconfluent x u) (sconfluent y v)
sconfluent (under-dup x y) (under-dup u v) = CR.zip under-dup (sconfluent x u) (sconfluent y v)

isteps-to-steps : ∀ {A} → StarSym (IStep {A}) ⇒ CommonReduct (Star Step)
isteps-to-steps = from-StarSym (Confluent-Star sconfluent) ∘ StarSym.map istep-to-step

betas-to-steps : ∀ {A} → Star (Beta {A}) ⇒ CommonReduct (Star Step)
betas-to-steps = isteps-to-steps ∘ Star.concatMap beta-to-isteps

--------------------------------------------------------------------------------
-- Combined, we get confluence for beta+D
--------------------------------------------------------------------------------

beta-confluent : ∀ {A} → GlobalConfluent (Beta {A})
beta-confluent ab ac with betas-to-steps ab | betas-to-steps ac
... | ad || bd | ae || ce with Confluent-Star sconfluent ad ae
... | df || ef = Star.concatMap step-to-betas (bd ◅◅ df) || Star.concatMap step-to-betas (ce ◅◅ ef)

I found the following counter-example to eta-contraction of pairs:
http://www.seas.upenn.edu/~sweirich/types/archive/1991/msg00014.html