Proof of correctness of addition and multiplication of Church numerals in Agda

agda/Lambda/ChurchNumerals.agda

@@ -0,0 +1,135 @@
+
+module Lambda.ChurchNumerals where
+
+open import Function
+open import Data.Nat
+open import Data.Star
+open import Data.Star.Properties
+open import Relation.Binary.PropositionalEquality
+
+open import Lambda.Core
+open import Lambda.ClosedTerms
+open import Lambda.Properties
+
+open →β⋆-Reasoning
+
+iter-tapp : ℕ → Term → Term → Term
+iter-tapp 0       f b = b
+iter-tapp (suc n) f b = tapp f (iter-tapp n f b)
+
+iter-tapp-+ : ∀ n m f b → iter-tapp n f (iter-tapp m f b) ≡ iter-tapp (n + m) f b
+iter-tapp-+ 0       m f b = refl
+iter-tapp-+ (suc n) m f b = cong (tapp f) (iter-tapp-+ n m f b)
+
+iter-tapp-closed : ∀ n f b l → Closed′ l f → Closed′ l b → Closed′ l (iter-tapp n f b)
+iter-tapp-closed 0       f b l f-closed′ b-closed′ = b-closed′
+iter-tapp-closed (suc n) f b l f-closed′ b-closed′ = ctapp f-closed′ (iter-tapp-closed n f b l f-closed′ b-closed′)
+
+iter-tapp-subst : ∀ n f b v s → iter-tapp n f b [ v ≔ s ] ≡ iter-tapp n (f [ v ≔ s ]) (b [ v ≔ s ])
+iter-tapp-subst 0       f b v s = refl
+iter-tapp-subst (suc n) f b v s = cong (tapp (f [ v ≔ s ])) (iter-tapp-subst n f b v s)
+
+iter-tapp-shift : ∀ n f b c d → shift c d (iter-tapp n f b) ≡ iter-tapp n (shift c d f) (shift c d b)
+iter-tapp-shift 0       f b c d = refl
+iter-tapp-shift (suc n) f b c d = cong (tapp (shift c d f)) (iter-tapp-shift n f b c d)
+
+iter-tapp-unshift : ∀ n f b c d → unshift c d (iter-tapp n f b) ≡ iter-tapp n (unshift c d f) (unshift c d b)
+iter-tapp-unshift 0       f b c d = refl
+iter-tapp-unshift (suc n) f b c d = cong (tapp (unshift c d f)) (iter-tapp-unshift n f b c d)
+
+-- (λ s. λ z. s (s (... (s z)))) where the number of applications of `s` is given by the first parameter
+church : ℕ → Term
+church n = tabs (tabs (iter-tapp n (tvar 1) (tvar 0)))
+
+church-closed : ∀ n → Closed (church n)
+church-closed n = ctabs (ctabs (iter-tapp-closed n (tvar 1) (tvar 0) 2 (ctvar (s≤s (s≤s z≤n))) (ctvar (s≤s z≤n))))
+
+-- (λ a b s z. a s (b s z))
+church-+ : Term
+church-+ = tabs (tabs (tabs (tabs (tapp (tapp (tvar 3) (tvar 1))
+                                        (tapp (tapp (tvar 2) (tvar 1)) (tvar 0))))))
+
+church-+-correct : ∀ n m → tapp (tapp church-+ (church n)) (church m) →β⋆ church (n + m)
+church-+-correct n m =
+  begin
+    tapp (tapp church-+ (church n)) (church m)
+      →β⋆⟨ return (→βappl (→βbeta-closed (church-closed n))) ⟩
+    tapp (tabs (tabs (tabs (tapp (tapp (church n) (tvar 1)) _)))) (church m)
+      →β⋆⟨ return (→βbeta-closed (church-closed m)) ⟩
+    (tabs ∘ tabs)
+      ↘⟨ →β⋆abs ∘ →β⋆abs ⟩
+        begin
+          tapp (tapp _ (tvar 1)) (tapp (tapp (church m) _) _)
+            ≡⟨ cong₂ tapp (cong₂ tapp (closed-beta-closed (church n) 2 (church m) (church-closed n)) refl) refl ⟩
+          tapp (tapp (church n) (tvar 1)) (tapp (tapp (church m) (tvar 1)) (tvar 0))
+            →β⋆⟨ →βappl →βbeta ◅ →βappr (→βappl →βbeta) ◅ ε ⟩
+          tapp (tabs _) (tapp (tabs _) (tvar 0))
+            ≡⟨ (let a = λ k → cong tabs (trans (cong (unshift 1 1) (iter-tapp-subst k (tvar 1) (tvar 0) 1 (tvar 3))) (iter-tapp-unshift k (tvar 3) (tvar 0) 1 1)) in cong₂ tapp (a n) (cong₂ tapp (a m) refl)) ⟩
+          tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (tapp (tabs (iter-tapp m (tvar 2) (tvar 0))) (tvar 0))
+            →β⋆⟨ return (→βappr →βbeta) ⟩
+          tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) _
+            ≡⟨ cong (tapp _) (trans (cong (unshift 1 0) (iter-tapp-subst m (tvar 2) (tvar 0) 0 (tvar 1))) (iter-tapp-unshift m (tvar 2) (tvar 1) 1 0)) ⟩
+          tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (iter-tapp m (tvar 1) (tvar 0))
+            →β⋆⟨ return →βbeta ⟩
+          _
+           ≡⟨ trans (cong (unshift 1 0) (iter-tapp-subst n (tvar 2) (tvar 0) 0 (shift 1 0 (iter-tapp m (tvar 1) (tvar 0))))) (trans (iter-tapp-unshift n (tvar 2) (shift 1 0 (iter-tapp m (tvar 1) (tvar 0))) 1 0) (cong (iter-tapp n (tvar 1)) (trans (cong (unshift 1 0) (iter-tapp-shift m (tvar 1) (tvar 0) 1 0)) (iter-tapp-unshift m (tvar 2) (tvar 1) 1 0)))) ⟩
+          iter-tapp n (tvar 1) (iter-tapp m (tvar 1) (tvar 0))
+            ≡⟨ iter-tapp-+ n m (tvar 1) (tvar 0) ⟩
+          iter-tapp (n + m) (tvar 1) (tvar 0)
+        ∎
+      ↙
+    tabs (tabs (iter-tapp (n + m) (tvar 1) (tvar 0)))
+      ≡⟨ refl ⟩
+    church (n + m)
+  ∎
+
+-- (λ a b s. a (y s))
+church-* : Term
+church-* = tabs (tabs (tabs (tapp (tvar 2) (tapp (tvar 1) (tvar 0)))))
+
+iter-tapp-* : ∀ n m → iter-tapp n (tabs (iter-tapp m (tvar 2) (tvar 0))) (tvar 0) →β⋆ iter-tapp (n * m) (tvar 1) (tvar 0)
+iter-tapp-* 0 m = ε
+iter-tapp-* (suc n) m =
+  begin
+    tapp (tabs (iter-tapp m (tvar 2) (tvar 0))) (iter-tapp n (tabs (iter-tapp m (tvar 2) (tvar 0))) (tvar 0))
+      →β⋆⟨ →β⋆appr (iter-tapp-* n m) ⟩
+    tapp (tabs (iter-tapp m (tvar 2) (tvar 0))) (iter-tapp (n * m) (tvar 1) (tvar 0))
+      →β⋆⟨ return →βbeta ⟩
+    _
+      ≡⟨ trans (cong (unshift 1 0) (iter-tapp-subst m (tvar 2) (tvar 0) 0 _)) (trans (iter-tapp-unshift m _ _ _ _) (cong (iter-tapp m (tvar 1)) (trans (cong (unshift 1 0) (iter-tapp-shift (n * m) _ _ 1 0)) (iter-tapp-unshift (n * m) _ _ 1 0)))) ⟩
+    iter-tapp m (tvar 1) (iter-tapp (n * m) (tvar 1) (tvar 0))
+      ≡⟨ iter-tapp-+ m (n * m) (tvar 1) (tvar 0) ⟩
+    iter-tapp (m + n * m) (tvar 1) (tvar 0)
+  ∎
+
+church-*-correct : ∀ n m → (tapp (tapp church-* (church n)) (church m)) →β⋆ church (n * m)
+church-*-correct n m =
+  begin
+    tapp (tapp church-* (church n)) (church m)
+      →β⋆⟨ return (→βappl (→βbeta-closed (church-closed n))) ⟩
+    tapp (tabs (tabs (tapp (church n) (tapp (tvar 1) (tvar 0))))) (church m)
+      →β⋆⟨ return (→βbeta-closed (church-closed m)) ⟩
+    tabs
+      ↘⟨ →β⋆abs ⟩
+        begin
+          (tapp (beta-closed (church n) 1 (church m)) (tapp (church m) (tvar 0)))
+            ≡⟨ cong₂ tapp (closed-beta-closed _ _ _ (church-closed n)) refl ⟩
+          tapp (church n) (tapp (church m) (tvar 0))
+            →β⋆⟨ return (→βappr →βbeta) ⟩
+          tapp (church n) _
+            ≡⟨ cong (tapp (church n)) (cong tabs (trans (cong (unshift 1 1) (iter-tapp-subst m _ _ _ _)) (iter-tapp-unshift m _ _ _ _))) ⟩
+          tapp (church n) (tabs (iter-tapp m (tvar 1) (tvar 0)))
+            →β⋆⟨ return →βbeta ⟩
+          tabs _
+            ≡⟨ cong tabs (trans (cong (unshift 1 1) (iter-tapp-subst n _ _ _ _)) (iter-tapp-unshift n _ _ _ _)) ⟩
+          tabs (iter-tapp n (tabs _) (tvar 0))
+            ≡⟨ cong tabs (cong₂ (iter-tapp n) (cong tabs (trans (cong (unshift 1 2) (trans (shiftAdd 1 1 1 (iter-tapp m (tvar 1) (tvar 0))) (iter-tapp-shift m (tvar 1) (tvar 0) 2 1))) (iter-tapp-unshift m (tvar 3) (tvar 0) 1 2))) refl) ⟩
+          tabs (iter-tapp n (tabs (iter-tapp m (tvar 2) (tvar 0))) (tvar 0))
+            →β⋆⟨ →β⋆abs (iter-tapp-* n m) ⟩
+          tabs (iter-tapp (n * m) (tvar 1) (tvar 0))
+        ∎
+      ↙
+    tabs (tabs (iter-tapp (n * m) (tvar 1) (tvar 0)))
+      ≡⟨ refl ⟩
+    church (n * m)
+  ∎

