diff --git a/iris/cofe.v b/iris/cofe.v index f0cd655a8d4be000e6f00b1270737259b9500937..2c27d072fd07a2c4a49e8e23ec306392e4080a33 100644 --- a/iris/cofe.v +++ b/iris/cofe.v @@ -93,35 +93,36 @@ Section cofe. End cofe. (** Fixpoint *) -Program Definition fixpoint_chain `{Cofe A} (f : A → A) `{!Contractive f} - (x : A) : chain A := {| chain_car i := Nat.iter i f x |}. +Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A → A) + `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}. Next Obligation. intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|]. destruct i as [|i]; simpl; try lia; apply contractive, IH; auto with lia. Qed. -Program Definition fixpoint `{Cofe A} (f : A → A) `{!Contractive f} - (x : A) : A := compl (fixpoint_chain f x). +Program Definition fixpoint `{Cofe A, Inhabited A} (f : A → A) + `{!Contractive f} : A := compl (fixpoint_chain f). Section fixpoint. - Context `{Cofe A} (f : A → A) `{!Contractive f}. - Lemma fixpoint_unfold x : fixpoint f x ≡ f (fixpoint f x). + Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}. + Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f). Proof. apply equiv_dist; intros n; unfold fixpoint. - rewrite (conv_compl (fixpoint_chain f x) n). - by rewrite (chain_cauchy (fixpoint_chain f x) n (S n)) at 1 by lia. + rewrite (conv_compl (fixpoint_chain f) n). + by rewrite (chain_cauchy (fixpoint_chain f) n (S n)) at 1 by lia. Qed. - Lemma fixpoint_ne (g : A → A) `{!Contractive g} x y n : - (∀ z, f z ={n}= g z) → fixpoint f x ={n}= fixpoint g y. + Lemma fixpoint_ne (g : A → A) `{!Contractive g} n : + (∀ z, f z ={n}= g z) → fixpoint f ={n}= fixpoint g. Proof. - intros Hfg; unfold fixpoint; rewrite (conv_compl (fixpoint_chain f x) n), - (conv_compl (fixpoint_chain g y) n). + intros Hfg; unfold fixpoint. + rewrite (conv_compl (fixpoint_chain f) n),(conv_compl (fixpoint_chain g) n). induction n as [|n IH]; simpl in *; [done|]. rewrite Hfg; apply contractive, IH; auto using dist_S. Qed. - Lemma fixpoint_proper (g : A → A) `{!Contractive g} x : - (∀ x, f x ≡ g x) → fixpoint f x ≡ fixpoint g x. + Lemma fixpoint_proper (g : A → A) `{!Contractive g} : + (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g. Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. End fixpoint. +Global Opaque fixpoint. (** Function space *) Structure cofeMor (A B : cofeT) : Type := CofeMor { @@ -170,6 +171,8 @@ Lemma cofe_mor_ext {A B} (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x. Proof. done. Qed. Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B). Infix "-n>" := cofe_mor (at level 45, right associativity). +Instance cofe_more_inhabited (A B : cofeT) + `{Inhabited B} : Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)). (** Identity and composition *) Definition cid {A} : A -n> A := CofeMor id. diff --git a/iris/cofe_solver.v b/iris/cofe_solver.v index 59a85698f3ebcc5ab8c38540bc4a9ae468d520c4..81b86c3cfda04c6dc09f7bcda07c5006891bae94 100644 --- a/iris/cofe_solver.v +++ b/iris/cofe_solver.v @@ -2,7 +2,7 @@ Require Export iris.cofe. Section solver. Context (F : cofeT → cofeT → cofeT). -Context (p : F (CofeT unit) (CofeT unit)). +Context `{Finhab : Inhabited (F (CofeT unit) (CofeT unit))}. Context (map : ∀ {A1 A2 B1 B2 : cofeT}, ((A2 -n> A1) * (B1 -n> B2)) → (F A1 B1 -n> F A2 B2)). Arguments map {_ _ _ _} _. @@ -22,7 +22,7 @@ Proof. by rewrite <-!cofe_mor_ext; intros Hf Hg Hx; rewrite Hf, Hg, Hx. Qed. Fixpoint A (k : nat) : cofeT := match k with 0 => CofeT unit | S k => F (A k) (A k) end. Fixpoint f {k} : A k -n> A (S k) := - match k with 0 => CofeMor (λ _, p) | S k => map (g,f) end + match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end with g {k} : A (S k) -n> A k := match k with 0 => CofeMor (λ _, () : CofeT ()) | S k => map (f,g) end. Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl. diff --git a/iris/logic.v b/iris/logic.v index 7d6ce839194db5b4db6a1d438db154d6f221b35c..9aa9f4c53e307dc7e28d5c2ecf27938176b85180 100644 --- a/iris/logic.v +++ b/iris/logic.v @@ -74,6 +74,7 @@ Instance uPred_entails {M} : SubsetEq (uPred M) := λ P Q, ∀ x n, Program Definition uPred_const {M} (P : Prop) : uPred M := {| uPred_holds n x := P |}. Solve Obligations with done. +Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True). Program Definition uPred_and {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := P n x ∧ Q n x |}.