通过矛盾的定理将假设重写为false

发布于 2025-01-20 12:59:01 字数 269 浏览 2 评论 0原文

我想表明

[seq q x t | x <- iota 0 (t + 1)] != [::]

我决定解构 iota 0 (t + 1) 因为我有一个引理：

iota 0 (t + 1) != [::]

所以解构的第一个情况应该有 iota 0 (t + 1) = [::] 根据提到的定理，这是错误的，我可以区分。如何使用引理重写第一个破坏情况中的方程？我无法弄清楚。

谢谢。

原文

I want to show that

[seq q x t | x <- iota 0 (t + 1)] != [::]

I decided to destruct iota 0 (t + 1) because I have a lemma that says:

iota 0 (t + 1) != [::]

So the first case of destruct should have iota 0 (t + 1) = [::] which by the theorem mentioned is false, and I can discriminate. How can I rewrite the equation in the first destruct case using the lemma? I cannot figure it out.

Thanks.

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

夜巴黎 2025-01-27 12:59:02

你不需要破坏。请注意，iota 是通过其第二个变量的递归来定义的。您当前的目标无法简化，因为 t + 1 不以构造函数开头。但是，您可以通过重写addn1将其放入可以解决的表单中。

回复收藏 0 原文

清君侧 2025-01-27 12:59:02

除了计算之外，正如 Arthur 所建议的那样，您有时还可以使用对位来处理不等式（搜索“contra” 来查找变体版本）。

例如，在您的情况下，如果添加一些单射性约束，您可以显示：

Lemma foo (q : nat -> nat -> nat) t (injq: injective (q^~ t)) :
  iota 0 (t + 1) != [::] -> [seq q x t | x <- iota 0 (t + 1)] != [::].
Proof.
apply: contra_neq.
rewrite [RHS]( _ : [::] = [seq q x t | x <- [::]]) //.
exact: inj_map. 
Qed.

In addition to computation, as Arthur suggests, you can sometimes use contraposition to deal with non-equalities (do Search "contra" for variant versions).

For instance, in your case, you can show, if you add some injectivity constraint:

Lemma foo (q : nat -> nat -> nat) t (injq: injective (q^~ t)) :
  iota 0 (t + 1) != [::] -> [seq q x t | x <- iota 0 (t + 1)] != [::].
Proof.
apply: contra_neq.
rewrite [RHS]( _ : [::] = [seq q x t | x <- [::]]) //.
exact: inj_map. 
Qed.

回复收藏 0 原文

~没有更多了~