agda/Lambda/ClosedTerms.agda

@@ -0,0 +1,94 @@
+
+module Lambda.ClosedTerms where
+
+open import Data.Empty
+open import Data.Nat
+open import Data.Nat.Properties
+open import Relation.Binary hiding (nonEmpty)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+open import Lambda.Core
+
+data Closed′ (n : ℕ) : Term → Set where
+  ctvar : ∀ {v} → v < n → Closed′ n (tvar v)
+  ctapp : ∀ {t₁ t₂} → Closed′ n t₁ → Closed′ n t₂ → Closed′ n (tapp t₁ t₂)
+  ctabs : ∀ {t} → Closed′ (suc n) t → Closed′ n (tabs t)
+
+closed-incr : ∀ {n} {t} i → Closed′ n t → Closed′ (n + i) t
+closed-incr {n} {tvar x} i (ctvar x<n) = ctvar (≤-trans x<n (m≤m+n n i))
+  where open DecTotalOrder decTotalOrder renaming (trans to ≤-trans)
+closed-incr {n} {tapp t₁ t₂} i (ctapp ct₁ ct₂) = ctapp (closed-incr i ct₁) (closed-incr i ct₂)
+closed-incr {n} {tabs t} i (ctabs ct) = ctabs (closed-incr i ct)
+
+Closed : Term → Set
+Closed t = Closed′ 0 t
+
+<-irreflexive : ∀ n → ¬ (n < n)
+<-irreflexive 0 ()
+<-irreflexive (suc n) ssn≤sn = <-irreflexive n (≤-pred ssn≤sn)
+
+<⇒≢ : ∀ n m → n < m → n ≢ m
+<⇒≢ n m n<m n≡m rewrite sym n≡m = <-irreflexive n n<m
+
+closed′-subst : ∀ {n} t s v → Closed′ n t → n ≤ v → t [ v ≔ s ] ≡ t
+closed′-subst (tvar x) s v (ctvar x<n) n≤v with v ≟ x
+... | yes v≡x = ⊥-elim (<⇒≢ x v (≤-trans x<n n≤v) (sym v≡x))
+  where open DecTotalOrder decTotalOrder renaming (trans to ≤-trans)
+... | no  _   = refl
+closed′-subst (tapp t₁ t₂) s v (ctapp ct₁ ct₂) n≤v = cong₂ tapp (closed′-subst t₁ s v ct₁ n≤v) (closed′-subst t₂ s v ct₂ n≤v)
+closed′-subst (tabs t) s v (ctabs ct) n≤v = cong tabs (closed′-subst t (shift 1 0 s) (suc v) ct (s≤s n≤v))
+
+closed-subst : ∀ t s v → Closed t → t [ v ≔ s ] ≡ t
+closed-subst t s v closed = closed′-subst t s v closed z≤n
+
+closed′-shift : ∀ {n} t d c → Closed′ n t → n ≤ c → shift d c t ≡ t
+closed′-shift (tvar x) d c (ctvar x<n) n≤c with c ≤? x
+... | yes c≤x = ⊥-elim (<-irreflexive x (≤-trans x<n (≤-trans n≤c c≤x)))
+  where open DecTotalOrder decTotalOrder renaming (trans to ≤-trans)
+... | no  _   = refl
+closed′-shift (tapp t₁ t₂) d c (ctapp ct₁ ct₂) n≤c = cong₂ tapp (closed′-shift t₁ d c ct₁ n≤c) (closed′-shift t₂ d c ct₂ n≤c)
+closed′-shift (tabs t) d c (ctabs ct) n≤c = cong tabs (closed′-shift t d (suc c) ct (s≤s n≤c))
+
+closed-shift : ∀ t d c → Closed t → shift d c t ≡ t
+closed-shift t d c closed = closed′-shift t d c closed z≤n
+
+closed′-unshift : ∀ {n} t d c → Closed′ n t → n ≤ c → unshift d c t ≡ t
+closed′-unshift (tvar x) d c (ctvar x<n) n≤c with c ≤? x
+... | yes c≤x = ⊥-elim (<-irreflexive x (≤-trans x<n (≤-trans n≤c c≤x)))
+  where open DecTotalOrder decTotalOrder renaming (trans to ≤-trans)
+... | no  _   = refl
+closed′-unshift (tapp t₁ t₂) d c (ctapp ct₁ ct₂) n≤c = cong₂ tapp (closed′-unshift t₁ d c ct₁ n≤c) (closed′-unshift t₂ d c ct₂ n≤c)
+closed′-unshift (tabs t) d c (ctabs ct) n≤c = cong tabs (closed′-unshift t d (suc c) ct (s≤s n≤c))
+
+closed-unshift : ∀ t d c → Closed t → unshift d c t ≡ t
+closed-unshift t d c closed = closed′-unshift t d c closed z≤n
+
+beta-closed : Term → ℕ → Term → Term
+beta-closed (tvar x) v s with v ≟ x
+... | yes p = s
+... | no  p = unshift 1 v (tvar x)
+beta-closed (tapp t₁ t₂) v s = tapp (beta-closed t₁ v s) (beta-closed t₂ v s)
+beta-closed (tabs t) v s = tabs (beta-closed t (suc v) s)
+
+beta-closed-unshift-subst : ∀ t s v → Closed s → unshift 1 v (t [ v ≔ s ]) ≡ beta-closed t v s
+beta-closed-unshift-subst (tvar x) s v c with v ≟ x
+... | yes v≡x = closed-unshift s 1 v c
+... | no  v≢x = refl
+beta-closed-unshift-subst (tapp t₁ t₂) s v c = cong₂ tapp (beta-closed-unshift-subst t₁ s v c) (beta-closed-unshift-subst t₂ s v c)
+beta-closed-unshift-subst (tabs t) s v c = cong tabs (trans (cong (unshift 1 (suc v)) (cong (_[_≔_] t (suc v)) (closed-shift s 1 0 c)))
+                                                            (beta-closed-unshift-subst t s (suc v) c))
+
+→βbeta-closed : ∀ {t} {s} → Closed s → tapp (tabs t) s →β beta-closed t 0 s
+→βbeta-closed {t} {s} c rewrite sym (trans (cong (unshift 1 0) (cong (_[_≔_] t 0) (closed-shift s 1 0 c))) (beta-closed-unshift-subst t s 0 c)) = →βbeta
+
+closed′-beta-closed : ∀ {n} t v s → Closed′ n t → n ≤ v → beta-closed t v s ≡ t
+closed′-beta-closed (tvar x) v s (ctvar x<n) n≤v with v ≟ x
+... | yes v≡x = ⊥-elim (<⇒≢ x v (≤-trans x<n n≤v) (sym v≡x))
+  where open DecTotalOrder decTotalOrder renaming (trans to ≤-trans)
+... | no  p = closed′-unshift (tvar x) 1 v (ctvar x<n) n≤v
+closed′-beta-closed (tapp t₁ t₂) v s (ctapp ct₁ ct₂) n≤v = cong₂ tapp (closed′-beta-closed t₁ v s ct₁ n≤v) (closed′-beta-closed t₂ v s ct₂ n≤v)
+closed′-beta-closed (tabs t) v s (ctabs ct) n≤v = cong tabs (closed′-beta-closed t (suc v) s ct (s≤s n≤v))
+
+closed-beta-closed : ∀ t v s → Closed t → beta-closed t v s ≡ t
+closed-beta-closed t v s c = closed′-beta-closed t v s c z≤n

