Set Implicit Arguments.
Require Import Omega.
Require Import Coq.Init.Nat.
Require Export FinTypes.External.

Collection of Basic Definition and Lemmas

Rewriting with equalities on numbers provable by omega

Ltac rewrite_eq Eq := let E := fresh in assert (Eq) as E by omega; rewrite E; clear E.
Ltac rewrite_eq_in Eq T := let E := fresh in assert (Eq) as E by omega; rewrite E in T; clear E.
Tactic Notation "rewrite_eq" constr(Eq) := (rewrite_eq Eq).
Tactic Notation "rewrite_eq" constr(Eq) "in" hyp(T) := (rewrite_eq_in Eq T).

Ltac oauto := try (omega); try (cbn;omega); auto.
Ltac comega := cbn; omega.

Tactics for Simplification of Decisions

Lemma decision_true (X:Type) (P:Prop) (decP:dec P) (x y : X) (p:P): (if (decision P) then x else y ) = x.
Proof.
  decide P.
  - reflexivity.
  - exfalso. auto.
Qed.

Lemma decision_false (X:Type) (P:Prop) (decP:dec P) (x y : X) (p:~P): (if (decision P) then x else y ) = y.
Proof.
  decide P.
  - exfalso. auto.
  - reflexivity.
Qed.

Ltac trivial_decision := repeat ( try (rewrite decision_true in * by auto); try (rewrite decision_false in * by auto); try (rewrite decision_true in * by comega); try(rewrite decision_false in * by comega)).

Definition logic_dec (p : Prop) := p \/ ~ p.
Existing Class logic_dec.

Utility Lemmas regarding numbers

Lemma complete_induction (P : nat -> Prop) : P 0 -> (forall n, (forall m, m <= n -> P m ) -> (P (S n))) -> forall n, P n.
Proof.
  intros p0 pS.
  enough (forall n, forall m, m <= n -> P m).
  - intros n. apply (H n n). omega.
  - induction n; intros m L.
    + now rewrite_eq (m = 0).
    + decide (m = S n) as [D|D].
      * rewrite D. apply pS. apply IHn.
      * apply IHn. omega.
Qed.

Lemma max_le_left n m k: k <= n -> k <= max n m.
Proof.
  intros L.
  pose (p := (Nat.le_max_l n m)).
  omega.
Qed.

Lemma max_le_right n m k : k <= m -> k <= max n m.
Proof.
  intros L. rewrite Nat.max_comm. now apply max_le_left.
Qed.

Lemma max_le k m n : k <= max m n -> k <= m \/ k <= n.
Proof.
destruct (Nat.max_dec m n) as [D|D]; rewrite D; tauto.
Qed.

Lemma mul_ge_0 n m : n > 0 -> m > 0 -> n * m > 0.
Proof.
  intros L1 L2. apply Nat.lt_0_mul'; split; omega.
Qed.

Lemma mul_ge_0_reverse n m : n * m > 0 -> n > 0 /\ m > 0.
Proof.
  intros L. apply Nat.lt_0_mul'. omega.
Qed.

Lemma mul_geq_left n m k : n <= m -> k > 0 -> n <= m * k.
Proof.
  intros L G.
  rewrite_eq (n = n * 1). apply Nat.mul_le_mono; omega.
Qed.

Lemma mul_div n m : n > 0 -> m > 0 -> n * m / m = n.
Proof.
  Import Nat.
  intros L1 L2. rewrite <-(mul_1_l m). rewrite (mul_assoc n). rewrite div_mul_cancel_r by omega.
    rewrite mul_1_r. now rewrite div_1_r.
Qed.

Lemma S_z_minus_1 n : n > 0 -> S(n - 1) = n.
Proof.
  intros L. omega.
Qed.

Lemma pow_ge_zero' i k: k > 0 -> Nat.pow k i > 0.
Proof.
  intros L. induction i; cbn.
  - omega.
  - apply mul_ge_0; omega.
Qed.

Lemma pow_ge_zero i : Nat.pow 2 i > 0.
Proof.
  induction i; cbn; omega.
Qed.

Languages

Language Speak for predicates, makes some things sound more naturally

Section Languages.

  Variable (X:Type).

  Definition Language := X -> Prop.

  Definition empty_language : Language := fun _=> False.
  Definition universal_language : Language := fun _ => True.

  Definition language_inclusion (P Q :Language) :=
       forall w, P w -> Q w.

  Definition language_eq (P Q: Language) := (forall w, P w <-> Q w).

  Definition language_union (P Q: Language) : Language:= fun w => P w \/ Q w.

  Definition language_intersection(P Q: Language): Language:= fun w => P w /\ Q w.

  Definition language_complement (P : Language) :Language := fun w => ~ (P w ).

  Definition language_difference (P Q : Language) : Language := fun w => P w /\ ~ Q w.

