### More consistent naming for fixpoints.

```- Use Φ and Ψ for predicates.
- Use _1 and _2 suffixes for the different directions of a lemma.
- Not all lemmas started with _uPred; we do not let the bigop lemmas (for instance)
start with uPred_ either, so I just got rid of the prefix.```
parent b59ddcd1
Pipeline #4358 passed with stage
in 6 minutes and 30 seconds
 ... ... @@ -7,70 +7,73 @@ Import uPred. the logic. *) Definition uPred_mono_pred {M A} (F : (A → uPred M) → (A → uPred M)) := ∀ P Q, ((□ ∀ x, P x → Q x) → ∀ x, F P x → F Q x)%I. ∀ Φ Ψ, ((□ ∀ x, Φ x → Ψ x) → ∀ x, F Φ x → F Ψ x)%I. Definition uPred_least_fixpoint {M A} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M := (∀ P, □ (∀ x, F P x → P x) → P x)%I. Definition uPred_least_fixpoint {M A} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M := (∀ Φ, □ (∀ x, F Φ x → Φ x) → Φ x)%I. Definition uPred_greatest_fixpoint {M A} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M := (∃ P, □ (∀ x, P x → F P x) ∧ P x)%I. Definition uPred_greatest_fixpoint {M A} (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M := (∃ Φ, □ (∀ x, Φ x → F Φ x) ∧ Φ x)%I. Section least. Context {M : ucmraT} {A} (F : (A → uPred M) → (A → uPred M)) (Hmono : uPred_mono_pred F). Context {M : ucmraT}. Context {A} (F : (A → uPred M) → (A → uPred M)) (Hmono : uPred_mono_pred F). Lemma F_fix_implies_least_fixpoint x : F (uPred_least_fixpoint F) x ⊢ uPred_least_fixpoint F x. Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x ⊢ uPred_least_fixpoint F x. Proof. iIntros "HF" (P) "#Hincl". iApply "Hincl". iApply (Hmono _ P); last done. iIntros "HF" (Φ) "#Hincl". iApply "Hincl". iApply (Hmono _ Φ); last done. iIntros "!#" (y) "Hy". iApply "Hy". done. Qed. Lemma least_fixpoint_implies_F_fix x : Lemma least_fixpoint_unfold_1 x : uPred_least_fixpoint F x ⊢ F (uPred_least_fixpoint F) x. Proof. iIntros "HF". iApply "HF". iIntros "!#" (y) "Hy". iApply Hmono; last done. iIntros "!#" (z) "?". by iApply F_fix_implies_least_fixpoint. by iApply least_fixpoint_unfold_2. Qed. Corollary uPred_least_fixpoint_unfold x : Corollary least_fixpoint_unfold x : uPred_least_fixpoint F x ≡ F (uPred_least_fixpoint F) x. Proof. apply (anti_symm _); auto using least_fixpoint_implies_F_fix, F_fix_implies_least_fixpoint. apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2. Qed. Lemma uPred_least_fixpoint_ind (P : A → uPred M) : □ (∀ y, F P y → P y) ⊢ ∀ x, uPred_least_fixpoint F x → P x. Proof. iIntros "#HP" (x) "HF". iApply "HF". done. Qed. Lemma least_fixpoint_ind (Φ : A → uPred M) : □ (∀ y, F Φ y → Φ y) ⊢ ∀ x, uPred_least_fixpoint F x → Φ x. Proof. iIntros "#HΦ" (x) "HF". iApply "HF". done. Qed. End least. Section greatest. Context {M : ucmraT} {A} (F : (A → uPred M) → (A → uPred M)) (Hmono : uPred_mono_pred F). Lemma greatest_fixpoint_implies_F_fix x : Lemma greatest_fixpoint_unfold_1 x : uPred_greatest_fixpoint F x ⊢ F (uPred_greatest_fixpoint F) x. Proof. iDestruct 1 as (P) "[#Hincl HP]". iApply (Hmono P (uPred_greatest_fixpoint F)). - iAlways. iIntros (y) "Hy". iExists P. by iSplit. iDestruct 1 as (Φ) "[#Hincl HΦ]". iApply (Hmono Φ (uPred_greatest_fixpoint F)). - iIntros "!#" (y) "Hy". iExists Φ. auto. - by iApply "Hincl". Qed. Lemma F_fix_implies_greatest_fixpoint x : Lemma greatest_fixpoint_unfold_2 x : F (uPred_greatest_fixpoint F) x ⊢ uPred_greatest_fixpoint F x. Proof. iIntros "HF". iExists (F (uPred_greatest_fixpoint F)). iIntros "{\$HF} !#"; iIntros (y) "Hy". iApply (Hmono with "[] Hy"). iAlways. iIntros (z) "?". by iApply greatest_fixpoint_implies_F_fix. iIntros "{\$HF} !#" (y) "Hy". iApply (Hmono with "[] Hy"). iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1. Qed. Corollary uPred_greatest_fixpoint_unfold x : Corollary greatest_fixpoint_unfold x : uPred_greatest_fixpoint F x ≡ F (uPred_greatest_fixpoint F) x. Proof. apply (anti_symm _); auto using greatest_fixpoint_implies_F_fix, F_fix_implies_greatest_fixpoint. apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2. Qed. Lemma uPred_greatest_fixpoint_coind (P : A → uPred M) : □ (∀ y, P y → F P y) ⊢ ∀ x, P x → uPred_greatest_fixpoint F x. Proof. iIntros "#HP" (x) "Hx". iExists P. by iIntros "{\$Hx} !#". Qed. Lemma greatest_fixpoint_coind (Φ : A → uPred M) : □ (∀ y, Φ y → F Φ y) ⊢ ∀ x, Φ x → uPred_greatest_fixpoint F x. Proof. iIntros "#HΦ" (x) "Hx". iExists Φ. by iIntros "{\$Hx} !#". Qed. End greatest.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!