(**
 * dec.
 * Some utilities for proving decidability of predicates.
 *
 * @author Olga Caprotti and Martijn Oostdijk
 * @version $Revision$
 *)

Require Arith.
Require ZArith.
Require EqNat.

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

Fixpoint allbefore [P:nat->Prop; n:nat]: Prop :=
   Cases n of
      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]: Prop :=
   Cases n of
      O     => False
    | (S x) => (exbefore P x) \/ (P x)
   end.

Theorem allbefore_ok: (P:nat->Prop)(n:nat)
            ((q: nat)(lt q n) -> (P q)) <-> (allbefore P n).
Proof.
   Intro.
   Induction n.
   Simpl.
   Split.
   Tauto.
   Intros.
   Elim (lt_n_O q).
   Assumption.
   Simpl.
   Intros m IHm.
   Elim IHm.
   Intros.
   Split.
   Intros.
   Split.
   Apply H.
   Intros.
   Apply (H1 q).
   Unfold lt.
   Unfold lt in H2.
   Apply le_S.
   Assumption.
   Apply (H1 m).
   Unfold lt.
   Apply le_n.
   Intro.
   Elim H1.
   Intro.
   Intro.
   Intros.
   Elim (le_lt_or_eq q m).
   Intros.
   Apply H0.
   Assumption.
   Assumption.
   Intros.
   Rewrite H5.
   Assumption.
   Unfold lt in H4.
   Apply (le_S_n q m).
   Assumption.
Qed.

Theorem exbefore_ok: (P:nat->Prop)(n:nat)
            (EX q:nat | (lt q n) /\ (P q)) <-> (exbefore P n).
Proof.
   Intro P.
   Induction n.
   Simpl.
   Split.
   Intros.
   Elim H.
   Intros.
   Elim H0.
   Intros.
   Elim (lt_n_O x).
   Assumption.
   Intros.
   Elim H.
   Intros m IHm.
   Simpl.
   Elim IHm.
   Intros.
   Split.
   Intro.
   Elim H1.
   Intro.
   Intros.
   Elim H2.
   Intros.
   Elim (le_lt_or_eq x m).
   Intros.
   Left.
   Apply H.
   Split with x.
   Split.
   Assumption.
   Assumption.
   Intros.
   Right.
   Rewrite H5 in H4.
   Assumption.
   Apply (le_S_n x m).
   Assumption.
   Intros.
   Elim H1.
   Intros.
   Case H0.
   Assumption.
   Intros.
   Split with x.
   Elim H3.
   Intros.
   Split.
   Unfold lt.
   Unfold lt in H4.
   Apply le_S.
   Assumption.
   Assumption.
   Intros.
   Split with m.
   Split.
   Unfold lt.
   Apply le_n.
   Assumption.
Qed.


(* some decidable relations on nat *)

Lemma eqdec: (n,m:nat) n=m \/ ~n=m.
Proof.
   Induction n.
   Intro.
   Case m.
   Left.
   Reflexivity.
   Right.
   Discriminate.
   Intros.
   Case m.
   Right.
   Discriminate.
   Intro m0.
   Elim (H m0).
   Left.
   Rewrite H0.
   Reflexivity.
   Right.
   Intro.
   Apply H0.
   Inversion H1.
   Reflexivity.
Qed.

Lemma ledec: (n,m:nat) (le n m) \/ ~(le n m).
Proof.
   Intros. Elim (le_or_lt n m).
   Left. Assumption.
   Right. Apply lt_not_le. Assumption.
Qed.

Lemma ltdec: (n,m:nat) (lt n m) \/ ~(lt n m).
Proof.
   Unfold lt. Intros. Apply ledec.
Qed.

Lemma gedec: (n,m:nat) (ge n m) \/ ~(ge n m).
Proof.
   Unfold ge. Intros. Apply ledec.
Qed.

Lemma gtdec: (n,m:nat) (gt n m) \/ ~(gt n m).
Proof.
   Unfold gt. Intros. Apply ltdec.
Qed.

(* relations on Z *)

Lemma zeqdec: (x,y:Z) x=y\/~x=y.
Proof.
   Intros. Elim (dec_eq x y). Left. Assumption. Right. Assumption.
