# Proving a claim

> The proofs an app needs, from a move's one-liner to "the control is on screen exactly when its move is enabled".

A claim's evidence comes at several strengths. The strongest is a proof that Lean's kernel has
checked, using only the three standard axioms. This chapter shows the proofs a small app has, in
the order you meet them.

## The proof a move needs

A move's `sound` clause proves that its handler meets its `post`, for every state (and every key
and text operation) where the move is enabled. For an item's checkbox, `apply` flips the item and
`post` says the items are the old ones with that item flipped, so both sides compute to the same
thing and `rfl` closes it:

```lean
move ^4 toggleItem (s : State) (k : Nat) "Toggle an item" in ^1 where
  does "Press an item's checkbox."
  sees "The item is marked done, or not done again."
  enabled := has s k
  on press
    apply := toggle k s
    post s' := s'.items = s.items.map (flip k)
    sound := by intro s k _; rfl
```

`test/fixture/lean/Fixture.lean`, lines 255–262

Most moves are like that: `post` restates `apply` in the terms a reader cares about, and the proof
is `rfl`, a tuple of `rfl`s, or a lemma about the model. When a proof needs real logic about a
function the app calls, prove a lemma about that function next to it and cite it. The fixture's
invariant does that for `add`:

```lean
/-- ^7's statement. -/
def Inv (s : State) : Prop := 0 < s.nextId ∧ ∀ i ∈ s.items, i.id < s.nextId

theorem add_inv {s : State} (h : Inv s) : Inv (add s) := by
  obtain ⟨hn, hb⟩ := h
  unfold add
  by_cases ht : trimmed s.field.text = []
  · simp only [ht, ↓reduceIte]; exact ⟨hn, hb⟩
  · simp only [ht, ↓reduceIte]
    refine ⟨Nat.succ_pos _, fun i hi => ?_⟩
    simp only [List.mem_append, List.mem_singleton] at hi
    rcases hi with hi | rfl
    · exact Nat.lt_succ_of_lt (hb i hi)
    · exact Nat.lt_succ_self _
```

`test/fixture/lean/Fixture.lean`, lines 191–204

## Checks you get for free

Flows are proved by evaluation: `decide` runs the witness through the machine at compile time. You
can do the same for any small fact with `example … := by decide`. The framework's own theorem
`update_unclaimed` gives facts about every input at once: an action whose claim no move of the
app has changes nothing and asks nothing of the host, so an app never has to prove that about a
stray click.

## Presence: the control is there exactly when the move is enabled

A move's `enabled` says when it is available. Whether its control is actually on screen is a
question about the view, so the app proves it: the control's ref is among the view's controls
exactly when the move is enabled. A counter proves it for a
Reset button that is there only when the count is above zero.

The framework's layout and frame theorems (`Frame.controls_ofLaid_layout`) carry that through to
every frame the running app shows: the accessibility tree of the frame, for any text measurements
and any window size.

## Pressable: a click at its centre presses it

