- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
在 Cubical Agda 的标准库中,有 finite multisets我在下面复制了其优雅的定义:
{-# OPTIONS --cubical --safe #-}
open import Cubical.Foundations.Prelude
infixr 20 _∷_
data FMSet (A : Set) : Set where
[] : FMSet A
_∷_ : (x : A) → (xs : FMSet A) → FMSet A
comm : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
trunc : isSet (FMSet A)
_++_ : ∀ {A : Set} -> FMSet A → FMSet A → FMSet A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
comm x y xs i ++ ys = comm x y (xs ++ ys) i
trunc xs1 xs2 p q i j ++ ys =
trunc (xs1 ++ ys) (xs2 ++ ys) (cong (_++ ys) p) (cong (_++ ys) q) i j
[]
是一个右中性元素,使用抽象引理
FMSetElimProp.f
我不明白。因此,我试图直接证明,但我被卡住了。这是我的尝试:
unitr-++ : ∀ {A : Set} (ys : FMSet A) → ys ++ [] ≡ ys
unitr-++ [] = refl
unitr-++ (y ∷ ys) = cong ((y ∷_)) (unitr-++ ys)
unitr-++ (comm x y xs i) = cong₂ {!comm x y!} (unitr-++ xs) refl
unitr-++ (trunc xs1 xs2 p q i j) = {!!}
最佳答案
回答这个问题的两个 SO 问题是 this one for comm
和 this one for trunc
.和你一样,我也遇到过同样的挫折:如果所有这些类型都是 Set
s,为什么我需要写任何东西,更不用说复杂的东西了,来证明一些2路径?!?!
所以,首先,从第一个链接的答案开始,让我们从
comm x y xs i ++ ys = ?
Goal:
comm x y (xs ++ []) i ≡ comm x y xs i
comm x y (xs ++ []) ≡ comm x y xs
只需
xs + [] ≡ xs
感应地。所以,让我们问一下,这到底会给我们带来什么。把
cong (comm x y) (unitr-++ xs)
并询问它的类型:
Have:
PathP
(λ i → x ∷ y ∷ unitr-++ xs i ≡ y ∷ x ∷ unitr-++ xs i)
(comm x y (xs ++ [])) (comm x y xs)
Square
正是这些面孔:
isSet→isSet' trunc
(comm x y (xs ++ []))
(comm x y xs)
(λ j → x ∷ y ∷ unitr-++ xs i)
(λ j → y ∷ x ∷ unitr-++ xs i)
unitr-++ (comm x y xs i) j = isSet→isSet' trunc
(comm x y (xs ++ []))
(comm x y xs)
(λ j → x ∷ y ∷ unitr-++ xs j)
(λ j → y ∷ x ∷ unitr-++ xs j)
j i
unitr-++ (trunc xs1 xs2 p q i j)
r : Cube ? ? ? ? ? ?
r = cong (cong unitr-++) (trunc xs1 xs2 p q)
C-c C-s
在所有六个面孔中,Agda 告诉我们:
r : Cube (λ i j → trunc xs1 xs2 p q i j ++ [])
(λ i j → unitr-++ xs1 j)
(λ i j → unitr-++ xs2 j)
(λ i j → trunc xs1 xs2 p q i j)
(λ i j → unitr-++ (p i) j)
(λ i j → unitr-++ (q i) j)
Set
s 也是
Groupoid
s 的事实,正如
hLevelSuc 2 _
所见证的那样):
unitr-++ (trunc xs1 xs2 p q i j) = isGroupoid→isGroupoid' (hLevelSuc 2 _ trunc)
(λ i j → trunc xs1 xs2 p q i j ++ [])
(λ i j → unitr-++ xs1 j)
(λ i j → unitr-++ xs2 j)
(λ i j → trunc xs1 xs2 p q i j)
(λ i j → unitr-++ (p i) j)
(λ i j → unitr-++ (q i) j)
i
j
FMSetElimProp
做。它实现了上述所有这些机制,对于
FMSet
具体来说,但对于所有功能和这些功能的所有属性,一举两得。所以你不必看这个答案和两个链接的答案,然后一遍又一遍地做所有这些,实际上最后它不应该有任何区别,因为所有构建的路径都是路径等效的反正。
关于proof - 有限多重集作为 Cubical Agda 中的 HIT,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/58154559/
所以我试图理解为什么这段代码在 () 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)
我是一名优秀的程序员,十分优秀!