个人中心
文章发布
退出
作者热门文章
- html - 出于某种原因，IE8 对我的 Sass 文件中继承的 html5 CSS 不友好？
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景？
28
4
是否有一种方法可以定义一个“本地”Ltac 表达式，我可以用它来证明引理但在外部不可见？
Lemma Foo ...
Proof.
Ltac ll := ...
destrict t.
- reflexivity.
- ll.
- ll.
Qed.
(* ll should not be visible here *)
最佳答案
您可以使用一个部分:
Section Foo.
Ltac solve := exact I.
Lemma Foo : True.
Proof.
solve.
Qed.
End Foo.
关于Coq:本地 ltac 定义，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/51961226/
28
4
0
我想写一个带有可选变量名的策略。原始策略如下所示: Require Import Classical. Ltac save := let H := fresh in apply NNPP;
我正在做一些关于在 Coq 中形式化简单类型的 lambda 演算的练习，并且想使用 Ltac 自动化我的证明。在证明进步定理时: Theorem progress : forall t T,
我有一个包含对一些引理的调用的目标 foo在比赛的分支内。该调用使用变量 R 作为其参数之一。分行本地: | SomeConstr => fun R => .... (foo a b c R) ...
我如何调用 rewrite在 ltac 中只重写一次？我认为 coq 的文档提到了一些关于 rewrite at 的内容。但我还没有能够在实践中实际使用它，也没有例子。 这是我正在尝试做的一个例子:
是否有一种方法可以定义一个“本地”Ltac 表达式，我可以用它来证明引理但在外部不可见？ Lemma Foo ... Proof. Ltac ll := ... destrict t.
在尝试创建一个循环可变长度参数列表的 Ltac 定义时，我在 Coq 8.4pl2 上遇到了以下意外行为。谁能给我解释一下吗？ Ltac ltac_loop X := match X with
是否有一种方法可以定义一个“本地”Ltac 表达式，我可以用它来证明引理但在外部不可见？ Lemma Foo ... Proof. Ltac ll := ... destrict t.
我正在寻找一种方法来通过它的名字来匹配它。像这样: Ltac mytactic h_name := let h := hyp_from_name h_name in match h with
我想在 coq 中制定一个 Ltac 策略，它需要 1 个或 3 个参数。我读过 ltac_No_arg在 LibTactics 模块，但如果我理解正确，我将不得不调用我的策略: Coq idtac
在 Ltac 中，依赖归纳对我来说似乎不同。并不是。 以下工作正常: Require Import Coq.Program.Equality. Goal forall (x:unit) (y:unit
我想在某些假设存在而另一个假设不存在的情况下应用规则。我如何检查是否存在这种情况？ 例如: Variable X Y : Prop. Axiom A: X -> Y. Axiom B: X -> Z.
我在看QuickChick项目的时候遇到了Require Import Ltac.这句话我不知道这是做什么的以及 Ltac 在哪里模块是。我找到了一个文件 plugins/ltac/Ltac.v ，但
Ltac checkForall H := let T := type of H in match T with | forall x, ?P x => idtac | _ =
Require Import Streams. CoFixpoint map {X Y : Type} (f : X -> Y) (s : Stream X) : Stream Y := Cons
我是一名优秀的程序员,十分优秀！