End Languages.

Arguments empty_language {X} _.
Arguments universal_language {X} _.

Notation "x <$= y" := (language_inclusion x y) (at level 70).
Notation "x =$= y" := (language_eq x y) (at level 70).
Notation "x \$/ y" := (language_union x y) (at level 69).
Notation "x /$\ y" := (language_intersection x y) (at level 69).
Notation "x ^$~ " := (language_complement x) (at level 68).
Notation "{}" := (empty_language) (at level 20).

Hint Unfold language_intersection.
Hint Unfold language_union.
Hint Unfold language_complement.
Hint Unfold language_eq.
Hint Unfold language_inclusion.
Hint Unfold empty_language.
Hint Unfold universal_language.

Section LanguageLemmata.
  Variable X:Type.
  Variables L L_1 L_2 : Language X.

  Lemma language_empty_iff : L =$= {} <-> (forall w, ~ (L w ) ).
  Proof. firstorder. Qed.

  Lemma language_universal_iff : L =$= universal_language <-> (forall w, L w ).
  Proof. firstorder. Qed.

  Lemma language_eq_iff : L_1 =$= L_2 <-> L_1 <$= L_2 /\ L_2 <$= L_1.
  Proof. firstorder. Qed.

  Lemma language_eq_symmetric: L_1 =$= L_2 <-> L_2 =$= L_1.
  Proof. firstorder. Qed.

  Lemma language_union_comm: L_1 \$/ L_2 =$= L_2 \$/ L_1.
  Proof. firstorder. Qed.

  Lemma language_intersection_comm: L_1 /$\ L_2 =$= L_2 /$\ L_1.
  Proof. firstorder. Qed.

End LanguageLemmata.

Instance language_eq_equivalence X: Equivalence (@language_eq X).
Proof.
  constructor; firstorder.
Qed.

Instance language_eq_mem X w: Proper (@language_eq X ==> iff) (fun L => L w).
Proof.
  firstorder.
Qed.

Instance language_union_proper X: Proper (@language_eq X ==> @language_eq X ==> @language_eq X) (@language_union X).
Proof. firstorder. Qed.
Instance language_intersection_proper X: Proper (@language_eq X ==> @language_eq X ==> @language_eq X) (@language_intersection X).
Proof. firstorder. Qed.
Instance language_difference_proper X: Proper (@language_eq X ==> @language_eq X ==> @language_eq X) (@language_difference X).
Proof. firstorder. Qed.
Instance language_complement_proper X: Proper (@language_eq X ==> @language_eq X) (@language_complement X).
Proof. firstorder. Qed.

Constructive Choice for nat

Taken from ICL and modified to have a choice proving that it takes the smallest witness

Inductive safe (p : nat -> Prop) (n : nat) : Prop :=
| safeB : p n -> safe p n
| safeS : safe p (S n) -> ~ p n -> safe p n.

Section First.
  Variable p : nat -> Prop.
  Variable p_dec : forall n, dec (p n).

Lemma safe_dclosed k n : k <= n -> safe p n -> safe p k.
Proof.
  intros A B. induction A as [|n A].
  - exact B.
  - decide (p n); apply IHA.
    + now left.
    + right; auto.
Qed.

  Fixpoint first (n : nat) (A : safe p n) : {x | p x /\ forall j, n <= j < x -> ~ p j }.
  Proof.
    decide (p n).
    - exists n. split; auto. intros j L. exfalso. omega.
    - enough {x : nat | p x /\ (forall j : nat, S n <= j < x -> ~ p j )} as [x [P Q]].
      + exists x. split; auto. intros j B. decide (j = n).
        * now subst n.
        * apply Q. omega.
      + apply first. destruct A; tauto.
  Qed.

  Lemma cc_nat_first : (exists x, p x ) -> {x | p x /\ forall j, 0 <= j < x -> ~ p j }.
  Proof.
    intros A. apply first with (n:=0).
    destruct A as [n A].
    apply safe_dclosed with (n:=n). omega. left. exact A.
  Qed.

  Lemma cc_nat : (exists x, p x ) -> {x | p x}.
  Proof.
    intros A. destruct (cc_nat_first A) as [x [P _]]. now exists x.
  Qed.

End First.

Lemma pair_proj1 (X Y: Type) (x:X) (y:Y): fst (x , y ) = x.
Proof. now intros. Qed.
Lemma pair_proj2 (X Y: Type) (x:X) (y:Y): snd (x , y ) = y.
Proof. now intros. Qed.