如何在精益中证明a =b a+ 1 = b + 1？

作者: 布偶的表弟派大星丶
发布时间: 2024-01-12 06:54:19 (3月前)
转自：

4 条回复

0#
回复此人
v-star*위위 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 你可以使用 <a href="https://github.com/leanprover/lean/blob/d315e424ff17faf6fe096a0a1407b70193009726/library/init/logic.lean#L83" rel="nofollow noreferrer"> <code> congr_arg </code> </A> 引理 </p> <pre> <code> lemma congr_arg {�� : Sort u} {�� : Sort v} {a? a? : ��} (f : �� ) : a? = a? �� f a? = f a? </code> </pre> <P> 这意味着如果为函数提供相等的输入，输出值也将相等。 </p> <P> 证据如下： </p> <pre> <code> example (a b : nat) (H : a = b) : a + 1 = b + 1 := congr_arg (�� n, n + 1) H </code> </pre> <P> 请注意，精益能够推断出我们的功能 <code> �� n, n + 1 </code> ，所以证明可以简化为 <code> congr_arg _ H </code> 。 </p> </DIV>

编辑
1#
回复此人
记忆只剩空城 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 更一般：a = b - ＆gt;环中的a + c = b + c </p> <pre> <code> import algebra.ring open algebra variable {A : Type} variables [s : ring A] (a b c : A) include s example (a b c : A) (H1 : a = b) : a + c = b + c := eq.subst H1 rfl </code> </pre> </DIV>

编辑
2#
回复此人
一腔诗意喂了狗 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 而 <code> congr_arg </code> 一般来说这是一个很好的解决方案，这个具体的例子确实可以解决 <code> eq.subst </code> +更高阶的统一（其中 <code> congr_arg </code> 在内部使用）。 </p> <pre> <code> example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := eq.subst H1 rfl </code> </pre> </DIV>

编辑

登录后才能参与评论