关于阿格达的平等

Question

我是Agda的新手。我有以下代码要证明。现在我有问题lemma1c。因为它要我证明z = a时z等于c。我有一个= c和c = c，以及trans函数。所以我试图写

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

但是我想让z不在范围内。我该如何解决？

假定一套：b：A：p：a≡bq：b≡ctrans：∀{ℓ} {A：设置ℓ} {x y z：A}→x≡y→y≡z→x≡z反式反射=反射lemma0：c≡clemma0 =反映-目标：c≡c，反射：x≡xlemma1a：a≡clemma1a重写p = qlemma1c：∀{z：A}→z≡a→z≡clemma1c {z} =反式{} {lemma1a}

Answer 1

您必须使用显式参数（不带括号）调用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

Answer 2

弯括号用于标记隐式参数。也就是说，通常Agda可以从上下文中得出的参数-例如，通过将依赖类型的x ≡ y传递给trans，您已经告诉Agda什么是ℓ，A，x和y。同样，通过将{z}标记为隐式参数，您不需要将其显式传递给lemma1c，并且通常不需要在lemma1c {z} = ...行上将其匹配。