bookshelf/Bookshelf/Smullyan/Aviary.lean

245 lines
4.4 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

/-! # Smullyan.Aviary
A collection of combinator birds representable in Lean. Certain duplicators,
e.g. mockingbirds, are not directly expressible since they would require
encoding a signature in which an argument has types `α` *and* `αα`.
Duplicators that are included, e.g. the warbler, are not exactly correct
considering they still have the same limitation described above during actual
use. Their inclusion here serves more as pseudo-documentation than anything.
-/
/-- #### Bald Eagle
`E'xy₁y₂y₃z₁z₂z₃ = x(y₁y₂y₃)(z₁z₂z₃)`
-/
def E' (x : α → β → γ)
(y₁ : δ → ε → α) (y₂ : δ) (y₃ : ε)
(z₁ : ζ → η → β) (z₂ : ζ) (z₃ : η) := x (y₁ y₂ y₃) (z₁ z₂ z₃)
/-- #### Becard
`B₃xyzw = x(y(zw))`
-/
def B₃ (x : α → ε) (y : β → α) (z : γ → β) (w : γ) := x (y (z w))
/-- #### Blackbird
`B₁xyzw = x(yzw)`
-/
def B₁ (x : α → ε) (y : β → γα) (z : β) (w : γ) := x (y z w)
/-- #### Bluebird
`Bxyz = x(yz)`
-/
def B (x : αγ) (y : β → α) (z : β) := x (y z)
/-- #### Bunting
`B₂xyzwv = x(yzwv)`
-/
def B₂ (x : α → ζ) (y : β → γ → ε → α) (z : β) (w : γ) (v : ε) := x (y z w v)
/-- #### Cardinal Once Removed
`C*xyzw = xywz`
-/
def C_star (x : α → β → γ → δ) (y : α) (z : γ) (w : β) := x y w z
notation "C*" => C_star
/-- #### Cardinal
`Cxyz = xzy`
-/
def C (x : α → β → δ) (y : β) (z : α) := x z y
/-- #### Converse Warbler
`W'xy = yxx`
-/
def W' (x : α) (y : αα → β) := y x x
/-- #### Dickcissel
`D₁xyzwv = xyz(wv)`
-/
def D₁ (x : α → β → δ → ε) (y : α) (z : β) (w : γ → δ) (v : γ) := x y z (w v)
/-! #### Double Mockingbird
`M₂xy = xy(xy)`
-/
/-- #### Dove
`Dxyzw = xy(zw)`
-/
def D (x : αγ → δ) (y : α) (z : β → γ) (w : β) := x y (z w)
/-- #### Dovekie
`D₂xyzwv = x(yz)(wv)`
-/
def D₂ (x : α → δ → ε) (y : β → α) (z : β) (w : γ → δ) (v : γ) := x (y z) (w v)
/-- #### Eagle
`Exyzwv = xy(zwv)`
-/
def E (x : α → δ → ε) (y : α) (z : β → γ → δ) (w : β) (v : γ) := x y (z w v)
/-- #### Finch Once Removed
`F*xyzw = xwzy`
-/
def F_star (x : α → β → γ → δ) (y : γ) (z : β) (w : α) := x w z y
notation "F*" => F_star
/-- #### Finch
`Fxyz = zyx`
-/
def F (x : α) (y : β) (z : β → αγ) := z y x
/-- #### Goldfinch
`Gxyzw = xw(yz)`
-/
def G (x : αγ → δ) (y : β → γ) (z : β) (w : α) := x w (y z)
/-- #### Hummingbird
`Hxyz = xyzy`
-/
def H (x : α → β → αγ) (y : α) (z : β) := x y z y
/-- #### Identity Bird
`Ix = x`
-/
def I (x : α) : α := x
/-- #### Kestrel
`Kxy = x`
-/
def K (x : α) (_ : β) := x
/-! #### Lark
`Lxy = x(yy)`
-/
/-! #### Mockingbird
`Mx = xx`
-/
/-- #### Owl
`Oxy = y(xy)`
-/
def O (x : (α → β) → α) (y : α → β) := y (x y)
/-- #### Phoenix
`Φxyzw = x(yw)(zw)`
-/
def Φ (x : β → γ → δ) (y : α → β) (z : αγ) (w : α) := x (y w) (z w)
/-- #### Psi Bird
`Ψxyzw = x(yz)(yw)`
-/
def Ψ (x : ααγ) (y : β → α) (z : β) (w : β) := x (y z) (y w)
/-- #### Quacky Bird
`Q₄xyz = z(yx)`
-/
def Q₄ (x : α) (y : α → β) (z : β → γ) := z (y x)
/-- #### Queer Bird
`Qxyz = y(xz)`
-/
def Q (x : α → β) (y : β → γ) (z : α) := y (x z)
/-- #### Quirky Bird
`Q₃xyz = z(xy)`
-/
def Q₃ (x : α → β) (y : α) (z : β → γ) := z (x y)
/-- #### Quixotic Bird
`Q₁xyz = x(zy)`
-/
def Q₁ (x : αγ) (y : β) (z : β → α) := x (z y)
/-- #### Quizzical Bird
`Q₂xyz = y(zx)`
-/
def Q₂ (x : α) (y : β → γ) (z : α → β) := y (z x)
/-- #### Robin Once Removed
`R*xyzw = xzwy`
-/
def R_star (x : α → β → γ → δ) (y : γ) (z : α) (w : β) := x z w y
notation "R*" => R_star
/-- #### Robin
`Rxyz = yzx`
-/
def R (x : α) (y : β → αγ) (z : β) := y z x
/-- #### Sage Bird
`Θx = x(Θx)`
-/
partial def Θ [Inhabited α] (x : αα) := x (Θ x)
/-- #### Starling
`Sxyz = xz(yz)`
-/
def S (x : α → β → γ) (y : α → β) (z : α) := x z (y z)
/-- #### Thrush
`Txy = yx`
-/
def T (x : α) (y : α → β) := y x
/-! #### Turing Bird
`Uxy = y(xxy)`
-/
/-- #### Vireo Once Removed
`V*xyzw = xwyz`
-/
def V_star (x : α → β → γ → δ) (y : β) (z : γ) (w : α) := x w y z
notation "V*" => V_star
/-- #### Vireo
`Vxyz = zxy`
-/
def V (x : α) (y : β) (z : α → β → γ) := z x y
/-- #### Warbler
`Wxy = xyy`
-/
def W (x : αα → β) (y : α) := x y y