### Induction Principles for Natural Numbers in Acorn

Source: https://context7.com/acornprover/acornlib/llms.txt

Provides standard and strong induction principles for proving properties over natural numbers. Includes the `true_below` helper function and an example theorem demonstrating strong induction. Requires the `nat` module.

```acorn
from nat import Nat, strong_induction, true_below

// Standard induction is built into Nat
theorem standard_induction(p: Nat -> Bool) {
    p(Nat.0) and forall(n: Nat) { p(n) implies p(n.suc) }
    implies forall(n: Nat) { p(n) }
}

// Strong induction: assume property for all smaller values
define true_below(f: Nat -> Bool, n: Nat) -> Bool {
    forall(x: Nat) { x < n implies f(x) }
}

theorem strong_induction(f: Nat -> Bool) {
    forall(k: Nat) {
        true_below(f, k) implies f(k)
    } implies forall(n: Nat) { f(n) }
}

// Example: every number > 1 has a prime divisor (uses strong induction)
theorem has_prime_divisor(n: Nat) {
    1 < n implies exists(p: Nat) {
        p.is_prime and p.divides(n)
    }
}
```

--------------------------------

### Acorn Documentation Style

Source: https://github.com/acornprover/acornlib/blob/master/AGENTS.md

In Acorn, doc comments for types, typeclasses, and attributes must start with `///`. Comments should use mathematical language, avoiding programming-specific terms like 'returns' or 'checks'.

```acorn
// Good:
/// The smaller of two elements.

// Bad: "returns" is what a programmer would say.
/// Returns the smaller of two elements.

// Good:
/// True if f is continuous everywhere on the reals.

// Bad: "checks" is what a programmer would say.
/// Checks if f is continuous everywhere on the reals.
```

--------------------------------

### Option Type for Optional Values in Acorn

Source: https://context7.com/acornprover/acornlib/llms.txt

Implements the `Option` type for representing optional values, useful for partial functions and error handling. Demonstrates pattern matching with `match` and provides a `safe_div` example. Requires the `prelude` module.

```acorn
from prelude import Option

// Option type definition
inductive Option[T] {
    none           // Absence of value
    some(T)        // Presence of value
}

// Pattern matching usage
define unwrap_or[T](opt: Option[T], default: T) -> T {
    match opt {
        Option.none { default }
        Option.some(value) { value }
    }
}

// Example: safe division returning Option
define safe_div(a: Nat, b: Nat) -> Option[Nat] {
    if b = Nat.0 {
        Option.none
    } else {
        Option.some(a / b)  // assuming integer division defined
    }
}
```

--------------------------------

### Sequence Convergence and Limits in Acorn

Source: https://context7.com/acornprover/acornlib/llms.txt

Defines sequence convergence, limits, and related theorems using epsilon-delta definitions. Supports sequence operations like addition and multiplication, and proves limit theorems. Requires `real.real_seq` and `real.limits` modules.

```acorn
from real.real_seq import converges, converges_to, limit, tail_bound
from real.limits import same_limit, vanishes, abs_seq

// Sequence type
type Sequence = Nat -> Real

// Convergence definition
define converges_to(a: Nat -> Real, L: Real) -> Bool {
    forall(eps: Real) {
        eps.is_positive implies exists(N: Nat) {
            forall(n: Nat) {
                n >= N implies a(n).is_close(L, eps)
            }
        }
    }
}

// Limit exists and is unique
define converges(a: Nat -> Real) -> Bool {
    exists(L: Real) { converges_to(a, L) }
}

// Extract the limit of a convergent sequence
let lim(a: Nat -> Real) -> L: Real satisfy {
    converges_to(a, L)
}

// Sequence operations
define add_seq(a: Nat -> Real, b: Nat -> Real, n: Nat) -> Real {
    a(n) + b(n)
}

define prod_seq(a: Nat -> Real, b: Nat -> Real, n: Nat) -> Real {
    a(n) * b(n)
}

// Limit theorems
theorem limit_add_seq(a: Nat -> Real, b: Nat -> Real) {
    converges(a) and converges(b) implies
    converges(add_seq(a, b)) and limit(add_seq(a, b)) = limit(a) + limit(b)
}

theorem limit_prod_seq(a: Nat -> Real, b: Nat -> Real) {
    converges(a) and converges(b) implies
    limit(prod_seq(a, b)) = limit(a) * limit(b)
}

// Vanishing sequences
define vanishes(a: Nat -> Real) -> Bool {
    converges(a) and limit(a) = Real.0
}
```

