Ltac :可选参数策略
Ltac是Coq中的一个命令，用于控制Coq的证明策略。它是"Language Tactical"的缩写，可以理解为一种控制语言的策略。
Ltac命令可以用来定义和组合证明策略，以便在Coq中自动化和简化证明过程。它允许用户编写自定义的策略，以便在证明过程中应用特定的推理规则、引理或定理。
Ltac的可选参数策略是指在使用Ltac命令时可以传递的可选参数。这些参数可以用来进一步定制和调整证明策略的行为。
例如，可以使用Ltac命令定义一个简单的策略，该策略将给定的定理应用到当前的证明目标上：
Ltac apply_theorem := apply my_theorem.在这个例子中，apply_theorem是自定义的策略名称，my_theorem是要应用的定理。然后，可以在证明过程中使用这个策略：
Proof.
apply_theorem.
(* 继续证明 *)
Qed.除了定义自定义策略，Ltac还提供了许多内置的策略和策略组合子，可以用于自动化证明过程。例如，intros策略用于引入假设，apply策略用于应用定理，rewrite策略用于重写等等。
总之，Ltac是Coq中用于控制证明策略的命令，可选参数策略是Ltac命令中可传递的参数，用于进一步定制和调整证明策略的行为。通过使用Ltac和合适的策略，可以简化和自动化Coq中的证明过程。
腾讯云相关产品和产品介绍链接地址：
相关·内容
1回答
我想在coq中制定一个Ltac策略，它可以接受1个或3个参数。我在模块中读过关于ltac_No_arg的文章，但如果我理解正确的话，我将不得不用以下命令调用我的策略：
Coq < mytactic arg_1 ltac_no_arg ltac_no_arg.
这不是很方便。
有没有办法得到这样的结果？：
Coq < mytactic arg_1.
Coq < mytactic arg_1 arg_2 arg_3.
浏览 8提问于2017-06-30得票数 6
回答已采纳
在试图创建一个在变量长度参数列表上循环的Ltac定义时，我在coq8.4pl2上遇到了以下意外行为。有人能给我解释一下吗？
Ltac ltac_loop X :=
match X with
| 0 => idtac "done"
| _ => (fun Y => idtac "hello"; ltac_loop Y)
end.
Goal True.
ltac_loop 0. (* prints "done" as expected *)
ltac_loop 1 0. (* prints "h
浏览 2提问于2014-03-29得票数 7
回答已采纳
2回答
假设我有一个花哨的策略来解决特定类型的引理：
Ltac solveFancy :=
some_preparation;
repeat (first [important_step1 | important_step2];
some_cleanup);
solve_basecase.
现在我使用这个策略来进一步证明这类引理，我随后想在这个策略中使用它。
Lemma fancy3 := …. Proof. … Qed.
Ltac important_step3 := apply fancy3;[some|specific|stuff].
现在，我可以简单地重新定义L
浏览 21提问于2018-02-19得票数 7
回答已采纳
2回答
在Ltac中实现复杂策略时，有一些Ltac命令或战术调用，我希望这些命令或策略调用失败，并在预期的地方执行(例如终止repeat，或导致回溯)。这些故障通常在故障级别0时引发。
在较高级别“转义”周围的try或repeat块时引发的故障，对于发出意外故障信号非常有用。
我所缺少的是一种运行策略tac并将其失败(即使是在0级)处理为更高级别的方法，同时保留失败的信息。这将使我能够确保repeat不会因为Ltac编程错误而终止。
我能在Ltac中实施这样一种提高级别的战术吗？
浏览 2提问于2017-07-14得票数 6
回答已采纳
1回答
我想写一个带有可选变量名的策略。最初的策略如下：
Require Import Classical.
Ltac save :=
let H := fresh in
apply NNPP;
intro H;
apply H.
我想让用户有机会选择他想要的名称，并像这样使用它:例如，save a。
我用编写了一个变体
Require Import Classical.
Inductive ltac_No_arg : Set :=
| ltac_no_arg : ltac_No_arg.
Ltac savetactic h :=
match type of h wi
浏览 0提问于2018-03-29得票数 2
回答已采纳
1回答
我正在尝试编写以下函数： Ltac restore_dims :=
repeat match goal with
| [ |- context[@Mmult ?m ?n ?o ?A ?B]] => let Matrix m' n' := type of A in
let Matrix n'' o' := type of B in
replace m with m&#
浏览 9提问于2019-04-02得票数 1
回答已采纳
1回答
我正在考虑写战术，这将考虑多个目标，并在此基础上作出决定。然而，当我使用match goal with并盯着一个目标时，我怎么说“请找到另一个像这样的目标呢？”
或者说，一个更普遍的问题是，我如何在Ltac的目标之间切换？
浏览 0提问于2018-04-08得票数 5
我有过
1 subgoals, subgoal 1
n : nat
b : bool
m : nat
H1: P1
H2: P2
H3: P1
H4: P2
=========
some_goal
在我运行策略auto_group_duplicates之后，它将变成
1 subgoals, subgoal 1
n, m : nat
b : bool
H1, H3: P1
H2, H4: P2
=========
some_goal
有这样的战术吗？
浏览 0提问于2021-07-08得票数 0
回答已采纳
我试图写一种策略，可以在目标和假设上工作，类似于symmetry，但也适用于不等式。现在，有一些关于广义重写的，但是这是非常高级的，也许应该是另一个问题。这就是说，这里是我的实现，它为我的用例工作(虽然很尴尬)：
Require Import Coq.PArith.BinPos.
Ltac symmetry' :=
lazymatch goal with
| [ |- ?x <> ?y ] => unfold not; intros NQ; symmetry in NQ; revert NQ
| [ |- _ ] => symmetry
end
浏览 9提问于2022-01-08得票数 0
回答已采纳
有时候，我有一个最好的证明，那就是把它投射到另一个空间。我现在做以下几件事：
remember (f x) as y eqn:H; clear H; clear x.
我试着用Ltac实现自动化：
Ltac project x y :=
let z := fresh in
remember x as y eqn:z; clear z; clear x.
但我得到了以下错误：
Error: Ltac variable x is bound to f x which cannot be coerced to a variable.
这里有什么问题？
浏览 3提问于2017-11-05得票数 2
回答已采纳
2回答
我相信这个标题是很清楚的：
我希望有一种策略，假设一个命题，如果成功的话，我会继续寻找另一个命题，然后我发现，第一个命题暗示着第二个命题，这是作为一个假设在上下文中提出的。
例如，Ltac cp P Q创建一个子目标Q，并将P放在上下文中。如果我确实能够到达子目标Q，那么子目标就会被释放，P->Q就会添加到上下文中。我怎样才能做到这一点？
编辑:很明显，在证明assert (P->Q). intro.做了这件事的同时，我不能将它们合并成Ltac策略，这给出了No focused proof (No proof-editing in progress).的一个错误。
浏览 2提问于2018-10-21得票数 1
回答已采纳
1回答
在下面的例子中，我是否可以用一种策略代替replace来简化这个表达式呢？
Require Import Vector.
Goal forall (n b:nat) (x:t nat n), (map (fun a => plus b a) x) = x.
Proof.
intros n b x.
replace (fun a => plus b a) with (plus b) by auto.
...
浏览 6提问于2017-09-20得票数 2
回答已采纳
假设中有一些等式(=)和不等式(<>)，例如：
e : x2 = x1
n : x3 <> x1
我想使用像assumption这样的策略，但有时目标中的预期(Un)相等是相反的，比如：
x1 = x2
x1 <> x3
我的问题是：
是否可以自动将上述(Un)相等的对称形式引入假设中？
如果没有，是否可以用符号来写一个战术来做到这一点。
到目前为止，我可以手动这样做：
assert (x1 = x2) by (symmetry in e; assumption).
assert (x1 <> x3) by (unfold not; intro
浏览 0提问于2015-11-27得票数 0
回答已采纳
就像的op一样，我正在根据实际情况在-nois下重新开发Coq.Init.Prelude。
我想用战术，但他们没有用。
我试过Declare ML Module "ltac_plugin".，但没有用。
Welcome to Coq v8.8 (eccf1d50b020e87b4d19d0bda43361e1e82d01b1)
Coq < Declare ML Module "ltac_plugin".
[Loading ML file ltac_plugin.cmxs ... done]
Coq < Goal forall A:Prop, fo
浏览 0提问于2018-06-19得票数 2
回答已采纳
1回答
对于这些简单的推理规则，我想要Ltac战术。
在Modus Ponens中，如果我有H:P->Q和H1:P，Ltac mp H H1将把Q添加到上下文中作为H2 : Q。
在ModusTol透镜中，如果我有H:P->Q和H1:~Q，那么Ltac mt H H1将向上下文中添加H2:~P。
我写了一封信给大家，但它在复杂的情况下行不通，因为先例也是一种暗示。
Ltac mp H0 H1 := let H := fresh "H" in apply H0 in H1 as H.
编辑:我在另一个看似无关的问题()中找到了对apply的答案，在这个问题中，apply的“哑
浏览 2提问于2018-10-22得票数 4
回答已采纳
2回答
我目前正在尝试用一个可以容易生成的术语实例化存在主义量词(在这个特定的例子中，来自tauto)。我第一次尝试：
Ltac mytac :=
match goal with
| |- (exists (_ : ?X), _) => cut X;
[ let t := fresh "t" in intro t ; exists t; firstorder
| tauto ]
end.
这种策略将适用于一个简单的问题，如
Lemma obv1(
浏览 0提问于2017-10-17得票数 1
回答已采纳
假设我有下面的简单引理，我想获得有关split的信息。
Lemma and_prop : forall (P : Prop) (Q : Prop),
P -> Q -> P /\ Q.
Proof.
intros P Q HP HQ.
Info 100 split.
哪种输出
simple refine ?X10@{__:=P; __:=Q; __:=HP; __:=HQ}
谁能解释一下这意味着什么，为什么我需要一个自然数的信息？
浏览 6提问于2021-11-17得票数 0
回答已采纳
1回答
我想要一种Ltac战术，这种战术可以起到拆解交换的作用。主要是，如果我在假设P \/ Q的某个地方有一个子术语H，Ltac Com H会在上下文中添加Q \/ P作为另一个假设。
我尝试通过公理和apply提供换位规则；但是它只适用于简单的假设，例如在R -> (P \/ Q)中失败；它应该添加到上下文R -> (Q \/ P)中。
浏览 2提问于2018-10-23得票数 2
回答已采纳
我正在研究一个证据，我的一个子目标看起来有点像这样：
Goal forall
(a b : bool)
(p: Prop)
(H1: p -> a = b)
(H2: p),
negb a = negb b.
Proof.
intros.
apply H1 in H2. rewrite H2. reflexivity.
Qed.
该证明不依赖于任何外部引理，而只是将一个假设应用于另一个假设，然后用已知的假设重写步骤。
有办法实现自动化吗？我试过做intros. auto.，但没有效果。我怀疑这是因为auto只能执行apply步骤，而不能执行rewrite步骤，
浏览 4提问于2016-11-14得票数 5
回答已采纳
这是我为使用Is_true而构建的一些自动化的一部分。我有一个Lemma Is_true_implb_impl : (Is_true x -> Is_true y) <-> Is_true (implb x y).，我有一个Is_true (implb ?x ?y)形式的假设H，我用Ltac elim_Is_true := match goal with ...来匹配。当我将Is_true_implb_impl x y应用到H中时(如果我没有用x和y实例化它不能匹配)，那么假设就变成了Is_true y，并得到了Is_true x作为一个新的子目标。(我试图通过编写一种断言I
浏览 5提问于2019-09-29得票数 0
回答已采纳
2回答
我正在做一些关于在Coq中格式化简单类型的lambda微积分的练习，并希望使用Ltac自动完成我的证明。在证明进展定理时：
Theorem progress : forall t T,
empty |-- t \in T -> value t \/ exists t', t ==> t'.
我想出了一段Ltac代码：
Ltac progress_when_stepping :=
(* right, because progress statement places stepping on the right of \/ *)
right;
(* u
浏览 2提问于2016-05-06得票数 3
回答已采纳
我在我的证明上下文中有H : P -> Q，我需要Q来完成我的证明，但是我没有任何P的证据：
在证明了目标P后，是否有一种策略或其他任何方法可以使前提P -> Q成为一个新的目标，然后用Q代替P。然后，我可以直接使用Q来证明最初的目标。
然而，我也可以使用assert (HP : P)，然后使用(H HP)来获得Q，但是我必须手工复制P，这是不方便的(特别是当P很长，H : P -> Q还在的时候)。
我读过，但没有什么有用的东西，也许我错过了。
浏览 16提问于2022-04-26得票数 0
1回答
当我查看QuickChick项目时，我遇到了一个句子Require Import Ltac. --我不知道它是干什么的，也不知道Ltac模块在哪里。我找到了一个文件plugins/ltac/Ltac.v，但是这个文件不可能是空的，因为这个文件是空的(顺便问一下，包含一个空文件的目的是什么？)我试过Locate Ltac.，但我得到了Error: Syntax error: [constr:global] expected after 'Ltac' (in [locatable]).，这更让人困惑。
Ltac模块是做什么的，Ltac.v文件在哪里，为什么Loacte命令在这种情况
浏览 2提问于2018-03-30得票数 4
回答已采纳
这个问题是关于我正在做的一个项目，也就是用Coq编码原则。原则推导出推理规则，其中之一是系统：
∀P Q R:支柱，P→Q，Q→R : P→R
我正在尝试创建一个Ltac脚本来编码Syll推断表单。()的以下MP策略非常有效：
Ltac MP H1 H2 :=
match goal with
| [ H1 : ?P -> ?Q, H2 : ?P |- _ ] => specialize (H1 H2)
end.
在这里，我认为"=>“右边的策略是H1在H2中的应用。现在，相关的系统策略不起作用：
Ltac Syll H1 H2 :=
match go
浏览 1提问于2020-09-14得票数 1
回答已采纳
1回答
在我的项目中，我试图保持一些小的缺点，以加快校对速度。然而，当我编写Ltac支持这样的体系结构时，我找不到一种方法来引用各种后盾。基本上，我想做以下几点：
Tactic Notation "myauto" ???(db) := auto with db.
事情会比这复杂得多。但是，Coq解析器似乎热切地将db解析为提示基的具体名称，因此将引发类似以下错误消息：
Error: No such Hint database: db.
我可以参数化auto家族的提示基选项吗？
浏览 0提问于2018-03-25得票数 2
回答已采纳
1回答
我正在尝试编写一个返回值的策略，在此过程中，它需要检查某个东西是否是一个等价物。
不幸的是，我不能使用is_evar，因为这样策略就不会被视为返回值(而是另一种策略)。下面是一个例子。
有什么建议吗？
Ltac reify_wrt values ls :=
match ls with
| nil => constr:(@nil nat)
| ?a :: ?ls' => let i := lookup a values in
let idx := reify_wrt values ls' in
浏览 2提问于2017-08-29得票数 4
回答已采纳
如果我在我的证明上下文中有一个看起来像H: True -> P的假设，并且我想把它转换成H: P，那么最简单的方法是什么？我尝试过simpl in H，但它什么也不做，我找到的唯一方法就是非常不满意的pose proof (H Coq.Init.Logic.I) as H。难道没有更简单的方法吗？
浏览 2提问于2020-03-23得票数 3
回答已采纳
3回答
如何在ltac中调用rewrite来仅重写一个实例？我认为coq的文档提到了一些关于rewrite at的东西，但我还没有能够在实践中实际使用它，也没有例子。
这是我正在尝试做的一个例子：
Definition f (a b: nat): nat.
Admitted.
Theorem theorem1: forall a b: nat, f a b = 4.
Admitted.
Theorem theorem2: forall (a b: nat), (f a b) + (f a b) = 8.
Proof.
intros a b.
(*
my goal here is f a b + f
浏览 6提问于2017-08-01得票数 5
回答已采纳
2回答
用Coq编写Ltac时，可能会尝试编写
try match goal with
|- context [?x && true] => rewrite andb_true_r
end
而不是
try rewrite andb_true_r
不要毫无意义地调用rewrite --这是在更大的策略的内部循环中进行的，在大多数情况下，我们都希望重写失败。
但这真的更快吗？还是rewrite失败的速度和我写的手写match一样快？
浏览 1提问于2018-02-27得票数 2
回答已采纳
的Ltac章节展示了一种“错误”的策略：
Theorem t1' : forall x : nat, x = x.
match goal with
| [ |- forall x, ?P ] => trivial
end.
然后这本书解释了
The problem is that unification variables may not contain locally bound variables.
In this case, [?P] would need to be bound to [x = x], which contains the local qu
浏览 2提问于2020-05-14得票数 2
回答已采纳
在中，我们发现以下内容：
(** [idB = \x:Bool. x] *)
Notation idB :=
(abs x Bool (var x)).
(** [idBB = \x:Bool->Bool. x] *)
Notation idBB :=
(abs x (Arrow Bool Bool) (var x)).
[...]
(** (We write these as [Notation]s rather than [Definition]s to make
things easier for [auto].) *)
这里到底是什么？从Notation
浏览 2提问于2019-10-12得票数 0
回答已采纳
2回答
我在看
Theorem eq_add_1 : forall n m,
n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
Proof.
intros n m. rewrite one_succ. intro H.
assert (H1 : exists p, n + m == S p) by now exists 0.
apply eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
left. rewrite H1 in H; rewrite add_succ
浏览 4提问于2020-09-10得票数 2
回答已采纳
在Coq (8.5p1，ch9.2)分支和回溯行为中，我很难理解multiple successes的概念。例如，从文档中：
回溯分支
我们可以使用以下结构进行分支：
expr1 + expr2
战术可以被看作是有几个成功。当一种战术失败时，它要求更多先前战术的成功。expr1 + expr2拥有v1的所有成功，其次是v2的所有成功。
我不明白的是，为什么我们首先需要多方面的成功？一个成功不足以完成一个证据吗？
此外，从文档中可以看出，似乎有一些成本较低的分支规则在某种程度上是“有偏见的”，包括
first [ expr1 | ::: | exprn ]
和
expr1 || expr
浏览 4提问于2016-07-07得票数 3
回答已采纳
2回答
我正在学习命题逻辑和推理规则。析取三段论规则指出，如果我们有前提(P或Q)，也有(而不是P)，那么我们就可以达到Q。
我一辈子都想不出在Coq里该怎么做。假设我有：
H : A \/ B
H0 : ~ A
______________________________________(1/1)
我应该用什么策略来达到
H1 : B.
另外，如果有人能和我分享Coq策略中的基本推理规则，如modus Tol透镜，或者析取介绍等，我会很高兴。我是否可以使用插件？
浏览 0提问于2018-10-20得票数 4
回答已采纳
在我的假设列表中，我有：
X : Type
l' : list X
n' : nat
H : S (length l') = S n'
我的目标是length l' = n'。
所以我试了一下f_equal in H。但我得到了以下错误：
Syntax error: [tactic:ltac_use_default] expected after [tactic:tactic] (in [vernac:tactic_command]).
我认为我应该能够将f_equal应用于H以删除两边的S，这是错误的吗？
浏览 19提问于2022-05-02得票数 0
回答已采纳
2回答
假设我们有一个归纳数据结构和它的一些谓词：
Inductive A : EClass :=
X | Y .
Definition P (a: A) : bool :=
match a with
X => true
| Y => false
end.
然后，我提出了一个定理，说明存在一个元素a，使得P a返回true：
Theorem test :
exists a: A, P a.
可能有各种各样的方法，我在想如何用案例分析来证明它，在我看来，它是这样的：
请记住，有两种方法可以构造A
一个接一个地试一遍，如果我们找到一个像P a这样的目击证人，就停下
浏览 4提问于2017-09-24得票数 3
回答已采纳
有没有办法像rewrite lem in *一样，为所有可能的H调用apply lem in H Axiom P Q : nat -> Prop.
Axiom lem : forall (n : nat), P n -> Q n.
Goal P O -> P (S O) -> True.
intros. apply lem in H. apply lem in H0.
浏览 9提问于2019-02-18得票数 2
我遇到了这样一种情况，即setoid重写不起作用，因为可转换类型与策略不匹配。我想出的解决办法在兰巴达下行不通。寻求建议：
Require Import Setoid Morphisms Relations.
(* Sample definitions *)
Record S {i o: nat} : Type.
Definition C {i o: nat} (f: @S i o): @S i o. Admitted.
Definition B {o:nat} (z:nat): @S (o+o) o. Admitted.
(* Relations *)
Parameter R: for
浏览 4提问于2017-12-05得票数 2
回答已采纳
$ coqtop -nois
Welcome to Coq 8.7.0 (October 2017)
Coq < Ltac i := idtac.
Toplevel input, characters 0-4:
> Ltac i := idtac.
> ^^^^
Error: Syntax error: illegal begin of vernac.
我正在"coqtop -nois“下重新开发"Coq.Init.Prelude”和"HoTT.Basics.Overture“。我发现很难直接编写表达式。这就是我想使用战术的原因。我想知道为什么我不能
浏览 2提问于2018-02-17得票数 3
回答已采纳
考虑以下事态发展：
Definition done {T : Type} (x : T) := True.
Goal Test.
pose 1 as n.
assert (done n) by constructor.
Fail ltac:(
match goal with
| [ H : done _ |- _ ] => fail
| [ H : _ |- _ ] =>
match goal with
| [ _: done H |- _ ] => idtac "H == n"
|
浏览 1提问于2018-10-21得票数 0
回答已采纳
我正在使用Terraform设置多个标记策略定义。我在自定义json文件中提到了带有策略定义id和参数的标记定义。
tag_definitions.json
[
{
"parameters": {
"tagName": {
"value": "cost_center"
},
"tagValue": {
"value": "${cost_center}"
}
},
"po
浏览 2提问于2021-11-03得票数 2
1回答
策略可以将ident或num作为：
instantiate (ident:= term)
instantiate (num := term)
现在我想在战术定义中使用第二个。例如：
Ltac my_instantiate n x:=
instantiate(n:=x).
不幸的是，这会产生以下错误：
Ltac变量n被绑定到1，这不能强制到一个新的标识符。
我怀疑ltac正在尝试第一次使用instantiate。如何告诉coq按位置实例化，或者如何正确地传递argumetn？
下面是一个很小的例子：
Ltac my_instantiate n x:=
instanti
浏览 0提问于2018-12-04得票数 1
在我的证明中，这是可行的
induction H1 as [ | | | | | | | | | ].
但是，当我把它换成
dependent induction H1 as [ | | | | | | | | | ].
我得到了"Error:语法错误: tactic:ltac_use_default预期在之后“。
在进行依赖归纳时，您能认真地选择变量的名称吗？这太疯狂了；我真的希望我只是语法错误。
谢谢。
浏览 0提问于2020-08-15得票数 1
回答已采纳
1回答
下面是我想要做的一个简短的例子。 假设我有一个关系 Inductive divisible: nat -> nat -> Type :=
| one : forall n, divisible n 1.
..etc... 我还有下面的ltac Ltac simplify := autorewrite with blah： 我想定义一个ltac，它确实简化为一个“可分”目标中的第一个术语。就像这样 Ltac simplify_fst :=
match goal with |- (divisible ?N ?M) =>
autorewrite with subst1 in
浏览 18提问于2021-06-26得票数 0
回答已采纳
我有以下Ltac (来自)，它以前在CoQ8.4pl6上工作，但它不在CoQ8.5beta 3上工作：
Ltac maybe_intro_sym A B :=
match goal with
|[H:B=A|-_] => fail 1
|[H:A=B|-_] => assert (B=A) by auto
end.
Ltac maybe_intro_sym_neg A B :=
match goal with
|[H:B<>A|-_] => fail 1
|[H:A<>B|-_] => assert
浏览 1提问于2015-12-02得票数 1
回答已采纳
这本书的作者已经为口吃练习的一些单元测试提供了证明。不幸的是，他们没有解释它们是如何工作的。我能够理解所有的证明，只有一个例外： Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).
Examp
浏览 16提问于2019-06-26得票数 0
回答已采纳
是否有可能以及如何在前向链接模式中将Coq用作计算器或规则引擎？Coq脚本通常需要声明可以找到证据的目标。但是，是否有可能在其他方向上进行，例如，计算由某些规则限定的一些结果的集合，例如，通过一些步骤。我对全一阶逻辑的序列演算特别感兴趣。我猜(但我不知道)有一些一阶逻辑的序列演算的实现或包，但它是用于定理证明的。我喜欢用这样的顺序演算来推导出一些有指导的顺序的结果。在Coq中这是可能的吗？
浏览 1提问于2019-09-08得票数 0
有一个简单的定义
Inductive B := bb.
Inductive C := cc.
Inductive A :=
| mkA1 : B -> A
| mkA2 : C -> A.
Definition id (a: A) : A :=
match a with
| mkA1 b => mkA1 b
| mkA2 c => mkA2 c
end.
我试图通过案例分析(destruct)进行证明，比如：
Theorem Foo :
forall a1 a2 : A , a1 <> a2 -> id a1 <>
浏览 2提问于2017-07-23得票数 1
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
即时通信 IM
实时音视频活动推荐
腾讯云开发者
