updated

Author: HaoyiZeng

theories/PostsProblem/lowness.v

@@ -84,225 +84,186 @@ Section Requirements_Meet.
 
     Hypothesis wall_spec: forall e L n, φ (λ x, Dec (In x L)) e e n ≤ wall e L n.
 
+    Definition use := λ e n, φ (χ n) e e n.
+
+    Lemma eventally_greater_than_use_gen e:
+      (∃ n, (∀ e', e' < e → ∀ n', n < n' → ¬ (recv_att wall) e' n')) →
+      (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
+    Proof.
+      intros Hc. destruct Hc as [s Hs].
+      exists (S s). intros m Hm x [e_ [He_ He_']].
+      destruct (Dec (e_ < e)) as [E|E].
+      { exfalso. enough (recv_att wall e_ m).
+        unshelve eapply (Hs e_ _ m); eauto; lia.
+        split; first lia. destruct He_' as [H _].
+        apply H. }
+      assert (e ≤ e_) by lia; clear E.
+      destruct He_', H1, H1, H1, H1, H3.
+      specialize(H5 e H).
+      enough (use e m <= wall e (P_func m) m) by lia.
+      apply wall_spec.
+    Qed.
+
+    Lemma eventally_greater_than_use_classically e:
+      ¬¬ (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
+    Proof.
+      intros H_. eapply (@recv_at_most_once_bound_classically wall e).
+      intros H'. apply H_. 
+      by apply eventally_greater_than_use_gen.
+    Qed.
 
 
-(* 
-    Lemma N_requirements e : (∞∀ n, P_Ω e n ↓) ∨ (∞∀ n, ¬ P_Ω e n ↓).
+    Fact wall_convergence_gen e : 
+      (∃ N, (∀ s, N ≤ s → ∀ x, extendP (P_func s) s x → use e s < x)
+        ∧ pdec (∃ x, N ≤ x ∧ use e x ≠ 0)) ->
+      (∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b).
     Proof.
-      destruct (@eventally_greater_than_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 (N & HN & Hp).
+      assert (∀ m, dec (use e m = 0)) as HD by eauto.
+      destruct Hp as [H'|H'].
+      - enough (∃ x, N ≤ x ∧ use e x ≠ 0) as H''.
+        clear H'. destruct H'' as [x [H1 H2]].
+        destruct (use e x) as [|k] eqn: H; first done; clear H2.
+        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|lia].
         + 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. lia. enough (P_func m = l) as ->. apply H2.
-              eapply F_uni; [apply F_func_correctness|apply H1]. }
-              assert (wall e (P_func m) m ≥ S n). {
-              rewrite <-E. apply wall_spec. }
-            destruct (Dec (a = x)).
-            lia. apply Dec_auto. rewrite <- H0 in K.
+          * assert (use e m < a).
+            { eapply HN. lia. enough (P_func m = l) as ->. apply H5.
+              eapply F_uni; [apply F_func_correctness|apply H4]. }
+            assert (wall e (P_func m) m ≥ S k). { rewrite <-IHHt.
+            unfold use. unfold χ, the_priority_method.χ.
+            specialize (wall_spec e (F_func (simple_extension wall) m) m).  
+            eapply wall_spec. }
+            destruct (Dec (a = x0)).
+            lia. apply Dec_auto. rewrite <- H3 in K.
             destruct K; first done.
             enough ((F_func (simple_extension wall) m) = l) as -> by done.
-            eapply F_uni; last apply H1; apply F_func_correctness.
+            eapply F_uni; last apply H4; 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. *)
-
-
-  Definition use := λ e n, φ (χ n) e e n.
-
-  Lemma eventally_greater_than_use_gen e:
-    (∃ n, (∀ e', e' < e → ∀ n', n < n' → ¬ (recv_att wall) e' n')) →
-    (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
-  Proof.
-    intros Hc. destruct Hc as [s Hs].
-    exists (S s). intros m Hm x [e_ [He_ He_']].
-    destruct (Dec (e_ < e)) as [E|E].
-    { exfalso. enough (recv_att wall e_ m).
-      unshelve eapply (Hs e_ _ m); eauto; lia.
-      split; first lia. destruct He_' as [H _].
-      apply H. }
-    assert (e ≤ e_) by lia; clear E.
-    destruct He_', H1, H1, H1, H1, H3.
-    specialize(H5 e H).
-    enough (use e m <= wall e (P_func m) m) by lia.
-    apply wall_spec.
-  Qed.
-
-  Lemma eventally_greater_than_use_classically e:
-    ¬¬ (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
-  Proof.
-    intros H_. eapply (@recv_at_most_once_bound_classically wall e).
-    intros H'. apply H_. 
-    by apply eventally_greater_than_use_gen.
-  Qed.
-
-
-  Fact wall_convergence_gen e : 
-    (∃ N, (∀ s, N ≤ s → ∀ x, extendP (P_func s) s x → use e s < x)
-      ∧ pdec (∃ x, N ≤ x ∧ use e x ≠ 0)) ->
-    (∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b).
-  Proof.
-    intros (N & HN & Hp).
-    assert (∀ m, dec (use e m = 0)) as HD by eauto.
-    destruct Hp as [H'|H'].
-    - enough (∃ x, N ≤ x ∧ use e x ≠ 0) as H''.
-      clear H'. destruct H'' as [x [H1 H2]].
-      destruct (use e x) as [|k] eqn: H; first done; clear H2.
-      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|lia].
-      + intros K%Dec_true. specialize (F_func_correctness (simple_extension wall) (S m)) as HE.
-        inv HE. 
-        * assert (use e m < a).
-          { eapply HN. lia. enough (P_func m = l) as ->. apply H5.
-            eapply F_uni; [apply F_func_correctness|apply H4]. }
-          assert (wall e (P_func m) m ≥ S k). { rewrite <-IHHt.
-          unfold use. unfold χ, the_priority_method.χ.
-          specialize (wall_spec e (F_func (simple_extension wall) m) m).  
-          eapply wall_spec. }
-          destruct (Dec (a = x0)).
-          lia. apply Dec_auto. rewrite <- H3 in K.
-          destruct K; first done.
-          enough ((F_func (simple_extension wall) m) = l) as -> by done.
-          eapply F_uni; last apply H4; 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.
-      + apply H'.
-    - exists 0. exists N. intros.
-      destruct (use e m) eqn: E; first done.
-      exfalso. apply H'. exists m. split; first done.
-      congruence.
-  Qed.
-
-
-  Fact wall_convergence_classically e : ¬¬ ∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b.
-  Proof.
-    intros H. eapply (eventally_greater_than_use_classically). intros [N HN].
-    assert (¬¬ pdec (∃ x, N ≤ x ∧ use e x ≠ 0)).
-    { ccase (∃ x, N ≤ x ∧ use e x ≠ 0) as [H_|H'_]; eauto.
-      - intros Hp. apply Hp. left. done.
-      - intros Hp. apply Hp. right. done. }
-    apply H0. intros H0'.
-    apply H, wall_convergence_gen.
-    exists N; eauto.
-  Qed.
+            assumption.
+        + apply H'.
+      - exists 0. exists N. intros.
+        destruct (use e m) eqn: E; first done.
+        exfalso. apply H'. exists m. split; first done.
+        congruence.
+    Qed.
 
-  Hypothesis Σ_1_lem: LEM_Σ 1.
 
-  Lemma attention_bound:  
-    ∀ k, ∃ s, ∀ e, e < k → ∀ s', s < s' → ~ recv_att wall e s'.
-  Proof. by apply recv_at_most_once_bound. Qed.
+    Fact wall_convergence_classically e : ¬¬ ∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b.
+    Proof.
+      intros H. eapply (eventally_greater_than_use_classically). intros [N HN].
+      assert (¬¬ pdec (∃ x, N ≤ x ∧ use e x ≠ 0)).
+      { ccase (∃ x, N ≤ x ∧ use e x ≠ 0) as [H_|H'_]; eauto.
+        - intros Hp. apply Hp. left. done.
+        - intros Hp. apply Hp. right. done. }
+      apply H0. intros H0'.
+      apply H, wall_convergence_gen.
+      exists N; eauto.
+    Qed.
 
-  Lemma eventally_greater_than_use e: 
-    (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
-  Proof. apply eventally_greater_than_use_gen, attention_bound. Qed.
+    Hypothesis Σ_1_lem: LEM_Σ 1.
 
-  Fact wall_convergence e : ∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b.
-  Proof.
-    apply wall_convergence_gen.
-    destruct (eventally_greater_than_use e) as [N HN].
-    exists N. split; first done.
-    destruct level1 as (_&h2&_).
-    rewrite h2 in Σ_1_lem.
-    unfold principles.LPO in *.
-    destruct (@Σ_1_lem (λ x, Dec (N ≤ x ∧ use e x ≠ 0))) as [[N' HN']|].
-    left. exists N'. eauto.
-    right. intros [x Hx]. apply H. exists x. eauto.
-  Qed.
+    Lemma attention_bound:  
+      ∀ k, ∃ s, ∀ e, e < k → ∀ s', s < s' → ~ recv_att wall e s'.
+    Proof. by apply recv_at_most_once_bound. Qed.
 
-  Corollary N_requirements e : ((∞∀ n, P_Ω e n ↓) ∨ (∞∀ n, ¬ P_Ω e n ↓)).
-  Proof.
-    destruct (wall_convergence e) as (b&n&Hn).
-    destruct b. 
-    - right. exists n. intros.
-      enough(P_Ω e m = None) by congruence.
-      unfold P_Ω, Ω.
-      apply φ_spec0'.
-      by apply Hn.
-    - left. exists n. intros.
-      unfold P_Ω, Ω.
-      apply φ_spec0_1.
-      unfold use in Hn.
-      by rewrite (Hn m H).
-  Qed.
+    Lemma eventally_greater_than_use e: 
+      (∞∀ s, ∀ x, extendP (P_func s) s x → use e s < x).
+    Proof. apply eventally_greater_than_use_gen, attention_bound. Qed.
 
-  Lemma eventally_greater_than_wall e: 
-    (∞∀ s, ∀ x, extendP (P_func s) s x → wall e (P_func s) s < x).
-  Proof.
-    destruct (@attention_bound (S e)) as [s Hs].
-    exists (S s). intros m Hm x [e_ [He_ He_']].
-    destruct (Dec (e_ < e)) as [E|E].
-    { exfalso. enough (recv_att wall e_ m).
-      unshelve eapply (Hs e_ _ m); eauto; lia.
-      split; first lia. destruct He_' as [H _].
-      apply H. }
-    assert (e ≤ e_) by lia; clear E.
-    destruct He_', H1, H1, H1, H1, H3.
-    by eapply H5.
-  Qed.
-
-  Lemma step_ex_spec: ∀ e, (∞∃ n, P_Ω e n ↓) → Ξ e (char_rel P) e.
-  Proof.
-    intros e He.
-    destruct (eventally_greater_than_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, simpleness.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 lia. rewrite E in HP. specialize (HN m Em x HP).
-      assert (k ≤ m) as Ek by lia.
-      enough (x ≤ φ (χ m) e e m).
-      exfalso. assert (φ (χ m) e e m < x).
-      assert(φ (χ m) e e m  ≤ wall e (P_func m) m).
-      { specialize (wall_spec e (F_func (simple_extension wall) m) m).
-        unfold χ, the_priority_method.χ.
-        by rewrite wall_spec. }
-      lia.
-      enough (φ (χ  m) e e m = φ (χ  k) e e k) by lia.
-      assert (φ (χ m) e e m = B).  
-      { rewrite <- (Hb m). reflexivity. lia. }
-      assert (φ (χ k) e e k = B).  
-      { rewrite <- (Hb k). reflexivity. lia. }
+    Fact wall_convergence e : ∃ b n: nat, ∀ m : nat, n ≤ m → use e m = b.
+    Proof.
+      apply wall_convergence_gen.
+      destruct (eventally_greater_than_use e) as [N HN].
+      exists N. split; first done.
+      destruct level1 as (_&h2&_).
+      rewrite h2 in Σ_1_lem.
+      unfold principles.LPO in *.
+      destruct (@Σ_1_lem (λ x, Dec (N ≤ x ∧ use e x ≠ 0))) as [[N' HN']|].
+      left. exists N'. eauto.
+      right. intros [x Hx]. apply H. exists x. eauto.
+    Qed.
+
+    Corollary N_requirements e : ((∞∀ n, P_Ω e n ↓) ∨ (∞∀ n, ¬ P_Ω e n ↓)).
+    Proof.
+      destruct (wall_convergence e) as (b&n&Hn).
+      destruct b. 
+      - right. exists n. intros.
+        enough(P_Ω e m = None) by congruence.
+        unfold P_Ω, Ω.
+        apply φ_spec0'.
+        by apply Hn.
+      - left. exists n. intros.
+        unfold P_Ω, Ω.
+        apply φ_spec0_1.
+        unfold use in Hn.
+        by rewrite (Hn m H).
+    Qed.
+
+    Lemma eventally_greater_than_wall e: 
+      (∞∀ s, ∀ x, extendP (P_func s) s x → wall e (P_func s) s < x).
+    Proof.
+      destruct (@attention_bound (S e)) as [s Hs].
+      exists (S s). intros m Hm x [e_ [He_ He_']].
+      destruct (Dec (e_ < e)) as [E|E].
+      { exfalso. enough (recv_att wall e_ m).
+        unshelve eapply (Hs e_ _ m); eauto; lia.
+        split; first lia. destruct He_' as [H _].
+        apply H. }
+      assert (e ≤ e_) by lia; clear E.
+      destruct He_', H1, H1, H1, H1, H3.
+      by eapply H5.
+    Qed.
+
+    Lemma step_ex_spec: ∀ e, (∞∃ n, P_Ω e n ↓) → Ξ e (char_rel P) e.
+    Proof.
+      intros e He.
+      destruct (eventally_greater_than_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, simpleness.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 lia. rewrite E in HP. specialize (HN m Em x HP).
+        assert (k ≤ m) as Ek by lia.
+        enough (x ≤ φ (χ m) e e m).
+        exfalso. assert (φ (χ m) e e m < x).
+        assert(φ (χ m) e e m  ≤ wall e (P_func m) m).
+        { specialize (wall_spec e (F_func (simple_extension wall) m) m).
+          unfold χ, the_priority_method.χ.
+          by rewrite wall_spec. }
+        lia.
+        enough (φ (χ  m) e e m = φ (χ  k) e e k) by lia.
+        assert (φ (χ m) e e m = B).  
+        { rewrite <- (Hb m). reflexivity. lia. }
+        assert (φ (χ k) e e k = B).  
+        { rewrite <- (Hb k). reflexivity. lia. }
+          lia. 
+        enough (φ (χ  m) e e m = φ (χ  k) e e k) by lia.
+        assert (φ (χ m) e e m = B).  
+        { rewrite <- (Hb m). reflexivity. lia. }
+        assert (φ (χ k) e e k = B).  
+        { rewrite <- (Hb k). reflexivity. lia. }
         lia. 
-      enough (φ (χ  m) e e m = φ (χ  k) e e k) by lia.
-      assert (φ (χ m) e e m = B).  
-      { rewrite <- (Hb m). reflexivity. lia. }
-      assert (φ (χ k) e e k = B).  
-      { rewrite <- (Hb k). reflexivity. lia. }
-      lia. 
-    - intros H%Dec_true.
-      eapply F_with_top. 
-      exists (F_func _ k), k; split; eauto.
-      eapply F_func_correctness.
-  Qed.
+      - intros H%Dec_true.
+        eapply F_with_top. 
+        exists (F_func _ k), k; split; eauto.
+        eapply F_func_correctness.
+    Qed.
 
   End wall_greater_than_use.