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.
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