问题标签 [isar]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
coq - 如何在 Coq 中编写中间证明语句 - 类似于 Isar 中的“使用 Lemma1, Lemma2 by auto 声明”但在 Coq 中？
我想在 Coq 证明脚本中编写中间引理，例如，在 SCRIPTProof. SCRIPT Qed.本身内部 - 类似于在 Isar 中所做的。如何在 Coq 中做到这一点？例如：
我知道该exact声明并想知道是否是这样...但是我也希望像在 Isar 中一样拥有该声明的证据，have by auto或者using Proof. LEMMA_PROOF Qed.
为了使其具体化，我试图做这些非常简单的证明：
但我不确定它是如何工作的，而且效果不太好。
有关的：
- 我知道 Czar ( https://coq.discourse.group/t/what-is-the-difference-between-ssreflect-and-czar/824 ) 但 Coq afaik 不再支持。
isabelle - Is there an automatic way to generate Isar scripts given a correct Isabelle tactic script?
I know this might be rather out there question but I was curious if it was possible to automatically generate an Isar script given an Isabelle script. My guess is that it should be possible but the problem would be ill-posed as there might be many possible Isar scripts given a tactic script.
My guess of an approach would be something like this:
- execute the Isabelle tactic script (to reveal many intermediate statements)
- select with some heuristic
H(maybe based on human proofs) of which sub-trees of the proof tree to close withhave lemma_sub_tree_i using L1, L2, L3, ..., Ln by SomeProof(perhaps theby ...has more Isar scripts we automatically generated, so this function is recursive) - Verify the new Isar script is valid i.e. output the new Isar script if the statement is the same as the original Isabelle tactic proof and the proof goes through/type checks/validates.
Is this possible? At the very least - is it possible in principle with some (hopefully sensible heuristic H. (Of course I know that step 2 is rather important and hoping there is a heuristic that I could truly use in practice to make an actual implementation of this).
Related:
- https://www.reddit.com/r/isabelle/comments/rh0mh7/is_there_an_automatic_way_to_generate_isar/
- https://www.quora.com/unanswered/Is-there-an-automatic-way-to-generate-Isar-scripts-given-a-correct-Isabelle-tactic-script
- https://isabelle.zulipchat.com/#narrow/stream/202967-New-Members.20.26.20Projects/topic/automatic.20isabelle.20-.3E.20Isar.20conversion
flutter - Flutter - 未定义 Isar 架构
我决定在我的下一个项目中使用Isar 数据库，我发现它在处理本地数据时非常有用。
我按照其网站上的快速入门指南进行操作。我添加了依赖项。注释了联系人类。Ran 代码生成器。但在第四步，我在创建 Isar 实例时创建架构时遇到问题。
问题是我在哪里输入了 ContactSchema，它说
所以我要问的问题是，我遵循了指南，但我无法创建模式。如何创建一个以使 Isar db 工作？
更新：
添加后part 'contact.g.dart'，输入此命令flutter pub run build_runner build即可。
isabelle - 对第二个论点 Isar 的归纳
我收到“无法应用初始证明方法⌂”
在 Isabelle 中，rotate_tac我猜可以使用归纳法来处理所需的论点，Isar 的等价物是什么？用“假设”和“显示”重新表述引理会有所帮助吗？