5
$\begingroup$

I am reading the software foundations for Coq, and one property that I would like to prove is the excluded middle for $\leq$. The definitions are the following

Inductive nat : Type :=
| O
| S (n : nat).


Inductive bool : Type :=
  | true
  | false.

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
end.
Notation "x <=? y" := (leb x y) (at level 70).
Theorem EQEM: forall n m, n <=? m = true \/ n <=? m = false.

The proof is easy but how to implement it in Coq? Since the function is to type bool and terminates, the output is always a bool, and that should complete the proof. Induction seems to lead nowhere, although an infinite descent argument also concludes the matter trivially, perhaps there is something I missed...

$\endgroup$
7
  • $\begingroup$ Universal statements in Peano arithmetic are usually proved by induction, this case you need a double induction, on both $n$ and $m$. It's basically the repetition of the definition of leb. $\endgroup$
    – Berci
    Sep 19, 2020 at 15:18
  • $\begingroup$ You have described anti-symmetry of $\leq$ in the title, but some sort of "excluded middle" in the Coq code. I'm not familiar with Coq, in general it's true that for all booleans you have $b=\text{true}$ or $b=\text{false}$ which should have a short proof via pattern matching - mostly a matter of knowing Coq syntax. Anti-symmetry of $\leq$ is less trivial, but the key point is that it's trivial if $n=0$ or $m=0$ and otherwise you can use that (leb (S n) (S m)) is judgmentally equal to (leb n m) - so the proof is by matching into cases on if either $n$ or $m$ is zero. $\endgroup$ Sep 19, 2020 at 15:47
  • $\begingroup$ @Berci yes, strong double induction does work. But to prove strong induction principle, some properties of $\leq$ are needed. $\endgroup$
    – Dole
    Sep 19, 2020 at 21:32
  • $\begingroup$ Are you able to prove $x = 0 \lor x \ne 0$ ? $\endgroup$
    – DanielV
    Sep 19, 2020 at 22:16
  • $\begingroup$ @DanielV Yes, that is no problem. $\endgroup$
    – Dole
    Sep 19, 2020 at 23:17

1 Answer 1

0
$\begingroup$

And here are the answers, thank you for the very helpful comments. First, as was pointed out, a regular induction can solve the problem. Some attention must be paid to the order of operations, it is possible to get stuck.

Theorem EQEM: forall n m, n <=? m = true \/ n <=? m = false.
induction n. intros m. destruct m. left. reflexivity.
left. reflexivity. intros m. induction m. right.
reflexivity. specialize (IHn m). simpl. exact IHn.
Qed.

However, the substitution proof works as well.

Theorem LEMB: forall b: bool, b = true \/ b = false.
Proof. destruct b. left. reflexivity. right. reflexivity. Qed.

Theorem EQEM: forall n m, n <=? m = true \/ n <=? m = false.
Proof. pose LEMB as H. intros n m. specialize (H (n <=? m)).
exact H. Qed.
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .