does lean use the proof of a lemma when applying it?

Stream: new members

[rzeta0]

I think I read somewhere that Lean uses the proof of a lemma when applying it.

That is, the statement of variables and conclusion (proposition) on the first line of a lemma definition are not sufficient.

I would therefore expect the following code to produce an error - but it reports no errors. It seems the example successful uses the lemma Nat.le_or_succ_le even though it has no proof!

import Mathlib.Tactic

lemma Nat.le_or_succ_le (a b: ℕ): a ≤ b ∨ b + 1 ≤ a := by
  --rw [Nat.succ_le]
  --exact le_or_lt a b
  sorry

example {a : ℕ} :  a ≤ 2 ∨ 3 ≤ a  := by
  apply Nat.le_or_succ_le a 2

I'd be grateful for a clarification.

Even if sorry suppresses errors, how would the internal compilation work if the lemma actually has no proof?

[Kyle Miller]

No, applying theorems and lemmas never will look at the proofs.

[Kyle Miller]

The type of the theorem/proof (that is, the statement of variables and the conclusion, what you see when you hover over Nat.le_or_succ_le or when you do #check Nat.le_or_succ_le) is all that is considered.

[Kyle Miller]

Another experiment you can do is use axiom instead of lemma.

[Kyle Miller]

In contrast, sometimes processes in Lean will unfold a definition when type checking.

[Kyle Miller]

(I think that the main place that happens is when a definition appears in the type of something.)

[rzeta0]

I'm surprised !

So for very large complex multi-part proofs, how does Lean ensure that one part of the proof didn't use an unproven lemma?

Is there a switch or option which tells lean to throw up an error if it finds an unjustified lemma?

[Kyle Miller]

I think the answer is that sorry is not an unfinished proof, it's invoking the "sorry axiom" sorryAx. This axiom lets you prove anything. It's by convention that we treat this as an unfinished proof.

Also, sorry logs a warning, so you can't miss that it was used. You can see if a theorem depends on a theorem making use of sorry by using #print axioms theTheoremYouCareAbout

[Kevin Buzzard]

Just to be clear here -- the proofs using other sorried results compile, but the sorry is viral in the sense that print axioms will always remember any sorry used anywhere along the way.