Qed.

(* the connectives preserve decidability *)

Lemma notdec: (P:Prop)(P\/~P)->(~P\/P).
Proof.
   Intros. Elim H.
   Right. Assumption.
   Left. Assumption.
Qed.

Lemma anddec: (P,Q:Prop)(P\/~P)->(Q\/~Q)->(P/\Q)\/~(P/\Q).
Proof.
   Intros. Elim H. Elim H0.
   Left. Split. Assumption. Assumption.
   Right. Intro. Apply H1. Elim H3. Intros. Assumption.
   Right. Intro. Apply H1. Elim H2. Intros. Assumption.
Qed.

Lemma ordec: (P,Q:Prop)(P\/~P)->(Q\/~Q)->(P\/Q)\/~(P\/Q).
Proof.
   Intros. Elim H.
   Left. Left. Assumption.
   Elim H0.
   Left. Right. Assumption.
   Right. Intro. Elim H3. Assumption. Assumption.
Qed.

Lemma impdec: (P,Q:Prop)(P\/~P)->(Q\/~Q)->(P->Q)\/~(P->Q).
Proof.
   Intros. Elim H.
   Elim H0.
   Left. Intros. Assumption.
   Right. Intro. Apply H1. Apply H3. Assumption.
   Left. Intros. Elim H1. Assumption.
Qed.

Lemma iffdec: (P,Q:Prop)(P\/~P)->(Q\/~Q)->(P<->Q)\/~(P<->Q).
Proof.
   Unfold iff. Intros.
   Apply anddec.
   Apply impdec. Assumption. Assumption.
   Apply impdec. Assumption. Assumption.
Qed.

(* bounded quantifiers preserve decidability *)

Theorem alldec:
   (P:nat->Prop)(N:nat)
      ((n:nat)(P n)\/~(P n)) ->
         ((x:nat)(lt x N)->(P x)) \/ ~((x:nat)(lt x N)->(P x)).
Proof.
   Intro P. Induction N.
   Left. Intros. Elim (lt_n_O x). Assumption.
   Intros M IH decP.
   Elim IH. Elim (decP M).
   Left. Intros. Unfold lt in H1. Elim (le_lt_or_eq x M). Intros.
   Apply H0. Assumption.
   Intros. Rewrite H2. Assumption.
   Apply le_S_n. Assumption.
   Right. Intro. Apply H. Apply H1. Apply lt_n_Sn.
   Right. Intro. Apply H. Intros. Apply H0. Apply lt_S. Assumption.
   Assumption.
Qed.

Theorem exdec:
   (P:nat->Prop)(N:nat)
      ((n:nat)(P n)\/~(P n)) ->
         (EX x:nat | (lt x N) /\ (P x)) \/ ~(EX x:nat | (lt x N) /\ (P x)).
Proof.
   Intro P. Induction N.
   Intro decP.
   Right. Intro. Elim H. Intros. Elim H0. Intros. Elim (lt_n_O x). Assumption.
   Intros M IH decP.
   Elim IH. Left.
   Elim H. Intros. Split with x. Elim H0. Intros.
   Split.
   Apply lt_S. Assumption.
   Assumption.
   Intros.
   Elim (decP M).
   Left. Split with M. Split. Apply lt_n_Sn.
   Assumption.
   Right. Intro.
   Elim H1. Intros. Elim H2. Intros.
   Unfold lt in H3. Elim (le_lt_or_eq x M).
   Intro. Apply H. Split with x. Split. Assumption.
   Assumption.
   Intro. Apply H0. Rewrite <- H5. Assumption.
   Apply le_S_n. Assumption.
   Assumption.
Qed.

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

Theorem decDeMorgan:
   (N:nat)(P:nat->Prop)
      ((n:nat)(P n)\/~(P n)) ->
         (EX x:nat | (lt x N) /\ (P x)) <-> ~((x:nat)(lt x N) -> ~(P x)).
