The Low Wall Function

(* ##################################### *)

Definition inf_exists (P: Prop) := n, m, n m P m.
  Notation "'∞∃' x .. y , p" :=
    (inf_exists (λ x, .. (inf_exists (λ y, p)) ..))
        (at level 200, x binder, right associativity,
        format "'[' '∞∃' '/ ' x .. y , '/ ' p ']'")
    : type_scope.

  Notation "f ↓" := (f = Some ()) (at level 30).

  Global Instance dec_le: m n, dec (m n).
  Proof. intros n m; destruct (le_gt_dec n m); [by left|right; ]. Qed.

Section Requirements_Lowness_Correctness.

  Variable P: Prop.
  Variable f: bool.
  Hypothesis S_P: stable_semi_decider P f.

  Definition Φ_ := (Φ_ f).

  Fact Φ_spec e x: Ξ e (char_rel P) x ∞∀ n, Φ_ e x n .
  Proof. intro H. unfold Φ_. apply (Φ_spec S_P H). Qed.

  Definition Ω e n := Φ_ e e n.

  Section classic_logic.

Requirements


  Hypothesis N_requirements: e, (∞∃ n, Ω e n ) Ξ e (char_rel P) e.
  Definition limit_decider e n: bool := Dec (Ω e n ).

  Section with_LEM_2.

  Hypothesis LEM_Σ_2:
   (P: Prop), ( n m, dec (P n m)) ( n, m, P n m) ¬ ( n, m, P n m).

  Hypothesis LEM_Π_2:
   (P: Prop), ( n m, dec (P n m)) ( n, m, P n m) ¬ ( n, m, P n m).

  Lemma limit_case e: (∞∀ n, Ω e n ) (∞∀ n, ¬ Ω e n ).
  Proof.
    assert ( m n, dec (m n ¬ Ω e n )) as H by eauto.
    destruct (LEM_Σ_2 H); first by right.
    left. apply Φ_spec, N_requirements. intros i.
    assert ( n, dec (n i Ω e n )) as H'' by eauto.
    destruct (@LEM_Σ_2 (λ n _, i n Ω e n ) ) as [[w Hw]|]; first eauto.
    exists w; apply Hw; exact 42.
    assert ( n, i n Ω e n ).
    { intros m Hm HM. eapply . exists m; eauto. }
    exfalso. eapply . by exists i.
  Qed.


  Lemma Jump_limit : limit_computable (P´).
  Proof.
    exists limit_decider; split; intros.
    - unfold J. split.
      intros [w Hw]%Φ_spec; exists w; intros??.
      apply Dec_auto. by eapply Hw.
      intros [N HN]. eapply N_requirements.
      intros m. exists (S N + m); split; first .
      eapply Dec_true. eapply HN. .
    - unfold J. split; intros H.
      destruct (limit_case x) as [[k Hk]|].
      enough (Ξ x (char_rel P) x) by easy.
      eapply N_requirements. intros m. exists (S k + m).
      split; first . eapply Hk. .
      destruct as [w Hw]. exists w.
      intros. specialize (Hw n ). unfold limit_decider.
      destruct (Dec _); eauto.
      destruct H as [w Hw].
      intros [k Hneg]%Φ_spec.
      set (N := S (max w k)).
      assert (Ω x N ). { eapply Hneg. . }
      enough (¬ Ω x N ) by eauto.
      eapply Dec_false. eapply Hw. .
  Qed.

  End with_LEM_2.

  Section with_LEM_1.

  Hypothesis convergent: e, (∞∀ n, Ω e n ) (∞∀ n, ¬ Ω e n ).

  Lemma Jump_limit_1 : limit_computable (P´).
  Proof.
    exists limit_decider; split; intros.
    - unfold J. split.
      intros [w Hw]%Φ_spec; exists w; intros??.
      apply Dec_auto. by eapply Hw.
      intros [N HN]. eapply N_requirements.
      intros m. exists (S N + m); split; first .
      eapply Dec_true. eapply HN. .
    - unfold J. split; intros H.
      destruct (convergent x) as [[k Hk]|].
      enough (Ξ x (char_rel P) x) by easy.
      eapply N_requirements. intros m. exists (S k + m).
      split; first . eapply Hk. .
      destruct as [w Hw]. exists w.
      intros. specialize (Hw n ). unfold limit_decider.
      destruct (Dec _); eauto.
      destruct H as [w Hw].
      intros [k Hneg]%Φ_spec.
      set (N := S (max w k)).
      assert (Ω x N ). { eapply Hneg. . }
      enough (¬ Ω x N ) by eauto.
      eapply Dec_false. eapply Hw. .
  Qed.

  End with_LEM_1.

  End classic_logic.
(* 
  Section intuitionistic_logic.
  Hypothesis N_requirements: ∀ e, (∞∃ n, Ω e n ↓) → ¬¬ Ξ e (char_rel P) e.

  Lemma N_requirements': ∀ e, ¬¬ ((∞∃ n, Ω e n ↓) → Ξ e (char_rel P) e).
  Proof. firstorder. Qed.

  Fact dn_or (R Q: Prop): (¬¬ R ∨ ¬¬ Q) → ¬¬ (R ∨ Q).
  Proof. firstorder. Qed.
  Lemma not_not_limit_case e: ~ ~ ((∞∀ n, Ω e n ↓) ∨ (∞∀ n, ¬ Ω e n ↓)).
  Proof.
    ccase (∃ n, ∀ m, n ≤ m → ¬ Ω e m ↓) as |.
    apply dn_or. { right. eauto. }
    ccase (∀ i, ∃ n, i ≤ n ∧ Ω e n ↓) as |.
    intros H_. apply (@N_requirements' e).
    intros N_requirements'.
    apply H_. left. apply Φ_spec, N_requirements'. intros i.
    { destruct (H2 i) as w Hw. exists w. apply Hw.  }
    exfalso. clear P S_P N_requirements.
    apply H2. intros i.
  Admitted.
  
    Definition not_not_limit_computable {X} (P: X -> Prop) :=
      exists f: X -> nat -> bool, 
        forall x, ~~
        ((P x <-> exists N, forall n, n >= N -> f x n = true) /\
          (~ P x <-> exists N, forall n, n >= N -> f x n = false)).

    Fact dn_and (R Q: Prop): (¬¬ R ∧ ¬¬ Q) → ¬¬ (R ∧ Q).
    Proof. firstorder. Qed.

    Lemma not_not_Jump_limit : not_not_limit_computable (P´).
    Proof.
      exists limit_decider; intro x.
      apply dn_and.   
      split; intros.
      - unfold J. intros H_.
        eapply (@N_requirements' x). intros N_requirements'.
        apply H_. split.
        intros w HwΦ_spec.
        set (N := S (max w k')).
        assert (Ω x N ↓). { eapply Hneg. lia. }
        enough (¬ Ω x N ↓) by eauto.
        eapply Dec_false. eapply Hw. lia.  
        apply H_. split. 
        destruct h2 as w Hw. exists w.
        intros. specialize (Hw n H0). unfold limit_decider.
        destruct (Dec _); eauto.
        intro H. destruct H as w Hw.
        intros k Hneg*)


End Requirements_Lowness_Correctness.

Section Wall.

Construction


    Instance wall_instance: Wall := λ e L n, φ (λ x, Dec (In x L)) e e n.
    Definition P := P wall.
    Definition P_func := P_func wall.
    Instance E: Extension := simple_extension wall.

    Fact P_semi_decidable: semi_decidable P.
    Proof. eapply P_semi_decidable. Qed.

    Definition χ := χ (simple_extension wall).
    Definition P_Φ := (Φ_ χ).
    Definition P_Ω := (Ω χ).

    Section Verifiction.

Verifiction


    Hypothesis Σ_1_lem: LEM_Σ 1.

    Lemma attend_at_most_once_bound_constructive:
       k, s, e, e < k s', s < s' attend wall e s'.
    Proof. by apply attend_at_most_once_bound_test. Qed.

    Lemma eventally_wall:
       e, (∞∀ s, x, extendP (P_func s) s x wall e (P_func s) s < x).
    Proof.
      intros e.
      destruct (@attend_at_most_once_bound_constructive (S e)) as [s Hs].
      exists (S s). intros m Hm x [e_ [He_ He_']].
      destruct (Dec (e_ < e)) as [E|E].
      { exfalso. enough (attend wall e_ m).
        unshelve eapply (Hs e_ _ m); eauto; .
        split; first . destruct He_' as [H _].
        apply H. }
      assert (e e_) by ; clear E.
      destruct He_', , , , , .
      by eapply .
    Qed.


    Fact wall_convergence e : b : , lim_to wall (wall e) b.
    Proof.
      destruct (@eventally_wall e) as [N HN].
      assert ( m, dec (wall e (P_func m) m = 0)) as HD by eauto.
      assert (pdec ( x, N x wall e (P_func x) x = 0)) as [H'|H'].
      { apply assume_Π_1_lem. apply Σ_1_lem. intros x. eauto. }

      (* ccase (∀ x, N ≤ x → wall e (P_func x) x = 0) as H'|H'. *)
      - exists 0. exists N. intros. by apply H'.
      - enough ( x, N x wall e (P_func x) x 0) as H''.
        clear H'. destruct H'' as [x [ ]].
        destruct (wall e (P_func x) x) as [|k] eqn: H; first done; clear .
        exists (S k), x. intros t Ht. induction Ht; first done.
        rewrite (@φ_spec1 χ _ _ _ _ IHHt).
        reflexivity.
        intros; split.
        + intros K%Dec_true. apply Dec_auto.
          enough (incl (F_func (simple_extension wall) m) (F_func (simple_extension wall) (S m))).
          eauto. eapply F_mono; [apply F_func_correctness|apply F_func_correctness|].
        + intros K%Dec_true. specialize (F_func_correctness (simple_extension wall) (S m)) as HE.
          inv HE.
          * assert (wall e (P_func m) m < a).
            { eapply HN. . enough (P_func m = l) as . apply .
              eapply F_uni; [apply F_func_correctness|apply ]. }
            assert (wall e (P_func m) m = S k). { rewrite IHHt. reflexivity. }
            rewrite in . destruct (Dec (a = )).
            . apply Dec_auto. rewrite in K.
            destruct K; first done.
            enough ((F_func (simple_extension wall) m) = l) as by done.
            eapply F_uni; last apply ; apply F_func_correctness.
          * apply Dec_auto.
            enough (F_func (simple_extension wall) m = F_func (simple_extension wall) (S m)) as by eauto.
            eapply F_uni; first apply F_func_correctness.
            assumption.
        + eapply assume_Σ_1_dne. apply Σ_1_lem.
          { intro x. eauto. }
          intro H. apply H'. intros x Hx.
          assert ( n m: , ~~n=m n=m).
           { intros n m Hnm. destruct (Dec (n=m)); eauto.
              exfalso. by apply Hnm. }
          apply . intros Hmn.
          apply H. now exists x; split.
    Qed.


    Lemma N_requirements: e, (∞∃ n, P_Ω e n ) Ξ e (char_rel P) e.
    Proof.
      intros e He.
      destruct (@eventally_wall e) as [N HN].
      destruct (@wall_convergence e) as [B [b Hb]].
      set (M := max N b). destruct (He M) as [k [Hk Hk']].
      eapply (@φ_spec χ e e k); first apply Hk'.
      intros x Hx. unfold P, simple_extension.P.
      rewrite F_with_top. split.
      - intros (L & m & HL & HLs &HP).
        assert (L = P_func m) as E. { eapply F_uni. apply HL. apply F_func_correctness. }
        assert (x::L = P_func (S m)) as E'. { eapply F_uni. apply HLs. apply F_func_correctness. }
        apply Dec_auto. destruct (Dec (S m k)) as [E_|E_].
        enough (incl (P_func (S m)) (P_func k)). rewrite E' in H.
        eauto. eapply F_mono; last apply E_; apply F_func_correctness.
        assert (N m) as Em by . rewrite E in HP. specialize (HN m Em x HP).
        assert (k m) as Ek by . enough (x φ (χ m) e e m).
        exfalso. assert (φ (χ m) e e m < x).
        apply HN. . enough (φ (χ m) e e m = φ (χ k) e e k) by congruence.
        assert (φ (χ m) e e m = B).
        { rewrite (Hb m). reflexivity. . }
        assert (φ (χ k) e e k = B).
        { rewrite (Hb k). reflexivity. . }
        congruence.
      - intros H%Dec_true.
        eapply F_with_top. exists (F_func _ k), k; split; eauto.
        eapply F_func_correctness.
    Qed.


    Lemma convergent e : (∞∀ n, P_Ω e n ) (∞∀ n, ¬ P_Ω e n ).
    Proof.
      destruct (@eventally_wall e) as [N HN].
      assert (pdec ( k, N k P_Ω e k )) as [[k [Hk HNk]]|H'] by (apply assume_Σ_1_lem; eauto).
      - left. exists k. intros n Hm.
        induction Hm; first done.
        unfold P_Ω, Ω, Φ_ in *.
        destruct (φ (χ m) e e m) eqn: E.
        { eapply φ_spec0' in E. congruence. }
        (* Check φ_spec2. *)
        eapply (@φ_spec2 χ _ ); eauto.
        intros x Hx; split.
        + intros K%Dec_true. apply Dec_auto.
          enough (incl (F_func (simple_extension wall) m) (F_func (simple_extension wall) (S m))).
          eauto. eapply F_mono; [apply F_func_correctness|apply F_func_correctness|].
        + intros K%Dec_true. specialize (F_func_correctness (simple_extension wall) (S m)) as HE.
          inv HE.
          * assert (wall e (P_func m) m < a).
            { eapply HN. . enough (P_func m = l) as . apply .
              eapply F_uni; [apply F_func_correctness|apply ]. }
              assert (wall e (P_func m) m = S n). { unfold wall, wall_instance.
               rewrite E. reflexivity. }
            rewrite in H. destruct (Dec (a = x)).
            . apply Dec_auto. rewrite in K.
            destruct K; first done.
            enough ((F_func (simple_extension wall) m) = l) as by done.
            eapply F_uni; last apply ; apply F_func_correctness.
          * apply Dec_auto.
            enough (F_func (simple_extension wall) m = F_func (simple_extension wall) (S m)) as by eauto.
            eapply F_uni; first apply F_func_correctness.
            assumption.
      - right. exists N. intros m Hm.
        destruct (Dec (P_Ω e m )); eauto.
    Qed.


    Fact P_simple: simple P.
    Proof. eapply P_simple. intro e.
      intros H. apply H. apply wall_convergence.
    Qed.


    Hypothesis Σ_2_LEM:
       (P: Prop),
        ( n m, dec (P n m)) ( n, m, P n m) ¬ ( n, m, P n m).

    Fact jump_P_limit_test: limit_computable (P´).
    Proof.
      eapply Jump_limit; last done. apply F_with_χ.
      intros e He. eapply N_requirements; eauto.
    Qed.

    End Verifiction.

    Lemma eventally_wall_db e:
      ¬¬ (∞∀ s, x, extendP (P_func s) s x wall e (P_func s) s < x).
    Proof.
      intros H_. eapply (@attend_at_most_once_bound wall (S e)).
      intros [s Hs]. eapply H_; clear H_.
      exists (S s). intros m Hm x [e_ [He_ He_']].
      destruct (Dec (e_ < e)) as [E|E].
      { exfalso. enough (attend wall e_ m).
        unshelve eapply (Hs e_ _ m); eauto; .
        split; first . destruct He_' as [H _].
        apply H. }
      assert (e e_) by ; clear E.
      destruct He_', , , , , .
      by eapply .
    Qed.


    Fact wall_convergence_db e : ¬¬ b : , lim_to wall (wall e) b.
    Proof.
      intros H_.
      destruct (@eventally_wall_db e). intros [N HN].
      assert ( m, dec (wall e (P_func m) m = 0)) as HD by eauto.
      ccase ( x, N x wall e (P_func x) x = 0) as [H'|H'].
      - apply H_; clear H_. exists 0. exists N. intros. by apply H'.
      - enough (~~ x, N x wall e (P_func x) x 0) as H__.
        apply H__. intros H''.
        clear H'. destruct H'' as [x [ ]].
        apply H_; clear H_.
        destruct (wall e (P_func x) x) as [|k] eqn: H; first done; clear .
        exists (S k), x. intros t Ht. induction Ht; first done.
        rewrite (@φ_spec1 χ _ _ _ _ IHHt).
        reflexivity.
        intros; split.
        + intros K%Dec_true. apply Dec_auto.
          enough (incl (F_func (simple_extension wall) m) (F_func (simple_extension wall) (S m))).
          eauto. eapply F_mono; [apply F_func_correctness|apply F_func_correctness|].
        + intros K%Dec_true. specialize (F_func_correctness (simple_extension wall) (S m)) as HE.
          inv HE.
          * assert (wall e (P_func m) m < a).
            { eapply HN. . enough (P_func m = l) as . apply .
              eapply F_uni; [apply F_func_correctness|apply ]. }
            assert (wall e (P_func m) m = S k). { rewrite IHHt. reflexivity. }
            rewrite in . destruct (Dec (a = )).
            . apply Dec_auto. rewrite in K.
            destruct K; first done.
            enough ((F_func (simple_extension wall) m) = l) as by done.
            eapply F_uni; last apply ; apply F_func_correctness.
          * apply Dec_auto.
            enough (F_func (simple_extension wall) m = F_func (simple_extension wall) (S m)) as by eauto.
            eapply F_uni; first apply F_func_correctness.
            assumption.
        + intro H.
          apply H'. intros x Hx.
          assert ( n m: , ~~n=m n=m).
           { intros n m Hnm. destruct (Dec (n=m)); eauto.
              exfalso. by apply Hnm. }
          apply . intros Hmn.
          apply H. now exists x; split.
    Qed.


    Lemma N_requirements_db: e, (∞∃ n, P_Ω e n ) ¬ ¬ Ξ e (char_rel P) e.
    Proof.
      intros e He H_.
      apply (@eventally_wall_db e). intros [N HN].
      apply (@wall_convergence_db e). intros [B [b Hb]].
      apply H_; clear H_.
      set (M := max N b). destruct (He M) as [k [Hk Hk']].
      eapply (@φ_spec χ e e k); first apply Hk'.
      intros x Hx. unfold P, simple_extension.P.
      rewrite F_with_top. split.
      - intros (L & m & HL & HLs &HP).
        assert (L = P_func m) as E. { eapply F_uni. apply HL. apply F_func_correctness. }
        assert (x::L = P_func (S m)) as E'. { eapply F_uni. apply HLs. apply F_func_correctness. }
        apply Dec_auto. destruct (Dec (S m k)) as [E_|E_].
        enough (incl (P_func (S m)) (P_func k)). rewrite E' in H.
        eauto. eapply F_mono; last apply E_; apply F_func_correctness.
        assert (N m) as Em by . rewrite E in HP. specialize (HN m Em x HP).
        assert (k m) as Ek by . enough (x φ (χ m) e e m).
        exfalso. assert (φ (χ m) e e m < x).
        apply HN. . enough (φ (χ m) e e m = φ (χ k) e e k) by congruence.
        assert (φ (χ m) e e m = B).
        { rewrite (Hb m). reflexivity. . }
        assert (φ (χ k) e e k = B).
        { rewrite (Hb k). reflexivity. . }
        congruence.
      - intros H%Dec_true.
        eapply F_with_top. exists (F_func _ k), k; split; eauto.
        eapply F_func_correctness.
    Qed.


    (* Should be enough if we use DNE_Σ_2 to drop out ¬¬ for both
        eventally_wall and wall_convergence *)


    Section with_LEM_2.

    Hypothesis LEM_Σ_2:
     (P: Prop), ( n m, dec (P n m)) ( n, m, P n m) ¬ ( n, m, P n m).

    Hypothesis DN: P, ¬ ¬ P P.
    Fact jump_P_limit: limit_computable (P´).
    Proof.
      eapply Jump_limit; last done. apply F_with_χ.
      intros e He. eapply DN, N_requirements_db; eauto.
    Qed.


    End with_LEM_2.

    Section with_LEM_1.

    Hypothesis LEM_Σ_1: LEM_Σ 1.

    Fact jump_P_limit_2: limit_computable (P´).
    Proof.
      eapply Jump_limit_1; first apply F_with_χ.
      - intros e He. eapply N_requirements; eauto.
      - eapply convergent; eauto.
    Qed.


    End with_LEM_1.

End Wall.

(* Check jump_P_limit_2. *)