如何证明瘦= a = b→a + 1 = b + 1? [英] How to prove a = b → a + 1 = b + 1 in lean?
问题描述
我正在研究精简教程的第4章.
我希望能够证明简单的等式，例如a = b → a + 1 = b + 1 无需，而不必使用calc环境.换句话说，我想明确地构造以下证明项:
I'd like to be able to prove simple equalities, such as a = b → a + 1 = b + 1 without having to use the calc environment. In other words I'd like to explicitly construct the proof term of:
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry
我的最佳猜测是，我需要使用eq.subst和有关标准库中自然数相等的一些相关引理，但是我很茫然.我能找到的最接近的精益示例是:
My best guess is that I need to use eq.subst and some relevant lemma about equality on natural numbers from the standard library, but I'm at loss. The closest lean example I can find is this:
example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2
example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b :=
eq.subst H1 H2
推荐答案
虽然congr_arg通常是一个很好的解决方案，但确实可以通过eq.subst +高阶统一(congr_arg使用内部).
While congr_arg is a good solution in general, this specific example can indeed be solved with eq.subst + higher-order unification (which congr_arg uses internally).
example (a b : nat) (H1 : a = b) : a + 1 = b + 1 :=
eq.subst H1 rfl
这篇关于如何证明瘦= a = b→a + 1 = b + 1?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
