pkg install lean4

lean --version
lake --version

-- Natural number examples on FreeBSD 15.0

-- Basic theorem
theorem add_zero (n : Nat) : n + 0 = n := rfl

-- Proof by induction
theorem add_succ (n m : Nat) : n + Nat.succ m = Nat.succ (n + m) := rfl

-- Commutativity (from stdlib)
#check Nat.add_comm

-- Simple evaluation
#eval (List.range 10).map (· * 2)

-- Propositional logic examples

-- Modus ponens
theorem modus_ponens (P Q : Prop) (hp : P) (hpq : P → Q) : Q :=
  hpq hp

-- Conjunction introduction
theorem and_intro (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
  ⟨hp, hq⟩

-- Conjunction elimination
theorem and_left (P Q : Prop) (h : P ∧ Q) : P :=
  h.left

theorem and_right (P Q : Prop) (h : P ∧ Q) : Q :=
  h.right

-- Disjunction
theorem or_intro_left (P Q : Prop) (hp : P) : P ∨ Q :=
  Or.inl hp

-- Double negation (classical)
theorem dne (P : Prop) : ¬¬P → P := by
  intro hnnp
  by_contra hnp
  exact hnnp hnp

-- List operations and proofs

def myLength : List α → Nat
  | [] => 0
  | _ :: xs => 1 + myLength xs

def myReverse : List α → List α
  | [] => []
  | x :: xs => myReverse xs ++ [x]

-- Prove length is preserved by reverse
theorem reverse_length (xs : List α) : (myReverse xs).length = xs.length := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    simp [myReverse, List.length_append]
    omega

-- Map preserves length
theorem map_length (f : α → β) (xs : List α) : (xs.map f).length = xs.length := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp [ih]

#eval myReverse [1, 2, 3, 4, 5]
#eval myLength ["a", "b", "c"]

-- Type class examples

class Monoid (α : Type) where
  unit : α
  op : α → α → α
  left_unit : ∀ x, op unit x = x
  right_unit : ∀ x, op x unit = x
  assoc : ∀ x y z, op (op x y) z = op x (op y z)

-- Natural numbers under addition form a monoid
instance : Monoid Nat where
  unit := 0
  op := (· + ·)
  left_unit := Nat.zero_add
  right_unit := Nat.add_zero
  assoc := Nat.add_assoc

-- List concatenation forms a monoid
instance : Monoid (List α) where
  unit := []
  op := (· ++ ·)
  left_unit := List.nil_append
  right_unit := List.append_nil
  assoc := List.append_assoc

-- Generic fold using monoid
def mconcat [Monoid α] (xs : List α) : α :=
  xs.foldl Monoid.op Monoid.unit

#eval mconcat [[1,2], [3,4], [5,6]]  -- [1, 2, 3, 4, 5, 6]
#eval mconcat [1, 2, 3, 4, 5]        -- 15

-- In lakefile.lean, add:
require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

lake update
lake build

echo "=== Full System Info ==="
echo "OS: $(uname -srm)"
echo "Lean: $(lean --version 2>&1)"
echo "Lake: $(lake --version 2>&1)"
echo "procfs: $(mount | grep 'procfs on /proc' || echo 'NOT MOUNTED')"
echo "pkg: $(pkg info lean4 2>&1 | grep Version || echo 'NOT INSTALLED')"