Initial commit

Changes

1 changed files (+63/-0)

• main.lean (new)
  • @@ -0,0 +1,63 @@
    + -- import Mathlib.Tactic.SplitIfs + + -- import data.nat.basic + + inductive Vect (α : Type u) : Nat → Type u where + | nil : Vect α 0 + | cons : α → Vect α n → Vect α (n + 1) + + def Vect.zip : Vect α n → Vect β n → Vect (α × β) n + | .nil, .nil => .nil + | .cons x xs, .cons y ys => .cons (x, y) (zip xs ys) + + -- #eval (Vect.cons "Hello" (Vect.cons "world" Vect.nil)) + -- .zip (Vect.cons "Hello" (Vect.cons "world" Vect.nil)) + + def hi : Vect String 2 := Vect.cons "Hello" (Vect.cons "world" Vect.nil) + + -- #eval hi.zip hi + + -- def main : IO Unit := IO.println "Hello, world!" + + -- #eval main + + -- structure Pos where + -- succ :: + -- pred : Nat + + + + def merge [Ord α] (xs : List α) (ys : List α) : List α := + match xs, ys with + | [], _ => ys + | _, [] => xs + | x'::xs', y'::ys' => + match Ord.compare x' y' with + | .lt | .eq => x' :: merge xs' (y' :: ys') + | .gt => y' :: merge (x'::xs') ys' + + + + def lsb (i : Nat) : Nat := + if i == 0 then 0 else if i % 2 == 1 then 1 else 2 * lsb (i / 2) + termination_by i + decreasing_by + cases i + · simp + contradiction + · simp_all [Nat.div_lt_self] + + + -- theorem lsb_le_i : ∀ i : Nat, lsb i ≤ i := by + -- intro i + -- induction i with + -- | zero => + -- simp [lsb] + -- | succ n ih => + -- cases n with + -- | zero => + -- simp [lsb] + -- | succ n => + -- simp_all [lsb, Nat.div_lt_self] + -- split_ifs <;> simp_all [Nat.mul_le_mul_left] + -- <;> linarith