twanvl · October 23, 2013 10:07
diff --git a/2013-10-23-lambda.agda b/2013-10-23-lambda.agda
 -- Formalization of untyped lambda calculus
 module 2013-10-23-lambda where

 open import Level hiding (zero;suc)
 open import Function using (_∘_;id;_⟨_⟩_)
 open import Data.Empty
 open import Data.Star as Star using (Star;_◅_;_◅◅_;ε;_⋆)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality hiding (subst)
 open import Data.Product as P hiding (map;zip)
 open import Data.Nat using (ℕ;suc)
 open import Relation.Nullary
 open ≡-Reasoning

 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
  infixl 6 _$_
  -- The type of untyped lambda terms with free variables α
  data T (α : Set) : Set where
    -- a term can be a variable
    V : α → T α
    -- or an application
    _$_ : (x : T α) → (y : T α) → T α
    -- or an abstraction of a term with one more free variable
    Λ : T (Var α) → T α
  
  -- T forms a functor
  map : ∀ {α β} → (α → β) → T α → T β
  map f (V x) = V (f x)
  map f (x $ y) = map f x $ map f y
  map f (Λ x) = Λ (map (Var.map f) x)
  
  map-T : ∀ {α β} → (α → T β) → Var α → T (Var β)
  map-T f = unvar (V zero) (map suc ∘ f)
  
  -- and a monad
  bind : ∀ {α β} → (α → T β) → T α → T β
  bind f (V x) = f x
  bind f (x $ y) = bind f x $ bind f y
  bind f (Λ x) = Λ (bind (map-T f) x)
  
  -- note: we can't define the monad in terms of join directly,
  -- because the termination checker doesn't know that map preserves the size of the argument
  join : ∀ {α} → T (T α) → T α
  join = bind id
  
  -- we can use the monad for substitution
  subst : ∀ {α} → T α → T (Var α) → T α
  subst x = bind (unvar x V)
  
  -- 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 : ∀ {α β} {f g : α → β} → (f=g : ∀ x → f x ≡ g x) → (x : T α) → map f x ≡ map g x
    map-cong f=g (V x) = cong V (f=g x)
    map-cong f=g (x $ y) = cong₂ _$_ (map-cong f=g x) (map-cong f=g y)
    map-cong f=g (Λ x) = cong Λ (map-cong (unvar refl (cong suc ∘ f=g)) x)
    
    map-id : ∀ {α} → (x : T α) → map id x ≡ x
    map-id (V x) = refl
    map-id (x $ y) = cong₂ _$_ (map-id x) (map-id y)
    map-id (Λ x) = cong Λ (map-cong (unvar refl (\_ → refl)) x ⟨ trans ⟩ map-id x)
    
    map-map : ∀ {α β γ} (f : β → γ) (g : α → β) (x : T α)
            → map f (map g x) ≡ map (f ∘ g) x
    map-map f g (V x) = refl
    map-map f g (x $ y) = cong₂ _$_ (map-map f g x) (map-map f g y)
    map-map f g (Λ x) = cong Λ (map-map (Var.map f) (Var.map g) x
                      ⟨ trans ⟩ map-cong (unvar refl (\_ → refl)) x)
    
    -- let's also prove some properties of the monad
    bind-cong : ∀ {α β} {f g : α → T β}
              → (f=g : ∀ x → f x ≡ g x) → (x : T α) → bind f x ≡ bind g x
    bind-cong f=g (V x) = f=g x
    bind-cong f=g (x $ y) = cong₂ _$_ (bind-cong f=g x) (bind-cong f=g y)
    bind-cong f=g (Λ x) = cong Λ (bind-cong (unvar refl (cong (map suc) ∘ f=g)) x)
    
    bind-map : ∀ {α β} → (f : α → β)→ (x : T α) → bind (V ∘ f) x ≡ map f x
    bind-map f (V x) = refl
    bind-map f (x $ y) = cong₂ _$_ (bind-map f x) (bind-map f y)
    bind-map f (Λ x) = cong Λ (bind-cong (unvar refl (\_ → refl)) x
                      ⟨ trans ⟩ bind-map (Var.map f) x)
    
    bind-map₁ : ∀ {α β γ} (f : β → T γ) (g : α → β) (x : T α)
              → bind f (map g x) ≡ bind (f ∘ g) x
    bind-map₁ f g (V x) = refl
    bind-map₁ f g (x $ y) = cong₂ _$_ (bind-map₁ f g x) (bind-map₁ f g y)
    bind-map₁ f g (Λ x) = cong Λ (bind-map₁ _ _ x
                         ⟨ trans ⟩ bind-cong (unvar refl (\_ → refl)) x)
    
    bind-map₂ : ∀ {α β γ} (f : β → γ) (g : α → T β) (x : T α)
              → bind (map f ∘ g) x ≡ map f (bind g x)
    bind-map₂ f g (V x) = refl
    bind-map₂ f g (x $ y) = cong₂ _$_ (bind-map₂ f g x) (bind-map₂ f g y)
    bind-map₂ f g (Λ x) = cong Λ (bind-cong (unvar refl (lem ∘ g)) x
                         ⟨ trans ⟩ bind-map₂ _ _ x)
      where
      lem : ∀ y → map suc (map f y) ≡ map (Var.map f) (map suc y)
      lem y = map-map _ _ y ⟨ trans ⟩ sym (map-map _ _ y)
    
    bind-bind : ∀ {α β γ} (f : β → T γ) (g : α → T β) (x : T α)
              → bind f (bind g x) ≡ bind (bind f ∘ g) x
    bind-bind f g (V x) = refl
    bind-bind f g (x $ y) = cong₂ _$_ (bind-bind f g x) (bind-bind f g y) 
    bind-bind f g (Λ x) = cong Λ (bind-bind _ _ x
                         ⟨ trans ⟩ bind-cong (unvar refl (lem ∘ g)) x)
      where
      lem : ∀ y → bind (map-T f) (map suc y) ≡ map suc (bind f y)
      lem y = bind-map₁ _ _ y ⟨ trans ⟩ bind-map₂ _ _ y
    
    -- derived properties
    bind-return : ∀ {α} → (x : T α) → bind V x ≡ x
    bind-return x = bind-map id x ⟨ trans ⟩ map-id x
    
    -- derived properties
    map-subst : ∀ {α β} (f : α → β) (x : T α) (y : T (Var α))
              → map f (subst x y) ≡ subst (map f x) (map (Var.map f) y)
    map-subst f x y
      = sym (bind-map₂ _ _ y)
      ⟨ trans ⟩ bind-cong (unvar refl (\_ → refl)) y
      ⟨ trans ⟩ sym (bind-map₁ _ _ y)

    bind-subst : ∀ {α β} (f : α → T β) (x : T α) (y : T (Var α))
              → bind f (subst x y) ≡ subst (bind f x) (bind (map-T f) y)
    bind-subst f x y
      = bind-bind _ _ y ⟨ trans ⟩
        bind-cong (unvar refl (sym ∘ lem)) y ⟨ trans ⟩
        sym (bind-bind _ _ y)
      where
      lem : ∀ y → bind (unvar (bind f x) V) (map suc (f y)) ≡ f y
      lem y = bind-map₁ _ _ (f y) ⟨ trans ⟩ bind-return (f y)

  open Properties public

 open Term hiding (map;bind)

 -- Here are some example terms
 i k s : T ⊥
 i = Λ (V zero)
 k = Λ (Λ (V (suc zero)))
 s = Λ (Λ (Λ (V (suc (suc zero)) $ V zero $ (V (suc zero) $ V zero))))


 -- Beta reduction
 infix 5 _-β→_ _-β*→_
 data _-β→_ {α} : T α → T α → Set where
  $₁_ : ∀ {x x' y} → x -β→ x' → (x $ y) -β→ (x' $ y)
  $₂_ : ∀ {x y y'} → y -β→ y' → (x $ y) -β→ (x $ y')
  Λ : ∀ {x x'} → x -β→ x' → Λ x -β→ Λ x'
  β! : ∀ {x y} → (Λ x $ y) -β→ subst y x

 _-β*→_ : ∀ {α} → T α → T α → Set
 _-β*→_ = Star _-β→_

 -- We can do β-reduction manually
 -- SKK → λK0(K0) → λ0
 lemma₁ : (s $ k $ k) -β*→ i
 lemma₁ = $₁ β! ◅ β! ◅ Λ ($₁ β!) ◅ Λ β! ◅ ε



 -- Beta reduction is decidable
 eval₁ : ∀ {α} → (x : T α) → Dec (∃ (_-β→_ x))
 eval₁ (V x) = no no-V
  where
  no-V : ∀ {α} {x : α} → ¬ ∃ (_-β→_ (V x))
  no-V (_ , ())
 eval₁ (x $ y) = eval-$ x y
  where
  no-$ : ∀ {α x y}
       → ¬ ∃ (_-β→_ {α} x)
       → ¬ ∃ (_-β→_ y)
       → ¬ ∃ (\x' → x ≡ Λ x')
       → ¬ ∃ (_-β→_ (x $ y))
  no-$ nx ny nΛ (._ , $₁ s) = nx (, s)
  no-$ nx ny nΛ (._ , $₂ s) = ny (, s)
  no-$ nx ny nΛ (._ , β!) = nΛ (, refl)
  eval-$ : ∀ {α} x y → Dec (∃ (_-β→_ {α} (x $ y)))
  eval-$ x y with eval₁ x | eval₁ y
  eval-$ x y | _ | yes (y' , s) = yes (x $ y' , $₂ s)
  eval-$ x y | yes (x' , s) | _ = yes (x' $ y , $₁ s)
  eval-$ (Λ x)   _ | no nx | no ny = yes (, β!)
  eval-$ (V _)   _ | no nx | no ny = no (no-$ nx ny \{(_ , ())})
  eval-$ (_ $ _) _ | no nx | no ny = no (no-$ nx ny \{(_ , ())})
 eval₁ (Λ x) with eval₁ x
 ... | yes (x' , s) = yes (Λ x' , Λ s)
 ... | no n = no (no-Λ n)
  where
  no-Λ : ∀ {α x}
       → ¬ ∃ (_-β→_ {Var α} x)
       → ¬ ∃ (_-β→_ (Λ x))
  no-Λ nx (._ , Λ x) = nx (, x)

 -- And we can run β* up to n steps
 eval : ∀ {α} → ℕ → (x : T α) → ∃ (Star _-β→_ x)
 eval 0 x = , ε
 eval (suc n) x with eval₁ x
 ... | yes (x' , s) = , (s ◅ proj₂ (eval n x'))
 ... | no _ = , ε

 -- which makes it much nicer to prove lemma₁
 solve : ∀ {α} {x y : T α} → (n : ℕ) → (proj₁ (eval n x) ≡ y) → x -β*→ y
 solve {x = x} n refl = proj₂ (eval n x)

 lemma₁' : (s $ k $ k) -β*→ i
 lemma₁' = solve 4 refl

 module Relations where
  infix 3 _||_
  -- Here are some lemmas about confluence
  record CommonReduct' {la lb lc r s} {A : Set la} {B : Set lb} {C : Set lc}
                       (R : A → C → Set r) (S : B → C → Set 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

  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
  
  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)
  
  SemiConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  SemiConfluent R = GenConfluent R (Star R) (Star R) (Star R)
  
  --StrongConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
  --StrongConfluent R = GenConfluent R R (Star R) (MaybeRel R)
  
  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 r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
         → {f g h : A → B}
         → (∀ {u v} → R u v → S (f u) (h v))
         → (∀ {u v} → R u v → S (g u) (h v))
         → (∀ {u v} → CommonReduct R u v → CommonReduct S (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
  
    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

  open CommonReduct public using (CommonReduct)
  
  -- semi confluence implies confluence for R*
  SemiConfluent-to-Confluent : ∀ {a r A} {R : Rel {a} A r} → SemiConfluent R → Confluent (Star R)
  SemiConfluent-to-Confluent conf ε ab = ab || ε
  SemiConfluent-to-Confluent conf ab ε = ε || ab
  SemiConfluent-to-Confluent conf (ab ◅ bc) ad with conf ab ad
  ... | be || de with SemiConfluent-to-Confluent conf bc be
  ...   | cf || ef = cf || (de ◅◅ ef)

  -- note: could be weakened to require StrongConfluent
  Confluent-to-SemiConfluent : ∀ {a r A} {R : Rel {a} A r} → Confluent R → SemiConfluent R
  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
  
  Confluent-Star : ∀ {a r A} {R : Rel {a} A r} → Confluent R → Confluent (Star R)
  Confluent-Star = SemiConfluent-to-Confluent ∘ Confluent-to-SemiConfluent
  
 open Relations public

 -- We could prove confluence via parallel reduction
 data Parβ {α} : T α → T α → Set where
  V     : (x : α) → Parβ (V x) (V x)
  _$_   : ∀ {x x' y y'} → Parβ x x' → Parβ y y' → Parβ (x $ y) (x' $ y')
  Λ     : ∀ {x x'} → Parβ x x' → Parβ (Λ x) (Λ x')
  _$_◅β : ∀ {x x' y y'} → Parβ x x' → Parβ y y' → Parβ (Λ x $ y) (subst y' x')

 ε-Par : ∀ {α} {x : T α} → Parβ x x
 ε-Par {α} {V x} = V x
 ε-Par {α} {x $ x₁} = ε-Par $ ε-Par
 ε-Par {α} {Λ x} = Λ ε-Par

 β→Par : ∀ {α} → _-β→_ ⇒ Parβ {α}
 β→Par ($₁ x) = β→Par x $ ε-Par
 β→Par ($₂ x) = ε-Par $ β→Par x
 β→Par (Λ x) = Λ (β→Par x)
 β→Par β! = ε-Par $ ε-Par ◅β

 Par→β : ∀ {α} → Parβ {α} ⇒ _-β*→_
 Par→β (V x) = ε
 Par→β (x $ y) = Star.gmap (\xx → xx $ _) $₁_ (Par→β x)
             ◅◅ Star.gmap (\yy → _ $ yy) $₂_ (Par→β y)
 Par→β (Λ x) = Star.gmap Λ Λ (Par→β x)
 Par→β (x $ y ◅β) = Star.gmap (\yy → _ $ yy) $₂_ (Par→β y)
                 ◅◅ Star.gmap (\xx → Λ xx $ _) ($₁_ ∘ Λ) (Par→β x)
                 ◅◅ _-β→_.β! ◅ ε

 Par*→β : ∀ {α} → Star (Parβ {α}) ⇒ _-β*→_
 Par*→β = Par→β ⋆

 -- Parallel reduction is preserved under map and bind
 map-Par : ∀ {α β x x'}
         → (f : α → β)
         → Parβ x x'
         → Parβ (Term.map f x) (Term.map f x')
 map-Par f (V x) = V (f x)
 map-Par f (x $ y) = map-Par f x $ map-Par f y
 map-Par f (Λ x) = Λ (map-Par (Var.map f) x)
 map-Par f (_$_◅β {u} {u'} {v} {v'} x y) rewrite map-subst f v' u'
  = map-Par (Var.map f) x $ map-Par f y ◅β

 bind-Par : ∀ {α β y y'} {f g : α → T β}
         → (fg : ∀ x → Parβ (f x) (g x))
         → Parβ y y'
         → Parβ {β} (Term.bind f y) (Term.bind g y')
 bind-Par fg (V x) = fg x
 bind-Par fg (x $ y) = bind-Par fg x $ bind-Par fg y
 bind-Par fg (Λ x) = Λ (bind-Par (unvar ε-Par (map-Par suc ∘ fg)) x)
 bind-Par {g = g} fg (_$_◅β {u} {u'} {v} {v'} x y) rewrite bind-subst g v' u'
  = bind-Par (unvar ε-Par (map-Par suc ∘ fg)) x $ bind-Par fg y ◅β

 subst-Par : ∀ {α x y x' y'} → Parβ {α} x x' → Parβ y y' → Parβ (subst x y) (subst x' y')
 subst-Par x y = bind-Par (unvar x V) y

 confluence-Par : ∀ {α} → Confluent (Parβ {α})
 confluence-Par (V .x) (V x) = V x || V x
 confluence-Par (u $ x) (v $ y) = CommonReduct.zip _$_ (confluence-Par u v) (confluence-Par x y)
 confluence-Par (Λ u) (Λ v) = CommonReduct.map Λ (confluence-Par u v)
 confluence-Par (Λ u $ x) (v $ y ◅β) with confluence-Par u v | confluence-Par x y
 ... | uw || vw | xz || yz = uw $ xz ◅β || subst-Par yz vw
 confluence-Par (u $ x ◅β) (Λ v $ y) with confluence-Par u v | confluence-Par x y
 ... | uw || vw | xz || yz = subst-Par xz uw || vw $ yz ◅β
 confluence-Par (u $ x ◅β) (v $ y ◅β) with confluence-Par u v | confluence-Par x y
 ... | uw || vw | xz || yz = subst-Par xz uw || subst-Par yz vw

 confluence-Par* : ∀ {α} → Confluent (Star (Parβ {α}))
 confluence-Par* = Confluent-Star confluence-Par

 -- And now we get confluence for β*
 confluence : ∀ {α} → Confluent (Star (_-β→_ {α}))
 confluence ab ac = CommonReduct.map Par*→β (confluence-Par* (Star.map β→Par ab) (Star.map β→Par ac))
	-- Formalization of untyped lambda calculus
	module 2013-10-23-lambda where

	open import Level hiding (zero;suc)
	open import Function using (_∘_;id;_⟨_⟩_)
	open import Data.Empty
	open import Data.Star as Star using (Star;_◅_;_◅◅_;ε;_⋆)
	open import Relation.Binary
	open import Relation.Binary.PropositionalEquality hiding (subst)
	open import Data.Product as P hiding (map;zip)
	open import Data.Nat using (ℕ;suc)
	open import Relation.Nullary
	open ≡-Reasoning

	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
	infixl 6 _$_
	-- The type of untyped lambda terms with free variables α
	data T (α : Set) : Set where
	-- a term can be a variable
	V : α → T α
	-- or an application
	_$_ : (x : T α) → (y : T α) → T α
	-- or an abstraction of a term with one more free variable
	Λ : T (Var α) → T α

	-- T forms a functor
	map : ∀ {α β} → (α → β) → T α → T β
	map f (V x) = V (f x)
	map f (x $ y) = map f x $ map f y
	map f (Λ x) = Λ (map (Var.map f) x)

	map-T : ∀ {α β} → (α → T β) → Var α → T (Var β)
	map-T f = unvar (V zero) (map suc ∘ f)

	-- and a monad
	bind : ∀ {α β} → (α → T β) → T α → T β
	bind f (V x) = f x
	bind f (x $ y) = bind f x $ bind f y
	bind f (Λ x) = Λ (bind (map-T f) x)

	-- note: we can't define the monad in terms of join directly,
	-- because the termination checker doesn't know that map preserves the size of the argument
	join : ∀ {α} → T (T α) → T α
	join = bind id

	-- we can use the monad for substitution
	subst : ∀ {α} → T α → T (Var α) → T α
	subst x = bind (unvar x V)

	-- 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 : ∀ {α β} {f g : α → β} → (f=g : ∀ x → f x ≡ g x) → (x : T α) → map f x ≡ map g x
	map-cong f=g (V x) = cong V (f=g x)
	map-cong f=g (x $ y) = cong₂ _$_ (map-cong f=g x) (map-cong f=g y)
	map-cong f=g (Λ x) = cong Λ (map-cong (unvar refl (cong suc ∘ f=g)) x)

	map-id : ∀ {α} → (x : T α) → map id x ≡ x
	map-id (V x) = refl
	map-id (x $ y) = cong₂ _$_ (map-id x) (map-id y)
	map-id (Λ x) = cong Λ (map-cong (unvar refl (\_ → refl)) x ⟨ trans ⟩ map-id x)

	map-map : ∀ {α β γ} (f : β → γ) (g : α → β) (x : T α)
	→ map f (map g x) ≡ map (f ∘ g) x
	map-map f g (V x) = refl
	map-map f g (x $ y) = cong₂ _$_ (map-map f g x) (map-map f g y)
	map-map f g (Λ x) = cong Λ (map-map (Var.map f) (Var.map g) x
	⟨ trans ⟩ map-cong (unvar refl (\_ → refl)) x)

	-- let's also prove some properties of the monad
	bind-cong : ∀ {α β} {f g : α → T β}
	→ (f=g : ∀ x → f x ≡ g x) → (x : T α) → bind f x ≡ bind g x
	bind-cong f=g (V x) = f=g x
	bind-cong f=g (x $ y) = cong₂ _$_ (bind-cong f=g x) (bind-cong f=g y)
	bind-cong f=g (Λ x) = cong Λ (bind-cong (unvar refl (cong (map suc) ∘ f=g)) x)

	bind-map : ∀ {α β} → (f : α → β)→ (x : T α) → bind (V ∘ f) x ≡ map f x
	bind-map f (V x) = refl
	bind-map f (x $ y) = cong₂ _$_ (bind-map f x) (bind-map f y)
	bind-map f (Λ x) = cong Λ (bind-cong (unvar refl (\_ → refl)) x
	⟨ trans ⟩ bind-map (Var.map f) x)

	bind-map₁ : ∀ {α β γ} (f : β → T γ) (g : α → β) (x : T α)
	→ bind f (map g x) ≡ bind (f ∘ g) x
	bind-map₁ f g (V x) = refl
	bind-map₁ f g (x $ y) = cong₂ _$_ (bind-map₁ f g x) (bind-map₁ f g y)
	bind-map₁ f g (Λ x) = cong Λ (bind-map₁ _ _ x
	⟨ trans ⟩ bind-cong (unvar refl (\_ → refl)) x)

	bind-map₂ : ∀ {α β γ} (f : β → γ) (g : α → T β) (x : T α)
	→ bind (map f ∘ g) x ≡ map f (bind g x)
	bind-map₂ f g (V x) = refl
	bind-map₂ f g (x $ y) = cong₂ _$_ (bind-map₂ f g x) (bind-map₂ f g y)
	bind-map₂ f g (Λ x) = cong Λ (bind-cong (unvar refl (lem ∘ g)) x
	⟨ trans ⟩ bind-map₂ _ _ x)
	where
	lem : ∀ y → map suc (map f y) ≡ map (Var.map f) (map suc y)
	lem y = map-map _ _ y ⟨ trans ⟩ sym (map-map _ _ y)

	bind-bind : ∀ {α β γ} (f : β → T γ) (g : α → T β) (x : T α)
	→ bind f (bind g x) ≡ bind (bind f ∘ g) x
	bind-bind f g (V x) = refl
	bind-bind f g (x $ y) = cong₂ _$_ (bind-bind f g x) (bind-bind f g y)
	bind-bind f g (Λ x) = cong Λ (bind-bind _ _ x
	⟨ trans ⟩ bind-cong (unvar refl (lem ∘ g)) x)
	where
	lem : ∀ y → bind (map-T f) (map suc y) ≡ map suc (bind f y)
	lem y = bind-map₁ _ _ y ⟨ trans ⟩ bind-map₂ _ _ y

	-- derived properties
	bind-return : ∀ {α} → (x : T α) → bind V x ≡ x
	bind-return x = bind-map id x ⟨ trans ⟩ map-id x

	-- derived properties
	map-subst : ∀ {α β} (f : α → β) (x : T α) (y : T (Var α))
	→ map f (subst x y) ≡ subst (map f x) (map (Var.map f) y)
	map-subst f x y
	= sym (bind-map₂ _ _ y)
	⟨ trans ⟩ bind-cong (unvar refl (\_ → refl)) y
	⟨ trans ⟩ sym (bind-map₁ _ _ y)

	bind-subst : ∀ {α β} (f : α → T β) (x : T α) (y : T (Var α))
	→ bind f (subst x y) ≡ subst (bind f x) (bind (map-T f) y)
	bind-subst f x y
	= bind-bind _ _ y ⟨ trans ⟩
	bind-cong (unvar refl (sym ∘ lem)) y ⟨ trans ⟩
	sym (bind-bind _ _ y)
	where
	lem : ∀ y → bind (unvar (bind f x) V) (map suc (f y)) ≡ f y
	lem y = bind-map₁ _ _ (f y) ⟨ trans ⟩ bind-return (f y)

	open Properties public

	open Term hiding (map;bind)

	-- Here are some example terms
	i k s : T ⊥
	i = Λ (V zero)
	k = Λ (Λ (V (suc zero)))
	s = Λ (Λ (Λ (V (suc (suc zero)) $ V zero $ (V (suc zero) $ V zero))))


	-- Beta reduction
	infix 5 _-β→_ _-β*→_
	data _-β→_ {α} : T α → T α → Set where
	$₁_ : ∀ {x x' y} → x -β→ x' → (x $ y) -β→ (x' $ y)
	$₂_ : ∀ {x y y'} → y -β→ y' → (x $ y) -β→ (x $ y')
	Λ : ∀ {x x'} → x -β→ x' → Λ x -β→ Λ x'
	β! : ∀ {x y} → (Λ x $ y) -β→ subst y x

	_-β*→_ : ∀ {α} → T α → T α → Set
	_-β*→_ = Star _-β→_

	-- We can do β-reduction manually
	-- SKK → λK0(K0) → λ0
	lemma₁ : (s $ k $ k) -β*→ i
	lemma₁ = $₁ β! ◅ β! ◅ Λ ($₁ β!) ◅ Λ β! ◅ ε



	-- Beta reduction is decidable
	eval₁ : ∀ {α} → (x : T α) → Dec (∃ (_-β→_ x))
	eval₁ (V x) = no no-V
	where
	no-V : ∀ {α} {x : α} → ¬ ∃ (_-β→_ (V x))
	no-V (_ , ())
	eval₁ (x $ y) = eval-$ x y
	where
	no-$ : ∀ {α x y}
	→ ¬ ∃ (_-β→_ {α} x)
	→ ¬ ∃ (_-β→_ y)
	→ ¬ ∃ (\x' → x ≡ Λ x')
	→ ¬ ∃ (_-β→_ (x $ y))
	no-$ nx ny nΛ (._ , $₁ s) = nx (, s)
	no-$ nx ny nΛ (._ , $₂ s) = ny (, s)
	no-$ nx ny nΛ (._ , β!) = nΛ (, refl)
	eval-$ : ∀ {α} x y → Dec (∃ (_-β→_ {α} (x $ y)))
	eval-$ x y with eval₁ x \| eval₁ y
	eval-$ x y \| _ \| yes (y' , s) = yes (x $ y' , $₂ s)
	eval-$ x y \| yes (x' , s) \| _ = yes (x' $ y , $₁ s)
	eval-$ (Λ x) _ \| no nx \| no ny = yes (, β!)
	eval-$ (V _) _ \| no nx \| no ny = no (no-$ nx ny \{(_ , ())})
	eval-$ (_ $ _) _ \| no nx \| no ny = no (no-$ nx ny \{(_ , ())})
	eval₁ (Λ x) with eval₁ x
	... \| yes (x' , s) = yes (Λ x' , Λ s)
	... \| no n = no (no-Λ n)
	where
	no-Λ : ∀ {α x}
	→ ¬ ∃ (_-β→_ {Var α} x)
	→ ¬ ∃ (_-β→_ (Λ x))
	no-Λ nx (._ , Λ x) = nx (, x)

	-- And we can run β* up to n steps
	eval : ∀ {α} → ℕ → (x : T α) → ∃ (Star _-β→_ x)
	eval 0 x = , ε
	eval (suc n) x with eval₁ x
	... \| yes (x' , s) = , (s ◅ proj₂ (eval n x'))
	... \| no _ = , ε

	-- which makes it much nicer to prove lemma₁
	solve : ∀ {α} {x y : T α} → (n : ℕ) → (proj₁ (eval n x) ≡ y) → x -β*→ y
	solve {x = x} n refl = proj₂ (eval n x)

	lemma₁' : (s $ k $ k) -β*→ i
	lemma₁' = solve 4 refl

	module Relations where
	infix 3 _\|\|_
	-- Here are some lemmas about confluence
	record CommonReduct' {la lb lc r s} {A : Set la} {B : Set lb} {C : Set lc}
	(R : A → C → Set r) (S : B → C → Set 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

	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

	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)

	SemiConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
	SemiConfluent R = GenConfluent R (Star R) (Star R) (Star R)

	--StrongConfluent : ∀ {a r} {A : Set a} (R : Rel A r) → Set (a ⊔ r)
	--StrongConfluent R = GenConfluent R R (Star R) (MaybeRel R)

	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 r s} {A : Set a} {B : Set b} {R : Rel A r} {S : Rel B s}
	→ {f g h : A → B}
	→ (∀ {u v} → R u v → S (f u) (h v))
	→ (∀ {u v} → R u v → S (g u) (h v))
	→ (∀ {u v} → CommonReduct R u v → CommonReduct S (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

	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

	open CommonReduct public using (CommonReduct)

	-- semi confluence implies confluence for R*
	SemiConfluent-to-Confluent : ∀ {a r A} {R : Rel {a} A r} → SemiConfluent R → Confluent (Star R)
	SemiConfluent-to-Confluent conf ε ab = ab \|\| ε
	SemiConfluent-to-Confluent conf ab ε = ε \|\| ab
	SemiConfluent-to-Confluent conf (ab ◅ bc) ad with conf ab ad
	... \| be \|\| de with SemiConfluent-to-Confluent conf bc be
	... \| cf \|\| ef = cf \|\| (de ◅◅ ef)

	-- note: could be weakened to require StrongConfluent
	Confluent-to-SemiConfluent : ∀ {a r A} {R : Rel {a} A r} → Confluent R → SemiConfluent R
	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

	Confluent-Star : ∀ {a r A} {R : Rel {a} A r} → Confluent R → Confluent (Star R)
	Confluent-Star = SemiConfluent-to-Confluent ∘ Confluent-to-SemiConfluent

	open Relations public

	-- We could prove confluence via parallel reduction
	data Parβ {α} : T α → T α → Set where
	V : (x : α) → Parβ (V x) (V x)
	_$_ : ∀ {x x' y y'} → Parβ x x' → Parβ y y' → Parβ (x $ y) (x' $ y')
	Λ : ∀ {x x'} → Parβ x x' → Parβ (Λ x) (Λ x')
	_$_◅β : ∀ {x x' y y'} → Parβ x x' → Parβ y y' → Parβ (Λ x $ y) (subst y' x')

	ε-Par : ∀ {α} {x : T α} → Parβ x x
	ε-Par {α} {V x} = V x
	ε-Par {α} {x $ x₁} = ε-Par $ ε-Par
	ε-Par {α} {Λ x} = Λ ε-Par

	β→Par : ∀ {α} → _-β→_ ⇒ Parβ {α}
	β→Par ($₁ x) = β→Par x $ ε-Par
	β→Par ($₂ x) = ε-Par $ β→Par x
	β→Par (Λ x) = Λ (β→Par x)
	β→Par β! = ε-Par $ ε-Par ◅β

	Par→β : ∀ {α} → Parβ {α} ⇒ _-β*→_
	Par→β (V x) = ε
	Par→β (x $ y) = Star.gmap (\xx → xx $ _) $₁_ (Par→β x)
	◅◅ Star.gmap (\yy → _ $ yy) $₂_ (Par→β y)
	Par→β (Λ x) = Star.gmap Λ Λ (Par→β x)
	Par→β (x $ y ◅β) = Star.gmap (\yy → _ $ yy) $₂_ (Par→β y)
	◅◅ Star.gmap (\xx → Λ xx $ _) ($₁_ ∘ Λ) (Par→β x)
	◅◅ _-β→_.β! ◅ ε

	Par→β : ∀ {α} → Star (Parβ {α}) ⇒ _-β→_
	Par*→β = Par→β ⋆

	-- Parallel reduction is preserved under map and bind
	map-Par : ∀ {α β x x'}
	→ (f : α → β)
	→ Parβ x x'
	→ Parβ (Term.map f x) (Term.map f x')
	map-Par f (V x) = V (f x)
	map-Par f (x $ y) = map-Par f x $ map-Par f y
	map-Par f (Λ x) = Λ (map-Par (Var.map f) x)
	map-Par f (_$_◅β {u} {u'} {v} {v'} x y) rewrite map-subst f v' u'
	= map-Par (Var.map f) x $ map-Par f y ◅β

	bind-Par : ∀ {α β y y'} {f g : α → T β}
	→ (fg : ∀ x → Parβ (f x) (g x))
	→ Parβ y y'
	→ Parβ {β} (Term.bind f y) (Term.bind g y')
	bind-Par fg (V x) = fg x
	bind-Par fg (x $ y) = bind-Par fg x $ bind-Par fg y
	bind-Par fg (Λ x) = Λ (bind-Par (unvar ε-Par (map-Par suc ∘ fg)) x)
	bind-Par {g = g} fg (_$_◅β {u} {u'} {v} {v'} x y) rewrite bind-subst g v' u'
	= bind-Par (unvar ε-Par (map-Par suc ∘ fg)) x $ bind-Par fg y ◅β

	subst-Par : ∀ {α x y x' y'} → Parβ {α} x x' → Parβ y y' → Parβ (subst x y) (subst x' y')
	subst-Par x y = bind-Par (unvar x V) y

	confluence-Par : ∀ {α} → Confluent (Parβ {α})
	confluence-Par (V .x) (V x) = V x \|\| V x
	confluence-Par (u $ x) (v $ y) = CommonReduct.zip _$_ (confluence-Par u v) (confluence-Par x y)
	confluence-Par (Λ u) (Λ v) = CommonReduct.map Λ (confluence-Par u v)
	confluence-Par (Λ u $ x) (v $ y ◅β) with confluence-Par u v \| confluence-Par x y
	... \| uw \|\| vw \| xz \|\| yz = uw $ xz ◅β \|\| subst-Par yz vw
	confluence-Par (u $ x ◅β) (Λ v $ y) with confluence-Par u v \| confluence-Par x y
	... \| uw \|\| vw \| xz \|\| yz = subst-Par xz uw \|\| vw $ yz ◅β
	confluence-Par (u $ x ◅β) (v $ y ◅β) with confluence-Par u v \| confluence-Par x y
	... \| uw \|\| vw \| xz \|\| yz = subst-Par xz uw \|\| subst-Par yz vw

	confluence-Par* : ∀ {α} → Confluent (Star (Parβ {α}))
	confluence-Par* = Confluent-Star confluence-Par

	-- And now we get confluence for β*
	confluence : ∀ {α} → Confluent (Star (_-β→_ {α}))
	confluence ab ac = CommonReduct.map Par→β (confluence-Par (Star.map β→Par ab) (Star.map β→Par ac))