Ltac:在包含用户定义符号的假设上与ltac匹配

文章/答案/技术大牛

发布

1回答

coq、coq-tactic、ltac

我对ordType和它的布尔比较运算符==、<b和<=b的中缀符号有以下定义。Ltac show_H:= | H: ?x == ?然而，当我在下面的引理中使用这个定义来显示假设的名称时，它会

浏览 6提问于2018-08-16得票数 2

回答已采纳

1回答

在编写Coq时，Unicode符号无法进行通用验证。

unicode、coq、proof-general

我在Ubuntu中使用Coq 8.11，并附带了一般证据。我写道：普通->显示->快速选项-> Unicode令牌 Ltac example2≔失败。错误失败： Ltac example3 :=失败。幸运的</

浏览 8提问于2020-04-23得票数 2

回答已采纳

1回答

软件基础阴影Ltac匹配符号

coq

在几个符号中使用了|-。例如，在中这会干扰Ltac匹配结构。例如，这是： match goal with end.在Stlc之外工作很好，但是一旦定义了这个表示法，它就会失败，因为： Tople

浏览 4提问于2015-04-17得票数 1

回答已采纳

1回答

我怎样才能写出一种既适用于目标又适用于假设的战术？

coq、coq-tactic

我试图写一种策略，可以在目标和假设上工作，类似于symmetry，但也适用于不等式。现在，有一些关于广义重写的，但是这是非常高级的，也许应该是另一个问题。这就是说，这里是我的实现，它为我的用例工作(虽然很尴尬)： lazymatch goal with | [ |- ?x <> ?这很好，但是如果我们在我们希望应用symm

浏览 9提问于2022-01-08得票数 0

回答已采纳

2回答

Ltac中一元数据构造函数的匹配

coq、ltac

我正在做一些关于在Coq中格式化简单类型的lambda微积分的练习，并希望使用Ltac自动完成我的证明。我想出了一段Ltac代码： (* right, because progress statement places stepping on==>表示计算的单个步骤(通过小步骤语义)。每一场比赛的意图是：当我们有一个假设时，匹配</

浏览 2提问于2016-05-06得票数 3

回答已采纳

1回答

我怎么写那些表现得像“毁灭.一样”的战术？

coq、ltac

在coq中，策略有一个变体，它接受一种“连接分离引入模式”，允许用户为引入的变量指定名称，即使在解压复杂的归纳类型时也是如此。我希望我的自定义策略允许(或要求，无论哪个更容易)用户提供一个介绍模式，我<

浏览 3提问于2015-05-09得票数 8

回答已采纳

1回答

如何在Ltac中进行“阴性”匹配？

coq、ltac

我想在假设存在的情况下应用一条规则，而另一种则不适用。我怎样才能检查这种情况呢？Variable X Y : Prop. match goal with let H' := fresh "DET" inH:XTrueH:XDET0

浏览 1提问于2015-02-09得票数 4

回答已采纳

1回答

为了简单起见，我们可以假设它是一个列表(但实际上类型更复杂，有多个cons构造函数，并且重写规则使用等价而不是相等)。我在编写自定义Ltac表达式方面没有太多经验，但我似乎可以定义如下内容： Ltac norm_cons := | H: ?这样，我们在第一个模式中捕获[]并跳过重写，否则执行重写。也许这需要一个跌倒的案例，但这不是重点:我如何给(类似于)这个给autorewrite一个提示？我尝试将上面的内容<e

浏览 20提问于2021-03-30得票数 1

1回答

如何匹配“匹配”表达式？

coq、ltac

我试图为假设写一条规则，它是在match构造的帮助下制定的： | S (S _) => 10%nat============================我怎样才能与这些假设相匹配呢

浏览 2提问于2015-02-11得票数 7

回答已采纳

1回答

如何在策略产生条件下检查可兑换性？

coq、coq-tactic

假设我有以下策略来检查一个术语是否是字面上的零： match x with | _ => constr:false如果这是球门上的战术，我会这么做 match x with | ?在这个具体的示例中，减少x或计算它(let xx := eval compute in x)可能有效，但在更复杂的示例中，计算成本可能会令人望而却步，特别是

浏览 3提问于2015-10-10得票数 1

回答已采纳

2回答

避免在假设和目标中应用策略的重复代码

coq

我发现我自己(某种程度上)在重复代码，因为当它们匹配时，我想在目标和假设中使用相同的策略。有时，这并不是因为我正在匹配，而只是因为我定义了一个自定义策略，但根据上下文，我希望将其应用于目标或命名假设。例如： Ltac my_tac H := simpl in H; rewrite X in H; ... ; other_tactic in H.在某种程度上，我想知道这个目标有一个名字，比如GOAL，就像<e

浏览 40提问于2021-09-23得票数 6

1回答

自动从本地上下文中选择假设

coq、coq-tactic

我有一个有如下部分的示例脚本： - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.似乎它将是一个选择的选择，使用;来解决干净，不幸的是，假设是到处都是。我怎么能把不同的校对组合在一起呢？

浏览 6提问于2017-05-27得票数 3

回答已采纳

1回答

Coq中定义与让的区别

functional-programming、coq、theorem-proving

定义和Coq中的“让”有什么区别？为什么有些定义需要证明？就像。这是群论中g1.v的一段代码。 Definition exp : Z -> U -> U.这个证据的目的是什么？

浏览 3提问于2015-02-11得票数 5

回答已采纳

1回答

在coq中递归地反转假设

recursion、coq

我在定义一种在证明上下文中递归反转假设的策略时遇到了麻烦。例如，假设我有一个证明上下文，其中包含如下假设：并且希望重复地反转该假设以获得包含该假设的证明上下文然而，有时颠倒一个假设会将不同的假设放到不同的</

浏览 0提问于2011-12-31得票数 9

回答已采纳

1回答

模式匹配从目标模式匹配中得到的假设

coq、ltac

Fail ltac:( | [ H : done _ |- _ ] => fail match我发现这非常令人惊讶，因为范围内唯一的假设是n和done n，而done n已经被顶级匹配的第一个分支发送了。如何在不显式引用done n的情况下匹配n，如第二个匹配的第一个分支？

浏览 1提问于2018-10-21得票数 0

回答已采纳

1回答

消除Coq中案例分析产生的冗余子目标

coq

有一个简单的定义Inductive C := cc. | mkA1 : B -> Ab: B______________________________________(2/4)____________________________________

浏览 2提问于2017-07-23得票数 1

回答已采纳

1回答

在中有像apply lem这样的东西吗？*

coq

有没有办法像rewrite lem in *一样，为所有可能的H调用apply lem in H Axiom P Q : nat -> Prop.

浏览 9提问于2019-02-18得票数 2

2回答

是否有一种方法可以通过重写步骤自动执行Coq验证？

automation、coq

我正在研究一个证据，我的一个子目标看起来有点像这样： (a b : bool) (H1: p -> a = b) negb该证明不依赖于任何外部引理，而只是将一个假设应用于另一个假设，然后用已知的假设重写步骤。有办法实现自动化吗？我试过做intros. auto.，但没有效果。也许我需要更有力的策略？我想让它自动化的原因是，在我最初的问题中，我实

浏览 4提问于2016-11-14得票数 5

回答已采纳

2回答

如何查找Coq验证策略的定义或实现？

math、coq、proof

如何找到像intros或destruct这样的东西的确切含义，比如查找一个实现(或者如果不可能的话，一个定义)？怎样才能有效地做到这一点？

浏览 4提问于2020-09-10得票数 2

回答已采纳

2回答

Ltac模式匹配:为什么‘`forall x，?P’不匹配` `forall x，x‘？

coq、coq-tactic、ltac

Ltac checkForall H := match T with 这就是我在这里看到的行为的原因吗？

浏览 1提问于2017-06-04得票数 3

回答已采纳

点击加载更多