invalid_lemma: a @[lemma] that cannot be a theorem

A lemma is a function marked @[lemma]. Its result type, {Unit | P}, states a theorem P about its parameters, and its body is the proof. A lemma never runs: the compiler removes every lemma and every call to one before the program is built. So a lemma has to follow five rules, numbered as in the message:

• L1. Its result type is {Unit | P}, and P does not mention the unit value _.
• L2. Its body is total and pure. It has no effects (println, send, spawn), no failure path (panic, todo, a typed hole, a division the checker can’t prove safe), no match that might not match, and no lambdas. It never binds a parameter’s name again, with a let or a pattern: the theorem is about the parameters as passed in, so let n = 0 must not make n == 0 look true. An assert is allowed. Inside a lemma it is a step of the proof, checked statically, never at run time.
• L3. It calls only reflected functions, other lemmas, constructors, and the builtins the logic knows (arithmetic, comparisons on Int and Float, &&, ||, not).
• L4. If it is recursive, the checker can prove the recursion terminates. Its recursive call is used as the induction hypothesis.
• L5. It is only ever called, never used as a value. It carries none of @[opaque], @[measure], @[diverges], @[trusted] or @[assume].

A program that triggers it

mod Main do
  @[lemma]
  fn bogus(n : Int) : {Unit | n == n + 1} do
    panic("unreachable")
  end

  fn main() : Int do
    0
  end
end

bogus breaks L2. Its only path ends in panic, so on every path where it “returns”, anything holds. Since a lemma never runs, nothing would ever catch the false theorem.

The fix

State something true, and prove it with a body that returns ():

mod Main do
  @[lemma]
  fn plus_zero(n : Int) : {Unit | n + 0 == n} do
    ()
  end

  fn main() : Int do
    0
  end
end

Why the rule exists

A lemma’s theorem becomes a fact at every call, with no runtime check behind it. Every rule closes one way to “prove” something false:

• a failure path proves anything on that path (L2);
• an effect would be lost when the call is removed (L2);
• an unknown callee has no definition to reason with (L3);
• an induction hypothesis over a recursion that may not terminate is circular (L4);
• a lemma used as a value would need to exist at run time (L5).

See also: the language reference, the lemmas guide, lemma_unproved, invalid_measure.

Scoped assert … by blocks use this diagnostic too. Their hints must be total and pure; only a proved goal becomes a fact outside the block. See scoped proof hints.