clutch.meas_lang.lang

(* From HB Require Import structures. *)
(* From Stdlib Require Import Logic.ClassicalEpsilon Psatz. *)
(* From stdpp Require Import base numbers binders strings gmap. *)
(* From mathcomp Require Import reals. *)
(* From mathcomp.analysis Require Import measure lebesgue_measure. *)
(* From mathcomp Require Import ssrbool all_algebra eqtype choice boolp fintype. *)
(* From iris.algebra Require Export ofe. *)
(* From clutch.prelude Require Export stdpp_ext. *)
(* From clutch.common Require Export locations. *)
(* From clutch.meas_lang Require Import ectxi_language ectx_language. *)

(* From Stdlib Require Export Reals. *)
(* From clutch.prob.monad Require Export laws. *)
(* From mathcomp.analysis Require Export Rstruct. *)

(* From mathcomp Require Import classical_sets. *)

(* Fix giryM to be the giry type with stdlib-valued real numbers *)
(* Notation giryM := (giryM (R := R)). *)

(* (* *)
(* From Stdlib Require Import Reals Psatz. *)
(* From stdpp Require Export binders strings. *)
(* From stdpp Require Import fin. *)
(* From stdpp Require Import gmap fin_maps countable fin. *)
(* From clutch.prob Require Export distribution. *)
(* From clutch.common Require Export language ectx_language ectxi_language locations. *)
(* From iris.prelude Require Import options. *)
(* From mathcomp Require Import ssrbool eqtype fintype choice all_algebra finmap. *)
(* From mathcomp Require Import mathcomp_extra boolp classical_sets functions. *)
(* From mathcomp Require Import cardinality fsbigop. *)
(* From mathcomp.analysis Require Import reals ereal signed normedtype sequences esum numfun measure lebesgue_measure lebesgue_integral. *)
(* *) *)

(* Delimit Scope expr_scope with E. *)
(* Delimit Scope val_scope with V. *)

(* Global Instance classical_eq_dec {T : Type} : EqDecision T. *)
(* Proof.  intros ? ?; apply ClassicalEpsilon.excluded_middle_informative. Defined. *)

(* (* Instances for Z *) *)
(* HB.instance Definition _ := gen_eqMixin Z. *)
(* HB.instance Definition _ := gen_choiceMixin Z. *)
(* HB.instance Definition _ := isPointed.Build Z inhabitant. *)

(* (* Instances for loc *) *)
(* HB.instance Definition _ := gen_eqMixin loc. *)
(* HB.instance Definition _ := gen_choiceMixin loc. *)
(* HB.instance Definition _ := isPointed.Build loc inhabitant. *)

(* Module meas_lang. *)

(* (* Type of base_lit, parameterized by leaf types *) *)
(* Inductive base_lit_pre {TZ TB TL TR : Type} : Type := *)
(*   | LitInt  (n : TZ) *)
(*   | LitBool (b : TB) *)
(*   | LitUnit *)
(*   | LitLoc  (l : TL) *)
(*   | LitLbl  (l : TL) *)
(*   | LitReal (r : TR). *)

(* Inductive un_op : Set := *)
(*   | NegOp | MinusUnOp. *)

(* Inductive bin_op : Set := *)
(*   | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *) *)
(*   | AndOp | OrOp | XorOp (* Bitwise *) *)
(*   | ShiftLOp | ShiftROp (* Shifts *) *)
(*   | LeOp | LtOp | EqOp (* Relations *) *)
(*   | OffsetOp. (* Pointer offset *) *)

(* Inductive expr_pre {TZ TB TL TR : Type} := *)
(*   (* Values *) *)
(*   | Val (v : val_pre) *)
(*   (* Base lambda calculus *) *)
(*   | Var (x : string) *)
(*   | Rec (f x : binder) (e : expr_pre) *)
(*   | App (e1 e2 : expr_pre) *)
(*   (* Base types and their operations *) *)
(*   | UnOp (op : un_op) (e : expr_pre) *)
(*   | BinOp (op : bin_op) (e1 e2 : expr_pre) *)
(*   | If (e0 e1 e2 : expr_pre) *)
(*   (* Products *) *)
(*   | Pair (e1 e2 : expr_pre) *)
(*   | Fst (e : expr_pre) *)
(*   | Snd (e : expr_pre) *)
(*   (* Sums *) *)
(*   | InjL (e : expr_pre) *)
(*   | InjR (e : expr_pre) *)
(*   | Case (e0 e1 e2 : expr_pre) *)
(*   (* Heap *) *)
(*   | AllocN (e1 e2 : expr_pre) (* Array length and initial value *) *)
(*   | Load (e : expr_pre) *)
(*   | Store (e1 e2 : expr_pre) *)
(*   (* Finite probabilistic choice *) *)
(*   | AllocTape (e : expr_pre) *)
(*   | Rand (e1 e2 : expr_pre) *)
(*   (* Real probabilistic choice *) *)
(*   | AllocUTape *)
(*   | URand (e : expr_pre) *)
(*   (* No-op operator used for cost *) *)
(*   | Tick (e : expr_pre ) *)
(* with val_pre {TZ TB TL TR : Type} := *)
(*   | LitV (l : @base_lit_pre TZ TB TL TR) *)
(*   | RecV (f x : binder) (e : expr_pre) *)
(*   | PairV (v1 v2 : val_pre) *)
(*   | InjLV (v : val_pre) *)
(*   | InjRV (v : val_pre). *)

(* Section expr_algebra. *)
(*   (** Defines the sigma algebra over expressions *) *)
(*   Local Open Scope classical_set_scope. *)

(*   (* FIXME: move *) *)
(*   Definition image3 {TA TB TC rT} (A : set TA) (B : set TB) (C : set TC) (f : TA -> TB -> TC -> rT) := *)
(*     set z | exists2 x, A x & exists2 y, B y & exists2 w, C w & f x y w = z. *)
(*   Arguments image3 _ _ _ _ _ _ _ _ /. *)

(*   Definition TZ : measurableType default_measure_display := <<discr Z>>. *)
(*   Definition TB : measurableType default_measure_display := <<discr bool>>. *)
(*   Definition TL : measurableType default_measure_display := <<discr loc>>. *)
(*   Definition TR : measurableType default_measure_display := (R : realType). *)

(*   Definition base_lit_S : Type := @base_lit_pre (set TZ) (set TB) (set TL) (set TR). *)
(*   Definition val_S      : Type := @val_pre      (set TZ) (set TB) (set TL) (set TR). *)
(*   Definition expr_S     : Type := @expr_pre     (set TZ) (set TB) (set TL) (set TR). *)

(*   Definition base_lit_T : Type := @base_lit_pre TZ TB TL TR. *)
(*   Definition val_T      : Type := @val_pre      TZ TB TL TR. *)
(*   Definition expr_T     : Type := @expr_pre     TZ TB TL TR. *)

(*   (* Cylinder constructions *) *)

(*   (* Trees with sets on their leaves -> sets of trees with values on their leaves *) *)
(*   Definition base_lit_ST (b : base_lit_S) : set base_lit_T := *)
(*     match b with *)
(*     | LitInt  s => image s LitInt *)
(*     | LitBool s => image s LitBool *)
(*     | LitUnit   => set LitUnit *)
(*     | LitLoc  s => image s LitLoc *)
(*     | LitLbl  s => image s LitLbl *)
(*     | LitReal s => image s LitReal *)
(*     end. *)

(*   Fixpoint expr_ST (e : expr_S) : set expr_T := *)
(*     match e with *)
(*     | Val v          => image (val_ST v) Val *)
(*     | Var x          => set (Var x) *)
(*     | Rec f x e      => image  (expr_ST e)   (Rec f x) *)
(*     | App e1 e2      => image2 (expr_ST e1) (expr_ST e2) App *)
(*     | UnOp op e      => image  (expr_ST e)  (UnOp op) *)
(*     | BinOp op e1 e2 => image2 (expr_ST e1) (expr_ST e2) (BinOp op) *)
(*     | If e0 e1 e2    => image3 (expr_ST e0) (expr_ST e1) (expr_ST e2) If *)
(*     | Pair e1 e2     => image2 (expr_ST e1) (expr_ST e2) Pair *)
(*     | Fst e1         => image  (expr_ST e1) Fst *)
(*     | Snd e1         => image  (expr_ST e1) Snd *)
(*     | InjL e1        => image  (expr_ST e1) InjL *)
(*     | InjR e1        => image  (expr_ST e1) InjR *)
(*     | Case e0 e1 e2  => image3 (expr_ST e0) (expr_ST e1) (expr_ST e2) Case *)
(*     | AllocN e1 e2   => image2 (expr_ST e1) (expr_ST e2) AllocN *)
(*     | Load e         => image  (expr_ST e)  Load *)
(*     | Store e1 e2    => image2 (expr_ST e1) (expr_ST e2) Store *)
(*     | AllocTape e    => image  (expr_ST e)  AllocTape *)
(*     | Rand e1 e2     => image2 (expr_ST e1) (expr_ST e2) Rand *)
(*     | AllocUTape     => set AllocUTape *)
(*     | URand e        => image  (expr_ST e)  URand *)
(*     | Tick e         => image  (expr_ST e)  Tick *)
(*     end *)
(*     with *)
(*       val_ST (v : val_S) : set val_T := *)
(*       match v with *)
(*       | LitV b       => image  (base_lit_ST b) LitV *)
(*       | RecV f x e   => image  (expr_ST e) (RecV f x) *)
(*       | PairV v1 v2  => image2 (val_ST v1) (val_ST v2) PairV *)
(*       | InjLV v      => image  (val_ST v) InjLV *)
(*       | InjRV v      => image  (val_ST v) InjRV *)
(*       end. *)

