(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   dec.
   Some utilities for proving decidability of predicates.

   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import Arith.
Require Import ZArith.
Require Import EqNat.

(** Checks that all nats before n are P *)

Fixpoint allbefore (P : nat -> Prop) (n : nat) {struct n} : Prop :=
  match n with
  | O => True
  | S x => allbefore P x /\ P x
  end.

(** Checks that some nat before n is P *)

Fixpoint exbefore (P : nat -> Prop) (n : nat) {struct n} : Prop :=
  match n with
  | O => False
  | S x => exbefore P x \/ P x
  end.

Theorem allbefore_ok :
 forall (P : nat -> Prop) (n : nat),
 (forall q : nat, q < n -> P q) <-> allbefore P n.
Proof.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: forall n m : nat, iff (@eq nat n m) (@eq bool (Nat.eqb n m) true) *)
   simple induction n.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   simpl in |- *.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: forall _ : @eq nat n0 n1, @eq nat n0 n1 *)
(* Goal: forall _ : istrue (Nat.eqb (S n0) (S n1)), @eq nat (S n0) (S n1) *)
   tauto.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: P q *)
(* Goal: forall (n : nat) (_ : iff (forall (q : nat) (_ : lt q n), P q) (allbefore P n)), iff (forall (q : nat) (_ : lt q (S n)), P q) (allbefore P (S n)) *)
   elim (lt_n_O q).
(* Goal: @eq Z x y *)
   assumption.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   simpl in |- *.
(* Goal: forall (n : nat) (_ : iff (@ex nat (fun q : nat => and (lt q n) (P q))) (exbefore P n)), iff (@ex nat (fun q : nat => and (lt q (S n)) (P q))) (exbefore P (S n)) *)
   intros m IHm.
(* Goal: iff (@ex nat (fun q : nat => and (lt q (S m)) (P q))) (or (exbefore P m) (P m)) *)
   elim IHm.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: @eq Z x y *)
   apply H.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: P q *)
(* Goal: P m *)
(* Goal: forall (_ : and (allbefore P m) (P m)) (q : nat) (_ : lt q (S m)), P q *)
   apply (H1 q).
(* Goal: forall n m : nat, or (lt n m) (not (lt n m)) *)
   unfold lt in |- *.
(* Goal: le (S q) (S m) *)
(* Goal: P m *)
(* Goal: forall (_ : and (allbefore P m) (P m)) (q : nat) (_ : lt q (S m)), P q *)
   unfold lt in H2.
(* Goal: le (S x) (S m) *)
(* Goal: P x *)
(* Goal: forall _ : P m, @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   apply le_S.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: P m *)
(* Goal: forall (_ : and (allbefore P m) (P m)) (q : nat) (_ : lt q (S m)), P q *)
   apply (H1 m).
(* Goal: forall n m : nat, or (lt n m) (not (lt n m)) *)
   unfold lt in |- *.
(* Goal: le (S m) (S m) *)
(* Goal: P m *)
   apply le_n.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: False *)
(* Goal: forall _ : not (forall (x : nat) (_ : lt x N), not (P x)), @ex nat (fun x : nat => and (lt x N) (P x)) *)
   elim H1.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: P q *)
   elim (le_lt_or_eq q m).
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: istrue (Nat.eqb n0 n1) *)
(* Goal: forall _ : istrue (Nat.eqb (S n0) (S n1)), @eq nat (S n0) (S n1) *)
   apply H0.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: P q *)
(* Goal: le q m *)
   rewrite H5.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: le (S x) (S m) *)
