Agda中一个空类型的证明
Agda中一个空类型的证明
提问于 2013-08-09 03:10:01
我正试图在agda中证明2*3!=5。为此，我将定义一个带有签名2*3≡5→⊥的函数。
利用我对乘法的定义
data _*_≡_ : ℕ → ℕ → ℕ → Set where
base : ∀ {n} → 0 * n ≡ 0
succ : ∀ {n m k j} → m * n ≡ j → j + n ≡ k → suc m * n ≡ k我已经证明
1*3≡3 : 1 * 3 ≡ 3
1*3≡3 = (succ base) znn和
3+3≡5 : 3 + 3 ≡ 5 → ⊥
3+3≡5 (sns (sns (sns ())))但当我试图证明：
m235 : 2 * 3 ≡ 5 → ⊥
m235 ( ( succ 1*3≡3 ) ( x ) ) = ( 3+3≡5 x )编译器输出这个关于x的错误。
.j != (suc 2) of type ℕ
when checking that the expression x has type 3 + 3 ≡ 5抱歉，如果这是个愚蠢的问题。提前谢谢。
回答 1
Stack Overflow用户
回答已采纳
发布于 2013-08-09 06:09:42
首先，您忘记了包含_+_≡_的定义。我想是这样的：
data _+_≡_ : ℕ → ℕ → ℕ → Set where
znn : ∀ {n} → 0 + n ≡ n
sns : ∀ {n m k} → n + m ≡ k → suc n + m ≡ suc k接下来，您的问题不是如何找到正确的语法，而是必须弄清楚如何从2 * 3 ≡ 5类型的值中得出结论。使用您所做的模式匹配，您可以询问Agda上下文中有哪些值可用，方法是将右侧替换为a ?，调用C编译并使用C，以询问上下文：
m235 : 2 * 3 ≡ 5 → ⊥
m235 ( ( succ 1*3≡3 ) ( x ) ) = ?Agda将说：
Goal : ⊥
-----------------------------
x : .j + 3 ≡ 5
1*3≡3 : 1 * 3 ≡ .j
.j : ℕ也就是说:你希望证明底部(即假设中的不一致性)，并且在上下文中有3个可用的值。您有一个1 * 3 ≡ .j类型的证明，对于一个未知的数字.j，还有一个.j + 3 ≡ 5类型的证明。你似乎假设Agda会自动注意到j必须是3，但这对它来说太难了:它只会从统一中得出结论，而不是执行实际的推理本身。因此，解决方案是帮助Agda理解为什么.j必须是3。
m235 : 2 * 3 ≡ 5 → ⊥
m235 ((succ (succ base znn)) sum) = ?现在，上下文看起来如下：
Goal: ⊥
————————————————————————————————————————————————————————————
x : 3 + 3 ≡ 5现在，您可以将x类型的验证3 + 3 ≡ 5与以前证明不存在这种证据的证据结合起来：
m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ (succ base znn) x) = 3+3≡5 x更新:我在第一次阅读时就错过了，但问题中有一个误解，我错过了，也没能解释。错误在以下代码中：
m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ 1*3≡3 x) = 3+3≡5 x这里的误解是，这个子句左边的变量名称1*3≡3没有引用由相同名称定义的值。相反，它引入了一个新的变量，Agda知道它具有相同的类型，但是它不知道它的值。
可以通过使用AGDA2.3.2中引入的“模式同义词”特性来实现您预期的目标:参见发布说明
pattern 1*3≡3 = (succ base) znn
m235 : 2 * 3 ≡ 5 → ⊥
m235 (succ 1*3≡3 x) = 3+3≡5 x只有模式同义词在模式中被扩展，而其他值则不是。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/18139523
复制相关文章
相似问题
腾讯云开发者
