proof - agda 的检查功能是如何工作的？

In lại 作者：行者123 更新时间：2023-12-04 04:43:21 25 4

crazy : ℕ -> ℕ
crazy 0 = 10
crazy 1 = 0
crazy 2 = 0
crazy 3 = 1
crazy 4 = 0
crazy xxx = xxx

safebad : {nn : ℕ} -> (crazy nn) ≢ 0 -> Fin (crazy nn)
safebad {1} hh with hh refl
... | ()
safebad {2} hh with hh refl
... | ()
safebad {4} hh with hh refl
... | ()
safebad {0} hh = # 0
safebad {3} hh = # 0
safebad {suc (suc (suc (suc (suc _))))} _ = # 0

safegood : (nn : ℕ) -> (crazy nn) ≢ 0 -> Fin (crazy nn)
safegood nn nez with crazy nn | inspect crazy nn
... | 0 | [ proof ] = ⊥-elim ???
... | _ | _ = # 0

safegood nn nez with crazy nn
... | w = ?

safegood nn nez with crazy nn
... | zero = ?
... | suc w = ?

safegood nn nez with crazy nn
... | zero = ⊥-elim (nez refl)
... | suc w = ?

open Deprecated-inspect
  renaming (inspect to inspect′)

safegood₂ : (nn : ℕ) → crazy nn ≢ 0 → Fin (crazy nn)
safegood₂ nn nez with inspect′ (crazy nn)
... | zero with-≡ eq = ⊥-elim (nez eq)
... | suc _ with-≡ eq = ?

safegood : (nn : ℕ) → crazy nn ≢ 0 → Fin (crazy nn)
safegood nn nez with crazy nn | inspect crazy nn
... | 0 | [ proof ] = ⊥-elim (subst (λ x → x ≢ 0) (sym proof) nez proof)
... | _ | _ = ?

25 4 0

• agda - Agda 如何确定类型是不可能的

  所以我试图理解为什么这段代码在 () data sometype : List ℕ → Set where constr : (l1 l2 : List ℕ)(n : ℕ) → sometype

• Agda (Agda):如何获得依赖类型的值？

  我最近问了这个问题: An agda proposition used in the type -- what does it mean? 并获得了关于如何使类型隐式和获得真正的编译时错误的深思熟虑的

• agda - Agda 中类型归属的一般形式是什么？

  背景:我正在研究 Prabakhar Ragde 的 "Logic and Computation Intertwined" ，对计算直觉逻辑的绝妙介绍。在他的最后一章中，他介绍了使用 Agda 的一

• agda - Agda 类别库的背景？

  我正在尝试了解 Categories 库，但我对 Agda 还很陌生，所以我正在寻找某种文档来解释在该库的实现中所做的选择。在自述文件中有一个链接到这样的东西，但它坏了。 最佳答案 对于将来登陆这里的

• agda - Agda 中数据结构的导数

  我目前正在 Agda 中实现常规数据结构的衍生物， 如 Conor McBride [5] 的 One-Hole Context 论文中所述。 Löh & Magalhães [3,4] 也在 OHC

• agda - Agda 中的参数化利用证明

  阅读 this answer促使我尝试构造并证明多态容器函数的规范形式。构造很简单，但证明让我很困惑。以下是我尝试编写证明的简化版本。 简化版本证明了足够多态的函数，由于参数性，不能仅根据参数的选择来

• agda - Agda 中实例参数的问题

  我正在尝试遵循 McBride 的 How to Keep Your Neighbours in Order 的代码，并且无法理解为什么 Agda(我使用的是 Agda 2.4.2.2)给出以下错误信

• agda - Agda 中通过归纳原理定义的函数

  在 Agda 中玩证明验证时，我意识到我对某些类型明确使用了归纳原则，而在其他情况下则使用模式匹配。 我终于在维基百科上找到了一些关于模式匹配和归纳原则的文字:“在 Agda 中，依赖类型模式匹配是该

• agda - Agda 中的非平凡否定

  我看到的所有否定，即 A -> Bottom in agda 形式的结论都来自荒谬的模式匹配。还有其他情况可以在agda中获得否定吗？依赖类型理论中是否还有其他可能的情况？ 最佳答案 类型理论通常没有

• agda - 忽略 Agda 中的点模式会出现什么问题？

  我是 agda 的新手，正在阅读 http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf .我的浅薄知识以某种方式发现点阵图案不是很有必要

• agda - 如何告诉 Agda 展开一个定义来证明等价性

  我有这样一个函数: open import Data.Char open import Data.Nat open import Data.Bool open import Relation.Bina

• agda - 在 Agda 中应用规则

  我是 Agda 的新手，我认为我在那个范式中仍然有问题需要思考。这是我的问题..我有一个类型 monoid 和一个类型 Group 实现如下: record Monoid : Set₁ where

• agda - 在 Agda 中用证明无关的等价关系重写？

  我对类型理论和依赖类型编程还很陌生，最近正在试验 Agda 的各种功能。以下是我编写的记录类型 C 的一个非常简化的示例，它包含多个组件记录和一些我们可以用来证明事物的约束。 open import

• agda - 立方体 agda 中针对特定计算行为的路径与等价关系

  我在 Cubical agda 工作，并试图为以后的证明建立一些通用的实用程序。其中之一是，对于任何类型 A，它与 Σ A (\_ -> Top) 类型“相同”，其中 Top是具有一个元素的类型。问题

• agda - 在 Agda 中使用依赖对的问题

  我在学习 Agda by tutorial ，现在我正在阅读有关依赖对的信息。 所以，这是代码片段: data Σ (A : Set) (B : A → Set) : Set where _,_

• agda - 为什么 Agda 需要在这里进行模式匹配

  我有以下几点: open import Agda.Builtin.Equality open import Agda.Builtin.Nat renaming (Nat to ℕ) open impo

• agda - 为什么下面的 Agda 代码不会进行类型检查？

  我是 Agda 的新手，对此感到困惑。 open import Data.Vec open import Data.Nat open import Data.Nat.DivMod open impor

• agda - 为什么函数组合和应用程序在 Agda 中有依赖实现？

  为什么函数组合 (∘) 和应用程序 ($) 有可用的实现 https://github.com/agda/agda-stdlib/blob/master/src/Function.agda#L74-L

• agda - 这个 Agda 错误是什么？

  我是第一次尝试 Agda，我已经定义了 Bool 数据类型及其基本函数，就像所有教程所说的那样: data Bool : Set where true : Bool false : Bool not

• agda - 我可以使用值的范式来避免 Agda 中不完整的模式匹配吗？

  在下面的 Agda 程序中，我收到关于 one 定义中缺少大小写的警告，尽管 myList 仅适合 cons 案例。 open import Data.Nat data List (A : Set)