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
- How can I prove, that
le C A
is a false premise? - Is there an other other proof strategy that I should use?
- 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 ofle 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: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. (Thereflect P b
predicate means that the propositionP
is equivalent to the assertionb = true
.)