(* Goal: P x *)
(* Goal: forall _ : P m, @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   unfold lt in H4.
(* Goal: le q m *)
   apply (le_S_n q m).
(* Goal: @eq Z x y *)
   assumption.
Qed.

Theorem exbefore_ok :
 forall (P : nat -> Prop) (n : nat),
 (exists q : nat, q < n /\ P q) <-> exbefore P n.
Proof.
(* Goal: forall (P : forall _ : nat, Prop) (N : nat) (_ : forall n : nat, or (P n) (not (P n))), or (@ex nat (fun x : nat => and (lt x N) (P x))) (not (@ex nat (fun x : nat => and (lt x N) (P x)))) *)
   intro P.
(* Goal: forall n m : nat, iff (@eq nat n m) (@eq bool (Nat.eqb n m) true) *)
   simple induction n.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   simpl in |- *.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
(* Goal: forall _ : not (@ex nat (fun x : nat => and (lt x M) (P x))), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   elim H.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x O) (P x)) *)
(* Goal: forall (n : nat) (_ : forall _ : not (forall (x : nat) (_ : lt x n), not (P x)), @ex nat (fun x : nat => and (lt x n) (P x))) (_ : not (forall (x : nat) (_ : lt x (S n)), not (P x))), @ex nat (fun x : nat => and (lt x (S n)) (P x)) *)
   elim H0.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: not (P x) *)
(* Goal: forall (n : nat) (_ : forall _ : not (forall (x : nat) (_ : lt x n), not (P x)), @ex nat (fun x : nat => and (lt x n) (P x))) (_ : not (forall (x : nat) (_ : lt x (S n)), not (P x))), @ex nat (fun x : nat => and (lt x (S n)) (P x)) *)
   elim (lt_n_O x).
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
(* Goal: forall _ : not (@ex nat (fun x : nat => and (lt x M) (P x))), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   elim H.
(* Goal: forall (n : nat) (_ : iff (@ex nat (fun q : nat => and (lt q n) (P q))) (exbefore P n)), iff (@ex nat (fun q : nat => and (lt q (S n)) (P q))) (exbefore P (S n)) *)
   intros m IHm.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   simpl in |- *.
(* Goal: iff (@ex nat (fun q : nat => and (lt q (S m)) (P q))) (or (exbefore P m) (P m)) *)
   elim IHm.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: False *)
(* Goal: forall _ : not (forall (x : nat) (_ : lt x N), not (P x)), @ex nat (fun x : nat => and (lt x N) (P x)) *)
   elim H1.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: False *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   elim H2.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: or (exbefore P m) (P m) *)
(* Goal: forall _ : or (exbefore P m) (P m), @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   elim (le_lt_or_eq x m).
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: forall _ : P M, or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall _ : not (P M), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   left.
(* Goal: @eq Z x y *)
   apply H.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
   split with x.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: forall _ : not (P M), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   right.
(* Goal: P m *)
(* Goal: le x m *)
(* Goal: forall _ : or (exbefore P m) (P m), @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   rewrite H5 in H4.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: le x m *)
(* Goal: forall _ : or (exbefore P m) (P m), @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   apply (le_S_n x m).
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: False *)
(* Goal: forall _ : not (forall (x : nat) (_ : lt x N), not (P x)), @ex nat (fun x : nat => and (lt x N) (P x)) *)
   elim H1.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
(* Goal: forall _ : P m, @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   case H0.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
   split with x.
(* Goal: @eq bool true false *)
(* Goal: forall (_ : forall _ : @eq comparison Lt Eq, @eq Z x y) (_ : forall _ : @eq Z x y, @eq comparison Lt Eq) (_ : not (@eq Z x y)), @eq bool false false *)
(* Goal: forall (_ : forall _ : @eq comparison Gt Eq, @eq Z x y) (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : not (@eq Z x y)), @eq bool false false *)
(* Goal: forall _ : @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false, not (@eq Z x y) *)
   elim H3.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: forall n m : nat, or (lt n m) (not (lt n m)) *)
   unfold lt in |- *.
(* Goal: le (S x) (S m) *)
(* Goal: P x *)
(* Goal: forall _ : P m, @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   unfold lt in H4.
(* Goal: le (S x) (S m) *)
(* Goal: P x *)
(* Goal: forall _ : P m, @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   apply le_S.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun q : nat => and (lt q (S m)) (P q)) *)
   split with m.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: forall n m : nat, or (lt n m) (not (lt n m)) *)
   unfold lt in |- *.
(* Goal: le (S m) (S m) *)
(* Goal: P m *)
   apply le_n.
(* Goal: @eq Z x y *)
   assumption.
Qed.


(** some decidable relations on nat *)

Lemma eqdec : forall n m : nat, n = m \/ n <> m.
Proof.
(* Goal: forall n m : nat, iff (@eq nat n m) (@eq bool (Nat.eqb n m) true) *)
   simple induction n.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: iff (@eq nat (S n1) m) (@eq bool (Nat.eqb (S n1) m) true) *)
   case m.
(* Goal: forall _ : P M, or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall _ : not (P M), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   left.
(* Goal: @eq bool false false *)
(* Goal: forall _ : @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false, not (@eq Z x y) *)
   reflexivity.
(* Goal: forall _ : not (P M), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   right.
(* Goal: forall _ : @eq comparison Gt Eq, False *)
(* Goal: @eq comparison Gt Eq *)
   discriminate.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: iff (@eq nat (S n1) m) (@eq bool (Nat.eqb (S n1) m) true) *)
   case m.
(* Goal: forall _ : not (P M), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   right.
(* Goal: forall _ : @eq comparison Gt Eq, False *)
(* Goal: @eq comparison Gt Eq *)
   discriminate.
(* Goal: forall n : nat, or (@eq nat (S n0) (S n)) (not (@eq nat (S n0) (S n))) *)
   intro m0.
(* Goal: or (@eq nat (S n0) (S m0)) (not (@eq nat (S n0) (S m0))) *)
   elim (H m0).
(* Goal: forall _ : P M, or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall _ : not (P M), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   left.
(* Goal: @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end true *)
(* Goal: forall _ : @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end true, @eq Z x y *)
   rewrite H0.
(* Goal: @eq bool false false *)
(* Goal: forall _ : @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false, not (@eq Z x y) *)
   reflexivity.
(* Goal: forall _ : not (P M), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   right.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: istrue (Nat.eqb n0 n1) *)
(* Goal: forall _ : istrue (Nat.eqb (S n0) (S n1)), @eq nat (S n0) (S n1) *)
   apply H0.
(* Goal: @eq nat n0 m0 *)
   inversion H1.
(* Goal: @eq bool false false *)
(* Goal: forall _ : @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false, not (@eq Z x y) *)
   reflexivity.
Qed.

Lemma ledec : forall n m : nat, n <= m \/ ~ n <= m.
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. elim (le_or_lt n m).
(* Goal: @eq Z x y *)
   left. assumption.
(* Goal: @eq Z x y *)
   right. apply lt_not_le. assumption.
Qed.

Lemma ltdec : forall n m : nat, n < m \/ ~ n < m.
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   unfold lt in |- *. intros. apply ledec.
Qed.

Lemma gedec : forall n m : nat, n >= m \/ ~ n >= m.
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   unfold ge in |- *. intros. apply ledec.
Qed.

Lemma gtdec : forall n m : nat, n > m \/ ~ n > m.
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   unfold gt in |- *. intros. apply ltdec.
Qed.

(** relations on Z *)

Lemma zeqdec : forall x y : Z, x = y \/ x <> y.
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. elim (dec_eq x y). left. assumption. right. assumption.
Qed.

(** the connectives preserve decidability *)

Lemma notdec : forall P : Prop, P \/ ~ P -> ~ P \/ ~ ~ P.
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. elim H.
(* Goal: not (@eq Z x y) *)
   right. intro.  apply H1. assumption.
(* Goal: @eq Z x y *)
   left. assumption.
Qed.

Lemma anddec :
 forall P Q : Prop, P \/ ~ P -> Q \/ ~ Q -> P /\ Q \/ ~ (P /\ Q).
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. elim H. elim H0.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   left. split. assumption. assumption.
(* Goal: not (@eq Z x y) *)
   right. intro. apply H1. elim H3. intros. assumption.
(* Goal: not (@eq Z x y) *)
   right. intro. apply H1. elim H2. intros. assumption.
Qed.

Lemma ordec :
 forall P Q : Prop, P \/ ~ P -> Q \/ ~ Q -> (P \/ Q) \/ ~ (P \/ Q).
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. elim H.
(* Goal: @eq Z x y *)
   left. left. assumption.
(* Goal: @ex nat (fun x : nat => and (lt x O) (P x)) *)
(* Goal: forall (n : nat) (_ : forall _ : not (forall (x : nat) (_ : lt x n), not (P x)), @ex nat (fun x : nat => and (lt x n) (P x))) (_ : not (forall (x : nat) (_ : lt x (S n)), not (P x))), @ex nat (fun x : nat => and (lt x (S n)) (P x)) *)
   elim H0.
(* Goal: @eq Z x y *)
   left. right. assumption.
(* Goal: not (@eq Z x y) *)
   right. intro. elim H3. assumption. assumption.
Qed.

Lemma impdec :
 forall P Q : Prop, P \/ ~ P -> Q \/ ~ Q -> (P -> Q) \/ ~ (P -> Q).
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. elim H.
(* Goal: @ex nat (fun x : nat => and (lt x O) (P x)) *)
(* Goal: forall (n : nat) (_ : forall _ : not (forall (x : nat) (_ : lt x n), not (P x)), @ex nat (fun x : nat => and (lt x n) (P x))) (_ : not (forall (x : nat) (_ : lt x (S n)), not (P x))), @ex nat (fun x : nat => and (lt x (S n)) (P x)) *)
   elim H0.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   left. intros. assumption.
(* Goal: not (@eq Z x y) *)
   right. intro. apply H1. apply H3. assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   left. intros. elim H1. assumption.
Qed.

Lemma iffdec :
 forall P Q : Prop, P \/ ~ P -> Q \/ ~ Q -> (P <-> Q) \/ ~ (P <-> Q).
Proof.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   unfold iff in |- *. intros.
(* Goal: or (and (forall _ : P, Q) (forall _ : Q, P)) (not (and (forall _ : P, Q) (forall _ : Q, P))) *)
   apply anddec.
(* Goal: @eq Z x y *)
   apply impdec. assumption. assumption.
(* Goal: @eq Z x y *)
   apply impdec. assumption. assumption.
Qed.

(** bounded quantifiers preserve decidability *)

Theorem alldec :
 forall (P : nat -> Prop) (N : nat),
 (forall n : nat, P n \/ ~ P n) ->
 (forall x : nat, x < N -> P x) \/ ~ (forall x : nat, x < N -> P x).
Proof.
(* Goal: forall (P : forall _ : nat, Prop) (N : nat) (_ : forall n : nat, or (P n) (not (P n))), or (@ex nat (fun x : nat => and (lt x N) (P x))) (not (@ex nat (fun x : nat => and (lt x N) (P x)))) *)
   intro P. simple induction N.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   left. intros. elim (lt_n_O x). assumption.
(* Goal: forall (n : nat) (_ : forall _ : forall n0 : nat, or (P n0) (not (P n0)), or (@ex nat (fun x : nat => and (lt x n) (P x))) (not (@ex nat (fun x : nat => and (lt x n) (P x))))) (_ : forall n0 : nat, or (P n0) (not (P n0))), or (@ex nat (fun x : nat => and (lt x (S n)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S n)) (P x)))) *)
   intros M IH decP.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
   elim IH. elim (decP M).
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   left. intros. unfold lt in H1. elim (le_lt_or_eq x M). intros.
(* Goal: @eq Z x y *)
   apply H0. assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. rewrite H2. assumption.
(* Goal: @eq Z x y *)
   apply le_S_n. assumption.
(* Goal: not (@eq Z x y) *)
   right. intro. apply H. apply H1. apply lt_n_Sn.
(* Goal: not (@eq Z x y) *)
   right. intro. apply H. intros. apply H0. apply lt_S. assumption.
(* Goal: @eq Z x y *)
   assumption.
Qed.

Theorem exdec :
 forall (P : nat -> Prop) (N : nat),
 (forall n : nat, P n \/ ~ P n) ->
 (exists x : nat, x < N /\ P x) \/ ~ (exists x : nat, x < N /\ P x).
Proof.
(* Goal: forall (P : forall _ : nat, Prop) (N : nat) (_ : forall n : nat, or (P n) (not (P n))), or (@ex nat (fun x : nat => and (lt x N) (P x))) (not (@ex nat (fun x : nat => and (lt x N) (P x)))) *)
   intro P. simple induction N.
(* Goal: forall _ : forall n : nat, or (P n) (not (P n)), or (@ex nat (fun x : nat => and (lt x O) (P x))) (not (@ex nat (fun x : nat => and (lt x O) (P x)))) *)
(* Goal: forall (n : nat) (_ : forall _ : forall n0 : nat, or (P n0) (not (P n0)), or (@ex nat (fun x : nat => and (lt x n) (P x))) (not (@ex nat (fun x : nat => and (lt x n) (P x))))) (_ : forall n0 : nat, or (P n0) (not (P n0))), or (@ex nat (fun x : nat => and (lt x (S n)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S n)) (P x)))) *)
   intro decP.
