Failing when use "destruct" tactic to "or" hypothesis if the conclusion is sumbool

[zhengpushi]

Please check the code in ex1, why “destruct H” fail? what’s the meaning of this error message?

(* the hypothesis is "or" and the conclusion is "sumbool" *)
Example ex1 : forall m : nat, (m = 1 \/ m = 2) -> {m = 1} + {m = 2}.
Proof.
  intros.
  Fail destruct H.
(* Case analysis on sort Set is not allowed for inductive definition or. *)
(* why failed here? *)
  Abort.

(* the hypothesis is "or" and the conclusion is a simple prop *)
Example ex2 : forall m : nat, (m = 1 \/ m = 2) -> m >= 1.
Proof.
  intros.
  destruct H.                   (* it's OK *)
Admitted.

(* the hypothesis is "and" and the conclusion is "sumbool" *)
Example ex3 : forall m : nat, 1 <= m <= 2 -> {m = 1} + {m = 2}.
Proof.
  intros.
  destruct H.                   (* it's OK *)
Admitted.

[olaure01]

Your 3 examples basically sum up the situation with respect to destructing/eliminating a term of sort Prop as it is given in the reference manual (destruct is building a match construct). To make it simple:

• you can eliminate from Prop to Prop (your ex2)
• you cannot eliminate from Prop to Set/Type (your ex1) except if the inductive type your are trying to destruct has at most one constructor (your ex3) (indeed or has two constructors while and has only one constructor, and both are in Prop while sumbool is in Set)

[davidjao]

Although destruct H does not work in general, you can nevertheless prove your first example by using properties of the natural numbers: repeat (destruct m; try intuition discriminate).

[zhengpushi]

Thank you. It realy help me.