程序员经验分享-hwhale

有没有办法禁用 Coq 中的特定符号？

2023-12-30

我希望在 Coqide 中，证明状态不使用某种符号（但仍使用所有其他符号）。

这可能吗？


据我在文档中的理解，这是不可能的。您也许可以使用打开/关闭范围，但我不确定它是否有效，因为明确指出只要有可能，符号将用于打印。

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

coq

Notation

有没有办法禁用 Coq 中的特定符号？ 的相关文章

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

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

  • 如何在 Coq 中将一条线的公理定义为两个点

    我想找一个例子axiom in Coq类似于几何中的线公理 如果给定两个点 则这两点之间存在一条线 我想看看如何在 Coq 中定义它 本质上选择这个简单的直线公理来看看如何定义一些非常原始的东西 因为我很难在自然语言之外定义它 具体来说 我

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

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

  • Coq Proof Assistant 中依赖类型的问题

    考虑以下简单的表达语言 Inductive Exp Set EConst nat gt Exp EVar nat gt Exp EFun nat gt list Exp gt Exp 及其格式良好的谓词 Definition Env lis

  • Powershell：二维数组

    以下内容按预期工作 values a b c d foreach value in values write host Value 0 value 0 write host Value 1 value 1 结果 1 Value 0 a Va

  • 引入先前证明的定理作为假设

    假设我已经在coq中证明了某个定理 稍后我想将其作为假设引入到另一个定理的证明中 有没有一种简洁的方法来做到这一点 当我想做一些诸如案例证明之类的事情时 我通常会出现这种需要 我发现做到这一点的一种方法是assert陈述定理 然后立即证明它

  • for 循环的简洁数学符号

    如果这不属于这里 我很抱歉 但我正在寻找一种方法来描述我的代码的数学背景 使用 numpy 我对两个以上的维数组求和 a shape 10 5 2 b shape 5 2 c a b c shape 10 5 2 是否有一个纯粹的数学符号

  • 理解大 O 表示法 - 破解编码面试示例 9

    我被这两个代码困住了 Code 1 int f int n if n lt 1 return 1 return f n 1 f n 1 Code 2 平衡二叉搜索树 int sum Node node if node null return

  • 如何将假设中的具体变量更改为存在量化变量？

    假设我有一个这样的假设 FooProp a b 我想将假设改为这种形式 exists a FooProp a b 我怎样才能做到这一点 我知道我能做到assert exists a FooProp a b by eauto但我试图找到一个不

  • JSON 点符号转字符串

    我在 javascript 中使用 JSON 并且尝试获取点表示法表示的字符串值 例如AAA BBB 0 CCC DDD 5 EEE 123 采用 JSON 点表示法格式 但我想获得价值AAA BBB 0 CCC DDD 5 EEE作为字符

  • 逻辑：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 中证明可逆列表是回文

    这是我对回文的归纳定义 Inductive pal X Type list X gt Prop pal0 pal pal1 forall x X pal x pal2 forall x X l list X pal l gt pal x l

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

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

  • Coq :> 符号

    这可能是非常微不足道的 但我找不到任何关于 gt 符号在 Coq 中含义的信息 有什么区别 U 类型 和 W gt 类型 这取决于符号出现的位置 例如 如果它位于记录声明内 它会指示 Coq 添加相应的记录投影作为强制 具体来说 假设我们有

  • Coq 中 MSet 的使用示例

    MSets https coq inria fr library Coq MSets MSets html似乎是 OCaml 式有限集的最佳选择 可悲的是 我找不到示例用途 如何定义一个空的MSet或单身人士MSet 我怎样才能结合两个MS

  • python 中的大 O 表示法

    有谁知道有什么学习大符号的好资源吗 特别是学习如何遍历一些代码并能够看到它会是 O N 2 或 O logN 最好能告诉我为什么这样的代码等于 O N log N def complex numbers N len numbers resu

  • 在 Coq 中，“if then else”允许非布尔第一个参数？

    我读过一些教程if a then b else c代表match a with true gt b false gt c end 然而 很奇怪的是 前者不检查类型a 而后者当然确保a是一个布尔值 例如 Coq lt Check if nil

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

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

  • 在 coq 的 then 部分中使用 if expression = true 的证明

    对于所有 1 Require Import ZArith Znumtheory Local Open Scope Z scope Require Coq Program Tactics Require Coq Program Wf Lemm

  • 在依赖类型的函数式编程语言中，扁平化列表是否更容易？

    在 haskell 中寻找一个可以展平任意深度嵌套列表的函数时 即应用的函数concat递归并在最后一次迭代时停止 使用非嵌套列表 我注意到这需要有一个更灵活的类型系统 因为随着列表深度的变化 输入类型也会变化 确实 有几个 stackov

