Coq's proof #Coq

Question

I try to solve this proof but I don't find how to it. I have two subgoals but I don't even know if it's correct.

Here the lemma that I trid to solve with this but I'm stuck :

2 subgoals

a, b : Nat

H : Equal (leB a b) True

______________________________________(1/2)

Equal match b with

| Z => False

| S m' => leB a m'

end (leB a b) / Equal (leB b (S a)) (leB a b)

______________________________________(2/2)

Equal (leB (S a) b) True / Equal (leB b (S a)) True

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

First, don't introduce all variables in the beginning with intros. You will get a too weak induction hypothesis. Just introduce a.

Then in each branch, consider the different cases of b with the destruct tactic. It will simplify your goal and you can see if it is the left or the right side of goal that is true, and use your refl lemma to finish the goal.

The last case require that you use your induction hypothesis, and it is here that it is important that it holds for all b, not just one specific b.

Also, you didn't provide a definition for you Nat type, I guess it is something like this:

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

Here is a proof.

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.

While it may not be as insightful, you can also use tactics that try these steps to get a shorter proof.

induction a; destruct b; firstorder.

will also prove your lemma.