时间戳

首页 > 解决方案 > 关于 Agda 中的平等

functional-programming - 关于 Agda 中的平等

问题描述

我是阿格达的新手。我有以下要证明的代码。现在我对lemma1c有问题。因为它要我证明当 z = a 时，z 将等于 c。我有 a = c 和 c = c，还有 trans 函数。所以我试图写

lemma1c = trans {z = a}, {a = c}

但我想得到 z is not in scope 错误。我该如何解决这个问题？

假定
  一套
  一个：一个
  乙：一个
  丙：一个
  p : a ≡ b
  q : b ≡ c
  trans : ∀ {ℓ}{A : Set ℓ}{xyz : A} → x ≡ y → y ≡ z → x ≡ z
  反式 refl refl = refl

  引理0 : c ≡ c
  引理0 = refl
  -- 目标：c ≡ c，参考：x ≡ x
  引理1a : a ≡ c
  lemma1a 重写 p = q

  引理1c : ∀ {z : A} → z ≡ a → z ≡ c
  lemma1c {z} = 反式 {} {lemma1a}

标签： functional-programmingagda

解决方案

您必须trans使用显式参数（不带括号）调用函数，这会导致以下定义：

lemma1c : ∀ {z : A} → z ≡ a → z ≡ c
lemma1c z≡a = trans z≡a lemma1a

你也可以rewrite像在前面的引理中那样使用：

lemma1d : ∀ {z : A} → z ≡ a → z ≡ c
lemma1d z≡a rewrite lemma1a = z≡a

推荐阅读