lemma_unproved: a lemma whose theorem the checker could not prove

A lemma (@[lemma]) states a theorem P in its result type, {Unit | P}. Its body is the proof. The checker proves P at every place the body can return, using what is known there:

• the branch of the if or match that leads to it;
• the facts from lemma calls before it;
• every assert before it that was itself proved.

If one of those returns does not prove, the lemma is unproved. A call to an unproved lemma gives the caller no facts. Nothing is assumed on its word. This is a warning, and an error inside a cap verified module.

An assert inside a lemma is a step of the proof, checked statically. It never runs. A step that can’t be proved is not assumed afterwards, so assert false cannot “prove” anything.

A program that triggers it

mod Main do
  fn cat(xs : List(Int), ys : List(Int)) : List(Int) do
    match xs do
      Nil -> ys
      Cons(h, t) -> Cons(h, cat(t, ys))
    end
  end

  @[lemma]
  fn cat_nil(xs : List(Int)) : {Unit | cat(xs, Nil) == xs} do
    ()
  end

  fn main() : Int do
    0
  end
end

cat(xs, Nil) == xs is true, but proving it needs induction on xs. Unfolding cat once leaves cat(t, Nil) in the goal, which is the same question one element shorter.

The fix

Split the cases with match, and call the lemma itself on the tail. The recursive call is the induction hypothesis. The checker accepts it because cat_nil(t) recurses on a smaller list, so it terminates.

mod Main do
  fn cat(xs : List(Int), ys : List(Int)) : List(Int) do
    match xs do
      Nil -> ys
      Cons(h, t) -> Cons(h, cat(t, ys))
    end
  end

  @[lemma]
  fn cat_nil(xs : List(Int)) : {Unit | cat(xs, Nil) == xs} do
    match xs do
      Nil -> ()
      Cons(_, t) -> cat_nil(t)
    end
  end

  fn main() : Int do
    0
  end
end

When a single step is still too big, state it as an assert before the return. The assert is proved on its own, then used.

Why the rule exists

A lemma never runs, so nothing at run time checks its theorem. Facts from an unproved lemma would be assumptions without evidence, and one false assumption is enough to “prove” any refinement in the program.

See also: the language reference, the lemmas guide, invalid_lemma, lemma_unproved_call.

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.