程序员经验分享-hwhale

可以在 Coq 的蕴涵中使用 destruct 吗？

2024-03-17

destruct可以用来分割and, or在柯克。不过好像也可以用暗示？ 例如我想证明~~(~~P -> P)

Lemma test P : ~~(~~P -> P).
Proof.
unfold not.
intro pffpf.
apply pffpf.
intro pff.
destruct pff.
intro p.
apply pffpf.
intro pff.
exact p.
Qed.

when destruct pff.它工作正常，但我不知道为什么？谁能为我解释一下吗？


The destruct如果蕴涵的结论是归纳（或共归纳）类型，则策略对蕴涵起作用。因此它适用于你的例子，因为False是归纳定义的。然而，如果我们想出一个不同的定义False，它可能不一定有效。例如，以下脚本在以下位置失败destruct pff line:

Definition False : Prop := forall A : Prop, A.
Definition not (P : Prop) : Prop := P -> False.

Lemma test P : not (not (not (not P) -> P)).
unfold not.
intro pffpf.
apply pffpf.
intro pff.
destruct pff. (* Fails here *)
intro p.
apply pffpf.
intro pff.
exact p.
Qed.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

coq

coqtactic

可以在 Coq 的蕴涵中使用 destruct 吗？ 的相关文章

  • Coq 中是否有一套最小完整的策略？

    我见过很多 Coq 策略 它们在功能上是相互重叠的 例如 当你在假设中得到确切的结论时 你可以使用assumption apply exact trivial 也许还有其他人 其他例子包括destruct and induction对于无感

  • 在 Coq 中实现向量加法

    在某些依赖类型语言 例如 Idris 中实现向量加法相当简单 根据维基百科上的例子 import Data Vect default total pairAdd Num a gt Vect n a gt Vect n a gt Vect n

  • 在 Coq 中使用我自己的 == 运算符重写策略

    我试图直接从字段的公理证明简单的字段属性 经过对 Coq 原生现场支持的一些实验 像这个 我决定最好简单地写下 10 条公理并使其自成一体 我在需要使用的时候遇到了困难rewrite与我自己的 运算符自然不起作用 我意识到我必须添加一些我的

  • 归纳命题在 Coq 中如何运作？

    我正在阅读软件基础中的 IndProp 和 Adam Chlipala 的第 4 章书 但我在理解归纳命题时遇到了困难 为了运行示例 让我们使用 Inductive ev nat gt Prop ev 0 ev 0 ev SS forall

  • 证明唯一的零长度向量为零

    我有一个类型定义为 Inductive bits nat gt Set bitsNil bits 0 bitsCons forall l bool gt bits l gt bits S l 我试图证明 Lemma emptyIsAlway

  • Ltac：通过回溯重复策略 n 次

    假设我有一个像这样的策略 取自 HaysTac 它搜索一个参数来专门化一个特定的假设 Ltac find specialize in H multimatch goal with v gt specialize H v end 然而 我想写

  • 用约翰·梅杰的等式重写

    约翰 梅杰的等式带有以下重写引理 Check JMeq ind r JMeq ind r forall A Type x A P A gt Prop P x gt forall y A JMeq y x gt P y 很容易将其概括为 Le

  • coqide - 无法从同一文件夹加载模块

    我无法加载 CoqIde 中同一文件夹中的模块 我正在尝试从 Software Foundations 加载源代码 我正在包含 SF 源代码的文件夹中运行 coqidecoqide or coqide 然后打开并运行该文件后 我收到此错误

  • 在 Coq 中，重写适用于 = 但不适用于 <-> (iff)

    我在证明期间有以下内容 我需要替换normal form step t with value t因为有一个已证明的定理存在等价 H1 t1 gt t1 normal form step t1 t2 tm H2 t2 gt t2 normal

  • 如何在 Coq 中禁用我的自定义符号？

    我定义了一个符号来模拟命令式编程 Notation a gt gt b b a at level 50 然而之后 所有函数应用表达式都表示为 gt gt 样式 例如 在 Coq Toplevel 的证明模式下 我可以看到 bs nat gt

  • 如何在 Coq 中切换当前目标？

    是否可以切换当前目标或子目标来在 Coq 中进行证明 例如 我有一个这样的目标 来自 eexists 1 1 s gt 0 r1 r1 s1 s r3 r3 s2 我想做的是split并首先证明正确的连接 我认为这将给出存在变量的值 s 并

  • 逻辑：tr_rev_ Correct 的辅助引理

    在逻辑章节中 介绍了反向列表函数的尾递归版本 我们需要证明它可以正确工作 Fixpoint rev append X l1 l2 list X list X match l1 with gt l2 x l1 gt rev append l1

  • 如何一步步检查 Coq 中更复杂的策略的作用？

    我试图经历那些著名的和精彩的软件基础书籍 https softwarefoundations cis upenn edu lf current Basics html lab30但我举了一个例子simpl and reflexivity 只

  • Coq QArith 除以零就是零，为什么？

    我注意到在 Coq 的有理数定义中 零的倒数被定义为零 通常 除以零是没有明确定义 合法 允许的 Require Import QArith Lemma inv zero is zero 0 0 Proof unfold Qeq refle

  • Coq：添加“强归纳”策略

    对自然数的 强 或 完全 归纳意味着当证明 n 上的归纳步骤时 您可以假设该属性对于任何 k 都成立 Theorem strong induction forall P nat gt Prop forall n nat forall k n

  • 可以在 Coq 的蕴涵中使用 destruct 吗？

    destruct可以用来分割and or在柯克 不过好像也可以用暗示 例如我想证明 P gt P Lemma test P P gt P Proof unfold not intro pffpf apply pffpf intro pff

  • Coq 中的案例分析证明

    我试图证明关于以下函数的命题 Program Fixpoint division m nat n nat measure m nat match lt nat 0 n with false gt 0 true gt match leq na

  • 为什么coq互感类型必须具有相同的参数？

    下列的亚瑟的建议 https stackoverflow com a 17304209 403875 我改变了我的Fixpoint相互关系Inductive这种关系 建立 游戏之间的不同比较 而不是 深入研究 但现在我收到一条全新的错误消息

  • 没有可判定的相等性或排除中间值的鸽巢证明

    在软件基础中IndProp v https softwarefoundations cis upenn edu lf current IndProp html lab244一个人被要求证明鸽巢原理 并且可以使用排除中间 但有人提到这并不是绝

  • 为什么较新的依赖类型语言没有采用 SSReflect 的方法？

    我在 Coq 的 SSReflect 扩展中发现了两个约定 它们似乎特别有用 但我还没有看到它们在较新的依赖类型语言 Lean Agda Idris 中得到广泛采用 首先 可能的谓词被表示为布尔返回函数而不是归纳定义的数据类型 默认情况下