(* Goal: not (@eq Z x y) *)
   right. intro. elim H. intros. elim H0. intros. elim (lt_n_O x). assumption.
(* Goal: forall (n : nat) (_ : forall _ : forall n0 : nat, or (P n0) (not (P n0)), or (@ex nat (fun x : nat => and (lt x n) (P x))) (not (@ex nat (fun x : nat => and (lt x n) (P x))))) (_ : forall n0 : nat, or (P n0) (not (P n0))), or (@ex nat (fun x : nat => and (lt x (S n)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S n)) (P x)))) *)
   intros M IH decP.
(* Goal: forall _ : P M, or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall _ : not (P M), or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   elim IH. left.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   elim H. intros. split with x. elim H0. intros.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: @eq Z x y *)
   apply lt_S. assumption.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: or (@ex nat (fun x : nat => and (lt x (S M)) (P x))) (not (@ex nat (fun x : nat => and (lt x (S M)) (P x)))) *)
(* Goal: forall n : nat, or (P n) (not (P n)) *)
   elim (decP M).
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   left. split with M. split. apply lt_n_Sn.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: not (@eq Z x y) *)
   right. intro.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   elim H1. intros. elim H2. intros.
(* Goal: not (P x) *)
   unfold lt in H3. elim (le_lt_or_eq x M).
