@[reducible, inline]

abbrev Sequence (n : ℕ) (α : Type) : Type

Equations

• Sequence n α = { t : List α // t.length = n }

def sequence_lift {α : Type} (t : List α) : Sequence t.length α

Equations

• sequence_lift t = ⟨t, ⋯⟩

instance seq_b {α : Type} {n : ℕ} [BEq α] : BEq (Sequence n α)

Equations

• seq_b = { beq := fun (l r : Sequence n α) => ↑l == ↑r }

def Sequence.nil {γ : Type} : Sequence 0 γ

Equations

• Sequence.nil = ⟨[], Sequence.nil.proof_1⟩

theorem nil_equiv {α : Type} {t : Sequence 0 α} : t = Sequence.nil

def Sequence.single {α : Type} (a : α) : Sequence 1 α

Equations

• Sequence.single a = ⟨[a], Sequence.single.proof_1⟩

def Sequence.cons {α : Type} {n : ℕ} (a : α) : Sequence n α → Sequence n.succ α

Equations

• Sequence.cons a s = ⟨a :: ↑s, ⋯⟩

theorem not_nil_len {α : Type} (ls : List α) (len_nz : 0 < ls.length) : ¬ls = []

theorem seq_is_len {α : Type} {n : ℕ} (s : Sequence n α) : (↑s).length = n

def Sequence.head {α : Type} {n : ℕ} (seq : Sequence n.succ α) : α

Equations

• seq.head = (↑seq).head ⋯

def Sequence.head' {α : Type} {n : ℕ} (seq : Sequence n α) (notZ : 0 < n) : α

Equations

• seq.head' notZ = (↑seq).head ⋯

def Sequence.tail {α : Type} {n : ℕ} (seq : Sequence n.succ α) : Sequence n α

Equations

• seq.tail = ⟨(↑seq).tail, ⋯⟩

theorem Sequence.lmm_destruct {α : Type} {n : ℕ} (s : Sequence n.succ α) : s = cons s.head s.tail

def Sequence.pmatch {α : Type} {n : ℕ} (s : Sequence n α) : Sequence 0 α ⊕ α × Sequence n.pred α

Equations

• s_2.pmatch = Sum.inl Sequence.nil
• s_2.pmatch = Sum.inr (s_2.head, s_2.tail)

def Sequence.destruct {α : Type} {n : ℕ} (s : Sequence n.succ α) : α × Sequence n α

Equations

• s.destruct = (s.head, s.tail)

def Sequence.foldr {α β : Type} {n : ℕ} (f : α → β → β) (b : β) (sq : Sequence n α) : β

Equations

• Sequence.foldr f b s_1 = b
• Sequence.foldr f b s_1 = match s_1.destruct with | (a, as) => f a (Sequence.foldr f b as)

def Sequence.foldl {α β : Type} {n : ℕ} (f : β → α → β) (b : β) (sq : Sequence n α) : β

Equations

• Sequence.foldl f b s_1 = b
• Sequence.foldl f b s_1 = Sequence.foldl f (f b s_1.head) s_1.tail

def Sequence.tail_pred {α : Type} {n : ℕ} (s : Sequence n α) : Sequence n.pred α

Equations

• s_2.tail_pred = Sequence.nil
• s_2.tail_pred = s_2.tail

def Sequence.init {α : Type} {n : ℕ} (seq : Sequence n.succ α) : Sequence n α

Equations

• seq.init = ⟨List.take n ↑seq, ⋯⟩

def sequence_coerce {α : Type} {n m : ℕ} (hEq : n = m) (s : Sequence n α) : Sequence m α

Equations

• sequence_coerce hEq_2 s_2 = Sequence.nil
• sequence_coerce hEq_2 s_2 = Sequence.cons s_2.head (sequence_coerce ⋯ s_2.tail)

theorem rfl_coerce {α : Type} (l r : List α) : l = r → ∀ (n m : ℕ) (lp : l.length = m) (rp : r.length = n) (heq : n = m), ⟨l, lp⟩ = sequence_coerce heq ⟨r, rp⟩

theorem cons_seq_coerce {α : Type} {n m : ℕ} {heq : n = m} (a : α) (seq : Sequence n α) : Sequence.cons a (sequence_coerce heq seq) = sequence_coerce ⋯ (Sequence.cons a seq)

theorem same_length {α : Type} {n m : ℕ} (l : Sequence n α) (r : Sequence m α) : ↑l = ↑r → n = m

def beq_sequences {α : Type} [BEq α] {n : ℕ} : BEq (Sequence n α)

Equations

• beq_sequences = { beq := fun (sl sr : Sequence n α) => ↑sl == ↑sr }

def beq_sequences_poly {α : Type} [BEq α] {n m : ℕ} (l : Sequence n α) (r : Sequence m α) : Bool

Equations

• beq_sequences_poly l r = (n == m && ↑l == ↑r)

def Sequence.last {α : Type} {n : ℕ} (seq : Sequence n.succ α) : α

Equations

• seq_2.last = seq_2.head
• seq_2.last = seq_2.tail.last

def lastSeq' {α : Type} {n m : ℕ} (seq : Sequence n α) (ns : n = m + 1) : α

Equations

• lastSeq' seq ns = (sequence_coerce ns seq).last

def Sequence.constant {α : Type} (n : ℕ) (a : α) : Sequence n α

Equations

• Sequence.constant Nat.zero a = Sequence.nil
• Sequence.constant pn.succ a = Sequence.cons a (Sequence.constant pn a)

theorem constant_succ {α : Type} {n : ℕ} {a : α} : ↑(Sequence.constant n.succ a) = a :: ↑(Sequence.constant n a)

def polyLenSeqEq {α : Type} [BEq α] {n m : ℕ} (p : Sequence n α) (q : Sequence m α) : Bool

Equations

• polyLenSeqEq p_2 q_2 = true
• polyLenSeqEq p_2 q_2 = if (p_2.head == q_2.head) = true then polyLenSeqEq p_2.tail q_2.tail else false
• polyLenSeqEq p q = false

theorem seqEqLawLength {α : Type} [BEq α] {m n : ℕ} (p : Sequence n α) (q : Sequence m α) (pEq : polyLenSeqEq p q = true) : n = m

theorem seqEqLawRfl {α : Type} [BEq α] [LawfulBEq α] {n : ℕ} (p : Sequence n α) : polyLenSeqEq p p = true

def zip_succ_int {α : Type} {n : ℕ} (h : α) (seq : Sequence n.succ α) : Sequence n.succ (α × α)

Equations

• zip_succ_int h seq_2 = Sequence.single (h, seq_2.head)
• zip_succ_int h seq_2 = Sequence.cons (h, seq_2.head) (zip_succ_int seq_2.head seq_2.tail)

def zip_succ {α : Type} {n : ℕ} (seq : Sequence n.succ.succ α) : Sequence n.succ (α × α)

Equations

• zip_succ seq = zip_succ_int seq.head seq.tail

def Sequence.append {α : Type} {n m : ℕ} (p : Sequence n α) (q : Sequence m α) : Sequence (n + m) α

Equations

• p.append q = ⟨(↑p).append ↑q, ⋯⟩

def Sequence.snoc {α : Type} {n : ℕ} (seq : Sequence n α) (a : α) : Sequence n.succ α

Equations

• seq.snoc a = seq.append (Sequence.single a)

def Sequence.getI {α : Type} {n : ℕ} (seq : Sequence n α) (i : ℕ) (iLTn : i < n) : α

Equations

• seq.getI Nat.zero iLTn_2 = seq.head' iLTn_2
• seq.getI pn.succ iLTn_2 = seq.tail_pred.getI pn ⋯

def desc_Seq {n : ℕ} {α : Type} (seq : Sequence n.succ α) : α × Sequence n α

Equations

• desc_Seq seq = (seq.head, seq.tail)

def Sequence.map {α β : Type} {n : ℕ} (f : α → β) (seq : Sequence n α) : Sequence n β

Equations

• Sequence.map f seq = ⟨List.map f ↑seq, ⋯⟩

theorem map_tail {α β : Type} {n : ℕ} (f : α → β) (seq : Sequence n.succ α) : (Sequence.map f seq).tail = Sequence.map f seq.tail

def Sequence.zip_with {α β ε : Type} {n : ℕ} (f : α → β → ε) (sl : Sequence n α) (sr : Sequence n β) : Sequence n ε

Equations

• Sequence.zip_with f sl_2 sr_2 = Sequence.nil
• Sequence.zip_with f sl_2 sr_2 = Sequence.cons (f sl_2.head sr_2.head) (Sequence.zip_with f sl_2.tail sr_2.tail)

def Sequence.nats' {n : ℕ} (start : ℕ) : Sequence n ℕ

Equations

• Sequence.nats' start = Sequence.nil
• Sequence.nats' start = Sequence.cons start (Sequence.nats' start.succ)

