Library ninfty
Require Import prelude.
Require Import hlemmas.
Require Import FunctionalExtensionality.
Require Import Bool.
Require Import Omega.
Definition cantor := nat -> bool.
Definition decreasing (f : nat -> bool) : Type :=
forall n, (negb (f (S n))) || f n = true.
Definition N_infty := Σ s : cantor, decreasing s.
Notation "'ℕ∞'" := N_infty.
Lemma N_infty_hset : hset ℕ∞.
apply Sigma_hset.
- apply forall_hset; intros; apply bool_hset.
- intros; apply forall_hset; intros; apply hprop_hset, bool_hset.
Qed.
Definition succ_infty (p : ℕ∞) : ℕ∞.
exists (fun n => match n with 0 => true | S k => π₁ p k end).
destruct p as [s p];
intros [|]; auto. simpl; destruct (negb (s 0)); reflexivity.
Defined.
Definition zero_infty : ℕ∞.
exists (fun _ => false); intros ?; auto.
Defined.
Fixpoint N_infty_of_nat (n : nat) : ℕ∞ :=
match n with
0 => zero_infty
| S n => succ_infty (N_infty_of_nat n)
end.
Lemma pred_infty (p : ℕ∞) : ℕ∞.
exists (fun n => π₁ p (S n)).
destruct p as [? d]; intros ?;apply d.
Defined.
Lemma N_infty_eq : forall p q : ℕ∞, π₁ p = π₁ q -> p = q.
intros; apply Sigma_eq_uncurried.
exists H.
apply forall_hprop; intro; apply bool_hset.
Qed.
Lemma pred_succ_eq (p : ℕ∞) : pred_infty (succ_infty p) = p.
destruct p.
apply N_infty_eq; reflexivity.
Qed.
Lemma injective_succ_infty : injective succ_infty.
intros ? ? ?.
apply (f_equal pred_infty) in H.
do 2 rewrite pred_succ_eq in H; assumption.
Qed.
Lemma noconf_infty : forall x, ¬ succ_infty x = zero_infty.
intros.
apply (f_equal (fun z => π₁ z 0)) in H.
simpl in H.
inversion H.
Qed.
Definition ω : ℕ∞.
exists (fun _ => true); intros ?; reflexivity.
Defined.
Lemma trueleft : forall u : ℕ∞, forall n, π₁ u n = true -> forall k, k <= n -> π₁ u k = true.
intros [? ?]; simpl; intros.
induction H0; auto.
apply IHle; specialize (d m).
rewrite H in d; apply d.
Qed.
Lemma falseright : forall u : ℕ∞, forall n, π₁ u n = false -> forall k, n <= k -> π₁ u k = false.
intros [? ?]; simpl; intros.
induction H0; auto.
specialize (d m); rewrite IHle in d; destruct (x (S m)); simpl in *; congruence.
Qed.
Lemma N_infty_of_nat_eq : forall k n, π₁ (N_infty_of_nat n) k = Nat.ltb k n.
induction k; induction n; simpl in *; auto.
rewrite IHk; auto.
Qed.
Lemma firstzeronat : forall u : ℕ∞, forall n, π₁ u n = false -> (forall k, k < n -> π₁ u k = true) -> u = N_infty_of_nat n.
intros [? ?]; simpl; intros; apply N_infty_eq; extensionality z; simpl.
rewrite N_infty_of_nat_eq.
specialize (falseright (existT _ x d) _ H z); intros.
specialize (H0 z).
case_eq (z <? n); intros.
+ apply Nat.ltb_lt in H2; auto.
+ apply Nat.ltb_ge in H2; auto.
Qed.
Lemma minimizationdec : forall p : nat -> bool, forall n, p n = true -> Σ k : nat, (p k = true) × (forall m, m < k -> p m = false).
intros p n; revert p; induction n.
- intros; exists 0; split; auto.
intros; exfalso; omega.
- intros.
case_eq (p 0).
+ intros; exists 0; split; auto; intros; exfalso; omega.
+ intros; destruct (IHn (fun n => p (S n)) H) as [w [? ?]]; exists (S w); split; [assumption|].
intros [|?] ?; auto.
apply e0; omega.
Qed.
Lemma zeronat : forall u : ℕ∞, forall n, π₁ u n = false -> Σ k : nat, u = N_infty_of_nat k.
intros.
assert (negb (π₁ u n) = true) by (destruct (π₁ u n); auto).
destruct (minimizationdec (fun k => negb (π₁ u k)) _ H0) as [? [? ?]].
exists x; apply firstzeronat.
- destruct (π₁ u x); simpl in *; congruence.
- intros k p; specialize (e0 k p).
destruct (π₁ u k); simpl in *; congruence.
Qed.
Lemma notnatω : forall u, (forall n, u <> N_infty_of_nat n) -> u = ω.
intros; apply N_infty_eq.
extensionality k; destruct u as [s ?]; simpl in *.
case_eq (s k); auto.
intro; exfalso.
destruct (zeronat (existT _ s d) _ H0).
eapply H; eassumption.
Qed.
Lemma dense : forall p (b : bool), p ω = b -> (forall n, p (N_infty_of_nat n) = b) -> forall u, p u = b.
intros; destruct b.
+ case_eq (p u); auto; intros; exfalso.
assert (u <> ω) by
(intros; subst; congruence).
apply H2, notnatω.
intros ? ?; subst.
specialize (H0 n).
congruence.
+ case_eq (p u); auto; intros; exfalso.
assert (u <> ω) by
(intros; subst; congruence).
apply H2, notnatω.
intros ? ?; subst.
specialize (H0 n).
congruence.
Qed.
Fixpoint ε_N_infty1 (f : ℕ∞ -> bool) (n : nat) : bool :=
match n with
0 => negb (f zero_infty)
| S k => ε_N_infty1 f k && negb (f (N_infty_of_nat (S k)))
end.
Lemma ε_N_infty1_decr : forall f, decreasing (ε_N_infty1 f).
intros ? ?.
induction n; simpl in *.
- destruct (f zero_infty); simpl; try reflexivity.
apply orb_true_r.
- destruct (ε_N_infty1 f n), (f (N_infty_of_nat n)), (f (succ_infty (N_infty_of_nat n))), (f (succ_infty (succ_infty (N_infty_of_nat n))));
simpl in *; congruence.
Qed.
Definition ε_N_infty f : ℕ∞ := existT _ (ε_N_infty1 f) (ε_N_infty1_decr f).
Lemma ε_N_infty_zero_true f : f zero_infty = true -> ε_N_infty f = N_infty_of_nat 0.
intros; apply firstzeronat.
+ simpl.
rewrite H; reflexivity.
+ intros; omega.
Qed.
Lemma ε_N_infty_nat1_prod : forall f x, (forall y, y <= x -> f (N_infty_of_nat y) = false) -> ε_N_infty1 f x = true.
induction x.
+ intros.
specialize (H 0); simpl in *; rewrite H; reflexivity.
+ intros.
simpl.
rewrite IHx; auto.
specialize (H (S x)); simpl in *; rewrite H; auto.
Qed.
Lemma ε_N_infty_nat_min : forall x f, f (N_infty_of_nat x) = true -> (forall y, y < x -> f (N_infty_of_nat y) = false) -> ε_N_infty f = N_infty_of_nat x.
intros.
apply firstzeronat.
+ destruct x; simpl in *; rewrite H; [reflexivity|].
apply andb_false_r.
+ simpl.
intros; apply ε_N_infty_nat1_prod.
intros; apply H0; omega.
Qed.
Lemma ε_N_infty_spec : forall f, f ω = false -> f (ε_N_infty f) = false -> (forall x, f x = false).
intros.
assert (forall x, f (N_infty_of_nat x) = false).
{
intros z; case_eq (f (N_infty_of_nat z)); auto; intros.
apply (minimizationdec (fun z => f (N_infty_of_nat z))) in H1.
destruct H1 as [? [? ?]].
exfalso.
assert (ε_N_infty f = N_infty_of_nat x0) by
(apply ε_N_infty_nat_min; auto).
congruence.
}
apply dense; auto.
Qed.
Lemma N_infty_omniscient : omniscient N_infty.
intros ?.
case_eq (f ω); intros; eauto.
case_eq (f (ε_N_infty f)); eauto.
intros; right; apply ε_N_infty_spec; assumption.
Qed.
Require Import hlemmas.
Require Import FunctionalExtensionality.
Require Import Bool.
Require Import Omega.
Definition cantor := nat -> bool.
Definition decreasing (f : nat -> bool) : Type :=
forall n, (negb (f (S n))) || f n = true.
Definition N_infty := Σ s : cantor, decreasing s.
Notation "'ℕ∞'" := N_infty.
Lemma N_infty_hset : hset ℕ∞.
apply Sigma_hset.
- apply forall_hset; intros; apply bool_hset.
- intros; apply forall_hset; intros; apply hprop_hset, bool_hset.
Qed.
Definition succ_infty (p : ℕ∞) : ℕ∞.
exists (fun n => match n with 0 => true | S k => π₁ p k end).
destruct p as [s p];
intros [|]; auto. simpl; destruct (negb (s 0)); reflexivity.
Defined.
Definition zero_infty : ℕ∞.
exists (fun _ => false); intros ?; auto.
Defined.
Fixpoint N_infty_of_nat (n : nat) : ℕ∞ :=
match n with
0 => zero_infty
| S n => succ_infty (N_infty_of_nat n)
end.
Lemma pred_infty (p : ℕ∞) : ℕ∞.
exists (fun n => π₁ p (S n)).
destruct p as [? d]; intros ?;apply d.
Defined.
Lemma N_infty_eq : forall p q : ℕ∞, π₁ p = π₁ q -> p = q.
intros; apply Sigma_eq_uncurried.
exists H.
apply forall_hprop; intro; apply bool_hset.
Qed.
Lemma pred_succ_eq (p : ℕ∞) : pred_infty (succ_infty p) = p.
destruct p.
apply N_infty_eq; reflexivity.
Qed.
Lemma injective_succ_infty : injective succ_infty.
intros ? ? ?.
apply (f_equal pred_infty) in H.
do 2 rewrite pred_succ_eq in H; assumption.
Qed.
Lemma noconf_infty : forall x, ¬ succ_infty x = zero_infty.
intros.
apply (f_equal (fun z => π₁ z 0)) in H.
simpl in H.
inversion H.
Qed.
Definition ω : ℕ∞.
exists (fun _ => true); intros ?; reflexivity.
Defined.
Lemma trueleft : forall u : ℕ∞, forall n, π₁ u n = true -> forall k, k <= n -> π₁ u k = true.
intros [? ?]; simpl; intros.
induction H0; auto.
apply IHle; specialize (d m).
rewrite H in d; apply d.
Qed.
Lemma falseright : forall u : ℕ∞, forall n, π₁ u n = false -> forall k, n <= k -> π₁ u k = false.
intros [? ?]; simpl; intros.
induction H0; auto.
specialize (d m); rewrite IHle in d; destruct (x (S m)); simpl in *; congruence.
Qed.
Lemma N_infty_of_nat_eq : forall k n, π₁ (N_infty_of_nat n) k = Nat.ltb k n.
induction k; induction n; simpl in *; auto.
rewrite IHk; auto.
Qed.
Lemma firstzeronat : forall u : ℕ∞, forall n, π₁ u n = false -> (forall k, k < n -> π₁ u k = true) -> u = N_infty_of_nat n.
intros [? ?]; simpl; intros; apply N_infty_eq; extensionality z; simpl.
rewrite N_infty_of_nat_eq.
specialize (falseright (existT _ x d) _ H z); intros.
specialize (H0 z).
case_eq (z <? n); intros.
+ apply Nat.ltb_lt in H2; auto.
+ apply Nat.ltb_ge in H2; auto.
Qed.
Lemma minimizationdec : forall p : nat -> bool, forall n, p n = true -> Σ k : nat, (p k = true) × (forall m, m < k -> p m = false).
intros p n; revert p; induction n.
- intros; exists 0; split; auto.
intros; exfalso; omega.
- intros.
case_eq (p 0).
+ intros; exists 0; split; auto; intros; exfalso; omega.
+ intros; destruct (IHn (fun n => p (S n)) H) as [w [? ?]]; exists (S w); split; [assumption|].
intros [|?] ?; auto.
apply e0; omega.
Qed.
Lemma zeronat : forall u : ℕ∞, forall n, π₁ u n = false -> Σ k : nat, u = N_infty_of_nat k.
intros.
assert (negb (π₁ u n) = true) by (destruct (π₁ u n); auto).
destruct (minimizationdec (fun k => negb (π₁ u k)) _ H0) as [? [? ?]].
exists x; apply firstzeronat.
- destruct (π₁ u x); simpl in *; congruence.
- intros k p; specialize (e0 k p).
destruct (π₁ u k); simpl in *; congruence.
Qed.
Lemma notnatω : forall u, (forall n, u <> N_infty_of_nat n) -> u = ω.
intros; apply N_infty_eq.
extensionality k; destruct u as [s ?]; simpl in *.
case_eq (s k); auto.
intro; exfalso.
destruct (zeronat (existT _ s d) _ H0).
eapply H; eassumption.
Qed.
Lemma dense : forall p (b : bool), p ω = b -> (forall n, p (N_infty_of_nat n) = b) -> forall u, p u = b.
intros; destruct b.
+ case_eq (p u); auto; intros; exfalso.
assert (u <> ω) by
(intros; subst; congruence).
apply H2, notnatω.
intros ? ?; subst.
specialize (H0 n).
congruence.
+ case_eq (p u); auto; intros; exfalso.
assert (u <> ω) by
(intros; subst; congruence).
apply H2, notnatω.
intros ? ?; subst.
specialize (H0 n).
congruence.
Qed.
Fixpoint ε_N_infty1 (f : ℕ∞ -> bool) (n : nat) : bool :=
match n with
0 => negb (f zero_infty)
| S k => ε_N_infty1 f k && negb (f (N_infty_of_nat (S k)))
end.
Lemma ε_N_infty1_decr : forall f, decreasing (ε_N_infty1 f).
intros ? ?.
induction n; simpl in *.
- destruct (f zero_infty); simpl; try reflexivity.
apply orb_true_r.
- destruct (ε_N_infty1 f n), (f (N_infty_of_nat n)), (f (succ_infty (N_infty_of_nat n))), (f (succ_infty (succ_infty (N_infty_of_nat n))));
simpl in *; congruence.
Qed.
Definition ε_N_infty f : ℕ∞ := existT _ (ε_N_infty1 f) (ε_N_infty1_decr f).
Lemma ε_N_infty_zero_true f : f zero_infty = true -> ε_N_infty f = N_infty_of_nat 0.
intros; apply firstzeronat.
+ simpl.
rewrite H; reflexivity.
+ intros; omega.
Qed.
Lemma ε_N_infty_nat1_prod : forall f x, (forall y, y <= x -> f (N_infty_of_nat y) = false) -> ε_N_infty1 f x = true.
induction x.
+ intros.
specialize (H 0); simpl in *; rewrite H; reflexivity.
+ intros.
simpl.
rewrite IHx; auto.
specialize (H (S x)); simpl in *; rewrite H; auto.
Qed.
Lemma ε_N_infty_nat_min : forall x f, f (N_infty_of_nat x) = true -> (forall y, y < x -> f (N_infty_of_nat y) = false) -> ε_N_infty f = N_infty_of_nat x.
intros.
apply firstzeronat.
+ destruct x; simpl in *; rewrite H; [reflexivity|].
apply andb_false_r.
+ simpl.
intros; apply ε_N_infty_nat1_prod.
intros; apply H0; omega.
Qed.
Lemma ε_N_infty_spec : forall f, f ω = false -> f (ε_N_infty f) = false -> (forall x, f x = false).
intros.
assert (forall x, f (N_infty_of_nat x) = false).
{
intros z; case_eq (f (N_infty_of_nat z)); auto; intros.
apply (minimizationdec (fun z => f (N_infty_of_nat z))) in H1.
destruct H1 as [? [? ?]].
exfalso.
assert (ε_N_infty f = N_infty_of_nat x0) by
(apply ε_N_infty_nat_min; auto).
congruence.
}
apply dense; auto.
Qed.
Lemma N_infty_omniscient : omniscient N_infty.
intros ?.
case_eq (f ω); intros; eauto.
case_eq (f (ε_N_infty f)); eauto.
intros; right; apply ε_N_infty_spec; assumption.
Qed.