CODEWITHSUNDEEP
theorem-provinglean
Kevin Buzzard
Kevin Buzzard

Reputation: 537

lean : eq.subst chokes on h:(n=0)

Using Lean, the computer proof checking system.

The first of these proofs succeeds, the second does not.

variables n m : nat

theorem works (h1 : n = m) (h2 : 0 < n) : (0 < m) :=
eq.subst h1 h2

theorem nowrk (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
eq.subst h3 h4

The error occurs in the eq.subst and is the following:

"eliminator" elaborator type mismatch, term
  h4
has type
  0 < n
but is expected to have type
  n < n

[and then some additional information]

I don't understand the error message. I tried various obvious permutations in the hypotheses like 0 = n or n > 0, but I couldn't get it to work, or to produce an error message which I could understand.

Can anyone clarify? I read the part of Theorem Proving In Lean about congr_arg etc but these other commands didn't help me.

Upvotes: 2

Views: 381

Answers (2)

user7396200
user7396200

Reputation: 561

eq.subst relies on higher order unification to compute the motive for the substitution, which is inherently a heuristic and sort of finicky process. Lean's heuristic fails in your second case. (You can see the incorrect motive in the error message.) There are other methods that will do this more intelligently.

Using automation:

theorem nowrk (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
by simp * at * -- this may not work on 3.2.0

theorem nowrk2 (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
by cc

Using rewrite:

theorem nowrk3 (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
by rw h3 at h4; assumption

Using eq.subst and explicitly giving the motive:

theorem nowrk4 (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
@eq.subst _ (λ h, 0 < h) _ _ h3 h4

theorem nowrk4' (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
@eq.subst _ ((<) 0) _ _ h3 h4 -- more concise notation for the above

Using calc mode:

theorem nowrk5 (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
calc 0 < n : h4
   ... = 0 : h3

Using pattern matching:

theorem nowork6 : Π n, n = 0 → 0 < n → 0 < 0
| ._ rfl prf := prf

Upvotes: 3

Adam Kurkiewicz
Adam Kurkiewicz

Reputation: 1642

First, it's a good programming practice to give meaningful names to your functions.

The first lemma could be called subst_ineq_right, or subst_ineq, if it's clear from the context that you always substitute on the right.

Now, in the case of your first lemma, it is unambiguous which term the elaborator will synthesise. Given h1 of type n = m and h2 of type 0 < n, the elaborator does some complicated recursor magic, which substitutes n for m in 0 < n and produces a term of type 0 < m, as required:

lemma subst_ineq (h1 : n = m) (h2 : 0 < n) : (0 < m) :=
    eq.subst h1 h2

This unfortunately fails in your second lemma, say subst_zero_ineq

lemma subst_zero_ineq (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
    eq.subst h3 h4

This is because there is now ambiguity in what term the elaborator will synthesise. It can either substitute n for 0, or 0 for n in 0 < n. For unfathomable reasons, the elaborator chooses to do the latter, producing a term of type n < n. The result is not a term of type 0 < 0, and the proof doesn't type check.

One way to remove the inambiguity is to use subst_ineq in a proof of subst_zero_ineq, for example:

lemma subst_zero_ineq (h3 : n = 0) (h4 : 0 < n) : (0 < 0) :=
    subst_ineq n 0 h3 h4

typechecs correctly.

Upvotes: 2

Related Questions