随机推荐

  • 如何在 WooCommerce 中启用自定义产品类型的价格和库存

    我在 WooCommerce 应用程序中创建了自定义产品类型 function register variable bulk product type class WC Product Variable bulk extends WC Pr

  • jQuery 图像网格系统

    我有一个关于图像网格系统的问题 我创建了这个DEMO http codepen io shadowman86 pen YPpedQ来自 codepen io 在此演示中您可以看到 div class photo row div class

  • 创建位图时使用与密度无关的像素作为宽度和高度

    Bitmap createBitmap int width int height Bitmap Config config 方法只是说给它一个高度和一个宽度 没有指示这些是实际像素还是 dp 像素 我的问题 1 这些值是 dp 像素吗 2

  • 具有小数精度的格式数字字段？

    当然 我遗漏了一些非常明显的东西 我有一个精度为 2 的小数字段 但 Formtastic 仅以一位小数显示它 除非实际值有 2 位 我缺少什么 Model create table items force gt true do t t s

  • 你能让 std::shared_ptr 管理用 new T[] 分配的数组吗？

    你能做一个std shared ptr http en cppreference com w cpp memory shared ptr指向一个数组 例如 std shared ptr

  • npm：术语“npm”不被识别为 cmdlet、函数、脚本文件或可操作程序的名称

    当我检查节点 v时 一切正常并打印出来 但 npm 显示此错误 我怎样才能解决这个问题 请帮我 我搜索了很多时间并找到了解决方案 一旦安装nodejs gt 请重新启动笔记本电脑 然后设置路径 系统属性 gt 环境设置 gt C Progr

  • Git LFS 文件未推送到远程存储库

    我正在尝试使用 git LFS 将 xlsx 文件推送到远程存储库 我尝试了两种方法 使用 Sourcetree 点击菜单和使用终端服务器 两者都会产生相同的错误消息 我在 Bitbucket 中设置了一个远程存储库并设置了允许 LFS 选

  • WPF C# 类、文本框和参考，Easy(?)“当前上下文中不存在”

    我正在拔头发 我创建了一个类 employee cs 我最初在 Window1 xaml cs 上的 公共部分类 Window1 Window 中开发了这个类 当将其移动到单独的类时 我无法再引用文本框 组合框等 我该怎么办 给出的错误是

  • Python 交互式 Shell - 带有 print 的 SyntaxError [重复]

    这个问题在这里已经有答案了 我是Python新手 我在 Windows 2003 虚拟机上安装了 Python 推出Python Shell 输入以下代码 print Hello World 它立即向我吐出以下内容 语法错误 语法无效 以下

  • 哈希表 v 自平衡搜索树

    我很想知道使用自平衡树技术来存储项目比使用哈希表更重要的推理是什么 我发现哈希表无法维护插入顺序 但我始终可以在顶部使用链表来存储插入顺序序列 我发现对于少量的值 哈希函数会增加成本 但我总是可以将哈希函数与密钥一起保存以加快查找速度 我知

  • 检测何时将文本输入到文本区域并相应地更改它

    我有一个textarea用户可以在其中输入或粘贴其他人的电子邮件地址 并在按 提交 按钮后向他们发送邀请 每封电子邮件必须用逗号分隔 并且在提交表单之前有效 验证由jQuery 验证插件 http jqueryvalidation org

  • “在‘​​vue’中找不到导出‘默认’（作为‘Vue’导入）

    我是 VueJs 的初学者 这是我的第一个应用程序 import BootstrapVue from bootstrap vue import createApp from vue import App from App vue const

  • “函数”对象没有属性“tk”是什么意思？

    我目前正在开发一个程序 可以让您注册一个帐户 然后通过将详细信息写入 txt 文档并再次读取它们来再次登录 一切都工作正常 直到我添加以下内容 def login fh open usernamepassword txt r lines f

  • 在 Swift 中过滤具有多个条件和类型的对象数组

    我正在尝试在我的应用程序中进行一些复杂的过滤 但我不知道下一步该做什么 我的数据由一个字典数组组成 其中每个字典中的值可以是String Int or String let person1 String Any first name Joh

  • Onload 使输入大小适合文本长度

    我试图让 jQuery 测试 onLoad 输入框中文本的长度 并更改输入框的大小以适应 这是迄今为止我的代码尝试 emailSubject attr size this val length 我收到以下错误 this val 不是函数 我

  • Zend_Validate_Float 语言环境不适用于 hi_IN 语言环境

    在使用 hi IN 进行数字验证时 我面临以下问题 其中 Zend Locale Format isFloat 对于非单个数字和任何语言环境都可以正常工作 但不适用于单位数字和区域设置 hi IN 源代码 测试用例 foreach arra

  • 有没有办法识别 c/c++ 库的版本？

    例如 如何获取 usr lib libz a的版本 如果可以获取其他有用的信息 例如编译器 架构等 那就太好了 我想知道这一点的原因是 当我编译程序并与特定版本的 libz 链接时 gcc 总是说它忽略了我在命令行中提供的 libz gcc

  • 覆盖 require.js 中的 setTimeout

    我们在项目中使用 require js 我们需要重写设置超时时间在第 705 行 这是我们需要的代码以某种方式忽略 省略这个 setTimeout 根本 我的意思是运行它 问题是 如果我在更改版本时显式地在开源代码中更改它 代码将丢失 我应

  • 将数组传递给存储过程

    我必须将数组和字符串传递给存储过程并返回数据表 C side public DataTable fetchRequested string empID string account string refNo string orgID str

  • 可以在 Coq 的蕴涵中使用 destruct 吗？

    destruct可以用来分割and or在柯克 不过好像也可以用暗示 例如我想证明 P gt P Lemma test P P gt P Proof unfold not intro pffpf apply pffpf intro pff

热门标签