def Sequence.nats {n : ℕ} : Sequence n ℕ

Equations

• Sequence.nats = Sequence.nats' 0

def Sequence.imap {α β : Type} {n : ℕ} (f : ℕ → α → β) (seq : Sequence n α) : Sequence n β

Equations

• Sequence.imap f seq = Sequence.zip_with (flip f) seq Sequence.nats

def Sequence.reverse {α : Type} {n : ℕ} (seq : Sequence n α) : Sequence n α

Equations

• seq.reverse = ⟨(↑seq).reverse, ⋯⟩

def Sequence.take {α : Type} {n : ℕ} (m : ℕ) (mLTn : m ≤ n) (s : Sequence n α) : Sequence m α

Equations

• Sequence.take m mLTn s = ⟨List.take m ↑s, ⋯⟩

def Sequence.drop {α : Type} {n : ℕ} (m : ℕ) (s : Sequence n α) : Sequence (n - m) α

Equations

• Sequence.drop m s = ⟨List.drop m ↑s, ⋯⟩

def Sequence.split {α : Type} {n : ℕ} (p : Sequence n α) (m : ℕ) (mLTn : m ≤ n) : Sequence m α × Sequence (n - m) α

Equations

• p.split m mLTn = (Sequence.take m mLTn p, Sequence.drop m p)