(*   (* All trees with measurable sets on their leaves *) *)
(*   Definition base_lit_ML : set base_lit_S := *)
(*     fun b => *)
(*       match b with *)
(*       | LitInt  s => measurable s *)
(*       | LitBool s => measurable s *)
(*       | LitUnit   => True *)
(*       | LitLoc  s => measurable s *)
(*       | LitLbl  s => measurable s *)
(*       | LitReal s => measurable s *)
(*       end. *)

(*   Fixpoint expr_ML (e : expr_S) : Prop := *)
(*     match e with *)
(*     | Val v          => val_ML v *)
(*     | Var x          => True *)
(*     | Rec f x e      => expr_ML e *)
(*     | App e1 e2      => expr_ML e1 /\ expr_ML e2 *)
(*     | UnOp op e      => expr_ML e *)
(*     | BinOp op e1 e2 => expr_ML e1 /\ expr_ML e2 *)
(*     | If e0 e1 e2    => expr_ML e0 /\ expr_ML e1 /\ expr_ML e2 *)
(*     | Pair e1 e2     => expr_ML e1 /\ expr_ML e2 *)
(*     | Fst e1         => expr_ML e1 *)
(*     | Snd e1         => expr_ML e1 *)
(*     | InjL e1        => expr_ML e1 *)
(*     | InjR e1        => expr_ML e1 *)
(*     | Case e0 e1 e2  => expr_ML e0 /\ expr_ML e1 /\ expr_ML e2 *)
(*     | AllocN e1 e2   => expr_ML e1 /\ expr_ML e2 *)
(*     | Load e         => expr_ML e *)
(*     | Store e1 e2    => expr_ML e1 /\ expr_ML e2 *)
(*     | AllocTape e    => expr_ML e *)
(*     | Rand e1 e2     => expr_ML e1 /\ expr_ML e2 *)
(*     | AllocUTape     => True *)
(*     | URand e        => expr_ML e *)
(*     | Tick e         => expr_ML e *)
(*     end *)
(*   with *)
(*     val_ML (v : val_S) : Prop := *)
(*       match v with *)
(*       | LitV b       => base_lit_ML b *)
(*       | RecV f x e   => expr_ML e *)
(*       | PairV v1 v2  => val_ML v1 /\ val_ML v2 *)
(*       | InjLV v      => val_ML v *)
(*       | InjRV v      => val_ML v *)
(*       end. *)

(*   (* Cylinders: Generators for the sigma algebra *) *)
(*   Definition base_lit_cyl : set (set base_lit_T) := image base_lit_ML base_lit_ST. *)
(*   Definition expr_cyl     : set (set expr_T)     := image expr_ML     expr_ST. *)
(*   Definition val_cyl      : set (set val_T)      := image val_ML      val_ST. *)

(*   (* Generate sigma algebras from the cylinders *) *)

(*   HB.instance Definition _ := gen_eqMixin base_lit_T. *)
(*   HB.instance Definition _ := gen_choiceMixin base_lit_T. *)
(*   HB.instance Definition _ := isPointed.Build base_lit_T LitUnit. *)

(*   HB.instance Definition _ := gen_eqMixin val_T. *)
(*   HB.instance Definition _ := gen_choiceMixin val_T. *)
(*   HB.instance Definition _ := isPointed.Build val_T (LitV LitUnit). *)

(*   HB.instance Definition _ := gen_eqMixin expr_T. *)
(*   HB.instance Definition _ := gen_choiceMixin expr_T. *)
(*   HB.instance Definition _ := isPointed.Build expr_T (Val (LitV LitUnit)). *)

(*   (* FIXME: Remove! *) *)
(*   Local Lemma base_lit_meas_obligation : *)
(*     ∀ A : set base_lit_T, <<s base_lit_cyl>> A → <<s base_lit_cyl >> (~` A). *)
(*   Proof. eapply sigma_algebraC. Qed. *)
(*   Local Lemma val_meas_obligation : *)
(*     ∀ A : set val_T, <<s val_cyl>> A → <<s val_cyl >> (~` A). *)
(*   Proof. eapply sigma_algebraC. Qed. *)
(*   Local Lemma expr_meas_obligation : *)
(*     ∀ A : set expr_T, <<s expr_cyl>> A → <<s expr_cyl >> (~` A). *)
(*   Proof. eapply sigma_algebraC. Qed. *)

(*   HB.instance Definition _ := @isMeasurable.Build *)
(*     (sigma_display base_lit_cyl) *)
(*     base_lit_T *)
(*     <<s base_lit_cyl>> *)
(*     (@sigma_algebra0 _ setT base_lit_cyl) *)
(*     base_lit_meas_obligation *)
(*     (@sigma_algebra_bigcup _ setT base_lit_cyl). *)

(*   HB.instance Definition _ := @isMeasurable.Build *)
(*     (sigma_display val_cyl) *)
(*     val_T *)
(*     <<s val_cyl>> *)
(*     (@sigma_algebra0 _ setT val_cyl) *)
(*     val_meas_obligation *)
(*     (@sigma_algebra_bigcup _ setT val_cyl). *)

(*   HB.instance Definition _ := @isMeasurable.Build *)
(*     (sigma_display expr_cyl) *)
(*     expr_T *)
(*     <<s expr_cyl>> *)
(*     (@sigma_algebra0 _ setT expr_cyl) *)
(*     expr_meas_obligation *)
(*     (@sigma_algebra_bigcup _ setT expr_cyl). *)

(*   (* User-facing types *) *)
(*   Definition base_lit : measurableType base_lit_cyl.-sigma := base_lit_T. *)
(*   Definition expr : measurableType expr_cyl.-sigma := expr_T. *)
(*   Definition val : measurableType val_cyl.-sigma := val_T. *)

(* End expr_algebra. *)

(* (**  General lemmas about tapes *) *)

(* Definition tape_content_t (A : Type) : Type := nat -> option A. *)

(* Record tape (A : Type) : Type := { *)
(*   tape_position : nat; *)
(*   tape_contents : tape_content_t A *)
(* }. *)

(* Definition emptyTapeContents {A : Type} : tape_content_t A := fun _ => None. *)

(* Definition emptyTape {A : Type} : tape A := *)
(*   {| tape_position := 0 ; *)
(*      tape_contents := emptyTapeContents *)
(*   |}. *)

(* (* History lookup: look through absolute history *) *)
(* Global Instance tape_content_lookup {A} : Lookup nat A (tape_content_t A) := fun i => fun h => h i. *)

(* (**  Specialize tapes to btapes and utapes, construct siga algebra *) *)
(* Section tapes_algebra. *)
(*   Local Open Scope classical_set_scope. *)

(*   (* Tapes in the computable fragment *) *)
(*   Record pre_btape : Type := { *)
(*       btape_tape :> tape nat; *)
(*       btape_bound : nat *)
(*   }. *)

(*   (* Tapes of real numbers *) *)
(*  Definition pre_utape : Type := tape R. *)

(*   (* FIXME: move *) *)
(*   Definition image4 {TA TB TC TD rT} (A : set TA) (B : set TB) (C : set TC) (D : set TD) (f : TA -> TB -> TC -> TD -> rT) := *)
(*     set z | exists2 x, A x & exists2 y, B y & exists2 w, C w & exists2 v, D v & f x y w v = z. *)
(*   Arguments image4 _ _ _ _ _ _ _ _ _ /. *)

(*   Definition btape_basis_emp : set (set pre_btape) := *)
(*     let bound_set : set nat := setT in *)
(*     let pos_set : set nat := setT in *)

(*     (* The set of all btapes such that *)
(*        - the bound is b *)
(*        - the position is p *)
(*        - the content is empty *) *)
(*     let construct b p := *)
(*       set {| btape_tape := {| tape_position := p; tape_contents := (fun _ => None) |} ; *)
(*               btape_bound := b |}] in *)
(*     image2 bound_set pos_set construct. *)

(*   Program Definition btape_basis_full : set (set pre_btape) := *)
(*     let bound_set : set nat := setT in *)
(*     let pos_set   : set nat := setT in *)
(*     let index_set : set nat := setT in *)
(*     let value_set : set nat := setT in *)

(*     (* The set of all btapes such that *)
(*        - the bound is b *)
(*        - the position is p *)
(*        - the content at index i is set to the value v *) *)
(*     let construct b p i v := *)
(*       (fun bt => *)
(*          exists contents, *)
(*            bt = {| btape_tape := {| tape_position := p; tape_contents := contents |}; btape_bound := b|} /\ *)
(*            contents !! i = Some v) in *)

(*     image4 bound_set pos_set index_set value_set construct. *)

(*   Definition btape_basis := btape_basis_emp `|` btape_basis_full. *)

(*   HB.instance Definition _ := gen_eqMixin pre_btape. *)
(*   HB.instance Definition _ := gen_choiceMixin pre_btape. *)
(*   HB.instance Definition _ := isPointed.Build pre_btape {| btape_tape := emptyTape ; btape_bound := 0 |}. *)

(*   Local Lemma btape_meas_obligation : ∀ A : set pre_btape, <<s btape_basis>> A → <<s btape_basis>> (~` A). *)
(*   Proof. eapply sigma_algebraC. Qed. *)

