world_prop.v 4.39 KB
 Filip Sieczkowski committed May 28, 2014 1 2 ``````(** In this file, we show how we can use the solution of the recursive domain equations to build a higher-order separation logic *) `````` Filip Sieczkowski committed Oct 07, 2014 3 4 ``````Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst. Require Import ModuRes.Finmap ModuRes.Constr. `````` Ralf Jung committed Feb 14, 2015 5 ``````Require Import ModuRes.PCM ModuRes.UPred. `````` Ralf Jung committed Feb 09, 2015 6 `````` `````` Ralf Jung committed Feb 01, 2015 7 8 ``````(* This interface keeps some of the details of the solution opaque *) Module Type WORLD_PROP (Res : PCM_T). `````` Ralf Jung committed Feb 09, 2015 9 `````` (* PreProp: The solution to the recursive equation. Equipped with a discrete order. *) `````` Ralf Jung committed Feb 01, 2015 10 `````` Parameter PreProp : cmtyp. `````` Ralf Jung committed Feb 09, 2015 11 12 13 `````` Instance PProp_preo : preoType PreProp := disc_preo PreProp. Instance PProp_pcm : pcmType PreProp := disc_pcm PreProp. Instance PProp_ext : extensible PreProp := disc_ext PreProp. `````` Ralf Jung committed Feb 01, 2015 14 15 16 17 `````` (* Defines Worlds, Propositions *) Definition Wld := nat -f> PreProp. Definition Props := Wld -m> UPred Res.res. `````` Ralf Jung committed Feb 09, 2015 18 `````` `````` Ralf Jung committed Feb 14, 2015 19 `````` (* Define all the things on Props, so they have names - this shortens the terms later. *) `````` Ralf Jung committed Feb 09, 2015 20 21 22 23 24 `````` 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 := _. `````` Ralf Jung committed Feb 01, 2015 25 26 `````` (* Establish the recursion isomorphism *) `````` Ralf Jung committed Feb 09, 2015 27 28 `````` Parameter ı : PreProp -n> halve (cmfromType Props). Parameter ı' : halve (cmfromType Props) -n> PreProp. `````` Ralf Jung committed Feb 01, 2015 29 30 31 32 `````` Axiom iso : forall P, ı' (ı P) == P. Axiom isoR: forall T, ı (ı' T) == T. End WORLD_PROP. `````` Ralf Jung committed Feb 09, 2015 33 `````` `````` Ralf Jung committed Feb 01, 2015 34 ``````(* Now we come to the actual implementation *) `````` Ralf Jung committed Feb 01, 2015 35 ``````Module WorldProp (Res : PCM_T) : WORLD_PROP Res. `````` Filip Sieczkowski committed May 28, 2014 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 `````` (** The construction is parametric in the monoid we choose *) Import Res. (** We need to build a functor that would describe the following recursive domain equation: Prop ≃ (Loc -f> Prop) -m> UPred (Res) As usual, we split the negative and (not actually occurring) positive occurrences of Prop. *) Section Definitions. (** We'll be working with complete metric spaces, so whenever something needs an additional preorder, we'll just take a discrete one. *) Local Instance pt_disc P `{cmetric P} : preoType P | 2000 := disc_preo P. Local Instance pcm_disc P `{cmetric P} : pcmType P | 2000 := disc_pcm P. Definition FProp P `{cmP : cmetric P} := `````` Filip Sieczkowski committed Jun 03, 2014 54 `````` (nat -f> P) -m> UPred res. `````` Filip Sieczkowski committed May 28, 2014 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 `````` Context {U V} `{cmU : cmetric U} `{cmV : cmetric V}. Definition PropMorph (m : V -n> U) : FProp U -n> FProp V := fdMap (disc_m m) ▹. End Definitions. Module F <: SimplInput (CBUlt). Import CBUlt. Open Scope cat_scope. Definition F (T1 T2 : cmtyp) := cmfromType (FProp T1). Program Instance FArr : BiFMap F := fun P1 P2 P3 P4 => n[(PropMorph)] F 1 1 := umconst (pcmconst (up_cr (const True))). End F. Module F_In := InputHalve(F). Module Import Fix := Solution(CBUlt)(F_In). (** Now we can name the two isomorphic spaces of propositions, and the space of worlds. We'll store the actual solutions in the worlds, and use the action of the FPropO on them as the space we normally work with. *) Definition PreProp := DInfO. Definition Props := FProp PreProp. Definition Wld := (nat -f> PreProp). `````` Ralf Jung committed Jan 31, 2015 99 100 101 102 `````` (* Define an order on PreProp. *) Instance PProp_preo: preoType PreProp := disc_preo PreProp. Instance PProp_pcm : pcmType PreProp := disc_pcm PreProp. Instance PProp_ext : extensible PreProp := disc_ext PreProp. `````` Filip Sieczkowski committed May 28, 2014 103 `````` `````` Ralf Jung committed Jan 31, 2015 104 105 106 107 108 109 110 `````` (* Give names to the things for Props, so the terms can get shorter. *) 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 := _. `````` Ralf Jung committed Feb 02, 2015 111 112 113 114 115 116 117 118 119 `````` (* Establish the isomorphism *) Definition ı : PreProp -t> halve (cmfromType Props) := Unfold. Definition ı' : halve (cmfromType Props) -t> PreProp := Fold. Lemma iso P : ı' (ı P) == P. Proof. apply (FU_id P). Qed. Lemma isoR T : ı (ı' T) == T. Proof. apply (UF_id T). Qed. `````` Filip Sieczkowski committed May 28, 2014 120 ``End WorldProp.``