Agda：重写子表达式答案

【问题标题】：Agda: rewrite subexpressionAgda：重写子表达式
【发布时间】：2020-10-23 02:32:51
【问题描述】：

我试图证明：

AddTodoSetsNewCompletedToFalse :
  ∀ {n : ℕ} (todos : Vec Todo (1 + n)) (text : String) →
    Todo.completed (last (AddTodo todos text)) ≡ false
AddTodoSetsNewCompletedToFalse todos text = ?

在哪里

AddTodoLastAddedElementIsTodo :
  ∀ {a} {A : Set a} {n} (todos : Vec Todo n) (text : String) →
    last (AddTodo todos text) ≡ 
      record
        { id        = 1
        ; completed = false
        ; text      = text
        }
AddTodoLastAddedElementIsTodo todos text = vecLast todos

和

vecLast : ∀ {a} {A : Set a} {l n} (xs : Vec A n) → last (xs ∷ʳ l) ≡ l
vecLast []       = refl
vecLast (_ ∷ xs) = P.trans (prop (xs ∷ʳ _)) (vecLast xs)
  where
    prop : ∀ {a} {A : Set a} {n x} (xs : Vec A (suc n)) → last (x ∷ xs) ≡ last xs
    prop xs with initLast xs
    ...        | _ , _ , refl = refl

我尝试使用rewrite 并得到：

AddTodoSetsNewCompletedToFalse :
  ∀ {a} {A : Set a} {n} (todos : Vec Todo n) (text : String) →
    Todo.completed (last (AddTodo todos text)) ≡ false
AddTodoSetsNewCompletedToFalse todos text rewrite AddTodoLastAddedElementIsTodo todos text = refl

但错误：

_a_100 : Agda.Primitive.Level

出现了。

我不确定如何解决这个问题。来自here 我知道这与隐式参数有关。但不知道如何解决它

这种错误表示未解决的元变量，这意味着 Agda 无法推断出隐式参数

谢谢！

【问题讨论】：

标签： agda

【解决方案1】：

您不要将A 用于AddTodoSetsNewCompletedToFalse 类型的任何内容。另外，这不是错误，而是未解决的元数据。

所以发生的情况是，无论您使用AddTodoSetsNewCompletedToFalse，参数或结果类型中的任何内容都不会限制A（以及随后的a）的选择，因此统一器无法解决这些元变量。您可以通过写 AddTodoSetsNewCompletedToFalse {a = _} {A = _} 并观察这两个元数据未解决来明确发生了什么。

您应该简单地从AddTodoSetsNewCompletedToFalse 的类型中删除前两个参数（a 和A）。

【讨论】：