andrej.v

From Coq.Unicode Require Import Utf8.
From Coq.Program Require Import Tactics.

Record Tomega := {
  yes : nat → Prop;
  no : nat → Prop;
  disjoint : ∀ n, ¬ (yes n ∧ no n)
}.

Definition leq (x y : Tomega) :=
  (∀ n, yes x n → yes y n) ∧
  (∀ n, no x n → no y n).

Infix "≤" := leq.

Definition maximal (x : Tomega) :=
  ∀ y, x ≤ y → y ≤ x.

Definition complement_closed (x : Tomega) :=
  (∀ n, ¬ yes x n → no x n) ∧
  (∀ n, ¬ no x n → yes x n).

Lemma yes_not_no x n : yes x n → ¬ no x n.
Proof. pose proof (disjoint x n); firstorder. Qed.

Lemma no_not_yes x n : no x n → ¬ yes x n.
Proof. pose proof (disjoint x n); firstorder. Qed.

Program Definition complete_yes (x : Tomega) : Tomega :=
{| yes n := ¬ no x n;
   no n := no x n;
|}.
Next Obligation.
Proof. tauto. Qed.

Lemma leq_complete_yes x : x ≤ complete_yes x.
Proof. split; intros ?; simpl; auto using yes_not_no. Qed.

Program Definition complete_no (x : Tomega) : Tomega :=
{| yes n := yes x n;
   no n := ¬ yes x n;
|}.
Next Obligation.
Proof. tauto. Qed.

Lemma leq_complete_no x : x ≤ complete_no x.
Proof. split; intros ?; simpl; auto using no_not_yes. Qed.

Lemma complement_closed_maximal x :
  maximal x ↔ complement_closed x.
Proof.
  split.
  - intros Hmx; split; intros n Hn.
    + pose proof (leq_complete_no x) as [? ?]%Hmx; firstorder.
    + pose proof (leq_complete_yes x) as [? ?]%Hmx; firstorder.
  - intros Hcc y Hy; split; intros n Hn.
    + apply Hcc; intros Hn'.
      apply Hy in Hn'.
      apply (disjoint y n); tauto.
    + apply Hcc; intros Hn'.
      apply Hy in Hn'.
      apply (disjoint y n); tauto.
Qed.

Definition total (x : Tomega) := ∀ n, yes x n ∨ no x n.

Definition both_dec (x : Tomega) :=
  (∀ n, yes x n ∨ ¬ yes x n) ∧
  (∀ n, no x n ∨ ¬ no x n).

Lemma maximal_total_both_dec x :
  maximal x → (total x ↔ both_dec x).
Proof.
  intros Hx%complement_closed_maximal.
  split.
  - intros Ht; split; intros n.
    + destruct (Ht n); auto using no_not_yes.
    + destruct (Ht n); auto using yes_not_no.
  - intros [Hby Hbn] n.
    destruct (Hby n) as [|?%Hx]; auto.
Qed.