(* Goal: not (@eq Z x y) *)
   intro. apply H. split with x. split. assumption.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: not (@eq Z x y) *)
   intro. apply H0. rewrite <- H5. assumption.
(* Goal: @eq Z x y *)
   apply le_S_n. assumption.
(* Goal: @eq Z x y *)
   assumption.
Qed.

(** De Morgan's law holds for decidable P if the quantifiers are bounded *)

Theorem decDeMorgan :
 forall (N : nat) (P : nat -> Prop),
 (forall n : nat, P n \/ ~ P n) ->
 ((exists x : nat, x < N /\ P x) <-> ~ (forall x : nat, x < N -> ~ P x)).
Proof.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: @ex nat (fun x : nat => and (lt x O) (P x)) *)
(* Goal: forall (n : nat) (_ : forall _ : not (forall (x : nat) (_ : lt x n), not (P x)), @ex nat (fun x : nat => and (lt x n) (P x))) (_ : not (forall (x : nat) (_ : lt x (S n)), not (P x))), @ex nat (fun x : nat => and (lt x (S n)) (P x)) *)
   elim H0.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: False *)
(* Goal: forall _ : not (forall (x : nat) (_ : lt x N), not (P x)), @ex nat (fun x : nat => and (lt x N) (P x)) *)
   elim H1.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: False *)
