Remove the concept of an `LTuple`.
parent
e1af33e805
commit
708295f53f
|
|
@ -29,7 +29,7 @@ Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$.
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
|
|
||||||
\lean{Bookshelf/Enderton/Chapter\_0}{Enderton.Chapter\_0.lemma\_0a}
|
TODO
|
||||||
|
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,3 @@
|
||||||
import Common.LTuple.Basic
|
|
||||||
|
|
||||||
/-! # Enderton.Chapter_0
|
/-! # Enderton.Chapter_0
|
||||||
|
|
||||||
Useful Facts About Sets
|
Useful Facts About Sets
|
||||||
|
|
@ -7,272 +5,6 @@ Useful Facts About Sets
|
||||||
|
|
||||||
namespace Enderton.Chapter_0
|
namespace Enderton.Chapter_0
|
||||||
|
|
||||||
/--
|
-- TODO
|
||||||
The following describes a so-called "generic" tuple. Like an `LTuple`, a generic
|
|
||||||
`n`-tuple is defined recursively like so:
|
|
||||||
|
|
||||||
`⟨x₁, ..., xₙ⟩ = ⟨⟨x₁, ..., xₙ₋₁⟩, xₙ⟩`
|
|
||||||
|
|
||||||
Unlike `LTuple`, this tuple bends the syntax above further. For example,
|
|
||||||
both tuples above are equivalent to:
|
|
||||||
|
|
||||||
`⟨⟨x₁, ..., xₘ⟩, xₘ₊₁, ..., xₙ⟩`
|
|
||||||
|
|
||||||
for some `1 ≤ m ≤ n`. This distinction is purely syntactic, and introduced
|
|
||||||
solely to prove `lemma_0a`. In other words, `LTuple` is an always-normalized
|
|
||||||
variant of an `GTuple`. In general, prefer it over this when working within
|
|
||||||
Enderton's book.
|
|
||||||
-/
|
|
||||||
inductive GTuple : (α : Type u) → (size : Nat × Nat) → Type u where
|
|
||||||
| nil : GTuple α (0, 0)
|
|
||||||
| snoc : GTuple α (p, q) → LTuple α r → GTuple α (p + q, r)
|
|
||||||
|
|
||||||
syntax (priority := high) "t[" term,* "]" : term
|
|
||||||
|
|
||||||
macro_rules
|
|
||||||
| `(t[]) => `(LTuple.nil)
|
|
||||||
| `(t[$x]) => `(LTuple.snoc t[] $x)
|
|
||||||
| `(t[$xs:term,*, $x]) => `(LTuple.snoc t[$xs,*] $x)
|
|
||||||
|
|
||||||
syntax (priority := high) "g[" term,* "]" : term
|
|
||||||
|
|
||||||
macro_rules
|
|
||||||
| `(g[]) => `(GTuple.nil)
|
|
||||||
| `(g[$x]) => `(GTuple.snoc g[] t[$x])
|
|
||||||
| `(g[g[$xs:term,*], $ys:term,*]) => `(GTuple.snoc g[$xs,*] t[$ys,*])
|
|
||||||
| `(g[$x, $xs:term,*]) => `(GTuple.snoc g[] t[$x, $xs,*])
|
|
||||||
|
|
||||||
namespace GTuple
|
|
||||||
|
|
||||||
open scoped LTuple
|
|
||||||
|
|
||||||
/-! ## Normalization -/
|
|
||||||
|
|
||||||
/--
|
|
||||||
Converts an `GTuple` into "normal form".
|
|
||||||
-/
|
|
||||||
def norm : GTuple α (m, n) → LTuple α (m + n)
|
|
||||||
| g[] => t[]
|
|
||||||
| snoc is ts => LTuple.concat is.norm ts
|
|
||||||
|
|
||||||
/--
|
|
||||||
Normalization of an empty `GTuple` yields an empty `Tuple`.
|
|
||||||
-/
|
|
||||||
theorem norm_nil_eq_nil : @norm α 0 0 nil = LTuple.nil :=
|
|
||||||
rfl
|
|
||||||
|
|
||||||
/--
|
|
||||||
Normalization of a pseudo-empty `GTuple` yields an empty `Tuple`.
|
|
||||||
-/
|
|
||||||
theorem norm_snoc_nil_nil_eq_nil : @norm α 0 0 (snoc g[] t[]) = t[] := by
|
|
||||||
unfold norm norm
|
|
||||||
rfl
|
|
||||||
|
|
||||||
/--
|
|
||||||
Normalization elimates `snoc` when the `snd` component is `nil`.
|
|
||||||
-/
|
|
||||||
theorem norm_snoc_nil_elim {t : GTuple α (p, q)}
|
|
||||||
: norm (snoc t t[]) = norm t := by
|
|
||||||
cases t with
|
|
||||||
| nil => simp; unfold norm norm; rfl
|
|
||||||
| snoc tf tl =>
|
|
||||||
simp
|
|
||||||
conv => lhs; unfold norm
|
|
||||||
|
|
||||||
/--
|
|
||||||
Normalization eliminates `snoc` when the `fst` component is `nil`.
|
|
||||||
-/
|
|
||||||
theorem norm_nil_snoc_elim {ts : LTuple α n}
|
|
||||||
: norm (snoc g[] ts) = cast (by simp) ts := by
|
|
||||||
unfold norm norm
|
|
||||||
rw [LTuple.nil_concat_self_eq_self]
|
|
||||||
|
|
||||||
/--
|
|
||||||
Normalization distributes across `Tuple.snoc` calls.
|
|
||||||
-/
|
|
||||||
theorem norm_snoc_snoc_norm
|
|
||||||
: norm (snoc as (LTuple.snoc bs b)) = LTuple.snoc (norm (snoc as bs)) b := by
|
|
||||||
unfold norm
|
|
||||||
rw [← LTuple.concat_snoc_snoc_concat]
|
|
||||||
|
|
||||||
/--
|
|
||||||
Normalizing an `GTuple` is equivalent to concatenating the normalized `fst`
|
|
||||||
component with the `snd`.
|
|
||||||
-/
|
|
||||||
theorem norm_snoc_eq_concat {t₁ : GTuple α (p, q)} {t₂ : LTuple α n}
|
|
||||||
: norm (snoc t₁ t₂) = LTuple.concat t₁.norm t₂ := by
|
|
||||||
conv => lhs; unfold norm
|
|
||||||
|
|
||||||
/-! ## Equality -/
|
|
||||||
|
|
||||||
/--
|
|
||||||
Implements Boolean equality for `GTuple α n` provided `α` has decidable
|
|
||||||
equality.
|
|
||||||
-/
|
|
||||||
instance BEq [DecidableEq α] : BEq (GTuple α n) where
|
|
||||||
beq t₁ t₂ := t₁.norm == t₂.norm
|
|
||||||
|
|
||||||
/-! ## Basic API -/
|
|
||||||
|
|
||||||
/--
|
|
||||||
Returns the number of entries in the `GTuple`.
|
|
||||||
-/
|
|
||||||
def size (_ : GTuple α n) := n
|
|
||||||
|
|
||||||
/--
|
|
||||||
Returns the number of entries in the "shallowest" portion of the `GTuple`. For
|
|
||||||
example, the length of `x[x[1, 2], 3, 4]` is `3`, despite its size being `4`.
|
|
||||||
-/
|
|
||||||
def length : GTuple α n → Nat
|
|
||||||
| g[] => 0
|
|
||||||
| snoc g[] ts => ts.size
|
|
||||||
| snoc _ ts => 1 + ts.size
|
|
||||||
|
|
||||||
/--
|
|
||||||
Returns the first component of our `GTuple`. For example, the first component of
|
|
||||||
tuple `x[x[1, 2], 3, 4]` is `t[1, 2]`.
|
|
||||||
-/
|
|
||||||
def fst : GTuple α (m, n) → LTuple α m
|
|
||||||
| g[] => t[]
|
|
||||||
| snoc ts _ => ts.norm
|
|
||||||
|
|
||||||
/--
|
|
||||||
Given `GTuple α (m, n)`, the `fst` component is equal to an initial segment of
|
|
||||||
size `k` of the tuple in normal form.
|
|
||||||
-/
|
|
||||||
theorem self_fst_eq_norm_take (t : GTuple α (m, n)) : t.fst = t.norm.take m :=
|
|
||||||
match t with
|
|
||||||
| g[] => by
|
|
||||||
unfold fst
|
|
||||||
rw [LTuple.self_take_zero_eq_nil]
|
|
||||||
simp
|
|
||||||
| snoc tf tl => by
|
|
||||||
unfold fst
|
|
||||||
conv => rhs; unfold norm
|
|
||||||
rw [LTuple.eq_take_concat]
|
|
||||||
simp
|
|
||||||
|
|
||||||
/--
|
|
||||||
If the normal form of an `GTuple` is equal to a `Tuple`, the `fst` component
|
|
||||||
must be a prefix of the `Tuple`.
|
|
||||||
-/
|
|
||||||
theorem norm_eq_fst_eq_take {t₁ : GTuple α (m, n)} {t₂ : LTuple α (m + n)}
|
|
||||||
: (t₁.norm = t₂) → (t₁.fst = t₂.take m) := by
|
|
||||||
intro h
|
|
||||||
rw [self_fst_eq_norm_take, h]
|
|
||||||
|
|
||||||
/--
|
|
||||||
Returns the first component of our `GTuple`. For example, the first component of
|
|
||||||
tuple `x[x[1, 2], 3, 4]` is `t[3, 4]`.
|
|
||||||
-/
|
|
||||||
def snd : GTuple α (m, n) → LTuple α n
|
|
||||||
| g[] => t[]
|
|
||||||
| snoc _ ts => ts
|
|
||||||
|
|
||||||
end GTuple
|
|
||||||
|
|
||||||
/-! ## Lemma 0A -/
|
|
||||||
|
|
||||||
section
|
|
||||||
|
|
||||||
variable {k m n : Nat}
|
|
||||||
variable (p : 1 ≤ m)
|
|
||||||
variable (q : n + (m - 1) = m + k)
|
|
||||||
|
|
||||||
private lemma n_eq_succ_k : n = k + 1 := by
|
|
||||||
let ⟨m', h⟩ := Nat.exists_eq_succ_of_ne_zero $ show m ≠ 0 by
|
|
||||||
intro h
|
|
||||||
have ff : 1 ≤ 0 := h ▸ p
|
|
||||||
ring_nf at ff
|
|
||||||
exact ff.elim
|
|
||||||
calc
|
|
||||||
n = n + (m - 1) - (m - 1) := by rw [Nat.add_sub_cancel]
|
|
||||||
_ = m' + 1 + k - (m' + 1 - 1) := by rw [q, h]
|
|
||||||
_ = m' + 1 + k - m' := by simp
|
|
||||||
_ = 1 + k + m' - m' := by rw [Nat.add_assoc, Nat.add_comm]
|
|
||||||
_ = 1 + k := by simp
|
|
||||||
_ = k + 1 := by rw [Nat.add_comm]
|
|
||||||
|
|
||||||
private lemma n_pred_eq_k : n - 1 = k := by
|
|
||||||
have h : k + 1 - 1 = k + 1 - 1 := rfl
|
|
||||||
conv at h => lhs; rw [←n_eq_succ_k p q]
|
|
||||||
simp at h
|
|
||||||
exact h
|
|
||||||
|
|
||||||
private lemma n_geq_one : 1 ≤ n := by
|
|
||||||
rw [n_eq_succ_k p q]
|
|
||||||
simp
|
|
||||||
|
|
||||||
private lemma min_comm_succ_eq : min (m + k) (k + 1) = k + 1 :=
|
|
||||||
Nat.recOn k
|
|
||||||
(by simp; exact p)
|
|
||||||
(fun k' ih => calc min (m + (k' + 1)) (k' + 1 + 1)
|
|
||||||
_ = min (m + k' + 1) (k' + 1 + 1) := by conv => rw [Nat.add_assoc]
|
|
||||||
_ = min (m + k') (k' + 1) + 1 := Nat.min_succ_succ (m + k') (k' + 1)
|
|
||||||
_ = k' + 1 + 1 := by rw [ih])
|
|
||||||
|
|
||||||
private lemma n_eq_min_comm_succ : n = min (m + k) (k + 1) := by
|
|
||||||
rw [min_comm_succ_eq p]
|
|
||||||
exact n_eq_succ_k p q
|
|
||||||
|
|
||||||
private lemma n_pred_m_eq_m_k : n + (m - 1) = m + k := by
|
|
||||||
rw [←Nat.add_sub_assoc p, Nat.add_comm, Nat.add_sub_assoc (n_geq_one p q)]
|
|
||||||
conv => lhs; rw [n_pred_eq_k p q]
|
|
||||||
|
|
||||||
private def castNorm : GTuple α (n, m - 1) → LTuple α (m + k)
|
|
||||||
| xs => cast (by rw [q]) xs.norm
|
|
||||||
|
|
||||||
private def castFst : GTuple α (n, m - 1) → LTuple α (k + 1)
|
|
||||||
| xs => cast (by rw [n_eq_succ_k p q]) xs.fst
|
|
||||||
|
|
||||||
private def castTake (ys : LTuple α (m + k)) :=
|
|
||||||
cast (by rw [min_comm_succ_eq p]) (ys.take (k + 1))
|
|
||||||
|
|
||||||
/-- #### Lemma 0A
|
|
||||||
|
|
||||||
Assume that `⟨x₁, ..., xₘ⟩ = ⟨y₁, ..., yₘ, ..., yₘ₊ₖ⟩`. Then
|
|
||||||
`x₁ = ⟨y₁, ..., yₖ₊₁⟩`.
|
|
||||||
-/
|
|
||||||
theorem lemma_0a (xs : GTuple α (n, m - 1)) (ys : LTuple α (m + k))
|
|
||||||
: (castNorm q xs = ys) → (castFst p q xs = castTake p ys) := by
|
|
||||||
intro h
|
|
||||||
suffices HEq
|
|
||||||
(cast (_ : LTuple α n = LTuple α (k + 1)) xs.fst)
|
|
||||||
(cast (_ : LTuple α (min (m + k) (k + 1)) = LTuple α (k + 1)) (LTuple.take ys (k + 1)))
|
|
||||||
from eq_of_heq this
|
|
||||||
congr
|
|
||||||
· exact n_eq_min_comm_succ p q
|
|
||||||
· rfl
|
|
||||||
· exact n_eq_min_comm_succ p q
|
|
||||||
· exact HEq.rfl
|
|
||||||
· exact Eq.recOn
|
|
||||||
(motive := fun _ h => HEq
|
|
||||||
(_ : n + (n - 1) = n + k)
|
|
||||||
(cast h (show n + (n - 1) = n + k by rw [n_pred_eq_k p q])))
|
|
||||||
(show (n + (n - 1) = n + k) = (min (m + k) (k + 1) + (n - 1) = n + k) by
|
|
||||||
rw [n_eq_min_comm_succ p q])
|
|
||||||
HEq.rfl
|
|
||||||
· exact n_geq_one p q
|
|
||||||
· exact n_pred_eq_k p q
|
|
||||||
· exact Eq.symm (n_eq_min_comm_succ p q)
|
|
||||||
· exact n_pred_eq_k p q
|
|
||||||
· rw [GTuple.self_fst_eq_norm_take]
|
|
||||||
unfold castNorm at h
|
|
||||||
simp at h
|
|
||||||
rw [←h, ←n_eq_succ_k p q]
|
|
||||||
have h₂ := Eq.recOn
|
|
||||||
(motive := fun x h => HEq
|
|
||||||
(LTuple.take xs.norm n)
|
|
||||||
(LTuple.take (cast (show LTuple α (n + (m - 1)) = LTuple α x by rw [h]) xs.norm) n))
|
|
||||||
(show n + (m - 1) = m + k by rw [n_pred_m_eq_m_k p q])
|
|
||||||
HEq.rfl
|
|
||||||
exact Eq.recOn
|
|
||||||
(motive := fun x h => HEq
|
|
||||||
(cast h (LTuple.take xs.norm n))
|
|
||||||
(LTuple.take (cast (_ : LTuple α (n + (m - 1)) = LTuple α (m + k)) xs.norm) n))
|
|
||||||
(show LTuple α (min (n + (m - 1)) n) = LTuple α n by simp)
|
|
||||||
h₂
|
|
||||||
|
|
||||||
end
|
|
||||||
|
|
||||||
end Enderton.Chapter_0
|
end Enderton.Chapter_0
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,4 @@
|
||||||
import Common.Combinator
|
import Common.Combinator
|
||||||
import Common.List
|
import Common.List
|
||||||
import Common.LTuple
|
|
||||||
import Common.Real
|
import Common.Real
|
||||||
import Common.Set
|
import Common.Set
|
||||||
|
|
@ -1 +0,0 @@
|
||||||
import Common.LTuple.Basic
|
|
||||||
|
|
@ -1,277 +0,0 @@
|
||||||
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
|
|
||||||
Loading…
Reference in New Issue