`lean/SpectreKnot/Basic.lean`

52 lines · 10 declarations, each with its own page · on GitHub · hide comments

Basic types and helpers. No Mathlib: everything here is core Lean.

All 39 files, and the declarations of this one

1/-

2Basic types and helpers. No Mathlib: everything here is core Lean.

3-/

5namespace SpectreKnot

7/-- The nine kinds of supertile (paper §2.2). -/

8inductive Kind where

9 | Gamma | Delta | Theta | Lambda | Xi | Pi | Sigma | Phi | Psi

10 deriving DecidableEq, Repr

12/-- The eight letters of the edge labels of [SMKGS-spectre, Fig. 4.2], signs ignored (paper §6.1). -/

13inductive Letter where

15 deriving DecidableEq, Repr

17/-- `iter f n x = f (f (... (f x)))`, `n` times. (Core Lean has no `f^[n]`.) -/

18def iter {α : Type} (f : α → α) : Nat → α → α

19 | 0, x => x

20 | n + 1, x => f (iter f n x)

22/-- Zero steps leave `x` where it is. -/

23@[simp] theorem iter_zero {α : Type} (f : α → α) (x : α) : iter f 0 x = x := rfl

25/-- `n + 1` steps are `n` steps, then one more application of `f`. -/

26theorem iter_succ {α : Type} (f : α → α) (n : Nat) (x : α) : iter f (n + 1) x = f (iter f n x) := rfl

28/-- The extra step can also be taken first: `n + 1` steps from `x` are `n` steps from `f x`. -/

29theorem iter_succ' {α : Type} (f : α → α) (n : Nat) (x : α) : iter f (n + 1) x = iter f n (f x) := by

30 induction n with

31 | zero => rfl

32 | succ n ih => rw [iter_succ, ih, iter_succ]

34/-- `m + n` steps are `n` steps followed by `m` steps. -/

35theorem iter_add {α : Type} (f : α → α) (m n : Nat) (x : α) : iter f (m + n) x = iter f m (iter f n x) := by

36 induction m with

37 | zero => simp

38 | succ m ih => rw [Nat.add_right_comm, iter_succ, ih, iter_succ]

40/-- Cyclic successor on `0 … E-1`. -/

41def nxt (E x : Nat) : Nat := if x + 1 = E then 0 else x + 1

43/-- Cyclic predecessor on `0 … E-1`. -/

44def prv (E x : Nat) : Nat := if x = 0 then E - 1 else x - 1

46/-- The Fibonacci numbers, `fib 1 = fib 2 = 1`. -/

47def fib : Nat → Nat

48 | 0 => 0

49 | 1 => 1

50 | n + 2 => fib n + fib (n + 1)

52end SpectreKnot