module Combinators where
open import Equality.Propositional.Cubical
open import Prelude hiding (id; if_then_else_; not; const)
open import Tactic.By.Propositional
open import Equality.Decision-procedures equality-with-J
open import H-level.Closure equality-with-J
import Nat equality-with-J as Nat
open import Atom
open import Chi χ-ℕ-atoms
open import Coding χ-ℕ-atoms
open import Constants χ-ℕ-atoms
open import Deterministic χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms
open import Reasoning χ-ℕ-atoms
open import Substitution χ-ℕ-atoms
open import Termination χ-ℕ-atoms
open import Values χ-ℕ-atoms
open χ-atoms χ-ℕ-atoms
import Coding.Instances.Nat
open import Free-variables.Remove-substs
loop : Exp
loop = rec v-x (var v-x)
loop-closed : Closed loop
loop-closed =
Closed′-closed-under-rec $
Closed′-closed-under-var (inj₁ refl)
¬loop⇓ : ¬ Terminates loop
¬loop⇓ (_ , p) = lemma p
where
lemma : ∀ {w} → ¬ loop ⇓ w
lemma (rec p) with v-x V.≟ v-x
... | no x≢x = x≢x refl
... | yes _ = lemma p
id : Exp
id = lambda v-x (var v-x)
id-closed : Closed id
id-closed = from-⊎ (closed? id)
id-correct : ∀ {e v} → e ⇓ v → apply id e ⇓ v
id-correct {e = e} {v = v} e⇓v =
apply id e ⟶⟨ apply lambda e⇓v ⟩
var v-x [ v-x ← v ] ≡⟨ var-step-≡ (refl {x = v-x}) ⟩⟶
v ■⟨ ⇓-Value e⇓v ⟩
private
equal-ℕ′ : Exp
equal-ℕ′ =
rec v-equal (lambda v-m (lambda v-n (case (var v-m) branches)))
module Equal-ℕ where
zero-branches =
branch c-zero [] (const c-true []) ∷
branch c-suc (v-n ∷ []) (const c-false []) ∷
[]
suc-branches =
branch c-zero [] (const c-false []) ∷
branch c-suc (v-n ∷ []) (
apply (apply (var v-equal) (var v-m)) (var v-n)) ∷
[]
branches =
branch c-zero [] (case (var v-n) zero-branches) ∷
branch c-suc (v-m ∷ []) (case (var v-n) suc-branches) ∷
[]
equal-ℕ : Exp → Exp → Exp
equal-ℕ e₁ e₂ = apply (apply equal-ℕ′ e₁) e₂
equal-ℕ-closed :
∀ {xs e₁ e₂} →
Closed′ xs e₁ → Closed′ xs e₂ → Closed′ xs (equal-ℕ e₁ e₂)
equal-ℕ-closed {xs} cl-e₁ cl-e₂ =
Closed′-closed-under-apply
(Closed′-closed-under-apply
(from-⊎ (closed′? equal-ℕ′ xs))
cl-e₁)
cl-e₂
equal-ℕ-correct :
∀ m n →
equal-ℕ ⌜ m ⌝ ⌜ n ⌝ ⇓
⌜ Prelude.if m Nat.≟ n then true else false ⌝
equal-ℕ-correct m n =
equal-ℕ ⌜ m ⌝ ⌜ n ⌝ ≡⟨⟩⟶
apply (apply equal-ℕ′ ⌜ m ⌝) ⌜ n ⌝ ⟶⟨ apply (apply (rec lambda) (rep⇓rep m) lambda) (rep⇓rep n) ⟩
case (⌜ m ⌝ [ v-n ← ⌜ n ⌝ ])
(branches [ v-equal ← equal-ℕ′ ]B⋆
[ v-m ← ⌜ m ⌝ ]B⋆ [ v-n ← ⌜ n ⌝ ]B⋆) ≡⟨ remove-substs [] ⟩⟶
case ⌜ m ⌝
(branches [ v-equal ← equal-ℕ′ ]B⋆
[ v-m ← ⌜ m ⌝ ]B⋆ [ v-n ← ⌜ n ⌝ ]B⋆) ⇓⟨ lemma m n ⟩■
⌜ Prelude.if m Nat.≟ n then true else false ⌝
where
open Equal-ℕ
lemma :
∀ m n →
case ⌜ m ⌝
(branches [ v-equal ← equal-ℕ′ ]B⋆
[ v-m ← ⌜ m ⌝ ]B⋆ [ v-n ← ⌜ n ⌝ ]B⋆)
⇓
⌜ Prelude.if m Nat.≟ n then true else false ⌝
lemma zero zero =
case ⌜ zero ⌝
(branches [ v-equal ← equal-ℕ′ ]B⋆
[ v-m ← ⌜ zero ⌝ ]B⋆ [ v-n ← ⌜ zero ⌝ ]B⋆) ⟶⟨ _⇓_.case (rep⇓rep zero) here [] ⟩
case ⌜ zero ⌝ zero-branches ⇓⟨ case (rep⇓rep zero) here [] (rep⇓rep (true ⦂ Bool)) ⟩■
⌜ true ⦂ Bool ⌝
lemma zero (suc n) =
case ⌜ zero ⌝
(branches [ v-equal ← equal-ℕ′ ]B⋆
[ v-m ← ⌜ zero ⌝ ]B⋆ [ v-n ← ⌜ suc n ⌝ ]B⋆) ⟶⟨ case (rep⇓rep zero) here [] ⟩
case ⌜ suc n ⌝ zero-branches ⇓⟨ case (rep⇓rep (suc n)) (there (λ ()) here) (∷ [])
(rep⇓rep (false ⦂ Bool)) ⟩■
⌜ false ⦂ Bool ⌝
lemma (suc m) zero =
case ⌜ suc m ⌝
(branches [ v-equal ← equal-ℕ′ ]B⋆
[ v-m ← ⌜ suc m ⌝ ]B⋆ [ v-n ← ⌜ zero ⌝ ]B⋆) ⟶⟨ case (rep⇓rep (suc m)) (there (λ ()) here) (∷ []) ⟩
case ⌜ zero ⌝
(suc-branches [ v-equal ← equal-ℕ′ ]B⋆ [ v-m ← ⌜ m ⌝ ]B⋆
[ v-n ← ⌜ zero ⌝ ]B⋆) ⇓⟨ case (rep⇓rep zero) here [] (rep⇓rep (false ⦂ Bool)) ⟩■
⌜ false ⦂ Bool ⌝
lemma (suc m) (suc n) =
case ⌜ suc m ⌝
(branches [ v-equal ← equal-ℕ′ ]B⋆
[ v-m ← ⌜ suc m ⌝ ]B⋆ [ v-n ← ⌜ suc n ⌝ ]B⋆) ⟶⟨ case (rep⇓rep (suc m)) (there (λ ()) here) (∷ []) ⟩
case (⌜ suc n ⌝ [ v-m ← ⌜ m ⌝ ])
(suc-branches [ v-equal ← equal-ℕ′ ]B⋆ [ v-m ← ⌜ m ⌝ ]B⋆
[ v-n ← ⌜ suc n ⌝ ]B⋆) ≡⟨ remove-substs [] ⟩⟶
case ⌜ suc n ⌝
(suc-branches [ v-equal ← equal-ℕ′ ]B⋆ [ v-m ← ⌜ m ⌝ ]B⋆
[ v-n ← ⌜ suc n ⌝ ]B⋆) ⟶⟨ case (rep⇓rep (suc n)) (there (λ ()) here) (∷ []) ⟩
apply (apply equal-ℕ′ (⌜ m ⌝ [ v-n ← ⌜ n ⌝ ])) ⌜ n ⌝ ≡⟨ remove-substs [] ⟩⟶
apply (apply equal-ℕ′ ⌜ m ⌝) ⌜ n ⌝ ≡⟨⟩⟶
equal-ℕ ⌜ m ⌝ ⌜ n ⌝ ⇓⟨ equal-ℕ-correct m n ⟩
⌜ Prelude.if m Nat.≟ n then true else false ⌝ ≡⟨ by lem ⟩⟶
⌜ Prelude.if suc m Nat.≟ suc n then true else false ⌝ ■⟨ rep-value (Prelude.if suc m Nat.≟ suc n then true else false) ⟩
where
lem : Prelude.if m Nat.≟ n then true else false ≡
Prelude.if suc m Nat.≟ suc n then true else false
lem with m Nat.≟ n
... | yes _ = refl
... | no _ = refl
private
equal-ℕ-correct′ :
∀ m n {v} →
equal-ℕ ⌜ m ⌝ ⌜ n ⌝ ⇓ v →
v ≡ ⌜ Prelude.if m Nat.≟ n then true else false ⌝
equal-ℕ-correct′ m n p =
⇓-deterministic p (equal-ℕ-correct m n)
equal-ℕ-correct-ℕ-atoms :
∀ m n →
equal-ℕ ⌜ m ⌝ ⌜ n ⌝ ⇓
⌜ Prelude.if Atoms._≟_ ℕ-atoms m n then true else false ⌝
equal-ℕ-correct-ℕ-atoms m n =
subst
{x = m Nat.≟ n}
{y = Atoms._≟_ ℕ-atoms m n}
(λ (x : Dec (m ≡ n)) →
equal-ℕ ⌜ m ⌝ ⌜ n ⌝ ⇓
⌜ Prelude.if x then true else false ⌝)
(Dec-closure-propositional ext ℕ-set _ _)
(equal-ℕ-correct m n)
private
member′ : Exp
member′ =
lambda v-x body
module Member where
cons-branches =
branch c-true [] (const c-true []) ∷
branch c-false [] (apply (var v-member) (var v-xs)) ∷
[]
branches =
branch c-nil [] (const c-false []) ∷
branch c-cons (v-y ∷ v-xs ∷ []) (
case (equal-ℕ (var v-x) (var v-y))
cons-branches) ∷
[]
body = rec v-member (lambda v-xs (case (var v-xs) branches))
body-closed : ∀ {xs} → Closed′ (v-x ∷ xs) body
body-closed {xs} = from-⊎ (closed′? body (v-x ∷ xs))
member : Exp → Exp → Exp
member m ns = apply (apply member′ m) ns
member-closed :
∀ {xs m ns} →
Closed′ xs m → Closed′ xs ns → Closed′ xs (member m ns)
member-closed cl-m cl-ns =
Closed′-closed-under-apply
(Closed′-closed-under-apply
(Closed′-closed-under-lambda Member.body-closed)
cl-m)
cl-ns
member-correct :
∀ m ns →
member ⌜ m ⌝ ⌜ ns ⌝ ⇓
⌜ Prelude.if V.member m ns then true else false ⌝
member-correct m ns =
member ⌜ m ⌝ ⌜ ns ⌝ ≡⟨⟩⟶
apply (apply member′ ⌜ m ⌝) ⌜ ns ⌝ ⟶⟨ apply (apply lambda (rep⇓rep m) (rec lambda)) (rep⇓rep ns) ⟩
case ⌜ ns ⌝
(branches [ v-x ← ⌜ m ⌝ ]B⋆ [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆) ⇓⟨ lemma ns ⟩■
⌜ Prelude.if V.member m ns then true else false ⌝
where
open Member
lemma :
∀ ns →
case ⌜ ns ⌝ (branches [ v-x ← ⌜ m ⌝ ]B⋆
[ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆)
⇓
⌜ Prelude.if V.member m ns then true else false ⌝
lemma [] =
case ⌜ [] ⦂ List ℕ ⌝
(branches [ v-x ← ⌜ m ⌝ ]B⋆
[ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆) ⇓⟨ case (rep⇓rep ([] ⦂ List ℕ)) here [] (const []) ⟩■
⌜ false ⦂ Bool ⌝
lemma (n ∷ ns) =
case ⌜ n List.∷ ns ⌝
(branches [ v-x ← ⌜ m ⌝ ]B⋆
[ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆) ⟶⟨ case (rep⇓rep (n List.∷ ns)) (there (λ ()) here) (∷ ∷ []) ⟩
case (equal-ℕ (⌜ m ⌝ [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]
[ v-xs ← ⌜ ns ⌝ ] [ v-y ← ⌜ n ⌝ ])
⌜ n ⌝)
(cons-branches [ v-x ← ⌜ m ⌝ ]B⋆
[ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
[ v-xs ← ⌜ ns ⌝ ]B⋆ [ v-y ← ⌜ n ⌝ ]B⋆) ≡⟨ remove-substs [] ⟩⟶
case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
(⟨ cons-branches [ v-x ← ⌜ m ⌝ ]B⋆ ⟩
[ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
[ v-xs ← ⌜ ns ⌝ ]B⋆ [ v-y ← ⌜ n ⌝ ]B⋆) ≡⟨ ⟨by⟩ (subst-∉-B⋆ _ _ ⌜ m ⌝ (from-⊎ (v-x ∈?-B⋆ cons-branches))) ⟩⟶
case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
⟨ cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
[ v-xs ← ⌜ ns ⌝ ]B⋆ [ v-y ← ⌜ n ⌝ ]B⋆ ⟩ ≡⟨ ⟨by⟩ (subst-∉-B⋆ _ _ _
λ { (._ , ._ , ._ , inj₁ refl , const _ () , _)
; (._ , ._ , ._ , inj₂ (inj₁ refl) , y∈FV[body[x←m]ns] , _) →
Closed′-closed-under-apply
(Closed′-closed-under-subst body-closed (rep-closed m))
(rep-closed ns)
v-y (λ ()) y∈FV[body[x←m]ns]
; (_ , _ , _ , (inj₂ (inj₂ ())) , _) }) ⟩⟶
case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
(cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
[ v-xs ← ⌜ ns ⌝ ]B⋆) ⇓⟨ lemma′ (m Nat.≟ n) (equal-ℕ-correct m n) ⟩■
⌜ Prelude.if V.member m (n ∷ ns) then true else false ⌝
where
lemma′ :
(m≟n : Dec (m ≡ n)) →
equal-ℕ ⌜ m ⌝ ⌜ n ⌝
⇓
⌜ Prelude.if m≟n then true else false ⌝ →
case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
(cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
[ v-xs ← ⌜ ns ⌝ ]B⋆)
⇓
⌜ Prelude.if V.member m (n ∷ ns) then true else false ⌝
lemma′ (yes m≡n) hyp =
case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
(cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
[ v-xs ← ⌜ ns ⌝ ]B⋆) ⟶⟨ case hyp here [] ⟩
⌜ true ⦂ Bool ⌝ ≡⟨ cong ⌜_⌝ lem ⟩⟶
⌜ Prelude.if V.member m (n ∷ ns) then true else false ⌝ ■⟨ rep-value (Prelude.if V.member m (n ∷ ns) then true else false) ⟩
where
lem : true ≡ Prelude.if V.member m (n ∷ ns) then true else false
lem with m Nat.≟ n
... | yes _ = refl
... | no m≢n = ⊥-elim (m≢n m≡n)
lemma′ (no m≢n) hyp =
case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
(cons-branches [ v-member ← body′ ]B⋆ [ v-xs ← ⌜ ns ⌝ ]B⋆) ⟶⟨ case hyp (there (λ ()) here) [] ⟩
apply (body′ [ v-xs ← ⌜ ns ⌝ ]) ⌜ ns ⌝ ≡⟨ remove-substs ((body′ , body′-closed) ∷ []) ⟩⟶
apply body′ ⌜ ns ⌝ ⟶⟨ apply (rec lambda) (rep⇓rep ns) ⟩
case ⌜ ns ⌝
(branches [ v-x ← ⌜ m ⌝ ]B⋆
[ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆) ⇓⟨ lemma ns ⟩
⌜ Prelude.if V.member m ns then true else false ⌝ ≡⟨ cong ⌜_⌝ lem ⟩⟶
⌜ Prelude.if V.member m (n ∷ ns) then true else false ⌝ ■⟨ rep-value (Prelude.if V.member m (n ∷ ns) then true else false) ⟩
where
body′ = body [ v-x ← ⌜ m ⌝ ]
body′-closed =
Closed′-closed-under-subst body-closed (rep-closed m)
lem : Prelude.if V.member m ns then true else false ≡
Prelude.if V.member m (n ∷ ns) then true else false
lem with m Nat.≟ n
... | yes m≡n = ⊥-elim (m≢n m≡n)
... | no _ with V.member m ns
... | yes _ = refl
... | no _ = refl
infix 5 if_then_else_
if_then_else_ : Exp → Exp → Exp → Exp
if c then t else f =
case c (branch c-true [] t ∷
branch c-false [] f ∷
[])
if-then-else-closed :
∀ {xs c t f} →
Closed′ xs c → Closed′ xs t → Closed′ xs f →
Closed′ xs (if c then t else f)
if-then-else-closed c-cl t-cl f-cl =
Closed′-closed-under-case
c-cl
λ where
_ (inj₁ refl) → t-cl
_ (inj₂ (inj₁ refl)) → f-cl
if-then-else-correct :
∀ {A : Type} ⦃ cA : Rep A Consts ⦄ {e₁ e₂ e₃}
(b₁ : Bool) (v₂ v₃ : A) →
e₁ ⇓ ⌜ b₁ ⌝ → e₂ ⇓ ⌜ v₂ ⌝ → e₃ ⇓ ⌜ v₃ ⌝ →
if e₁ then e₂ else e₃ ⇓ ⌜ Prelude.if b₁ then v₂ else v₃ ⌝
if-then-else-correct true _ _ e₁⇓ e₂⇓ e₃⇓ = case e₁⇓ here [] e₂⇓
if-then-else-correct false _ _ e₁⇓ e₂⇓ e₃⇓ =
case e₁⇓ (there (λ ()) here) [] e₃⇓
not : Exp → Exp
not e = if e then ⌜ false ⦂ Bool ⌝ else ⌜ true ⦂ Bool ⌝
not-closed : ∀ {xs e} → Closed′ xs e → Closed′ xs (not e)
not-closed cl-e =
if-then-else-closed
cl-e
(Closed→Closed′ (from-⊎ (closed? ⌜ false ⦂ Bool ⌝)))
(Closed→Closed′ (from-⊎ (closed? ⌜ true ⦂ Bool ⌝)))
not-correct : ∀ {e} (b : Bool) → e ⇓ ⌜ b ⌝ → not e ⇓ ⌜ Prelude.not b ⌝
not-correct true e⇓ = case e⇓ here [] (rep⇓rep (false ⦂ Bool))
not-correct false e⇓ =
case e⇓ (there (λ ()) here) [] (rep⇓rep (true ⦂ Bool))
and : Exp → Exp → Exp
and e₁ e₂ = if e₁ then e₂ else ⌜ false ⦂ Bool ⌝
and-closed :
∀ {xs e₁ e₂} → Closed′ xs e₁ → Closed′ xs e₂ → Closed′ xs (and e₁ e₂)
and-closed cl-e₁ cl-e₂ =
if-then-else-closed
cl-e₁
cl-e₂
(Closed→Closed′ (from-⊎ (closed? ⌜ false ⦂ Bool ⌝)))
and-correct :
∀ {e₁ e₂} b₁ b₂ →
e₁ ⇓ ⌜ b₁ ⌝ → e₂ ⇓ ⌜ b₂ ⌝ →
and e₁ e₂ ⇓ ⌜ b₁ ∧ b₂ ⌝
and-correct b₁ b₂ e₁⇓ e₂⇓ =
if-then-else-correct b₁ b₂ false e₁⇓ e₂⇓ (rep⇓rep (false ⦂ Bool))
or : Exp → Exp → Exp
or e₁ e₂ = if e₁ then ⌜ true ⦂ Bool ⌝ else e₂
or-closed :
∀ {xs e₁ e₂} → Closed′ xs e₁ → Closed′ xs e₂ → Closed′ xs (or e₁ e₂)
or-closed cl-e₁ cl-e₂ =
if-then-else-closed
cl-e₁
(Closed→Closed′ (from-⊎ (closed? ⌜ true ⦂ Bool ⌝)))
cl-e₂
or-correct :
∀ {e₁ e₂} b₁ b₂ →
e₁ ⇓ ⌜ b₁ ⌝ → e₂ ⇓ ⌜ b₂ ⌝ →
or e₁ e₂ ⇓ ⌜ b₁ ∨ b₂ ⌝
or-correct b₁ b₂ e₁⇓ e₂⇓ =
if-then-else-correct b₁ true b₂ e₁⇓ (rep⇓rep (true ⦂ Bool)) e₂⇓
equal-Bool : Exp → Exp → Exp
equal-Bool e₁ e₂ =
if e₁ then e₂ else not e₂
equal-Bool-closed :
∀ {xs e₁ e₂} →
Closed′ xs e₁ → Closed′ xs e₂ → Closed′ xs (equal-Bool e₁ e₂)
equal-Bool-closed cl-e₁ cl-e₂ =
if-then-else-closed cl-e₁ cl-e₂ (not-closed cl-e₂)
equal-Bool-correct :
∀ {e₁ e₂} b₁ b₂ →
e₁ ⇓ ⌜ b₁ ⌝ → e₂ ⇓ ⌜ b₂ ⌝ →
equal-Bool e₁ e₂ ⇓ ⌜ Prelude.if b₁ Bool.≟ b₂ then true else false ⌝
equal-Bool-correct {e₁} {e₂} b₁ b₂ e₁⇓ e₂⇓ =
equal-Bool e₁ e₂ ⇓⟨ if-then-else-correct b₁ b₂ (Prelude.not b₂) e₁⇓ e₂⇓ (not-correct b₂ e₂⇓) ⟩
⌜ Prelude.if b₁ then b₂ else Prelude.not b₂ ⌝ ≡⟨ cong ⌜_⌝ (lemma b₁ b₂) ⟩⟶
⌜ Prelude.if b₁ Bool.≟ b₂ then true else false ⌝ ■⟨ rep-value (Prelude.if b₁ Bool.≟ b₂ then true else false) ⟩
where
lemma :
∀ b₁ b₂ →
Prelude.if b₁ then b₂ else Prelude.not b₂ ≡
Prelude.if b₁ Bool.≟ b₂ then true else false
lemma true true = refl
lemma true false = refl
lemma false true = refl
lemma false false = refl
decode-Bool : Exp → Exp
decode-Bool e =
case e
(branch c-const (v-c ∷ v-es ∷ [])
(equal-ℕ (var v-c) ⌜ c-true ⌝) ∷ [])
decode-Bool-closed :
∀ {xs e} → Closed′ xs e → Closed′ xs (decode-Bool e)
decode-Bool-closed cl-e =
Closed′-closed-under-case
cl-e
λ where
_ (inj₁ refl) →
equal-ℕ-closed
(Closed′-closed-under-var
(from-⊎ (V.member v-c (v-c ∷ v-es ∷ _))))
(Closed→Closed′ (rep-closed c-true))
decode-Bool-correct :
∀ {e} (b : Bool) →
e ⇓ ⌜ ⌜ b ⌝ ⦂ Exp ⌝ → decode-Bool e ⇓ ⌜ b ⌝
decode-Bool-correct true e⇓ =
case e⇓ here (∷ ∷ []) (equal-ℕ-correct c-true c-true)
decode-Bool-correct false e⇓ =
case e⇓ here (∷ ∷ []) (equal-ℕ-correct c-false c-true)