- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我有这样一个函数:
open import Data.Char
open import Data.Nat
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning
foo : Char → Char → ℕ
foo c1 c2 with c1 == c2
... | true = 123
... | false = 456
我想证明,当我用相同的参数 (foo c c
) 调用它时,它总是产生 123
:
foo-eq⇒123 : ∀ (c : Char) → foo c c ≡ 123
foo-eq⇒123 c =
foo c c ≡⟨ {!!} ⟩
123 ∎
我可以使用 refl
来证明一个简单的例子:
foo-example : foo 'a' 'a' ≡ 123
foo-example = refl
所以,我认为我可以将 refl
放入洞中,因为所有 Agda 需要做的就是 beta-reduce foo c c
。但是,用 refl
替换孔会产生以下错误:
.../Unfold.agda:15,14-18
(foo c c
| Relation.Nullary.Decidable.Core.isYes
(Relation.Nullary.Decidable.Core.map′ Data.Char.Properties.≈⇒≡
Data.Char.Properties.≈-reflexive
(Relation.Nullary.Decidable.Core.map′
(Data.Nat.Properties.≡ᵇ⇒≡ (toℕ c) (toℕ c))
(Data.Nat.Properties.≡⇒≡ᵇ (toℕ c) (toℕ c)) (T? (toℕ c ≡ᵇ toℕ c)))))
!= 123 of type ℕ
when checking that the expression refl has type foo c c ≡ 123
我怀疑问题在于 Agda 不会自动理解 c == c
对所有 c
都是 true
:
c==c : ∀ (c : Char) → (c == c) ≡ true
c==c c = refl
.../Unfold.agda:23,10-14
Relation.Nullary.Decidable.Core.isYes
(Relation.Nullary.Decidable.Core.map′ Data.Char.Properties.≈⇒≡
Data.Char.Properties.≈-reflexive
(Relation.Nullary.Decidable.Core.map′
(Data.Nat.Properties.≡ᵇ⇒≡ (toℕ c) (toℕ c))
(Data.Nat.Properties.≡⇒≡ᵇ (toℕ c) (toℕ c)) (T? (toℕ c ≡ᵇ toℕ c))))
!= true of type Bool
when checking that the expression refl has type (c == c) ≡ true
那么,证明我的 foo-eq⇒123
定理的正确方法是什么?
最佳答案
Agda 内置的 Char
类型有点奇怪。让我们将它与一个非奇怪的内置类型 ℕ
进行对比。 ℕ
的相等性测试如下所示。
_≡ᵇ_ : Nat → Nat → Bool
zero ≡ᵇ zero = true
suc n ≡ᵇ suc m = n ≡ᵇ m
_ ≡ᵇ _ = false
请注意,n ≡ᵇ n
也不会归约为 true
。毕竟,Agda 不知道 n
是 zero
还是 suc
,即两个子句中的哪一个要申请归约。因此,这与您的 Char
示例存在相同的问题。但是对于 ℕ
来说,有一个简单的方法。
让我们再次查看您的示例,并添加一个基于 ℕ
的 foo
、bar
版本。
open import Data.Char using (Char ; _==_ ; _≟_)
open import Data.Nat using (ℕ ; zero ; suc ; _≡ᵇ_)
open import Data.Bool using (true ; false)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
open import Relation.Nullary using (yes ; no)
open import Relation.Nullary.Negation using (contradiction)
foo : Char → Char → ℕ
foo c1 c2 with c1 == c2
... | true = 123
... | false = 456
bar : ℕ → ℕ → ℕ
bar n1 n2 with n1 ≡ᵇ n2
... | true = 123
... | false = 456
那么,ℕ
的简单出路是什么?我们在 n
上进行模式匹配/案例拆分以减少 n ≡ᵇ n
刚好 来进行我们的证明。即,要么到基本情况零
,要么到下一个递归步骤suc n
。
bar-eq⇒123 : ∀ n → bar n n ≡ 123
bar-eq⇒123 zero = refl
bar-eq⇒123 (suc n) = bar-eq⇒123 n
ℕ
只有两个构造函数,我们知道 ≡ᵇ
是什么样子,所以模式匹配很简单。
对于Char
,事情要复杂得多。长话短说,Char
的相等性测试是根据函数 toℕ
定义的,Agda 没有给我们定义。此外,Char
数据类型是假设的,没有任何构造函数。所以像 bar-eq⇒123
这样的证明不是 Char
的选项。我们没有子句,也没有构造函数。 (我不会将 'a'
称为 Char
的构造函数。类似于 1234
不是 的构造函数ℕ
.)
那么,我们可以做什么?请注意,您引用的错误消息中的 c == c
简化为涉及 isYes
的相当复杂的内容。如果我们将 c == c
减少一点点(而不是尽可能多),我们会得到 isYes (c ≟ c)
(而不是复杂的错误消息中的内容)。
_≟_
是 Char
的可判定相等性(即“是否相等?” bool 值和证明的组合)。 isYes
去掉证明并给我们 bool 值。
我的证明想法是不对 c
进行案例拆分(就像我们对 ℕ
所做的那样),而是对 c ≟ c
。这将产生两种情况,并将 isYes
分别减少为 true
或 false
。 true
的情况很明显。 false
案例可能会因与可判定等式的证明相矛盾而被驳回。
foo-eq⇒123 : ∀ c → foo c c ≡ 123
foo-eq⇒123 c with c ≟ c
... | yes p = refl
... | no ¬p = contradiction refl ¬p
请注意,反过来,此证明不容易转换为 ℕ
,因为 _≡ᵇ_
不是基于可判定的相等性并且 isYes
。它是原始的。
对于 Char
和 ℕ
,而不是使用 _==_
,也许更好的想法是始终坚持可判定的相等性> 或 _≡ᵇ_
。 foo
将如下所示。
baz : Char → Char → ℕ
baz c1 c2 with c1 ≟ c2
... | yes p = 123
... | no ¬p = 456
foo-eq⇒123
证明将适用于它不变。
关于agda - 如何告诉 Agda 展开一个定义来证明等价性,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/72793516/
所以我试图理解为什么这段代码在 () data sometype : List ℕ → Set where constr : (l1 l2 : List ℕ)(n : ℕ) → sometype
我最近问了这个问题: An agda proposition used in the type -- what does it mean? 并获得了关于如何使类型隐式和获得真正的编译时错误的深思熟虑的
背景:我正在研究 Prabakhar Ragde 的 "Logic and Computation Intertwined" ,对计算直觉逻辑的绝妙介绍。在他的最后一章中,他介绍了使用 Agda 的一
我正在尝试了解 Categories 库,但我对 Agda 还很陌生,所以我正在寻找某种文档来解释在该库的实现中所做的选择。在自述文件中有一个链接到这样的东西,但它坏了。 最佳答案 对于将来登陆这里的
我目前正在 Agda 中实现常规数据结构的衍生物, 如 Conor McBride [5] 的 One-Hole Context 论文中所述。 Löh & Magalhães [3,4] 也在 OHC
阅读 this answer促使我尝试构造并证明多态容器函数的规范形式。构造很简单,但证明让我很困惑。以下是我尝试编写证明的简化版本。 简化版本证明了足够多态的函数,由于参数性,不能仅根据参数的选择来
我正在尝试遵循 McBride 的 How to Keep Your Neighbours in Order 的代码,并且无法理解为什么 Agda(我使用的是 Agda 2.4.2.2)给出以下错误信
在 Agda 中玩证明验证时,我意识到我对某些类型明确使用了归纳原则,而在其他情况下则使用模式匹配。 我终于在维基百科上找到了一些关于模式匹配和归纳原则的文字:“在 Agda 中,依赖类型模式匹配是该
我看到的所有否定,即 A -> Bottom in agda 形式的结论都来自荒谬的模式匹配。还有其他情况可以在agda中获得否定吗?依赖类型理论中是否还有其他可能的情况? 最佳答案 类型理论通常没有
我是 agda 的新手,正在阅读 http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf .我的浅薄知识以某种方式发现点阵图案不是很有必要
我有这样一个函数: open import Data.Char open import Data.Nat open import Data.Bool open import Relation.Bina
我是 Agda 的新手,我认为我在那个范式中仍然有问题需要思考。这是我的问题..我有一个类型 monoid 和一个类型 Group 实现如下: record Monoid : Set₁ where
我对类型理论和依赖类型编程还很陌生,最近正在试验 Agda 的各种功能。以下是我编写的记录类型 C 的一个非常简化的示例,它包含多个组件记录和一些我们可以用来证明事物的约束。 open import
我在 Cubical agda 工作,并试图为以后的证明建立一些通用的实用程序。其中之一是,对于任何类型 A,它与 Σ A (\_ -> Top) 类型“相同”,其中 Top是具有一个元素的类型。问题
我在学习 Agda by tutorial ,现在我正在阅读有关依赖对的信息。 所以,这是代码片段: data Σ (A : Set) (B : A → Set) : Set where _,_
我有以下几点: open import Agda.Builtin.Equality open import Agda.Builtin.Nat renaming (Nat to ℕ) open impo
我是 Agda 的新手,对此感到困惑。 open import Data.Vec open import Data.Nat open import Data.Nat.DivMod open impor
为什么函数组合 (∘) 和应用程序 ($) 有可用的实现 https://github.com/agda/agda-stdlib/blob/master/src/Function.agda#L74-L
我是第一次尝试 Agda,我已经定义了 Bool 数据类型及其基本函数,就像所有教程所说的那样: data Bool : Set where true : Bool false : Bool not
在下面的 Agda 程序中,我收到关于 one 定义中缺少大小写的警告,尽管 myList 仅适合 cons 案例。 open import Data.Nat data List (A : Set)
我是一名优秀的程序员,十分优秀!