2

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.

Kevin Buzzard
  • 537
  • 4
  • 11
  • You can use an expanded version of `works` to get `nowrk` to work: ```theorem nowrk (h3 : n = 0) (h4 : 0 < n) : (0 < 0) := @works n 0 h3 h4``` – Adam Kurkiewicz Jul 29 '17 at 13:28
  • Also, [this might be of interest](https://stackoverflow.com/questions/45142007/proving-substitution-property-of-successor-over-equality) – Adam Kurkiewicz Jul 29 '17 at 13:29

2 Answers2

3

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
user7396200
  • 551
  • 3
  • 4
  • Thanks for this answer, `nowrk4` is particularly illuminating when it comes to understanding the function of motive in `eq.subst` – Adam Kurkiewicz Jul 30 '17 at 22:06
  • Is there a manual of tactics available? It doesn't look like the `cc` tactic is covered in the tutorial. – Adam Kurkiewicz Jul 30 '17 at 23:11
  • My understanding is that a comprehensive Lean manual is being written at present and until then we have the three pdf's and the source code to go on. "by cc" just almost crashed my machine, which might not be unrelated to the fact that it's undocumented... – Kevin Buzzard Aug 01 '17 at 04:44
  • tests/lean/run/cc_ac3.lean has cc pwning various things. – Kevin Buzzard Aug 01 '17 at 05:09
2

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.

Adam Kurkiewicz
  • 1,526
  • 1
  • 15
  • 34
  • Many thanks for this. I guess that your answer reveals my underlying question though, which is that in practice I don't want to prove subst_ineq if all I want is subst_zero_ineq. The problem which needs to be solved by the elaborator seems to be "I have something of type n=0 and something of type 0 – Kevin Buzzard Jul 30 '17 at 20:20
  • "It can either substitute n for 0, or 0 for n in 0 < n." This is wrong. The substitution happens left to right; look at the type of `@eq.subst`. – user7396200 Jul 30 '17 at 21:15
  • @RobLewis thanks, you're obviously right. This means my analysis of the problem is somewhat incorrected. The problem is not in what gets substituted, but how `0 < n` gets interpreted as a property. @KevinBuzzard hoped it would be interpreted as a property of n, but it gets interpreted as a property of 0. Is that right? – Adam Kurkiewicz Jul 30 '17 at 21:55
  • I wouldn't phrase it as "a property of 0" or "a property of n." Lean is trying to find a "property" `λ k, ...` that evaluates to `0 < n` when applied to `n`, and `0 < 0` when applied to 0. In principle, Lean has access to all of `h3`, `h4`, and the expected type `0 < 0` when it tries to compute this property. – user7396200 Jul 31 '17 at 13:22