bookshelf/Common/LTuple/Basic.lean

277 lines
7.5 KiB
Plaintext
Raw Normal View History

2023-02-21 21:42:58 +00:00
import Mathlib.Tactic.Ring
2023-05-08 19:37:02 +00:00
/-! # Common.LTuple.Basic
2023-05-04 22:37:54 +00:00
The following is a representation of a (possibly empty) left-biased tuple. A
left-biased `n`-tuple is defined recursively as follows:
```
⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩
```
Note a `Tuple` exists in Lean already. This implementation differs in two
notable ways:
2023-02-21 21:42:58 +00:00
2023-05-04 22:37:54 +00:00
1. It is left-associative. The built-in `Tuple` instance evaluates e.g.
`(x₁, x₂, x₃)` as `(x₁, (x₂, x₃))` instead of `((x₁, x₂), x₃)`.
2. Internally, the built-in `Tuple` instance is syntactic sugar for nested
`Prod` instances. Unlike this implementation, an `LTuple` is a homogeneous
collection.
2023-02-21 21:42:58 +00:00
2023-05-04 22:37:54 +00:00
In general, prefer using `Prod` over `LTuple`. This exists primarily to solve
certain theorems outlined in [^1].
2023-05-04 22:37:54 +00:00
[^1]: Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San
Diego: Harcourt/Academic Press, 2001.
-/
/--
#### LTuple
A left-biased, possibly empty, homogeneous `Tuple`-like structure..
2023-02-21 21:42:58 +00:00
-/
inductive LTuple : (α : Type u) → (size : Nat) → Type u where
| nil : LTuple α 0
| snoc : LTuple α n → α → LTuple α (n + 1)
2023-02-21 21:42:58 +00:00
namespace LTuple
2023-02-21 21:42:58 +00:00
2023-05-04 22:37:54 +00:00
/-! ## Coercions -/
scoped instance : CoeOut (LTuple α (min (m + n) m)) (LTuple α m) where
coe := cast (by simp)
scoped instance : Coe (LTuple α 0) (LTuple α (min n 0)) where
coe := cast (by rw [Nat.min_zero])
scoped instance : Coe (LTuple α 0) (LTuple α (min 0 n)) where
coe := cast (by rw [Nat.zero_min])
scoped instance : Coe (LTuple α n) (LTuple α (min n n)) where
coe := cast (by simp)
scoped instance : Coe (LTuple α n) (LTuple α (0 + n)) where
coe := cast (by simp)
scoped instance : Coe (LTuple α (min m n + 1)) (LTuple α (min (m + 1) (n + 1))) where
coe := cast (by rw [Nat.min_succ_succ])
scoped instance : Coe (LTuple α m) (LTuple α (min (m + n) m)) where
coe := cast (by simp)
2023-05-04 22:37:54 +00:00
/-! ### Equality -/
2023-02-21 21:42:58 +00:00
2023-05-04 22:37:54 +00:00
/--
Two values `a` and `b` are equal **iff** `[a] = [b]`.
-/
theorem eq_iff_singleton : (a = b) ↔ (snoc a nil = snoc b nil) := by
2023-02-21 21:42:58 +00:00
apply Iff.intro
· intro h; rw [h]
· intro h; injection h
2023-05-04 22:37:54 +00:00
/--
Two lists are equal **iff** their heads and tails are equal.
-/
theorem eq_iff_snoc {t₁ t₂ : LTuple α n}
2023-02-21 21:42:58 +00:00
: (a = b ∧ t₁ = t₂) ↔ (snoc t₁ a = snoc t₂ b) := by
apply Iff.intro
· intro ⟨h₁, h₂ ⟩; rw [h₁, h₂]
· intro h
injection h with _ h₁ h₂
exact And.intro h₂ h₁
/--
2023-04-10 21:30:29 +00:00
Implements decidable equality for `Tuple α m`, provided `a` has decidable
equality.
2023-02-21 21:42:58 +00:00
-/
protected def hasDecEq [DecidableEq α] (t₁ t₂ : LTuple α n)
: Decidable (Eq t₁ t₂) :=
2023-02-21 21:42:58 +00:00
match t₁, t₂ with
2023-05-04 22:37:54 +00:00
| nil, nil => isTrue rfl
2023-02-21 21:42:58 +00:00
| snoc as a, snoc bs b =>
match LTuple.hasDecEq as bs with
2023-02-21 21:42:58 +00:00
| isFalse np => isFalse (fun h => absurd (eq_iff_snoc.mpr h).right np)
| isTrue hp =>
if hq : a = b then
isTrue (eq_iff_snoc.mp $ And.intro hq hp)
else
isFalse (fun h => absurd (eq_iff_snoc.mpr h).left hq)
instance [DecidableEq α] : DecidableEq (LTuple α n) := LTuple.hasDecEq
2023-02-21 21:42:58 +00:00
2023-05-04 22:37:54 +00:00
/-! ## Basic API -/
2023-02-21 21:42:58 +00:00
/--
2023-05-04 22:37:54 +00:00
Returns the number of entries in an `LTuple`.
2023-02-21 21:42:58 +00:00
-/
def size (_ : LTuple α n) : Nat := n
2023-02-21 21:42:58 +00:00
/--
2023-05-04 22:37:54 +00:00
Returns all but the last entry of an `LTuple`.
2023-02-21 21:42:58 +00:00
-/
def init : (t : LTuple α (n + 1)) → LTuple α n
| snoc vs _ => vs
2023-02-21 21:42:58 +00:00
/--
2023-05-04 22:37:54 +00:00
Returns the last entry of an `LTuple`.
2023-02-21 21:42:58 +00:00
-/
def last : LTuple α (n + 1) → α
| snoc _ v => v
2023-02-21 21:42:58 +00:00
/--
2023-05-04 22:37:54 +00:00
Prepends an entry to an `LTuple`.
2023-02-21 21:42:58 +00:00
-/
def cons : LTuple α n → α → LTuple α (n + 1)
| nil, a => snoc nil a
2023-02-21 21:42:58 +00:00
| snoc ts t, a => snoc (cons ts a) t
2023-05-04 22:37:54 +00:00
/-! ## Concatenation -/
2023-02-21 21:42:58 +00:00
/--
2023-05-04 22:37:54 +00:00
Joins two `LTuple`s together end to end.
2023-02-21 21:42:58 +00:00
-/
def concat : LTuple α m → LTuple α n → LTuple α (m + n)
| is, nil => is
2023-02-21 21:42:58 +00:00
| is, snoc ts t => snoc (concat is ts) t
/--
2023-05-04 22:37:54 +00:00
Concatenating an `LTuple` with `nil` yields the original `LTuple`.
-/
theorem self_concat_nil_eq_self (t : LTuple α m) : concat t nil = t :=
match t with
| nil => rfl
| snoc _ _ => rfl
/--
2023-05-04 22:37:54 +00:00
Concatenating `nil` with an `LTuple` yields the original `LTuple`.
-/
theorem nil_concat_self_eq_self (t : LTuple α m) : concat nil t = t := by
induction t with
| nil => unfold concat; simp
| @snoc n as a ih =>
2023-04-10 21:30:29 +00:00
unfold concat
rw [ih]
suffices HEq (snoc (cast (_ : LTuple α n = LTuple α (0 + n)) as) a) ↑(snoc as a)
2023-04-10 21:30:29 +00:00
from eq_of_heq this
have h₁ := Eq.recOn
(motive := fun x h => HEq
(snoc (cast (show LTuple α n = LTuple α x by rw [h]) as) a)
2023-04-10 21:30:29 +00:00
(snoc as a))
(show n = 0 + n by simp)
HEq.rfl
exact Eq.recOn
(motive := fun x h => HEq
(snoc (cast (_ : LTuple α n = LTuple α (0 + n)) as) a)
2023-04-10 21:30:29 +00:00
(cast h (snoc as a)))
(show LTuple α (n + 1) = LTuple α (0 + (n + 1)) by simp)
2023-04-10 21:30:29 +00:00
h₁
/--
2023-05-04 22:37:54 +00:00
Concatenating an `LTuple` to a nonempty `LTuple` moves `concat` calls closer to
the expression leaves.
-/
theorem concat_snoc_snoc_concat {bs : LTuple α n}
: concat as (snoc bs b) = snoc (concat as bs) b :=
rfl
/--
2023-05-04 22:37:54 +00:00
`snoc` is equivalent to concatenating the `init` and `last` elements of an
`LTuple` together.
-/
theorem snoc_eq_init_concat_last (as : LTuple α m)
: snoc as a = concat as (snoc nil a) := by
cases as with
| nil => rfl
| snoc _ _ => simp; unfold concat concat; rfl
2023-05-04 22:37:54 +00:00
/-! ## Initial Sequences -/
/--
2023-05-04 22:37:54 +00:00
Takes the first `k` entries from an `LTuple` to form a new `LTuple`, or the
entire `LTuple` if `k` exceeds the size.
-/
def take (t : LTuple α n) (k : Nat) : LTuple α (min n k) :=
if h : n ≤ k then
cast (by rw [min_eq_left h]) t
else
match t with
| nil => nil
| @snoc _ n' as a => cast (by rw [min_lt_succ_eq h]) (take as k)
where
min_lt_succ_eq {m : Nat} (h : ¬m + 1 ≤ k) : min m k = min (m + 1) k := by
have h' : k + 1 ≤ m + 1 := Nat.lt_of_not_le h
simp at h'
rw [min_eq_right h', min_eq_right (Nat.le_trans h' (Nat.le_succ m))]
/--
2023-05-04 22:37:54 +00:00
Taking no entries from any `LTuple` should yield an empty `LTuple`.
-/
theorem self_take_zero_eq_nil (t : LTuple α n) : take t 0 = @nil α := by
induction t with
| nil => simp; rfl
| snoc as a ih => unfold take; simp; rw [ih]; simp
/--
2023-05-04 22:37:54 +00:00
Taking any number of entries from an empty `LTuple` should yield an empty
`LTuple`.
-/
theorem nil_take_zero_eq_nil (k : Nat) : (take (@nil α) k) = @nil α := by
cases k <;> (unfold take; simp)
/--
2023-05-04 22:37:54 +00:00
Taking `n` entries from an `LTuple` of size `n` should yield the same `LTuple`.
2023-02-21 21:42:58 +00:00
-/
theorem self_take_size_eq_self (t : LTuple α n) : take t n = t := by
cases t with
| nil => simp; rfl
| snoc as a => unfold take; simp
/--
2023-05-04 22:37:54 +00:00
Taking `n - 1` elements from an `LTuple` of size `n` yields the same result,
regardless of the last entry's value.
-/
theorem take_subst_last {as : LTuple α n} (a₁ a₂ : α)
: take (snoc as a₁) n = take (snoc as a₂) n := by
unfold take
simp
/--
2023-05-04 22:37:54 +00:00
Taking `n` elements from an `LTuple` of size `n + 1` is the same as invoking
`init`.
-/
theorem init_eq_take_pred (t : LTuple α (n + 1)) : take t n = init t := by
2023-04-10 21:30:29 +00:00
cases t with
| snoc as a =>
unfold init take
simp
rw [self_take_size_eq_self]
simp
/--
2023-05-04 22:37:54 +00:00
If two `LTuple`s are equal, then any initial sequences of these two `LTuple`s
are also equal.
-/
theorem eq_tuple_eq_take {t₁ t₂ : LTuple α n}
2023-04-10 21:30:29 +00:00
: (t₁ = t₂) → (t₁.take k = t₂.take k) := by
intro h
rw [h]
/--
2023-05-04 22:37:54 +00:00
Given an `LTuple` of size `k`, concatenating an arbitrary `LTuple` and taking
`k` elements yields the original `LTuple`.
-/
theorem eq_take_concat {t₁ : LTuple α m} {t₂ : LTuple α n}
: take (concat t₁ t₂) m = t₁ := by
induction t₂ with
2023-04-10 21:30:29 +00:00
| nil =>
simp
rw [self_concat_nil_eq_self, self_take_size_eq_self]
| @snoc n' as a ih =>
2023-04-10 21:30:29 +00:00
simp
rw [concat_snoc_snoc_concat]
unfold take
simp
rw [ih]
simp
2023-02-21 21:42:58 +00:00
2023-05-04 22:37:54 +00:00
end LTuple