问精益高尔夫小贴士

EN

介绍

如果您刚刚完成了自然数游戏，您可能熟悉intro的策略，这可以用来创建含义/函数。然而，这种策略很少是最高明的。

如果你的介绍是你证明的第一部分，那么隐含的表达可能会更好。比较：

def q:list ℕ→ℕ:=by{intro x,induction x,exact 0,exact x_hd+x_ih}

使用

def q(x:list ℕ):ℕ:=by{induction x,exact 0,exact x_hd+x_ih}

这常常是你最好的选择。但是，如果可以推断函数的类型，则还有其他选项。

def f:ℕ→ℕ:=by{intro x,exact x+3}
def f(x:ℕ):ℕ:=by{exact x+3}
def f:=λx,by{exact x+3}
def f(x):=by{exact x+3}

这些是按长度排序的，因此隐式forall (最后一个选项仍然是隐式的)是最短的。但是，如果函数是提交的，lambda可以将def f:=表达式删除，使其在这种情况下是最短的。

使用by而不是begin ... end

by可以短于begin和end。

def foo(m:ℕ):m=m:=begin refl,end

长于

def bar(m:ℕ):m=m :=by refl

你也可以用它来做多个战术，但是你需要用支撑套住战术，就像小麦向导指出的那样。例如，by{rw add_assoc,refl}比begin rw add_assoc,refl end短。

;和<|>组合子.

;使得由最后一个策略创建的所有子目标都应用了下一个策略；例如，lemma asda (n : ℕ) : n = n := by { induction n; refl }是一个有效的证明。作为奖励，它还允许您不使用大括号(例如def k(n:ℕ):n=n:=by induction n;refl)。

<|>更加利基，但仍然很有用；它允许您执行一种策略，如果它失败，则另一种策略则相反。它也不允许大括号(虽然这比,长，所以不那么有用)。例如：

example(x):0+x=x:=by induction x;refl<|>rw nat.zero_add