Commit edff0fe3 authored by Robbert Krebbers's avatar Robbert Krebbers

Use Inhabited type class for fixpoint and solver.

parent d9bae949
...@@ -93,35 +93,36 @@ Section cofe. ...@@ -93,35 +93,36 @@ Section cofe.
End cofe. End cofe.
(** Fixpoint *) (** Fixpoint *)
Program Definition fixpoint_chain `{Cofe A} (f : A A) `{!Contractive f} Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A A)
(x : A) : chain A := {| chain_car i := Nat.iter i f x |}. `{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
Next Obligation. Next Obligation.
intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|]. 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. destruct i as [|i]; simpl; try lia; apply contractive, IH; auto with lia.
Qed. Qed.
Program Definition fixpoint `{Cofe A} (f : A A) `{!Contractive f} Program Definition fixpoint `{Cofe A, Inhabited A} (f : A A)
(x : A) : A := compl (fixpoint_chain f x). `{!Contractive f} : A := compl (fixpoint_chain f).
Section fixpoint. Section fixpoint.
Context `{Cofe A} (f : A A) `{!Contractive f}. Context `{Cofe A, Inhabited A} (f : A A) `{!Contractive f}.
Lemma fixpoint_unfold x : fixpoint f x f (fixpoint f x). Lemma fixpoint_unfold : fixpoint f f (fixpoint f).
Proof. Proof.
apply equiv_dist; intros n; unfold fixpoint. apply equiv_dist; intros n; unfold fixpoint.
rewrite (conv_compl (fixpoint_chain f x) n). rewrite (conv_compl (fixpoint_chain f) n).
by rewrite (chain_cauchy (fixpoint_chain f x) n (S n)) at 1 by lia. by rewrite (chain_cauchy (fixpoint_chain f) n (S n)) at 1 by lia.
Qed. Qed.
Lemma fixpoint_ne (g : A A) `{!Contractive g} x y n : Lemma fixpoint_ne (g : A A) `{!Contractive g} n :
( z, f z ={n}= g z) fixpoint f x ={n}= fixpoint g y. ( z, f z ={n}= g z) fixpoint f ={n}= fixpoint g.
Proof. Proof.
intros Hfg; unfold fixpoint; rewrite (conv_compl (fixpoint_chain f x) n), intros Hfg; unfold fixpoint.
(conv_compl (fixpoint_chain g y) n). rewrite (conv_compl (fixpoint_chain f) n),(conv_compl (fixpoint_chain g) n).
induction n as [|n IH]; simpl in *; [done|]. induction n as [|n IH]; simpl in *; [done|].
rewrite Hfg; apply contractive, IH; auto using dist_S. rewrite Hfg; apply contractive, IH; auto using dist_S.
Qed. Qed.
Lemma fixpoint_proper (g : A A) `{!Contractive g} x : Lemma fixpoint_proper (g : A A) `{!Contractive g} :
( x, f x g x) fixpoint f x fixpoint g x. ( x, f x g x) fixpoint f fixpoint g.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed. Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
End fixpoint. End fixpoint.
Global Opaque fixpoint.
(** Function space *) (** Function space *)
Structure cofeMor (A B : cofeT) : Type := CofeMor { 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. ...@@ -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. Proof. done. Qed.
Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B). Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B).
Infix "-n>" := cofe_mor (at level 45, right associativity). 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 *) (** Identity and composition *)
Definition cid {A} : A -n> A := CofeMor id. Definition cid {A} : A -n> A := CofeMor id.
......
...@@ -2,7 +2,7 @@ Require Export iris.cofe. ...@@ -2,7 +2,7 @@ Require Export iris.cofe.
Section solver. Section solver.
Context (F : cofeT cofeT cofeT). 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}, Context (map : {A1 A2 B1 B2 : cofeT},
((A2 -n> A1) * (B1 -n> B2)) (F A1 B1 -n> F A2 B2)). ((A2 -n> A1) * (B1 -n> B2)) (F A1 B1 -n> F A2 B2)).
Arguments map {_ _ _ _} _. Arguments map {_ _ _ _} _.
...@@ -22,7 +22,7 @@ Proof. by rewrite <-!cofe_mor_ext; intros Hf Hg Hx; rewrite Hf, Hg, Hx. Qed. ...@@ -22,7 +22,7 @@ Proof. by rewrite <-!cofe_mor_ext; intros Hf Hg Hx; rewrite Hf, Hg, Hx. Qed.
Fixpoint A (k : nat) : cofeT := Fixpoint A (k : nat) : cofeT :=
match k with 0 => CofeT unit | S k => F (A k) (A k) end. match k with 0 => CofeT unit | S k => F (A k) (A k) end.
Fixpoint f {k} : A k -n> A (S k) := 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 := with g {k} : A (S k) -n> A k :=
match k with 0 => CofeMor (λ _, () : CofeT ()) | S k => map (f,g) end. 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. Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
......
...@@ -74,6 +74,7 @@ Instance uPred_entails {M} : SubsetEq (uPred M) := λ P Q, ∀ x n, ...@@ -74,6 +74,7 @@ Instance uPred_entails {M} : SubsetEq (uPred M) := λ P Q, ∀ x n,
Program Definition uPred_const {M} (P : Prop) : uPred M := Program Definition uPred_const {M} (P : Prop) : uPred M :=
{| uPred_holds n x := P |}. {| uPred_holds n x := P |}.
Solve Obligations with done. 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 := Program Definition uPred_and {M} (P Q : uPred M) : uPred M :=
{| uPred_holds n x := P n x Q n x |}. {| uPred_holds n x := P n x Q n x |}.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment