问题标签 [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.

86 问题
Newest
Active
Bountied
318
Unanswered
0 投票
2 回答
99 浏览

coq - 如何在 Coq 中编写中间证明语句 - 类似于 Isar 中的“使用 Lemma1, Lemma2 by auto 声明”但在 Coq 中？

我想在 Coq 证明脚本中编写中间引理，例如，在 SCRIPTProof. SCRIPT Qed.本身内部 - 类似于在 Isar 中所做的。如何在 Coq 中做到这一点？例如：

我知道该exact声明并想知道是否是这样...但是我也希望像在 Isar 中一样拥有该声明的证据，have by auto或者using Proof. LEMMA_PROOF Qed.

为了使其具体化，我试图做这些非常简单的证明：

但我不确定它是如何工作的，而且效果不太好。

有关的：

0 投票
0 回答
62 浏览

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:

  1. execute the Isabelle tactic script (to reveal many intermediate statements)
  2. select with some heuristic H (maybe based on human proofs) of which sub-trees of the proof tree to close with have lemma_sub_tree_i using L1, L2, L3, ..., Ln by SomeProof (perhaps the by ... has more Isar scripts we automatically generated, so this function is recursive)
  3. 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:

0 投票
1 回答
50 浏览

flutter - Flutter - 未定义 Isar 架构

我决定在我的下一个项目中使用Isar 数据库，我发现它在处理本地数据时非常有用。

我按照其网站上的快速入门指南进行操作。我添加了依赖项。注释了联系人类。Ran 代码生成器。但在第四步，我在创建 Isar 实例时创建架构时遇到问题。

问题是我在哪里输入了 ContactSchema，它说

所以我要问的问题是，我遵循了指南，但我无法创建模式。如何创建一个以使 Isar db 工作？

更新：

添加后part 'contact.g.dart'，输入此命令flutter pub run build_runner build即可。

0 投票
1 回答
34 浏览

isabelle - 嵌套案例 Isar

0 投票
1 回答
32 浏览

isabelle - 感应引入“坏名声”

0 投票
1 回答
27 浏览

isabelle - 对第二个论点 Isar 的归纳

我收到“无法应用初始证明方法⌂”

在 Isabelle 中，rotate_tac我猜可以使用归纳法来处理所需的论点，Isar 的等价物是什么？用“假设”和“显示”重新表述引理会有所帮助吗？


12345678910