Commit 091265d4 authored by Ralf Jung's avatar Ralf Jung

use "-n>" in the world_prop signature

parent 1804f34f
......@@ -470,7 +470,7 @@ Section FinDom.
Context {V} `{cV : pcmType V}.
Definition equiv_fd (f1 f2 : K -f> V) := forall k, f1 k == f2 k.
Global Program Instance type_findom : Setoid (K -f> V) := mkType equiv_fd.
Global Program Instance type_findom : Setoid (K -f> V) | 5:= mkType equiv_fd.
Next Obligation.
split.
- intros m k; reflexivity.
......@@ -489,7 +489,7 @@ Section FinDom.
| S _ => forall k, f1 k = n = f2 k
end.
Global Program Instance metric_findom : metric (K -f> V) := mkMetr dist_fd.
Global Program Instance metric_findom : metric (K -f> V) | 5 := mkMetr dist_fd.
Next Obligation.
revert n; intros [| n] f1 f2 EQf g1 g2 EQg; [reflexivity |]; split;
intros EQ k; [symmetry in EQf, EQg |]; rewrite EQf, EQg; apply EQ.
......@@ -552,7 +552,7 @@ Section FinDom.
fun n => Indom_lookup x (findom_t (σ (S n))) (proj2 (In_inlst _ _) (finmap_chain_dom _ _ _ HIn)).
Program Instance finmap_chainx_cauchy (σ : chain (K -f> V)) {σc : cchain σ} x (HIn : x dom (σ 1)) :
cchain (finmap_chainx σ x HIn).
cchain (finmap_chainx σ x HIn) | 5.
Next Obligation.
unfold cchain; intros.
assert (HT : Some (finmap_chainx σ x HIn i) = S n = Some (finmap_chainx σ x HIn j)); [| apply dist_mono, HT].
......@@ -562,7 +562,7 @@ Section FinDom.
Definition findom_lub (σ : chain (K -f> V)) (σc : cchain σ) : K -f> V :=
findom_map _ _ (σ 1) (fun x HLu => compl (finmap_chainx σ x (proj1 (In_inlst _ _) HLu))).
Global Program Instance findom_cmetric : cmetric (K -f> V) := mkCMetr findom_lub.
Global Program Instance findom_cmetric : cmetric (K -f> V) | 5 := mkCMetr findom_lub.
Next Obligation.
intros [| n]; [exists 0; intros; exact I |].
assert (HT : exists m, forall x, inlst x (dom (σ 1)) = true -> forall (X : inlst x (dom (σ 1)) = true) i,
......
......@@ -58,7 +58,7 @@ Section PUMMorphProps1.
Definition PMEquiv (x y : T -m> U) := mu_morph x == mu_morph y.
Global Program Instance PMtypeM : Setoid (T -m> U) := mkType PMEquiv.
Global Program Instance PMtypeM : Setoid (T -m> U) | 5 := mkType PMEquiv.
Next Obligation.
split.
- intros f x; simpl; reflexivity.
......@@ -68,7 +68,7 @@ Section PUMMorphProps1.
Definition PMDist n (f g : T -m> U) := (mu_morph f) = n = (mu_morph g).
Global Program Instance PMMetric : metric (T -m> U) := mkMetr PMDist.
Global Program Instance PMMetric : metric (T -m> U) | 5 := mkMetr PMDist.
Next Obligation.
intros f g EQfg h i EQhi; split; intros EQ x; [symmetry in EQfg, EQhi |]; rewrite (EQfg x), (EQhi x); apply EQ.
Qed.
......@@ -126,7 +126,7 @@ Section PUMMorphProps1.
rewrite HSub; reflexivity.
Qed.
Global Program Instance PMcmetric : cmetric (T -m> U) :=
Global Program Instance PMcmetric : cmetric (T -m> U) | 5 :=
mkCMetr PMCompl.
Next Obligation.
apply (conv_cauchy (liftc mu_morph_ne σ)).
......
......@@ -4,6 +4,7 @@ Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst.
Require Import ModuRes.Finmap ModuRes.Constr.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
(* This interface keeps some of the details of the solution opaque *)
Module Type WORLD_PROP (Res : PCM_T).
(* PreProp: The solution to the recursive equation. Equipped with a discrete order *)
......@@ -15,17 +16,18 @@ Module Type WORLD_PROP (Res : PCM_T).
(* Defines Worlds, Propositions *)
Definition Wld := nat -f> PreProp.
Definition Props := Wld -m> UPred Res.res.
(* Define all the things on Props, so they have names - this shortens the terms later *)
Instance Props_ty : Setoid Props := _.
Instance Props_m : metric Props := _.
Instance Props_cm : cmetric Props := _.
Instance Props_preo : preoType Props := _.
Instance Props_pcm : pcmType Props := _.
Instance Props_ty : Setoid Props | 1 := _.
Instance Props_m : metric Props | 1 := _.
Instance Props_cm : cmetric Props | 1 := _.
Instance Props_preo : preoType Props| 1 := _.
Instance Props_pcm : pcmType Props | 1 := _.
(* Establish the recursion isomorphism *)
Parameter ı : PreProp -t> halve (cmfromType Props).
Parameter ı' : halve (cmfromType Props) -t> PreProp.
Parameter ı : PreProp -n> halve (cmfromType Props).
Parameter ı' : halve (cmfromType Props) -n> PreProp.
Axiom iso : forall P, ı' (ı P) == P.
Axiom isoR: forall T, ı (ı' T) == T.
End WORLD_PROP.
......
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