From d32b553c339ea14d88fb9f66cbd17ff61588ba93 Mon Sep 17 00:00:00 2001 From: Tim Baumann Date: Sun, 26 May 2013 12:52:56 +0200 Subject: [PATCH 1/8] formalize closed terms in Agda --- agda/Lambda/ClosedTerms.agda | 58 ++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 agda/Lambda/ClosedTerms.agda diff --git a/agda/Lambda/ClosedTerms.agda b/agda/Lambda/ClosedTerms.agda new file mode 100644 index 0000000..deeb064 --- /dev/null +++ b/agda/Lambda/ClosedTerms.agda @@ -0,0 +1,58 @@ + +module Lambda.ClosedTerms where + +open import Data.Empty +open import Data.Nat +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 + tvar-Closed′ : ∀ {v} → v < n → Closed′ n (tvar v) + tapp-Closed′ : ∀ {t₁ t₂} → Closed′ n t₁ → Closed′ n t₂ → Closed′ n (tapp t₁ t₂) + tabs-Closed′ : ∀ {t} → Closed′ (suc n) t → Closed′ n (tabs t) + +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 Date: Sun, 26 May 2013 12:54:13 +0200 Subject: [PATCH 2/8] prove correctness of addition of church numerals --- agda/Lambda/ChurchNumerals.agda | 96 +++++++++++++++++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 agda/Lambda/ChurchNumerals.agda diff --git a/agda/Lambda/ChurchNumerals.agda b/agda/Lambda/ChurchNumerals.agda new file mode 100644 index 0000000..6910251 --- /dev/null +++ b/agda/Lambda/ChurchNumerals.agda @@ -0,0 +1,96 @@ + +module Lambda.ChurchNumerals where + +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 + +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′ = tapp-Closed′ 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 = tabs-Closed′ (tabs-Closed′ (iter-tapp-closed n (tvar 1) (tvar 0) 2 (tvar-Closed′ (s≤s (s≤s z≤n))) (tvar-Closed′ (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) ⟩ + tapp (tabs (tabs (tabs (tapp (tapp (unshift 1 3 (shift 1 0 (shift 1 0 (shift 1 0 (shift 1 0 (church n)))))) (tvar 1)) _)))) (church m) + ≅⟨ cong₂ tapp (cong tabs (cong tabs (cong tabs (cong₂ tapp (cong₂ tapp eq₁ refl) refl)))) refl ⟩ + tapp (tabs (tabs (tabs (tapp (tapp (church n) (tvar 1)) _)))) (church m) + ⟶⋆⟨ return →βbeta ⟩ + tabs (tabs (tapp (tapp (unshift 1 (suc (suc 0)) (church n [ suc (suc 0) ≔ shift 1 0 (shift 1 0 (shift 1 0 (church m))) ])) (tvar 1)) + (tapp (tapp (unshift 1 2 (shift 1 0 (shift 1 0 (shift 1 0 (church m))))) _) _))) + ≅⟨ cong tabs (cong tabs (cong₂ tapp (cong₂ tapp eq₂ refl) (cong₂ tapp (cong₂ tapp eq₃ refl) refl))) ⟩ + tabs (tabs (tapp (tapp (church n) (tvar 1)) (tapp (tapp (church m) (tvar 1)) (tvar 0)))) + ⟶⋆⟨ →βabs (→βabs (→βappl →βbeta)) ◅ (→βabs (→βabs (→βappr (→βappl →βbeta))) ◅ ε) ⟩ + tabs (tabs (tapp (tabs _) (tapp (tabs _) (tvar 0)))) + ≅⟨ cong tabs (cong tabs (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))) ⟩ + tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (tapp (tabs (iter-tapp m (tvar 2) (tvar 0))) (tvar 0)))) + ⟶⋆⟨ return (→βabs (→βabs (→βappr →βbeta))) ⟩ + tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) _)) + ≅⟨ cong tabs (cong tabs (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)))) ⟩ + tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (iter-tapp m (tvar 1) (tvar 0)))) + ⟶⋆⟨ return (→βabs (→βabs →βbeta)) ⟩ + tabs (tabs _) + ≅⟨ cong tabs (cong tabs (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)))))) ⟩ + tabs (tabs (iter-tapp n (tvar 1) (iter-tapp m (tvar 1) (tvar 0)))) + ≅⟨ cong tabs (cong tabs (iter-tapp-+ n m (tvar 1) (tvar 0))) ⟩ + tabs (tabs (iter-tapp (n + m) (tvar 1) (tvar 0))) + ≅⟨ refl ⟩ + church (n + m) + β∎ + where open StarReasoning (_→β_) renaming (_≡⟨_⟩_ to _≅⟨_⟩_; begin_ to βbegin_; _∎ to _β∎) + open ≡-Reasoning hiding (_≅⟨_⟩_) + eq₁ = begin + (unshift 1 3 (shift 1 0 (shift 1 0 (shift 1 0 (shift 1 0 (church n)))))) + ≡⟨ cong (unshift 1 3) (trans (shiftAdd 1 1 0 (shift 1 0 (shift 1 0 (church n)))) (trans (shiftAdd 2 1 0 (shift 1 0 (church n))) (shiftAdd 3 1 0 (church n)))) ⟩ + unshift 1 3 (shift 4 0 (church n)) + ≡⟨ cong (unshift 1 3) (closed-shift (church n) 4 0 (church-closed n)) ⟩ + unshift 1 3 (church n) + ≡⟨ closed-unshift (church n) 1 3 (church-closed n) ⟩ + church n + ∎ + eq₂ = (trans (cong (unshift 1 2) (closed-subst (church n) (shift 1 0 (shift 1 0 (shift 1 0 (church m)))) 2 (church-closed n))) (closed-unshift (church n) 1 2 (church-closed n))) + eq₃ = begin + unshift 1 2 (shift 1 0 (shift 1 0 (shift 1 0 (church m)))) ≡⟨ cong (unshift 1 2) (trans (shiftAdd 1 1 0 (shift 1 0 (church m))) (shiftAdd 2 1 0 (church m))) ⟩ + unshift 1 2 (shift 3 0 (church m)) ≡⟨ cong (unshift 1 2) (closed-shift (church m) 3 0 (church-closed m)) ⟩ + unshift 1 2 (church m) ≡⟨ closed-unshift (church m) 1 2 (church-closed m) ⟩ + church m + ∎ \ No newline at end of file From 61378d70fd3842699a9f55624dff53c4f9ab23b2 Mon Sep 17 00:00:00 2001 From: Tim Baumann Date: Sun, 26 May 2013 13:02:17 +0200 Subject: [PATCH 3/8] use new module for reasoning about beta-reduction in agda --- agda/Lambda/ChurchNumerals.agda | 15 ++++++++------- agda/Lambda/Core.agda | 3 +++ 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/agda/Lambda/ChurchNumerals.agda b/agda/Lambda/ChurchNumerals.agda index 6910251..8743f80 100644 --- a/agda/Lambda/ChurchNumerals.agda +++ b/agda/Lambda/ChurchNumerals.agda @@ -10,6 +10,8 @@ open import Lambda.Core open import Lambda.ClosedTerms open import Lambda.Properties +open →β⋆-Reasoning renaming (_≡⟨_⟩_ to _≅⟨_⟩_; begin_ to βbegin_; _∎ to _β∎) + iter-tapp : ℕ → Term → Term → Term iter-tapp 0 f b = b iter-tapp (suc n) f b = tapp f (iter-tapp n f b) @@ -50,24 +52,24 @@ church-+-correct : ∀ n m → tapp (tapp church-+ (church n)) (church m) →β* church-+-correct n m = βbegin tapp (tapp church-+ (church n)) (church m) - ⟶⋆⟨ return (→βappl →βbeta) ⟩ + →β⋆⟨ return (→βappl →βbeta) ⟩ tapp (tabs (tabs (tabs (tapp (tapp (unshift 1 3 (shift 1 0 (shift 1 0 (shift 1 0 (shift 1 0 (church n)))))) (tvar 1)) _)))) (church m) ≅⟨ cong₂ tapp (cong tabs (cong tabs (cong tabs (cong₂ tapp (cong₂ tapp eq₁ refl) refl)))) refl ⟩ tapp (tabs (tabs (tabs (tapp (tapp (church n) (tvar 1)) _)))) (church m) - ⟶⋆⟨ return →βbeta ⟩ + →β⋆⟨ return →βbeta ⟩ tabs (tabs (tapp (tapp (unshift 1 (suc (suc 0)) (church n [ suc (suc 0) ≔ shift 1 0 (shift 1 0 (shift 1 0 (church m))) ])) (tvar 1)) (tapp (tapp (unshift 1 2 (shift 1 0 (shift 1 0 (shift 1 0 (church m))))) _) _))) ≅⟨ cong tabs (cong tabs (cong₂ tapp (cong₂ tapp eq₂ refl) (cong₂ tapp (cong₂ tapp eq₃ refl) refl))) ⟩ tabs (tabs (tapp (tapp (church n) (tvar 1)) (tapp (tapp (church m) (tvar 1)) (tvar 0)))) - ⟶⋆⟨ →βabs (→βabs (→βappl →βbeta)) ◅ (→βabs (→βabs (→βappr (→βappl →βbeta))) ◅ ε) ⟩ + →β⋆⟨ →βabs (→βabs (→βappl →βbeta)) ◅ (→βabs (→βabs (→βappr (→βappl →βbeta))) ◅ ε) ⟩ tabs (tabs (tapp (tabs _) (tapp (tabs _) (tvar 0)))) ≅⟨ cong tabs (cong tabs (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))) ⟩ tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (tapp (tabs (iter-tapp m (tvar 2) (tvar 0))) (tvar 0)))) - ⟶⋆⟨ return (→βabs (→βabs (→βappr →βbeta))) ⟩ + →β⋆⟨ return (→βabs (→βabs (→βappr →βbeta))) ⟩ tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) _)) ≅⟨ cong tabs (cong tabs (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)))) ⟩ tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (iter-tapp m (tvar 1) (tvar 0)))) - ⟶⋆⟨ return (→βabs (→βabs →βbeta)) ⟩ + →β⋆⟨ return (→βabs (→βabs →βbeta)) ⟩ tabs (tabs _) ≅⟨ cong tabs (cong tabs (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)))))) ⟩ tabs (tabs (iter-tapp n (tvar 1) (iter-tapp m (tvar 1) (tvar 0)))) @@ -76,8 +78,7 @@ church-+-correct n m = ≅⟨ refl ⟩ church (n + m) β∎ - where open StarReasoning (_→β_) renaming (_≡⟨_⟩_ to _≅⟨_⟩_; begin_ to βbegin_; _∎ to _β∎) - open ≡-Reasoning hiding (_≅⟨_⟩_) + where open ≡-Reasoning hiding (_≅⟨_⟩_) eq₁ = begin (unshift 1 3 (shift 1 0 (shift 1 0 (shift 1 0 (shift 1 0 (church n)))))) ≡⟨ cong (unshift 1 3) (trans (shiftAdd 1 1 0 (shift 1 0 (shift 1 0 (church n)))) (trans (shiftAdd 2 1 0 (shift 1 0 (church n))) (shiftAdd 3 1 0 (church n)))) ⟩ diff --git a/agda/Lambda/Core.agda b/agda/Lambda/Core.agda index f248180..2c0f849 100644 --- a/agda/Lambda/Core.agda +++ b/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 @@ -60,3 +61,5 @@ 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 _→β⋆⟨_⟩_) \ No newline at end of file From 8f6201d39ca933b8f7d1d6dbf0d6e6115792e56b Mon Sep 17 00:00:00 2001 From: Tim Baumann Date: Sun, 26 May 2013 14:34:11 +0200 Subject: [PATCH 4/8] simplify proof of church addition by using special reduction rule for closed terms --- agda/Lambda/ChurchNumerals.agda | 44 +++++++++------------------------ agda/Lambda/ClosedTerms.agda | 31 ++++++++++++++++++++++- 2 files changed, 42 insertions(+), 33 deletions(-) diff --git a/agda/Lambda/ChurchNumerals.agda b/agda/Lambda/ChurchNumerals.agda index 8743f80..268b101 100644 --- a/agda/Lambda/ChurchNumerals.agda +++ b/agda/Lambda/ChurchNumerals.agda @@ -10,7 +10,7 @@ open import Lambda.Core open import Lambda.ClosedTerms open import Lambda.Properties -open →β⋆-Reasoning renaming (_≡⟨_⟩_ to _≅⟨_⟩_; begin_ to βbegin_; _∎ to _β∎) +open →β⋆-Reasoning iter-tapp : ℕ → Term → Term → Term iter-tapp 0 f b = b @@ -50,48 +50,28 @@ church-+ = tabs (tabs (tabs (tabs (tapp (tapp (tvar 3) (tvar 1)) church-+-correct : ∀ n m → tapp (tapp church-+ (church n)) (church m) →β* church (n + m) church-+-correct n m = - βbegin + begin tapp (tapp church-+ (church n)) (church m) - →β⋆⟨ return (→βappl →βbeta) ⟩ - tapp (tabs (tabs (tabs (tapp (tapp (unshift 1 3 (shift 1 0 (shift 1 0 (shift 1 0 (shift 1 0 (church n)))))) (tvar 1)) _)))) (church m) - ≅⟨ cong₂ tapp (cong tabs (cong tabs (cong tabs (cong₂ tapp (cong₂ tapp eq₁ refl) refl)))) refl ⟩ + →β⋆⟨ return (→βappl (→βbeta-closed (church-closed n))) ⟩ tapp (tabs (tabs (tabs (tapp (tapp (church n) (tvar 1)) _)))) (church m) - →β⋆⟨ return →βbeta ⟩ - tabs (tabs (tapp (tapp (unshift 1 (suc (suc 0)) (church n [ suc (suc 0) ≔ shift 1 0 (shift 1 0 (shift 1 0 (church m))) ])) (tvar 1)) - (tapp (tapp (unshift 1 2 (shift 1 0 (shift 1 0 (shift 1 0 (church m))))) _) _))) - ≅⟨ cong tabs (cong tabs (cong₂ tapp (cong₂ tapp eq₂ refl) (cong₂ tapp (cong₂ tapp eq₃ refl) refl))) ⟩ + →β⋆⟨ return (→βbeta-closed (church-closed m)) ⟩ + tabs (tabs (tapp (tapp _ (tvar 1)) (tapp (tapp (church m) _) _))) + ≡⟨ cong tabs (cong tabs (cong₂ tapp (cong₂ tapp (closed-beta-closed (church n) 2 (church m) (church-closed n)) refl) refl)) ⟩ tabs (tabs (tapp (tapp (church n) (tvar 1)) (tapp (tapp (church m) (tvar 1)) (tvar 0)))) →β⋆⟨ →βabs (→βabs (→βappl →βbeta)) ◅ (→βabs (→βabs (→βappr (→βappl →βbeta))) ◅ ε) ⟩ tabs (tabs (tapp (tabs _) (tapp (tabs _) (tvar 0)))) - ≅⟨ cong tabs (cong tabs (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))) ⟩ + ≡⟨ cong tabs (cong tabs (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))) ⟩ tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (tapp (tabs (iter-tapp m (tvar 2) (tvar 0))) (tvar 0)))) →β⋆⟨ return (→βabs (→βabs (→βappr →βbeta))) ⟩ tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) _)) - ≅⟨ cong tabs (cong tabs (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)))) ⟩ + ≡⟨ cong tabs (cong tabs (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)))) ⟩ tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (iter-tapp m (tvar 1) (tvar 0)))) →β⋆⟨ return (→βabs (→βabs →βbeta)) ⟩ tabs (tabs _) - ≅⟨ cong tabs (cong tabs (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)))))) ⟩ + ≡⟨ cong tabs (cong tabs (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)))))) ⟩ tabs (tabs (iter-tapp n (tvar 1) (iter-tapp m (tvar 1) (tvar 0)))) - ≅⟨ cong tabs (cong tabs (iter-tapp-+ n m (tvar 1) (tvar 0))) ⟩ + ≡⟨ cong tabs (cong tabs (iter-tapp-+ n m (tvar 1) (tvar 0))) ⟩ tabs (tabs (iter-tapp (n + m) (tvar 1) (tvar 0))) - ≅⟨ refl ⟩ + ≡⟨ refl ⟩ church (n + m) - β∎ - where open ≡-Reasoning hiding (_≅⟨_⟩_) - eq₁ = begin - (unshift 1 3 (shift 1 0 (shift 1 0 (shift 1 0 (shift 1 0 (church n)))))) - ≡⟨ cong (unshift 1 3) (trans (shiftAdd 1 1 0 (shift 1 0 (shift 1 0 (church n)))) (trans (shiftAdd 2 1 0 (shift 1 0 (church n))) (shiftAdd 3 1 0 (church n)))) ⟩ - unshift 1 3 (shift 4 0 (church n)) - ≡⟨ cong (unshift 1 3) (closed-shift (church n) 4 0 (church-closed n)) ⟩ - unshift 1 3 (church n) - ≡⟨ closed-unshift (church n) 1 3 (church-closed n) ⟩ - church n - ∎ - eq₂ = (trans (cong (unshift 1 2) (closed-subst (church n) (shift 1 0 (shift 1 0 (shift 1 0 (church m)))) 2 (church-closed n))) (closed-unshift (church n) 1 2 (church-closed n))) - eq₃ = begin - unshift 1 2 (shift 1 0 (shift 1 0 (shift 1 0 (church m)))) ≡⟨ cong (unshift 1 2) (trans (shiftAdd 1 1 0 (shift 1 0 (church m))) (shiftAdd 2 1 0 (church m))) ⟩ - unshift 1 2 (shift 3 0 (church m)) ≡⟨ cong (unshift 1 2) (closed-shift (church m) 3 0 (church-closed m)) ⟩ - unshift 1 2 (church m) ≡⟨ closed-unshift (church m) 1 2 (church-closed m) ⟩ - church m - ∎ \ No newline at end of file + ∎ \ No newline at end of file diff --git a/agda/Lambda/ClosedTerms.agda b/agda/Lambda/ClosedTerms.agda index deeb064..598fc13 100644 --- a/agda/Lambda/ClosedTerms.agda +++ b/agda/Lambda/ClosedTerms.agda @@ -55,4 +55,33 @@ closed′-unshift (tapp t₁ t₂) d c (tapp-Closed′ t₁-closed′ t₂-close closed′-unshift (tabs t) d c (tabs-Closed′ t-closed′) n≤c = cong tabs (closed′-unshift t d (suc c) t-closed′ (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 \ No newline at end of file +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 (tvar-Closed′ x Date: Sun, 26 May 2013 15:03:35 +0200 Subject: [PATCH 5/8] =?UTF-8?q?rename=20constructors=20for=20Closed?= =?UTF-8?q?=E2=80=B2?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- agda/Lambda/ChurchNumerals.agda | 4 ++-- agda/Lambda/ClosedTerms.agda | 32 ++++++++++++++++---------------- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/agda/Lambda/ChurchNumerals.agda b/agda/Lambda/ChurchNumerals.agda index 268b101..29785d1 100644 --- a/agda/Lambda/ChurchNumerals.agda +++ b/agda/Lambda/ChurchNumerals.agda @@ -22,7 +22,7 @@ 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′ = tapp-Closed′ f-closed′ (iter-tapp-closed n f b l f-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 @@ -41,7 +41,7 @@ church : ℕ → Term church n = tabs (tabs (iter-tapp n (tvar 1) (tvar 0))) church-closed : ∀ n → Closed (church n) -church-closed n = tabs-Closed′ (tabs-Closed′ (iter-tapp-closed n (tvar 1) (tvar 0) 2 (tvar-Closed′ (s≤s (s≤s z≤n))) (tvar-Closed′ (s≤s z≤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 diff --git a/agda/Lambda/ClosedTerms.agda b/agda/Lambda/ClosedTerms.agda index 598fc13..c7d3d45 100644 --- a/agda/Lambda/ClosedTerms.agda +++ b/agda/Lambda/ClosedTerms.agda @@ -10,9 +10,9 @@ open import Relation.Nullary open import Lambda.Core data Closed′ (n : ℕ) : Term → Set where - tvar-Closed′ : ∀ {v} → v < n → Closed′ n (tvar v) - tapp-Closed′ : ∀ {t₁ t₂} → Closed′ n t₁ → Closed′ n t₂ → Closed′ n (tapp t₁ t₂) - tabs-Closed′ : ∀ {t} → Closed′ (suc n) t → Closed′ n (tabs t) + 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 : Term → Set Closed t = Closed′ 0 t @@ -25,34 +25,34 @@ Closed t = Closed′ 0 t <⇒≢ n m n Date: Sun, 26 May 2013 17:02:35 +0200 Subject: [PATCH 6/8] simplified proof of church addition using congruence construction --- agda/Lambda/ChurchNumerals.agda | 41 +++++++++++++++++++-------------- agda/Lambda/Confluence.agda | 34 +++++++++------------------ agda/Lambda/Core.agda | 23 +++++++++++++++--- 3 files changed, 55 insertions(+), 43 deletions(-) diff --git a/agda/Lambda/ChurchNumerals.agda b/agda/Lambda/ChurchNumerals.agda index 29785d1..bca705c 100644 --- a/agda/Lambda/ChurchNumerals.agda +++ b/agda/Lambda/ChurchNumerals.agda @@ -1,6 +1,7 @@ module Lambda.ChurchNumerals where +open import Function open import Data.Nat open import Data.Star open import Data.Star.Properties @@ -48,29 +49,35 @@ 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 → 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 (tapp (tapp _ (tvar 1)) (tapp (tapp (church m) _) _))) - ≡⟨ cong tabs (cong tabs (cong₂ tapp (cong₂ tapp (closed-beta-closed (church n) 2 (church m) (church-closed n)) refl) refl)) ⟩ - tabs (tabs (tapp (tapp (church n) (tvar 1)) (tapp (tapp (church m) (tvar 1)) (tvar 0)))) - →β⋆⟨ →βabs (→βabs (→βappl →βbeta)) ◅ (→βabs (→βabs (→βappr (→βappl →βbeta))) ◅ ε) ⟩ - tabs (tabs (tapp (tabs _) (tapp (tabs _) (tvar 0)))) - ≡⟨ cong tabs (cong tabs (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))) ⟩ - tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (tapp (tabs (iter-tapp m (tvar 2) (tvar 0))) (tvar 0)))) - →β⋆⟨ return (→βabs (→βabs (→βappr →βbeta))) ⟩ - tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) _)) - ≡⟨ cong tabs (cong tabs (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)))) ⟩ - tabs (tabs (tapp (tabs (iter-tapp n (tvar 2) (tvar 0))) (iter-tapp m (tvar 1) (tvar 0)))) - →β⋆⟨ return (→βabs (→βabs →βbeta)) ⟩ - tabs (tabs _) - ≡⟨ cong tabs (cong tabs (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)))))) ⟩ - tabs (tabs (iter-tapp n (tvar 1) (iter-tapp m (tvar 1) (tvar 0)))) - ≡⟨ cong tabs (cong tabs (iter-tapp-+ n m (tvar 1) (tvar 0))) ⟩ + (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) diff --git a/agda/Lambda/Confluence.agda b/agda/Lambda/Confluence.agda index 2af54c1..99cb053 100644 --- a/agda/Lambda/Confluence.agda +++ b/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) diff --git a/agda/Lambda/Core.agda b/agda/Lambda/Core.agda index 2c0f849..9f27685 100644 --- a/agda/Lambda/Core.agda +++ b/agda/Lambda/Core.agda @@ -45,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 @@ -62,4 +74,9 @@ tapp t1 t2 * = tapp (t1 *) (t2 *) tabs t * = tabs (t *) module →β⋆-Reasoning where - open StarReasoning (_→β_) public renaming (_⟶⋆⟨_⟩_ to _→β⋆⟨_⟩_) \ No newline at end of file + 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) \ No newline at end of file From 48c03f5ac81c97316c067a105e8738c38106b242 Mon Sep 17 00:00:00 2001 From: Tim Baumann Date: Sun, 26 May 2013 23:35:32 +0200 Subject: [PATCH 7/8] prove correctness of multiplication of church numerals --- agda/Lambda/ChurchNumerals.agda | 53 +++++++++++++++++++++++++++++++++ agda/Lambda/ClosedTerms.agda | 23 +++++++++----- 2 files changed, 68 insertions(+), 8 deletions(-) diff --git a/agda/Lambda/ChurchNumerals.agda b/agda/Lambda/ChurchNumerals.agda index bca705c..1872384 100644 --- a/agda/Lambda/ChurchNumerals.agda +++ b/agda/Lambda/ChurchNumerals.agda @@ -21,6 +21,8 @@ iter-tapp-+ : ∀ n m f b → iter-tapp n f (iter-tapp m f b) ≡ iter-tapp (n + 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-* : ∀ n m f b → iter-tapp n () + 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′) @@ -81,4 +83,55 @@ church-+-correct n m = 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) ∎ \ No newline at end of file diff --git a/agda/Lambda/ClosedTerms.agda b/agda/Lambda/ClosedTerms.agda index c7d3d45..f6206a4 100644 --- a/agda/Lambda/ClosedTerms.agda +++ b/agda/Lambda/ClosedTerms.agda @@ -3,6 +3,7 @@ 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 @@ -14,6 +15,12 @@ data Closed′ (n : ℕ) : Term → Set where 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 Date: Sun, 26 May 2013 23:37:52 +0200 Subject: [PATCH 8/8] small cleanup --- agda/Lambda/ChurchNumerals.agda | 2 -- 1 file changed, 2 deletions(-) diff --git a/agda/Lambda/ChurchNumerals.agda b/agda/Lambda/ChurchNumerals.agda index 1872384..d73ce2b 100644 --- a/agda/Lambda/ChurchNumerals.agda +++ b/agda/Lambda/ChurchNumerals.agda @@ -21,8 +21,6 @@ iter-tapp-+ : ∀ n m f b → iter-tapp n f (iter-tapp m f b) ≡ iter-tapp (n + 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-* : ∀ n m f b → iter-tapp n () - 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′)