随机推荐

  • 从对象验证消息中删除字段名称

    我在表单中使用它对对象进行了简单的活动记录验证 form error messages message gt header message gt 这又会输出类似 FieldName My Custom message 的内容 我需要做的是从

  • JavaFX BooleanProperty 和 Hibernate

    我正在尝试将 JavaFX BooleanPropety 添加到由 Hibernate 保留的模型中 但出现以下错误 Caused by org hibernate MappingException Could not determine

  • 避免在释放控件时调用 Invoke

    我的工作线程中有以下代码 ImageListView下面是源自Control if mImageListView null mImageListView IsHandleCreated mImageListView IsDisposed i

  • RSpec：如何存根继承的方法 current_user （无需设计）？

    我有一个基于 MHartl 的控制器RoR4 教程 http www railstutorial org book single page 就像 MHartl 一样 我没有使用设计 I 推出了我自己的身份验证系统 http www rail

  • UIImagePickerController 快门

    I have bug with UIImagePickerController which source type is camera Sometimes after controller appeared shutter is not o

  • 实现 π (pi) 的 Spigot 算法

    我很难理解插口算法找到 pi here http www cut the knot org Curriculum Algorithms SpigotForPi shtml在页面底部 我在第 2 部分 将 A 放入常规形式 的底部迷失了方向

  • 如何在 C# 中的随机端口上创建 HttpListener 类？

    我想创建一个在内部提供网页服务的应用程序 并且可以在同一台计算机上的多个实例中运行 为此 我想创建一个HttpListener监听的端口是 随机选择 目前未使用 本质上 我想要的是这样的 mListener new HttpListener

  • 如何设置新创建的 emacsclient 的样式和位置？

    我最近改用 emacsclient 进行大部分文本编辑 我正在尝试将一些设置迁移到新的 略有不同的 环境 特别是 在我的 emacs 文件中 我有一个设置窗口大小并准备一些主题的函数 但是 emacs 文件中的代码不会在每次调用 emacs

  • 如何在 AppEngine Standard 和 Nodejs 中提供静态文件

    The 文档 https cloud google com appengine docs standard nodejs serving static files表示您只需更新您的 app yaml 就像 AppEngine 中的任何语言一

  • MongoDB：将多个集合中的数据合并为一个......如何？

    我如何 在 MongoDB 中 将多个集合中的数据合并到一个集合中 我可以使用map reduce吗 如果可以的话怎么办 因为我是新手 所以我非常感谢一些例子 MongoDB 3 2 现在允许人们通过以下方式将多个集合中的数据合并为一个集合

  • 测试 SQL Server 连接

    我构建了一个基于 Excel 的工具 它使用 ODBC 连接和查询表从 SQL Server 2014 提取数据 该工具必须与 Mac Office 2016 兼容 因此需要 ODBC 和查询表 我正在努力测试用户是否可以连接到 SQL S

  • 将两个多边形区域合并为R中的单个多边形区域

    我是 R 中处理空间数据和多边形的新手 我有两个独立的形状文件 包含从 Google 地球中提取的两个多边形 因此 基本上第一个形状文件是一个位置 例如购物中心等 第二个形状文件是第一个位置周围三公里的半径 我将两个形状文件作为 Spati

  • Glade：如何在 GtkAssistant 中编辑页面

    我想将内容添加到 Glade 中的助手窗口 GtkAssistant 的页面中 当我添加新助手时 GtkAssistant 下没有出现任何子项 此外 我无法选择 或删除或更改 Glade 生成的 3 个默认页面的内容 我只能选择助手本身 因

  • 使用 groovy 修改 Soap UI 请求

    我们需要查找当前国家 地区的经销商数量 在下面的 xml 请求中 每个请求的键值对都会有所不同 Soap 请求的输入将在 txt 文件中给出 根据 txt 文件中的输入数量 我需要动态生成键值对 xml 标签 Format of Input

  • 使用python计算矢量投影

    有没有更简单的命令来计算矢量投影 我改为使用以下内容 x np array 3 4 0 y np array 10 5 6 z float np dot x y z1 float np dot x x z2 np sqrt z1 z3 z

  • 当我尝试登录注册用户并通过解析启用推送通知时，我的应用程序崩溃

    我正在尝试通过解析启用推送通知 如果已经有用户缓存并登录到应用程序 则解析通知代码将起作用 但是 如果我注销并尝试注册新用户 应用程序就会崩溃 并且收到一条错误消息 NSInvalidArgumentException 原因 不能对 PFO

  • 我应该如何解释稀疏_分类_交叉熵函数的输出？

    作为输入 a 具有浮点数 1 0 或 0 0 当我尝试用我的模型和sparse categorical crossentropy损失我得到类似的东西 0 4846592 0 5153408 我如何知道它预测什么类别 您看到的这些数字是给定输

  • 从对象数组中删除相同的值

    我想通过比较 2 个数组来从数组中删除相同的对象 样本数据 arr1 id 1 name a id 2 name b id 3 name c id 4 name d arr2 id 1 name a id 4 name d let newA

  • 如何在android中的videoview中播放rtmp视频？

    我想在 videoview 中播放 rtmp 视频 那么如何在我的应用程序中播放 rtmp 视频 String host rtmp example com String fileName www mp4 int port 1935 Conn

  • 有没有办法禁用 Coq 中的特定符号？

    我希望在 Coqide 中 证明状态不使用某种符号 但仍使用所有其他符号 这可能吗 据我在文档中的理解 这是不可能的 您也许可以使用打开 关闭范围 但我不确定它是否有效 因为明确指出只要有可能 符号将用于打印

热门标签