From 038067e1226dd1d04d4460e04b01afb79eb173a5 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Sat, 11 Feb 2023 01:21:43 -0500
Subject: [PATCH] cool

---
 SizedArray.lean | 494 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 494 insertions(+)
 create mode 100644 SizedArray.lean

diff --git a/SizedArray.lean b/SizedArray.lean
new file mode 100644
index 0000000..822b863
--- /dev/null
+++ b/SizedArray.lean
@@ -0,0 +1,494 @@
+def SizedArray (α : Type u) (n : Nat) :=
+  {as : List α // as.length = n}
+
+namespace SizedArray
+
+def inner {n : Nat} : SizedArray α n → List α :=
+  λxs => xs.val
+
+def empty : SizedArray α 0 := ⟨[], rfl⟩
+def singleton (a : α) : SizedArray α 1 := ⟨[a], rfl⟩ 
+
+def cons {n : Nat} : α → SizedArray α n → SizedArray α (n.succ) := 
+  λx xs =>
+    let ⟨xs, h⟩ := xs
+    ⟨x :: xs, by rw [List.length_cons, h]⟩ 
+
+def replicate (n : Nat) (x : α) : SizedArray α n :=
+  match n with
+  | Nat.zero => empty
+  | Nat.succ n => cons x (replicate n x)
+
+def append {a b : Nat} (as : SizedArray α a) (bs : SizedArray α b)
+  : SizedArray α (a + b) := by
+  let ⟨as, heqa⟩ := as
+  let ⟨bs, heqb⟩ := bs
+
+  let combined := as ++ bs
+  let (len_proof : combined.length = a + b) := by
+    rw [List.length_append]
+    rw [heqa, heqb]
+
+  exact ⟨combined, len_proof⟩  
+
+def from_list (xs : List α) : SizedArray α (xs.length) := 
+  match xs with
+  | List.nil => empty
+  | List.cons x xs => cons x (from_list xs)
+
+@[simp]
+def tail_neq_implies_neq
+  (a b : α) (as bs : List α) (h : as ≠ bs)
+  : a :: as ≠ b :: bs := by
+  induction as with
+  | nil => 
+    induction bs with
+    | nil => simp at h
+    | cons b bs => simp
+  | cons a' as' =>
+    simp [*]
+
+@[simp]
+def length_neq_implies_neq :
+  ∀{as bs : List α}, as.length ≠ bs.length → as ≠ bs
+  | [],     [], h => absurd h (by simp)
+  | [], (_::_), _ => by simp
+  | (_::_), [], _ => by simp
+  | (x::xs), (y::ys), h =>
+    let (h₂ : xs.length ≠ ys.length) := by
+      cases xs with
+      | nil =>
+        rw [List.length] at h
+        simp at h
+        rw [List.length_nil]
+        exact h
+      | cons x xs => 
+        rw [List.length, List.length, List.length] at h
+        simp at h
+        exact h
+    let h₃ := @length_neq_implies_neq α xs ys h₂
+    tail_neq_implies_neq x y xs ys h₃ 
+
+-- def length_g0_imp_nonempty (xs : List α) ⦃h : xs.length > 0⦄
+--   : List α ≠ List.nil := sorry
+
+-- def is_not_empty {n : Nat} {h : n > 0}
+--   : inner (SizedArray α n) ≠ [] := sorry
+
+def gt_flip {a b : Nat} (h : a > b) : (b < a) := by simp [*]
+def lt_flip {a b : Nat} (h : a < b) : (b > a) := by simp [*]
+def ge_flip {a b : Nat} (h : a ≥ b) : (b ≤ a) := by simp [*]
+def le_flip {a b : Nat} (h : a ≤ b) : (b ≥ a) := by simp [*]
+
+def gt_comm {a b : Nat} : a > b ↔ b < a := by simp [*]
+def lt_comm {a b : Nat} : a < b ↔ b > a := by simp [*]
+def ge_comm {a b : Nat} : a ≥ b ↔ b ≤ a := by simp [*]
+def le_comm {a b : Nat} : a ≤ b ↔ b ≥ a := by simp [*]
+
+def gt_implies_neq {a b : Nat} (h : a > b) : a ≠ b := by
+  have hlt := gt_flip h
+  have neq := Nat.ne_of_lt hlt
+  exact Ne.symm neq
+
+def lt_implies_neq {a b : Nat} (h : a < b) : a ≠ b := by 
+  have hgt := lt_flip h
+  have (neq : b ≠ a) := gt_implies_neq hgt
+  exact Ne.symm neq
+
+def length_gt_zero_implies_nonempty {xs : List α} (h : xs.length > 0)
+  : xs ≠ [] := 
+    let (hnz : List.length xs ≠ 0) := gt_implies_neq h
+    let (hne_len : xs.length ≠ [].length) := by
+      rw [List.length_nil]
+      exact hnz
+
+    length_neq_implies_neq hne_len
+
+def length_eq_zero_implies_empty {xs : List α} (_ : xs.length = 0)
+  : xs = [] :=
+  match xs with
+  | List.nil => rfl
+
+def empty_implies_length_eq_zero {xs : List α} (h : xs = [])
+  : xs.length = 0 := by
+    rw [h]
+    rfl
+
+def length_zero_iff_empty {xs : List α}
+  : xs.length = 0 ↔ xs = [] :=
+  ⟨
+    length_eq_zero_implies_empty, 
+    empty_implies_length_eq_zero
+  ⟩ 
+
+def not_empty_implies_length_neq_zero {xs : List α} (h : xs ≠ [])
+  : xs.length ≠ 0 := 
+  match xs with
+  | List.nil => by
+    have (nh : [] = []) := Eq.refl ([] : List α)
+    exact absurd nh h
+  | List.cons head tail => by
+    rw [List.length_cons]
+    exact Nat.succ_ne_zero (List.length tail)
+
+def length_gt_zero_iff_nonempty {xs : List α}
+  : xs.length > 0 ↔ xs ≠ [] := 
+  ⟨
+    length_gt_zero_implies_nonempty,
+    by
+      intro h
+      have hnz := not_empty_implies_length_neq_zero h
+      exact Nat.zero_lt_of_ne_zero hnz
+  ⟩  
+
+
+@[simp]
+def length_succ_implies_nonempty
+  {n : Nat} {xs : List α} (h : xs.length = n.succ)
+  : xs ≠ [] := by
+    apply length_gt_zero_implies_nonempty
+    have (hsnnz : n.succ ≠ 0) := Nat.succ_ne_zero n
+    have (hsngz : n.succ > 0) := Nat.zero_lt_of_ne_zero hsnnz
+    have (h :  xs.length > 0) := Eq.substr h hsngz
+    exact lt_flip h
+
+def head {n : Nat} (h : n > 0) : SizedArray α n → α :=
+  λxs =>
+    let ⟨xs, h₂⟩ := xs
+    let (hgz : List.length xs > 0) := Eq.substr h₂ h 
+    let hne := length_gt_zero_implies_nonempty hgz
+    
+    List.head xs hne
+
+def succ_inj {a b : Nat} (h : a.succ = b.succ) : a = b := by
+  induction a with
+  | zero =>
+    induction b with
+    | zero => rfl
+    | succ n =>
+      simp at h
+      simp
+      rw [Nat.add_succ] at h
+      simp at h
+  | succ n _ =>
+    simp at h
+    rw [Nat.succ_eq_add_one]
+    exact h
+
+-- def gt_and_lt_implies_false {a b : Nat} (hgt : a > b) (hlt : a < b)
+--   : False := sorry
+
+def succ_inj_gt {a b : Nat} (h : a > b) : a.succ > b.succ := by
+  have (h₂ : b < a) := gt_flip h
+  have (h₃ : Nat.succ b < Nat.succ a) := Nat.succ_lt_succ h₂ 
+  exact gt_flip h₃ 
+
+def tail_length_lt_source_length (x : α) (xs : List α) : ((x :: xs).length > xs.length) := by
+  rw [List.length_cons]
+  induction (List.length xs) with
+  | zero => simp
+  | succ n ih =>
+    apply succ_inj_gt
+    exact ih
+
+@[simp]
+def gt_self_implies_false {n : Nat} (h : n > n) : False := 
+  let neq := gt_implies_neq h
+  let eq  := Eq.refl n
+  absurd eq neq
+  
+def tail_list {n : Nat} (h : n > 0) (xs : SizedArray α n) 
+  : List α := by
+    let ⟨xs, heqn⟩ := xs
+    let (hgz : List.length xs > 0) := Eq.substr heqn h 
+    let (hne : xs ≠ []) := length_gt_zero_implies_nonempty hgz
+
+    match xs with
+    | List.nil => exact (by simp at hne)
+    | List.cons _ xs => exact xs
+
+def safe_tail (xs : List α) (h : xs.length > 0) : List α :=
+  match xs with
+  | List.nil => by
+    rw [List.length_nil] at h
+    exact (gt_self_implies_false h).elim
+  | List.cons _ xs => xs
+
+def safe_tail_len (xs : List α) (h : xs.length > 0)
+  : (safe_tail xs h).length = xs.length.pred := by
+  induction xs with
+  | nil => simp at h
+  | cons a as _ =>  
+    rw [safe_tail]
+    simp
+  
+def tail {n : Nat} (h : n > 0) (xs : SizedArray α n)
+  : SizedArray α n.pred := by
+    let ⟨xs, heqn⟩ := xs
+    let (hgz : List.length xs > 0) := Eq.substr heqn h 
+    let tail := safe_tail xs hgz
+    let (tail_len : (safe_tail xs hgz).length = (List.length xs).pred)
+      := safe_tail_len xs hgz
+    rw [heqn] at tail_len
+
+    exact ⟨tail, tail_len⟩ 
+
+def uncons (h : n > 0) (xs : SizedArray α n) 
+  : α × (SizedArray α n.pred) := 
+    ⟨head h xs, tail h xs⟩ 
+
+def map {n : Nat} (f : α → β) (xs : SizedArray α n) : SizedArray β n :=
+  match n with
+  | Nat.zero => empty
+  | Nat.succ n => 
+    let (hnz : n.succ > 0) := lt_flip (Nat.zero_lt_succ n)
+    let ⟨head, tail⟩ := uncons hnz xs 
+    cons (f head) (map f tail)
+
+def reverse {n : Nat} (xs : SizedArray α n) : SizedArray α n := by
+  let ⟨xs, heqn⟩ := xs
+  let reversed := xs.reverse
+  let h := List.length_reverse xs
+  rw [heqn] at h
+  exact ⟨reversed, h⟩ 
+  -- match n with
+  -- | Nat.zero => empty
+  -- | Nat.succ n => by
+  --   let ⟨xs, heqn⟩ := xs
+  --   let (hne : xs ≠ []) := length_succ_implies_nonempty heqn
+  --   let (hnz : xs.length ≠ 0) := not_empty_implies_length_neq_zero hne
+  --   let (hgz : xs.length > 0) := Nat.zero_lt_of_ne_zero hnz
+  --   let ⟨head, tail⟩ := uncons hgz ⟨xs, rfl⟩ 
+    
+  --   let reversed := append (reverse tail) (singleton head)
+  --   rw [heqn, Nat.pred_succ, ← Nat.succ_eq_add_one] at reversed
+  --   exact reversed
+
+def matchable {n : Nat} (xs : SizedArray α n)
+  : Option (α × (SizedArray α n.pred)) :=
+  match n with
+  | Nat.zero => none
+  | Nat.succ x => by
+    let (hgz : x.succ > 0) := by
+      have (h : 0 < x.succ) := Nat.zero_lt_succ x
+      exact lt_flip h
+
+    let (h : α × (SizedArray α x)) := by
+      have h₂ := uncons hgz xs
+      simp at h₂ 
+      exact h₂
+
+    rw [Nat.pred_succ]
+    exact some h
+
+inductive Either (α β : Type u) where
+| left  : α → Either α β
+| right : β → Either α β
+
+def matchable' {n : Nat} (xs : SizedArray α n) 
+  : Either (SizedArray α 0) (α × (SizedArray α n.pred)) := by
+  match n with
+  | Nat.zero => exact Either.left empty
+  | Nat.succ x => 
+    apply Either.right
+
+    rw [Nat.pred_succ]
+
+    let (hgz : x.succ > 0) := by
+      have h₂ := Nat.zero_lt_succ x
+      exact lt_flip h₂ 
+
+    exact uncons hgz xs
+
+
+-- def matchable_with_proofs {n : Nat} (xs : SizedArray α n)
+--   : Either ((SizedArray α 0) × n = 0) ((α × (SizedArray α n.pred)) × n > 0) := by
+--   match n with
+--   | zero => sorry
+
+-- this is actually not true!
+-- 1.pred = 0 ∧ 0.pred = 0 so this would prove 1 = 0 which is FALSE!
+-- sure is inconvenient though
+-- def pred_eq {a b : Nat} (h : a.pred = b.pred) : a = b := by
+--   induction a with
+--   | zero =>
+--     rw [Nat.pred_zero] at h
+--     induction b with
+--     | zero => rfl
+--     | succ n ih =>
+--       rw [Nat.pred_succ] at h
+-- 
+--   | succ n ih => sorry
+
+def pred_sub_assoc {a b : Nat}
+  : (Nat.pred a) - b = Nat.pred (a - b) := by
+    induction a with
+    | zero => rw [Nat.pred_zero, Nat.zero_sub, Nat.pred_zero ]
+    | succ n _ =>
+      rw [← Nat.sub_succ, Nat.pred_succ]
+      rw [Nat.succ_sub_succ]
+
+
+def drop {from_len : Nat} (n : Nat) (xs : SizedArray α from_len) 
+  : SizedArray α (from_len - n) := by
+  let ⟨inner, heqn⟩ := xs
+  match inner with
+  | List.nil => 
+    rw [List.length_nil] at heqn
+    rw [← heqn]
+    rw [Nat.zero_sub]
+    exact empty
+  | List.cons x xs' => 
+    rw [List.length_cons] at heqn
+
+    match n with 
+    | Nat.zero =>
+      rw [Nat.sub_zero]
+      exact xs
+    | Nat.succ n =>
+      let (hgz : from_len > 0) := by
+        let hnz := Nat.succ_ne_zero (List.length xs')
+        rw [← heqn] 
+        exact Nat.zero_lt_of_ne_zero hnz
+
+      rw [Nat.sub_succ]
+      rw [← pred_sub_assoc]
+      exact drop n (tail hgz xs)
+
+example : SizedArray Nat 2 := drop 3 (from_list [1, 2, 3, 4, 5])
+example : SizedArray Nat 0 := drop 100 (from_list [1, 2, 3, 4, 5])
+
+#check drop 1 (drop 2 (from_list [1,2,3,4,5,6]))
+
+def drop_end {from_len : Nat} (n : Nat) (xs : SizedArray α from_len)
+  : SizedArray α (from_len - n) := 
+  let reversed := reverse xs
+  let dropped := drop n reversed
+  reverse dropped
+
+#eval drop_end 1 (drop 2 (from_list [1,2,3,4,5,6]))
+
+-- def min_comm {a b : Nat} : min a b = min b a := by
+--   rw [Nat.min_def, Nat.min_def]
+--   sorry
+
+def succ_le_succ_iff_le {a b : Nat} : a.succ ≤ b.succ ↔ a ≤ b :=
+  ⟨
+    Nat.le_of_succ_le_succ,
+    Nat.succ_le_succ
+  ⟩ 
+
+#check ite_congr
+
+def map_ite (f : β → γ) {c : Prop} [Decidable c] {a b : β}
+  : f (if c then a else b) = (if c then (f a) else (f b)) := by
+  cases h : decide c with
+  | false => 
+    let (hcf : c = False) := eq_false_of_decide h
+    simp only [hcf]
+    rw [ite_false, ite_false]
+  | true =>
+    let (hcf : c = True) := eq_true_of_decide h
+    simp only [hcf]
+    rw [ite_true, ite_true]
+
+def succ_min {a b : Nat} : (min a b).succ = min a.succ b.succ := by
+  rw [Nat.min_def]
+  rw [Nat.min_def]
+  let (h₁ : (a ≤ b) = (a.succ ≤ b.succ)) := by rw [succ_le_succ_iff_le]
+  rw [map_ite Nat.succ]
+  simp only [h₁]
+
+def zip {α β : Type u} {a b : Nat} (as : SizedArray α a) (bs : SizedArray β b)
+  : SizedArray (α × β) (min a b) := 
+  match a, b with
+  | 0, _ => by
+    rw [Nat.min_def]
+    simp
+    exact empty
+  | x', 0 => by
+    rw [Nat.min_def]
+    simp
+    match x' with
+    | 0 => simp; exact empty
+    | Nat.succ x => simp; exact empty
+  | Nat.succ a, Nat.succ b => by
+    let ⟨as_inner, haeqn⟩ := as
+    let ⟨bs_inner, hbeqn⟩ := bs
+    let hane := length_succ_implies_nonempty haeqn
+    let hagz :=
+      not_empty_implies_length_neq_zero hane
+      |> Nat.zero_lt_of_ne_zero 
+      |> lt_flip
+    let hbne := length_succ_implies_nonempty hbeqn
+    let hbgz :=
+      not_empty_implies_length_neq_zero hbne
+      |> Nat.zero_lt_of_ne_zero 
+      |> lt_flip
+    let hngz := lt_flip <| Eq.subst haeqn hagz
+    let ⟨a_head, a_tail⟩ := uncons hngz as
+    let hngz := lt_flip <| Eq.subst hbeqn hbgz
+    let ⟨b_head, b_tail⟩ := uncons hngz bs
+
+    let bleh := cons (a_head, b_head) (zip a_tail b_tail)
+    rw [Nat.pred_succ, Nat.pred_succ] at bleh
+    rw [succ_min] at bleh
+    exact bleh
+
+def take {from_len : Nat} (n : Nat) (xs : SizedArray α from_len)
+  : SizedArray α (min n from_len) := 
+  let dummy := replicate n ()
+  let zipped := zip dummy xs
+  map Prod.snd zipped
+  -- let reversed := reverse xs
+  -- let dropped := drop (from_len - n) reversed
+  -- let unreversed := reverse dropped
+  -- cases n with
+  -- | zero => 
+  --   rw [Nat.sub_zero, Nat.sub_self] at unreversed
+  --   rw [Nat.min_def]
+  --   simp
+  --   exact empty
+  -- | succ x => 
+  --   let n := x.succ
+  --   let (result : SizedArray α (min n from_len)) := sorry
+
+  --   exact result
+    -- sep sep sep sep
+    -- cases from_len with
+    -- | zero => 
+    --   rw [Nat.min_def]
+    --   simp
+    --   exact empty
+    -- | succ y => 
+    --   c
+    --   sorry
+
+  -- match n with
+  -- | Nat.zero => 
+  --   rw [Nat.min]
+  --   simp
+  --   exact empty
+  -- | Nat.succ x => 
+  --   match from_len with
+  --   | Nat.zero => 
+  --     rw [Nat.min]
+  --     simp
+  --     exact empty
+  --   | Nat.succ x' =>
+  --     let ⟨inner, heqsn⟩ := xs
+  --     let (hne : inner ≠ []) := length_succ_implies_nonempty heqsn
+  --     let (hnz : inner.length ≠ 0) := not_empty_implies_length_neq_zero hne
+  --     let (hgz : inner.length > 0) := Nat.zero_lt_of_ne_zero hnz
+  --     -- let ⟨head, tail⟩ := uncons hgz ⟨inner, rfl⟩ 
+  --     -- have taken := cons head (take x tail)
+  --     -- simp at taken
+  --     -- let tail := take x' (tail hgz ⟨inner, rfl⟩)
+  --     -- simp [*] at tail
+      
+
+  --     sorry
+
+-- example : SizedArray Nat 3 := take 3 (by simp) (from_list [1,2,3,4,5])
+
+#eval from_list [1,2,3,4,5,6,7,8,9,10] |> take 7 |> drop 2 |> reverse |> map (· * 2) |> (tail (by simp) ·)