def Sequence.join {α : Type} {n : ℕ} (f : α → α → α) (seq : Sequence (2 * n) α) : Sequence n α

Equations

• Sequence.join f seq_2 = Sequence.nil
• Sequence.join f seq_2 = Sequence.cons (f seq_2.head seq_2.tail.head) (Sequence.join f seq_2.tail.tail)

theorem pp2 {n : ℕ} : 2 ^ n.succ = 2 ^ n + 2 ^ n

theorem gt0Add (m n : ℕ) (hm : 0 < m) (hn : 0 ≤ n) : 0 < m + n

theorem geq0Add (m n : ℕ) (hm : 0 ≤ m) (hn : 0 ≤ n) : 0 ≤ m + n

theorem pow_gt_zero {m : ℕ} : 0 < 2 ^ m

theorem pow_geq_one {m : ℕ} : 1 ≤ 2 ^ m

theorem ppGT {n : ℕ} : 0 < 2 ^ n + 2 ^ n + (2 ^ n + 2 ^ n) - 1 - (2 ^ n + 2 ^ n - 1)

theorem eqPP {n : ℕ} : 2 ^ (n + 1) + 2 ^ (n + 1) - 1 - (2 ^ (n + 1) - 1) = 2 ^ (n + 1) - 1 + 1

def half_split {α : Type} {n : ℕ} (seq : Sequence (2 * n) α) : Sequence n α × Sequence n α

Equations

• half_split seq = (Sequence.take n ⋯ seq, sequence_coerce ⋯ (Sequence.drop n seq))

def half_split_pow {α : Type} {n : ℕ} (seq : Sequence (2 ^ n.succ) α) : Sequence (2 ^ n) α × Sequence (2 ^ n) α

Equations

• half_split_pow seq = (Sequence.take (2 ^ n) ⋯ seq, sequence_coerce ⋯ (Sequence.drop (2 ^ n) seq))

def Sequence.consume_pow {α : Type} {lgn : ℕ} (f : α → α → α) (seq : Sequence (2 ^ lgn) α) : α

Equations

• Sequence.consume_pow f seq_2 = seq_2.head
• Sequence.consume_pow f seq_2 = Sequence.consume_pow f (Sequence.join f (sequence_coerce ⋯ seq_2))

def Sequence.perfect_split {α : Type} {n : ℕ} (seq : Sequence (2 ^ n.succ - 1) α) : Sequence (2 ^ n - 1) α × α × Sequence (2 ^ n - 1) α

Equations

• seq.perfect_split = match seq.split (2 ^ n - 1) ⋯ with | (seql, hdseqr) => (seql, hdseqr.head' ⋯, (sequence_coerce ⋯ hdseqr).tail)

def sequence_forget {α : Type} {n : ℕ} (seq : Sequence n α) : List α

Equations

• sequence_forget seq = ↑seq

theorem split_seq_eq {α : Type} {n m : ℕ} {mLTn : m ≤ n} (seq : Sequence n α) : match seq.split m mLTn with | (seql, seqr) => seq = sequence_coerce ⋯ (seql.append seqr)

theorem ExtraCoerce {α : Type} {n : ℕ} (req : n = n) (seq : Sequence n α) : seq = sequence_coerce req seq

theorem coerce_trans {α : Type} {n m l : ℕ} {fst : n = m} {snd : m = l} (seq : Sequence n α) : sequence_coerce snd (sequence_coerce fst seq) = sequence_coerce ⋯ seq

theorem coerce_eq_comm {α : Type} {n m : ℕ} {heq : n = m} (seql : Sequence n α) (seqr : Sequence m α) : sequence_coerce heq seql = seqr → seql = sequence_coerce ⋯ seqr

theorem coerce_eq_comm' {α : Type} {n m : ℕ} {heq : m = n} (seql : Sequence n α) (seqr : Sequence m α) : seql = sequence_coerce heq seqr → sequence_coerce ⋯ seql = seqr

theorem coerce_eq_coerce {α : Type} {n m l : ℕ} {reql : n = l} {reqr : m = l} (seql : Sequence n α) (seqr : Sequence m α) : sequence_coerce reql seql = sequence_coerce reqr seqr → sequence_coerce ⋯ seql = seqr

theorem rfl_coerce_up {α : Type} {n m : ℕ} {meq : n = m} (ls : List α) {lp : ls.length = n} : ls = ↑(sequence_coerce meq ⟨ls, lp⟩)

theorem TailCoerDrop {α : Type} {n m : ℕ} (d : ℕ) {heq : n - d = m + 1} (seq : Sequence n α) : (sequence_coerce heq (Sequence.drop d seq)).tail = sequence_coerce ⋯ (Sequence.drop d.succ seq)

theorem TakeCoerce {α : Type} {n m k : ℕ} {kLT : k ≤ n} (heq : k = m) (seq : Sequence n α) : sequence_coerce heq (Sequence.take k kLT seq) = Sequence.take m ⋯ seq