Being in the tree isn't enough: another node could be painted over the control, or it could be
laid out with no size. Hit testing is Lean, so this is a theorem too. For a rigid view
([chapter 3](https://cairn.iamnbutler.workers.dev/docs/guide/view-and-layout.md)) the framework reduces it to a condition on the view
alone, `FitsIn`, proved once for every window above a minimum size. A view that isn't rigid,
like the fixture's, is checked one concrete layout at a time: `checkPressable` decides it for a
laid-out frame, and `pressable_of_check` turns that into the theorem. The fuzzer checks that
each enabled move's control is pressable at its centre, in every state it reaches.

The runtime's own theorems take it from there: if the pointer reaches a control at its centre, a
pointer down and up there deliver exactly a press of that control to `update`.

## Invariants

An invariant's proof is the most work in a typical app: `init` for the starting state, then one
obligation per handler, each saying that handler keeps the property. The chapter on
[moves and flows](https://cairn.iamnbutler.workers.dev/docs/guide/moves-and-flows.md#invariants) shows the shape. The fixture's ^7
needs three short lemmas, `add_inv`, `toggle_inv` and `delete_inv`, one per function that changes
the items. A count of items left takes about thirty lines of ordinary list reasoning.

## Runtime checks

Some things are easier to check by running than by proving. `#guard` runs code at compile time;
the fixture's tests drive the real runtime, with clicks found by hit testing and frames through
the real byte encoding:

```lean
def typed : List Event :=
  clickOn (run []) fieldRef ++ [.insertText "  milk ", .key .enter {}, .insertText "eggs"]
def two : List Event := typed ++ clickOn (run typed) addRef

#guard texts (st typed) == [(1, "milk", false)]
#guard texts (st two) == [(1, "milk", false), (2, "eggs", false)]
def toggled : List Event := two ++ clickOn (run two) (toggleRef 1)
#guard texts (st toggled) == [(1, "milk", true), (2, "eggs", false)]
#guard left (st toggled) == 1
def deleted : List Event := toggled ++ clickOn (run toggled) (deleteRef 2)
#guard texts (st deleted) == [(1, "milk", true)]
/-- The buttons under Flash: Top, End, Go to row, Hide rows, then Badge, Clear badge, Announce. -/
def moreRefs : List ControlRef :=
  [topRef, endButtonRef, goRowRef, hideRef, badgeRef, clearBadgeRef, announceRef]
-- Tab order: field, Add, Passcode, Flash, Add above, Add below, the buttons under them, then each
-- item's checkbox, delete button and ⋯, the posts' Like buttons and Refresh (and then the list's
-- rows, `notRow`).
#guard ((tabOrder (run two).laid).map (·.ref)).filter notRow ==
  [fieldRef, addRef, passRef, flashRef, addTopRef, addEndRef] ++ moreRefs ++
  [toggleRef 1, deleteRef 1, moreRef 1, toggleRef 2, deleteRef 2, moreRef 2, likeRef 1, likeRef 2,
   likeRef 3, likeRef 4, refreshRef]
-- Flash sets its timer; the note shows until it fires.
def flashed : List Event := clickOn (run []) flashRef
#guard (st flashed).flash
-- The frame through the v1 boundary carries the keyed controls.
#guard ((decodeFrame (frameBytes Frame.boundary (run two))).map fun f =>
  (f.ax.toList.filterMap (·.control)).filter notRow) ==
  some ([fieldRef, addRef, passRef, flashRef, addTopRef, addEndRef] ++ moreRefs ++
        [toggleRef 1, deleteRef 1, moreRef 1, toggleRef 2, deleteRef 2, moreRef 2, likeRef 1,
         likeRef 2, likeRef 3, likeRef 4, refreshRef])
```

`test/fixture/lean/Fixture/Tests.lean`, lines 27–56

## The rules

These hold for every proof that counts as evidence, and `make check` enforces them:

- **No `sorry`.** An unfinished proof fails the build.
- **Only the standard axioms**: `propext`, `Classical.choice` and `Quot.sound`. The axiom audit
  looks at every theorem.
- **No escape hatches**: `native_decide`, `bv_decide`, `implemented_by`, `debug.skipKernelTC` and
  `axiom` are rejected by a lint, and every declaration is replayed through the kernel.

What a proof still leaves you to trust, and what the other kinds of evidence add, is on
[How much to trust a claim](https://cairn.iamnbutler.workers.dev/docs/reference/trust.md).
For proofs about geometry, `omega` does most of the work, since layout is integers. For bounded
enumerations, `decide +kernel`. For lists of nodes, write recursion structurally: `children.map f`
makes a definition that `rfl` and `decide` can't see through.

From https://cairn.iamnbutler.workers.dev/docs/guide/proving/. All of Cairn's docs for language models: https://cairn.iamnbutler.workers.dev/llms.txt