(* Goal: forall _ : not (forall (x : nat) (_ : lt x N), not (P x)), @ex nat (fun x : nat => and (lt x N) (P x)) *)
   apply (H2 x H3 H4).
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   elim N. intros. elim H0. intros. elim (lt_n_O x). assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros M IH. intros.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
   elim (H M).
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
(* Goal: forall _ : not (P M), @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
   split with M.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: lt M (S M) *)
(* Goal: P M *)
(* Goal: forall _ : not (P M), @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
   apply lt_n_Sn.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
   cut (~ (forall x : nat, x < M -> ~ P x)).
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
   elim IH.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @ex nat (fun x : nat => and (lt x (S M)) (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
   split with x.
(* Goal: @eq bool true false *)
(* Goal: forall (_ : forall _ : @eq comparison Lt Eq, @eq Z x y) (_ : forall _ : @eq Z x y, @eq comparison Lt Eq) (_ : not (@eq Z x y)), @eq bool false false *)
(* Goal: forall (_ : forall _ : @eq comparison Gt Eq, @eq Z x y) (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : not (@eq Z x y)), @eq bool false false *)
(* Goal: forall _ : @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false, not (@eq Z x y) *)
   elim H3.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: lt x (S M) *)
(* Goal: P x *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
(* Goal: not (forall (x : nat) (_ : lt x M), not (P x)) *)
   apply lt_S.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: not (@eq Z x y) *)
   intro.
(* Goal: istrue (Nat.eqb n0 n1) *)
(* Goal: forall _ : istrue (Nat.eqb (S n0) (S n1)), @eq nat (S n0) (S n1) *)
   apply H0.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: not (P x) *)
   elim (le_lt_or_eq x M).
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: @eq comparison Gt Eq *)
   apply H2.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: not (P x) *)
(* Goal: le x M *)
   rewrite H4.
(* Goal: @eq Z x y *)
   assumption.
(* Goal: le x M *)
   unfold lt in H3.
(* Goal: le x M *)
   apply le_S_n.
(* Goal: @eq Z x y *)
   assumption.
Qed.


(** Some nice boolean stuff... *)

Definition istrue (b : bool) := if b then True else False.

Lemma beq_nat_ok : forall n m : nat, n = m <-> istrue (beq_nat n m).
Proof.
(* Goal: forall n m : nat, iff (@eq nat n m) (@eq bool (Nat.eqb n m) true) *)
   simple induction n.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   intro m. case m. simpl in |- *. tauto. simpl in |- *. split. discriminate. tauto.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   case m. simpl in |- *. split. discriminate. tauto.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. elim (H n1).
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   split.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   intros. simpl in |- *. apply H0. injection H2. tauto.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   simpl in |- *. intros. rewrite (H1 H2). reflexivity.
Qed.

Lemma beq_nat_eq : forall n m : nat, n = m <-> beq_nat n m = true.
Proof.
(* Goal: forall n m : nat, iff (@eq nat n m) (@eq bool (Nat.eqb n m) true) *)
   simple induction n.
(* Goal: not (@eq Z x y) *)
   intro. case m.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   simpl in |- *. split. reflexivity. reflexivity.
(* Goal: not (@eq Z x y) *)
   simpl in |- *. split. intro. discriminate. intro. discriminate.
(* Goal: iff (@eq nat (S n1) m) (@eq bool (Nat.eqb (S n1) m) true) *)
   intros n1 IH. intro m. case m.