--------------------------------

### Run Acorn Verifier

Source: https://github.com/acornprover/acornlib/blob/master/AGENTS.md

The `acorn` command is used to run the verifier. It should be executed after every code change to ensure the proof remains verifiable. If the verifier is not available, use the 'acorn-installation' skill to set it up.

```shell
acorn
```

--------------------------------

### Integer (Int) Construction and Arithmetic in Acorn

Source: https://context7.com/acornprover/acornlib/llms.txt

Explains the construction of the `Int` type from natural numbers using `from_nat` and `neg_suc`. It covers integer arithmetic, negation, and ordering properties, demonstrating signed number representation.

```acorn
from int import Int

numerals Int

// Integer construction
let positive: Int = Int.from_nat(Nat.5)  // 5
let negative: Int = Int.neg_suc(Nat.4)   // -5 (neg_suc(n) = -(n+1))

// Arithmetic operations
let sum = 5 + (-3)    // 2
let diff = 3 - 7      // -4
let prod = (-2) * 3   // -6

// Absolute value returns Nat
define abs(a: Int) -> Nat {
    match a {
        Int.from_nat(n) { n }
        Int.neg_suc(k) { k.suc }
    }
}

// Negation
theorem neg_neg(a: Int) {
    -(-a) = a
}

// Ordering extends naturally
theorem int_ordering {
    Int.neg_suc(Nat.2) < Int.0  // -3 < 0
}
```

--------------------------------

### Acorn Set Operations

Source: https://context7.com/acornprover/acornlib/llms.txt

Illustrates set construction, membership testing, standard set operations (union, intersection, difference, complement), subset relations, insertion, removal, and cardinality for Acorn sets.

```acorn
from set import Set

// Set construction
let empty: Set[Nat] = Set[Nat].empty_set
let universal = Set[Nat].universal_set
let singleton_3 = Set[Nat].singleton(3)

// Membership via contains predicate
structure Set[K] {
    contains: K -> Bool
}

// Set operations
let union = a.union(b)              // a ∪ b
let intersection = a.intersection(b) // a ∩ b
let difference = a.difference(b)     // a \ b
let complement = a.c                  // aᶜ

// Subset relation
define subset(self, s: Set[K]) -> Bool {
    forall(x: K) {
        self.contains(x) implies s.contains(x)
    }
}

// Insert and remove
let with_elem = s.insert(5)
let without_elem = s.remove(5)

// Set theorems
theorem union_comm[K](a: Set[K], b: Set[K]) {
    a.union(b) = b.union(a)
}

theorem intersection_assoc[K](a: Set[K], b: Set[K], c: Set[K]) {
    a.intersection(b.intersection(c)) = a.intersection(b).intersection(c)
}

theorem double_inclusion[K](a: Set[K], b: Set[K]) {
    a.subset(b) and b.subset(a) implies a = b
}

// Finite set cardinality
define cardinality_is(self, n: Nat) -> Bool {
    exists(containing_list: List[K]) {
        containing_list.contains_set(self) and
        containing_list.filter(self.contains).unique.length = n
    }
}
```

--------------------------------

### Acorn List Operations

Source: https://context7.com/acornprover/acornlib/llms.txt

Demonstrates construction, concatenation, membership testing, length calculation, map, filter, uniqueness, and range generation for Acorn's immutable linked lists.

```acorn
from list import List

// List construction
let empty: List[Nat] = List.nil[Nat]
let single = List.singleton(5)
let multi = List.cons(1, List.cons(2, List.cons(3, List.nil)))

// Concatenation
let combined = List.cons(1, List.nil) + List.cons(2, List.nil)

// Membership testing
theorem contains_example {
    List.cons(3, List.cons(5, List.nil)).contains(5)
}

// Length
define length(self) -> Nat {
    match self {
        List.nil { Nat.0 }
        List.cons(_, tail) { tail.length.suc }
    }
}

// Map function
define map[U](self, f: T -> U) -> List[U] {
    match self {
        List.nil { List.nil[U] }
        List.cons(head, tail) {
            List.cons(f(head), tail.map(f))
        }
    }
}

// Filter
define filter(self, f: T -> Bool) -> List[T] {
    match self {
        List.nil { List.nil[T] }
        List.cons(head, tail) {
            if f(head) {
                List.cons(head, tail.filter(f))
            } else {
                tail.filter(f)
            }
        }
    }
}

// Uniqueness (removes duplicates)
let unique_list = List.cons(1, List.cons(1, List.cons(2, List.nil))).unique
// Result: [1, 2]

// Range generation
let range_5 = Nat.range(5)  // [0, 1, 2, 3, 4]
```

