Coq 的证明 #Coq

Question

我试图解决这个证明，但我不知道如何解决。我有两个子目标，但我什至不知道它是否正确。

这里是我试图解决的引理，但我卡住了：

2 个子目标

a, b : 自然

H : 等于 (leB a b) 真

______________________________________(1/2)

等于匹配 b

| Z => 假

| S m' => leB a m'

结束 (leB a b) / 等于 (leB b (S a)) (leB a b)

______________________________________(2/2)

等于 (leB (S a) b) 真 / 等于 (leB b (S a)) 真

Inductive Bool : Type :=
          True : Bool | False : Bool.

Definition Not(b : Bool) : Bool :=
          Bool_rect (fun a => Bool)
                     False
                     True
                     b.



Lemma classic : forall b : Bool, Equal b (Not (Not b)).
Proof.
intro.
induction b.
simpl.
apply refl.
simpl.
apply refl.
Qed.

Definition Equal(T : Type)(x y : T) : Prop :=
           forall P : T -> Prop, (P x) -> (P y).

Arguments Equal[T].
(* Avec certaines versions Arguments Equal[T] *)

Lemma refl : forall T : Type, forall x : T, Equal x x.
Proof.
intros.
unfold Equal.
intros.
assumption.
Qed.

Fixpoint leB n m : Bool :=
  match n, m with
    | Z, _ => True
    | _, Z => False
    | S n', S m' => leB n' m'
  end.

Answer 1

首先，不要在intros开头引入所有变量。你会得到一个太弱的归纳假设。介绍一下a.

然后在每个分支中，使用destruct 策略考虑b 的不同情况。它将简化您的目标，您可以查看目标的左侧或右侧是否为真，并使用您的 refl 引理来完成目标。

最后一种情况需要您使用归纳假设，重要的是它适用于所有 b，而不仅仅是一个特定的 b.

另外，你没有为你的Nat类型提供定义，我猜是这样的：

Inductive Nat := Z | S (n:Nat).

这里有一个证明。

Lemma Linear : forall a b, (Equal (leB a b) True) \/ (Equal (leB b a) True). 
  Proof.
induction a. 
- intros b. destruct b; simpl.
    + left. apply refl. 
    + left. apply refl.
- intros b. destruct b; simpl.
  + right. apply refl.
  + destruct (IHa b) as [Hleft | Hright].
    ++ left. apply Hleft.
    ++ right. apply Hright.
Qed.

虽然它可能不那么有见地，但您也可以使用尝试这些步骤的策略来获得更短的证明。

induction a; destruct b; firstorder.

也会证明你的引理。

Coq 的证明 #Coq

Coq's proof #Coq

coq

coq-tactic