(* Goal: not (@eq Z x y) *)
   simpl in |- *. split. intro. discriminate. intro. discriminate.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   intro m1. intros. simpl in |- *.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   elim (IH m1). split.
(* Goal: not (@eq Z x y) *)
   intro. injection H1. assumption.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. rewrite H0. reflexivity. assumption.
Qed.

Lemma beq_nat_neq : forall n m : nat, n <> m <-> beq_nat n m = false.
Proof.
(* Goal: forall n m : nat, iff (@eq nat n m) (@eq bool (Nat.eqb n m) true) *)
   simple induction n.
(* Goal: not (@eq Z x y) *)
   intro. case m. simpl in |- *. split.
(* Goal: not (@eq Z x y) *)
   intro. elim H. reflexivity. intro. discriminate.
(* Goal: not (@eq Z x y) *)
   intro m1. simpl in |- *. split. reflexivity. intro. discriminate.
(* Goal: iff (@eq nat (S n1) m) (@eq bool (Nat.eqb (S n1) m) true) *)
   intros n1 IH. intro m. case m.
(* Goal: not (@eq Z x y) *)
   simpl in |- *. split. reflexivity. intro. discriminate.
(* Goal: iff (@eq nat (S n1) (S m1)) (@eq bool (Nat.eqb (S n1) (S m1)) true) *)
   intro m1. simpl in |- *.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   elim (IH m1). split.
(* Goal: not (@eq Z x y) *)
   intro. apply H. intro. elim H1. rewrite H2. reflexivity.
(* Goal: not (@eq Z x y) *)
   intro. intro. elim H0. assumption. injection H2. intro. assumption.
Qed.

Lemma zeq_bool_eq : forall x y : Z, x = y <-> Zeq_bool x y = true.
Proof.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   intros. elim (Zcompare_Eq_iff_eq x y). intros. unfold Zeq_bool in |- *. split.

   (* -> *)
(* Goal: not (@eq Z x y) *)
   intro. rewrite H0.
(* Goal: @eq Z x y *)
   reflexivity. assumption.

   (* <- *)
(* Goal: not (@eq Z x y) *)
   intro. apply H. generalize H1.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison (Z.compare x y) Eq) (_ : @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false), not (@eq Z x y) *)
   elim (x ?= y)%Z.
(* Goal: not (@eq Z x y) *)
   intro. reflexivity.
(* Goal: not (@eq Z x y) *)
   intro. discriminate H2.
(* Goal: not (@eq Z x y) *)
   intro. discriminate H2.
Qed.

Lemma zeq_bool_neq : forall x y : Z, x <> y <-> Zeq_bool x y = false.
Proof.
(* Goal: iff (not (@eq Z x y)) (@eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false) *)
   intros. elim (Zcompare_Eq_iff_eq x y). intros. unfold Zeq_bool in |- *. split.

   (* -> *)
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison (Z.compare x y) Eq) (_ : @eq bool match Z.compare x y with | Eq => true | Lt => false | Gt => false end false), not (@eq Z x y) *)
   generalize H0. generalize H. elim (x ?= y)%Z.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. elim H3. apply H1. reflexivity.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. reflexivity.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. reflexivity.

   (* <- *)
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. generalize H1. generalize H0. elim (x ?= y)%Z.
(* Goal: forall (_ : forall _ : @eq Z x y, @eq comparison Gt Eq) (_ : @eq bool false false), not (@eq Z x y) *)
   intros. discriminate H3.
(* Goal: not (@eq Z x y) *)
   intros. intro. cut (Datatypes.Lt = Datatypes.Eq). discriminate.
(* Goal: @eq Z x y *)
   apply H2. assumption.
(* Goal: not (@eq Z x y) *)
   intros. intro. cut (Datatypes.Gt = Datatypes.Eq). discriminate.
(* Goal: @eq Z x y *)
   apply H2. assumption.
Qed.
