Context

I am trying to define the partial order A ≤ B ≤ C with a relation le in Coq and prove that it is decidable: forall x y, {le x y} + {~le x y}.

I succeeded to do it through an equivalent boolean function leb but cannot find a way to prove it directly (or le_antisym for that mater). I get stuck in situations like the following:

1 subgoal
H : le C A
______________________________________(1/1)
False

Questions

1. How can I prove, that le C A is a false premise?
2. Is there an other other proof strategy that I should use?
3. Should I define my predicate le differently?

Minimal executable example

Require Import Setoid.

Ltac inv H := inversion H; clear H; subst.

Inductive t : Set := A | B | C.

Ltac destruct_ts :=
  repeat match goal with
  | [ x : t |- _ ] => destruct x
  end.

Inductive le : t -> t -> Prop :=
  | le_refl : forall x, le x x
  | le_trans : forall x y z, le x y -> le y z -> le x z
  | le_A_B : le A B
  | le_B_C : le B C .

Definition leb (x y : t) : bool :=
  match x, y with
  | A, _ => true
  | _, C => true
  | B, B => true
  | _, _ => false
  end.

Theorem le_iff_leb : forall x y,
  le x y <-> leb x y = true.
Proof.
  intros x y. split; intro H.
  - induction H; destruct_ts; simpl in *; congruence.
  - destruct_ts; eauto using le; simpl in *; congruence.
Qed.

Theorem le_antisym : forall x y,
  le x y -> le y x -> x = y.
Proof.
  intros x y H1 H2.
  rewrite le_iff_leb in *. (* How to prove that without using [leb]? *)
  destruct x, y; simpl in *; congruence.
Qed.

Theorem le_dec : forall x y, { le x y } + { ~le x y }.
  intros x y.
  destruct x, y; eauto using le.
  - apply right.
    intros H. (* Stuck here *)
    inv H.
    rewrite le_iff_leb in *.
    destruct y; simpl in *; congruence.
  - apply right.
    intros H; inv H. (* Same thing *)
    rewrite le_iff_leb in *.
    destruct y; simpl in *; congruence.
  - apply right.
    intros H; inv H. (* Same thing *)
    rewrite le_iff_leb in *.
    destruct y; simpl in *; congruence.
Qed.

The problem with le is the transitivity constructor: when doing inversion or induction on a proof of le x y, we know nothing about the middle point that comes out of the transitivity case, which often leads to failed proof attempts. You can prove your result with an alternative (but still inductive) characterization of the relation:

Require Import Setoid.

Ltac inv H := inversion H; clear H; subst.

Inductive t : Set := A | B | C.

Inductive le : t -> t -> Prop :=
  | le_refl : forall x, le x x
  | le_trans : forall x y z, le x y -> le y z -> le x z
  | le_A_B : le A B
  | le_B_C : le B C .

Inductive le' : t -> t -> Prop :=
  | le'_refl : forall x, le' x x
  | le'_A_B  : le' A B
  | le'_B_C  : le' B C
  | le'_A_C  : le' A C.

Lemma le_le' x y : le x y <-> le' x y.
Proof.
  split.
  - intros H.
    induction H as [x|x y z xy IHxy yz IHyz| | ]; try now constructor.
    inv IHxy; inv IHyz; constructor.
  - intros H; inv H; eauto using le.
Qed.

Theorem le_antisym : forall x y,
  le x y -> le y x -> x = y.
Proof.
  intros x y.
  rewrite 2!le_le'.
  intros []; trivial; intros H; inv H.
Qed.

Theorem le_dec : forall x y, { le x y } + { ~le x y }.
  intros x y.
  destruct x, y; eauto using le; right; rewrite le_le';
  intros H; inv H.
Qed.

In this case, however, I think that using an inductive characterization of le is not a good idea, because the boolean version is more useful. Naturally, there are occasions where you would like two characterizations of a relation: for instance, sometimes you would like a boolean test for equality on a type, but would like to use = for rewriting. The ssreflect proof language makes it easy to work in this style. For instance, here is another version of your first proof attempt. (The reflect P b predicate means that the proposition P is equivalent to the assertion b = true.)

From mathcomp Require Import ssreflect ssrfun ssrbool.

Inductive t : Set := A | B | C.

Inductive le : t -> t -> Prop :=
  | le_refl : forall x, le x x
  | le_trans : forall x y z, le x y -> le y z -> le x z
  | le_A_B : le A B
  | le_B_C : le B C .

Definition leb (x y : t) : bool :=
  match x, y with
  | A, _ => true
  | _, C => true
  | B, B => true
  | _, _ => false
  end.

Theorem leP x y : reflect (le x y) (leb x y).
Proof.
apply/(iffP idP); first by case: x; case y=> //=; eauto using le.
by elim=> [[]| | |] //= [] [] [].
Qed.

Theorem le_antisym x y : le x y -> le y x -> x = y.
Proof. by case: x; case: y; move=> /leP ? /leP ?. Qed.

Theorem le_dec : forall x y, { le x y } + { ~le x y }.
Proof. by move=> x y; case: (leP x y); eauto. Qed.