Как уничтожить значения выражений?

Question

Я изучаю Coq и пытаюсь доказать следующее, казалось бы, простое свойство.По сути, мне нужно рассмотреть все случаи для eqb x y, но мой обычный подход с использованием тактик destruct и induction здесь не работает.

Fixpoint eqb (x:nat) (y: nat) :bool :=
match x,y with
| 0, 0 => true
| S xx, S yy => eqb xx yy
| _,_ => false
end.

Definition bool_to_nat (b:bool) :nat := 
  match b with
  | true => 1
  | false => 0
  end.

Theorem should_be_easy: forall x:nat, forall y : nat,
  bool_to_nat (eqb x y) + bool_to_nat (negb (eqb x y)) = 1.
  intros x y. Abort.

Answer 1

intros x y.
destruct (eqb x y).