有人知道以下定理的Coq的任何标准库中的证明吗？如果有的话,我找不到它.
forall abc:nat,b> = c - > a + b - c = a +(b - c)
提前谢谢,马库斯.
我想在Coq中证明:
convert l' + 1 + (convert l' + 1) = convert l' + convert l' + 1 + 1
只有一些括号是多余的,不要让我使用reflexivity命令; 所以我该怎么做？
所有元素都是nat(自然)类型,因为这convert l'是一个返回nat数的函数,我不想使用像Omega这样的强大策略等等.
我开始学习Coq,并试图证明一些看似相当简单的东西:如果列表包含x,那么该列表中x的实例数将> 0.
我已经定义了contains和count函数,如下所示:
Fixpoint contains (n: nat) (l: list nat) : Prop :=
match l with
| nil => False
| h :: t => if beq_nat h n then True else contains n t
end.
Fixpoint count (n acc: nat) (l: list nat) : nat :=
match l with
| nil => acc
| h :: t => if beq_nat h n then count n (acc + 1) t else count n acc t
end.
我试图证明:
Lemma contains_count_ge1 : …我正在 Coq 中尝试互感应，我定义的第一个类型是
Inductive IsEven : nat -> Prop :=
| EvenO : IsEven O
| EvenS n : IsOdd n -> IsEven (S n)
with IsOdd : nat -> Prop :=
| OddS n : IsEven n -> IsOdd (S n).
我现在想证明偶数之和是偶数。我可以使用固定点和模式匹配来做到这一点：
Fixpoint even_plus_even (n m : nat) (evenn : IsEven n) (evenm : IsEven m) : IsEven (n + m) :=
match evenn with
| EvenO => evenm
| EvenS n' oddn' => EvenS (n' + m) (odd_plus_even …Goal forall (d : nat), d + 1 = d -> False.
Proof.
intros d H.
Abort.
我怎样才能证明False从H？inversion H只是复制它.
如果其中一个是偶数而另一个是奇数,则采用"两个自然之和很奇怪"的非常简单的证明:
Require Import Arith.
Require Import Coq.omega.Omega.
Definition even (n: nat) := exists k, n = 2 * k.
Definition odd (n: nat) := exists k, n = 2 * k + 1.
Lemma sum_odd_even : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
intros n. intros m. left.
destruct H. firstorder.
这段代码末尾的状态是:
2 subgoals
n, m, x : nat
H : n + m = 2 * …有人可以解释一下如何完成这个证明吗？（请不要给出实际答案，只是一些指导:)
练习来自 SF 第 1 卷，如标题所示，内容如下：
(** **** Exercise: 3 stars, standard (injection_ex3) *)
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
j = z :: l ->
x = y.
现在，我在介绍所有术语后尝试通过injectionon来解决这个问题H0。injection经过重写后H2，我最终得到了以下目标，但我不知道如何前进。
1 subgoal (ID 174)
X : Type
x, y, z : X
l, j : list X
H2 : x = …我不知道我用什么策略来证明这个结构.我尝试了两种方法,但我陷入了两种方法.
Lemma Exo17 : forall A : Prop, ~~(A \/ ~A).
Proof.
Methode 1
intro.
unfold not.
intro.
Methode 2
intro.
intro.
case H.