(*   HB.instance Definition _ := @isMeasurable.Build *)
(*     (sigma_display btape_basis) *)
(*     pre_btape *)
(*     <<s btape_basis>> *)
(*     (@sigma_algebra0 _ setT btape_basis) *)
(*     btape_meas_obligation *)
(*     (@sigma_algebra_bigcup _ setT btape_basis). *)

(*   Definition utape_basis_emp : set (set pre_utape) := *)
(*     let pos_set : set nat := setT in *)

(*     (* The set of all utapes such that *)
(*        - the position is p *)
(*        - the content is empty *) *)
(*     let construct p := *)
(*       set {| tape_position := p; tape_contents := (fun _ => None) |} in *)
(*     image pos_set construct. *)

(*   (* FIXME: This should not return a singleton! *) *)
(*   Definition utape_basis_full : set (set pre_utape) := *)
(*     let pos_set   : set nat := setT in *)
(*     let index_set : set nat := setT in *)
(*     let value_set : set (set (R : realType)) := 'measurable in *)

(*     (* The set of all utapes such that *)
(*        - the position is p *)
(*        - the content at position i is set to some value in set_of_v *) *)
(*     let construct p i set_of_v := *)
(*         (fun ut => *)
(*            exists contents r, *)
(*              ut = {| tape_position := p; tape_contents := contents |} /\ *)
(*              contents !! i = Some r /\ *)
(*              set_of_v r) in *)
(*     image3 pos_set index_set value_set construct. *)

(*   Definition utape_basis : set (set pre_utape) := utape_basis_emp `|` utape_basis_full. *)

(*   HB.instance Definition _ := gen_eqMixin pre_utape. *)
(*   HB.instance Definition _ := gen_choiceMixin pre_utape. *)
(*   HB.instance Definition _ := isPointed.Build pre_utape emptyTape. *)

(*   Local Lemma utape_meas_obligation : ∀ A : set pre_utape, <<s utape_basis>> A → <<s utape_basis>> (~` A). *)
(*   Proof. eapply sigma_algebraC. Qed. *)

(*   HB.instance Definition _ := @isMeasurable.Build *)
(*     (sigma_display utape_basis) *)
(*     pre_utape *)
(*     <<s utape_basis>> *)
(*     (@sigma_algebra0 _ setT utape_basis) *)
(*     utape_meas_obligation *)
(*     (@sigma_algebra_bigcup _ setT utape_basis). *)

(*   (* User-facing types *) *)
(*   Definition btape : measurableType btape_basis.-sigma := pre_btape. *)
(*   Definition utape : measurableType utape_basis.-sigma := pre_utape. *)

(* End tapes_algebra. *)

(* (* btape and utape definitions *) *)

(* (* All values of the tape are within the tape bound *) *)
(* Definition btape_inbounds (t : btape): Prop := *)
(*   forall n : nat, *)
(*     tape_contents _ t n = None \/ *)
(*     exists v : nat, tape_contents _ t n = Some v /\ v < btape_bound t. *)

(* (* All tape values prior to state have been determined *) *)
(* Definition tape_history_deterministic {A} (t : tape A) : Prop := *)
(*   forall i : nat, i < tape_position _ t -> exists v : A, tape_contents _ t i = Some v. *)

(* (* Tape lookup: look relative to current index. t !! 0  will be the next sample. *) *)
(* Global Instance tape_rel_lookup {A} : Lookup nat A (tape A) := fun i => fun t => (tape_contents _ t (i + tape_position _ t)). *)

(* Definition tape_content_update_unsafe {A} (i : nat) (v : option A) (h : tape_content_t A) : tape_content_t A *)
(*   := fun i' => if i' =? i then v else h i'. *)

(* Global Instance tape_content_insert {A} : Insert nat (option A) (tape_content_t A) := tape_content_update_unsafe. *)

(* Definition tapeUpdateUnsafe {A} (i : nat) (v : option A) (t : tape A) : tape A := *)
(*   {| tape_position := tape_position _ t; *)
(*      tape_contents := < (i + tape_position _ t) := v > (tape_contents _ t) *)
(*   |}. *)

(* Global Instance tape_insert {A} : Insert nat (option A) (tape A) := tapeUpdateUnsafe. *)

(* Program Definition tapeAdvance {A} (t : tape A) : tape A *)
(*   := {| tape_position := 1 + tape_position _ t; tape_contents := tape_contents _ t |}. *)

(* (* Advance the tape by 1, returning an updated tape and the first sample on the tape. *) *)
(* Program Definition tapeNext {A} (t : tape A) (H : isSome (t !! 0)) : A * (tape A) *)
(*   := match (t !! 0) with *)
(*      | None => _ *)
(*      | Some v => *)
(*          (v, *)
(*           {| tape_position := 1 + tape_position _ t; *)
(*              tape_contents := tape_contents _ t |}) *)
(*      end. *)
(* Next Obligation. by move=>/= ? ? H1 H2; symmetry in H2; rewrite H2//= in H1. Defined. *)

(* (* Representation predicates for common tape structures *) *)

(* Definition tapeHasPrefix {A} (t : tape A) (l : list A) : Prop *)
(*   := forall i : nat, i < length l -> t !! i = l !! i. *)

(* Definition tapeEmptyAfter {A} (t : tape A) (b : nat) : Prop *)
(*   := forall i : nat, i >= b -> t !! i = None. *)

(* (* Tapes a la base clutch *) *)
(* Definition isFiniteTape (t : btape) (l : list nat) : Prop *)
(*   :=   tapeHasPrefix t l *)
(*      /\ tapeEmptyAfter t (length l) *)
(*      /\ btape_inbounds t *)
(*      /\ tape_history_deterministic t. *)

(* (* TODO: realIsBinarySequence (cannonical form w/ 0-termination on dyadic numbers) *) *)

(* Definition tapeHasInfinitePrefix {A} (t : tape A) (f : nat -> A) : Prop *)
(*   := forall i : nat, t !! i = Some (f i). *)

(* (* TODO: tapeIsRealInRange (l : R) ... := bound = 1, tapeHasInfinitePrefic *) *)
(* (* tapeOfReal ... ?*) *)

(* (* Tape with "Junk" prefix *) *)
(* Definition tapeHasEventually {A} (t : tape A) (l : list A) : Prop *)
(*   := exists offset: nat, forall i : nat, i < length l -> t !! (i + offset) = l !! i. *)

(* Global Instance tape_inhabited {A} : Inhabited (tape A) := populate emptyTape. *)
(* Global Instance tapes_lookup_total {A} : LookupTotal loc (tape A) (gmap loc (tape A)). *)
(* Proof. apply map_lookup_total. Defined. *)
(* Global Instance tapes_insert {A} : Insert loc (tape A) (gmap loc (tape A)). *)
(* Proof. apply map_insert. Defined. *)

(* Bind Scope expr_scope with expr. *)
(* Bind Scope val_scope with val. *)

(* Notation of_val := Val (only parsing). *)

(* Definition to_val (e : expr) : option val := *)
(*   match e with *)
(*   | Val v => Some v *)
(*   | _ => None *)
(*   end. *)

(* Section state_algebra. *)

(*   Local Open Scope classical_set_scope. *)

(*   (** The state: a loc-indexed heap of vals, and loc-indexed tapes, and loc-indexed utapes *) *)
(*   Record state_pre : Type := { *)
(*     heap   : gmap loc val; *)
(*     tapes  : gmap loc btape; *)
(*     utapes : gmap loc utape *)
(*   }. *)

(*   Definition gmap_loc_cyl_emp d (T : measurableType d) : set (set (gmap loc T)) := *)
(*     set (fun g => forall l, g !! l = None). *)

(*   Definition gmap_loc_cyl_full d (T : measurableType d) : set (set (gmap loc T)) := *)
(*     let loc_set   : set loc := setT in *)
(*     let T_set     : set (set T) := d.-measurable in *)

(*     (* The set of all gmaps such that *)
(*         - the value at position l is set to an element in the set ts *) *)
(*     let construct (l : loc) (ts : set T) : set (gmap loc T) := *)
(*       fun g => exists v : T, g !! l = Some v /\ ts v in *)
(*     image2 loc_set T_set construct. *)

(*   Definition gmap_loc_cyl d (T : measurableType d) : set (set (gmap loc T)) := *)
(*     gmap_loc_cyl_emp d T `|` gmap_loc_cyl_full d T. *)

(*   (* The set of all states such that *)
(*      each field is a gmap cylinder *)
(*    *) *)
(*   Program Definition state_cyl : set (set state_pre) := *)
(*     let hs_set := gmap_loc_cyl _ val in *)
(*     let ts_set := gmap_loc_cyl _ btape in *)
(*     let us_set := gmap_loc_cyl _ utape in *)
(*     let construct (hs : set (gmap loc val)) (ht : set (gmap loc btape)) (hu : set (gmap loc utape)) : set state_pre := *)
(*       fun σ => *)
(*         exists g1 : gmap loc val, *)
(*         exists g2 : gmap loc btape, *)
(*         exists g3 : gmap loc utape, *)
(*         σ = {| heap := g1; tapes := g2; utapes := g3|} /\ *)
(*         hs g1 /\ *)
(*         ht g2 /\ *)
(*         hu g3 *)
(*       in *)
(*     image3 hs_set ts_set us_set construct. *)

(*   HB.instance Definition _ := gen_eqMixin state_pre. *)
(*   HB.instance Definition _ := gen_choiceMixin state_pre. *)
(*   HB.instance Definition _ := isPointed.Build state_pre {| heap := gmap_empty; tapes := gmap_empty; utapes := gmap_empty |}. *)

(*   Local Lemma state_pre_meas_obligation : ∀ A : set state_pre, <<s state_cyl>> A → <<s state_cyl>> (~` A). *)
(*   Proof. eapply sigma_algebraC. Qed. *)

(*   (* There's got to be a way to delete this *) *)
(*   HB.instance Definition _ := @isMeasurable.Build *)
(*     (sigma_display state_cyl) *)
(*     state_pre *)
(*     <<s state_cyl>> *)
(*     (@sigma_algebra0 _ setT state_cyl) *)
(*     state_pre_meas_obligation *)
(*     (@sigma_algebra_bigcup _ setT state_cyl). *)

(*   Definition state : measurableType state_cyl.-sigma := state_pre. *)

(* End state_algebra. *)

(* (** Equality and other typeclass stuff *) *)
(* Lemma to_of_val v : to_val (of_val v) = Some v. *)
(* Proof. by destruct v. Qed. *)

(* Lemma of_to_val e v : to_val e = Some v → of_val v = e. *)
(* Proof. destruct e=>//=. by intros = <-. Qed. *)

(* (* FIXME *)
(* Global Instance of_val_inj : Inj (=) (=) of_val. *)
(* Proof. intros ??. congruence. Qed. *)
(* *) *)

(* (* *)
(* Global Instance state_inhabited : Inhabited state := populate {| heap := gmap_empty; tapes := gmap_empty; utapes := gmap_empty |}. *)
(* Global Instance val_inhabited : Inhabited val := populate (LitV LitUnit). *)
(* Global Instance expr_inhabited : Inhabited expr := populate (Val inhabitant). *)
(* *) *)

(* Canonical Structure stateO := leibnizO state. *)
(* Canonical Structure locO := leibnizO loc. *)
(* Canonical Structure valO := leibnizO val. *)
(* Canonical Structure exprO := leibnizO expr. *)

(* (** Evaluation contexts *) *)
(* Inductive ectx_item := *)
(*   | AppLCtx (v2 : val) *)
(*   | AppRCtx (e1 : expr) *)
(*   | UnOpCtx (op : un_op) *)
(*   | BinOpLCtx (op : bin_op) (v2 : val) *)
(*   | BinOpRCtx (op : bin_op) (e1 : expr) *)
(*   | IfCtx (e1 e2 : expr) *)
(*   | PairLCtx (v2 : val) *)
(*   | PairRCtx (e1 : expr) *)
(*   | FstCtx *)
(*   | SndCtx *)
(*   | InjLCtx *)
(*   | InjRCtx *)
(*   | CaseCtx (e1 : expr) (e2 : expr) *)
(*   | AllocNLCtx (v2 : val) *)
(*   | AllocNRCtx (e1 : expr) *)
(*   | LoadCtx *)
(*   | StoreLCtx (v2 : val) *)
(*   | StoreRCtx (e1 : expr) *)
(*   | AllocTapeCtx *)
(*   | RandLCtx (v2 : val) *)
(*   | RandRCtx (e1 : expr) *)
(*   | URandCtx *)
(*   | TickCtx. *)

(* (* FIXME: Hide cosntructors, so that we don't need to mention base_lit *) *)

(* (* *)
(* Definition fill_item (Ki : ectx_item) (e : expr) : expr := *)
(*   match Ki with *)
(*   | AppLCtx v2 => App e (of_val v2) *)
(*   | AppRCtx e1 => App e1 e *)
(*   | UnOpCtx op => UnOp op e *)
(*   | BinOpLCtx op v2 => BinOp op e (Val v2) *)
(*   | BinOpRCtx op e1 => BinOp op e1 e *)
(*   | IfCtx e1 e2 => If e e1 e2 *)
(*   | PairLCtx v2 => Pair e (Val v2) *)
(*   | PairRCtx e1 => Pair e1 e *)
(*   | FstCtx => Fst e *)
(*   | SndCtx => Snd e *)
(*   | InjLCtx => InjL e *)
(*   | InjRCtx => InjR e *)
(*   | CaseCtx e1 e2 => Case e e1 e2 *)
(*   | AllocNLCtx v2 => AllocN e (Val v2) *)
(*   | AllocNRCtx e1 => AllocN e1 e *)
(*   | LoadCtx => Load e *)
(*   | StoreLCtx v2 => Store e (Val v2) *)
(*   | StoreRCtx e1 => Store e1 e *)
(*   | AllocTapeCtx => AllocTape e *)
(*   | RandLCtx v2 => Rand e (Val v2) *)
(*   | RandRCtx e1 => Rand e1 e *)
(*   | URandCtx => URand e *)
(*   | TickCtx => Tick e *)
(*   end. *)

(* Definition decomp_item (e : expr) : option (ectx_item * expr) := *)
(*   let noval (e : expr) (ei : ectx_item) := *)
(*     match e with Val _ => None | _ => Some (ei, e) end in *)
(*   match e with *)
(*   | App e1 e2      => *)
(*       match e2 with *)
(*       | (Val v)    => noval e1 (AppLCtx v) *)
(*       | _          => Some (AppRCtx e1, e2) *)
(*       end *)
(*   | UnOp op e      => noval e (UnOpCtx op) *)
(*   | BinOp op e1 e2 => *)
(*       match e2 with *)
(*       | Val v      => noval e1 (BinOpLCtx op v) *)
(*       | _          => Some (BinOpRCtx op e1, e2) *)
(*       end *)
(*   | If e0 e1 e2    => noval e0 (IfCtx e1 e2) *)
(*   | Pair e1 e2     => *)
(*       match e2 with *)
(*       | Val v      => noval e1 (PairLCtx v) *)
(*       | _          => Some (PairRCtx e1, e2) *)
(*       end *)
(*   | Fst e          => noval e FstCtx *)
(*   | Snd e          => noval e SndCtx *)
(*   | InjL e         => noval e InjLCtx *)
(*   | InjR e         => noval e InjRCtx *)
(*   | Case e0 e1 e2  => noval e0 (CaseCtx e1 e2) *)
(*   | AllocN e1 e2        => *)
(*       match e2 with *)
(*       | Val v      => noval e1 (AllocNLCtx v) *)
(*       | _          => Some (AllocNRCtx e1, e2) *)
(*       end *)

(*   | Load e         => noval e LoadCtx *)
(*   | Store e1 e2    => *)
(*       match e2 with *)
(*       | Val v      => noval e1 (StoreLCtx v) *)
(*       | _          => Some (StoreRCtx e1, e2) *)
(*       end *)
(*   | AllocTape e    => noval e AllocTapeCtx *)
(*   | Rand e1 e2     => *)
(*       match e2 with *)
(*       | Val v      => noval e1 (RandLCtx v) *)
(*       | _          => Some (RandRCtx e1, e2) *)
(*       end *)
(*   | URand e        => noval e URandCtx *)
(*   | Tick e         => noval e TickCtx *)
(*   | _              => None *)
(*   end. *)

(* (** Substitution *) *)
(* Fixpoint subst (x : string) (v : val) (e : expr)  : expr := *)
(*   match e with *)
(*   | Val _ => e *)
(*   | Var y => if decide (x = y) then Val v else Var y *)
(*   | Rec f y e => *)
(*      Rec f y *)
(*   | App e1 e2 => App (subst x v e1) (subst x v e2) *)
(*   | UnOp op e => UnOp op (subst x v e) *)
(*   | BinOp op e1 e2 => BinOp op (subst x v e1) (subst x v e2) *)
(*   | If e0 e1 e2 => If (subst x v e0) (subst x v e1) (subst x v e2) *)
(*   | Pair e1 e2 => Pair (subst x v e1) (subst x v e2) *)
(*   | Fst e => Fst (subst x v e) *)
(*   | Snd e => Snd (subst x v e) *)
(*   | InjL e => InjL (subst x v e) *)
(*   | InjR e => InjR (subst x v e) *)
(*   | Case e0 e1 e2 => Case (subst x v e0) (subst x v e1) (subst x v e2) *)
(*   | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2) *)
(*   | Load e => Load (subst x v e) *)
(*   | Store e1 e2 => Store (subst x v e1) (subst x v e2) *)
(*   | AllocTape e => AllocTape (subst x v e) *)
(*   | AllocUTape => AllocUTape *)
(*   | Rand e1 e2 => Rand (subst x v e1) (subst x v e2) *)
(*   | URand e => URand (subst x v e) *)
(*   | Tick e => Tick (subst x v e) *)
(*   end. *)

(* Definition subst' (mx : binder) (v : val) : expr → expr := *)
(*   match mx with BNamed x => subst x v | BAnon => λ x, x end. *)

(* (** The stepping relation *) *)
(* Definition un_op_eval (op : un_op) (v : val) : option val := *)
(*   match op, v with *)
(*   | NegOp, LitV (LitBool b) => Some  LitBool (negb b) *)
(*   | NegOp, LitV (LitInt z) => Some  LitInt (Z.lnot z) *)
(*   | MinusUnOp, LitV (LitInt z) => Some  LitInt (- z) *)
(*   | MinusUnOp, LitV (LitReal r) => Some  LitReal (- r)*)
(*   | _, _ => None *)
(*   end. *)


(* Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : base_lit := *)
(*   match op with *)
(*   | PlusOp => LitInt (n1 + n2) *)
(*   | MinusOp => LitInt (n1 - n2) *)
(*   | MultOp => LitInt (n1 * n2) *)
(*   | QuotOp => LitInt (n1 `quot` n2) *)
(*   | RemOp => LitInt (n1 `rem` n2) *)
(*   | AndOp => LitInt (Z.land n1 n2) *)
(*   | OrOp => LitInt (Z.lor n1 n2) *)
(*   | XorOp => LitInt (Z.lxor n1 n2) *)
(*   | ShiftLOp => LitInt (n1 ≪ n2) *)
(*   | ShiftROp => LitInt (n1 ≫ n2) *)
(*   | LeOp => LitBool (bool_decide (n1 ≤ n2)) *)
(*   | LtOp => LitBool (bool_decide (n1 < n2)) *)
(*   | EqOp => LitBool (bool_decide (n1 = n2)) *)
(*   | OffsetOp => LitInt (n1 + n2) (* Treat offsets as ints *) *)
(*   end*)


(* Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit := *)
(*   match op with *)
(*   | PlusOp | MinusOp | MultOp | QuotOp | RemOp => None (* Arithmetic *) *)
(*   | AndOp => Some (LitBool (b1 && b2)) *)
(*   | OrOp => Some (LitBool (b1 || b2)) *)
(*   | XorOp => Some (LitBool (xorb b1 b2)) *)
(*   | ShiftLOp | ShiftROp => None (* Shifts *) *)
(*   | LeOp | LtOp => None (* InEquality *) *)
(*   | EqOp => Some (LitBool (bool_decide (b1 = b2))) *)
(*   | OffsetOp => None *)
(*   end. *)

(* Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit := *)
(*   match op, v2 with *)
(*   | OffsetOp, LitInt off => Some *)
(*   | LeOp, LitLoc l2 => Some *)
(*   | LtOp, LitLoc l2 => Some *)
(*   | _, _ => None *)
(*   end. *)

(* Definition bin_op_eval_real (op : bin_op) (r1 r2 : R) : option base_lit := *)
(*   match op with *)
(*   | PlusOp => Some *)
(*   | MinusOp => Some *)
(*   | MultOp => Some *)
(*   | LeOp => Some  bool_decide *)
(*   | LtOp => Some  bool_decide *)
(*   | EqOp => Some  bool_decide *)
(*   | _ => None *)
(*   end*)

(* Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val := *)
(*   if decide (op = EqOp) then *)
(*     if decide (v1 = v2) then *)
(*       Some  LitBool *)
(*     else *)
(*       None *)
(*   else *)
(*     match v1 , v2 with *)
(*     | LitV (LitInt n1), LitV (LitInt n2) => Some  bin_op_eval_int op n1 n2 *)
(*     | LitV (LitReal r1), LitV (LitReal r2) => LitV <*)
(*     | LitV (LitBool b1), LitV (LitBool b2) => LitV <*)
(*     | LitV (LitLoc l1), LitV v2 => LitV <*)
(*     | _, _ => None *)
(*     end. *)

(* Definition state_upd_heap (f : gmap loc val → gmap loc val) (σ : state) : state := *)
(*   {| heap := f σ.(heap); tapes := σ.(tapes); utapes := σ.(utapes) |}. *)
(* Global Arguments state_upd_heap _ !_ /. *)

(* Definition state_upd_tapes (f : gmap loc btape → gmap loc btape) (σ : state) : state := *)
(*   {| heap := σ.(heap); tapes := f σ.(tapes); utapes := σ.(utapes) |}. *)
(* Global Arguments state_upd_tapes _ !_ /. *)

(* Definition state_upd_utapes (f : gmap loc utape → gmap loc utape) (σ : state) : state := *)
(*   {| heap := σ.(heap); tapes := σ.(tapes); utapes := f σ.(utapes) |}. *)
(* Global Arguments state_upd_utapes _ !_ /. *)

(* Lemma state_upd_tapes_twice σ l xs ys : *)
(*   state_upd_tapes < l := ys > (state_upd_tapes < l := xs > σ) = state_upd_tapes < l:= ys > σ. *)
(* Proof. rewrite /state_upd_tapes /=. f_equal. apply insert_insert_eq. Qed. *)

(* Lemma state_upd_tapes_same σ σ' l xs ys : *)
(*   state_upd_tapes <l:=ys> σ = state_upd_tapes <l:=xs> σ' -> xs = ys. *)
(* Proof. rewrite /state_upd_tapes /=. intros K. simplify_eq. *)
(*        rewrite map_eq_iff in H. *)
(*        specialize (H l). *)
(*        rewrite !lookup_insert_eq in H. *)
(*        by simplify_eq. *)
(* Qed. *)

(* Lemma state_upd_tapes_no_change σ l ys : *)
(*   tapes σ !! l = Some ys -> *)
(*   state_upd_tapes <l := ys> σ = σ . *)
(* Proof. *)
(*   destruct σ as ? t. simpl. *)
(*   intros Ht. *)
(*   f_equal. *)
(*   apply insert_id. done. *)
(* Qed. *)

(* (* *)
(* Lemma state_upd_tapes_same' σ σ' l n xs (x y : stdpp.fin.fin (S n)) : *)
(*   state_upd_tapes <l:=(fin (n; xs++[x]))> σ = state_upd_tapes <l:=(fin(n; xs++[y]))> σ' -> x = y. *)
(* Proof. intros H. apply state_upd_tapes_same in H. by simplify_eq. Qed. *)

(* Lemma state_upd_tapes_neq' σ σ' l n xs (x y : stdpp.fin.fin (S n)) : *)
(*   x≠y -> state_upd_tapes <l:=(fin(n; xs++[x]))> σ ≠ state_upd_tapes <l:=(fin(n; xs++[y]))> σ'. *)
(* Proof. move => H /state_upd_tapes_same ?. simplify_eq. Qed. *)
(* *) *)

(* Fixpoint heap_array (l : loc) (vs : list val) : gmap loc val := *)
(*   match vs with *)
(*   |  => ∅ *)
(*   | v :: vs' => {l := v} ∪ heap_array (l +ₗ 1) vs' *)
(*   end. *)

(* Lemma heap_array_singleton l v : heap_array l v = {l := v}. *)
(* Proof. by rewrite /heap_array right_id. Qed. *)

(* Lemma heap_array_app l vs1 vs2 : heap_array l (vs1 ++ vs2) = (heap_array l vs1) ∪ (heap_array (l +ₗ (length vs1)) vs2) . *)
(* Proof. *)
(*   revert l. *)
(*   induction vs1; intro l. *)
(*   - simpl. *)
(*     rewrite map_empty_union loc_add_0 //. *)
(*   - rewrite -app_comm_cons /= IHvs1. *)
(*     rewrite map_union_assoc. *)
(*     do 2 f_equiv. *)
(*     rewrite Nat2Z.inj_succ /=. *)
(*     rewrite /Z.succ *)
(*       Z.add_comm *)
(*       loc_add_assoc //. *)
(* Qed. *)

(* Lemma heap_array_lookup l vs v k : *)
(*   heap_array l vs !! k = Some v ↔ *)
(*   ∃ j, (0 ≤ j)*)
(* Proof. *)
(*   revert k l; induction vs as |v' vs IH => l' l /=. *)
(*   { rewrite lookup_empty. naive_solver lia. } *)
(*   rewrite -insert_union_singleton_l lookup_insert_Some IH. split. *)
(*   - intros [-> ?] | (Hl & j & ? & -> & ?). *)
(*     { eexists 0. rewrite loc_add_0. naive_solver lia. } *)
(*     eexists (1 + j)*)
(*   - intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=. *)
(*     { rewrite loc_add_0; eauto. } *)
(*     right. split. *)
(*     { rewrite -{1}(loc_add_0 l). intros ?*)
(*     assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj. *)
(*     { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. } *)
(*     rewrite Hj /= in Hil. *)
(*     eexists (j - 1)*)
(*     auto with lia. *)
(* Qed. *)

(* Lemma heap_array_map_disjoint (h : gmap loc val) (l : loc) (vs : list val) : *)
(*   (∀ i, (0 ≤ i)Z → h !! (l +ₗ i) = None) → *)
(*   (heap_array l vs) #ₘ h. *)
(* Proof. *)
(*   intros Hdisj. apply map_disjoint_spec=> l' v1 v2. *)
(*   intros (j&?&->&Hjinj_lt)*)
(*   move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj. *)
(* Qed. *)

(* Definition state_upd_heap_N (l : loc) (n : nat) (v : val) (σ : state) : state := *)
(*   state_upd_heap (λ h, heap_array l (replicate n v) ∪ h) σ. *)

(* Lemma state_upd_heap_singleton l v σ : *)
(*   state_upd_heap_N l 1 v σ = state_upd_heap <l:= v> σ. *)
(* Proof. *)
(*   destruct σ as h p. rewrite /state_upd_heap_N /=. f_equiv. *)
(*   rewrite right_id insert_union_singleton_l. done. *)
(* Qed. *)

(* Lemma state_upd_tapes_heap σ l1 l2 xs m v : *)
(*   state_upd_tapes <l2:=xs> (state_upd_heap_N l1 m v σ) = *)
(*   state_upd_heap_N l1 m v (state_upd_tapes <l2:=xs> σ). *)
(* Proof. *)
(*   by rewrite /state_upd_tapes /state_upd_heap_N /=. *)
(* Qed. *)

(* Lemma heap_array_replicate_S_end l v n : *)
(*   heap_array l (replicate (S n) v) = heap_array l (replicate n v) ∪ {l +ₗ n:= v}. *)
(* Proof. *)
(*   induction n. *)
(*   - simpl. *)
(*     rewrite map_union_empty. *)
(*     rewrite map_empty_union. *)
(*     by rewrite loc_add_0. *)
(*   - rewrite replicate_S_end *)
(*      heap_array_app *)
(*      IHn /=. *)
(*     rewrite map_union_empty length_replicate //. *)
(* Qed. *)

(* (* [local] Open Scope R. *) *)



(* Section pointed_instances. *)
(*   Local Open Scope classical_set_scope. *)

(*   (* Fail Check (<<discr state>> : measurableType _).  *) *)
(*   HB.instance Definition _ := gen_eqMixin state. *)
(*   HB.instance Definition _ := gen_choiceMixin state. *)
(*   HB.instance Definition _ := isPointed.Build state inhabitant. *)
(*   (* Check (<<discr state>> : measurableType _). *) *)

(*   (** cfg is pointed (automatic) *) *)
(*   (* Check (<<discr cfg>> : measurableType _).  *) *)

(*   (** state * loc is pointed (automatic) *) *)
(*   (* Check (<<discr (state * loc)>> : measurableType _). *) *)

(*   (** R is pointed *) *)
(*   Check (<<discr R>> : measurableType _). *)

(* End pointed_instances. *)


(* Section meas_semantics. *)
(*   Local Open Scope classical_set_scope. *)
(*   Local Open Scope expr_scope. *)

(*   Definition discr_cfg : measurableType _ := (<<discr expr>> * <<discr state>>)*)

(*   Definition head_stepM_def (c : discr_cfg) : giryM discr_cfg := *)
(*     let (e1, σ1) := c in *)
(*     match e1 with *)
(*     | Rec f x e => *)
(*         giryM_ret R ((Val *)
(*     | Pair (Val v1) (Val v2) => *)
(*         giryM_ret R ((Val *)
(*     | InjL (Val v) => *)
(*         giryM_ret R ((Val *)
(*     | InjR (Val v) => *)
(*         giryM_ret R ((Val *)
(*     | App (Val (RecV f x e1)) (Val v2) => *)
(*         giryM_ret R ((subst' x v2 (subst' f (RecV f x e1) e1) , σ1) : discr_cfg) *)
(*     | UnOp op (Val v) => *)
(*         match un_op_eval op v with *)
(*           | Some w => giryM_ret R ((Val w, σ1) : discr_cfg) *)
(*           | _ => giryM_zero *)
(*         end *)
(*     | BinOp op (Val v1) (Val v2) => *)
(*         match bin_op_eval op v1 v2 with *)
(*           | Some w => giryM_ret R ((Val w, σ1) : discr_cfg) *)
(*           | _ => giryM_zero *)
(*         end *)
(*     | If (Val (LitV (LitBool true))) e1 e2  => *)
(*         giryM_ret R ((e1 , σ1) : discr_cfg) *)
(*     | If (Val (LitV (LitBool false))) e1 e2 => *)
(*         giryM_ret R ((e2 , σ1) : discr_cfg) *)
(*     | Fst (Val (PairV v1 v2)) => *)
(*         giryM_ret R ((Val v1 , σ1) : discr_cfg) (* Syntax error when I remove the space between v1 and , *) *)
(*     | Snd (Val (PairV v1 v2)) => *)
(*         giryM_ret R ((Val v2, σ1) : discr_cfg) *)
(*     | Case (Val (InjLV v)) e1 e2 => *)
(*         giryM_ret R ((App e1 (Val v), σ1) : discr_cfg) *)
(*     | Case (Val (InjRV v)) e1 e2 => *)
(*         giryM_ret R ((App e2 (Val v), σ1) : discr_cfg) *)
(*     | AllocN (Val (LitV (LitInt N))) (Val v) => *)
(*         let ℓ := fresh_loc σ1.(heap) in *)
(*         if bool_decide (0 < Z.to_nat N)*)
(*           then giryM_ret R ((Val  LitLoc ℓ, state_upd_heap_N ℓ (Z.to_nat N) v σ1) : discr_cfg) *)
(*           else giryM_zero *)
(*     | Load (Val (LitV (LitLoc l))) => *)
(*         match σ1.(heap) !! l with *)
(*           | Some v => giryM_ret R ((Val v, σ1) : discr_cfg) *)
(*           | None => giryM_zero *)
(*         end *)
(*     | Store (Val (LitV (LitLoc l))) (Val w) => *)
(*         match σ1.(heap) !! l with *)
(*           | Some v => giryM_ret R ((Val *)
(*           | None => giryM_zero *)
(*         end *)
(*     (* Uniform sampling from 0, 1 , ..., N *) *)
(*     | Rand (Val (LitV (LitInt N))) (Val (LitV LitUnit)) => *)
(*         giryM_map *)
(*           (m_discr (fun (n : 'I_(S (Z.to_nat N))) => ((Val  LitInt n, σ1) : discr_cfg))) *)
(*           (giryM_unif (Z.to_nat N)) *)
(*     | AllocTape (Val (LitV (LitInt z))) => *)
(*         let ι := fresh_loc σ1.(tapes) in *)
(*         giryM_ret R ((Val  LitLbl ι, state_upd_tapes <ι := {| btape_tape := emptyTape ; btape_bound := (Z.to_nat z) |} > σ1) : discr_cfg) *)
(*     (* Rand with a tape *) *)
(*     | Rand (Val (LitV (LitInt N))) (Val (LitV (LitLbl l))) => *)
(*         match σ1.(tapes) !! l with *)
(*         | Some btape => *)
(*             (* There exists a tape with label l *) *)
(*             let τ := btape.(btape_tape) in *)
(*             let M := btape.(btape_bound) in *)
(*             if (bool_decide (M = Z.to_nat N)) then *)
(*               (* Tape bounds match *) *)
(*               match (τ !! 0) with *)
(*               | Some v => *)
(*                   (* There is a next value on the tape *) *)
(*                   let σ' := state_upd_tapes < l := {| btape_tape := (tapeAdvance τ); btape_bound := M |} > σ1 in *)
(*                   (giryM_ret R ((Val  LitInt *)
(*               | None => *)
(*                   (* Next slot on tape is empty *) *)
(*                   giryM_map *)
(*                     (m_discr (fun (v : 'I_(S (Z.to_nat N))) => *)
(*                        (* Fill the tape head with new sample *) *)
(*                        let τ' := < (0 : nat) := Some (v : nat) > τ in *)
(*                        (* Advance the tape *) *)
(*                        let σ' := state_upd_tapes < l := {| btape_tape := (tapeAdvance τ'); btape_bound := M |} > σ1 in *)
(*                        (* Return the new sample and state *) *)
(*                        ((Val  LitInt *)
(*                    (giryM_unif (Z.to_nat N)) *)
(*               end *)
(*             else *)
(*               (* Tape bounds do not match *) *)
(*               (* Do not advance the tape, but still generate a new sample *) *)
(*               giryM_map *)
(*                 (m_discr (fun (n : 'I_(S (Z.to_nat N))) => ((Val  LitInt n, σ1) : discr_cfg))) *)
(*                 (giryM_unif (Z.to_nat N)) *)
(*         | None => giryM_zero *)
(*         end *)
(*     | AllocUTape => *)
(*         let ι := fresh_loc σ1.(utapes) in *)
(*         giryM_ret R ((Val  LitLbl ι, state_upd_utapes < ι := emptyTape > σ1) : discr_cfg) *)
(*     (* Urand with no tape *) *)
(*     | URand (Val (LitV LitUnit)) => *)
(*         giryM_map *)
(*           (m_discr (fun u => ((Val  LitReal u, σ1) : discr_cfg))) *)
(*           giryM_zero *)
(*     (* Urand with a tape *) *)
(*     | URand (Val (LitV (LitLbl l))) => *)
(*         match σ1.(utapes) !! l with *)
(*         | Some τ => *)
(*             (* tape l is allocated *) *)
(*             match (τ !! 0) with *)
(*             | Some u => *)
(*                 (* Head has a sample *) *)
(*                 let σ' := state_upd_utapes < l := (tapeAdvance τ) > σ1 in *)
(*                 (giryM_ret R ((Val  LitReal u, σ') : discr_cfg)) *)
(*             | None => *)
(*                 (* Head has no sample *) *)
(*                 giryM_map *)
(*                   (m_discr (fun (u : R) => *)
(*                     (* Fill tape head with new sample *) *)
(*                     let τ' := < (0 : nat) := Some u > τ in *)
(*                     (* Advance tape *) *)
(*                     let σ' := state_upd_utapes < l := (tapeAdvance τ') > σ1 in *)
(*                     (* Return the update value an state *) *)
(*                     ((Val  LitReal u, σ') : discr_cfg))) *)
(*                   giryM_zero *)
(*             end *)
(*         | None => giryM_zero *)
(*         end *)
(*     | Tick (Val (LitV (LitInt n))) => giryM_ret R ((Val  LitUnit, σ1) : discr_cfg) *)
(*     | _ => giryM_zero *)
(*     end. *)

(*   (* I don't care if this this true; we will delete it soon and replace it with a proof for the real SA. *) *)
(*   Local Lemma head_stepM_def_measurable : *)
(*     @measurable_fun _ _ discr_cfg (giryM discr_cfg) setT head_stepM_def. *)
(*   Proof. Admitted. *)

(*   HB.instance Definition _ := *)
(*     isMeasurableMap.Build _ _ _ _ _ head_stepM_def_measurable. *)

(*   Definition head_stepM : measurable_map (<<discr expr>> * <<discr state>>)type) := *)
(*     head_stepM_def. *)

(* End meas_semantics. *)


(* (* *)
(* Lemma state_step_unfold σ α N ns: *)
(*   tapes σ !! α = Some (N; ns) -> *)
(*   state_step σ α = dmap (λ n, state_upd_tapes (<α := (N; ns ++ [n])>) σ) (dunifP N). *)
(* Proof. *)
(*   intros H. *)
(*   rewrite /state_step. *)
(*   rewrite bool_decide_eq_true_2; last first. *)
(*   { by apply elem_of_dom. } *)
(*   by rewrite (lookup_total_correct (tapes σ) α (N; ns)); last done. *)
(* Qed. *)
(* *) *)

(* (** Basic properties about the language *) *)
(* Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki). *)
(* Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed. *)

(* Lemma fill_item_val Ki e : *)
(*   is_Some (to_val (fill_item Ki e)) → is_Some (to_val e). *)
(* Proof. intros v ?. induction Ki; simplify_option_eq; eauto. Qed. *)

(* (* ??? *) *)
(* (* *)
(* Lemma val_head_stuck e σ ρ : *)
(*   head_step e σ ρ > 0 → to_val e = None. *)
(* Proof. destruct ρ, e; |done... rewrite /pmf /=. lra. Qed. *)

(* Lemma head_ctx_step_val Ki e σ ρ : *)
(*   head_step (fill_item Ki e) σ ρ > 0 → is_Some (to_val e). *)
(* Proof. *)
(*   destruct ρ, Ki ; *)
(*     rewrite /pmf/= ; *)
(*     repeat case_match; clear -H ; inversion H; intros ; (lra || done). *)
(* Qed. *)

(* *) *)

(* Local Open Scope classical_set_scope. *)

(* (** A relational characterization of the support of head_step to make it easier to *)
(*     do inversion and prove reducibility easier c.f. lemma below *) *)
(* Inductive head_step_rel : expr -> state -> expr -> state → Prop := *)
(* (* Values *) *)
(* | RecS f x e σ : *)
(*   head_step_rel (Rec f x e) σ (Val *)
(* | PairS v1 v2 σ : *)
(*   head_step_rel (Pair (Val v1) (Val v2)) σ (Val *)
(* | InjLS v σ : *)
(*   head_step_rel (InjL  InjLV v) σ *)
(* | InjRS v σ : *)
(*   head_step_rel (InjR  InjRV v) σ *)

(* (* Pure reductions *) *)
(* | BetaS f x e1 v2 e' σ : *)
(*   e' = subst' x v2 (subst' f (RecV f x e1) e1) → *)
(*   head_step_rel (App (Val *)
(* | UnOpS op v v' σ : *)
(*   un_op_eval op v = Some v' → *)
(*   head_step_rel (UnOp op (Val v)) σ (Val v') σ *)
(* | BinOpS op v1 v2 v' σ : *)
(*   bin_op_eval op v1 v2 = Some v' → *)
(*   head_step_rel (BinOp op (Val v1) (Val v2)) σ (Val v') σ *)
(* | IfTrueS e1 e2 σ : *)
(*   head_step_rel (If (Val  LitBool true) e1 e2) σ e1 σ *)
(* | IfFalseS e1 e2 σ : *)
(*   head_step_rel (If (Val  LitBool false) e1 e2) σ e2 σ *)
(* | FstS v1 v2 σ : *)
(*   head_step_rel (Fst (Val *)
(* | SndS v1 v2 σ : *)
(*   head_step_rel (Snd (Val *)
(* | CaseLS v e1 e2 σ : *)
(*   head_step_rel (Case (Val *)
(* | CaseRS v e1 e2 σ : *)
(*   head_step_rel (Case (Val *)

(* (* Heap *) *)
(* | AllocNS z N v σ l : *)
(*   l = fresh_loc σ.(heap) → *)
(*   N = Z.to_nat z → *)
(*   (0 < N)*)
(*   head_step_rel *)
(*     (AllocN (Val (LitV (LitInt z))) (Val v)) σ *)
(*     (Val  LitLoc l) (state_upd_heap_N l N v σ) *)
(* | LoadS l v σ : *)
(*   σ.(heap) !! l = Some v → *)
(*   head_step_rel (Load (Val  LitLoc l)) σ (of_val v) σ *)
(* | StoreS l v w σ : *)
(*   σ.(heap) !! l = Some v → *)
(*   head_step_rel (Store (Val  LitLoc l) (Val w)) σ *)
(*     (Val *)

(* (* Rand *) *)
(* | RandNoTapeS z N (n_int : Z) (n_nat : nat) σ: *)
(*   N = Z.to_nat z → *)
(*   n_nat < N -> *)
(*   Z.of_nat n_nat = n_int -> *)
(*   head_step_rel (Rand (Val  LitInt z) (Val  LitV *)
(* | AllocTapeS z N σ l : *)
(*   l = fresh_loc σ.(tapes) → *)
(*   N = Z.to_nat z → *)
(*   head_step_rel (AllocTape (Val (LitV (LitInt z)))) σ *)
(*     (Val  LitLbl l) (state_upd_tapes <l := {| btape_tape := emptyTape ; btape_bound := N |}> σ) *)
(* | RandTapeS l z N n b b' σ : *)
(*   N = Z.to_nat z → *)
(*   σ.(tapes) !! l = Some {| btape_tape := b ; btape_bound := N |} -> *)
(*   b !! 0 = Some (Z.to_nat n) -> *)
(*   b' = tapeAdvance b -> *)
(*   head_step_rel (Rand (Val (LitV (LitInt z))) (Val (LitV (LitLbl l)))) σ *)
(*     (Val  LitInt *)
(* | RandTapeEmptyS l z N (n_nat : nat) (n_int : Z) σ : *)
(*   N = Z.to_nat z → *)
(*   Z.of_nat n_nat = n_int -> *)
(*   n_nat < N -> *)
(*   σ.(tapes) !! l = Some {| btape_tape := emptyTape; btape_bound := N |} → *)
(*   head_step_rel (Rand (Val (LitV (LitInt z))) (Val  LitLbl l)) σ (Val  LitInt n_nat) σ *)
(* | RandTapeOtherS l z M N b (n_nat : nat) (n_int : Z) σ : *)
(*   N = Z.to_nat z → *)
(*   Z.of_nat n_nat = n_int -> *)
(*   n_nat < N -> *)
(*   σ.(tapes) !! l = Some {| btape_tape := b ; btape_bound := M |} → *)
(*   N ≠ M → *)
(*   head_step_rel (Rand (Val (LitV (LitInt z))) (Val  LitLbl l)) σ (Val  LitInt n_int) σ *)

(* (* Urand *) *)
(* | URandNoTapeS (r : R) σ : *)
(*   (0 <= r)*)
(*   (r <= 1)*)
(*   head_step_rel (URand (Val  LitV *)
(* | AllocUTapeS σ l : *)
(*   l = fresh_loc σ.(tapes) → *)
(*   head_step_rel AllocUTape σ *)
(*     (Val  LitLbl l) (state_upd_utapes <l := emptyTape> σ) *)
(* | URandTapeS l b b' r σ : *)
(*   σ.(utapes) !! l = Some b -> *)
(*   b !! 0 = Some r -> *)
(*   b' = tapeAdvance b -> *)
(*   head_step_rel (URand (Val (LitV (LitLbl l)))) σ *)
(*     (Val  LitReal *)
(* | URandTapeEmptyS l (r : R) b σ : *)
(*   (0 <= r)*)
(*   (r <= 1)*)
(*   σ.(utapes) !! l = Some b → *)
(*   head_step_rel (URand (Val  LitLbl l)) σ (Val  LitReal r) σ *)

(* (* Tick *) *)
(* | TickS σ z : *)
(*   head_step_rel (Tick  LitV  LitV *)

(* Create HintDb head_step. *)
(* Global Hint Constructors head_step_rel : head_step. *)
(* (* 0*)
(*    unconstrained. *) *)
(* Global Hint Extern 1 *)
(*   (head_step_rel (Rand (Val (LitV _)) (Val (LitV LitUnit))) _ _ _) => *)
(*          eapply (RandNoTapeS _ _ 0*)
(* Global Hint Extern 1 *)
(*   (head_step_rel (Rand (Val (LitV _)) (Val (LitV (LitLbl _)))) _ _ _) => *)
(*          eapply (RandTapeEmptyS _ _ _ 0*)
(* Global Hint Extern 1 *)
(*   (head_step_rel (Rand (Val (LitV _)) (Val (LitV (LitLbl _)))) _ _ _) => *)
(*          eapply (RandTapeOtherS _ _ _ _ _ 0*)

(* (* *)
(* Ltac inv_head_step := *)
(*   repeat *)
(*     match goal with *)
(*     | H : context @bool_decide ?P ?dec |- _ => *)
(*         try (rewrite bool_decide_eq_true_2 in H; |done); *)
(*         try (rewrite bool_decide_eq_false_2 in H; |done); *)
(*         destruct_decide (@bool_decide_reflect P dec); simplify_eq *)
(*     | _ => progress simplify_map_eq; simpl in *; inv_distr; repeat case_match; inv_distr *)
(*     | H : to_val _ = Some _ |- _ => apply of_to_val in H *)
(*     | H : is_Some (_ !! _) |- _ => destruct H *)
(*     end. *)

(* Lemma head_step_support_equiv_rel e1 e2 σ1 σ2 : *)
(*   head_step e1 σ1 (e2, σ2) > 0 ↔ head_step_rel e1 σ1 e2 σ2. *)
(* Proof. *)
(*   split. *)
(*   - intros ?. destruct e1; inv_head_step; eauto with head_step. *)
(*   - inversion 1; simplify_map_eq/=; try case_bool_decide; simplify_eq; solve_distr; done. *)
(* Qed. *)

(* Lemma state_step_support_equiv_rel σ1 α σ2 : *)
(*   state_step σ1 α σ2 > 0 ↔ state_step_rel σ1 α σ2. *)
(* Proof. *)
(*   rewrite /state_step. split. *)
(*   - case_bool_decide; |intros; inv_distr. *)
(*     case_match. intros ?. inv_distr. *)
(*     econstructor; eauto with lia. *)
(*   - inversion_clear 1. *)
(*     rewrite bool_decide_eq_true_2 // H1. solve_distr. *)
(* Qed. *)

(* Lemma state_step_head_step_not_stuck e σ σ' α : *)
(*   state_step σ α σ' > 0 → (∃ ρ, head_step e σ ρ > 0) ↔ (∃ ρ', head_step e σ' ρ' > 0). *)
(* Proof. *)
(*   rewrite state_step_support_equiv_rel. *)
(*   inversion_clear 1. *)
(*   split; intros [e2 σ2] Hs. *)
(*   (* TODO: the sub goals used to be solved by simplify_map_eq  *) *)
(*   - destruct e; inv_head_step; try by (unshelve (eexists; solve_distr)). *)
(*     + destruct (decide (α = l1)); simplify_eq. *)
(*       * rewrite lookup_insert_eq in H11. done. *)
(*       * rewrite lookup_insert_ne // in H11. rewrite H11 in H7. done. *)
(*     + destruct (decide (α = l1)); simplify_eq. *)
(*       * rewrite lookup_insert_eq in H11. done. *)
(*       * rewrite lookup_insert_ne // in H11. rewrite H11 in H7. done. *)
(*     + destruct (decide (α = l1)); simplify_eq. *)
(*       * rewrite lookup_insert_eq in H10. done. *)
(*       * rewrite lookup_insert_ne // in H10. rewrite H10 in H7. done. *)
(*   - destruct e; inv_head_step; try by (unshelve (eexists; solve_distr)). *)
(*     + destruct (decide (α = l1)); simplify_eq. *)
(*       * apply not_elem_of_dom_2 in H11. done. *)
(*       * rewrite lookup_insert_ne // in H7. rewrite H11 in H7.  done. *)
(*     + destruct (decide (α = l1)); simplify_eq. *)
(*       * rewrite lookup_insert_eq // in H7. *)
(*         apply not_elem_of_dom_2 in H11. done. *)
(*       * rewrite lookup_insert_ne // in H7. rewrite H11 in H7. done. *)
(*     + destruct (decide (α = l1)); simplify_eq. *)
(*       * rewrite lookup_insert_eq // in H7. *)
(*         apply not_elem_of_dom_2 in H10. done. *)
(*       * rewrite lookup_insert_ne // in H7. rewrite H10 in H7. done. *)
(* Qed. *)

(* *) *)

(* (* *)
(* Lemma head_step_mass e σ : *)
(*   (∃ ρ, head_step e σ ρ > 0) → SeriesC (head_step e σ) = 1. *)
(* Proof. *)
(*   intros [] Hs%head_step_support_equiv_rel. *)
(*   inversion Hs; *)
(*     repeat (simplify_map_eq/=; solve_distr_mass || case_match; try (case_bool_decide; done)). *)
(* Qed. *)
(* *) *)
(* Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 : *)
(*   to_val e1 = None → to_val e2 = None → *)
(*   fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2. *)
(* Proof. destruct Ki2, Ki1; naive_solver eauto with f_equal. Qed. *)
(* Fixpoint height (e : expr) : nat := *)
(*   match e with *)
(*   | Val _ => 1 *)
(*   | Var _ => 1 *)
(*   | Rec _ _ e => 1 + height e *)
(*   | App e1 e2 => 1 + height e1 + height e2 *)
(*   | UnOp _ e => 1 + height e *)
(*   | BinOp _ e1 e2 => 1 + height e1 + height e2 *)
(*   | If e0 e1 e2 => 1 + height e0 + height e1 + height e2 *)
(*   | Pair e1 e2 => 1 + height e1 + height e2 *)
(*   | Fst e => 1 + height e *)
(*   | Snd e => 1 + height e *)
(*   | InjL e => 1 + height e *)
(*   | InjR e => 1 + height e *)
(*   | Case e0 e1 e2 => 1 + height e0 + height e1 + height e2 *)
(*   | AllocN e1 e2 => 1 + height e1 + height e2 *)
(*   | Load e => 1 + height e *)
(*   | Store e1 e2 => 1 + height e1 + height e2 *)
(*   | AllocTape e => 1 + height e *)
(*   | AllocUTape => 1 *)
(*   | Rand e1 e2 => 1 + height e1 + height e2 *)
(*   | URand e => 1 + height e *)
(*   | Tick e => 1 + height e *)
(*   end. *)

(* Definition expr_ord (e1 e2 : expr) : Prop := (height e1 < height e2)*)

(* Lemma expr_ord_wf' h e : (height e ≤ h)*)
(* Proof. *)
(*   rewrite /expr_ord. revert e; induction h. *)
(*   { destruct e; simpl; lia. } *)
(*   intros ; simpl; *)
(*     constructor; simpl; intros ; eauto with lia. *)
(* Defined. *)

(* Lemma expr_ord_wf : well_founded expr_ord. *)
(* Proof. red; intro; eapply expr_ord_wf'; eauto. Defined. *)


(* (* TODO: this proof is slow, but I do not see how to make it faster... *) *)
(* Lemma decomp_expr_ord Ki e e' : decomp_item e = Some (Ki, e') → expr_ord e' e. *)
(* Proof. *)
(*   rewrite /expr_ord /decomp_item. *)
(*   destruct Ki ; repeat destruct_match ; intros = ; subst ; cbn ; lia. *)
(* Qed. *)

(* Lemma decomp_fill_item Ki e : *)
(*   to_val e = None → decomp_item (fill_item Ki e) = Some (Ki, e). *)
(* Proof. destruct Ki ; simpl ; by repeat destruct_match. Qed. *)

(* (* TODO: this proof is slow, but I do not see how to make it faster... *) *)
(* Lemma decomp_fill_item_2 e e' Ki : *)
(*   decomp_item e = Some (Ki, e') → fill_item Ki e' = e ∧ to_val e' = None. *)
(* Proof. *)
(*   rewrite /decomp_item ; *)
(*     destruct e ; try done ; *)
(*     destruct Ki ; cbn ; repeat destruct_match ; intros = ; subst ; auto. *)
(* Qed. *)

(* Local Open Scope classical_set_scope. *)

(* Definition fill_item_mf K := m_discr (fill_item K : <<discr expr>> -> <<discr expr>>). *)

(* Definition meas_lang_mixin : *)
(*   @MeasEctxiLanguageMixin _ _ _ <<discr expr>> <<discr val>> <<discr state>> ectx_item *)
(*     of_val to_val fill_item_mf decomp_item expr_ord head_stepM_def. *)
(* Proof. *)
(*   split. *)
(* Admitted. *)

(* ***) *)

(* End meas_lang. *)
(* (* *)

(* (** Language *) *)


(* Canonical Structure meas_ectxi_lang := MeasEctxiLanguage meas_lang.head_stepM meas_lang.meas_lang_mixin. *)
(* Canonical Structure meas_ectx_lang := MeasEctxLanguageOfEctxi meas_ectxi_lang. *)
(* Canonical Structure meas_lang := MeasLanguageOfEctx meas_ectx_lang. *)

(* (* Prefer meas_lang names over ectx_language names. *) *)
(* Export meas_lang. *)
(* *) *)