agda/Lambda/Confluence.agda

@@ -13,18 +13,6 @@ open import Relation.Binary.PropositionalEquality
 open import Lambda.Core
 open import Lambda.Properties
 
-→β*appl : ∀ {t1 t1' t2} → t1 →β* t1' → tapp t1 t2 →β* tapp t1' t2
-→β*appl ε = ε
-→β*appl (r1 ◅ r2) = →βappl r1 ◅ →β*appl r2
-
-→β*appr : ∀ {t1 t2 t2'} → t2 →β* t2' → tapp t1 t2 →β* tapp t1 t2'
-→β*appr ε = ε
-→β*appr (r1 ◅ r2) = →βappr r1 ◅ →β*appr r2
-
-→β*abs : ∀ {t t'} → t →β* t' → tabs t →β* tabs t'
-→β*abs ε = ε
-→β*abs (r1 ◅ r2) = →βabs r1 ◅ →β*abs r2
-
 parRefl : ∀ {t} → t →βP t
 parRefl {tvar _} = →βPvar
 parRefl {tapp _ _} = →βPapp parRefl parRefl
@@ -36,11 +24,11 @@ parRefl {tabs _} = →βPabs parRefl
 →β⊂→βP (→βappr r) = →βPapp parRefl (→β⊂→βP r)
 →β⊂→βP (→βabs r) = →βPabs (→β⊂→βP r)
 
-→βP⊂→β* : _→βP_ ⇒ _→β*_
-→βP⊂→β* →βPvar = ε
-→βP⊂→β* (→βPapp r1 r2) = →β*appl (→βP⊂→β* r1) ◅◅ →β*appr (→βP⊂→β* r2)
-→βP⊂→β* (→βPabs r) = →β*abs (→βP⊂→β* r)
-→βP⊂→β* (→βPbeta r1 r2) = →β*appl (→β*abs (→βP⊂→β* r1)) ◅◅ →β*appr (→βP⊂→β* r2) ◅◅ →βbeta ◅ ε
+→βP⊂→β⋆ : _→βP_ ⇒ _→β⋆_
+→βP⊂→β⋆ →βPvar = ε
+→βP⊂→β⋆ (→βPapp r1 r2) = →β⋆appl (→βP⊂→β⋆ r1) ◅◅ →β⋆appr (→βP⊂→β⋆ r2)
+→βP⊂→β⋆ (→βPabs r) = →β⋆abs (→βP⊂→β⋆ r)
+→βP⊂→β⋆ (→βPbeta r1 r2) = →β⋆appl (→β⋆abs (→βP⊂→β⋆ r1)) ◅◅ →β⋆appr (→βP⊂→β⋆ r2) ◅◅ →βbeta ◅ ε
 
 shiftConservation→β : ∀ {d c} → _→β_ ⇒ ((λ a b → a → b) on Shifted d c)
 shiftConservation→β {d} {c} {tapp (tabs t1) t2} →βbeta (sapp (sabs s1) s2) =
@@ -49,12 +37,12 @@ shiftConservation→β (→βappl p) (sapp s1 s2) = sapp (shiftConservation→β
 shiftConservation→β (→βappr p) (sapp s1 s2) = sapp s1 (shiftConservation→β p s2)
 shiftConservation→β (→βabs p) (sabs s1) = sabs (shiftConservation→β p s1)
 
-shiftConservation→β* : ∀ {d c} → _→β*_ ⇒ ((λ a b → a → b) on Shifted d c)
-shiftConservation→β* ε s = s
-shiftConservation→β* (p1 ◅ p2) s = shiftConservation→β* p2 (shiftConservation→β p1 s)
+shiftConservation→β⋆ : ∀ {d c} → _→β⋆_ ⇒ ((λ a b → a → b) on Shifted d c)
+shiftConservation→β⋆ ε s = s
+shiftConservation→β⋆ (p1 ◅ p2) s = shiftConservation→β⋆ p2 (shiftConservation→β p1 s)
 
 shiftConservation→βP : ∀ {d c t1 t2} → t1 →βP t2 → Shifted d c t1 → Shifted d c t2
-shiftConservation→βP p s = shiftConservation→β* (→βP⊂→β* p) s
+shiftConservation→βP p s = shiftConservation→β⋆ (→βP⊂→β⋆ p) s
 
 shiftLemma : ∀ {t t' d c} → t →βP t' → shift d c t →βP shift d c t'
 shiftLemma →βPvar = parRefl
@@ -192,7 +180,7 @@ confluence→βP = SemiConfluence⇒Confluence $ Diamond⇒SemiConfluence diamon
 confluence→β : Confluence _→β_
 confluence→β r1 r2 =
   proj₁ c ,
-  Data.Star.concat (Data.Star.map →βP⊂→β* (proj₁ (proj₂ c))) ,
-  Data.Star.concat (Data.Star.map →βP⊂→β* (proj₂ (proj₂ c))) where
+  Data.Star.concat (Data.Star.map →βP⊂→β⋆ (proj₁ (proj₂ c))) ,
+  Data.Star.concat (Data.Star.map →βP⊂→β⋆ (proj₂ (proj₂ c))) where
   c = confluence→βP (Data.Star.map →β⊂→βP r1) (Data.Star.map →β⊂→βP r2)
 

agda/Lambda/Core.agda

@@ -5,6 +5,7 @@ import Level
 open import Function
 open import Data.Nat
 open import Data.Star
+open import Data.Star.Properties
 open import Relation.Nullary
 open import Relation.Binary
 
@@ -44,8 +45,20 @@ data _→β_ : Rel Term Level.zero where
   →βappr : ∀ {t1 t2 t2'} → t2 →β t2' → tapp t1 t2 →β tapp t1 t2'
   →βabs  : ∀ {t t'} → t →β t' → tabs t →β tabs t'
 
-_→β*_ : Rel Term Level.zero
-_→β*_ = Star _→β_
+_→β⋆_ : Rel Term Level.zero
+_→β⋆_ = Star _→β_
+
+→β⋆appl : ∀ {t1 t1' t2} → t1 →β⋆ t1' → tapp t1 t2 →β⋆ tapp t1' t2
+→β⋆appl ε = ε
+→β⋆appl (r1 ◅ r2) = →βappl r1 ◅ →β⋆appl r2
+
+→β⋆appr : ∀ {t1 t2 t2'} → t2 →β⋆ t2' → tapp t1 t2 →β⋆ tapp t1 t2'
+→β⋆appr ε = ε
+→β⋆appr (r1 ◅ r2) = →βappr r1 ◅ →β⋆appr r2
+
+→β⋆abs : ∀ {t t'} → t →β⋆ t' → tabs t →β⋆ tabs t'
+→β⋆abs ε = ε
+→β⋆abs (r1 ◅ r2) = →βabs r1 ◅ →β⋆abs r2
 
 data _→βP_ : Rel Term Level.zero where
   →βPvar : ∀ {n} → tvar n →βP tvar n
@@ -60,3 +73,10 @@ tapp (tabs t1) t2 * = unshift 1 0 (t1 * [ 0 ≔ shift 1 0 (t2 *) ])
 tapp t1 t2 * = tapp (t1 *) (t2 *)
 tabs t * = tabs (t *)
 
+module →β⋆-Reasoning where
+  open StarReasoning (_→β_) public renaming (_⟶⋆⟨_⟩_ to _→β⋆⟨_⟩_)
+
+  infixr 2 _↘⟨_⟩_↙_
+
+  _↘⟨_⟩_↙_ : ∀ {a} {b} {z} → (f : Term → Term) → (∀ {x} {y} → x →β⋆ y → f x →β⋆ f y) → a →β⋆ b → f b IsRelatedTo z → f a IsRelatedTo z
+  f ↘⟨ congr ⟩ a→β⋆b ↙ (relTo fb→β⋆z) = relTo (congr a→β⋆b ◅◅ fb→β⋆z)