bookshelf/Common/LTuple/Basic.lean

277 lines
7.5 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.

import Mathlib.Tactic.Ring
/-! # Common.LTuple.Basic
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:
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.
In general, prefer using `Prod` over `LTuple`. This exists primarily to solve
certain theorems outlined in [^1].
[^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..
-/
inductive LTuple : (α : Type u) → (size : Nat) → Type u where
| nil : LTuple α 0
| snoc : LTuple α n → α → LTuple α (n + 1)
namespace LTuple
/-! ## 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)
/-! ### Equality -/
/--
Two values `a` and `b` are equal **iff** `[a] = [b]`.
-/
theorem eq_iff_singleton : (a = b) ↔ (snoc a nil = snoc b nil) := by
apply Iff.intro
· intro h; rw [h]
· intro h; injection h
/--
Two lists are equal **iff** their heads and tails are equal.
-/
theorem eq_iff_snoc {t₁ t₂ : LTuple α n}
: (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₁
/--
Implements decidable equality for `Tuple α m`, provided `a` has decidable
equality.
-/
protected def hasDecEq [DecidableEq α] (t₁ t₂ : LTuple α n)
: Decidable (Eq t₁ t₂) :=
match t₁, t₂ with
| nil, nil => isTrue rfl
| snoc as a, snoc bs b =>
match LTuple.hasDecEq as bs with
| 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
/-! ## Basic API -/
/--
Returns the number of entries in an `LTuple`.
-/
def size (_ : LTuple α n) : Nat := n
/--
Returns all but the last entry of an `LTuple`.
-/
def init : (t : LTuple α (n + 1)) → LTuple α n
| snoc vs _ => vs
/--
Returns the last entry of an `LTuple`.
-/
def last : LTuple α (n + 1) → α
| snoc _ v => v
/--
Prepends an entry to an `LTuple`.
-/
def cons : LTuple α n → α → LTuple α (n + 1)
| nil, a => snoc nil a
| snoc ts t, a => snoc (cons ts a) t
/-! ## Concatenation -/
/--
Joins two `LTuple`s together end to end.
-/
def concat : LTuple α m → LTuple α n → LTuple α (m + n)
| is, nil => is
| is, snoc ts t => snoc (concat is ts) t
/--
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
/--
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 =>
unfold concat
rw [ih]
suffices HEq (snoc (cast (_ : LTuple α n = LTuple α (0 + n)) as) a) ↑(snoc as a)
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)
(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)
(cast h (snoc as a)))
(show LTuple α (n + 1) = LTuple α (0 + (n + 1)) by simp)
h₁
/--
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
/--
`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
/-! ## Initial Sequences -/
/--
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))]
/--
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
/--
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)
/--
Taking `n` entries from an `LTuple` of size `n` should yield the same `LTuple`.
-/
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
/--
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
/--
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
cases t with
| snoc as a =>
unfold init take
simp
rw [self_take_size_eq_self]
simp
/--
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}
: (t₁ = t₂) → (t₁.take k = t₂.take k) := by
intro h
rw [h]
/--
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
| nil =>
simp
rw [self_concat_nil_eq_self, self_take_size_eq_self]
| @snoc n' as a ih =>
simp
rw [concat_snoc_snoc_concat]
unfold take
simp
rw [ih]
simp
end LTuple