用减法证明等价性

Question

我正在学习精益，并且正在研究一个非常简单的例子：

def toFin6 (n:Nat) : Fin 6 :=
  if p:n < 6 then { val := n, isLt := by exact p }
  else
    toFin6 (n - 1)
  decreasing_by
    simp_wf
    induction n
    /- n = 0 -/
    contradiction
    /- n > 0 -/
    sorry

我很欣赏有更简单的方法将

Nat

转换为

Fin X

类型。但是，这不是重点。我被困在这里，目标实际上是这样的：

theorem p (n:Nat) : Nat.succ n - 1 == n :=
by 
  sorry

从逻辑上讲，这似乎很简单：

(n+1)-1 == n

。另外，我知道我可以按如下方式解决此问题：

import Mathlib.Tactic.Linarith

theorem p (n:Nat) : Nat.succ n - 1 == n :=
by 
  simp

好的，但是如何在没有

simp

的情况下仅使用前奏中的基本战术来做到这一点？ 似乎

Nat.succ_sub_one

在这里可能有用。

Answer 1

好吧，所以我最终想出了这个：

theorem p (n:Nat) : Nat.succ n - 1 = n :=
by
  rw [Nat.succ_sub_succ]
  rw [Nat.sub_zero]

只有通过 VS 代码补全，我才发现了这些策略。有没有他们的名单？