Package map-reduce-bit3x3: Correctness proof for the map reduce 3x3 bit matrix example

Information

name	map-reduce-bit3x3
version	1.1
description	Correctness proof for the map reduce 3x3 bit matrix example
author	Joe Hurd <joe@gilith.com>
license	MIT
requires	base
show	Data.Bool Data.List Data.Pair

Files

Package tarball map-reduce-bit3x3-1.1.tgz
Theory file map-reduce-bit3x3.thy (included in the package tarball)

Defined Constants

Bit
- Bit.*
- Bit.+
Bit3
- Bit3.dot
Bit3x3
- Bit3x3.*
- Bit3x3.identity
- Bit3x3.product

Theorems

⊦ Bit3x3.product = foldl Bit3x3.* Bit3x3.identity

⊦ ∀a b. Bit.* a b ⇔ a ∧ b

⊦ ∀a b. Bit.+ a b ⇔ ¬(a ⇔ b)

⊦ ∀l₁ l₂.
Bit3x3.product (l₁ @ l₂) =
Bit3x3.* (Bit3x3.product l₁) (Bit3x3.product l₂)

⊦ Bit3x3.identity = ((⊤, ⊥, ⊥), (⊥, ⊤, ⊥), ⊥, ⊥, ⊤)

⊦ ∀a₁ a₂ a₃ b₁ b₂ b₃.
Bit3.dot (a₁, a₂, a₃) (b₁, b₂, b₃) ⇔
Bit.+ (Bit.* a₁ b₁) (Bit.+ (Bit.* a₂ b₂) (Bit.* a₃ b₃))

⊦ ∀a.
∃a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃.
a = ((a₁₁, a₁₂, a₁₃), (a₂₁, a₂₂, a₂₃), a₃₁, a₃₂, a₃₃)

⊦ ∀a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃.
    Bit3x3.* ((a₁₁, a₁₂, a₁₃), (a₂₁, a₂₂, a₂₃), a₃₁, a₃₂, a₃₃)
      ((b₁₁, b₁₂, b₁₃), (b₂₁, b₂₂, b₂₃), b₃₁, b₃₂, b₃₃) =
    ((Bit3.dot (a₁₁, a₁₂, a₁₃) (b₁₁, b₂₁, b₃₁),
      Bit3.dot (a₁₁, a₁₂, a₁₃) (b₁₂, b₂₂, b₃₂),
      Bit3.dot (a₁₁, a₁₂, a₁₃) (b₁₃, b₂₃, b₃₃)),
     (Bit3.dot (a₂₁, a₂₂, a₂₃) (b₁₁, b₂₁, b₃₁),
      Bit3.dot (a₂₁, a₂₂, a₂₃) (b₁₂, b₂₂, b₃₂),
      Bit3.dot (a₂₁, a₂₂, a₂₃) (b₁₃, b₂₃, b₃₃)),
     Bit3.dot (a₃₁, a₃₂, a₃₃) (b₁₁, b₂₁, b₃₁),
     Bit3.dot (a₃₁, a₃₂, a₃₃) (b₁₂, b₂₂, b₃₂),
     Bit3.dot (a₃₁, a₃₂, a₃₃) (b₁₃, b₂₃, b₃₃))

Input Type Operators

→
bool
Data
- List
  - list
- Pair
  - ×

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - ⊥
  - ⊤
- List
  - @
  - foldl
- Pair
  - ,
  - fst
  - snd

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ∀t. t ⇒ t

⊦ ∀a. ∃x. x = a

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊥ ⇔ ⊥

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀x y. fst (x, y) = x

⊦ ∀x y. snd (x, y) = y

⊦ ∀p. ∃x y. p = (x, y)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀t₁ t₂. t₁ ∧ t₂ ⇔ t₂ ∧ t₁

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀p a. (∃x. a = x ∧ p x) ⇔ p a

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀p q. (∃x. p x) ⇒ q ⇔ ∀x. p x ⇒ q

⊦ ∀t₁ t₂ t₃. (t₁ ∧ t₂) ∧ t₃ ⇔ t₁ ∧ t₂ ∧ t₃

⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b

⊦ ∀g f b l₁ l₂.
(∀s. g s b = s) ∧ (∀s₁ s₂ x. g s₁ (f s₂ x) = f (g s₁ s₂) x) ⇒
foldl f b (l₁ @ l₂) = g (foldl f b l₁) (foldl f b l₂)