Proof.
   Split.
   Intro.
   Elim H0.
   Intros.
   Intro.
   Elim H1.
   Intros.
   Apply (H2 x H3 H4).
   Elim N. Intros. Elim H0. Intros. Elim (lt_n_O x). Assumption.
   Intros M IH. Intros.
   Elim (H M).
   Intros.
   Split with M.
   Split.
   Apply lt_n_Sn.
   Assumption.
   Intros.
   Cut ~((x:nat)(lt x M)->~(P x)).
   Intros.
   Elim IH.
   Intros.
   Split with x.
   Elim H3.
   Intros.
   Split.
   Apply lt_S.
   Assumption.
   Assumption.
   Assumption.
   Intro.
   Apply H0.
   Intros.
   Elim (le_lt_or_eq x M).
   Intros.
   Apply H2.
   Assumption.
   Intros.
   Rewrite H4.
   Assumption.
   Unfold lt in H3.
   Apply le_S_n.
   Assumption.
Qed.


(* Some nice boolean stuff... *)

Definition istrue := [b:bool]if b then True else False.

Lemma beq_nat_ok: (n,m:nat) n=m <-> (istrue (beq_nat n m)).
Proof.
   Induction n.
   Intro m. Case m. Simpl. Tauto. Simpl. Split. Discriminate. Tauto.
   Intros.
   Case m. Simpl. Split. Discriminate. Tauto.
   Intros. Elim (H n1).
   Split.
   Intros. Simpl. Apply H0. Injection H2. Tauto.
   Simpl. Intros. Rewrite (H1 H2). Reflexivity.
Qed.

Lemma beq_nat_eq: (n,m:nat)n=m<->(beq_nat n m)=true.
Proof.
   Induction n.
   Intro. Case m.
   Simpl. Split. Reflexivity. Reflexivity.
   Simpl. Split. Intro. Discriminate. Intro. Discriminate.
   Intros n1 IH. Intro m. Case m.
   Simpl. Split. Intro. Discriminate. Intro. Discriminate.
   Intro m1. Intros. Simpl.
   Elim (IH m1). Split.
   Intro. Injection H1. Assumption.
   Intros. Rewrite H0. Reflexivity. Assumption.
Qed.

Lemma beq_nat_neq: (n,m:nat)~n=m<->(beq_nat n m)=false.
Proof.
   Induction n.
   Intro. Case m. Simpl. Split.
   Intro. Elim H. Reflexivity. Intro. Discriminate.
   Intro m1. Simpl. Split. Reflexivity. Intro. Discriminate.
   Intros n1 IH. Intro m. Case m.
   Simpl. Split. Reflexivity. Intro. Discriminate.
   Intro m1. Simpl.
   Elim (IH m1). Split.
   Intro. Apply H. Intro. Elim H1. Rewrite H2. Reflexivity.
   Intro. Intro. Elim H0. Assumption. Injection H2. Intro. Assumption.
Qed.

Lemma zeq_bool_eq: (x,y:Z)x=y<->(Zeq_bool x y)=true.
Proof.
   Intros. Elim (Zcompare_EGAL x y). Intros. Unfold Zeq_bool. Split.

   (* -> *)
   Intro. Rewrite H0.
   Reflexivity. Assumption.

   (* <- *)
   Intro. Apply H. Generalize H1.
   Elim `x ?= y`.
   Intro. Reflexivity.
   Intro. Discriminate H2.
   Intro. Discriminate H2.
Qed.

Lemma zeq_bool_neq: (x,y:Z)~x=y<->(Zeq_bool x y)=false.
Proof.
   Intros. Elim (Zcompare_EGAL x y). Intros. Unfold Zeq_bool. Split.

   (* -> *)
   Generalize H0. Generalize H. Elim `x ?= y`.
   Intros. Elim H3. Apply H1. Reflexivity.
   Intros. Reflexivity.
   Intros. Reflexivity.

   (* <- *)
   Intros. Generalize H1. Generalize H0. Elim `x ?= y`.
   Intros. Discriminate H3.
   Intros. Intro. Cut INFERIEUR=EGAL. Discriminate.
   Apply H2. Assumption.
   Intros. Intro. Cut SUPERIEUR=EGAL. Discriminate.
   Apply H2. Assumption.
Qed.