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.