∀a b. a+b=b+a

Question

这个问题是精益 LotM的一部分。

环是一种结构，它采用我们熟悉的加法和乘法规则，并对它们进行抽象，这样我们就可以对它们进行推理。为了做到这一点，我们将许多预期的属性描述为公理，看看我们可以对遵循这些公理的系统说些什么。例如，a + (b + c) = (a + b) + c是通常给出的公理之一。

但是，环公理究竟是什么，取决于你问谁。因为，环可以用许多等价的方法来定义。通常，给定的公理之一是对于任何a和b，然后是a + b = b + a。我们称之为相加交换性。然而，这个公理是不需要的！通常我们可以用更基本的公理来证明它。

在这个挑战中，我将在精益编程语言中给出环的最小公理集，您的任务是证明交换性。

ring类定义如下：

universe u

class ring (α : Type u) extends has_add α, has_mul α, has_one α, has_zero α, has_neg α :=
  ( add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c )
  ( mul_assoc : ∀ a b c : α, a * (b * c) = (a * b) * c )
  ( add_left_id : ∀ a : α, 0 + a = a )
  ( mul_left_id : ∀ a : α, 1 * a = a )
  ( mul_right_id : ∀ a : α, a * 1 = a )
  ( add_left_inv : ∀ a : α, (-a) + a = 0 )
  ( left_distribute : ∀ a b c : α, a * (b + c) = a * b + a * c )
  ( right_distribute : ∀ a b c : α, (a + b) * c = a * c + b * c)

open ring

您的目标是创建一个与以下类型相同的对象：

axiom add_comm {α : Type*} [ring α] : ∀ a b : α, a + b = b + a 

这与证明索赔相同。

只要基础类型正确，您可以在这里重命名任何东西。因此，下面是一个较小但完全有效的证明头：

def k{A:Type*}[ring A]:∀a b:A,a+b=b+a

你不能使用不同但相似的类型。因此，例如，重新定义=的表示法以使证明变得简单：

local notation a `=` b := true
def k{A:Type*}[ring A]:∀a b:A,a+b=b+a := λ x y, trivial

不是有效的答案，即使类型看起来是相同的。(感谢埃里克指出了这种可能的漏洞。)

您必须实际证明索赔，这样您就不能在证明中使用sorry或axiom。

这是密码-高尔夫，所以答案将以字节为单位得分，目标是更少的字节。

如果您想进行这个挑战，但不知道从哪里开始，只需使用LotM帖子中的链接即可。我很乐意在聊天的时候帮忙。

Answer 1

精益，268个字节

import tactic.cache
def k{A}[r:ring A](a b:A):a+b=b+a:=by{casesI
r with _ _ _ _ _ c _ d _ _ e f,let g:=λa:A,trans(by
simp*:_=-(a+-a)+(a+-a+a+-a))$by
simp[<-c,*],let:=λa,trans(by
rw[<-c,e,g]:a+b+_=a+(-a+a))$by
rw[c,g,d],transitivity-a+(1+1)*(a+b)+-b,rw f,simp*,simp*}

使用精益编辑器运行