How to prove decidability of a partial order inductive predicate?

Link:: https://stackoverflow.com/q/50390613

Display all goals and responses

Question

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.forall x y : t, le x y <-> leb x y = true
Proof.forall x y : t, le x y <-> leb x y = true
  intros x y.x, y: t
le x y <-> leb x y = true split; intro H.x, y: t
H: le x y
leb x y = true
x, y: t
H: leb x y = true
le x y
  -x, y: t
H: le x y
leb x y = true induction H; destruct_ts; simpl in *; congruence.
  -x, y: t
H: leb x y = true
le x y destruct_ts; eauto using le; simpl in *; congruence.
Qed.

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

Theorem le_dec : forall x y, { le x y } + { ~le x y }.forall x y : t, {le x y} + {~ le x y}
  intros x y.x, y: t
{le x y} + {~ le x y} destruct x, y; eauto using le.{le B A} + {~ le B A}
{le C A} + {~ le C A}
{le C B} + {~ le C B}
  -{le B A} + {~ le B A} apply right.~ le B A intros H. (* Stuck here *)H: le B A
False
    inv H.y: t
H0: le B y
H1: le y A
False rewrite le_iff_leb in *.y: t
H0: leb B y = true
H1: leb y A = true
False
    destruct y; simpl in *; congruence.
  -{le C A} + {~ le C A} apply right.~ le C A intros H. (* Same thing *)H: le C A
False
    inv H.y: t
H0: le C y
H1: le y A
False rewrite le_iff_leb in *.y: t
H0: leb C y = true
H1: leb y A = true
False
    destruct y; simpl in *; congruence.
  -{le C B} + {~ le C B} apply right.~ le C B intros H. (* Same thing *)H: le C B
False
    inv H.y: t
H0: le C y
H1: le y B
False rewrite le_iff_leb in *.y: t
H0: leb C y = true
H1: leb y B = true
False
    destruct y; simpl in *; congruence.
Qed.

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 B A
  ============================
  False

Questions

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

Answer

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.x: t
x <> A -> ~ le x A
Proof.x: t
x <> A -> ~ le x A remember A; intros; induction 1; subst; firstorder congruence. Qed.

Lemma not_leCX x : x <> C -> ~ le C x.x: t
x <> C -> ~ le C x
Proof.x: t
x <> C -> ~ le C x 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 }.x, y: t
{le x y} + {~ le x y}
Proof.x, y: t
{le x y} + {~ le x y}
  destruct x, y; try (left; abstract constructor).{le A C} + {~ le A C}
{le B A} + {~ le B A}
{le C A} + {~ le C A}
{le C B} + {~ le C B}
  -{le A C} + {~ le A C} left; abstract (eapply le_trans; constructor).
  -{le B A} + {~ le B A} right; abstract now apply not_leXA.
  -{le C A} + {~ le C A} right; abstract now apply not_leCX.
  -{le C B} + {~ le C B} 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
: {le B A} + {~ le B A}

and

Compute le_dec' B A.= right
    (not_leXA B
       (fun x : B = A =>
        match
          x in (_ = H) return (H = A -> False)
        with
        | eq_refl =>
            fun x0 : B = A =>
            match
              match
                x0 in (_ = H)
                return
                  match H with
                  | B => True
                  | _ => False
                  end
              with
              | eq_refl => I
              end return False
            with
            end
        end eq_refl))
: {le B A} + {~ le B A}