2

假设以下定义：

def app {α : Type} : Π{m n : ℕ}, vector α m → vector α n → vector α (n + m)
    | 0 _ [] v                   := by simp [add_zero]; assumption
    | (nat.succ _) _ (h :: t) v' := begin apply vector.cons,
                                              exact h,
                                          apply app t v'
                                    end

请注意(n + m)在定义中翻转，以免插入add_symm定义。另外，请记住，这add / +是在精益中的 rhs 上定义的。vector是一个手工滚动的 nil / cons 定义的长度索引列表。

所以无论如何，首先我们有一个引理，它从定义中得出：

theorem nil_app_v {α : Type} : ∀{n : ℕ} (v : vector α n),
    v = [] ++ v := assume n v, rfl

现在我们有一个不符合定义的引理，因此我用eq.rec它来制定它。

theorem app_nil_v {α : Type} : ∀{n : ℕ} (v : vector α n),
    v = eq.rec (v ++ []) (zero_add n)

请注意，这eq.rec只是C y → Π {a : X}, y = a → C a.

通过对 的归纳，证明的想法是微不足道的v。基本案例紧随定义，递归案例应紧随归纳假设和定义，但我无法说服 Lean 相信这一点。

begin
  intros n v,
  induction v,
    -- base case
    refl,
    -- inductive case
end

我从 Lean 得到的归纳假设是a_1 = eq.rec (a_1 ++ vector.nil) (zero_add n_1).

我如何将它与结论一起使用a :: a_1 = eq.rec (a :: a_1 ++ vector.nil) (zero_add (nat.succ n_1))？我可以unfold app将术语减少a :: a_1 ++ vector.nil到a :: (a_1 ++ vector.nil)，现在我被卡住了。

4

0 回答 0