Coq证明#Coq

Question

我试图解决这个证据，但我找不到它的方法。我有两个子目标，但我甚至不知道它是否正确。

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

2个次级目标

a，b: Nat

H: Equal (leB a，b) True

______________________________________(1/2)

等匹配b与

Z => False

S‘=> leB a m’

结束(leB A b) /相等(leB b (S a)) (leB A b)

______________________________________(2/2)

相等(leB (S ) b)真/等(leB b (S ))真

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。

然后，在每个分支中，用b策略考虑不同的destruct情况。它将简化您的目标，您可以看到目标的左边或右侧是真的，并使用您的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.

也会证明你的引理。