--------------------------------

### Real Numbers (Real) Definition and Properties in Acorn

Source: https://context7.com/acornprover/acornlib/llms.txt

Defines `Real` numbers using Dedekind cuts from rationals. It includes arithmetic, ordering, absolute value, and demonstrates key analysis concepts like closeness and the density of rationals in reals.

```acorn
from real import Real
from rat import Rat

// Real number construction from rationals
let x: Real = Real.from_rat(Rat.2)
let y: Real = Real.from_int(Int.3)

// Special values
let zero = Real.0
let one = Real.1
let half = Real.one_half

// Arithmetic
let sum = x + y
let neg = -x
let diff = x - y

// Ordering (total order)
theorem lte_or_gte(a: Real, b: Real) {
    a <= b or b <= a
}

// Absolute value
define abs(self) -> Real {
    if self.is_negative {
        -self
    } else {
        self
    }
}

// Closeness predicate for analysis
define is_close(self, other: Real, eps: Real) -> Bool {
    (self - other).abs < eps
}

// Key theorem: rationals are dense in reals
theorem rat_between_reals(a: Real, b: Real) {
    a < b implies exists(r: Rat) {
        a < Real.from_rat(r) and Real.from_rat(r) < b
    }
}

// Floor function exists for all reals
theorem floor_exists(a: Real) {
    exists(n: Int) {
        Real.from_int(n) <= a and a < Real.from_int(n + Int.1)
    }
}
```

--------------------------------

### Natural Numbers (Nat) Definition and Operations in Acorn

Source: https://context7.com/acornprover/acornlib/llms.txt

Defines the `Nat` type using Peano axioms and demonstrates basic arithmetic, ordering, divisibility, primality testing, and the division theorem. It showcases fundamental number theory concepts within Acorn.

```acorn
from nat import Nat

// Define natural numbers with explicit type
numerals Nat

// Basic arithmetic
let a: Nat = 5
let b: Nat = 3
let sum = a + b       // 8
let prod = a * b      // 15

// Ordering is defined via existence of difference
// a <= b iff exists(c: Nat) { a + c = b }
theorem example_ordering {
    3 <= 5
}

// Divisibility: a.divides(b) iff exists(c) { a * c = b }
theorem six_divides_twelve {
    6.divides(12)
}

// Primality testing
theorem seven_is_prime {
    7.is_prime
}

// Factorial
theorem factorial_five {
    5.factorial = 120
}

// Division theorem: for m, n with 0 < n, exists unique quotient and remainder
theorem division_theorem(m: Nat, n: Nat) {
    0 < n implies exists(q: Nat, r: Nat) {
        r < n and m = q * n + r
    }
}

// Infinitude of primes
theorem exists_infinite_primes(n: Nat) {
    exists(p: Nat) {
        n < p and p.is_prime
    }
}
```

--------------------------------

### Acorn Group Algebraic Structures

Source: https://context7.com/acornprover/acornlib/llms.txt

Defines the Group type class, extending Monoid, and illustrates axioms like inverse laws, cancellation laws, homomorphisms, and finite order for algebraic structures.

```acorn
from monoid import Monoid
from group import Group

// Group typeclass definition
typeclass G: Group extends Monoid {
    inverse: G -> G

    // Right inverse axiom (left inverse is derived)
    inverse_right(a: G) {
        a * a.inverse = G.1
    }
}

// Derived theorems
theorem inverse_left[G: Group](a: G) {
    a.inverse * a = G.1
}

theorem inverse_inverse[G: Group](a: G) {
    a.inverse.inverse = a
}

theorem inverse_mul[G: Group](a: G, b: G) {
    (a * b).inverse = b.inverse * a.inverse
}

// Cancellation laws
theorem left_cancel[G: Group](a: G, b: G, c: G) {
    a * b = a * c implies b = c
}

// Homomorphisms
define is_hom[G: Group, H: Group](f: G -> H) -> Bool {
    forall(a: G, b: G) {
        f(a * b) = f(a) * f(b)
    }
}

// Finite order
define has_finite_order[G: Group](g: G) -> Bool {
    exists(n: Nat) {
        n != Nat.0 and g.pow(n) = G.1
    }
}
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.