How to prove decidability of a partial order inductive predicate?

Question

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.

Answer 1

Note that you can make use of the definitions in Relations to define your order relation. For instance, it contains a definition of reflexive and transitive closure named clos_refl_trans. The resulting proofs are similar to those based on your definitions (cf. @Anton's answer).

Require Import Relations.

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

Inductive le : t -> t -> Prop :=
  | le_A_B : le A B
  | le_B_C : le B C.

Definition le' := clos_refl_trans _ le.

Lemma A_minimal : forall x, x <> A -> ~ le' x A.
Proof.
  intros. intros contra. remember A as a. induction contra; subst.
  - inversion H0.
  - contradiction.
  - destruct y; apply IHcontra2 + apply IHcontra1; congruence.
Qed.

Lemma C_maximal : forall x, x <> C -> ~ le' C x.
Proof.
  intros. intros contra. remember C as c. induction contra; subst.
  - inversion H0.
  - contradiction.
  - destruct y; apply IHcontra2 + apply IHcontra1; congruence.
Qed.

Lemma le'_antisym : forall x y,
  le' x y -> le' y x -> x = y.
Proof.
  intros. induction H.
  - destruct H.
    + apply A_minimal in H0; try discriminate. contradiction.
    + apply C_maximal in H0; try discriminate. contradiction.
  - reflexivity.
  - fold le' in *. rewrite IHclos_refl_trans1 by (eapply rt_trans; eassumption).
    apply IHclos_refl_trans2; (eapply rt_trans; eassumption).
Qed.

Answer 2

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.

Answer 3

I'd also go with Arthur's solution. But let me demonstrate another approach.

First, we'll need a couple of supporting lemmas:

Lemma not_leXA x : x <> A -> ~ le x A.
Proof. remember A; intros; induction 1; subst; firstorder congruence. Qed.

Lemma not_leCX x : x <> C -> ~ le C x.
Proof. remember C; intros; induction 1; subst; firstorder congruence. Qed.

Now we can define le_dec:

Definition le_dec x y : { le x y } + { ~le x y }.
Proof.
  destruct x, y; try (left; abstract constructor).
  - left; abstract (eapply le_trans; constructor).
  - right; abstract now apply not_leXA.
  - right; abstract now apply not_leCX.
  - right; abstract now apply not_leCX.
Defined.

Notice that I used Defined instead of Qed -- now you can calculate with le_dec, which is usually the point of using the sumbool type.

I also used abstract to conceal the proof terms from the evaluator. E.g. let's imagine I defined a le_dec' function which is the same as le_dec, but with all abstract removed, then we would get the following results when trying to compute le_dec B A / le_dec' B A :

Compute le_dec B A.
(* ==> right le_dec_subproof5 *) 

and

Compute le_dec' B A.
(* ==> right
     (not_leXA B
        (fun x : B = A =>
         match x in (_ = x0) return (x0 = A -> False) with
         | eq_refl =>
             fun x0 : B = A =>
             match
               match
                 x0 in (_ = x1)
                 return match x1 with
                        | B => True
                        | _ => False
                        end
               with
               | eq_refl => I
               end return False
             with
             end
         end eq_refl)) *)