PCF.Checks
{-# OPTIONS --rewriting --confluence-check #-} open import Agda.Builtin.Equality open import Agda.Builtin.Equality.Rewrite module PCF.Checks where open import Data.Bool.Base open import Agda.Builtin.Nat open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) open import PCF.Domain-Notation open import PCF.Types open import PCF.Constants open import PCF.Variables open import PCF.Environments open import PCF.Terms postulate {-# REWRITE fix-app elim-♯-η elim-♯-⊥ true-cond false-cond #-} -- Constants pattern 𝑁 n = 𝐿 (k n) pattern succ = 𝐿 +1′ pattern pred⊥ = 𝐿 -1′ pattern if = 𝐿 ⊃ᵢ pattern 𝑌 = 𝐿 Y pattern 𝑍 = 𝐿 Z -- Variables f = var 0 ι g = var 1 (ι ⇒ ι) h = var 2 (ι ⇒ ι ⇒ ι) a = var 3 ι b = var 4 ι -- Arithmetic check-41+1 : 𝒜′⟦ succ ␣ 𝑁 41 ⟧ ρ⊥ ≡ η 42 check-41+1 = refl check-43-1 : 𝒜′⟦ pred⊥ ␣ 𝑁 43 ⟧ ρ⊥ ≡ η 42 check-43-1 = refl -- Binding check-id : 𝒜′⟦ (ƛ a ␣ 𝑉 a) ␣ 𝑁 42 ⟧ ρ⊥ ≡ η 42 check-id = refl check-k : 𝒜′⟦ (ƛ a ␣ ƛ b ␣ 𝑉 a) ␣ 𝑁 42 ␣ 𝑁 41 ⟧ ρ⊥ ≡ η 42 check-k = refl check-ki : 𝒜′⟦ (ƛ a ␣ ƛ b ␣ 𝑉 b) ␣ 𝑁 41 ␣ 𝑁 42 ⟧ ρ⊥ ≡ η 42 check-ki = refl
\clearpage
check-suc-41 : 𝒜′⟦ (ƛ a ␣ (succ ␣ 𝑉 a )) ␣ 𝑁 41 ⟧ ρ⊥ ≡ η 42 check-suc-41 = refl check-pred-42 : 𝒜′⟦ (ƛ a ␣ (pred⊥ ␣ 𝑉 a)) ␣ 𝑁 43 ⟧ ρ⊥ ≡ η 42 check-pred-42 = refl check-if-zero : 𝒜′⟦ if ␣ (𝑍 ␣ 𝑁 0) ␣ 𝑁 42 ␣ 𝑁 0 ⟧ ρ⊥ ≡ η 42 check-if-zero = refl check-if-nonzero : 𝒜′⟦ if ␣ (𝑍 ␣ 𝑁 42) ␣ 𝑁 0 ␣ 𝑁 42 ⟧ ρ⊥ ≡ η 42 check-if-nonzero = refl -- fix (λf. 42) ≡ 42 check-fix-const : 𝒜′⟦ 𝑌 ␣ (ƛ f ␣ 𝑁 42) ⟧ ρ⊥ ≡ η 42 check-fix-const = fix-fix (λ x → η 42) -- fix (λg. λa. 42) 2 ≡ 42 check-fix-lambda : 𝒜′⟦ 𝑌 ␣ (ƛ g ␣ ƛ a ␣ 𝑁 42) ␣ 𝑁 2 ⟧ ρ⊥ ≡ η 42 check-fix-lambda = refl -- fix (λg. λa. ifz a then 42 else g (pred a)) 101 ≡ 42 check-countdown : 𝒜′⟦ 𝑌 ␣ (ƛ g ␣ ƛ a ␣ (if ␣ (𝑍 ␣ 𝑉 a) ␣ 𝑁 42 ␣ (𝑉 g ␣ (pred⊥ ␣ 𝑉 a)))) ␣ 𝑁 101 ⟧ ρ⊥ ≡ η 42 check-countdown = refl -- fix (λh. λa. λb. ifz a then b else h (pred a) (succ b)) 4 38 ≡ 42 check-sum-42 : 𝒜′⟦ (𝑌 ␣ (ƛ h ␣ ƛ a ␣ ƛ b ␣ (if ␣ (𝑍 ␣ 𝑉 a) ␣ 𝑉 b ␣ (𝑉 h ␣ (pred⊥ ␣ 𝑉 a) ␣ (succ ␣ 𝑉 b))))) ␣ 𝑁 4 ␣ 𝑁 38 ⟧ ρ⊥ ≡ η 42 check-sum-42 = refl -- Exponential in first arg?