问题标签 [logical-foundations]

我试图弄清楚 LF 测试脚本在从终端运行时如何输出手动评分的作业。例如，如果您查看Induction.v一个名为“plus_comm_informal我正在尝试获取测试脚本”的练习，以获取InductionTest.v我编写的评论或内容。所以我做了以下尝试猴子调试。

我保存了文件。然后我编译文件，coqc -Q . LF .\Induction.v然后运行测试文件coqc -Q . LF .\InductionTest.v

它的输出并没有给我在手动评分练习中传递的任何评论。终端输出的相关部分如下。

我错过了什么？

在 Logical Foundations 的 IndProp.v 中，我们具有以下归纳属性：

有没有可能解决这个问题：

据推测，人们需要某种歧视或矛盾，因为nostutter [] -> nostutter [x]这似乎没有意义，但我看不到任何能让我取得进步的东西。难道只是无法证明吗？

2

我正在研究软件基础并遇到错误。（https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html）

证明示例：

错误：在环境 x : string y : string 术语“eqb_string x y”的类型为“bool”，而预期的类型为“Datatypes.bool”。

关于如何进行的任何提示？

我正在尝试完成逻辑基础关于归纳命题一章的系列练习le_exercises。

这个系列主要基于归纳关系le，定义如下：

我坚持的特定定理如下：

到目前为止，我设法证明的这些系列中的先前定理是：

这本书给出了一个提示，指出该定理add_le_cases可能“更容易通过归纳证明n”，我以各种方式尝试过，但似乎无处可去。

我考虑过使用该plus_le定理，但似乎无法从中获得任何有用的信息。我觉得我的理解中肯定缺少一些重要的东西，但你不知道你不知道什么。

在逻辑基础关于归纳命题的章节中，练习exp_match_ex1涉及以下定义：

我一直试图证明以下引理：

结果是：

最初看起来尝试通过归纳继续ss可以让我取得进展，但我找不到任何方法来转换假设forall s : list T, In s (x :: ss) -> s =~ re，以便我可以fold app ss [ ] =~ Star re从归纳假设中证明(forall s : list T, In s ss -> s =~ re) -> fold app ss [ ] =~ Star re。

我目前对如何证明以下定理感到困惑：

我被困在这里：

我知道不可能简单地证明 coq 中的排中律，但我真的很想知道用这个给定的定理是否可以证明排中律？

全部

我试图理解 SF-LF 书 chp4 中提到的教堂数字。

我得到

似乎 cnat 是某种类型，并且同时起作用。怎么可能兼具类型和功能？任何人都可以帮助解释一下吗？