等式证明中的模式匹配(解构)

文章/答案/技术大牛

发布

1回答

idris

data T = A String | B String p : ((A s) = (A s')) -> (s = s') 如果我有(A s) = (A s')，如何获取s = s' 附言:我是伊德里斯的新手请随时编辑我的代码样式问题或添加相关的关键字。

浏览 12提问于2021-04-14得票数 1

回答已采纳

1回答

全函数中的等式证明与模式匹配

idris

我知道这是一个有点做作的例子，但我想知道如何使以下函数合计：foo 10 = 10Main.foo is not total as there are missing cases将impossible分支添加到HTNWs答案我得到的类型检查是这样的： total foo

浏览 13提问于2018-03-05得票数 1

回答已采纳

1回答

在Agda中忽略点模式会出什么问题？

agda

我是agda和阅读的新手。我的浅薄知识不知怎的发现点图案不太必要。可以很好地定义为inv _ _ (im x) = x我对coq比较熟悉，也不知道coq中有类似的东西。

浏览 0提问于2018-01-02得票数 3

回答已采纳

1回答

Agda:我能证明具有不同构造函数的类型是不相交的吗？

functional-programming、agda、dependent-type

如果我试图证明Nat和Bool在Agda中不相等： open import Data.Natopen import Data.Emptynoteq () 我得到了错误： Failed to solve the following constraints: Is empty: ℕ ≡ Bool 我知道不可能对类型本身进行模式匹配，但令我惊讶的是，编译器没有看到Nat和Bool具有不同的(类型)构造函

浏览 14提问于2020-01-13得票数 4

回答已采纳

1回答

什么是公理K？

pattern-matching、programming-languages、agda、dependent-type

我注意到自从HoTT以来，关于"Axiom K“的讨论越来越多。我相信这与模式匹配有关。我很惊讶在TAPL、ATTAPL或PFPL中找不到引用。什么是Axiom K？是否用于ML风格的模式匹配，就像在SML中一样(或者仅仅是dependent pattern 作为Axiom K的适当参考？

浏览 88提问于2016-08-31得票数 37

回答已采纳

1回答

subSetoid的类型

agda

函数是否有一种方法来要求两个Setoids，其中第一个Setoid中的相等意味着后者中的相等？当然，这需要两个Setoid共享它们的Carrier，而Carrier不是一个参数，而是一个记录字段。类型检查器拒绝了请求Carrier等式的天真尝试： ({x这不起作用，因为我们在等式证明上不

浏览 3提问于2014-01-16得票数 1

回答已采纳

1回答

为什么模式匹配有时在Agda中是“必不可少的”？

pattern-matching、agda、theorem-proving

为什么模式匹配有时在Agda中是“必不可少的”？η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ wPLFA的文本说：左侧的模式匹配是必不

浏览 1提问于2019-09-06得票数 2

回答已采纳

2回答

立方体Agda:如何证明两件不相等的东西

agda、cubical-type-theory

在立体Agda中，我如何证明两件事是不平等的？NATURAL ℕ #-} pos : ℕ → ℤ congZero : pos 0 ≡ neg 0oddThing2 : pos 0 ≡ congZero i1我发现了一个相当难看

浏览 6提问于2020-04-26得票数 4

回答已采纳

1回答

agda中的参:解释同余性质

equality、agda

有了以下相等的定义，我们就有了refl作为构造函数。data _≡_ {a} {A : Set a} (x : A) : A → Set a where并且我们可以证明函数在等式上是一致的。我认为我们是在隐藏参数上进行模式匹配:如果我们用另一个标识符替换第一次出现的情况，就会得到一个类型错误。在模式匹配之后，我认为m和n的定义是相同的。然后魔术发生了(应用了关系功

浏览 0提问于2014-11-23得票数 7

回答已采纳

1回答

解构是模糊的

c#、c#-7.3

我有一个向量类，有两个解构方法，如下所示：{foo.Deconstruct( out Vector2 dir, out double len );

浏览 0提问于2019-04-19得票数 15

回答已采纳

1回答

我需要异构的平等吗？

equality、proof、agda、dependent-type、heterogeneous

简要背景:我正在使用de索引实现上下文和重命名，然后用“未定义”的名称(书面ε)扩展这些概念。未定义的名称对Γ中的名称以及Γ和Γ‘之间的重命名都会产生偏序。在重命名(get)中查找一个名称，并查找一个相关的函数put，它以一种特定的方式反转get，从而生成一个(相当琐碎的) Galois连接。我现在要做的是展示get和put之间形成了Galois连接。一种方法是证明每个函数都是单调的</em

浏览 4提问于2014-05-11得票数 1

回答已采纳

1回答

模式匹配中的元组解构

c#、c#-10.0

经过长时间的休息之后，我正在研究c#中的新内容，并试图了解泛型类型匹配是如何工作的。同时，我想知道是否有可能解构模式中的元组，例如：{ ValueTuple<int, int> t => $"int point

浏览 3提问于2022-02-18得票数 0

回答已采纳

2回答

替换参数剥离它不应该使用的空间

regex、powershell

我对以下替换声明有一个理解上的问题。'Select {0}' -replace '[^\\](\{0\})', 'Success'相反，结果是：SelectSuccess 匹配

浏览 1提问于2019-03-31得票数 1

回答已采纳

1回答

(true=true)的所有证明都一样吗？

coq

我可以在Coq中证明以下内容吗？也就是说，true = true的所有证明都是相同的？我发现了以下线索，表明情况可能是这样的：

浏览 0提问于2018-06-13得票数 3

回答已采纳

1回答

如何在字符串的布尔等式上进行模式匹配，同时在Coq中的证明中获得所需的命题等式？

coq、equality、substitution、lambda-calculus、theorem-proving

我在SF中尝试证明substi_correct定理时被卡住了，因为我不知道如何在布尔等式上进行分裂，同时将其断言为命题相等。(*Doesn't work*) 证明的目标如下，不需要H: x0 = s0，这样我就可以继续了。s : tm ============================ substi s x0 (var s0) s 在Maps.v一章中，我们证明了，除了一个错误的情况外但是如何

浏览 33提问于2020-04-06得票数 0

回答已采纳

1回答

Agda中的点平等≗与命题平等≡

agda、equality-operator、agda-stdlib

在尝试使用list证明函数的属性时，我必须证明该属性是由map在列表上保留的。= refl我试图对命题等式≡做我的证明，但是map-cong证明了点态等式≗。我在这里有几个问题：我注意到map-cong以前是通过≡实现的，但它是通用的(我找到了这个)。这表明≗是≡的

浏览 13提问于2022-11-03得票数 0

回答已采纳

2回答

关于Coq上我的归纳型的平凡定理

coq

我不知道怎么证明。Euc 0不是一种归纳类型，所以我不能使用destruct t或induction t。请告诉我如何证明。

浏览 1提问于2020-09-07得票数 2

回答已采纳

1回答

抽象导致了一个错误的术语.但打得很好

coq

我在一个问题上被困了一段时间，为此我得出了一个较小的独立例子：Definition illt := forall x : f那么，这个错误消息有什么问题，我如何解决/调整我的初始目标呢？顺便说一下，这都是coq8.3。如果这是8.4中的问题，请告诉我，我很抱歉！)编辑:为了解决Robin的</

浏览 0提问于2013-02-14得票数 1

回答已采纳

1回答

`match goal`与let析构表达式不匹配

coq、coq-tactic

我正在尝试证明一个涉及使用解构let表达式的函数的定理，并尝试使用match goal策略来解构右侧，但由于某些原因，模式并不像我期望的那样匹配： match goal with (* why doesn't如果你有来自Certified Programming with Dependent Types的Cpdt (我非常喜欢他的自动化风格)，这里有一个应该可以运行的代码片段。我已经找

浏览 11提问于2020-11-11得票数 0

回答已采纳

1回答

如何巧妙地解构嵌套在记录中的新类型？

pattern-matching、purescript、newtype

我使用newtype作为记录的字段，而“父”类型上的模式匹配提取嵌套值很麻烦：newtype City = City { show (City { name }) = case name of (CityName cn) -> "City(" <> cn <> ")" 我可以解构“父”类型，但随

浏览 0提问于2016-10-03得票数 2

回答已采纳

点击加载更多