diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml new file mode 100644 index 0000000..a1b01f7 --- /dev/null +++ b/.github/workflows/docker-action.yml @@ -0,0 +1,33 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. +name: Docker CI + +on: + push: + branches: + - master + pull_request: + branches: + - '**' + workflow_dispatch: + +jobs: + build: + # the OS must be GNU/Linux to be able to use the docker-coq-action + runs-on: ubuntu-latest + strategy: + matrix: + image: + - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0' + fail-fast: false + steps: + - uses: actions/checkout@v4 + - uses: coq-community/docker-coq-action@v1 + with: + opam_file: 'coq-FreerDPS.opam' + custom_image: ${{ matrix.image }} + + +# See also: +# https://github.com/coq-community/docker-coq-action#readme +# https://github.com/erikmd/docker-coq-github-action-demo diff --git a/.gitignore b/.gitignore index 77882f9..5cd85bc 100644 --- a/.gitignore +++ b/.gitignore @@ -1,11 +1,13 @@ -**/Makefile -**/Makefile.conf -**/.CoqMakefile.d -**/.Makefile.d +**/Makefile.rocq +**/Makefile.rocq.conf +**/.Makefile.rocq.d **/*.glob **/*.vo **/*.vok **/*.vos **/.*.aux _opam -_build \ No newline at end of file +_build +freer_playground/.Makefile.d +freer_playground/Makefile +freer_playground/Makefile.conf \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..d80bd56 --- /dev/null +++ b/Makefile @@ -0,0 +1,15 @@ +all: Makefile.rocq + $(MAKE) -f Makefile.rocq all + +clean: Makefile.rocq + $(MAKE) -f Makefile.rocq cleanall + +Makefile.rocq: _CoqProject + rocq makefile -f _CoqProject -o Makefile.rocq + +_CoqProject Makefile: ; + +%: Makefile.rocq + $(MAKE) -f Makefile.rocq $@ + +.PHONY: all clean diff --git a/README.md b/README.md index 21867fe..acf66ce 100644 --- a/README.md +++ b/README.md @@ -1,59 +1,53 @@ -This repo is the home of **FreerDPS**. + +# Freer Equational Reasoning for Distributed and Probabilistic Systems -FreerDPS stands for : **Freer** *E*quational *R*easoning for **D**istributed and **P**robabilistic **S**ystems. +[![Docker CI][docker-action-shield]][docker-action-link] -# Code structure +[docker-action-shield]: https://github.com/FreerDPS/FreerDPS/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/FreerDPS/FreerDPS/actions/workflows/docker-action.yml -As of now, the code base is mainly a rewrite of [FreeSpec](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect. -# Install -## Libraries -You need to install the following libraries for the project to work : -- coq 9.0 (it will use rocq as soon as monae makes the move) -- monae -- infotheo -- mathcomp -- hierarchy builder +This work started as a rewrite/extension of [FreeSpec Core](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect. -## Commands +This work has been accepted for presentation to [COMPAS26](https://2026.compas-conference.fr/) (no paper available online). -Mainly for interns installing it first time : +## Meta -```sh -opam switch create . ocaml-base-compiler.4.14.2 -eval $(opam env) -opam pin add coq 9.0.0 -eval $(opam env) +- Author(s): + - Hugo Forraz (initial) +- License: [MIT License](LICENSE) +- Additional dependencies: + - [MathComp](https://math-comp.github.io) + - [MathComp Analysis](https://github.com/math-comp/analysis) + - [MathComp Algebra Tactics](https://github.com/math-comp/algebra-tactics) + - Monae +- Related publication(s): + - []() -opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq-hierarchy-builder coq-mathcomp-ssreflect coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable coq-mathcomp-classical -``` - -In case monae / infotheo can not be installed through opam, you can clone them from github and fix their versions. +## Building and installation instructions -Versions known to work : -- monae : dev -- infotheo : 0.9.6 => [I have a local fork for now](https://github.com/forrazh/infotheo/tree/fix/0.9.6) +The easiest way to install the latest released version of Freer Equational Reasoning for Distributed and Probabilistic Systems +is via [OPAM](https://opam.ocaml.org/doc/Install.html): -You just need to clone the repositories and run : - -```sh -eval $(opam env) # it should be the same switch as the one created above -oam pin add . +```shell +opam repo add rocq-released https://rocq-prover.org/opam/released +opam install coq-FreerDPS ``` -inside the repository. - -Once everything is installed, you can run the following commands : - -```sh -coq_makefile -f _CoqProject -o Makefile -make +To instead build and install manually, you need to make sure that all the +libraries this development depends on are installed. The easiest way to do that +is still to rely on opam: + +``` shell +git clone https://github.com/FreerDPS/FreerDPS.git +cd FreerDPS +opam repo add rocq-released https://rocq-prover.org/opam/released +opam install --deps-only . +make # or make -j +make install ``` - - -# Publications - -This work has been submitted to COMPAS and is under reviewing. \ No newline at end of file diff --git a/_CoqProject b/_CoqProject index 5035822..802a979 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,15 +1,16 @@ -Q theories FreerDPS + -arg -w -arg -projection-no-head-constant ./theories/Component.v ./theories/Contract.v ./theories/Core.v +./theories/mathcomp_extra.v ./theories/Hoare.v -./theories/HoareFacts.v -./theories/Impure.v +./theories/Freer.v ./theories/Init.v ./theories/Instrument.v -./theories/Interface.v +./theories/Effect.v ./theories/Semantics.v -./theories/Tactics.v ./theories/Typeclasses.v +./examples/airlock.v diff --git a/coq-FreerDPS.opam b/coq-FreerDPS.opam new file mode 100644 index 0000000..2757d15 --- /dev/null +++ b/coq-FreerDPS.opam @@ -0,0 +1,34 @@ +# This file was generated from `meta.yml`, please do not edit manually. +# Follow the instructions on https://github.com/coq-community/templates to regenerate. + +opam-version: "2.0" +maintainer: "Hugo Forraz" +version: "dev" + +homepage: "https://github.com/FreerDPS/FreerDPS" +dev-repo: "git+https://github.com/FreerDPS/FreerDPS.git" +bug-reports: "https://github.com/FreerDPS/FreerDPS/issues" +license: "MIT" + +synopsis: "TODO" +description: """ +This work started as a rewrite/extension of [FreeSpec Core](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect. + +This work has been accepted for presentation to [COMPAS26](https://2026.compas-conference.fr/) (no paper available online).""" + +build: [make "-j%{jobs}%"] +install: [make "install"] +depends: [ + "coq" + "rocq-mathcomp-ssreflect" {>= "2.5.0"} + "rocq-mathcomp-analysis" {>= "1.16.0"} + "coq-mathcomp-algebra-tactics" {>= "1.2.7"} + "rocq-monae" {= "0.9.2"} +] + +tags: [ + "logpath:" +] +authors: [ + "Hugo Forraz" +] diff --git a/dune-project b/dune-project index bda8af8..fddc530 100644 --- a/dune-project +++ b/dune-project @@ -14,7 +14,7 @@ (synopsis "A FreeSpec rewrite to bring the power of equational reasoning and probabilities.") (description "A longer description") (depends - (coq-monae (= "dev")) + (coq-monae (= "latest")) (coq-equations (="latest")) (coq-hierarchy-builder (= "latest")) (coq-mathcomp-ssreflect (= "latest")) @@ -26,10 +26,10 @@ (coq-mathcomp-classical (= "latest")) (coq (= "9.0")) (coq-stdlib (= "9.0.0")) - (coq-infotheo (= "dev")) + (coq-infotheo (= "0.9.7")) )) -; monae and infotheo are in dev for now because we want +; monae is in dev and infotheo is in 0.9.7 for now because we want ; to use the latest coq version available, which is not ; possible using the current opam versions. diff --git a/examples/airlock.v b/examples/airlock.v index 9f125d2..e6b430b 100644 --- a/examples/airlock.v +++ b/examples/airlock.v @@ -4,59 +4,52 @@ (* Copyright (C) 2018–2020 ANSSI *) -From Coq Require Import Arith. -From FreerDPS Require Import Core Impure Hoare. -From monae Require Import preamble hierarchy. +From FreerDPS Require Import Init. +(* WARNING: Move this import to its MathComp counterpart. *) +From Stdlib Require Import Arith. +From mathcomp Require Import all_boot classical_sets. +From FreerDPS Require Import Core Freer Hoare. -#[local] Open Scope nat_scope. -#[local] Open Scope monae_scope. +Import FreerFuns. +Generalizable All Variables. -Create HintDb airlock. (** * Specifying *) +(* Opaque denote. *) + -(** ** Doors *) +Module Export DoorsControllerM. +(** ** Doors *) Inductive door : Type := left | right. - -Definition door_eq_dec (d d' : door) : { d = d' } + { ~ d = d' } := - ltac:(decide equality). -Inductive DOORS : interface := +HB.instance Definition _ := gen_eqMixin door. + +Inductive DOORS : effect := | IsOpen : door -> DOORS bool | Toggle : door -> DOORS unit. -Generalizable All Variables. - -Arguments request {_ } _ _ _. - -Check request. - -Section a. - -Definition is_open `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im bool := trigger (inj_p $ IsOpen d). - -Definition toggle `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im unit := trigger (inj_p $ Toggle d). - -Definition open_door `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im unit := - is_open d >>= fun open => - when (negb open) (toggle d). - -Definition close_door `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im unit := - is_open d >>= fun open => - when open (toggle d). +Section doors_s. +Context `{Provide Fx DOORS} {im : freerMonad Fx}. +Definition is_open (d : door) : im bool := trigger $ IsOpen d. +Definition toggle (d : door) : im unit := trigger $ Toggle d. +Definition open_door (d : door) : im unit := + is_open d >>= fun open => when (~~ open) (toggle d). +Definition close_door (d : door) : im unit := + is_open d >>= (when ^~ (toggle d)). +End doors_s. (** ** Controller *) -Inductive CONTROLLER : interface := +Inductive CONTROLLER : effect := | Tick : CONTROLLER unit | RequestOpen (d : door) : CONTROLLER unit. -Definition tick `{Provide ix CONTROLLER} {im : impureMonad ix} : im unit := - trigger (inj_p Tick). - -Definition request_open `{Provide ix CONTROLLER} {im : impureMonad ix} (d : door) : im unit := - trigger (inj_p $ RequestOpen d). +Section controller_s. +Context `{Provide Fx CONTROLLER} {im : freerMonad Fx}. +Definition tick : im unit := trigger Tick. +Definition request_open (d : door) : im unit := trigger $ RequestOpen d. +End controller_s. Definition co (d : door) : door := match d with @@ -64,47 +57,34 @@ Definition co (d : door) : door := | right => left end. -Definition controller `{Provide ix DOORS, Provide ix (STORE nat)} {im : impureMonad ix} - : component (im:=im) CONTROLLER ix - (* . - move=>X; case=>[|d]. - - apply/bind=>[|cpt]. - + apply/iget. - + apply/when. - * apply: (15 [|_]. - -- apply/close_door/left. - -- apply/bind=>[|_]. - ++ apply/close_door/right. - ++ apply/iput/0. - - apply/bind=>[|_]. - + apply/close_door/co/d. - + apply/bind=>[|_]. - * apply/open_door/d. - * apply/iput/0. - Show Proof. *) - := +Lemma co_leftE : co left = right. +Proof. by []. Qed. + +Definition controller `{Provide Fx DOORS, Provide Fx (STORE nat)} + {im : freerMonad Fx} : component (im:=im) CONTROLLER Fx := fun _ op => match op with | Tick => iget >>= fun cpt => - when (15 > close_door right >> - iput 0 + iput 0%nat | RequestOpen d => - close_door (co d) >> - open_door d >> - iput 0 + close_door (co d) >> + open_door d >> + iput 0%nat end. +End DoorsControllerM. (** * Verifying the Airlock Controller *) (** ** Doors Specification *) -(** *** Witness States *) +(* ----------------------------- Witness States ----------------------------- *) Definition Ω : Type := bool * bool. +(* S : Type := left * rght. *) Definition sel (d : door) : Ω -> bool := match d with @@ -114,23 +94,21 @@ Definition sel (d : door) : Ω -> bool := Definition tog (d : door) (ω : Ω) : Ω := match d with - | left => (negb (fst ω), snd ω) - | right => (fst ω, negb (snd ω)) + | left => (~~ (fst ω), snd ω) + | right => (fst ω, ~~ (snd ω)) end. Lemma tog_equ_1 (d : door) (ω : Ω) - : sel d (tog d ω) = negb (sel d ω). - -Proof. - by case:d. -Qed. + : sel d (tog d ω) = ~~ (sel d ω). +Proof. by case: d. Qed. Lemma tog_equ_2 (d : door) (ω : Ω) : sel (co d) (tog d ω) = sel (co d) ω. +Proof. by case: d. Qed. -Proof. - destruct d; reflexivity. -Qed. +Opaque tog. + +(* -------------------------------------------------------------------------- *) (** From now on, we will reason about [tog] using [tog_equ_1] and [tog_equ_2]. FreeSpec tactics rely heavily on [cbn] to simplify certain terms, so we use @@ -141,237 +119,282 @@ Qed. trick to prevent [cbn] to unfold impure computations covered by intermediary theorems. *) -#[local] Opaque tog. - -Definition step (ω : Ω) (a : Type) (e : DOORS a) (x : a) := - match e with - | Toggle d => tog d ω - | _ => ω - end. - -(** *** Requirements *) +(* -------------------------------- Contract -------------------------------- *) +(* Ω = bool * bool : doors state *) +Definition step (ω : Ω) (a : Type) (op : DOORS a) (_ : a) : Ω := + if op is Toggle d then tog d ω else ω. +(** *** Requirements / Precondition *) Inductive doors_o_caller : Ω -> forall (a : Type), DOORS a -> Prop := - (** - Given the door [d] of o system [ω], it is always possible to ask for the state of [d]. *) - | req_is_open (d : door) (ω : Ω) : doors_o_caller ω bool (IsOpen d) - (** - Given the door [d] of o system [ω], if [d] is closed, then the second door [co d] has to be closed too for a request to toggle [d] to be valid. *) - -| req_toggle (d : door) (ω : Ω) (H : sel d ω = false -> sel (co d) ω = false) +| req_toggle (d : door) (ω : Ω) (H : sel (co d) ω -> sel d ω) : doors_o_caller ω unit (Toggle d). -Hint Constructors doors_o_caller : airlock. - -(** *** Promises *) - +(** *** Promises / PostCondition *) Inductive doors_o_callee : Ω -> forall (a : Type), DOORS a -> a -> Prop := - (** - When a system in a state [ω] reports the state of the door [d], it shall reflect the true state of [d]. *) - | doors_o_callee_is_open (d : door) (ω : Ω) (x : bool) (equ : sel d ω = x) : doors_o_callee ω bool (IsOpen d) x - -(** - There is no particular doors_o_calleeises on the result [x] of a request for [ω] to - close the door [d]. *) - +(** - There is no particular requirement on the result [x] of a request for + [ω] to close the door [d]. *) | doors_o_callee_toggle (d : door) (ω : Ω) (x : unit) : doors_o_callee ω unit (Toggle d) x. - Hint Constructors doors_o_callee : airlock. - -Definition doors_contract : contract DOORS Ω := +(* doors_c => {{door_caller}} p%step {{door_callee}} *) +Definition doors_c : contract DOORS Ω := make_contract step doors_o_caller doors_o_callee. +(* -------------------------------------------------------------------------- *) -(** ** Intermediary Lemmas *) - -(** Closing a door [d] in any system [ω] is always a respectful operation. *) +Section doors_pre_post_helpers. +Context `{Provide Fx DOORS} {a : Type}. -Lemma close_door_respectful `{Provide ix DOORS} {im : impureMonad ix} (ω : Ω) (d : door) - : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) (doors_contract) (close_door d))( ω). +Lemma doors_effect_preE (op : Fx a) (ω : Ω) : + pre (hoare_of_contract doors_c op) ω <-> + match proj_p op with + | Some door_op => doors_o_caller ω a door_op + | None => True + end. +Proof. by rewrite /hoare_of_contract /= /gen_caller_obligation. Qed. + +Lemma doors_effect_postE + (op : Fx a) (ω : Ω) (x : a) (ω' : Ω) : + post (hoare_of_contract doors_c op) ω x ω' <-> + match proj_p op with + | Some door_op => + ω' = step ω a door_op x /\ doors_o_callee ω a door_op x + | None => ω' = ω + end. +Proof. +rewrite /hoare_of_contract /= /gen_witness_update + /gen_callee_obligation. +case: (proj_p op)=> [door_op |] /=. +- by []. +by split=> [[-> _] | ->]. +Qed. +Lemma doors_pre_condE + (ω : Ω) (op : DOORS a) : + pre (hoare_of_contract doors_c (inj_p op)) ω <-> + doors_o_caller ω a op. +Proof. by rewrite doors_effect_preE proj_inj_p_equ. Qed. + +Lemma doors_post_condE + (ω : Ω) (op : DOORS a) (x : a) (ω' : Ω) : + post (hoare_of_contract doors_c (inj_p op)) ω x ω' <-> + ω' = step ω a op x /\ doors_o_callee ω a op x. +Proof. by rewrite doors_effect_postE proj_inj_p_equ. Qed. +End doors_pre_post_helpers. + +Opaque hoare_of_contract. + +(*--------------------------- Intermediary Lemmas ----------------------------*) +Section IntermLemmaS. +Context `{Provide Fx DOORS} (ω : Ω) (d : door). + +Lemma doors_is_open_post_retE (opened : bool) (ω' : Ω) : + post (hoare_of_contract doors_c + (A := bool) (inj_p (IsOpen d))) ω opened ω' <-> + post (@ret (hoare Ω) bool (sel d ω)) ω opened ω'. Proof. - prove impure with airlock; subst ; constructor. +rewrite doors_post_condE; + split=> [ [-> callee] | [<- <-] ]; + split=> //. +- by inversion callee; ssubst. +- exact: doors_o_callee_is_open. +Qed. - (* This leaves us with one goal to prove: +Lemma doors_is_open_preE : + pre (hoare_of_contract doors_c + (A := bool) (inj_p (IsOpen d))) ω <-> + pre (@ret (hoare Ω) bool (sel d ω)) ω. +Proof. +by split=> // _; + rewrite doors_pre_condE; + exact: req_is_open. +Qed. - [sel d ω = false -> sel (co d) ω = false] +Lemma doors_toggle_postE (u : unit) (ω' : Ω) : + post (hoare_of_contract doors_c + (A := unit) (inj_p (Toggle d))) ω u ω' <-> + ω' = tog d ω. +Proof. +by rewrite doors_post_condE; + split=> [ [-> _] | ->] //; split=>//; + exact: doors_o_callee_toggle. +Qed. - Yet, thanks to our call to [IsOpen d], we can predict that +Lemma doors_toggle_preE + (* Safe means : door 1 is closed -> door 2 is closed *) + (* Previous: (safe : sel d ω = false -> sel (co d) ω = false) *) + (safe : sel (co d) ω -> sel d ω) : + pre (hoare_of_contract doors_c + (A := unit) (inj_p (Toggle d))) ω <-> + pre (@ret (hoare Ω) unit tt) ω. +Proof. +by split=> // _; + rewrite doors_pre_condE; + exact: req_toggle safe. +Qed. +End IntermLemmaS. - [sel d ω = true] *) +Local Open Scope classical_set_scope. - inversion o_caller0; ssubst. - now rewrite H3. +Remark one_door_safe_all_doors_safe (ω : Ω) (d : door) + (safe : ~~sel d ω \/ ~~sel (co d) ω) + : forall (d' : door), ~~sel d' ω \/ ~~sel (co d') ω. +Proof. +by move: d safe=> + /[swap]; case; case=>//=; rewrite or_comm. Qed. - Hint Resolve close_door_respectful : airlock. +Definition doors_safe (ω : Ω) := ~~ sel left ω \/ ~~ sel right ω. -Lemma open_door_respectful `{Provide ix DOORS} (ω : Ω) - (d : door) (safe : sel (co d) ω = false) - : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract (open_door (ix := ix) d)) ω. +Section RespectfulAndRunLemmas. +Context `{Provide Fx DOORS} {im : freerMonad Fx}. +Local Notation "p ||> c" := (to_hoare (im:=im) c p) + (at level 50, no associativity). +(** Closing a door [d] in any system [ω] is always a respectful operation. *) +Lemma close_door_respectful (d : door) : + pre (close_door d ||> doors_c) = [set: _]. Proof. - prove impure; repeat constructor; subst. - by inversion o_caller0; ssubst. +rewrite /close_door -subTset=> ω _; apply: th_pre_bindA. +- by rewrite to_hoare_requestE doors_is_open_preE. +case=> ?; + rewrite to_hoare_when_preE // to_hoare_requestE doors_is_open_post_retE + => -[? <-]. +by rewrite to_hoare_requestE; + apply/(doors_toggle_preE ω d). Qed. - Hint Resolve open_door_respectful : airlock. - -Lemma close_door_run `{Provide ix DOORS} (ω : Ω) (d : door) (ω' : Ω) (x : unit) - (run : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract (close_door d)) ω x ω') - : sel d ω' = false. +Lemma open_door_respectful (ω : Ω) (d : door) (safe : ~~ sel (co d) ω) : + pre (open_door d ||> doors_c) ω. Proof. - run_simpl run; - cleanvert H1. - cleanvert run. - cleanvert H1. - run_simpl H2. - - cleanvert H2. - (* cleanvert H4. *) - - - cleanvert H1. - by rewrite tog_equ_1 H5. - by cleanvert run. +rewrite /open_door; apply: th_pre_bindA. +- by rewrite to_hoare_requestE doors_is_open_preE. +case=> ?; + rewrite to_hoare_when_preE // to_hoare_requestE doors_is_open_post_retE + => -[_ <-]. +rewrite to_hoare_requestE; + apply/(doors_toggle_preE ω d)=>//. +by move: safe=> /[swap] ->. Qed. - Hint Resolve close_door_run : airlock. +Lemma close_door_run (ω : Ω) (d : door) (ω' : Ω) (x : unit) + (run : post (close_door d ||> doors_c) ω x ω') : +~~ sel d ω'. +Proof. +move: run; rewrite /close_door th_post_bindA. +move=> [opened [? [ ]]]. +rewrite to_hoare_requestE doors_is_open_post_retE to_hoare_when_postE + => -[+ <-]. +case: opened=> [ + [[]] | /[swap] -> -> ] //. +by rewrite to_hoare_requestE doors_toggle_postE + => /[swap] ->; + rewrite tog_equ_1=> ->. +Qed. -#[local] Opaque close_door. -#[local] Opaque open_door. -#[local] Opaque Nat.ltb. +Opaque close_door. +Opaque open_door. +Opaque Nat.ltb. +Opaque sel. -Remark one_door_safe_all_doors_safe (ω : Ω) (d : door) - (safe : sel d ω = false \/ sel (co d) ω = false) - : forall (d' : door), sel d' ω = false \/ sel (co d') ω = false. +Lemma doors_request_preserves_safe + `(op : Fx a) (ω : Ω) (x : a) (ω' : Ω) : + pre (trigger op ||> doors_c) ω -> + post (trigger op ||> doors_c) ω x ω' -> + doors_safe ω -> doors_safe ω'. +Proof. +rewrite to_hoare_requestE doors_effect_preE doors_effect_postE. +case: (proj_p op)=> [door_op |] /=; last first. +- by move=> _ ->. +move=> + [-> _]. +move: door_op x; case=> d [] caller safe //=. +apply: (one_door_safe_all_doors_safe _ d). +move: safe=> /one_door_safe_all_doors_safe /(_ d). +case=> [d_closed | ?]; right; rewrite tog_equ_2 //. +apply/negP=> co_open; move/negP: d_closed=> d_closed. +by inversion caller as [|?? Hsafe]; subst; + move: co_open Hsafe d_closed=> -> ->. +Qed. +Lemma doors_handler_preserves_safe `(op : Fx a) : + preserves_invariant doors_safe (hoare_of_contract doors_c op). Proof. - intros d'. - destruct d; destruct d'; auto. - + cbn -[sel]. - now rewrite or_comm. - + cbn -[sel]. - fold (co right). - now rewrite or_comm. +move=> ??? Hpre Hpost; apply/doors_request_preserves_safe ; + rewrite to_hoare_requestE. +- exact: Hpre. +- exact: Hpost. Qed. -(** The objective of this lemma is to prove that, if either the right door or - the left door is closed, then after any respectful run of a computation - [p] that interacts with doors, this fact remains true. *) - -#[local] Opaque sel. - -Lemma respectful_run_inv `{Provide ix DOORS} {A} (p : impure ix A) - (ω : Ω) (safe : sel left ω = false \/ sel right ω = false) - (a : A) (ω' : Ω) - (hpre : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract p) ω) - (hpost: post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract p) ω a ω') - : sel left ω' = false \/ sel right ω' = false. - -(** We reason by induction on the impure computation [p]: - - - Either [p] is a local, pure computation; in such a case, the doors state - does not change, hence the proof is trivial. - - - Or [p] consists in a request to the doors interface, and a continuation - whose domain satisfies the theorem, i.e. it preserves the invariant that - either the left or the right door is closed. Due to this hypothesis, we - only have to prove that the first request made by [p] does not break the - invariant. We consider two cases. - - - Either the computation asks for the state of a given door ([IsOpen]), - then again the doors state does not change and the proof is trivial. - - Or the computation wants to toggle a door [d]. We know by hypothesis - that either [d] is closed or [d] is open (thanks to the - [one_door_safe_all_doors_safe] result and the [safe] hypothesis). - Again, we consider both cases. - - - If [d] is closed —and therefore will be opened—, then because we - consider a respectful run, [co d] is necessarily closed too (it is a - requirements of [door_contract]). Once [d] is opened, [co d] is still - closed. - - Otherwise, [co d] is closed, which means once [d] is toggled (no - matter its initial state), then [co d] is still closed. - - That is, we prove that, when [p] toggles [d], [co d] is necessarily - closed after the request has been handled. Because there is at least - one door closed ([co d]), we can conclude that either the right or the - left door is closed thanks to [one_door_safe_all_doors_safe]. *) +(** /!\ WARNING: This proof exits the Equational Reasoning. + * This is a known issue. I need to find a way to remove this + * induction but can't find one right now. + *) +Lemma doors_run_preserves_safe `(p : freer Fx A) : + preserves_invariant doors_safe (p |> doors_c). +Proof. +elim: p=> [value | X op k IH]. +- exact: preserves_invariant_ret. +by apply: preserves_invariant_bind=>//; + exact: doors_handler_preserves_safe. +Qed. +Lemma respectful_run_inv `(p : im A) + (ω : Ω) (safe : ~~ sel left ω \/ ~~ sel right ω) + (a : A) (ω' : Ω) + (hpre : pre (p |> doors_c) ω) + (hpost : post (p |> doors_c) ω a ω') : + ~~ sel left ω' \/ ~~ sel right ω'. Proof. - fold (co left) in *. - revert ω hpre hpost safe. - (* elim p=>[a'|B e f IH] ω pre run safe. *) - induction p; intros ω hpre run safe. - + by unroll_post run. - + run_simpl run. - have hpost : post (interface_to_hoare doors_contract (A:=β) e) ω x ω0 - by split; [apply H2| by rewrite H3]. - (* move: H1 => /(_ x ω0) => H1. *) - apply/(H1 x ω0) => //; [by apply hpre|]. - cbn in *. - inversion hpre; rewrite /=/gen_caller_obligation in H4. - (* simplify_gens *) - unfold gen_caller_obligation, gen_callee_obligation, gen_witness_update in *. - cbn in *. - destruct (proj_p e) as [e'|]. - ++ destruct hpost as [o_callee equω]. - destruct e' as [d|d]. - +++ rewrite H3. - apply safe. - +++ apply one_door_safe_all_doors_safe with (d := d); - apply one_door_safe_all_doors_safe with (d' := d) in safe; - subst. - inversion H4. - cbn. - by destruct safe as [safe|safe]; - right; rewrite tog_equ_2//. - ++ rewrite H3; - exact: safe. +by move: hpre hpost safe; + (** /!\ WARNING: Reifying bridge used here. + * This currently holds only with a known + * instance of FreerMonad being Freer (and + * not for all Freer Monads...). + *) + rewrite -ToHoareFreerBridge.to_hoare_reifyE; + exact: doors_run_preserves_safe. Qed. +End RespectfulAndRunLemmas. (** ** Main Theorem *) -Definition correct_component `{MayProvide jx j} - `(c : component i jx) `(ci : contract i Ωi) `(cj : contract j Ωj) - (pred : Ωi -> Ωj -> Prop) - : Prop := - forall (ωi : Ωi) (ωj : Ωj) (init : pred ωi ωj) - `(e : i α) (o_caller : caller_obligation ci ωi e), - pre (to_hoare cj $ c α e) ωj /\ - forall (x : α) (ωj' : Ωj) (run : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure jx) cj $ c α e) ωj x ωj'), - callee_obligation ci ωi e x /\ pred (witness_update ci ωi e x) ωj'. - - - -Lemma controller_correct `{StrictProvide2 ix DOORS (STORE nat)} - : correct_component controller - (no_contract CONTROLLER) - doors_contract - (fun _ ω => sel left ω = false \/ sel right ω = false). +Section controller_s. +Context `{StrictProvide2 Fx DOORS (STORE nat)} {im : freerMonad Fx}. + +Lemma controller_pre `(op: CONTROLLER α) (ω : Ω) + : pre ((controller (im:=im) α op) |> doors_c) ω. Proof. - move=>ωc ωd pred A eff req. - have hpre : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) doors_contract (controller A eff)) ωd. - { - case eff; do ! [prove impure with airlock; ssubst; constructor => //]. - - - (* case eff=> [|d]//; prove impure with airlock; ssubst; constructor=>//. *) - (* do ! [prove impure with airlock; ssubst; constructor=>//=]. *) - - by inversion o_caller; ssubst; rewrite H6. - - by inversion o_caller1; ssubst; rewrite H6. - - by inversion o_caller0; ssubst; rewrite H6. - - by inversion o_caller; ssubst; rewrite H6. - - by inversion o_caller1; ssubst;inversion o_caller; ssubst; rewrite H6 tog_equ_1/=H7. - - by inversion o_caller; ssubst. - } - - split=>[|a ωj' run]//=; - split=>//=. - by apply/(respectful_run_inv _ _ _ _ _ _ run). +case: op=> [|d]. +- (* Tick *) apply: th_pre_bindA. + + exact: to_hoare_distinguished_request_preI. + + move=> cpt? /to_hoare_distinguished_request_postE ->. + rewrite to_hoare_when_preE; + case: (15 //=; + apply: th_pre_bindA. + * by apply: th_pre_bindA=>[|*]; + rewrite close_door_respectful. + * by move=>*; + exact: to_hoare_distinguished_request_preI. +- (* Request Open *) apply: th_pre_bindA=>[|*]. + + apply: th_pre_bindA. + * by rewrite close_door_respectful. + * by move=>?? Hclose; exact/open_door_respectful/close_door_run/Hclose. + + exact: to_hoare_distinguished_request_preI. Qed. + +Theorem controller_correct + : correct_component controller (im:=im) + (no_contract CONTROLLER) doors_c (fun=> doors_safe). +Proof. +move=>? ω ?? op _; split=> [|?? Hpost]; [exact: controller_pre|split=> //]. +have Hpre := controller_pre op ω; move: Hpre Hpost. +exact: respectful_run_inv. +Qed. + +End controller_s. diff --git a/examples/ping/lossy_round_trip.v b/examples/ping/lossy_round_trip.v new file mode 100644 index 0000000..acac231 --- /dev/null +++ b/examples/ping/lossy_round_trip.v @@ -0,0 +1,360 @@ +(* Monae version poc *) +From mathcomp Require Import ssreflect ssrbool eqtype ssrnum ssralg reals sequences + interval_inference. +From infotheo Require Import realType_ext. +From monae Require Import preamble hierarchy monad_lib proba_lib proba_model. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope monae_scope. +Local Open Scope proba_scope. +Local Open Scope proba_monad_scope. +Local Open Scope mprog. +Local Open Scope ring_scope. +Local Open Scope reals_ext_scope. + +Import GRing.Theory. + +Module LossyRoundTripMod. + +Section lossy_round_trip_sec. + Context {R : realType} {M : probMonad R}. + + Inductive packet := Ping | Pong. + + Inductive outcome := + | GotPong + | LostPing + | LostPong. + + Definition transmit (delivery : {prob R}) (m : packet) : M (option packet) := + Ret (Some m) <| delivery |> Ret None. + + Definition client_send (delivery : {prob R}) : M (option packet) := + transmit delivery Ping. + + Definition server_reply (delivery : {prob R}) (incoming : option packet) + : M (option packet) := + match incoming with + | Some Ping => transmit delivery Pong + | Some Pong => Ret None + | None => Ret None + end. + + Definition client_receive (incoming : option packet) : M outcome := + match incoming with + | Some Pong => Ret GotPong + | Some Ping => Ret LostPong + | None => Ret LostPong + end. + + Definition ping_pong_once (delivery : {prob R}) : M outcome := + client_send delivery >>= fun to_server => + match to_server with + | Some Ping => server_reply delivery to_server >>= client_receive + | Some Pong => Ret LostPing + | None => Ret LostPing + end. + + Fixpoint ping_pong_retry (delivery : {prob R}) (fuel : nat) : M outcome := + match fuel with + | O => ping_pong_once delivery + | S fuel' => + ping_pong_once delivery >>= fun result => + match result with + | GotPong => Ret GotPong + | LostPing | LostPong => ping_pong_retry delivery fuel' + end + end. + + (* --- Probabilites --- *) + + (* q^2 *) + Definition round_trip_success_probability (p : {prob R}) : {prob R} := + (* let delivery := loss%:num.~%:i01 in *) + [p_of p, p]. + + Definition retry_step_probability (delivery retry : {prob R}) : {prob R} := + [s_of (round_trip_success_probability delivery), retry]. + + (* q ^ n *) + Fixpoint retry_success_probability (loss : {prob R}) (n : nat) : {prob R} := + match n with + | O => round_trip_success_probability loss + | S n' => + retry_step_probability loss (retry_success_probability loss n') + end. + + (* --- Event distribution --- *) + + Definition one_attempt_distribution (p : {prob R}) : M outcome := + (Ret GotPong <| p |> Ret LostPong) <| p |> Ret LostPing. + + Fixpoint retry_success_distribution (loss : {prob R}) (n : nat) : M outcome := + match n with + | O => one_attempt_distribution loss + | S n' => + (Ret GotPong <| loss |> retry_success_distribution loss n') <| loss |> + retry_success_distribution loss n' + end. + + (* --- Event coercion --- *) + + Definition success_event : pred outcome := fun result => + match result with + | GotPong => true + | LostPing | LostPong => false + end. + + (* Mapping to bcoin equiv *) + Definition success_of (run : M outcome) : M bool := + run >>= fun result => Ret (success_event result). + + Definition ping_pong_once_success (p : {prob R}) : M bool := + success_of (ping_pong_once p). + + Definition ping_pong_retry_success (p : {prob R}) (fuel : nat) : M bool := + success_of (ping_pong_retry p fuel). + + (* --- Unfolding lemmas --- *) + + Lemma transmitE delivery m : + transmit delivery m = (Ret (Some m) <| delivery |> Ret None :> M _). + Proof. by []. Qed. + + Lemma client_sendE delivery : + client_send delivery = transmit delivery Ping. + Proof. by []. Qed. + + Lemma server_replyE delivery incoming : + server_reply delivery incoming = + match incoming with + | Some Ping => transmit delivery Pong + | Some Pong | None => Ret None + end. + Proof. by case: incoming => [[]|]. Qed. + + Lemma client_receiveE incoming : + client_receive incoming = + Ret match incoming with + | Some Pong => GotPong + | Some Ping | None => LostPong + end. + Proof. by case: incoming => [[]|]. Qed. + + Lemma ping_pong_onceE delivery : + ping_pong_once delivery = + client_send delivery >>= fun to_server => + match to_server with + | Some Ping => + server_reply delivery to_server >>= client_receive + | Some Pong | None => Ret LostPing + end. + Proof. by []. Qed. + + Lemma ping_pong_retryE delivery fuel : + ping_pong_retry delivery fuel = + match fuel with + | O => ping_pong_once delivery + | S fuel' => + ping_pong_once delivery >>= fun result => + match result with + | GotPong => Ret GotPong + | LostPing | LostPong => ping_pong_retry delivery fuel' + end + end. + Proof. by case: fuel. Qed. + + Lemma ping_pong_retry_stepE delivery fuel : + ping_pong_retry delivery (S fuel) = + (Ret GotPong <| delivery |> ping_pong_retry delivery fuel) <| delivery |> + ping_pong_retry delivery fuel. + Proof. + rewrite ping_pong_retryE ping_pong_onceE client_sendE !transmitE. + rewrite !choice_bindDl !bindretf server_replyE !transmitE. + by rewrite !choice_bindDl !bindretf. + Qed. + + Lemma round_trip_success_probabilityE p : + round_trip_success_probability p = [p_of p, p]. + Proof. by []. Qed. + + Lemma retry_step_probabilityE delivery retry : + retry_step_probability delivery retry = + [s_of (round_trip_success_probability delivery), retry]. + Proof. by []. Qed. + + Lemma retry_success_probabilityE loss n : + retry_success_probability loss n = + match n with + | O => round_trip_success_probability loss + | S n' => retry_step_probability loss (retry_success_probability loss n') + end. + Proof. by case: n. Qed. + + Lemma retry_success_probability_stepE loss n : + retry_success_probability loss (S n) = + [s_of [p_of loss, loss], retry_success_probability loss n]. + Proof. + by rewrite retry_success_probabilityE retry_step_probabilityE + round_trip_success_probabilityE. + Qed. + + Lemma one_attempt_distributionE p : + one_attempt_distribution p = + (Ret GotPong <| p |> Ret LostPong) <| p |> Ret LostPing :> M _. + Proof. by []. Qed. + + Lemma retry_success_distributionE loss n : + retry_success_distribution loss n = + match n with + | O => one_attempt_distribution loss + | S n' => + (Ret GotPong <| loss |> retry_success_distribution loss n') <| loss |> + retry_success_distribution loss n' + end. + Proof. by case: n. Qed. + + Lemma success_eventE result : + success_event result = + match result with + | GotPong => true + | LostPing | LostPong => false + end. + Proof. by case: result. Qed. + + Lemma success_ofE run : + success_of run = (run >>= fun result => Ret (success_event result)). + Proof. by []. Qed. + + Lemma ping_pong_once_successE p : + ping_pong_once_success p = success_of (ping_pong_once p). + Proof. by []. Qed. + + Lemma ping_pong_retry_successE p fuel : + ping_pong_retry_success p fuel = success_of (ping_pong_retry p fuel). + Proof. by []. Qed. + + Lemma ping_pong_retry_success_stepE p fuel : + ping_pong_retry_success p (S fuel) = + (Ret true <| p |> ping_pong_retry_success p fuel) <| p |> + ping_pong_retry_success p fuel. + Proof. + rewrite ping_pong_retry_successE success_ofE ping_pong_retry_stepE. + rewrite !choice_bindDl !bindretf success_eventE. + by rewrite -!success_ofE -!ping_pong_retry_successE. + Qed. + + Lemma bcoinE p : + bcoin p = (Ret true <| p |> Ret false :> M bool). + Proof. by rewrite /bcoin. Qed. + + (* === Proofs === *) + + (* p = 1 *) + + Fact transmit_certain m : + transmit 1%:i01 m = Ret (Some m) :> M _. + Proof. + by rewrite transmitE choice1. + Qed. + + Fact ping_pong_once_certain : + ping_pong_once 1%:i01 = Ret GotPong :> M _. + Proof. + by rewrite ping_pong_onceE client_sendE transmit_certain bindretf + server_replyE transmit_certain bindretf client_receiveE. + Qed. + + Fact ping_pong_retry_certain fuel : + ping_pong_retry 1%:i01 fuel = Ret GotPong :> M _. + Proof. + by elim : fuel => [|n IH]; + rewrite ping_pong_retryE ping_pong_once_certain ?bindretf. + Qed. + + (* == One round == *) + + Lemma ping_pong_once_distribution_shape (loss : {prob R}) : + ping_pong_once (loss%:num.~%:i01) = one_attempt_distribution (loss%:num.~%:i01). + Proof. + by rewrite ping_pong_onceE one_attempt_distributionE client_sendE !transmitE + !choice_bindDl !bindretf server_replyE !transmitE + !choice_bindDl !bindretf client_receiveE. + Qed. + + Lemma ping_pong_once_success_probability (loss : {prob R}) : + ping_pong_once_success (loss%:num.~%:i01) = + bcoin (round_trip_success_probability (loss%:num.~%:i01)). + Proof. + rewrite ping_pong_once_successE success_ofE ping_pong_once_distribution_shape. + rewrite one_attempt_distributionE round_trip_success_probabilityE bcoinE + !choice_bindDl !bindretf !success_eventE. + + set d := loss%:num.~%:i01. + have [->/=|d0] := eqVneq d 0%:i01. + - by rewrite p_of_0s !choice0. + have [->/=|d1] := eqVneq d 1%:i01. + - by rewrite p_of_1s choice1. + have p1 : [p_of d, d] != 1%:i01 by rewrite p_of_rs1 (negbTE d1) andbF. + (* Give RHS the same form as LHS *) + rewrite -[Ret false in RHS](choicemm [q_of d, d]). + + by rewrite choiceA (s_of_pqK p1) (r_of_pqK p1 d0). + Qed. + + (* == Multiple rounds *) + + Fact bcoin_or_true (p q : {prob R}) : + Ret true <| p |> bcoin q = bcoin [s_of p, q] :> M bool. + Proof. + by rewrite !bcoinE choiceA choicemm. + Qed. + + Fact retry0 : forall n, retry_success_probability (widen_itv 0%:itv) n = 0%:i01. + Proof. + elim=> [|n IH]. + - by rewrite retry_success_probabilityE round_trip_success_probabilityE p_of_0s. + by rewrite retry_success_probability_stepE p_of_0s s_of_0q IH. + Qed. + + Fact retry1 : forall n, retry_success_probability (widen_itv 1%:itv) n = 1%:i01. + Proof. + case=> [|n]. + - by rewrite retry_success_probabilityE round_trip_success_probabilityE p_of_1s. + by rewrite retry_success_probability_stepE p_of_1s s_of_1q. + Qed. + + Lemma ping_pong_retry_distribution_shape (loss : {prob R}) (fuel : nat) : + ping_pong_retry (loss%:num.~%:i01) fuel = retry_success_distribution (loss%:num.~%:i01) fuel. + Proof. + elim : fuel => [|n IH]. + - exact: ping_pong_once_distribution_shape. + by rewrite ping_pong_retry_stepE retry_success_distributionE IH. + Qed. + + Theorem ping_pong_retry_success_probability (delivery : {prob R}) (fuel : nat) : + ping_pong_retry_success (delivery%:num.~%:i01) fuel = + bcoin (retry_success_probability (delivery%:num.~%:i01) fuel). + Proof. + elim : fuel => [|n]. + - exact: ping_pong_once_success_probability. + rewrite ping_pong_retry_success_stepE retry_success_probability_stepE => ->. + + set d := delivery%:num.~%:i01. + + have [->/=|d0] := eqVneq d 0%:i01. + - by rewrite !bcoinE p_of_0s s_of_0q retry0 !choice0. + have [->/=|d1] := eqVneq d 1%:i01. + - by rewrite !bcoinE p_of_1s s_of_1q retry1 !choice1. + + rewrite -(bcoin_or_true [p_of d, d] (retry_success_probability d n)). + have p1 : [p_of d, d] != 1%:i01 by rewrite p_of_rs1 (negbTE d1) andbF. + rewrite -[bcoin (retry_success_probability d n) in RHS](choicemm [q_of d, d]). + by rewrite choiceA (s_of_pqK p1) (r_of_pqK p1 d0). + Qed. + +End lossy_round_trip_sec. +End LossyRoundTripMod. diff --git a/examples/prob_airlock.v b/examples/prob_airlock.v deleted file mode 100644 index 6a72df2..0000000 --- a/examples/prob_airlock.v +++ /dev/null @@ -1,188 +0,0 @@ -(* This Source Code Form is subject to the terms of the Mozilla Public - * License, v. 2.0. If a copy of the MPL was not distributed with this - * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) - -(* Copyright (C) 2018–2020 ANSSI *) - -From Stdlib Require Import Arith. -From FreerDPS Require Import Core Impure Hoare. -From monae Require Import preamble hierarchy. - -From mathcomp Require Import unstable mathcomp_extra ring lra reals Rstruct. -From infotheo Require Import realType_ext ssr_ext fsdist convex. -#[local] Open Scope nat_scope. -#[local] Open Scope monae_scope. -#[local] Open Scope proba_scope. -Local Open Scope reals_ext_scope. - - - -Create HintDb airlock. - -(** * Specifying *) - -(** ** Doors *) - -Locate not_locked_false_eq_true. - -Ltac done := - trivial; hnf; intros; solve - [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial] - | discriminate | contradiction | split] - | match goal with H : ~ _ |- _ => solve [case H; trivial] end - | auto with freespec - ]. -Generalizable All Variables. -Arguments request {_ } _ _ _. - -Module ProbIfaceMod. - Section prob_sec. - Context {R : realType}. -Inductive prob_interface : interface := -| CanWork (p : {prob R}) : prob_interface bool -. - -Definition can_work `{Provide ix prob_interface} {im : impureMonad ix} (p:{prob R}) : im bool := ( trigger (inj_p $ CanWork p)). - - End prob_sec. -End ProbIfaceMod. - -Import ProbIfaceMod. - -Inductive door : Type := left | right. - -Definition door_eq_dec (d d' : door) : { d = d' } + { ~ d = d' } := - ltac:(decide equality). - -Inductive DOORS : interface := -| IsOpen : door -> DOORS bool -| Toggle : door -> DOORS unit. - - - -Check request. - -Section a. - - Context (R : realType). - -Definition is_open `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im bool := trigger (inj_p $ IsOpen d). - -Definition toggle `{Provide ix DOORS} {im : impureMonad ix} (d : door) : im unit := trigger (inj_p $ Toggle d). - -Definition open_door `{Provide2 ix DOORS prob_interface} {im : impureMonad ix} (d : door) (p : {prob R}) : im unit := - can_work p >>= fun ok => when ok $ - is_open d >>= fun open => - when (negb open) (toggle d). - -Definition close_door `{Provide2 ix DOORS prob_interface} {im : impureMonad ix} (d : door) (p: {prob R}): im unit := - can_work p >>= fun ok => when ok $ - is_open d >>= fun open => - when open (toggle d). - -(** ** Controller *) - -Inductive CONTROLLER : interface := -| Tick : CONTROLLER unit -| RequestOpen (d : door) : CONTROLLER unit. - -Definition tick `{Provide ix CONTROLLER} {im : impureMonad ix} : im unit := - trigger (inj_p Tick). - -Definition request_open `{Provide ix CONTROLLER} {im : impureMonad ix} (d : door) : im unit := - trigger (inj_p $ RequestOpen d). - -Definition co (d : door) : door := - match d with - | left => right - | right => left - end. - -Check (forall i, component CONTROLLER i). - -Search iget. - -Definition controller `{Provide ix DOORS, Provide ix (STORE nat), Provide ix prob_interface} {im : impureMonad ix} - : {prob R} -> component (im:=im) CONTROLLER ix - (* . - move=>X; case=>[|d]. - - apply/bind=>[|cpt]. - + apply/iget. - + apply/when. - * apply: (15 [|_]. - -- apply/close_door/left. - -- apply/bind=>[|_]. - ++ apply/close_door/right. - ++ apply/iput/0. - - apply/bind=>[|_]. - + apply/close_door/co/d. - + apply/bind=>[|_]. - * apply/open_door/d. - * apply/iput/0. - Show Proof. *) - := - fun p _ op => - match op with - | Tick => - iget >>= fun cpt => - when (15 > - close_door right p >> - iput 0 - | RequestOpen d => - close_door (co d) p >> - open_door d p >> - iput 0 - end. - -(** * Verifying the Airlock Controller *) - -(** ** Doors Specification *) - -(** *** Witness States *) - -Definition Ω : Type := bool * bool. - -Definition sel (d : door) : Ω -> bool := - match d with - | left => fst - | right => snd - end. - -Definition tog (d : door) (ω : Ω) : Ω := - match d with - | left => (negb (fst ω), snd ω) - | right => (fst ω, negb (snd ω)) - end. - -Lemma tog_equ_1 (d : door) (ω : Ω) - : sel d (tog d ω) = negb (sel d ω). - -Proof. - by case:d. -Qed. - -Lemma tog_equ_2 (d : door) (ω : Ω) - : sel (co d) (tog d ω) = sel (co d) ω. - -Proof. - destruct d; reflexivity. -Qed. - -(** From now on, we will reason about [tog] using [tog_equ_1] and [tog_equ_2]. - FreeSpec tactics rely heavily on [cbn] to simplify certain terms, so we use - the <> options of the [Arguments] vernacular command to prevent - [cbn] from unfolding [tog]. - - This pattern is common in FreeSpec. Later in this example, we will use this - trick to prevent [cbn] to unfold impure computations covered by intermediary - theorems. *) - -#[local] Opaque tog. - -Definition step (ω : Ω) (a : Type) (e : DOORS a) (x : a) := - match e with - | Toggle d => tog d ω - | _ => ω - end. diff --git a/freer_playground/_CoqProject b/freer_playground/_CoqProject deleted file mode 100644 index fa9ab22..0000000 --- a/freer_playground/_CoqProject +++ /dev/null @@ -1,7 +0,0 @@ --Q theories FreerTheories --arg -w -arg -projection-no-head-constant - -./theories/FreerMonad.v -./theories/FlipMonad.v -./theories/lib/ActoFreerCoproduct.v -./theories/lib/FreerFlip.v diff --git a/freer_playground/theories/FlipMonad.v b/freer_playground/theories/FlipMonad.v deleted file mode 100644 index 586d42d..0000000 --- a/freer_playground/theories/FlipMonad.v +++ /dev/null @@ -1,201 +0,0 @@ -Ltac typeof X := type of X. - -From Stdlib Require Import ssrmatching Reals. -From mathcomp Require Import ssreflect ssrbool ssralg reals. -From infotheo Require Import realType_ext. - -From HB Require Import structures. -From monae Require Import preamble hierarchy monad_lib proba_lib proba_model. - - -Local Open Scope monae_scope. -Local Open Scope proba_scope. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Local Open Scope reals_ext_scope. - -(* 1st step : FlipMonad *) -HB.mixin Record isMonadFlip {R : realType} (M : UU0 -> UU0) of Monad M := { - flip : forall (p : {prob R}), M bool ; - (* identity axiom *) - flip1 : flip 1%:pr = Ret true ; - (* skewed commutativity *) - flipNeg : forall (p: {prob R}), flip p = flip (Prob.p p).~%:pr >>= (fun x => Ret (~~x)) ; - (* idempotence *) - flipmm : forall (A:UU0) p (a:M A), flip p >> a = a ; - (* quasi associativity *) - (* flipA : forall (p q r s : {prob R}), - flip p >>= (fun a => flip q >>= (fun b => Ret ))) - = flip [r_of p, q] >>= (fun a => flip [s_of p, q] >>= (fun b => Ret (a && b))) *) - fA0:forall (T:UU0) (p q r s : {prob R}) (a b c : M T), - (* Prob.p p = (Prob.p r * Prob.p s)%R :> R -> ((Prob.p s).~ = (Prob.p p).~ * (Prob.p q).~)%R -> *) -flip p >>= (fun x => if x then a else flip q >>= (fun x0 => if x0 then b else c)) = -flip [s_of p, q] >>= - (fun x => if x then flip [r_of p, q] >>= (fun x0 => if x0 then a else b) else c) ; -}. - -#[short(type=flipMonad)] -HB.structure Definition MonadFlip {R : realType} := {M of isMonadFlip R M & }. - -Local Open Scope reals_ext_scope. - -Module FlipLib. - (* =========== correct =========== *) - Section proba2flipM. - Variable R : realType. - Variable M : probMonad R. - - Let flip_c (p : {prob R}) : M bool := bcoin p. - - -(*** identity laws ***) -Let flip1 : flip_c 1%:pr = Ret true. -Proof. exact: choice1. Qed. - -(*** negation law ***) -Let flipNeg : forall p, flip_c p = (flip_c ((Prob.p p).~ %:pr)) >>= (fun x => Ret (~~ x)). -Proof. - by move=>p; rewrite /flip_c/bcoin-choiceC choice_bindDl!bindretf. -Qed. - -(*** skewed commutativity law ***) -Let flipmm : forall (A:UU0) (p:{prob R}) (a : M A), flip_c p >> a = a. -Proof. - move=>A p a; rewrite/flip_c/bcoin choice_bindDl 2!bindretf. - exact: choicemm. -Qed. - -(*** quasi assoc law ***) -Let flipA : forall (T:UU0) (p q r s : {prob R}) (a b c : M T), - flip_c p >>= (fun x : bool => if x then a else flip_c q >>= (fun x0 : bool => if x0 then b else c)) - = flip_c [s_of p, q] >>= (fun x : bool => if x then flip_c [r_of p, q] >>= (fun x0 : bool => if x0 then a else b) else c). -Proof. - move=>T p q r s a b c. - rewrite /flip_c/bcoin!choice_bindDl!bindretf. - exact:choiceA. -Qed. - - #[non_forgetful_inheritance] - HB.instance Definition t_ := isMonadFlip.Build R M flip1 flipNeg flipmm flipA. - - End proba2flipM. - - (* =========== complete =========== *) - Section flip2probaM. - Variable R : realType. - Variable M : flipMonad R. - -Let choicef (p : {prob R}) (A:UU0) (a b : M A) : M A := flip p >>= (fun x => if x then a else b). - - - -(*** identity laws ***) -Let choice1 : forall (A:UU0) (a b : M A), choicef 1%:pr a b = a. -Proof. - move=>A a b/=. by rewrite /choicef flip1 bindretf. -Qed. - -(*** negation law ***) -Let choiceC : forall (A : UU0) (p:{prob R}) (a b : M A), choicef p a b = choicef ((Prob.p p).~ %:pr) b a. -Proof. - move=> A p a b. - rewrite /choicef flipNeg bindA. - congr (flip _ >>= _). - by apply/boolp.funext=>x; - rewrite bindretf if_neg. -Qed. - - -(*** skewed commutativity law ***) -Let choicemm : forall (A : UU0) (p : {prob R}) (a : M A), choicef p a a = a. -Proof. - move=>A p a. - rewrite /choicef -{3}(flipmm A p a). - congr (flip p >> _). - apply/boolp.funext=>x; - exact/if_same. -Qed. - -(*** quasi assoc law ***) -Let choiceA : - forall (T : UU0) (p q : {prob R}), - forall a b c : M T, - choicef p a (choicef q b c) = - choicef [s_of p, q] (choicef [r_of p, q] a b) c. -Proof. - by rewrite/choicef=>A p q a b c; apply: fA0. -Qed. - -Set Warnings "-redundant-canonical-projection". - - #[non_forgetful_inheritance] - HB.instance Definition _ := isMonadConvex.Build R M choicef choice1 choiceC choicemm choiceA. - -Let prob_bindDl p : - BindLaws.left_distributive ( @hierarchy.bind M) (fun A => @choicef p A). -Proof. -move=> A B m1 m2 k. -rewrite !/choicef bindA. -congr (flip p >>= _). -by apply/boolp.funext; case. -Qed. - - #[non_forgetful_inheritance] -HB.instance Definition _ := isMonadProb.Build R M prob_bindDl. - - End flip2probaM. -End FlipLib. - -HB.export FlipLib. - -Module FlipModel. - (* === test with ret/bind === *) -Section ConcreteFlip. - Variable R : realType. - - Definition flipacto := MonadProbModel.acto R. - - -Notation pr := (probMonad R). - -Definition cflip (p : {prob R}) := @bcoin R flipacto p. - -(*** identity laws ***) -Let flip1 : @cflip 1%:pr = ret R bool true. -Proof. exact: choice1. Qed. - -Ltac rw_choicebind_dl:=rewrite /cflip choice_bindDl!bindretf/=. - -(*** negation law ***) -Let flipNeg : forall p, cflip p = (cflip ((Prob.p p).~ %:pr) >>= (fun x => ret R bool (~~ x))). -Proof. - move=>p. - rw_choicebind_dl; - exact: choiceC. -Qed. - - -(*** skewed commutativity law ***) -Let flipmm : forall (A:UU0) (p:{prob R}) (a : flipacto A), (cflip p >>= (fun _ => a)) = a. -Proof. - move=>A p a. - rw_choicebind_dl; exact:choicemm. -Qed. - -(*** quasi assoc law ***) -Let flipA : forall (T:UU0) (p q r s : {prob R}) (a b c : flipacto T), - (cflip p >>= (fun x : bool => if x then a else (cflip q >>= (fun x0 : bool => if x0 then b else c)))) - = (cflip [s_of p, q] >>= (fun x : bool => if x then cflip [r_of p, q] >>= (fun x0 : bool => if x0 then a else b) else c )). -Proof. - move=>T p q r s a b c. - repeat rw_choicebind_dl. exact: choiceA. -Qed. - - HB.instance Definition _ := Monad.on flipacto. - HB.instance Definition _ := isMonadFlip.Build R flipacto flip1 flipNeg flipmm flipA. - -End ConcreteFlip. -End FlipModel. \ No newline at end of file diff --git a/freer_playground/theories/FreerMonad.v b/freer_playground/theories/FreerMonad.v deleted file mode 100644 index bb42e03..0000000 --- a/freer_playground/theories/FreerMonad.v +++ /dev/null @@ -1,173 +0,0 @@ -(* TODO: maybe push this to monae instead of using it here ?? *) - -From mathcomp Require Import ssreflect ssrfun. -From monae Require Import monad_lib monad_model monad_transformer hierarchy. -From HB Require Import structures. - -Local Open Scope monae_scope. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Definition Eff : UU0 := UU0 -> UU0. - -HB.mixin Record isFreerMonad (F : Eff) (M : UU0 -> UU0) of Monad M := { - (* F : UU0 -> UU0 ; *) - trigger : F ~~> M ; - denote {cm : monad} (denote_effect : F ~~> cm) : M ~~> cm; - denote_ret : forall (cm : monad) (denote_effect : F ~~> cm) X (x : X), - denote denote_effect X (ret X x) = @ret cm X x; - denote_bind : forall (cm : monad) (denote_effect : F ~~> cm) X Y m (f : X -> M Y), - denote denote_effect Y (m >>= f) = (denote denote_effect X m) >>= (fun x => denote denote_effect Y (f x)) ; - denote_trigger : forall (cm : monad) (denote_effect : F ~~> cm) X (fx : F X), - denote denote_effect X (trigger X fx) = denote_effect X fx; - denote_unique : forall (cm : monad) (denote_effect : F ~~> cm) (denote' : M ~~> cm), - (forall X (x : X), denote' X (ret X x) = @ret cm X x) -> - (forall X Y (m : M X) (f : X -> M Y), denote' Y (m >>= f) = (denote' X m) >>= (fun x => denote' Y (f x))) -> - (forall X (fx : F X), (denote' X (trigger X fx)) = denote_effect X fx) -> - forall X (m : M X), denote' X m = denote denote_effect X m -}. - -#[short(type=freerMonad)] -HB.structure Definition FreerMonad (F : Eff) := {M of isFreerMonad F M & }. - -Module FreerMonadMod. - Section freer. - - Variable F : Eff. - - Inductive Freer (X : UU0) := - | Pure : X -> Freer X - | Impure : forall Y, F Y -> (Y -> Freer X) -> Freer X - . - - Definition acto := fun X : UU0 => Freer X. - - Local Notation M := acto. - - Let ret : idfun ~~> M := fun _ x => Pure x. - - Local Fixpoint bind [A B : UU0] (m : M A) (f : A -> M B) := - match m with - | Pure x => f x - | Impure Y fy k => Impure fy (fun y => bind (k y) f) - end. - - Let left_neutral: BindLaws.left_neutral bind ret . - Proof. - rewrite /BindLaws.left_neutral. - by []. - Qed. - - Let right_neutral : BindLaws.right_neutral bind ret. - Proof. - move=>/=A. - elim=>[x|Y fy k IHm]//=. - congr Impure; - exact/boolp.funext. - Qed. - -Let assoc : BindLaws.associative bind. -Proof. - move=>/=A B C m f g. - elim:m=>//=Y fy k IHm. - congr Impure; - exact/boolp.funext. -Qed. - -HB.instance Definition _ := - isMonad_ret_bind.Build M left_neutral right_neutral assoc. - - End freer. - -End FreerMonadMod. - -HB.export FreerMonadMod. - -Module FreerMod. -Section freer. - -Variable F : Eff. - -Local Notation M := (acto F). - -Let trigger : F ~~> M := fun X fx => Impure fx (fun x => Pure F x). - -Local Fixpoint denote {cm : monad} (denote_effect : F ~~> cm) (X : UU0) (m : M X):cm X:= -match m with -| Pure x => Ret x -| Impure Y fy k => denote_effect Y fy >>= fun y => denote denote_effect (k y) -end. - -Let denote_ret : forall (cm : monad) (denote_effect : F ~~> cm) X (x : X), - denote denote_effect (Ret x) = Ret x. -Proof. - rewrite/=/denote. - by []. -Qed. - - -Let denote_bind (cm : monad) (denote_effect : F ~~> cm) X Y m (f : X -> M Y) : - denote denote_effect (m >>= f) = ( denote denote_effect m) >>= (fun x => denote denote_effect (f x)) . -Proof. - elim:m=>[x | Z fz k]/=. - - by rewrite !bindretf. - rewrite bindA=>H. - congr bind. - exact/boolp.funext/H. -Qed. - -Let denote_trigger : forall (cm : monad) (denote_effect : F ~~> cm) X (fx : F X), - denote denote_effect (trigger fx) = denote_effect X fx. -Proof. - move=>cm denote_effect X fx. - by rewrite/denote/trigger/=bindmret. -Qed. - -Let denote_unique : forall (cm : monad) (denote_effect : F ~~> cm) (denote' : M ~~> cm), - (forall X (x : X), denote' X (ret X x) = @hierarchy.ret cm X x) -> - (forall X Y (m : M X) (f : X -> M Y), denote' Y (m >>= f) = (denote' X m) >>= (fun x => denote' Y (f x))) -> - (forall X (fx : F X), (denote' X (trigger fx)) = denote_effect X fx) -> - forall X (m : M X), denote' X m = denote denote_effect m. -Proof. - move=>cm denote_effect denote' dret' dbind' dtrigger' X m. - rewrite/denote. - elim:m=>[x| Y fy k Hy]/=. - - exact/dret'. - under [in RHS]eq_bind do rewrite -Hy. - by rewrite -dtrigger'-dbind'/trigger. -Qed. - -HB.instance Definition _ := isFreerMonad.Build F M - denote_ret - denote_bind - denote_trigger - denote_unique. - - End freer. -End FreerMod. - -Lemma denote_if : forall (F : Eff) (M : freerMonad F) (cm : monad) (denote_effect : F ~~> cm) X (m m' : M X) b, - denote cm denote_effect X (if b then m else m') = if b then ( denote cm denote_effect X m) else ( denote cm denote_effect X m'). -Proof. - by move=>? ? ? ? ? ? ?; case. -Qed. - -HB.export FreerMod. - -(** This mixin is a first attepmt at equational reasoning, if we ever use it... *) -HB.mixin Record isFreerEquiv (F : Eff) := { - M : freerMonad F ; - cm : monad ; - denote_effect : F ~~> cm ; - equiv_rel : forall X, M X -> M X -> Prop ; - is_equiv_correct : forall (X : UU0) (m1 m2 : M X), - equiv_rel X m1 m2 -> - denote cm denote_effect X m1 = denote cm denote_effect X m2 ; -}. - - -#[short(type=freerMonadEq)] -HB.structure Definition FreerMonadEq := {F of isFreerEquiv F & }. - diff --git a/freer_playground/theories/lib/AbstractFreerCoproduct.v b/freer_playground/theories/lib/AbstractFreerCoproduct.v deleted file mode 100644 index 8150515..0000000 --- a/freer_playground/theories/lib/AbstractFreerCoproduct.v +++ /dev/null @@ -1,53 +0,0 @@ - -(* ======== Freeeeeee ======== *) - -(* Check monadM. - -HB.mixin Record isFreerMonadCoproduct (F G : Eff) (mf : freerMonad F) (mg : freerMonad G) (cm : monad) (M : UU0 -> UU0) of freerMonad (F<+>G) M := { - cp_left : monadM (mf) M ; - cp_right : monadM mg M ; - from_coproduct : (mf ~~> cm) -> (mg ~~> cm) -> (M ~~> cm) ; - cp_left_law : forall (f : monadM mf cm) (g : monadM mg cm) X (m : mf X), from_coproduct f g X (cp_left X m) = f X m ; - cp_right_law : forall (f : monadM mf cm) (g : monadM mg cm) X (m : mg X), from_coproduct f g X (cp_right X m) = g X m ; - from_coproduct_unique : forall (f : monadM mf cm) (g : monadM mg cm) (c : monadM M cm), (forall X m, c X (cp_left X m) = from_coproduct f g X (cp_left X m)) -> (forall X m, c X (cp_right X m) = from_coproduct f g X (cp_right X m)) -> forall X m, from_coproduct f g X m = c X m -}. - -#[short(type=coprodMF)] -HB.structure Definition CoproductOfMonads (freerMonad F freerMonad G cm : monad) := {M of isMonadCoproduct freerMonad F freerMonad G cm M &}. - - -Module FLeftCoprod. - Section leftc. - Variable F G : UU0 -> UU0. - Variable Mf : freerMonad F. - Variable Mfg : freerMonad (F <+> G). -Definition mmor_left [X] (mf : Mf X) : Mfg X. -case: mf. - -:= match mf with -| Pure x => Pure (F <+> G) x -| Impure Y fy k => Impure (inl fy) (fun y => mmor_left (k y)) -end. - -Let ret : MonadMLaws.ret mmor_left. -Proof. - by []. -Qed. - -Let bind : MonadMLaws.bind mmor_left. -Proof. - move=>a b m f. - elim: m=>[x|Y fy k H]//=. - congr (Impure); - apply/boolp.funext=>y. - by rewrite H. -Qed. - -(* HB.about isMonadM_ret_bind.Build. *) -HB.instance Definition _ := isMonadM_ret_bind.Build (acto F) (acto (F<+>G)) mmor_left ret bind. - End leftc. -End LeftCoprod. - - - - *) diff --git a/freer_playground/theories/lib/ActoFreerCoproduct.v b/freer_playground/theories/lib/ActoFreerCoproduct.v deleted file mode 100644 index 9fe0e8c..0000000 --- a/freer_playground/theories/lib/ActoFreerCoproduct.v +++ /dev/null @@ -1,166 +0,0 @@ - -From Stdlib Require Import ssrmatching Reals JMeq. -From mathcomp Require Import ssreflect. -From HB Require Import structures. -From monae Require Import preamble hierarchy monad_transformer. -From FreerTheories Require Import FreerMonad. - -Local Open Scope monae_scope. -Local Close Scope nat_scope. -Declare Scope fm_scope. -Local Open Scope fm_scope. - -(* Step 3 *) -Notation "F <+> G" := (fun X:Type => F X + G X)%type (at level 50) : fm_scope. - -HB.mixin Record isMonadCoproduct (N N': monad) (M : UU0 -> UU0) of Monad M := { - cp_left : monadM N M ; - cp_right : monadM N' M ; - from_coproduct : forall (cm : monad), - (N ~~> cm) -> (N' ~~> cm) -> (M ~~> cm) ; - cp_left_law : - forall cm - (f : monadM N cm) - (g : monadM N' cm) - X - (m : N X), - from_coproduct cm f g X (cp_left X m) = f X m ; - cp_right_law : forall (cm : monad) (f : monadM N cm) (g : monadM N' cm) X (m : N' X), - from_coproduct cm f g X (cp_right X m) = g X m ; - from_coproduct_unique : forall (cm : monad) (f : monadM N cm) (g : monadM N' cm) (c : monadM M cm), - (forall X m, c X (cp_left X m) = from_coproduct cm f g X (cp_left X m)) - -> (forall X m, c X (cp_right X m) = from_coproduct cm f g X (cp_right X m)) - -> forall X m, from_coproduct cm f g X m = c X m -}. - -#[short(type=coprodM)] -HB.structure Definition CoproductOfMonads (N N' : monad) := {M of isMonadCoproduct N N' M &}. - - -Module LeftCoprod. - Section leftc. - Variable F G : UU0 -> UU0. - -Fixpoint mmor_left [X] (mf : acto F X) : acto (F <+> G) X := match mf with -| Pure x => Pure (F <+> G) x -| Impure Y fy k => Impure (inl fy) (fun y => mmor_left (k y)) -end. - -Let ret : MonadMLaws.ret mmor_left. -Proof. - by []. -Qed. - -Let bind : MonadMLaws.bind mmor_left. -Proof. - move=>a b m f. - elim: m=>[x|Y fy k H]//=. - congr (Impure); - apply/boolp.funext=>y. - by rewrite H. -Qed. - -HB.instance Definition _ := isMonadM_ret_bind.Build (acto F) (acto (F<+>G)) mmor_left ret bind. - - End leftc. -End LeftCoprod. -HB.export LeftCoprod. - -Module RightCoprod. - Section righc. - Variable F G : UU0 -> UU0. - -Fixpoint mmor_right [X] (mf : acto G X) : acto (F <+> G) X := match mf with -| Pure x => Pure (F <+> G) x -| Impure Y fy k => Impure (inr fy) (fun y => mmor_right (k y)) -end. - -Let ret : MonadMLaws.ret mmor_right. -Proof. - move=>a. - by []. -Qed. - -Let bind : MonadMLaws.bind mmor_right. -Proof. - move=>a b m f. - elim: m=>[x|Y fy k H]//=. - congr (Impure); - apply/boolp.funext=>y. - by rewrite H. -Qed. - -HB.instance Definition _ := isMonadM_ret_bind.Build (acto G) (acto (F<+>G)) mmor_right ret bind. - - End righc. -End RightCoprod. -HB.export RightCoprod. - -Module FullCoprod. - Section cop. - Variable F G : UU0 -> UU0. - Notation Nacto := (acto F). - Notation Nacto':= (acto G). - Notation Macto := (acto (F<+>G)). - -Variable ammor_left : forall {X} (MF:freerMonad F) (MFG:freerMonad (F <+> G)) (mf : MF X), MFG X. -Variable ammor_right : forall {X} (MG:freerMonad G) (MFG:freerMonad (F <+> G)) (mg : MG X), MFG X. - -Definition ctrigger `{X:UU0} (MF:freerMonad F) (MG:freerMonad G) {MFG : freerMonad (F<+>G)} (fg : (F<+>G) X) - : MFG X. -Proof. - case: fg=>[fx|gx]. - apply/(ammor_left MF)/trigger/fx. - apply/(ammor_right MG)/trigger/gx. -Defined. - -Local Fixpoint from_coproduct (cm : monad) (l : Nacto ~~> cm) (r : Nacto' ~~> cm) `[X:UU0] (m : Macto X) : cm X -:= match m with -| Pure x => ret X x -| Impure Y fgy k => match fgy with - | inl f => l Y (Impure f (fun y:Y => Pure F y)) - | inr g => r Y (Impure g (fun y:Y => Pure G y)) - end >>= fun y => from_coproduct cm l r (k y) -end -. - -Notation mmor_l := (mmor_left F G). -Notation mmor_r := (mmor_right F G). - - -Let cp_left_law : forall (cm : monad) (f : monadM Nacto cm) (g : monadM Nacto' cm) X (m : Nacto X), from_coproduct cm f g (mmor_l m) = f X m. -Proof. - move=>cm f g X. - elim=>[x|Y fy k H]/=. - by rewrite -(monadMret (s:=f)). - under eq_bind do rewrite H. - by rewrite -monadMbind. -Qed. -Let cp_right_law : forall (cm : monad) (f : monadM Nacto cm) (g : monadM Nacto' cm) X (m : Nacto' X), from_coproduct cm f g (mmor_r m) = g X m. -Proof. - move=>cm f g X. - elim=>[x|Y fy k H]/=. - by rewrite -(monadMret (s:=g)). - under eq_bind do rewrite H. - by rewrite -monadMbind. -Qed. - -Let from_coproduct_unique : forall (cm : monad) (f : monadM Nacto cm) (g : monadM Nacto' cm) (c : monadM Macto cm), (forall X m, c X (mmor_l m) = from_coproduct cm f g (mmor_l m)) -> (forall X m, c X (mmor_r m) = from_coproduct cm f g (mmor_r m)) -> forall X m, from_coproduct cm f g m = c X m. -Proof. - move=>cm f g c Hl Hr X. - elim=>[x|Y fgy ky H]/=. - by rewrite/=-(monadMret (s:=c)). - under eq_bind do rewrite H. - by case: fgy=>[fy|gy]; - rewrite -?(cp_left_law cm f g) -?Hl - -?(cp_right_law cm f g) -?Hr - /=-(monadMbind (s:=c)). - -Qed. - -HB.instance Definition _ := isMonadCoproduct.Build (Nacto) (Nacto') (Macto) mmor_l mmor_r from_coproduct cp_left_law cp_right_law from_coproduct_unique. - - End cop. -End FullCoprod. - -HB.export FullCoprod. diff --git a/freer_playground/theories/lib/FreerFlip.v b/freer_playground/theories/lib/FreerFlip.v deleted file mode 100644 index e6a8927..0000000 --- a/freer_playground/theories/lib/FreerFlip.v +++ /dev/null @@ -1,119 +0,0 @@ -From Stdlib Require Import ssrmatching Reals JMeq Relations Morphisms Eqdep. -From mathcomp Require Import ssreflect ssrbool ssrnum ssralg reals. -From infotheo Require Import realType_ext. -From HB Require Import structures. -From monae Require Import preamble hierarchy monad_lib. -From FreerTheories Require Import FlipMonad FreerMonad. - -Declare Scope freer_flip_scope. - -Local Open Scope monae_scope. -Local Open Scope proba_scope. -Local Open Scope reals_ext_scope. -Local Open Scope freer_flip_scope. - -Reserved Notation "x <|| p ||> y" (at level 40, left associativity, y at next level). -Reserved Notation "a === b" (at level 90). - -Module FreerFlipModel. - - Section freer_flip. -Variable R:realType. - -Inductive FlipEff : UU0 -> UU0 := -| flip_e (p : {prob R}) : FlipEff bool -. - - -Arguments trigger {_ _ _}. -Variable M : (freerMonad FlipEff). - - -Definition flipf (p:{prob R}) := ( @trigger FlipEff M bool (flip_e p)). - - -(* Let fa := flipacto R. *) -Variable fl : flipMonad R. - -Definition denote_flip_effect : FlipEff ~~> fl := -fun X fx => match fx with -| flip_e p => flip p -end. - -Notation choice_of_Type := monad_model.choice_of_Type. - -Definition choicef {X} (p : {prob R}) (a b : M X) := flipf p >>= (fun b0 => if b0 then a else b). - -Notation "x <|| p ||> y" := - (choicef p x y) -(at level 40, left associativity, y at next level) : freer_flip_scope. - - -(* 5th step : Flip equiv laws *) -Inductive flip_rel :forall `[X : UU0] (m1 m2 : M X), Prop := -| rflip1 : flip_rel (flipf 1%:pr) (Ret true) -| rflipNeg : forall p, flip_rel (flipf p) ((flipf (Prob.p p).~%:pr) >>= (fun x => Ret (~~ x))) -| rflipmm : forall (A:UU0) p (a: (M A)), flip_rel (flipf p >> a) a - (* quasi associativity *) -| rflipA : forall (T:UU0) (p q r s : {prob R}) (a b c : M T), flip_rel - (a <|| p ||> (b <|| q ||> c)) - ((a <|| [r_of p, q] ||> b) <|| [s_of p, q] ||> c) - (* (flipf p >>= (fun x : bool => if x then a else flipf q >>= (fun x0 : bool => if x0 then b else c))) *) - (* (flipf [s_of p, q] >>= (fun x : bool => if x then flipf [r_of p, q] >>= (fun x0 : bool => if x0 then a else b) else c)) *) -| equiv_bind_congr : forall (A B :UU0) (a b : M A) (f g : A -> M B), - (* a === b -> (forall x, (f x) === (g x)) -> (a >>= f) === (b >>= g) *) - flip_rel a b -> (forall x, flip_rel (f x) (g x)) -> flip_rel (a >>= f) (b >>= g) -| equiv_refl : forall (A:UU0) (m : M A), flip_rel m m -| equiv_sym : forall (A:UU0) (m n : M A), flip_rel m n -> flip_rel n m -| equiv_trans : forall (A:UU0) (m n o : M A), flip_rel m n -> flip_rel n o -> flip_rel m o -. - -(* 6th step : Equiv correct *) -Lemma equiv_correct : forall (X : UU0) (m1 m2 : M X), - @flip_rel X m1 m2 -> - denote fl denote_flip_effect X m1 = denote fl denote_flip_effect X m2. -Proof. - move=>X m1 m2 H. - (* rewrite/denote/=. *) - elim: H=>[| p | A p a | T p q r s a b c - | A B a b f g Hab H Hfg H' - | A m | A m n Hmn H | A m n o Hmn H Hno H' - ]/= - ; last first. - - by rewrite H H'. - - by rewrite H. - - by []. - - rewrite !denote_bind ; congr bind. - + exact/H. - + apply/boolp.funext/H'. - (* all: rewrite/=. *) - all: rewrite ?denote_bind. - (* flip_a *) - under eq_bind do rewrite denote_if denote_bind; - under [in RHS]eq_bind do rewrite denote_if denote_bind; - under eq_bind do under eq_bind do rewrite denote_if; - under [in RHS]eq_bind do under eq_bind do rewrite denote_if. - all: rewrite !denote_trigger/denote_flip_effect. - - exact/fA0. - - exact/flipmm. - - under eq_bind do rewrite denote_ret; exact/flipNeg. - - rewrite denote_ret; exact/flip1. -Qed. - -HB.instance Definition _ := isFreerEquiv.Build FlipEff equiv_correct. - -Notation "a === b" := -(flip_rel a b) - (at level 90) : freer_flip_scope. - -End freer_flip. -End FreerFlipModel. - -HB.export FreerFlipModel. - -Arguments flip_rel {_ _ _}. -Arguments flipf {_ _}. -Arguments choicef {_ _ _}. - - - diff --git a/meta.yml b/meta.yml new file mode 100644 index 0000000..555e6c1 --- /dev/null +++ b/meta.yml @@ -0,0 +1,64 @@ +--- +fullname: Freer Equational Reasoning for Distributed and Probabilistic Systems +shortname: FreerDPS +organization: FreerDPS +community: false +action: true +coqdoc: false + +synopsis: + TODO + +description: |- + This work started as a rewrite/extension of [FreeSpec Core](https://github.com/lthms/FreeSpec) using [monae](https://github.com/affeldt-aist/monae) / ssreflect. + + This work has been accepted for presentation to [COMPAS26](https://2026.compas-conference.fr/) (no paper available online). + +publications: +- TODO + +authors: +- name: Hugo Forraz + initial: true + +maintainers: +- name: Hugo Forraz + initial: true + +opam-file-maintainer: Hugo Forraz + +license: + fullname: MIT License + identifier: MIT + file: LICENSE + +supported_rocq_versions: + text: 9.0 + opam: '{ (= "9.0") | (= "dev") }' + +tested_rocq_opam_versions: +- version: '2.5.0-rocq-prover-9.0' + repo: 'mathcomp/mathcomp' + +dependencies: +- opam: + name: rocq-mathcomp-ssreflect + version: '{>= "2.5.0"}' + description: |- + [MathComp](https://math-comp.github.io) +- opam: + name: rocq-mathcomp-analysis + version: '{>= "1.16.0"}' + description: |- + [MathComp Analysis](https://github.com/math-comp/analysis) +- opam: + name: coq-mathcomp-algebra-tactics + version: '{>= "1.2.7"}' + description: |- + [MathComp Algebra Tactics](https://github.com/math-comp/algebra-tactics) +- opam: + name: rocq-monae + version: '{= "0.9.2"}' + description: |- + Monae +--- \ No newline at end of file diff --git a/theories/Component.v b/theories/Component.v index 4714b8e..318464a 100644 --- a/theories/Component.v +++ b/theories/Component.v @@ -4,48 +4,67 @@ (* Copyright (C) 2018–2020 ANSSI *) +Attributes deprecated( + note="This file will probably be removed or + largely reworked in later versions."). + +From FreerDPS Require Import Init. (* From ExtLib Require Import StateMonad. *) -From mathcomp Require Import ssreflect. -From FreerDPS Require Export Interface Semantics Impure. -From monae Require Import preamble hierarchy monad_lib. -From HB Require Import structures. +From FreerDPS Require Export Effect Semantics Freer. +From FreerDPS Require Import Contract Hoare. +From monae Require Import monad_lib. + +Generalizable All Variables. + (** * Definition *) -(** In FreeSpec, a _component_ is an entity which exposes an interface [i], - and uses primitives of an interface [j] to compute the results of primitives - of [i]. Besides, a component is likely to carry its own internal state (of +(** In FreeSpec, a _component_ is an entity which exposes an effect [F], + and uses primitives of an effect [E] to compute the results of primitives + of [F]. Besides, a component is likely to carry its own internal state (of type [s]). << - i +-------------------+ j + F +-------------------+ E | | | | - +------>| | c : component i j |----->| + +------>| | c : component F E |----->| | | | | +-------------------+ >> - Thus, a component [c : component i j] is a polymorphic function which - maps primitives of [i] to impure computations using [j]. *) + Thus, a component [c : component F E] is a polymorphic function which + maps primitives of [F] to impure computations using [E]. *) -Definition component (i j : interface) `{im : impureMonad j} : Type := - forall (α : Type), i α -> im α. +Definition component (F E : effect) `{im : freerMonad E} : Type := + forall (α : Type), F α -> im α. + +Definition correct_component `{MayProvide Ex E} {im : freerMonad Ex} + `(c : component F Ex) `(cF : contract F ΩF) + `(cE : contract E ΩE) (pred : ΩF -> ΩE -> Prop) : + Prop := + forall (ωF : ΩF) (ωE : ΩE) (init : pred ωF ωE) + `(op : F α) (o_caller : caller_obligation cF ωF op), + pre (to_hoare cE $ c α op) ωE /\ + forall (x : α) (ωE' : ΩE), + post (to_hoare (im:=im) cE (c α op)) ωE x ωE' -> + callee_obligation cF ωF op x /\ + pred (witness_update cF ωF op x) ωE'. (** The similarity between FreeSpec components and operational semantics may be confusing at first. The main difference between the two concepts is simple: operational semantics are self-contained terms which can, alone, be used to - interpret impure computations of a given interface. Components, on the + interpret impure computations of a given effect. Components, on the other hand, are not self-contained. Without an operational semantics for - [j], we cannot use a component [c : component i j] to interpret an impure - computation using [i]. + [E], we cannot use a component [c : component F E] to interpret an impure + computation using [F]. - Given an initial semantics for [j], we can however derive an operational - semantics for [i] from a component [c]. *) + Given an initial semantics for [E], we can however derive an operational + semantics for [F] from a component [c]. *) (** * Semantics Derivation *) -CoFixpoint derive_semantics {i j} {im : impureMonad j} (c : component i j) (sem : semantics j) - : semantics i := +CoFixpoint derive_semantics {F E} {im : freerMonad E} + (c : component F E) (sem : semantics E) : semantics F := mk_semantics (fun a p => let (res, next) := (to_state (α:=im) _ $ c a p) sem in (res, derive_semantics c next)). @@ -57,44 +76,42 @@ CoFixpoint derive_semantics {i j} {im : impureMonad j} (c : component i j) (sem independently, then composing them together with [semprod] and [derive_semantics]. *) -Definition bootstrap {i} {im : impureMonad iempty} (c : component i iempty) : semantics i := - derive_semantics (im:=im) c iempty_semantics. +Definition bootstrap {F} {im : freerMonad eempty} + (c : component F eempty) : semantics F := + derive_semantics (im:=im) c eempty_semantics. (** * In-place Primitives Handling *) (** The function [with_component] allows for locally providing an additional - interface [j] within an impure computation of type [impure ix a]. The - primitives of [j] will be handled by impure computations, i.e., a component. - of type [c : compoment j ix s]. *) + effect [E] within an impure computation of type [freer Fx a]. The + primitives of [E] will be handled by impure computations, i.e., a component. + of type [c : compoment E Fx s]. *) Local Open Scope monae_scope. - #[local] -Fixpoint with_component_aux {ix j α} - (* {im : impureMonad ix} *) - (* {jm : impureMonad (ix + j)} *) -(c : component (im:=Impure.ImpureModule_acto__canonical__Impure_MonadImpure ix) j ix) (p : impure (ix + j) α) - : impure ix α := +Fixpoint with_component_aux {Fx E α} +(c : component + (im:=freer Fx) + E Fx) + (p : freer (Fx + E) α) + : freer Fx α := match p with - | local x => local x - | request_then T (in_right e) f => - c T e >>= fun res => with_component_aux c (f res) - | request_then _ (in_left e) f => - request_then e (fun x => with_component_aux c (f x)) + | pure x => pure x + | impure T (in_right op) k => + c T op >>= fun res => with_component_aux c (k res) + | impure _ (in_left op) k => + impure op (fun x => with_component_aux c (k x)) end. -Notation "m >>= f" := (impure_bind m f). -Notation "m >> f" := (impure_bind m (fun _ =>f)). - -Definition with_component {ix j α} - (* `{im : impureMonad ix} - `{ixjm : impureMonad (ix+j)} *) - (initializer : impure ix unit) - (c : component (im:=Impure.ImpureModule_acto__canonical__Impure_MonadImpure ix) j ix) - (finalizer : impure ix unit) - (p : impure (ix+j) α) - : impure ix α := +Definition with_component {Fx E α} + (initializer : freer Fx unit) + (c : component + (im:=freer Fx) + E Fx) + (finalizer : freer Fx unit) + (p : freer (Fx + E) α) + : freer Fx α := initializer >> with_component_aux c p >>= fun res => finalizer >> - local res. + pure res. diff --git a/theories/Contract.v b/theories/Contract.v index c975c77..3c7dff0 100644 --- a/theories/Contract.v +++ b/theories/Contract.v @@ -6,15 +6,13 @@ (** In this library, we provide the necessary material to reason about FreeSpec components both in isolation, and in composition. To do that, we focus our - reasoning principles on interfaces, by defining how their primitives shall + reasoning principles on effects, by defining how their primitives shall be used, and what to expect the result computed by “correct” operational semantics (according to a certain definition of “correct”). *) -From Stdlib Require Import Setoid Morphisms. +From FreerDPS Require Import Init. (* From ExtLib Require Import StateMonad MonadState MonadTrans. *) -From FreerDPS Require Import Interface Impure Semantics Component. -From mathcomp Require Import ssreflect. -From monae Require Import preamble hierarchy. +From FreerDPS Require Import Effect Freer. #[local] Open Scope signature_scope. Open Scope monae_scope. @@ -23,7 +21,7 @@ Generalizable All Variables. (** * Definition *) -(** A contract dedicated to [i : interface] primarily provides two +(** A contract dedicated to [F : effect] primarily provides two predicates. - [caller_obligation] distinguishes between primitives that can be used (by @@ -37,55 +35,55 @@ Generalizable All Variables. parameterized by what we have called a “witness.” A witness is a term which describes the necessary information of the past, and allows for taking decision for the present. It can be seen as an abstraction of the concrete - state of the interface implementor. + state of the effect implementor. To keep this state up-to-date after each primitive interpretation, contracts also define a dedicated function [witness_update]. *) -Record contract (i : interface) (Ω : Type) : Type := make_contract - { witness_update (ω : Ω) : forall (α : Type), i α -> α -> Ω - ; caller_obligation (ω : Ω) : forall (α : Type), i α -> Prop - ; callee_obligation (ω : Ω) : forall (α : Type), i α -> α -> Prop +Record contract (F : effect) (Ω : Type) : Type := make_contract + { witness_update (ω : Ω) : forall (α : Type), F α -> α -> Ω + ; caller_obligation (ω : Ω) : forall (α : Type), F α -> Prop + ; callee_obligation (ω : Ω) : forall (α : Type), F α -> α -> Prop }. Declare Scope contract_scope. Bind Scope contract_scope with contract. -Arguments make_contract [i Ω] (_ _ _). -Arguments witness_update [i Ω] (c ω) [α] (_ _). -Arguments caller_obligation [i Ω] (c ω) [α] (_). -Arguments callee_obligation [i Ω] (c ω) [α] (_ _). +Arguments make_contract [F Ω] (_ _ _). +Arguments witness_update [F Ω] (c ω) [α] (_ _). +Arguments caller_obligation [F Ω] (c ω) [α] (_). +Arguments callee_obligation [F Ω] (c ω) [α] (_ _). (** The most simple contract we can define is the one that requires anything both for the impure computations which uses the primitives of a - given interface, and for the operational semantics which compute results for + given effect, and for the operational semantics which compute results for these primitives. *) -Definition const_witness {i} := - fun (u : unit) (α : Type) (e : i α) (x : α) => u. +Definition const_witness {F} := + fun (u : unit) (α : Type) (e : F α) (x : α) => u. -Inductive no_caller_obligation {i Ω} (ω : Ω) (α : Type) (e : i α) : Prop := +Inductive no_caller_obligation {F Ω} (ω : Ω) (α : Type) (e : F α) : Prop := | mk_no_caller_obligation : no_caller_obligation ω α e. #[global] Hint Constructors no_caller_obligation : freespec. -Inductive no_callee_obligation {i Ω} (ω : Ω) (α : Type) (e : i α) (x : α) : Prop := +Inductive no_callee_obligation {F Ω} (ω : Ω) (α : Type) (e : F α) (x : α) : Prop := | mk_no_callee_obligation : no_callee_obligation ω α e x. #[global] Hint Constructors no_callee_obligation : freespec. -Definition no_contract (i : interface) : contract i unit := +Definition no_contract (F : effect) : contract F unit := {| witness_update := const_witness ; caller_obligation := no_caller_obligation ; callee_obligation := no_callee_obligation |}. (** A similar —and as simple— contract is the one that forbids the use of a - given interface. *) + given effect. *) -Definition do_no_use {i Ω} (ω : Ω) (α : Type) (e : i α) : Prop := False. +Definition do_no_use {F Ω} (ω : Ω) (α : Type) (e : F α) : Prop := False. -Definition forbid_specs (i : interface) : contract i unit := +Definition forbid_specs (F : effect) : contract F unit := {| witness_update := const_witness ; caller_obligation := do_no_use ; callee_obligation := no_callee_obligation @@ -93,25 +91,25 @@ Definition forbid_specs (i : interface) : contract i unit := (** * Contract Equivalence *) -Definition contract_caller_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) +Definition contract_caller_equ `(c1 : contract F Ω1) `(c2 : contract F Ω2) (f : Ω1 -> Ω2) : Prop := - forall ω1 a (p : i a), + forall ω1 a (p : F a), caller_obligation c1 ω1 p <-> caller_obligation c2 (f ω1) p. -Definition contract_callee_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) +Definition contract_callee_equ `(c1 : contract F Ω1) `(c2 : contract F Ω2) (f : Ω1 -> Ω2) : Prop := - forall ω1 a (p : i a) x, + forall ω1 a (p : F a) x, callee_obligation c1 ω1 p x <-> callee_obligation c2 (f ω1) p x. -Definition contract_witness_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) +Definition contract_witness_equ `(c1 : contract F Ω1) `(c2 : contract F Ω2) (f : Ω1 -> Ω2) : Prop := - forall ω1 a (p : i a) x, + forall ω1 a (p : F a) x, f (witness_update c1 ω1 p x) = witness_update c2 (f ω1) p x. -Inductive contract_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) +Inductive contract_equ `(c1 : contract F Ω1) `(c2 : contract F Ω2) : Type := | mk_contract_equ (f : Ω1 -> Ω2) (g : Ω2 -> Ω1) (iso1 : forall x, f (g x) = x) (iso2 : forall x, g (f x) = x) @@ -120,24 +118,24 @@ Inductive contract_equ `(c1 : contract i Ω1) `(c2 : contract i Ω2) (witness_equ : contract_witness_equ c1 c2 f) : contract_equ c1 c2. -Definition contract_iso_lr `(c1 : contract i Ω1) `(c2 : contract i Ω2) +Definition contract_iso_lr `(c1 : contract F Ω1) `(c2 : contract F Ω2) (equ : contract_equ c1 c2) (ω1 : Ω1) : Ω2 := match equ with | @mk_contract_equ _ _ _ _ _ f _ _ _ _ _ _ => f ω1 end. -Definition contract_iso_rl `(c1 : contract i Ω1) `(c2 : contract i Ω2) +Definition contract_iso_rl `(c1 : contract F Ω1) `(c2 : contract F Ω2) (equ : contract_equ c1 c2) (ω2 : Ω2) : Ω1 := match equ with | @mk_contract_equ _ _ _ _ _ _ g _ _ _ _ _ => g ω2 end. -Arguments contract_iso_lr {i Ω1 c1 Ω2 c2} (equ ω1). -Arguments contract_iso_rl {i Ω1 c1 Ω2 c2} (equ ω2). +Arguments contract_iso_lr {F Ω1 c1 Ω2 c2} (equ ω1). +Arguments contract_iso_rl {F Ω1 c1 Ω2 c2} (equ ω2). -Lemma contract_equ_refl `(c : contract i Ω) +Lemma contract_equ_refl `(c : contract F Ω) : contract_equ c c. Proof. @@ -147,7 +145,7 @@ Proof. + now intros ω α p x. Defined. -Lemma contract_equ_sym `(c1 : contract i Ω1) `(c2 : contract i Ω2) +Lemma contract_equ_sym `(c1 : contract F Ω1) `(c2 : contract F Ω2) (equ : contract_equ c1 c2) : contract_equ c2 c1. @@ -174,8 +172,8 @@ Proof. now rewrite equ. Defined. -Lemma contract_equ_trans `(c1 : contract i Ω1) `(c2 : contract i Ω2) - `(c3 : contract i Ω3) +Lemma contract_equ_trans `(c1 : contract F Ω1) `(c2 : contract F Ω2) + `(c3 : contract F Ω3) `(is_equ12 : contract_equ c1 c2) `(is_equ23 : contract_equ c2 c3) : contract_equ c1 c3. @@ -205,45 +203,45 @@ Defined. (** * Composing Contracts *) -(** As we compose interfaces and operational semantics, we can easily compose - contracts together, by means of the [contractprod] operator. Given [i] and [j] - two interfaces, if we can reason about [i] and [j] independently (e.g., the - caller obligations of [j] do not vary when we use [i]), then we can compose - [ci : contract i Ωi] and [cj : contract j Ωj], such that [contractprod ci cj] in a - contract for [i + j]. *) +(** As we compose effects and operational semantics, we can easily compose + contracts together, by means of the [contractprod] operator. Given [F] and [E] + two effects, if we can reason about [F] and [E] independently (e.g., the + caller obligations of [E] do not vary when we use [F]), then we can compose + [ci : contract F ΩF] and [cj : contract E ΩE], such that [contractprod ci cj] in a + contract for [F + E]. *) -Definition gen_witness_update `{MayProvide ix i} {Ω α} (c : contract i Ω) - (ω : Ω) (e : ix α) (x : α) +Definition gen_witness_update `{MayProvide Fx F} {Ω α} (c : contract F Ω) + (ω : Ω) (e : Fx α) (x : α) : Ω := match proj_p e with | Some e => witness_update c ω e x | None => ω end. -Definition gen_caller_obligation `{MayProvide ix i} {Ω α} (c : contract i Ω) - (ω : Ω) (e : ix α) +Definition gen_caller_obligation `{MayProvide Fx F} {Ω α} (c : contract F Ω) + (ω : Ω) (e : Fx α) : Prop := match proj_p e with | Some e => caller_obligation c ω e | None => True end. -Definition gen_callee_obligation `{MayProvide ix i} {Ω α} (c : contract i Ω) - (ω : Ω) (e : ix α) (x : α) +Definition gen_callee_obligation `{MayProvide Fx F} {Ω α} (c : contract F Ω) + (ω : Ω) (e : Fx α) (x : α) : Prop := match proj_p e with | Some e => callee_obligation c ω e x | None => True end. -Definition contractprod `{Provide ix i, Provide ix j} {Ωi Ωj} - (ci : contract i Ωi) (cj : contract j Ωj) - : contract ix (Ωi * Ωj) := - {| witness_update := fun (ω : Ωi * Ωj) (α : Type) (e : ix α) (x : α) => +Definition contractprod `{Provide Fx F, Provide Fx E} {ΩF ΩE} + (ci : contract F ΩF) (cj : contract E ΩE) + : contract Fx (ΩF * ΩE) := + {| witness_update := fun (ω : ΩF * ΩE) (α : Type) (e : Fx α) (x : α) => (gen_witness_update ci (fst ω) e x, gen_witness_update cj (snd ω) e x) - ; caller_obligation := fun (ω : Ωi * Ωj) (α : Type) (e : ix α) => + ; caller_obligation := fun (ω : ΩF * ΩE) (α : Type) (e : Fx α) => gen_caller_obligation ci (fst ω) e /\ gen_caller_obligation cj (snd ω) e - ; callee_obligation := fun (ω : Ωi * Ωj) (α : Type) (e : ix α) (x : α) => + ; callee_obligation := fun (ω : ΩF * ΩE) (α : Type) (e : Fx α) (x : α) => gen_callee_obligation ci (fst ω) e x /\ gen_callee_obligation cj (snd ω) e x |}. @@ -252,28 +250,28 @@ Infix "*" := contractprod : contract_scope. (** We also introduce a second composition operator which shares the witness state among its two operands. *) -(* FIXME: Should be [StrictProvide2 ix i j] *) +(* FIXME: Should be [StrictProvide2 Fx F E] *) -Definition sharedcontractprod `{Provide ix i, Provide ix j} - `(ci : contract i Ω) (cj : contract j Ω) - : contract ix Ω := +Definition sharedcontractprod `{Provide Fx F, Provide Fx E} + `(ci : contract F Ω) (cj : contract E Ω) + : contract Fx Ω := {| witness_update := - fun (ω : Ω) (α : Type) (e : ix α) (x : α) => - (* we need to check [i] before [j] because [sharedcontractprod] + fun (ω : Ω) (α : Type) (e : Fx α) (x : α) => + (* we need to check [F] before [E] because [sharedcontractprod] will be right associative *) - match proj_p (i:=i) e with + match proj_p (F:=F) e with | Some e => witness_update ci ω e x - | _ => match proj_p (i:=j) e with + | _ => match proj_p (F:=E) e with | Some e => witness_update cj ω e x | _ => ω end end; caller_obligation := - fun (ω : Ω) (α : Type) (e : ix α) => + fun (ω : Ω) (α : Type) (e : Fx α) => gen_caller_obligation ci ω e /\ gen_caller_obligation cj ω e; callee_obligation := - fun (ω : Ω) (α : Type) (e : ix α) (x : α) => + fun (ω : Ω) (α : Type) (e : Fx α) (x : α) => gen_callee_obligation ci ω e x /\ gen_callee_obligation cj ω e x |}. @@ -281,12 +279,12 @@ Infix "^" := sharedcontractprod : contract_scope. (** * Contract By Example *) -(** Finally, and as an example, we define a contract for the interface - [STORE s] we discuss in [FreeSpec.Core.Impure]. As a reminder, the - interface is defined as follows: +(** Finally, and as an example, we define a contract for the effect + [STORE s] we discuss in [FreerDPS.Freer]. As a reminder, the + effect is defined as follows: << -Inductive STORE (s : Type) : interface := +Inductive STORE (s : Type) : effect := | Get : STORE s s | Put (x : s) : STORE s unit. >> @@ -325,7 +323,7 @@ Definition store_specs (s : Type) : contract (STORE s) s := |}. (** Now, as we briefly mentionned, this contract allows for reasoning about an - impure computation which uses the [STORE s] interface, assuming the mutable, + impure computation which uses the [STORE s] effect, assuming the mutable, global variable has been initialized. We can define another contract that does not rely on such assumption, and on the contrary, requires an impure computation to initialize the variable prior to using it. @@ -336,5 +334,5 @@ Definition store_specs (s : Type) : contract (STORE s) s := This is one of the key benefits of the FreeSpec approach: because the contracts are defined independently from impure computations and - interfaces, we can actually define several contracts to consider + effects, we can actually define several contracts to consider different set of hypotheses. *) diff --git a/theories/Core.v b/theories/Core.v index 90c26c9..bc26183 100644 --- a/theories/Core.v +++ b/theories/Core.v @@ -4,13 +4,13 @@ (* Copyright (C) 2018–2020 ANSSI *) +From FreerDPS Require Import Init. From FreerDPS Require Export - Interface + Effect Typeclasses - Impure + Freer Semantics Component Contract Hoare - Tactics - . \ No newline at end of file + . diff --git a/theories/Effect.v b/theories/Effect.v new file mode 100644 index 0000000..d0165b1 --- /dev/null +++ b/theories/Effect.v @@ -0,0 +1,268 @@ +(* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +From FreerDPS Require Import Init. + +(** * Definition *) + +(** Following the definition of the <> package, effects in + FreeSpec are parameterized inductive types whose terms purposely describe + the primitives the effect provides. *) + +Definition effect := Type -> Type. + +Declare Scope effect_scope. +Bind Scope effect_scope with effect. + +(** Given [F : effect], a term of type [F α] identifies a primitive of [F] + expected to produce a result of type [α]. + + The simpler effect is the empty effect, which provides no primitives + whatsoever. *) + +Inductive eempty : effect := . + +(** Another example of general-purpose effect we can define is the [STORE s] + effect, where [s] is a type for a state, and [STORE s] allows for + manipulating a global, mutable variable of type [s] within an impure + computation. *) + +Inductive STORE (s : Type) : effect := +| Get : STORE s s +| Put (x : s) : STORE s unit. + +Arguments Get {s}. +Arguments Put [s] (x). + +(** According to the definition of [STORE s], an impure computation can use two + primitives. The term [Get : STORE s s] describes a primitive expected to + produce a result of type [s], that is the current value of the mutable + variable. Terms of the form [Put x : STORE s unit] describe a primitive + which does not produce any meaningful result, but is expected to update the + current value of the mutable variable. + + The use of the word “expected” to describe the primitive of [STORE s] is + voluntary. The definition of an effect does not attach any particular + semantics to the primitives it describes. This will come later, and in + fact, one effect may have many legitimate semantics. + + Impure computations are likely to use more than one effect, but the + [freer] monad takes only one argument. We introduce [eplus] (denoted by + [<+>] or [⊕]) to compose effects together. An impure computation + parameterized by [F ⊕ E] can therefore leverage the primitives of both [F] + and [E]. *) + +(** * Polymorphic Effect Composites *) + +(** When defining general-purpose impure computations that we expect to reuse in + different context, we want to leave the effect as a parameter, and rather + express the constraints in terms of effect availability. We tackle this + challenge by means of _effect composites_. + + - We say an effect composite [Fx] _provides_ a concrete effect [F] + when there exists a function [inj_p : forall α, F α -> Fx α]. + - Conversely, we can determine if a primitive of an effect composite [Fx] + is forwarded to a concrete effect [F] when there exists a function + [proj_p : forall α, Fx α -> option (F a)]. + + We encode this mechanics using two type classes: [MayProvide], and + [Provide]. *) + +Class MayProvide (Fx F : effect) : Type := + { proj_p {α} (e : Fx α) : option (F α) + }. + +Class Provide (Fx F : effect) `{MayProvide Fx F} : Type := + { inj_p {α} (e : F α) : Fx α + ; proj_inj_p_equ {α} (e : F α) : proj_p (inj_p e) = Some e + }. + +(** We provide a default instance for [MayProvide] in the form of a function + [proj_p] which always return [None]. We give to this default instance a + ridiculously high priority number to ensure it is selected only if no other + instances are found. *) + +Instance default_MayProvide (F E : effect) : MayProvide F E|1000 := + { proj_p := fun _ _ => None + }. + +(** It is expected that, for an effect composite [Fx] which provides [F] and + may provide [E], [inj_p] and [proj_p] do not mix up [F] and [E] + primitives. That is, injecting a primitive [e] of [F] inside [Fx], then + projecting the resulting primitive into [E] returns [None] as long as [F] + and [E] are two different effects. *) + +Class Distinguish (Fx F E : effect) `{Provide Fx F, MayProvide Fx E} : Prop := + { distinguish : forall {α} (e : F α), proj_p (F := E) (inj_p (Fx := Fx) e) = None + }. + +(** * Composing Effects *) + +(** We provide the [eplus] operator to compose effects together. That is, + [eplus] can be used to build _concrete_ (as opposed to polymorphic) + effect composite. *) + +Inductive eplus (F E : effect) (α : Type) := +| in_left (e : F α) : eplus F E α +| in_right (e : E α) : eplus F E α. + +Arguments in_left [F E α] (e). +Arguments in_right [F E α] (e). + +Register eplus as freespec.core.eplus.type. +Register in_left as freespec.core.eplus.in_left. +Register in_right as freespec.core.eplus.in_right. + +Infix "+" := eplus : effect_scope. + +(** For [eplus] to be used seamlessly as a concrete effect composite, we + provide the necessary instances for the [MayProvide], [Provide] and + [Distinguish] type classes. Note that these instances always prefer the + left operand of [eplus]. For instance, considering a situation where + there is an instance for [Provide Fx F] and an instance for [Provide Ex F], + the instance of [Provide (Fx + Ex) F] will rely on [Fx]. + + The main use case for [eplus] is to locally provide an additional + effect. For instance, we can consider a [with_state] function which would + locally give access to the [STORE] effect, that is [with_state : forall + Fx s α, s -> freer (Fx + STORE s) α -> freer Fx α]. In such a case, the + effect made locally available shall be the right operand of [eplus]. This + way, functions such as [with_state] are reentrant. If we take an example, + the following impure computation: + +<< +with_state true (with_state false get) +>> + + will return false (that is, the variable in the inner store). *) + +Instance refl_MayProvide (F : effect) : MayProvide F F := + { proj_p := fun _ e => Some e + }. + +#[program] +Instance refl_Provide (F : effect) : @Provide F F (refl_MayProvide F) := + { inj_p := fun (a : Type) (e : F a) => e + }. + +Instance eplus_left_MayProvide (Fx F E : effect) `{MayProvide Fx F} + : MayProvide (Fx + E) F := + { proj_p := fun _ e => + match e with + | in_left e => proj_p e + | _ => None + end + }. + +#[program] +Instance eplus_left_Provide (Fx F E : effect) `{Provide Fx F} + : @Provide (Fx + E) F (eplus_left_MayProvide Fx F E) := + { inj_p := fun (a : Type) (e : F a) => in_left (inj_p e) + }. + +Next Obligation. + now rewrite proj_inj_p_equ. +Qed. + +Instance eplus_right_MayProvide (F Ex E : effect) `{MayProvide Ex E} + : MayProvide (F + Ex) E := + { proj_p := fun _ e => + match e with + | in_right e => proj_p e + | _ => None + end + }. + +#[program] +Instance eplus_right_Provide (F Ex E : effect) `{Provide Ex E} + : @Provide (F + Ex) E (eplus_right_MayProvide F Ex E) := + { inj_p := fun _ e => in_right (inj_p e) + }. + +Next Obligation. + now rewrite proj_inj_p_equ. +Qed. + +(** By default, Coq's inference algorithm for type classe instances inference is + a depth-first search. This is not without consequence in our case. For + instance, if we consider the search of an instance for [MayProvide (F + E) + E], Coq will first try [eplus_right_MayProvide] (as explained previously), + meaning he now search for [MayProvide F E]. It turns out such an instance + exists: [default_MayProvide]. + + To circumvent this issue, we write a dedicated tactic [find_may_provide] + which attempts to find an instance for [MayProvide (?Fx + ?Ex) ?F] with + [refl_MayProvide], [eplus_left_MayProvide] and [eplus_right_MayProvide]. *) + +Ltac find_may_provide := + eapply refl_MayProvide + + (eapply eplus_left_MayProvide; find_may_provide) + + (eapply eplus_right_MayProvide; find_may_provide). + +#[global] Hint Extern 1 (MayProvide (eplus _ _) _) => + find_may_provide : typeclass_instances. + +#[program] +Instance refl_Distinguish (F E : effect) + : @Distinguish F F E ( @refl_MayProvide F) ( @refl_Provide F) ( @default_MayProvide F E). + +#[program] +Instance eplus_left_default_Distinguish (Fx Ex F E : effect) + `{M1 : MayProvide Fx F} `{P1 : @Provide Fx F M1} + : @Distinguish (Fx + Ex) F E + ( @eplus_left_MayProvide Fx F Ex M1) + ( @eplus_left_Provide Fx F Ex M1 P1) + ( @default_MayProvide _ E). + +#[program] +Instance eplus_right_default_Distinguish (Fx Ex F E : effect) + `{M1 : MayProvide Ex F} `{P1 : @Provide Ex F M1} + : @Distinguish (Fx + Ex) F E + ( @eplus_right_MayProvide Fx Ex F M1) + ( @eplus_right_Provide Fx Ex F M1 P1) + ( @default_MayProvide _ E). + +#[program] +Instance eplus_left_may_right_Distinguish (Fx Ex F E : effect) + `{M1 : MayProvide Fx F} `{P1 : @Provide Fx F M1} `{M2 : MayProvide Ex E} + : @Distinguish (Fx + Ex) F E + ( @eplus_left_MayProvide Fx F Ex M1) + ( @eplus_left_Provide Fx F Ex M1 P1) + ( @eplus_right_MayProvide Fx Ex E M2). + +#[program] +Instance eplus_right_may_left_Distinguish (Fx Ex F E : effect) + `{M1 : MayProvide Ex F} `{P1 : @Provide Ex F M1} `{M2 : MayProvide Fx E} + : @Distinguish (Fx + Ex) F E + ( @eplus_right_MayProvide Fx Ex F M1) + ( @eplus_right_Provide Fx Ex F M1 P1) + ( @eplus_left_MayProvide Fx E Ex M2). + +#[program] +Instance eplus_left_distinguish_left_Distinguish (Fx Ex F E : effect) + `{M1 : MayProvide Fx F} `{P1 : @Provide Fx F M1} `{M2 : MayProvide Fx E} + `{@Distinguish Fx F E M1 P1 M2} + : @Distinguish (Fx + Ex) F E + ( @eplus_left_MayProvide Fx F Ex M1) + ( @eplus_left_Provide Fx F Ex M1 P1) + ( @eplus_left_MayProvide Fx E Ex M2). + +Next Obligation. + apply distinguish. +Defined. + +#[program] +Instance eplus_right_distinguish_right_Distinguish (Fx Ex F E : effect) + `{M1 : MayProvide Ex F} `{P1 : @Provide Ex F M1} `{M2 : MayProvide Ex E} + `{@Distinguish Ex F E M1 P1 M2} + : @Distinguish (Fx + Ex) F E + ( @eplus_right_MayProvide Fx Ex F M1) + ( @eplus_right_Provide Fx Ex F M1 P1) + ( @eplus_right_MayProvide Fx Ex E M2). + +Next Obligation. + apply distinguish. +Defined. diff --git a/theories/Freer.v b/theories/Freer.v new file mode 100644 index 0000000..681ab00 --- /dev/null +++ b/theories/Freer.v @@ -0,0 +1,255 @@ +(* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) + +(* Copyright (C) 2018–2020 ANSSI *) + +(** In [FreeSpec.Core.Effect], we have introduced the [effect] type, to + model the set of primitives an impure computation can use. We also introduce + [MayProvide], [Provide] and [Distinguish]. They are three type classes which + allow for manipulating _polymorphic effect composite_. + + + In this library, we provide the [freer] monad, defined after the + <> monad introduced by the <> package (see + <>). *) + +From FreerDPS Require Import Init. +From mathcomp Require Import all_boot. +From FreerDPS Require Export Effect. + +Local Open Scope monae_scope. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Generalizable All Variables. + +(** We introduce the [freer] monad to describe impure computations, that is + computations which uses primitives from certain effects. *) + +(** * Definition *) + +(** The [freer] monad is an inductive datatype with two parameters: the + effect [F] to be used, and the type [α] of the result of the computation. + The fact that [freer] is inductive rather than co-inductive means it is not + possible to describe infinite computations. This also means it is possible + to interpret impure computations within Coq, providing an operational + semantics for [F]. *) + +Inductive freer (F : effect) (α : Type) : Type := +| pure (x : α) : freer F α +| impure {β} (op : F β) (f : β -> freer F α) : freer F α. + +Arguments pure [F α] (x). +Arguments impure [F α β] (op f). + +Fixpoint freer_bind (F : effect) {α β} (p : freer F α) (f : α -> freer F β) + : freer F β := + match p with + | pure x => f x + | impure Y op g => impure op (fun x => freer_bind (g x) f) + end. + +Declare Scope freer_scope. +Bind Scope freer_scope with freer. +Delimit Scope freer_scope with freer. + +(** We then provide the necessary instances of the <> Monad + typeclasses hierarchy. *) +(* mode of the freer monad *) +Section freer. +Context (F : effect). +Notation acto := (@freer F). + +Let ret : idfun ~~> acto := fun x => @pure F x. + +Let bind := fun A B m f => @freer_bind F A B m f. + +Let left_neutral : BindLaws.left_neutral bind ret. +Proof. by []. Qed. + +Let right_neutral : BindLaws.right_neutral bind ret. +Proof. by move=> T; elim => //b op f ih/=; congr impure; exact/funext. Qed. + +Let assoc : BindLaws.associative bind. +Proof. by move=> A B C + f g; elim=>//= *; congr impure; exact/funext. Qed. + +#[export] +HB.instance Definition _ := @isMonad_ret_bind.Build acto ret bind + left_neutral right_neutral assoc. + +(** * Defining Freer Computations *) + +(** FreeSpec users shall not use the [freer] monad constructors directly. The + [pure] function from the [Applicative] typeclass allows for defining pure + computations which do not depend on any freer primitive. The [bind] + function from the [Monad] typeclass allows for seamlessly combine freer + computations together. + + To complete these two monadic operations, we introduce the [request] + function, whose purpose is to define an freer computation that uses a given + primitive [op] from an effect [F], and returns its result. [request] does + not parameterize the [freer] monad with [F] directly, but rather with a + generic effect [Fx]. [Fx] is constrained with the [Provide] notation, so + that it has to provide at least [F]'s primitives. *) + +End freer. + +HB.mixin Record isMonadFreer (F : effect) (M : UU0 -> UU0) of Monad M := { + request : F ~~> M ; + denote (N : monad) (l : F ~~> N) : M ~~> N ; + denote_ret : forall (N : monad) (l : F ~~> N) X (x : X), + denote N l X (Ret x) = Ret x ; + denote_bind : forall (N : monad) (l : F ~~> N) X Y m (f : X -> M Y), + denote N l Y (m >>= f) = denote N l X m >>= (denote N l Y \o f) ; + denote_request : forall (N : monad) (l : F ~~> N) X (op : F X), + denote N l X (request X op) = l X op ; + denote_unique : forall (N : monad) (l : F ~~> N) (denote' : M ~~> N), + (forall X (x : X), denote' X (ret X x) = Ret x) -> + (forall X Y (m : M X) (f : X -> M Y), denote' Y (m >>= f) = + denote' X m >>= (denote' Y \o f)) -> + (forall X (op : F X), denote' X (request X op) = l X op) -> + forall X (m : M X), denote' X m = denote N l X m +}. + +#[short(type=freerMonad)] +HB.structure Definition MonadFreer (F : effect) := + {M of isMonadFreer F M & isMonad M & isFunctor M}. + +(** * Monad Instances *) +Module Freer. +Section freer. +Variable F : effect. + +Import Monad. + +Notation acto := (@freer F). + +Definition request_effect : F ~~> acto := fun α op => + impure (inj_p op) (@pure _ _). + +Definition lifter (M : monad) `(l : F ~~> M) : acto ~~> M := + fix aux a (p : acto a) := + match p with + | pure x => Ret x + | impure Y op f => l _ op >>= fun x => aux a (f x) + end. + +Let lifter_ret (cm : monad) (lifter_effect : F ~~> cm) X (x : X) : + lifter lifter_effect (ret X x) = @hierarchy.ret cm X x. +Proof. by []. Qed. + +Let lifter_bind : forall (cm : monad) (lifter_effect : F ~~> cm) X Y m + (f : X -> acto Y), + lifter lifter_effect (m >>= f) = + lifter lifter_effect m >>= (fun x => lifter lifter_effect (f x)). +Proof. + move=>cm lifter_effect X Y m f. + elim:m=>[x | Z fz k]/=. + - by rewrite !bindretf. + rewrite bindA=>H. + congr bind. + exact/boolp.funext/H. +Qed. + +Let lifter_trigger (cm : monad) (lifter_effect : F ~~> cm) X (op : F X) : + lifter lifter_effect (request_effect op) = lifter_effect X op. +Proof. by rewrite /lifter /request_effect/= bindmret. Qed. + +Let lifter_unique : forall (cm : monad) (lifter_effect : F ~~> cm) + (lifter' : acto ~~> cm), + (forall X (x : X), lifter' X (ret X x) = @hierarchy.ret cm X x) -> + (forall X Y (m : acto X) (f : X -> acto Y), + lifter' Y (m >>= f) = lifter' X m >>= (fun x => lifter' Y (f x))) -> + (forall X (op : F X), + lifter' X (request_effect op) = lifter_effect X op) -> + forall X (m : acto X), lifter' X m = lifter lifter_effect m. +Proof. + move=>cm lifter_effect lifter' dret' dbind' dtrigger' X m. + rewrite/lifter. + elim:m=>[x| Y fy k Hy]/=. + - exact/dret'. + under [in RHS]eq_bind do rewrite -Hy. + by rewrite -dtrigger'-dbind'/request_effect. +Qed. + +#[export] +HB.instance Definition _ := isMonadFreer.Build F acto + lifter_ret lifter_bind lifter_trigger lifter_unique. + +End freer. +End Freer. +HB.export Freer. + +Lemma denote_if : forall (F : effect) (M : freerMonad F) (cm : monad) + (lifter_effect : F ~~> cm) X (m m' : M X) b, + denote cm lifter_effect X (if b then m else m') = + if b then (denote cm lifter_effect X m) else (denote cm lifter_effect X m'). +Proof. by move=> ? ? ? ? ? ? ?; case. Qed. + +Lemma denote_when_request (Fx : effect) (M : freerMonad Fx) (cm : monad) + (l : Fx ~~> cm) (A X : Type) (guard : A -> bool) (op : Fx X) : + denote cm l unit \o + (fun x => when (guard x) (request X op : M X)) = + fun x => + if guard x then + l X op >>= (denote cm l unit \o fun=> (skip : M unit)) + else denote cm l unit (skip : M unit). +Proof. +by apply/funext=> x; rewrite compE denote_if; + case: (guard x)=> //=; + rewrite denote_bind denote_request. +Qed. + +(* example of freer monad using state *) +Module ImpSt. +Section impstate. +Context (F : effect) (S : UU0). + +Import Monad. + +Definition request_effect {Fx : effect} `{Provide Fx F} {A} + (op : F A) : freer Fx A := + impure (inj_p op) (@pure _ _). + +Let iget `{Provide F (STORE S)} : freer F S := request_effect (inj_p Get). +Let iput `{Provide F (STORE S)} (s : S) : freer F () := + request_effect (inj_p (Put s)). + +(** Note: there have been attempts to turn [request] into a typeclass + function (to seamlessly use [request] with a [MonadTrans] instance such as + [state_t]). The reason why it has not been kept into the codebase is that + the flexibility it gives for writing code has a real impact on the + verification process. It is simpler to reason about “pure” freer + computations (that is, not within a monad stack), then wrapping these + computations thanks to [lift]. + + The <> provides notations (inspired by the do notation of + Haskell) to write monadic functions more easily. These notations live + inside the [monad_scope]. *) + +(** * Lift *) + +End impstate. +End ImpSt. + +(* HB.export ImpSt. *) + +Module FreerFuns. +Definition trigger {Fx : effect} `{Provide Fx F} + {im : freerMonad Fx} : F ~~> im := + fun a op => request a (inj_p op). + +Arguments trigger {_ _ _ _ _ _} _. + +Definition iget {S} `{Provide F (STORE S)} {im : freerMonad F} : im S := + trigger Get. + +Definition iput {S} `{Provide F (STORE S)} {im : freerMonad F} + (s : S) : im unit := + trigger (Put s). +End FreerFuns. + +HB.export FreerFuns. diff --git a/theories/Hoare.v b/theories/Hoare.v index cd49a4d..ae57da0 100644 --- a/theories/Hoare.v +++ b/theories/Hoare.v @@ -4,15 +4,13 @@ (* Copyright (C) 2018–2020 ANSSI *) +From FreerDPS Require Import Init. (* From ExtLib Require Import Functor Applicative Monad. *) -From FreerDPS Require Import Interface Impure Contract. -From monae Require Import preamble hierarchy. -From mathcomp Require Import ssreflect. -From HB Require Import structures. +From FreerDPS Require Import Effect Freer Contract mathcomp_extra. +From mathcomp Require Import all_boot classical_sets. Generalizable All Variables. - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -30,121 +28,287 @@ Unset Printing Implicit Defensive. (** * Definition *) -Record hoare (Σ : Type) (α : Type) : Type := - mk_hoare { pre : Σ -> Prop - ; post : Σ -> α -> Σ -> Prop - }. +Record hoare (Σ : Type) (α : Type) : Type := mk_hoare { + pre : set Σ ; + post : Σ -> α -> set Σ }. Arguments mk_hoare {Σ α} (pre post). Arguments pre {Σ α} (_ _). Arguments post {Σ α} (_ _ _). Definition hoare_pure {Σ α} (x : α) : hoare Σ α := - mk_hoare (fun _ => True) (fun s y s' => x = y /\ s = s'). + mk_hoare [set: Σ] (fun s y s' => x = y /\ s = s'). -Definition hoare_bind {Σ α β} (h : hoare Σ α) (k : α -> hoare Σ β) : hoare Σ β := +Definition hoare_bind {Σ α β} + (h : hoare Σ α) (k : α -> hoare Σ β) : hoare Σ β := mk_hoare (fun s => pre h s /\ (forall x s', post h s x s' -> pre (k x) s')) (fun s x s'' => exists y s', post h s y s' /\ post (k y) s' x s''). -(** * Instances *) - -(** ** Functor *) - Definition hoare_map {Σ α β} (f : α -> β) (h : hoare Σ α) : hoare Σ β := hoare_bind h (fun x => hoare_pure (f x)). -(** ** Applicative *) - Definition hoare_apply {Σ α β} (hf : hoare Σ (α -> β)) (h : hoare Σ α) : hoare Σ β := hoare_bind hf (fun f => hoare_map f h). (** ** Monad *) + +(** Easier to had future laws from there. *) +HB.mixin Record isMonadHoare (S : UU0) + (M : UU0 -> UU0) of Monad M := {}. + +#[short(type=hoareMonad)] +HB.structure Definition MonadHoare (S : UU0) := + {M of isMonadHoare S M &}. + Module hoare_mon. - Section hm. - Variable Σ: UU0. - Let ret := @hoare_pure Σ. - Let bind := @hoare_bind Σ. - - Let right_neutral : BindLaws.right_neutral bind ret. - Proof. - move=>A. rewrite/bind/ret/hoare_bind/hoare_pure/=. - case=>pr po. - congr mk_hoare; apply/boolp.funext=>s. - - apply/boolp.propext; tauto. - apply/boolp.funext=>a; - apply/boolp.funext=>s'. - rewrite boolp.propeqE. - split. case=>a'; case=>s''. - all: move=>/=H. - - firstorder congruence. - by exists a; exists s'. - (* Prop exten *) - Qed. +Section hm. +Variable Σ : UU0. +Let ret := @hoare_pure Σ. +Let bind := @hoare_bind Σ. + +Let right_neutral : BindLaws.right_neutral bind ret. +Proof. +move=> A [pr po]. +rewrite /bind /ret /hoare_bind /hoare_pure/=; congr mk_hoare. +- by apply/funext => s/=; apply/propext; split; tauto. +- apply/eq3_fun => s a s''. + under eq2_exists do rewrite andA. + by rewrite ex2C ex2_eqr ex_eqr. +Qed. (* Local Open Scope ssripat_scope. *) - Let left_neutral : BindLaws.left_neutral bind ret. - Proof. - move=>A B a f. rewrite/bind/ret/hoare_bind/hoare_pure/=. - case eFA: (f a). - congr mk_hoare; apply/boolp.funext=>s. - - apply/boolp.propext=>/=; firstorder. - (* How to specialize ? *) - + by move: H0 eFA => /(_ a s) /[swap] -> /=; exact. - + by subst; rewrite eFA. - - apply/boolp.funext=>b; apply/boolp.funext=>s'. - rewrite boolp.propeqE. - split. - - case=>a'; case=>s''. - all: move=>/=H. - - firstorder. by rewrite -H-H1 eFA in H0. - - exists a; exists s. - rewrite eFA/=; - firstorder. - Qed. - - Let assoc : BindLaws.associative bind. - Proof. - move=>A B C m f g. rewrite/bind/ret/hoare_bind/hoare_pure/=. - case: m=>prA poA. - congr mk_hoare; apply/boolp.funext=>s. - - apply/boolp.propext=>/=; firstorder. - move:x s' x0 s'0 H0 H H1 H2 H3=>a s' b s'' Hcomb _ _ Hpostm Hpostf. - case eGB : (g b). - (* => /=[prC poC]. *) - move: Hcomb eGB=>/(_ b s'')/[swap]->; apply. - exists a; exists s'. - by split. - apply/boolp.funext=>c; - apply/boolp.funext=>s'''. - apply/boolp.propext=>/=. - firstorder; - move:x x0 x1 x2 H H0 H1=>x s'' y s' HpostA Hpostf Hpostg; - exists y; - exists s'; - firstorder. - Qed. - - HB.instance Definition _ := isMonad_ret_bind.Build (hoare Σ) left_neutral right_neutral assoc. - - End hm. +Let left_neutral : BindLaws.left_neutral bind ret. +Proof. +move=> A B a f; rewrite /bind /ret /hoare_bind /hoare_pure/=. +move fa : (f a) => [pr po]; congr mk_hoare. +- apply/funext=> s; rewrite andTP; apply/propext; split. + + by move=> /(_ a s); rewrite fa/=; exact. + + by move=> prs _ _ [<- <-]; rewrite fa. +- apply/eq3_fun => s b s'. + under eq2_exists do rewrite andC andA. + rewrite ex2C. + under eq_exists do rewrite ex_andl. + by rewrite ex_eqr_sym ex_eqr_sym fa. +Qed. + +Let assoc : BindLaws.associative bind. +Proof. +move=> A B C m f g; rewrite /bind /ret /hoare_bind /hoare_pure/=. +case: m => prA poA/=; congr mk_hoare. +- apply/funext => s; apply/propext; split. + + move=> [[prAs poApre postpre]]. + split => // a s1 sas1; split=> [|b s2 s'bs2]. + exact: poApre. + by apply: postpre; exists a, s1. + + move=> [prAs poApre]; split. + by split=> // a s1 /poApre[]. + move=> b s1 [x [s2]] [] /poApre [fxs2] /[swap] s2bs1. + exact. +- apply: eq3_fun => s c s1. + under eq2_exists do rewrite -ex_andl. + rewrite ex3C; apply: eq_exists => a. + under eq2_exists do rewrite -ex_andl. + rewrite ex3C; apply: eq_exists => s2. + rewrite -ex_andr. + under [in RHS]eq_exists do rewrite -ex_andr. + by under [in RHS]eq2_exists do rewrite andA. +Qed. + +HB.instance Definition _ := isMonad_ret_bind.Build (hoare Σ) + left_neutral right_neutral assoc. + +End hm. End hoare_mon. HB.export hoare_mon. +HB.instance Definition _ (S : UU0) := + isMonadHoare.Build S (hoare S). + +(** ** Primitive Views *) + +Lemma hoare_bindE {Σ α β} (h : hoare Σ α) (k : α -> hoare Σ β) : + @bind (hoare Σ) α β h k = hoare_bind h k. +Proof. by []. Qed. + +(** This actually may not be really useful as we reason + * either on pre or on post cond. + *) +Lemma hoare_ext {Σ α} (h1 h2 : hoare Σ α) : + (forall s, pre h1 s <-> pre h2 s) -> + (forall s x s', post h1 s x s' <-> post h2 s x s') -> + h1 = h2. +Proof. + case: h1 => pre1 post1; case: h2 => pre2 post2. + move=> pre_equiv post_equiv /=. + congr mk_hoare. + - apply/boolp.funext=> s. + exact/boolp.propext/pre_equiv. + apply/eq3_fun=> s x s'. + exact/boolp.propext/post_equiv. +Qed. + +(** ** Invariant Preservation *) + +Definition preserves_invariant {S A} + (invariant : S -> Prop) (h : hoare S A) := + forall state result state', + pre h state -> + post h state result state' -> + invariant state -> + invariant state'. + +Lemma preserves_invariant_ret {S A} + (invariant : S -> Prop) (result : A) : + preserves_invariant invariant (@ret (hoare S) A result). +Proof. by move=>???? [_ <-]. Qed. + +Lemma preserves_invariant_bind {S A B} (invariant : S -> Prop) + (h : hoare S A) (k : A -> hoare S B) : + preserves_invariant invariant h -> + (forall result, preserves_invariant invariant (k result)) -> + preserves_invariant invariant (h >>= k). +Proof. +move=> h_preserves k_preserves ??? [h_pre k_pre] [? [? [h_post k_post]]] Hsafe. +apply: k_preserves. +- exact/k_pre/h_post. +- exact: k_post. +by move: h_pre h_post Hsafe; exact: h_preserves. +Qed. + (** * Reasoning about Programs *) -Definition interface_to_hoare `{MayProvide ix i} `(c : contract i Ω) : ix ~~> hoare Ω := - fun a e => - {| pre := fun ω => gen_caller_obligation c ω e - ; post := fun ω x ω' => gen_callee_obligation c ω e x - /\ ω' = gen_witness_update c ω e x - |}. +Definition hoare_of_contract {Fx : effect} `{MayProvide Fx F} + `(c : contract F Ω) + : Fx ~~> hoare Ω := + fun a op => mk_hoare + (gen_caller_obligation c ^~ op) + (fun ω x ω' => ω' = gen_witness_update c ω op x /\ + gen_callee_obligation c ω op x). + +Definition to_hoare `{MayProvide Fx F} {im : freerMonad Fx} + `(c : contract F Ω) + : im ~~> hoare Ω := + denote _ (hoare_of_contract c). +Arguments to_hoare {Fx F _ im Ω} c {α} : rename. + +(** A Hoare triple can be interpreted from the program `p` + * through the contract `c`. + *) +Notation "p |> c" := (to_hoare c p) + (at level 50, no associativity). + +(* --------------------------------- Facts ---------------------------------- *) + +Section GenericToHoareSection. +Variable Fx : effect. +Context `{MayProvide Fx F} {im : freerMonad Fx} `(c : contract F Ω). + +Lemma to_hoare_requestE `(op : Fx a) : + to_hoare (im:=im) c (request a op) = hoare_of_contract c op. +Proof. exact: denote_request. Qed. + +Lemma to_hoare_skip_preI (ω : Ω) : + pre ((skip : im unit) |> c) ω. +Proof. by rewrite /to_hoare denote_ret. Qed. + +Section BindFacts. +Context `(p : im a) `(f : a -> im b). + +Lemma to_hoare_bindE : + to_hoare c (p >>= f) = + to_hoare c p >>= fun x => to_hoare c (f x). +Proof. exact: denote_bind. Qed. + +Lemma th_pre_bindA (ω : Ω) : + pre (to_hoare c p) ω -> + (forall x ω', + post (to_hoare c p) ω x ω' -> + pre (to_hoare c (f x)) ω') -> + pre (to_hoare c (p >>= f)) ω. +Proof. by move=> prefix suffix; rewrite to_hoare_bindE hoare_bindE; split. Qed. + +Lemma th_post_bindA (ω : Ω) (y : b) (ω' : Ω) : + post (to_hoare c (p >>= f)) ω y ω' <-> + exists x ω'', + post (to_hoare c p) ω x ω'' /\ post (to_hoare c (f x)) ω'' y ω'. +Proof. by rewrite to_hoare_bindE hoare_bindE. Qed. + +End BindFacts. + +Section WhenFacts. +Context `(p : im a) (guard : bool). + +Lemma to_hoare_when_preE (ω : Ω) : + pre (when guard p |> c) ω <-> + if guard then pre (p |> c) ω else True. +Proof. +by case: guard=> /=; + [rewrite to_hoare_bindE; split=> [[ ] | ] //|]; + split=> // *; exact: to_hoare_skip_preI. +Qed. + +Lemma to_hoare_when_postE (ω : Ω) (x : unit) (ω' : Ω) : + post (when guard p |> c) ω x ω' <-> + if guard + then exists y, post (p |> c) ω y ω' + else ω' = ω. +Proof. +case: x; case: guard=> /=; + rewrite ?th_post_bindA /to_hoare denote_ret; + last first. +- by split=> [[_ ->] | <-]. +by split=> [[y [? [? [_ <-]]]] | [y ?]]; + exists y=>//; + exists ω'; split. +Qed. + +End WhenFacts. +End GenericToHoareSection. + +Section ToHoareDistinguishSection. +Context {Fx F G : effect} + `{MayProvide Fx F, Provide Fx G, Distinguish Fx G F} + {im : freerMonad Fx} `(c : contract F Ω) + {A} (op : G A). + +(* Local Notation used to fix the freerMonad used with the to_hoare mapper. *) +Local Notation "p ||> c" := (to_hoare (im:=im) c p) + (at level 50, no associativity). + +Lemma to_hoare_distinguished_request_preI + (ω : Ω) : + pre (trigger op ||> c) ω. +Proof. +by rewrite to_hoare_requestE /hoare_of_contract + /gen_caller_obligation (@distinguish Fx G F). +Qed. -Definition to_hoare `{MayProvide ix i} {im : impureMonad ix} `(c : contract i Ω) - : im ~~> hoare Ω := - impure_lift _ (interface_to_hoare c). +Lemma to_hoare_distinguished_request_postE + (ω : Ω) (x : A) (ω' : Ω) : + post (trigger op ||> c) ω x ω' <-> + ω' = ω. +Proof. +by rewrite to_hoare_requestE /= + /gen_witness_update /gen_callee_obligation + (@distinguish Fx G F); + split=> [[-> _] | ->]. +Qed. +End ToHoareDistinguishSection. -Arguments to_hoare {ix i _ im Ω} c {α} : rename. +Module ToHoareFreerBridge. +(* Bridging lemma. Should ALWAYS be used carefully. *) +Lemma to_hoare_reifyE `{MayProvide Fx F} {im : freerMonad Fx} + `(c : contract F Ω) `(p : im A) : + to_hoare (im:=freer Fx) c + (denote (freer Fx) (@request Fx (freer Fx)) A p) + = to_hoare (im:=im) c p. +Proof. +by rewrite /to_hoare; + apply: (denote_unique (hoare Ω) (hoare_of_contract c) + (fun X => denote _ _ X \o denote _ _ X))=> *; + rewrite compE ?denote_ret ?denote_bind ?denote_request. +Qed. +End ToHoareFreerBridge. diff --git a/theories/HoareFacts.v b/theories/HoareFacts.v deleted file mode 100644 index 13b1be2..0000000 --- a/theories/HoareFacts.v +++ /dev/null @@ -1,159 +0,0 @@ -(* This Source Code Form is subject to the terms of the Mozilla Public - * License, v. 2.0. If a copy of the MPL was not distributed with this - * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) - -(* Copyright (C) 2018–2020 ANSSI *) - -From mathcomp Require Import ssreflect. -From FreerDPS Require Import Interface Impure Contract Hoare. -From monae Require Import preamble hierarchy. -Generalizable All Variables. - -(** * General Lemmas *) - -Lemma to_hoare_step `{MayProvide ix i} `(c : contract i Ω) - `(e : ix a) `(f : a -> impure ix a) - `(hpre : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (request_then e f)) ω) - (x : a) (step : gen_callee_obligation c ω e x) - : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (f x)) (gen_witness_update c ω e x). - -Proof. - destruct hpre as [hbefore hafter]. - apply hafter. - cbn. - unfold gen_callee_obligation, gen_witness_update in *. - now destruct proj_p. -Qed. - -#[global] Hint Resolve to_hoare_step : freespec. - -Lemma to_hoare_pre_bind_assoc `{MayProvide ix i} `(c : contract i Ω) - `(p : impure ix a) `(Hp : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c p) ω) - `(f : a -> impure ix b) - (run : forall (x : a) (ω' : Ω), - post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c p) ω x ω' -> pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (f x)) ω') - : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (impure_bind p f)) ω. - -Proof. - revert ω Hp run. - induction p; intros ω Hp run. - + now apply run. - + cbn in Hp. - destruct Hp as [He Hn]. - change (impure_bind (request_then e f0) f) - with (impure_bind (request_then e (fun x => f0 x)) f). - split. - ++ exact He. - ++ intros x ω' Hpost. - specialize Hn with x ω'. - destruct Hpost. - rewrite -> H2 in *. - assert (Hpre : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (f0 x)) (gen_witness_update c ω e x)) - by now apply Hn. - apply H0; [ apply Hpre |]. - intros y ω'' Hpost. - apply run. - cbn. - exists x. - exists ω'. - split; [split |]. - +++ exact H1. - +++ exact H2. - +++ rewrite H2. - exact Hpost. -Qed. - -Lemma to_hoare_post_bind_assoc `{MayProvide ix i} `(c : contract i Ω) - `(p : impure ix a) `(f : a -> impure ix b) - `(Hp : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c (impure_bind p f)) ω x ω') - : exists y ω'', - post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) c p) ω y ω'' /\ post (to_hoare c (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) $ f y) ω'' x ω'. - -Proof. -move: ω Hp; elim p=>[in_a|Y j k IH] ω. -- by exists in_a, ω. -case=>y [ω'' [Hp1 ]]. -move:IH=>/[apply]. -move=> [z [ω''' [Hp2 Hp3]]]. -exists z, ω'''. -split=>//. -exists y, ω''. -by split. -Qed. - -Lemma to_hoare_contractprod `{Provide ix i, Provide ix j} - `(ci : contract i Ωi) `(cj : contract j Ωj) - `(p : impure ix a) - `(prei : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) ci p) ωi) `(prej : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) cj p) ωj) - : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure ix) (ci * cj) p) (ωi, ωj). - -Proof. - revert ωi prei ωj prej. - induction p; intros ωi prei ωj prej. - + auto. - + destruct prei as [calleri Hcalleei]. - destruct prej as [callerj Hcalleej]. - split. - ++ now split. - ++ intros x [ωi' ωj'] [[calleei calleej] equωs]. - cbn in equωs. - inversion equωs; subst. - apply H3. - +++ apply Hcalleei. - now split. - +++ apply Hcalleej. - now split. -Qed. - -#[global] Hint Resolve to_hoare_contractprod : freespec. - -Lemma contract_equ_pre `(c1 : contract i Ω1) `(c2 : contract i Ω2) - `(equ : contract_equ c1 c2) (ω1 : Ω1) - `(p : impure i A) - : pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure i) c1 p) ω1 <-> pre (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure i) c2 p) (contract_iso_lr equ ω1). - -Proof. - elim: equ => f g iso1 iso2 caller_equ callee_equ witness_equ. - move: ω1. - elim: p=> [a | B e k IH] ω1. - - by split. - rewrite /=/gen_caller_obligation/gen_callee_obligation/gen_witness_update/=. - rewrite (caller_equ ω1 B e). - setoid_rewrite (callee_equ ω1 B e). - split => [[ocaller onext] | [ocaller onext]]; - split => // x ω1' [ocallee owitness]. - - by rewrite owitness -witness_equ -IH; eauto. - rewrite IH; eauto. - rewrite owitness /= witness_equ; eauto. -Qed. - -#[global] Hint Resolve contract_equ_pre : freespec. - -Lemma contract_equ_post `(c1 : contract i Ω1) `(c2 : contract i Ω2) - `(equ : contract_equ c1 c2) (ω1 ω1' : Ω1) - `(p : impure i a) (x : a) - (post1 : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure i) c1 p) ω1 x ω1') - : post (to_hoare (im:=ImpureModule_acto__canonical__Impure_MonadImpure i) c2 p) (contract_iso_lr equ ω1) x (contract_iso_lr equ ω1'). - -Proof. - induction equ. - cbn in *. - revert x ω1 ω1' post1. - induction p; intros y ω1 ω1' post1. - + destruct post1 as [xequ ω1equ]. - cbn. - now subst. - + cbn in post1. - destruct post1 as [x [ω1'' [[ocallee owitness] post1]]]. - eapply H in post1. - exists x. - exists (f ω1''). - split; auto. - cbn. - repeat split. - ++ eapply callee_equ; eauto. - ++ rewrite owitness. - apply witness_equ. -Qed. - -#[global] Hint Resolve contract_equ_post : freespec. diff --git a/theories/Impure.v b/theories/Impure.v deleted file mode 100644 index e92a80c..0000000 --- a/theories/Impure.v +++ /dev/null @@ -1,253 +0,0 @@ -(* This Source Code Form is subject to the terms of the Mozilla Public - * License, v. 2.0. If a copy of the MPL was not distributed with this - * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) - -(* Copyright (C) 2018–2020 ANSSI *) - -(** In [FreeSpec.Core.Interface], we have introduced the [interface] type, to - model the set of primitives an impure computation can use. We also introduce - [MayProvide], [Provide] and [Distinguish]. They are three type classes which - allow for manipulating _polymorphic interface composite_. - - - In this library, we provide the [impure] monad, defined after the - <> monad introduced by the <> package (see - <>). *) - -From mathcomp Require Import ssreflect ssrfun. -From Stdlib Require Import Program Setoid Morphisms. -From HB Require Import structures. -From monae Require Import preamble hierarchy. -From FreerDPS Require Export Interface. - -Local Open Scope monae_scope. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Generalizable All Variables. - -(** We introduce the [impure] monad to describe impure computations, that is - computations which uses primitives from certain interfaces. *) - -(** * Definition *) - -(** The [impure] monad is an inductive datatype with two parameters: the - interface [i] to be used, and the type [α] of the result of the computation. - The fact that [impure] is inductive rather than co-inductive means it is not - possible to describe infinite computations. This also means it is possible - to interpret impure computations within Coq, providing an operational - semantics for [i]. *) - -Inductive impure (i : interface) (α : Type) : Type := -| local (x : α) : impure i α -| request_then {β} (e : i β) (f : β -> impure i α) : impure i α. - -Arguments local [i α] (x). -Arguments request_then [i α β] (e f). - -Register impure as freespec.core.impure.type. -Register local as freespec.core.impure.local. -Register request_then as freespec.core.impure.request_then. - -Declare Scope impure_scope. -Bind Scope impure_scope with impure. -Delimit Scope impure_scope with impure. - -HB.mixin Record isMonadImpure (i : interface) (M : UU0 -> UU0) of Monad M := { - request : i ~~> M ; - impure_lift (N : monad) (l : i ~~> N) : M ~~> N ; - impure_lift_ret : forall (N : monad) (l : i ~~> N) X (x : X), - impure_lift N l X (ret X x) = @ret N X x; - impure_lift_bind : forall (N : monad) (l : i ~~> N) X Y m (f : X -> M Y), - impure_lift N l Y (m >>= f) = (impure_lift N l X m) >>= (fun x => impure_lift N l Y (f x)) ; - impure_lift_request : forall (N : monad) (l : i ~~> N) X (fx : i X), - impure_lift N l X (request X fx) = l X fx; - impure_lift_unique : forall (N : monad) (l : i ~~> N) (impure_lift' : M ~~> N), - (forall X (x : X), impure_lift' X (ret X x) = @ret N X x) -> - (forall X Y (m : M X) (f : X -> M Y), impure_lift' Y (m >>= f) = (impure_lift' X m) >>= (fun x => impure_lift' Y (f x))) -> - (forall X (fx : i X), (impure_lift' X (request X fx)) = l X fx) -> - forall X (m : M X), impure_lift' X m = impure_lift N l X m -}. - - -#[short(type=impureMonad)] -HB.structure Definition MonadImpure (i : interface) := {M of isMonadImpure i M & isMonad M & isFunctor M}. - -(** * Monad Instances *) - -(** We then provide the necessary instances of the <> Monad - typeclasses hierarchy. *) -Module ImpureModule. -Section freer. - -Variable i : UU0 -> UU0. -Definition acto := fun X => @impure i X. -Notation FM := acto. - -Definition impure_pure {α} (x : α) : impure i α := local x. - -Let ret : idfun ~~> FM := fun _ => impure_pure. - -Fixpoint impure_bind {α β} (p : impure i α) (f : α -> impure i β) : impure i β := - match p with - | local x => f x - | request_then Y e g => request_then e (fun x => impure_bind (g x) f) - end. - -Let bind := fun A B m f => @impure_bind A B m f. - -Let left_neutral : BindLaws.left_neutral bind ret. -Proof. - by []. -Qed. - -Let right_neutral : BindLaws.right_neutral bind ret. -Proof. - move=>/=A. - elim=>[x|Y fy k IHm]//=. - congr request_then. - exact/boolp.funext=>y. -Qed. - -Let assoc : BindLaws.associative bind. -Proof. - move=>/=A B C m f g. - elim:m=>//=Y fy k IHm. - congr request_then. - exact/boolp.funext=>y. -Qed. - -HB.instance Definition _ := @isMonad_ret_bind.Build acto ret bind left_neutral right_neutral assoc. - -(** * Defining Impure Computations *) - -(** FreeSpec users shall not use the [impure] monad constructors directly. The - [pure] function from the [Applicative] typeclass allows for defining pure - computations which do not depend on any impure primitive. The [bind] - function from the [Monad] typeclass allows for seamlessly combine impure - computations together. - - To complete these two monadic operations, we introduce the [request] - function, whose purpose is to define an impure computation that uses a given - primitive [e] from an interface [i], and returns its result. [request] does - not parameterize the [impure] monad with [i] directly, but rather with a - generic interface [ix]. [ix] is constrained with the [Provide] notation, so - that it has to provide at least [i]'s primitives. *) - -End freer. -End ImpureModule. - -HB.export ImpureModule. - -Module Impure. -Section freer. - -Variable i : interface. - -Local Notation M := (acto i). - -Definition requesti : i ~~> acto i := fun α e => - request_then (inj_p e) (fun x => local x). - -Definition lifter (M : monad) `(l : i ~~> M) : acto i ~~> M := - fix aux a (p : acto i a) := - match p with - | local x => Ret x - | request_then Y e f => l _ e >>= fun x => aux a (f x) - end. - -Let lifter_ret : forall (cm : monad) (lifter_effect : i ~~> cm) X (x : X), - lifter lifter_effect (ret X x) = @hierarchy.ret cm X x. -Proof. - rewrite/=/lifter. - by []. -Qed. - - -Let lifter_bind : forall (cm : monad) (lifter_effect : i ~~> cm) X Y m (f : X -> M Y), - lifter lifter_effect (m >>= f) = ( lifter lifter_effect m) >>= (fun x => lifter lifter_effect (f x)) . -Proof. - move=>cm lifter_effect X Y m f. - elim:m=>[x | Z fz k]/=. - - by rewrite !bindretf. - rewrite bindA=>H. - congr bind. - exact/boolp.funext/H. -Qed. - -Let lifter_trigger : forall (cm : monad) (lifter_effect : i ~~> cm) X (fx : i X), - lifter lifter_effect (requesti fx) = lifter_effect X fx. -Proof. - move=>cm lifter_effect X fx. - by rewrite/lifter/requesti/=bindmret. -Qed. - -Let lifter_unique : forall (cm : monad) (lifter_effect : i ~~> cm) (lifter' : M ~~> cm), - (forall X (x : X), lifter' X (ret X x) = @hierarchy.ret cm X x) -> - (forall X Y (m : M X) (f : X -> M Y), lifter' Y (m >>= f) = (lifter' X m) >>= (fun x => lifter' Y (f x))) -> - (forall X (fx : i X), (lifter' X (requesti fx)) = lifter_effect X fx) -> - forall X (m : M X), lifter' X m = lifter lifter_effect m. -Proof. - move=>cm lifter_effect lifter' dret' dbind' dtrigger' X m. - rewrite/lifter. - elim:m=>[x| Y fy k Hy]/=. - - exact/dret'. - under [in RHS]eq_bind do rewrite -Hy. - by rewrite -dtrigger'-dbind'/requesti. -Qed. - -HB.instance Definition _ := isMonadImpure.Build i M - lifter_ret - lifter_bind - lifter_trigger - lifter_unique. - -End freer. -End Impure. -HB.export Impure. - -Lemma impure_lift_if : forall (i : interface) (M : impureMonad i) (cm : monad) (lifter_effect : i ~~> cm) X (m m' : M X) b, - impure_lift cm lifter_effect X (if b then m else m') = if b then ( impure_lift cm lifter_effect X m) else ( impure_lift cm lifter_effect X m'). -Proof. - by move=>? ? ? ? ? ? ?; case. -Qed. -HB.export impure_lift_if. - -Module ImpSt. - Section impstate. - Variable i : interface. - Variable S : UU0. -Definition requestis `{Provide ix i} {A} (e : i A): acto ix A := - request_then (inj_p e) (fun x => local x). - - Let iget `{Provide i (STORE S)} : acto i S:=requestis (inj_p Get). - Let iput `{Provide i (STORE S)} (s : S) : acto i ():=requestis (inj_p (Put s)). - -(** Note: there have been attempts to turn [request] into a typeclass - function (to seamlessly use [request] with a [MonadTrans] instance such as - [state_t]). The reason why it has not been kept into the codebase is that - the flexibility it gives for writing code has a real impact on the - verification process. It is simpler to reason about “pure” impure - computations (that is, not within a monad stack), then wrapping these - computations thanks to [lift]. - - The <> provides notations (inspired by the do notation of - Haskell) to write monadic functions more easily. These notations live - inside the [monad_scope]. *) - -(** * Lift *) - - End impstate. -End ImpSt. - -(* HB.export ImpSt. *) - -Module ImpureFuns. -Definition trigger `{Provide ix i} {im : impureMonad ix} : ix ~~> im := fun a e => request a (inj_p e). -Definition iget {S} `{Provide i (STORE S)} {im : impureMonad i} : im S:= trigger (inj_p Get). -Definition iput {S} `{Provide i (STORE S)} {im : impureMonad i} (s : S) : im unit:= trigger (inj_p (Put s)). -End ImpureFuns. - -HB.export ImpureFuns. \ No newline at end of file diff --git a/theories/Init.v b/theories/Init.v index 1c1b509..d71336d 100644 --- a/theories/Init.v +++ b/theories/Init.v @@ -5,24 +5,21 @@ (* Copyright (C) 2018–2020 ANSSI *) (** * Utils Functions *) -(* From HB Require Export structures. *) From monae Require Export preamble hierarchy. -From mathcomp Require Export ssreflect. -Ltac done := - trivial; hnf; intros; solve - [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial] - | discriminate | contradiction | split] - | match goal with H : ~ _ |- _ => solve [case H; trivial] end - | auto with freespec - ]. -Local Open Scope monae_scope. - -Definition when {X} {M : monad} (b : bool) (m : M X) : M unit := if b then m >> skip else skip. +From HB Require Export structures. +From mathcomp Require Export ssreflect boolp. + +Global Close Scope nat_scope. +Global Open Scope monae_scope. + +Definition when {X} {M : monad} (b : bool) (m : M X) : M unit := + if b then m >> skip else skip. Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). (** * Tactics *) -From Stdlib Require Export Eqdep. +(* WARNING: Move this import to its MathComp counterpart. *) +From Stdlib Require Export Eqdep Program Setoid Morphisms. Ltac ssubst := lazymatch goal with @@ -32,7 +29,7 @@ Ltac ssubst := end. Reserved Infix "===" (at level 70, no associativity). - + Generalizable All Variables. Definition function_eq {a b} (r : b -> b -> Prop) (f g : a -> b) : Prop := diff --git a/theories/Instrument.v b/theories/Instrument.v index d16c1c2..976af1f 100644 --- a/theories/Instrument.v +++ b/theories/Instrument.v @@ -4,34 +4,36 @@ (* Copyright (C) 2018–2020 ANSSI *) -From FreerDPS Require Import Interface Semantics Contract. -From monae Require Import preamble hierarchy monad_transformer monad_model. -From HB Require Import structures. +Attributes deprecated( + note="This file is unused and will probably be removed in later versions."). -From mathcomp Require Import ssreflect. +From FreerDPS Require Import Init. +From FreerDPS Require Import Effect Semantics Contract. +From monae Require Import monad_transformer monad_model. Generalizable All Variables. -Notation instrument Ω i := (stateT Ω (StateMonad.acto (semantics i))). +Notation instrument Ω F := (stateT Ω (StateMonad.acto (semantics F))). -Definition modify {S} {M : stateMonad S} (f : S -> S) : M S := get >>= +Definition modify {S} {M : stateMonad S} (f : S -> S) : M S := get >>= fun s => put (f s) >>= fun _ => Ret s. Arguments liftS {_ _ _}. -Arguments interface_to_state {_ _}. +Arguments effect_to_state {_ _}. -Program Definition interface_to_instrument `{MayProvide ix i} `(c : contract i Ω) - : ix ~~> instrument Ω ix := - fun a e => - (liftS (A:=a) $ interface_to_state e) +Program Definition effect_to_instrument + `{MayProvide Fx F} `(c : contract F Ω) + : Fx ~~> instrument Ω Fx := + fun a e => + (liftS (A:=a) $ effect_to_state e) >>= fun x => modify (fun ω => gen_witness_update c ω e x) >>= fun _ => Ret x. -Definition to_instrument `{MayProvide ix i} `(c : contract i Ω) {im : impureMonad ix} - : im ~~> instrument Ω ix := - impure_lift _ $ interface_to_instrument c. - -Arguments to_instrument {ix i _ Ω} (c) {α} : rename. +Definition to_instrument `{MayProvide Fx F} `(c : contract F Ω) + {im : freerMonad Fx} + : im ~~> instrument Ω Fx := + denote _ $ effect_to_instrument c. +Arguments to_instrument {Fx F _ Ω} (c) {α} : rename. diff --git a/theories/Interface.v b/theories/Interface.v deleted file mode 100644 index 5961d61..0000000 --- a/theories/Interface.v +++ /dev/null @@ -1,268 +0,0 @@ -(* This Source Code Form is subject to the terms of the Mozilla Public - * License, v. 2.0. If a copy of the MPL was not distributed with this - * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) - -(* Copyright (C) 2018–2020 ANSSI *) - -From FreerDPS Require Export Init. -From Stdlib Require Import Program. - -(** * Definition *) - -(** Following the definition of the <> package, interfaces in - FreeSpec are parameterized inductive types whose terms purposely describe - the primitives the interface provides. *) - -Definition interface := Type -> Type. - -Declare Scope interface_scope. -Bind Scope interface_scope with interface. - -(** Given [i : interface], a term of type [i α] identifies a primitive of [i] - expected to produce a result of type [α]. - - The simpler interface is the empty interface, which provides no primitives - whatsoever. *) - -Inductive iempty : interface := . - -(** Another example of general-purpose interface we can define is the [STORE s] - interface, where [s] is a type for a state, and [STORE s] allows for - manipulating a global, mutable variable of type [s] within an impure - computation. *) - -Inductive STORE (s : Type) : interface := -| Get : STORE s s -| Put (x : s) : STORE s unit. - -Arguments Get {s}. -Arguments Put [s] (x). - -(** According to the definition of [STORE s], an impure computation can use two - primitives. The term [Get : STORE s s] describes a primitive expected to - produce a result of type [s], that is the current value of the mutable - variable. Terms of the form [Put x : STORE s unit] describe a primitive - which does not produce any meaningful result, but is expected to update the - current value of the mutable variable. - - The use of the word “expected” to describe the primitive of [STORE s] is - voluntary. The definition of an interface does not attach any particular - semantics to the primitives it describes. This will come later, and in - fact, one interface may have many legitimate semantics. - - Impure computations are likely to use more than one interface, but the - [impure] monad takes only one argument. We introduce [iplus] (denoted by - [<+>] or [⊕]) to compose interfaces together. An impure computation - parameterized by [i ⊕ j] can therefore leverage the primitives of both [i] - and [j]. *) - -(** * Polymorphic Interface Composites *) - -(** When defining general-purpose impure computations that we expect to reuse in - different context, we want to leave the interface as a parameter, and rather - express the constraints in terms of interface availability. We tackle this - challenge by means of _interface composites_. - - - We say an interface composite [ix] _provides_ a concrete interface [i] - when there exists a function [inj_p : forall α, i α -> ix α]. - - Conversely, we can determine if a primitive of an interface composite [ix] - is forwarded to a concrete interface [i] when there exists a function - [proj_p : forall α, ix α -> option (i a)]. - - We encode this mechanics using two type classes: [MayProvide], and - [Provide]. *) - -Class MayProvide (ix i : interface) : Type := - { proj_p {α} (e : ix α) : option (i α) - }. - -Class Provide (ix i : interface) `{MayProvide ix i} : Type := - { inj_p {α} (e : i α) : ix α - ; proj_inj_p_equ {α} (e : i α) : proj_p (inj_p e) = Some e - }. - -(** We provide a default instance for [MayProvide] in the form of a function - [proj_p] which always return [None]. We give to this default instance a - ridiculously high priority number to ensure it is selected only if no other - instances are found. *) - -Instance default_MayProvide (i j : interface) : MayProvide i j|1000 := - { proj_p := fun _ _ => None - }. - -(** It is expected that, for an interface composite [ix] which provides [i] and - may provide [j], [inj_p] and [proj_p] do not mix up [i] and [j] - primitives. That is, injecting a primitive [e] of [i] inside [ix], then - projecting the resulting primitive into [j] returns [None] as long as [i] - and [j] are two different interfaces. *) - -Class Distinguish (ix i j : interface) `{Provide ix i, MayProvide ix j} : Prop := - { distinguish : forall {α} (e : i α), proj_p (i := j) (inj_p (ix := ix) e) = None - }. - -(** * Composing Interfaces *) - -(** We provide the [iplus] operator to compose interface together. That is, - [iplus] can be used to build _concrete_ (as opposed to polymorphic) - interface composite. *) - -Inductive iplus (i j : interface) (α : Type) := -| in_left (e : i α) : iplus i j α -| in_right (e : j α) : iplus i j α. - -Arguments in_left [i j α] (e). -Arguments in_right [i j α] (e). - -Register iplus as freespec.core.iplus.type. -Register in_left as freespec.core.iplus.in_left. -Register in_right as freespec.core.iplus.in_right. - -Infix "+" := iplus : interface_scope. - -(** For [iplus] to be used seamlessly as a concrete interface composite, we - provide the necessary instances for the [MayProvide], [Provide] and - [Distinguish] type classes. Note that these instances always prefer the - left operand of [iplus]. For instance, considering a situation where - there is an instance for [Provide ix i] and an instance for [Provide jx i], - the instance of [Provide (ix + jx) i] will rely on [ix]. - - The main use case for [iplus] is to locally provide an additional - interface. For instance, we can consider a [with_state] function which would - locally give access to the [STORE] interface, that is [with_state : forall - ix s α, s -> impure (ix + STORE s) α -> impure ix α]. In such a case, the - interface made locally available shall be the right operand of [iplus]. This - way, functions such as [with_state] are reentrant. If we take an example, - the following impure computation: - -<< -with_state true (with_state false get) ->> - - will return false (that is, the variable in the inner store). *) - -Instance refl_MayProvide (i : interface) : MayProvide i i := - { proj_p := fun _ e => Some e - }. - -#[program] -Instance refl_Provide (i : interface) : @Provide i i (refl_MayProvide i) := - { inj_p := fun (a : Type) (e : i a) => e - }. - -Instance iplus_left_MayProvide (ix i j : interface) `{MayProvide ix i} - : MayProvide (ix + j) i := - { proj_p := fun _ e => - match e with - | in_left e => proj_p e - | _ => None - end - }. - -#[program] -Instance iplus_left_Provide (ix i j : interface) `{Provide ix i} - : @Provide (ix + j) i (iplus_left_MayProvide ix i j) := - { inj_p := fun (a : Type) (e : i a) => in_left (inj_p e) - }. - -Next Obligation. - now rewrite proj_inj_p_equ. -Qed. - -Instance iplus_right_MayProvide (i jx j : interface) `{MayProvide jx j} - : MayProvide (i + jx) j := - { proj_p := fun _ e => - match e with - | in_right e => proj_p e - | _ => None - end - }. - -#[program] -Instance iplus_right_Provide (i jx j : interface) `{Provide jx j} - : @Provide (i + jx) j (iplus_right_MayProvide i jx j) := - { inj_p := fun _ e => in_right (inj_p e) - }. - -Next Obligation. - now rewrite proj_inj_p_equ. -Qed. - -(** By default, Coq's inference algorithm for type classe instances inference is - a depth-first search. This is not without consequence in our case. For - instance, if we consider the search of an instance for [MayProvide (i + j) - j], Coq will first try [iplus_right_MayProvide] (as explained previously), - meaning he now search for [MayProvide i j]. It turns out such an instance - exists: [default_MayProvide]. - - To circumvent this issue, we write a dedicated tactic [find_may_provide] - which attempts to find an instance for [MayProvide (?ix + ?jx) ?i] with - [refl_MayProvide], [iplus_left_MayProvide] and [iplus_right_MayProvide]. *) - -Ltac find_may_provide := - eapply refl_MayProvide + - (eapply iplus_left_MayProvide; find_may_provide) + - (eapply iplus_right_MayProvide; find_may_provide). - -#[global] Hint Extern 1 (MayProvide (iplus _ _) _) => find_may_provide : typeclass_instances. - -#[program] -Instance refl_Distinguish (i j : interface) - : @Distinguish i i j ( @refl_MayProvide i) ( @refl_Provide i) ( @default_MayProvide i j). - -#[program] -Instance iplus_left_default_Distinguish (ix jx i j : interface) - `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1} - : @Distinguish (ix + jx) i j - ( @iplus_left_MayProvide ix i jx M1) - ( @iplus_left_Provide ix i jx M1 P1) - ( @default_MayProvide _ j). - -#[program] -Instance iplus_right_default_Distinguish (ix jx i j : interface) - `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1} - : @Distinguish (ix + jx) i j - ( @iplus_right_MayProvide ix jx i M1) - ( @iplus_right_Provide ix jx i M1 P1) - ( @default_MayProvide _ j). - -#[program] -Instance iplus_left_may_right_Distinguish (ix jx i j : interface) - `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1} `{M2 : MayProvide jx j} - : @Distinguish (ix + jx) i j - ( @iplus_left_MayProvide ix i jx M1) - ( @iplus_left_Provide ix i jx M1 P1) - ( @iplus_right_MayProvide ix jx j M2). - -#[program] -Instance iplus_right_may_left_Distinguish (ix jx i j : interface) - `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1} `{M2 : MayProvide ix j} - : @Distinguish (ix + jx) i j - ( @iplus_right_MayProvide ix jx i M1) - ( @iplus_right_Provide ix jx i M1 P1) - ( @iplus_left_MayProvide ix j jx M2). - -#[program] -Instance iplus_left_distinguish_left_Distinguish (ix jx i j : interface) - `{M1 : MayProvide ix i} `{P1 : @Provide ix i M1} `{M2 : MayProvide ix j} - `{@Distinguish ix i j M1 P1 M2} - : @Distinguish (ix + jx) i j - ( @iplus_left_MayProvide ix i jx M1) - ( @iplus_left_Provide ix i jx M1 P1) - ( @iplus_left_MayProvide ix j jx M2). - -Next Obligation. - apply distinguish. -Defined. - -#[program] -Instance iplus_right_distinguish_right_Distinguish (ix jx i j : interface) - `{M1 : MayProvide jx i} `{P1 : @Provide jx i M1} `{M2 : MayProvide jx j} - `{@Distinguish jx i j M1 P1 M2} - : @Distinguish (ix + jx) i j - ( @iplus_right_MayProvide ix jx i M1) - ( @iplus_right_Provide ix jx i M1 P1) - ( @iplus_right_MayProvide ix jx j M2). - -Next Obligation. - apply distinguish. -Defined. diff --git a/theories/Semantics.v b/theories/Semantics.v index 4145bfa..a426afd 100644 --- a/theories/Semantics.v +++ b/theories/Semantics.v @@ -4,46 +4,45 @@ (* Copyright (C) 2018–2020 ANSSI *) -(** In FreeSpec, there is no particular semantics attach to interface's - primitives. Once an interface has been defined, we can provide one (or +Attributes deprecated( + note="This file is unused and will probably be removed in later versions."). + +(** In FreeSpec, there is no particular semantics attach to effect's + primitives. Once an effect has been defined, we can provide one (or more) operational semantics to interpret its primitives. *) (** * Definition *) -(** An operational [semantics] for the interface [i] is coinductively defined as - a function which can be used to interpret any primitive of [i]; it produces +(** An operational [semantics] for the effect [F] is coinductively defined as + a function which can be used to interpret any primitive of [F]; it produces an [interp_out] term. *) -From mathcomp Require Import ssreflect. - -From Stdlib Require Import Program Setoid Morphisms. +From FreerDPS Require Import Init. (* From ExtLib Require Import Monad StateMonad. *) -From FreerDPS Require Export Interface Impure. -From monae Require Import preamble hierarchy monad_model. - -From HB Require Import structures. +From FreerDPS Require Export Effect Freer. +From monae Require Import monad_model. #[local] Open Scope signature_scope. #[local] Open Scope monae_scope. -CoInductive semantics (i : interface) : Type := -| mk_semantics (f : forall (α : Type), i α -> α * semantics i) : semantics i. +CoInductive semantics (F : effect) : Type := +| mk_semantics (f : forall (α : Type), F α -> α * semantics F) : semantics F. -Arguments mk_semantics [i] (f). +Arguments mk_semantics [F] (f). (** Thus, a [semantics] does not only compute a result for a primitive, but also provides a new semantics. This is necessary to model impurity: the same primitive may or may not return the same result when called several times. - As for interfaces, the simpler [semantics] is the operational semantics for - [iempty], the empty interface. *) + As for effects, the simpler [semantics] is the operational semantics for + [eempty], the empty effect. *) -Definition iempty_semantics : semantics iempty := - mk_semantics (fun α (e : iempty α) => match e with end). +Definition eempty_semantics : semantics eempty := + mk_semantics (fun α (e : eempty α) => match e with end). -(** We also provide a semantics for the [STORE s] interface: *) +(** We also provide a semantics for the [STORE s] effect: *) CoFixpoint store {s} (init : s) : semantics (STORE s) := mk_semantics (fun α (e : STORE s α) => @@ -55,16 +54,16 @@ CoFixpoint store {s} (init : s) : semantics (STORE s) := (** We provide several helper functions to interpret primitives with semantics. *) -Definition run_effect {i α} (sem : semantics i) (e : i α) : α * semantics i := +Definition run_effect {F α} (sem : semantics F) (e : F α) : α * semantics F := match sem with mk_semantics f => f α e end. -Definition eval_effect {i α} (sem : semantics i) (e : i α) : α := +Definition eval_effect {F α} (sem : semantics F) (e : F α) : α := fst (run_effect sem e). -Definition exec_effect {i α} (sem : semantics i) (e : i α) : semantics i := +Definition exec_effect {F α} (sem : semantics F) (e : F α) : semantics F := snd (run_effect sem e). -Lemma run_effect_equation {i α} (sem : semantics i) (e : i α) +Lemma run_effect_equation {F α} (sem : semantics F) (e : F α) : run_effect sem e = (eval_effect sem e, exec_effect sem e). Proof. @@ -72,11 +71,11 @@ Proof. destruct run_effect; reflexivity. Qed. -(** Besides, and similarly to interfaces, operational semantics can and should +(** Besides, and similarly to effects, operational semantics can and should be composed together. To that end, we provide the [semprod] operator. *) -CoFixpoint semprod {i j} (sem_i : semantics i) (sem_j : semantics j) - : semantics (i + j) := +CoFixpoint semprod {F E} (sem_i : semantics F) (sem_j : semantics E) + : semantics (F + E) := mk_semantics (fun _ e => match e with | in_left e => @@ -95,14 +94,15 @@ Infix "*" := semprod : semantics_scope. (** * Interpreting Impure Computations *) -(** A term of type [impure a] describes an impure computation expected to return +(** A term of type [freer F a] describes an impure computation expected to + return a term of type [a]. Interpreting this term means actually realizing the computation and producing the result. This requires to provide an - operational semantics for the interfaces used by the computation. + operational semantics for the effects used by the computation. Some operational semantics may be defined in Gallina by means of the [semantics] type. In such a case, we provide helper functions to use them in - conjunction with [impure] terms. The terminology follows a logic similar to + conjunction with [freer] terms. The terminology follows a logic similar to the Haskell state monad: - [run_impure] interprets an impure computation [p] with an operational @@ -111,50 +111,54 @@ Infix "*" := semprod : semantics_scope. - [eval_impure] only returns the result of [p]. - [exec_impure] only returns the new operational semantics. *) -Notation interp i := (StateMonad.acto (semantics i)). +Notation interp F := (StateMonad.acto (semantics F)). -Definition interface_to_state {i:interface} : i ~~> interp i := +Definition effect_to_state {F : effect} : F ~~> interp F := fun a e => (fun sem => run_effect sem e). -Definition to_state {i} {im : impureMonad i}: im ~~> interp i := impure_lift _ interface_to_state. +Definition to_state {F} {im : freerMonad F} : im ~~> interp F := + denote _ effect_to_state. -Arguments to_state {i α} _ : rename. +Arguments to_state {F α} _ : rename. -Definition run_impure {i a} {im : impureMonad i} (sem : semantics i) (p : im a) : a * semantics i := - (to_state _ p) sem. +Definition run_impure {F a} {im : freerMonad F} + (sem : semantics F) (p : im a) : a * semantics F := + (to_state _ p) sem. -Definition eval_impure {i a} {im : impureMonad i} (sem : semantics i) (p : im a) : a := +Definition eval_impure {F a} {im : freerMonad F} + (sem : semantics F) (p : im a) : a := fst (run_impure sem p). -Definition exec_impure {i a} {im : impureMonad i} (sem : semantics i) (p : im a) : semantics i := +Definition exec_impure {F a} {im : freerMonad F} + (sem : semantics F) (p : im a) : semantics F := snd (run_impure sem p). (** * In-place Primitives Handling *) -Fixpoint with_semantics {ix j α} (sem : semantics j) (p : impure (ix + j) α) - : impure ix α := +Fixpoint with_semantics {Fx E α} + (sem : semantics E) (p : freer (Fx + E) α) : freer Fx α := match p with - | Impure.local x => Impure.local x - | request_then _ (in_right e) f => + | pure x => Freer.pure x + | impure _ (in_right e) f => let (res, next) := run_effect sem e in with_semantics next (f res) - | request_then _ (in_left e) f => - request_then e (fun x => with_semantics sem (f x)) + | impure _ (in_left e) f => + impure e (fun x => with_semantics sem (f x)) end. (** We provide [with_store], a helper function to locally provide a mutable variable. *) -Definition with_store {ix s a} (x : s) (p : impure (ix + STORE s) a) - : impure ix a := +Definition with_store {Fx s a} (x : s) (p : freer (Fx + STORE s) a) + : freer Fx a := with_semantics (store x) p. (** Nesting [with_semantics] calls works to some extends. If each - [with_semantics] provides a different interface from the rest of the stack, + [with_semantics] provides a different effect from the rest of the stack, then everything behaves as expected. If, for some reason, you end up in a - situation where you provide the exact same interface twice (typically if you + situation where you provide the exact same effect twice (typically if you use [with_store]), then the typeclass inferences will favor the deepest one in the stack. For instance, @@ -165,6 +169,6 @@ Compute (with_store 0 (with_store 1 get)). returns << - = local 1 - : impure ?ix nat + = pure 1 + : freer ?Fx nat >> *) diff --git a/theories/Tactics.v b/theories/Tactics.v deleted file mode 100644 index f38fd1b..0000000 --- a/theories/Tactics.v +++ /dev/null @@ -1,266 +0,0 @@ -(* This Source Code Form is subject to the terms of the Mozilla Public - * License, v. 2.0. If a copy of the MPL was not distributed with this - * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) - -(* Copyright (C) 2018–2020 ANSSI *) - -(* From ExtLib Require Import Monad. *) -From monae Require Import preamble hierarchy. -From FreerDPS Require Import Init Interface Contract Impure Hoare HoareFacts. - -Ltac destruct_if_when := - let equ_cond := fresh "equ_cond" in - match goal with - | |- context[when (negb ?B) _] => case_eq B; intros equ_cond; cbn - | |- context[when ?B _] => case_eq B; intros equ_cond; cbn - | |- context[if (negb ?B) then _ else _] => case_eq B; intros equ_cond; cbn - | |- context[if ?B then _ else _] => case_eq B; intros equ_cond; cbn - | _ => idtac - end. - -Ltac destruct_if_when_in hyp := - let equ_cond := fresh "equ" in - match type of hyp with - | context[when (negb ?B) _] => case_eq B; - intro equ_cond; - rewrite equ_cond in hyp - | context[when ?B _] => case_eq B; - intro equ_cond; - rewrite equ_cond in hyp - | context[if (negb ?B) then _ else _] => case_eq B; - intro equ_cond; - rewrite equ_cond in hyp - | context[if ?B then _ else _] => case_eq B; - intro equ_cond; - rewrite equ_cond in hyp - | _ => idtac - end. - -Ltac simplify_gens := - repeat match goal with - | H : True |- _ => - clear H - - | H: _ /\ _ |- _ => - destruct H - - | |- context[@proj_p ?ix ?ix (refl_MayProvide ?ix) _ ?e] => - change (@proj_p ix ix (refl_MayProvide ix) _ e) with (Some e); - cbn match; - cbn beta - - | H: context[@proj_p ?ix ?ix (refl_MayProvide ?ix) _ ?e] |- _ => - change (@proj_p ix ix (refl_MayProvide ix) _ e) with (Some e) in H; - cbn match in H; - cbn beta in H - - | |- context[gen_witness_update _ _ _ _] => - unfold gen_witness_update; - repeat (rewrite proj_inj_p_equ || rewrite distinguish) - - | H : context[gen_witness_update _ _ _ _] |- _ => - unfold gen_witness_update in H; - repeat (rewrite proj_inj_p_equ in H || rewrite distinguish in H) - - | |- context[gen_caller_obligation ?c ?ω ?e] => - unfold gen_caller_obligation; - repeat (rewrite proj_inj_p_equ || rewrite distinguish) - - | H : context[gen_caller_obligation ?c ?ω ?e] |- _ => - unfold gen_caller_obligation in H; - repeat (rewrite proj_inj_p_equ in H || rewrite distinguish in H) - - | |- context[gen_callee_obligation ?c ?ω ?e ?x] => - unfold gen_callee_obligation; - repeat (rewrite proj_inj_p_equ || rewrite distinguish) - - | H : context[gen_callee_obligation ?c ?ω ?e ?x] |- _ => - unfold gen_callee_obligation in H; - repeat (rewrite proj_inj_p_equ in H || rewrite distinguish in H) - end. - -#[local] -Ltac prove_impure := - repeat (cbn -[ - to_hoare - gen_caller_obligation - gen_callee_obligation - gen_witness_update - lifter - ] in *; - simplify_gens; - destruct_if_when); - lazymatch goal with - - | |- _ /\ _ => - split; - prove_impure - - | |- forall _ _, _ /\ _ = _ -> _ => - let x := fresh "x" in - let ω' := fresh "ω" in - let o_caller := fresh "o_caller" in - let equ := fresh "equ" in - intros x ω' [o_caller equ]; - repeat rewrite -> equ in *; clear equ; clear ω'; - prove_impure - - | |- pre ?pcond ?ω => - - lazymatch pcond with - | lifter (i:=?ifce) (M:=?m) (interface_to_hoare ?c) (A:=_) ?p => let p := (eval hnf in p) in - lazymatch p with - | request_then ?e ?f => - let o_caller := fresh "o_caller" in - assert (o_caller : gen_caller_obligation c ω e) ; - [ prove_impure | constructor; prove_impure] - | local _ => constructor - | impure_bind (impure_bind ?p ?f) ?g => - rewrite (bindA p f g); - prove_impure - | bind ?p ?f => - apply to_hoare_pre_bind_assoc; [ eauto with freespec - | let x := fresh "x" in - let ω' := fresh "ω" in - let hpost := fresh "hpost" in - intros x ω' hpost; - prove_impure - ] - | _ => eauto with freespec - end - - | to_hoare ?c ?p => let p := (eval hnf in p) in - lazymatch p with - | request_then ?e ?f => - let o_caller := fresh "o_caller" in - assert (o_caller : gen_caller_obligation c ω e) ; - [ prove_impure | constructor; prove_impure] - | local _ => constructor - | impure_bind (impure_bind ?p ?f) ?g => - rewrite (bindA p f g); - prove_impure - | bind ?p ?f => - apply to_hoare_pre_bind_assoc; [ eauto with freespec - | let x := fresh "x" in - let ω' := fresh "ω" in - let hpost := fresh "hpost" in - intros x ω' hpost; - prove_impure - ] - | _ => eauto with freespec - end - | _ => idtac "==>not handled" - end - | |- ?a => - eauto with freespec - - end. - -Tactic Notation "prove" "impure" := prove_impure. -Tactic Notation "prove" "impure" "with" ident(db) := prove_impure; eauto with db. - -Ltac unroll_post run := - repeat (cbn -[ - to_hoare - gen_caller_obligation - gen_callee_obligation - gen_witness_update - ] in *; - simplify_gens; - destruct_if_when_in run); - lazymatch type of run with - - | post (to_hoare ?c ?p) ?ω ?x ?ω' => - let p := (eval hnf in p) in - lazymatch p with - | request_then ?e ?f => - inversion run; ssubst; - clear run; - lazymatch goal with - | next : exists _, post (interface_to_hoare c _ e) _ _ _ /\ _ |- _ => - let ω'' := fresh "ω" in - let o_callee := fresh "o_callee" in - let run := fresh "run" in - destruct next as [ω'' [o_callee run]]; - unroll_post run - | _ => idtac - end - - | local ?x => - inversion run; ssubst; - clear run - - | bind ?p ?f => - apply (bindA c p f) in run; - let run1 := fresh "run" in - let run2 := fresh "run" in - let x := fresh "x" in - let ω := fresh "ω" in - destruct run as [x [ω [run1 run2]]]; - unroll_post run1; unroll_post run2 - - | ?a => idtac - end - - | ?a => idtac - end. - - Ltac cleanvert hyp := inversion hyp; ssubst; move:hyp=>_. - -Ltac easy_simpl hyp := idtac "--simpl"; do ? [cbn -[ - to_hoare - gen_caller_obligation - gen_callee_obligation - gen_witness_update -] in *; simplify_gens; do ? destruct_if_when_in hyp]. - -Ltac run_simpl run := - idtac "run_simpl: " run; - easy_simpl run ; - match type of run with -| post (to_hoare ?c ?p) ?ω ?x ?ω' => - idtac "=> to_hoare" "c: " c " ; p: " p; - let p := (eval hnf in p) in - idtac "=> hnf of p: " p; - match p with - | request_then ?e ?f => - idtac "=> => impure!"; - cleanvert run; - idtac "=> => inverted"; - match goal with - | next : exists _, post (interface_to_hoare c (A:=_) e) _ _ _ /\ _ |- _ => - idtac "=> => => found next: " next; - let ω'' := fresh "ω" in - let o_callee := fresh "o_callee" in - let run := fresh "run" in - case: next =>ω'' [o_callee run]; - idtac "=> => => destructed as : [" ω'' "[" o_callee ", " run"]]"; - run_simpl run; - idtac "<== <== after run" - | _ => idtac "<== branched out exists match" - end - | local ?x => idtac "=> => PURE!"; cleanvert run - | _ => idtac "<== freer out" - end -| post (lifter (i:=?ifce) (M:=?m) (interface_to_hoare ?c) (A:=_) (bind ?f ?g)) _ _ _ => - idtac "=> lifter bind"; - let run1 := fresh "lrun" in - let run2 := fresh "rrun" in - let ω := fresh "ω" in - let x := fresh "x" in - idtac "=> var names : " run1 run2 ω x; - move: run => /(to_hoare_post_bind_assoc c f g); - idtac "=> thpba applied"; - move => [x [ω [run1 run2]]]; - idtac "=> destructed run"; - idtac "=>> run first:"; - run_simpl run1; - idtac "<<= finished first"; - idtac "=>> run second:"; - run_simpl run2; - idtac "<<= finished second" - (* idtac *) - (* destruct run as [x [ω [run1 run2]]]; *) - (* run_simpl run1; run_simpl run2 *) -| ?a => idtac "not post" -end. \ No newline at end of file diff --git a/theories/Typeclasses.v b/theories/Typeclasses.v index a541bfa..499617a 100644 --- a/theories/Typeclasses.v +++ b/theories/Typeclasses.v @@ -1,117 +1,117 @@ -From FreerDPS Require Import Interface. +From FreerDPS Require Import Init Effect. -Class Provide1 ix i1 `{Provide ix i1}. +Class Provide1 Fx F1 `{Provide Fx F1}. #[global] Hint Resolve Build_Provide1 : typeclass_instances. -Class Provide2 ix i1 i2 `{Provide ix i1, Provide ix i2}. +Class Provide2 Fx F1 F2 `{Provide Fx F1, Provide Fx F2}. #[global] Hint Resolve Build_Provide2 : typeclass_instances. -Class Provide3 ix i1 i2 i3 `{Provide ix i1, Provide ix i2, Provide ix i3}. +Class Provide3 Fx F1 F2 F3 `{Provide Fx F1, Provide Fx F2, Provide Fx F3}. #[global] Hint Resolve Build_Provide3 : typeclass_instances. -Class Provide4 ix i1 i2 i3 i4 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4}. +Class Provide4 Fx F1 F2 F3 F4 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4}. #[global] Hint Resolve Build_Provide4 : typeclass_instances. -Class Provide5 ix i1 i2 i3 i4 i5 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5}. +Class Provide5 Fx F1 F2 F3 F4 F5 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5}. #[global] Hint Resolve Build_Provide5 : typeclass_instances. -Class Provide6 ix i1 i2 i3 i4 i5 i6 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6}. +Class Provide6 Fx F1 F2 F3 F4 F5 F6 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6}. #[global] Hint Resolve Build_Provide6 : typeclass_instances. -Class Provide7 ix i1 i2 i3 i4 i5 i6 i7 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7}. +Class Provide7 Fx F1 F2 F3 F4 F5 F6 F7 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7}. #[global] Hint Resolve Build_Provide7 : typeclass_instances. -Class Provide8 ix i1 i2 i3 i4 i5 i6 i7 i8 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8}. +Class Provide8 Fx F1 F2 F3 F4 F5 F6 F7 F8 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8}. #[global] Hint Resolve Build_Provide8 : typeclass_instances. -Class Provide9 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9}. +Class Provide9 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9}. #[global] Hint Resolve Build_Provide9 : typeclass_instances. -Class Provide10 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10}. +Class Provide10 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10}. #[global] Hint Resolve Build_Provide10 : typeclass_instances. -Class Provide11 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11}. +Class Provide11 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11}. #[global] Hint Resolve Build_Provide11 : typeclass_instances. -Class Provide12 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12}. +Class Provide12 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, Provide Fx F12}. #[global] Hint Resolve Build_Provide12 : typeclass_instances. -Class Provide13 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13}. +Class Provide13 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 F13 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, Provide Fx F12, Provide Fx F13}. #[global] Hint Resolve Build_Provide13 : typeclass_instances. -Class Provide14 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, Provide ix i14}. +Class Provide14 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 F13 F14 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, Provide Fx F12, Provide Fx F13, Provide Fx F14}. #[global] Hint Resolve Build_Provide14 : typeclass_instances. -Class Provide15 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 i15 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, Provide ix i14, Provide ix i15}. +Class Provide15 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 F13 F14 F15 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, Provide Fx F12, Provide Fx F13, Provide Fx F14, Provide Fx F15}. #[global] Hint Resolve Build_Provide15 : typeclass_instances. -Class StrictProvide2 ix i1 i2 `{Provide ix i1, Provide ix i2, ! Distinguish ix i1 i2, ! Distinguish ix i2 i1}. +Class StrictProvide2 Fx F1 F2 `{Provide Fx F1, Provide Fx F2, ! Distinguish Fx F1 F2, ! Distinguish Fx F2 F1}. #[global] Hint Resolve Build_StrictProvide2 : typeclass_instances. -Class StrictProvide3 ix i1 i2 i3 `{Provide ix i1, Provide ix i2, Provide ix i3, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2}. +Class StrictProvide3 Fx F1 F2 F3 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2}. #[global] Hint Resolve Build_StrictProvide3 : typeclass_instances. -Class StrictProvide4 ix i1 i2 i3 i4 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3}. +Class StrictProvide4 Fx F1 F2 F3 F4 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3}. #[global] Hint Resolve Build_StrictProvide4 : typeclass_instances. -Class StrictProvide5 ix i1 i2 i3 i4 i5 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4}. +Class StrictProvide5 Fx F1 F2 F3 F4 F5 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4}. #[global] Hint Resolve Build_StrictProvide5 : typeclass_instances. -Class StrictProvide6 ix i1 i2 i3 i4 i5 i6 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5}. +Class StrictProvide6 Fx F1 F2 F3 F4 F5 F6 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5}. #[global] Hint Resolve Build_StrictProvide6 : typeclass_instances. -Class StrictProvide7 ix i1 i2 i3 i4 i5 i6 i7 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6}. +Class StrictProvide7 Fx F1 F2 F3 F4 F5 F6 F7 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6}. #[global] Hint Resolve Build_StrictProvide7 : typeclass_instances. -Class StrictProvide8 ix i1 i2 i3 i4 i5 i6 i7 i8 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7}. +Class StrictProvide8 Fx F1 F2 F3 F4 F5 F6 F7 F8 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F1 F8, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F2 F8, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F3 F8, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F4 F8, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F5 F8, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F6 F8, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6, ! Distinguish Fx F7 F8, ! Distinguish Fx F8 F1, ! Distinguish Fx F8 F2, ! Distinguish Fx F8 F3, ! Distinguish Fx F8 F4, ! Distinguish Fx F8 F5, ! Distinguish Fx F8 F6, ! Distinguish Fx F8 F7}. #[global] Hint Resolve Build_StrictProvide8 : typeclass_instances. -Class StrictProvide9 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8}. +Class StrictProvide9 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F1 F8, ! Distinguish Fx F1 F9, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F2 F8, ! Distinguish Fx F2 F9, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F3 F8, ! Distinguish Fx F3 F9, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F4 F8, ! Distinguish Fx F4 F9, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F5 F8, ! Distinguish Fx F5 F9, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F6 F8, ! Distinguish Fx F6 F9, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6, ! Distinguish Fx F7 F8, ! Distinguish Fx F7 F9, ! Distinguish Fx F8 F1, ! Distinguish Fx F8 F2, ! Distinguish Fx F8 F3, ! Distinguish Fx F8 F4, ! Distinguish Fx F8 F5, ! Distinguish Fx F8 F6, ! Distinguish Fx F8 F7, ! Distinguish Fx F8 F9, ! Distinguish Fx F9 F1, ! Distinguish Fx F9 F2, ! Distinguish Fx F9 F3, ! Distinguish Fx F9 F4, ! Distinguish Fx F9 F5, ! Distinguish Fx F9 F6, ! Distinguish Fx F9 F7, ! Distinguish Fx F9 F8}. #[global] Hint Resolve Build_StrictProvide9 : typeclass_instances. -Class StrictProvide10 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9}. +Class StrictProvide10 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F1 F8, ! Distinguish Fx F1 F9, ! Distinguish Fx F1 F10, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F2 F8, ! Distinguish Fx F2 F9, ! Distinguish Fx F2 F10, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F3 F8, ! Distinguish Fx F3 F9, ! Distinguish Fx F3 F10, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F4 F8, ! Distinguish Fx F4 F9, ! Distinguish Fx F4 F10, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F5 F8, ! Distinguish Fx F5 F9, ! Distinguish Fx F5 F10, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F6 F8, ! Distinguish Fx F6 F9, ! Distinguish Fx F6 F10, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6, ! Distinguish Fx F7 F8, ! Distinguish Fx F7 F9, ! Distinguish Fx F7 F10, ! Distinguish Fx F8 F1, ! Distinguish Fx F8 F2, ! Distinguish Fx F8 F3, ! Distinguish Fx F8 F4, ! Distinguish Fx F8 F5, ! Distinguish Fx F8 F6, ! Distinguish Fx F8 F7, ! Distinguish Fx F8 F9, ! Distinguish Fx F8 F10, ! Distinguish Fx F9 F1, ! Distinguish Fx F9 F2, ! Distinguish Fx F9 F3, ! Distinguish Fx F9 F4, ! Distinguish Fx F9 F5, ! Distinguish Fx F9 F6, ! Distinguish Fx F9 F7, ! Distinguish Fx F9 F8, ! Distinguish Fx F9 F10, ! Distinguish Fx F10 F1, ! Distinguish Fx F10 F2, ! Distinguish Fx F10 F3, ! Distinguish Fx F10 F4, ! Distinguish Fx F10 F5, ! Distinguish Fx F10 F6, ! Distinguish Fx F10 F7, ! Distinguish Fx F10 F8, ! Distinguish Fx F10 F9}. #[global] Hint Resolve Build_StrictProvide10 : typeclass_instances. -Class StrictProvide11 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10}. +Class StrictProvide11 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F1 F8, ! Distinguish Fx F1 F9, ! Distinguish Fx F1 F10, ! Distinguish Fx F1 F11, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F2 F8, ! Distinguish Fx F2 F9, ! Distinguish Fx F2 F10, ! Distinguish Fx F2 F11, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F3 F8, ! Distinguish Fx F3 F9, ! Distinguish Fx F3 F10, ! Distinguish Fx F3 F11, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F4 F8, ! Distinguish Fx F4 F9, ! Distinguish Fx F4 F10, ! Distinguish Fx F4 F11, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F5 F8, ! Distinguish Fx F5 F9, ! Distinguish Fx F5 F10, ! Distinguish Fx F5 F11, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F6 F8, ! Distinguish Fx F6 F9, ! Distinguish Fx F6 F10, ! Distinguish Fx F6 F11, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6, ! Distinguish Fx F7 F8, ! Distinguish Fx F7 F9, ! Distinguish Fx F7 F10, ! Distinguish Fx F7 F11, ! Distinguish Fx F8 F1, ! Distinguish Fx F8 F2, ! Distinguish Fx F8 F3, ! Distinguish Fx F8 F4, ! Distinguish Fx F8 F5, ! Distinguish Fx F8 F6, ! Distinguish Fx F8 F7, ! Distinguish Fx F8 F9, ! Distinguish Fx F8 F10, ! Distinguish Fx F8 F11, ! Distinguish Fx F9 F1, ! Distinguish Fx F9 F2, ! Distinguish Fx F9 F3, ! Distinguish Fx F9 F4, ! Distinguish Fx F9 F5, ! Distinguish Fx F9 F6, ! Distinguish Fx F9 F7, ! Distinguish Fx F9 F8, ! Distinguish Fx F9 F10, ! Distinguish Fx F9 F11, ! Distinguish Fx F10 F1, ! Distinguish Fx F10 F2, ! Distinguish Fx F10 F3, ! Distinguish Fx F10 F4, ! Distinguish Fx F10 F5, ! Distinguish Fx F10 F6, ! Distinguish Fx F10 F7, ! Distinguish Fx F10 F8, ! Distinguish Fx F10 F9, ! Distinguish Fx F10 F11, ! Distinguish Fx F11 F1, ! Distinguish Fx F11 F2, ! Distinguish Fx F11 F3, ! Distinguish Fx F11 F4, ! Distinguish Fx F11 F5, ! Distinguish Fx F11 F6, ! Distinguish Fx F11 F7, ! Distinguish Fx F11 F8, ! Distinguish Fx F11 F9, ! Distinguish Fx F11 F10}. #[global] Hint Resolve Build_StrictProvide11 : typeclass_instances. -Class StrictProvide12 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i1 i12, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i2 i12, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i3 i12, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i4 i12, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i5 i12, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i6 i12, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i7 i12, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i8 i12, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i9 i12, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i10 i12, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10, ! Distinguish ix i11 i12, ! Distinguish ix i12 i1, ! Distinguish ix i12 i2, ! Distinguish ix i12 i3, ! Distinguish ix i12 i4, ! Distinguish ix i12 i5, ! Distinguish ix i12 i6, ! Distinguish ix i12 i7, ! Distinguish ix i12 i8, ! Distinguish ix i12 i9, ! Distinguish ix i12 i10, ! Distinguish ix i12 i11}. +Class StrictProvide12 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, Provide Fx F12, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F1 F8, ! Distinguish Fx F1 F9, ! Distinguish Fx F1 F10, ! Distinguish Fx F1 F11, ! Distinguish Fx F1 F12, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F2 F8, ! Distinguish Fx F2 F9, ! Distinguish Fx F2 F10, ! Distinguish Fx F2 F11, ! Distinguish Fx F2 F12, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F3 F8, ! Distinguish Fx F3 F9, ! Distinguish Fx F3 F10, ! Distinguish Fx F3 F11, ! Distinguish Fx F3 F12, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F4 F8, ! Distinguish Fx F4 F9, ! Distinguish Fx F4 F10, ! Distinguish Fx F4 F11, ! Distinguish Fx F4 F12, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F5 F8, ! Distinguish Fx F5 F9, ! Distinguish Fx F5 F10, ! Distinguish Fx F5 F11, ! Distinguish Fx F5 F12, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F6 F8, ! Distinguish Fx F6 F9, ! Distinguish Fx F6 F10, ! Distinguish Fx F6 F11, ! Distinguish Fx F6 F12, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6, ! Distinguish Fx F7 F8, ! Distinguish Fx F7 F9, ! Distinguish Fx F7 F10, ! Distinguish Fx F7 F11, ! Distinguish Fx F7 F12, ! Distinguish Fx F8 F1, ! Distinguish Fx F8 F2, ! Distinguish Fx F8 F3, ! Distinguish Fx F8 F4, ! Distinguish Fx F8 F5, ! Distinguish Fx F8 F6, ! Distinguish Fx F8 F7, ! Distinguish Fx F8 F9, ! Distinguish Fx F8 F10, ! Distinguish Fx F8 F11, ! Distinguish Fx F8 F12, ! Distinguish Fx F9 F1, ! Distinguish Fx F9 F2, ! Distinguish Fx F9 F3, ! Distinguish Fx F9 F4, ! Distinguish Fx F9 F5, ! Distinguish Fx F9 F6, ! Distinguish Fx F9 F7, ! Distinguish Fx F9 F8, ! Distinguish Fx F9 F10, ! Distinguish Fx F9 F11, ! Distinguish Fx F9 F12, ! Distinguish Fx F10 F1, ! Distinguish Fx F10 F2, ! Distinguish Fx F10 F3, ! Distinguish Fx F10 F4, ! Distinguish Fx F10 F5, ! Distinguish Fx F10 F6, ! Distinguish Fx F10 F7, ! Distinguish Fx F10 F8, ! Distinguish Fx F10 F9, ! Distinguish Fx F10 F11, ! Distinguish Fx F10 F12, ! Distinguish Fx F11 F1, ! Distinguish Fx F11 F2, ! Distinguish Fx F11 F3, ! Distinguish Fx F11 F4, ! Distinguish Fx F11 F5, ! Distinguish Fx F11 F6, ! Distinguish Fx F11 F7, ! Distinguish Fx F11 F8, ! Distinguish Fx F11 F9, ! Distinguish Fx F11 F10, ! Distinguish Fx F11 F12, ! Distinguish Fx F12 F1, ! Distinguish Fx F12 F2, ! Distinguish Fx F12 F3, ! Distinguish Fx F12 F4, ! Distinguish Fx F12 F5, ! Distinguish Fx F12 F6, ! Distinguish Fx F12 F7, ! Distinguish Fx F12 F8, ! Distinguish Fx F12 F9, ! Distinguish Fx F12 F10, ! Distinguish Fx F12 F11}. #[global] Hint Resolve Build_StrictProvide12 : typeclass_instances. -Class StrictProvide13 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i1 i12, ! Distinguish ix i1 i13, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i2 i12, ! Distinguish ix i2 i13, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i3 i12, ! Distinguish ix i3 i13, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i4 i12, ! Distinguish ix i4 i13, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i5 i12, ! Distinguish ix i5 i13, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i6 i12, ! Distinguish ix i6 i13, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i7 i12, ! Distinguish ix i7 i13, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i8 i12, ! Distinguish ix i8 i13, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i9 i12, ! Distinguish ix i9 i13, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i10 i12, ! Distinguish ix i10 i13, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10, ! Distinguish ix i11 i12, ! Distinguish ix i11 i13, ! Distinguish ix i12 i1, ! Distinguish ix i12 i2, ! Distinguish ix i12 i3, ! Distinguish ix i12 i4, ! Distinguish ix i12 i5, ! Distinguish ix i12 i6, ! Distinguish ix i12 i7, ! Distinguish ix i12 i8, ! Distinguish ix i12 i9, ! Distinguish ix i12 i10, ! Distinguish ix i12 i11, ! Distinguish ix i12 i13, ! Distinguish ix i13 i1, ! Distinguish ix i13 i2, ! Distinguish ix i13 i3, ! Distinguish ix i13 i4, ! Distinguish ix i13 i5, ! Distinguish ix i13 i6, ! Distinguish ix i13 i7, ! Distinguish ix i13 i8, ! Distinguish ix i13 i9, ! Distinguish ix i13 i10, ! Distinguish ix i13 i11, ! Distinguish ix i13 i12}. +Class StrictProvide13 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 F13 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, Provide Fx F12, Provide Fx F13, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F1 F8, ! Distinguish Fx F1 F9, ! Distinguish Fx F1 F10, ! Distinguish Fx F1 F11, ! Distinguish Fx F1 F12, ! Distinguish Fx F1 F13, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F2 F8, ! Distinguish Fx F2 F9, ! Distinguish Fx F2 F10, ! Distinguish Fx F2 F11, ! Distinguish Fx F2 F12, ! Distinguish Fx F2 F13, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F3 F8, ! Distinguish Fx F3 F9, ! Distinguish Fx F3 F10, ! Distinguish Fx F3 F11, ! Distinguish Fx F3 F12, ! Distinguish Fx F3 F13, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F4 F8, ! Distinguish Fx F4 F9, ! Distinguish Fx F4 F10, ! Distinguish Fx F4 F11, ! Distinguish Fx F4 F12, ! Distinguish Fx F4 F13, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F5 F8, ! Distinguish Fx F5 F9, ! Distinguish Fx F5 F10, ! Distinguish Fx F5 F11, ! Distinguish Fx F5 F12, ! Distinguish Fx F5 F13, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F6 F8, ! Distinguish Fx F6 F9, ! Distinguish Fx F6 F10, ! Distinguish Fx F6 F11, ! Distinguish Fx F6 F12, ! Distinguish Fx F6 F13, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6, ! Distinguish Fx F7 F8, ! Distinguish Fx F7 F9, ! Distinguish Fx F7 F10, ! Distinguish Fx F7 F11, ! Distinguish Fx F7 F12, ! Distinguish Fx F7 F13, ! Distinguish Fx F8 F1, ! Distinguish Fx F8 F2, ! Distinguish Fx F8 F3, ! Distinguish Fx F8 F4, ! Distinguish Fx F8 F5, ! Distinguish Fx F8 F6, ! Distinguish Fx F8 F7, ! Distinguish Fx F8 F9, ! Distinguish Fx F8 F10, ! Distinguish Fx F8 F11, ! Distinguish Fx F8 F12, ! Distinguish Fx F8 F13, ! Distinguish Fx F9 F1, ! Distinguish Fx F9 F2, ! Distinguish Fx F9 F3, ! Distinguish Fx F9 F4, ! Distinguish Fx F9 F5, ! Distinguish Fx F9 F6, ! Distinguish Fx F9 F7, ! Distinguish Fx F9 F8, ! Distinguish Fx F9 F10, ! Distinguish Fx F9 F11, ! Distinguish Fx F9 F12, ! Distinguish Fx F9 F13, ! Distinguish Fx F10 F1, ! Distinguish Fx F10 F2, ! Distinguish Fx F10 F3, ! Distinguish Fx F10 F4, ! Distinguish Fx F10 F5, ! Distinguish Fx F10 F6, ! Distinguish Fx F10 F7, ! Distinguish Fx F10 F8, ! Distinguish Fx F10 F9, ! Distinguish Fx F10 F11, ! Distinguish Fx F10 F12, ! Distinguish Fx F10 F13, ! Distinguish Fx F11 F1, ! Distinguish Fx F11 F2, ! Distinguish Fx F11 F3, ! Distinguish Fx F11 F4, ! Distinguish Fx F11 F5, ! Distinguish Fx F11 F6, ! Distinguish Fx F11 F7, ! Distinguish Fx F11 F8, ! Distinguish Fx F11 F9, ! Distinguish Fx F11 F10, ! Distinguish Fx F11 F12, ! Distinguish Fx F11 F13, ! Distinguish Fx F12 F1, ! Distinguish Fx F12 F2, ! Distinguish Fx F12 F3, ! Distinguish Fx F12 F4, ! Distinguish Fx F12 F5, ! Distinguish Fx F12 F6, ! Distinguish Fx F12 F7, ! Distinguish Fx F12 F8, ! Distinguish Fx F12 F9, ! Distinguish Fx F12 F10, ! Distinguish Fx F12 F11, ! Distinguish Fx F12 F13, ! Distinguish Fx F13 F1, ! Distinguish Fx F13 F2, ! Distinguish Fx F13 F3, ! Distinguish Fx F13 F4, ! Distinguish Fx F13 F5, ! Distinguish Fx F13 F6, ! Distinguish Fx F13 F7, ! Distinguish Fx F13 F8, ! Distinguish Fx F13 F9, ! Distinguish Fx F13 F10, ! Distinguish Fx F13 F11, ! Distinguish Fx F13 F12}. #[global] Hint Resolve Build_StrictProvide13 : typeclass_instances. -Class StrictProvide14 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, Provide ix i14, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i1 i12, ! Distinguish ix i1 i13, ! Distinguish ix i1 i14, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i2 i12, ! Distinguish ix i2 i13, ! Distinguish ix i2 i14, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i3 i12, ! Distinguish ix i3 i13, ! Distinguish ix i3 i14, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i4 i12, ! Distinguish ix i4 i13, ! Distinguish ix i4 i14, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i5 i12, ! Distinguish ix i5 i13, ! Distinguish ix i5 i14, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i6 i12, ! Distinguish ix i6 i13, ! Distinguish ix i6 i14, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i7 i12, ! Distinguish ix i7 i13, ! Distinguish ix i7 i14, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i8 i12, ! Distinguish ix i8 i13, ! Distinguish ix i8 i14, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i9 i12, ! Distinguish ix i9 i13, ! Distinguish ix i9 i14, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i10 i12, ! Distinguish ix i10 i13, ! Distinguish ix i10 i14, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10, ! Distinguish ix i11 i12, ! Distinguish ix i11 i13, ! Distinguish ix i11 i14, ! Distinguish ix i12 i1, ! Distinguish ix i12 i2, ! Distinguish ix i12 i3, ! Distinguish ix i12 i4, ! Distinguish ix i12 i5, ! Distinguish ix i12 i6, ! Distinguish ix i12 i7, ! Distinguish ix i12 i8, ! Distinguish ix i12 i9, ! Distinguish ix i12 i10, ! Distinguish ix i12 i11, ! Distinguish ix i12 i13, ! Distinguish ix i12 i14, ! Distinguish ix i13 i1, ! Distinguish ix i13 i2, ! Distinguish ix i13 i3, ! Distinguish ix i13 i4, ! Distinguish ix i13 i5, ! Distinguish ix i13 i6, ! Distinguish ix i13 i7, ! Distinguish ix i13 i8, ! Distinguish ix i13 i9, ! Distinguish ix i13 i10, ! Distinguish ix i13 i11, ! Distinguish ix i13 i12, ! Distinguish ix i13 i14, ! Distinguish ix i14 i1, ! Distinguish ix i14 i2, ! Distinguish ix i14 i3, ! Distinguish ix i14 i4, ! Distinguish ix i14 i5, ! Distinguish ix i14 i6, ! Distinguish ix i14 i7, ! Distinguish ix i14 i8, ! Distinguish ix i14 i9, ! Distinguish ix i14 i10, ! Distinguish ix i14 i11, ! Distinguish ix i14 i12, ! Distinguish ix i14 i13}. +Class StrictProvide14 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 F13 F14 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, Provide Fx F12, Provide Fx F13, Provide Fx F14, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F1 F8, ! Distinguish Fx F1 F9, ! Distinguish Fx F1 F10, ! Distinguish Fx F1 F11, ! Distinguish Fx F1 F12, ! Distinguish Fx F1 F13, ! Distinguish Fx F1 F14, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F2 F8, ! Distinguish Fx F2 F9, ! Distinguish Fx F2 F10, ! Distinguish Fx F2 F11, ! Distinguish Fx F2 F12, ! Distinguish Fx F2 F13, ! Distinguish Fx F2 F14, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F3 F8, ! Distinguish Fx F3 F9, ! Distinguish Fx F3 F10, ! Distinguish Fx F3 F11, ! Distinguish Fx F3 F12, ! Distinguish Fx F3 F13, ! Distinguish Fx F3 F14, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F4 F8, ! Distinguish Fx F4 F9, ! Distinguish Fx F4 F10, ! Distinguish Fx F4 F11, ! Distinguish Fx F4 F12, ! Distinguish Fx F4 F13, ! Distinguish Fx F4 F14, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F5 F8, ! Distinguish Fx F5 F9, ! Distinguish Fx F5 F10, ! Distinguish Fx F5 F11, ! Distinguish Fx F5 F12, ! Distinguish Fx F5 F13, ! Distinguish Fx F5 F14, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F6 F8, ! Distinguish Fx F6 F9, ! Distinguish Fx F6 F10, ! Distinguish Fx F6 F11, ! Distinguish Fx F6 F12, ! Distinguish Fx F6 F13, ! Distinguish Fx F6 F14, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6, ! Distinguish Fx F7 F8, ! Distinguish Fx F7 F9, ! Distinguish Fx F7 F10, ! Distinguish Fx F7 F11, ! Distinguish Fx F7 F12, ! Distinguish Fx F7 F13, ! Distinguish Fx F7 F14, ! Distinguish Fx F8 F1, ! Distinguish Fx F8 F2, ! Distinguish Fx F8 F3, ! Distinguish Fx F8 F4, ! Distinguish Fx F8 F5, ! Distinguish Fx F8 F6, ! Distinguish Fx F8 F7, ! Distinguish Fx F8 F9, ! Distinguish Fx F8 F10, ! Distinguish Fx F8 F11, ! Distinguish Fx F8 F12, ! Distinguish Fx F8 F13, ! Distinguish Fx F8 F14, ! Distinguish Fx F9 F1, ! Distinguish Fx F9 F2, ! Distinguish Fx F9 F3, ! Distinguish Fx F9 F4, ! Distinguish Fx F9 F5, ! Distinguish Fx F9 F6, ! Distinguish Fx F9 F7, ! Distinguish Fx F9 F8, ! Distinguish Fx F9 F10, ! Distinguish Fx F9 F11, ! Distinguish Fx F9 F12, ! Distinguish Fx F9 F13, ! Distinguish Fx F9 F14, ! Distinguish Fx F10 F1, ! Distinguish Fx F10 F2, ! Distinguish Fx F10 F3, ! Distinguish Fx F10 F4, ! Distinguish Fx F10 F5, ! Distinguish Fx F10 F6, ! Distinguish Fx F10 F7, ! Distinguish Fx F10 F8, ! Distinguish Fx F10 F9, ! Distinguish Fx F10 F11, ! Distinguish Fx F10 F12, ! Distinguish Fx F10 F13, ! Distinguish Fx F10 F14, ! Distinguish Fx F11 F1, ! Distinguish Fx F11 F2, ! Distinguish Fx F11 F3, ! Distinguish Fx F11 F4, ! Distinguish Fx F11 F5, ! Distinguish Fx F11 F6, ! Distinguish Fx F11 F7, ! Distinguish Fx F11 F8, ! Distinguish Fx F11 F9, ! Distinguish Fx F11 F10, ! Distinguish Fx F11 F12, ! Distinguish Fx F11 F13, ! Distinguish Fx F11 F14, ! Distinguish Fx F12 F1, ! Distinguish Fx F12 F2, ! Distinguish Fx F12 F3, ! Distinguish Fx F12 F4, ! Distinguish Fx F12 F5, ! Distinguish Fx F12 F6, ! Distinguish Fx F12 F7, ! Distinguish Fx F12 F8, ! Distinguish Fx F12 F9, ! Distinguish Fx F12 F10, ! Distinguish Fx F12 F11, ! Distinguish Fx F12 F13, ! Distinguish Fx F12 F14, ! Distinguish Fx F13 F1, ! Distinguish Fx F13 F2, ! Distinguish Fx F13 F3, ! Distinguish Fx F13 F4, ! Distinguish Fx F13 F5, ! Distinguish Fx F13 F6, ! Distinguish Fx F13 F7, ! Distinguish Fx F13 F8, ! Distinguish Fx F13 F9, ! Distinguish Fx F13 F10, ! Distinguish Fx F13 F11, ! Distinguish Fx F13 F12, ! Distinguish Fx F13 F14, ! Distinguish Fx F14 F1, ! Distinguish Fx F14 F2, ! Distinguish Fx F14 F3, ! Distinguish Fx F14 F4, ! Distinguish Fx F14 F5, ! Distinguish Fx F14 F6, ! Distinguish Fx F14 F7, ! Distinguish Fx F14 F8, ! Distinguish Fx F14 F9, ! Distinguish Fx F14 F10, ! Distinguish Fx F14 F11, ! Distinguish Fx F14 F12, ! Distinguish Fx F14 F13}. #[global] Hint Resolve Build_StrictProvide14 : typeclass_instances. -Class StrictProvide15 ix i1 i2 i3 i4 i5 i6 i7 i8 i9 i10 i11 i12 i13 i14 i15 `{Provide ix i1, Provide ix i2, Provide ix i3, Provide ix i4, Provide ix i5, Provide ix i6, Provide ix i7, Provide ix i8, Provide ix i9, Provide ix i10, Provide ix i11, Provide ix i12, Provide ix i13, Provide ix i14, Provide ix i15, ! Distinguish ix i1 i2, ! Distinguish ix i1 i3, ! Distinguish ix i1 i4, ! Distinguish ix i1 i5, ! Distinguish ix i1 i6, ! Distinguish ix i1 i7, ! Distinguish ix i1 i8, ! Distinguish ix i1 i9, ! Distinguish ix i1 i10, ! Distinguish ix i1 i11, ! Distinguish ix i1 i12, ! Distinguish ix i1 i13, ! Distinguish ix i1 i14, ! Distinguish ix i1 i15, ! Distinguish ix i2 i1, ! Distinguish ix i2 i3, ! Distinguish ix i2 i4, ! Distinguish ix i2 i5, ! Distinguish ix i2 i6, ! Distinguish ix i2 i7, ! Distinguish ix i2 i8, ! Distinguish ix i2 i9, ! Distinguish ix i2 i10, ! Distinguish ix i2 i11, ! Distinguish ix i2 i12, ! Distinguish ix i2 i13, ! Distinguish ix i2 i14, ! Distinguish ix i2 i15, ! Distinguish ix i3 i1, ! Distinguish ix i3 i2, ! Distinguish ix i3 i4, ! Distinguish ix i3 i5, ! Distinguish ix i3 i6, ! Distinguish ix i3 i7, ! Distinguish ix i3 i8, ! Distinguish ix i3 i9, ! Distinguish ix i3 i10, ! Distinguish ix i3 i11, ! Distinguish ix i3 i12, ! Distinguish ix i3 i13, ! Distinguish ix i3 i14, ! Distinguish ix i3 i15, ! Distinguish ix i4 i1, ! Distinguish ix i4 i2, ! Distinguish ix i4 i3, ! Distinguish ix i4 i5, ! Distinguish ix i4 i6, ! Distinguish ix i4 i7, ! Distinguish ix i4 i8, ! Distinguish ix i4 i9, ! Distinguish ix i4 i10, ! Distinguish ix i4 i11, ! Distinguish ix i4 i12, ! Distinguish ix i4 i13, ! Distinguish ix i4 i14, ! Distinguish ix i4 i15, ! Distinguish ix i5 i1, ! Distinguish ix i5 i2, ! Distinguish ix i5 i3, ! Distinguish ix i5 i4, ! Distinguish ix i5 i6, ! Distinguish ix i5 i7, ! Distinguish ix i5 i8, ! Distinguish ix i5 i9, ! Distinguish ix i5 i10, ! Distinguish ix i5 i11, ! Distinguish ix i5 i12, ! Distinguish ix i5 i13, ! Distinguish ix i5 i14, ! Distinguish ix i5 i15, ! Distinguish ix i6 i1, ! Distinguish ix i6 i2, ! Distinguish ix i6 i3, ! Distinguish ix i6 i4, ! Distinguish ix i6 i5, ! Distinguish ix i6 i7, ! Distinguish ix i6 i8, ! Distinguish ix i6 i9, ! Distinguish ix i6 i10, ! Distinguish ix i6 i11, ! Distinguish ix i6 i12, ! Distinguish ix i6 i13, ! Distinguish ix i6 i14, ! Distinguish ix i6 i15, ! Distinguish ix i7 i1, ! Distinguish ix i7 i2, ! Distinguish ix i7 i3, ! Distinguish ix i7 i4, ! Distinguish ix i7 i5, ! Distinguish ix i7 i6, ! Distinguish ix i7 i8, ! Distinguish ix i7 i9, ! Distinguish ix i7 i10, ! Distinguish ix i7 i11, ! Distinguish ix i7 i12, ! Distinguish ix i7 i13, ! Distinguish ix i7 i14, ! Distinguish ix i7 i15, ! Distinguish ix i8 i1, ! Distinguish ix i8 i2, ! Distinguish ix i8 i3, ! Distinguish ix i8 i4, ! Distinguish ix i8 i5, ! Distinguish ix i8 i6, ! Distinguish ix i8 i7, ! Distinguish ix i8 i9, ! Distinguish ix i8 i10, ! Distinguish ix i8 i11, ! Distinguish ix i8 i12, ! Distinguish ix i8 i13, ! Distinguish ix i8 i14, ! Distinguish ix i8 i15, ! Distinguish ix i9 i1, ! Distinguish ix i9 i2, ! Distinguish ix i9 i3, ! Distinguish ix i9 i4, ! Distinguish ix i9 i5, ! Distinguish ix i9 i6, ! Distinguish ix i9 i7, ! Distinguish ix i9 i8, ! Distinguish ix i9 i10, ! Distinguish ix i9 i11, ! Distinguish ix i9 i12, ! Distinguish ix i9 i13, ! Distinguish ix i9 i14, ! Distinguish ix i9 i15, ! Distinguish ix i10 i1, ! Distinguish ix i10 i2, ! Distinguish ix i10 i3, ! Distinguish ix i10 i4, ! Distinguish ix i10 i5, ! Distinguish ix i10 i6, ! Distinguish ix i10 i7, ! Distinguish ix i10 i8, ! Distinguish ix i10 i9, ! Distinguish ix i10 i11, ! Distinguish ix i10 i12, ! Distinguish ix i10 i13, ! Distinguish ix i10 i14, ! Distinguish ix i10 i15, ! Distinguish ix i11 i1, ! Distinguish ix i11 i2, ! Distinguish ix i11 i3, ! Distinguish ix i11 i4, ! Distinguish ix i11 i5, ! Distinguish ix i11 i6, ! Distinguish ix i11 i7, ! Distinguish ix i11 i8, ! Distinguish ix i11 i9, ! Distinguish ix i11 i10, ! Distinguish ix i11 i12, ! Distinguish ix i11 i13, ! Distinguish ix i11 i14, ! Distinguish ix i11 i15, ! Distinguish ix i12 i1, ! Distinguish ix i12 i2, ! Distinguish ix i12 i3, ! Distinguish ix i12 i4, ! Distinguish ix i12 i5, ! Distinguish ix i12 i6, ! Distinguish ix i12 i7, ! Distinguish ix i12 i8, ! Distinguish ix i12 i9, ! Distinguish ix i12 i10, ! Distinguish ix i12 i11, ! Distinguish ix i12 i13, ! Distinguish ix i12 i14, ! Distinguish ix i12 i15, ! Distinguish ix i13 i1, ! Distinguish ix i13 i2, ! Distinguish ix i13 i3, ! Distinguish ix i13 i4, ! Distinguish ix i13 i5, ! Distinguish ix i13 i6, ! Distinguish ix i13 i7, ! Distinguish ix i13 i8, ! Distinguish ix i13 i9, ! Distinguish ix i13 i10, ! Distinguish ix i13 i11, ! Distinguish ix i13 i12, ! Distinguish ix i13 i14, ! Distinguish ix i13 i15, ! Distinguish ix i14 i1, ! Distinguish ix i14 i2, ! Distinguish ix i14 i3, ! Distinguish ix i14 i4, ! Distinguish ix i14 i5, ! Distinguish ix i14 i6, ! Distinguish ix i14 i7, ! Distinguish ix i14 i8, ! Distinguish ix i14 i9, ! Distinguish ix i14 i10, ! Distinguish ix i14 i11, ! Distinguish ix i14 i12, ! Distinguish ix i14 i13, ! Distinguish ix i14 i15, ! Distinguish ix i15 i1, ! Distinguish ix i15 i2, ! Distinguish ix i15 i3, ! Distinguish ix i15 i4, ! Distinguish ix i15 i5, ! Distinguish ix i15 i6, ! Distinguish ix i15 i7, ! Distinguish ix i15 i8, ! Distinguish ix i15 i9, ! Distinguish ix i15 i10, ! Distinguish ix i15 i11, ! Distinguish ix i15 i12, ! Distinguish ix i15 i13, ! Distinguish ix i15 i14}. +Class StrictProvide15 Fx F1 F2 F3 F4 F5 F6 F7 F8 F9 F10 F11 F12 F13 F14 F15 `{Provide Fx F1, Provide Fx F2, Provide Fx F3, Provide Fx F4, Provide Fx F5, Provide Fx F6, Provide Fx F7, Provide Fx F8, Provide Fx F9, Provide Fx F10, Provide Fx F11, Provide Fx F12, Provide Fx F13, Provide Fx F14, Provide Fx F15, ! Distinguish Fx F1 F2, ! Distinguish Fx F1 F3, ! Distinguish Fx F1 F4, ! Distinguish Fx F1 F5, ! Distinguish Fx F1 F6, ! Distinguish Fx F1 F7, ! Distinguish Fx F1 F8, ! Distinguish Fx F1 F9, ! Distinguish Fx F1 F10, ! Distinguish Fx F1 F11, ! Distinguish Fx F1 F12, ! Distinguish Fx F1 F13, ! Distinguish Fx F1 F14, ! Distinguish Fx F1 F15, ! Distinguish Fx F2 F1, ! Distinguish Fx F2 F3, ! Distinguish Fx F2 F4, ! Distinguish Fx F2 F5, ! Distinguish Fx F2 F6, ! Distinguish Fx F2 F7, ! Distinguish Fx F2 F8, ! Distinguish Fx F2 F9, ! Distinguish Fx F2 F10, ! Distinguish Fx F2 F11, ! Distinguish Fx F2 F12, ! Distinguish Fx F2 F13, ! Distinguish Fx F2 F14, ! Distinguish Fx F2 F15, ! Distinguish Fx F3 F1, ! Distinguish Fx F3 F2, ! Distinguish Fx F3 F4, ! Distinguish Fx F3 F5, ! Distinguish Fx F3 F6, ! Distinguish Fx F3 F7, ! Distinguish Fx F3 F8, ! Distinguish Fx F3 F9, ! Distinguish Fx F3 F10, ! Distinguish Fx F3 F11, ! Distinguish Fx F3 F12, ! Distinguish Fx F3 F13, ! Distinguish Fx F3 F14, ! Distinguish Fx F3 F15, ! Distinguish Fx F4 F1, ! Distinguish Fx F4 F2, ! Distinguish Fx F4 F3, ! Distinguish Fx F4 F5, ! Distinguish Fx F4 F6, ! Distinguish Fx F4 F7, ! Distinguish Fx F4 F8, ! Distinguish Fx F4 F9, ! Distinguish Fx F4 F10, ! Distinguish Fx F4 F11, ! Distinguish Fx F4 F12, ! Distinguish Fx F4 F13, ! Distinguish Fx F4 F14, ! Distinguish Fx F4 F15, ! Distinguish Fx F5 F1, ! Distinguish Fx F5 F2, ! Distinguish Fx F5 F3, ! Distinguish Fx F5 F4, ! Distinguish Fx F5 F6, ! Distinguish Fx F5 F7, ! Distinguish Fx F5 F8, ! Distinguish Fx F5 F9, ! Distinguish Fx F5 F10, ! Distinguish Fx F5 F11, ! Distinguish Fx F5 F12, ! Distinguish Fx F5 F13, ! Distinguish Fx F5 F14, ! Distinguish Fx F5 F15, ! Distinguish Fx F6 F1, ! Distinguish Fx F6 F2, ! Distinguish Fx F6 F3, ! Distinguish Fx F6 F4, ! Distinguish Fx F6 F5, ! Distinguish Fx F6 F7, ! Distinguish Fx F6 F8, ! Distinguish Fx F6 F9, ! Distinguish Fx F6 F10, ! Distinguish Fx F6 F11, ! Distinguish Fx F6 F12, ! Distinguish Fx F6 F13, ! Distinguish Fx F6 F14, ! Distinguish Fx F6 F15, ! Distinguish Fx F7 F1, ! Distinguish Fx F7 F2, ! Distinguish Fx F7 F3, ! Distinguish Fx F7 F4, ! Distinguish Fx F7 F5, ! Distinguish Fx F7 F6, ! Distinguish Fx F7 F8, ! Distinguish Fx F7 F9, ! Distinguish Fx F7 F10, ! Distinguish Fx F7 F11, ! Distinguish Fx F7 F12, ! Distinguish Fx F7 F13, ! Distinguish Fx F7 F14, ! Distinguish Fx F7 F15, ! Distinguish Fx F8 F1, ! Distinguish Fx F8 F2, ! Distinguish Fx F8 F3, ! Distinguish Fx F8 F4, ! Distinguish Fx F8 F5, ! Distinguish Fx F8 F6, ! Distinguish Fx F8 F7, ! Distinguish Fx F8 F9, ! Distinguish Fx F8 F10, ! Distinguish Fx F8 F11, ! Distinguish Fx F8 F12, ! Distinguish Fx F8 F13, ! Distinguish Fx F8 F14, ! Distinguish Fx F8 F15, ! Distinguish Fx F9 F1, ! Distinguish Fx F9 F2, ! Distinguish Fx F9 F3, ! Distinguish Fx F9 F4, ! Distinguish Fx F9 F5, ! Distinguish Fx F9 F6, ! Distinguish Fx F9 F7, ! Distinguish Fx F9 F8, ! Distinguish Fx F9 F10, ! Distinguish Fx F9 F11, ! Distinguish Fx F9 F12, ! Distinguish Fx F9 F13, ! Distinguish Fx F9 F14, ! Distinguish Fx F9 F15, ! Distinguish Fx F10 F1, ! Distinguish Fx F10 F2, ! Distinguish Fx F10 F3, ! Distinguish Fx F10 F4, ! Distinguish Fx F10 F5, ! Distinguish Fx F10 F6, ! Distinguish Fx F10 F7, ! Distinguish Fx F10 F8, ! Distinguish Fx F10 F9, ! Distinguish Fx F10 F11, ! Distinguish Fx F10 F12, ! Distinguish Fx F10 F13, ! Distinguish Fx F10 F14, ! Distinguish Fx F10 F15, ! Distinguish Fx F11 F1, ! Distinguish Fx F11 F2, ! Distinguish Fx F11 F3, ! Distinguish Fx F11 F4, ! Distinguish Fx F11 F5, ! Distinguish Fx F11 F6, ! Distinguish Fx F11 F7, ! Distinguish Fx F11 F8, ! Distinguish Fx F11 F9, ! Distinguish Fx F11 F10, ! Distinguish Fx F11 F12, ! Distinguish Fx F11 F13, ! Distinguish Fx F11 F14, ! Distinguish Fx F11 F15, ! Distinguish Fx F12 F1, ! Distinguish Fx F12 F2, ! Distinguish Fx F12 F3, ! Distinguish Fx F12 F4, ! Distinguish Fx F12 F5, ! Distinguish Fx F12 F6, ! Distinguish Fx F12 F7, ! Distinguish Fx F12 F8, ! Distinguish Fx F12 F9, ! Distinguish Fx F12 F10, ! Distinguish Fx F12 F11, ! Distinguish Fx F12 F13, ! Distinguish Fx F12 F14, ! Distinguish Fx F12 F15, ! Distinguish Fx F13 F1, ! Distinguish Fx F13 F2, ! Distinguish Fx F13 F3, ! Distinguish Fx F13 F4, ! Distinguish Fx F13 F5, ! Distinguish Fx F13 F6, ! Distinguish Fx F13 F7, ! Distinguish Fx F13 F8, ! Distinguish Fx F13 F9, ! Distinguish Fx F13 F10, ! Distinguish Fx F13 F11, ! Distinguish Fx F13 F12, ! Distinguish Fx F13 F14, ! Distinguish Fx F13 F15, ! Distinguish Fx F14 F1, ! Distinguish Fx F14 F2, ! Distinguish Fx F14 F3, ! Distinguish Fx F14 F4, ! Distinguish Fx F14 F5, ! Distinguish Fx F14 F6, ! Distinguish Fx F14 F7, ! Distinguish Fx F14 F8, ! Distinguish Fx F14 F9, ! Distinguish Fx F14 F10, ! Distinguish Fx F14 F11, ! Distinguish Fx F14 F12, ! Distinguish Fx F14 F13, ! Distinguish Fx F14 F15, ! Distinguish Fx F15 F1, ! Distinguish Fx F15 F2, ! Distinguish Fx F15 F3, ! Distinguish Fx F15 F4, ! Distinguish Fx F15 F5, ! Distinguish Fx F15 F6, ! Distinguish Fx F15 F7, ! Distinguish Fx F15 F8, ! Distinguish Fx F15 F9, ! Distinguish Fx F15 F10, ! Distinguish Fx F15 F11, ! Distinguish Fx F15 F12, ! Distinguish Fx F15 F13, ! Distinguish Fx F15 F14}. -#[global] Hint Resolve Build_StrictProvide15 : typeclass_instances. \ No newline at end of file +#[global] Hint Resolve Build_StrictProvide15 : typeclass_instances. diff --git a/theories/mathcomp_extra.v b/theories/mathcomp_extra.v new file mode 100644 index 0000000..ceb0711 --- /dev/null +++ b/theories/mathcomp_extra.v @@ -0,0 +1,87 @@ +(* This Source Code Form is subject to the terms of the Mozilla Public + * License, v. 2.0. If a copy of the MPL was not distributed with this + * file, You can obtain one at https://mozilla.org/MPL/2.0/. *) + +(**md**************************************************************************) +(* # Temporary logical lemmas awaiting inclusion in MathComp *) +(* *) +(* TODO: Move to MCA *) +(* *) +(* ``` *) +(* eq4_exists == congruence under four existential quantifiers *) +(* andTP == remove `True` from the left of a conjunction *) +(* ex2C == exchange two existential quantifiers *) +(* ex3C == exchange the first and third quantifiers *) +(* ex3AC == exchange the second and third quantifiers *) +(* ex_andl == distribute an existential over a right conjunction *) +(* ex_andr == distribute an existential over a left conjunction *) +(* ex_eqr == eliminate a right equality witness *) +(* ex_eqr_sym == eliminate a symmetric right equality witness *) +(* ex2_eqr == eliminate an equality under two existentials *) +(* ex2_eqr_sym == symmetric version of `ex2_eqr` *) +(* ``` *) +(* *) +(******************************************************************************) + +From FreerDPS Require Import Init. +From mathcomp Require Import all_boot. + +Lemma eq4_exists T S R N + (U V : forall (x : T) (y : S x) (z : R x y), N x y z -> Prop) : + (forall x y z n, U x y z n = V x y z n) -> + (exists x y z n, U x y z n) = (exists x y z n, V x y z n). +Proof. by move=> UV; apply/eq3_exists => x y z; exact/eq_exists. Qed. + +Lemma andTP (P : Prop) : (True /\ P) = P. +Proof. by apply/propext; split => // -[]. Qed. + +Lemma ex2C A B (P : A -> B -> Prop) : + (exists a b, P a b) = (exists b a, P a b). +Proof. by apply/propeqP; split=> -[x [y xy]]; [exists y, x | exists y, x]. Qed. + +Lemma ex3C A B C (P : A -> B -> C -> Prop) : + (exists a b c, P a b c) = (exists c b a, P a b c). +Proof. +apply/propeqP; split=> -[x [y [z xyz]]]. + by exists z, y, x. +by exists z, y, x. +Qed. + +Lemma ex3AC A B C (P : A -> B -> C -> Prop) : + (exists a b c, P a b c) = (exists a c b, P a b c). +Proof. +apply/propeqP; split=> [[a [b [c abc]]] | [a [c [b abc]]]]. + by exists a, c, b. +by exists a, b, c. +Qed. + +Lemma ex_andl A (P : A -> Prop) (Q : Prop) : + (exists a, P a /\ Q) = ((exists a, P a) /\ Q). +Proof. +apply/propeqP; split=> [[a [Pa q]] | [[a Pa] q]]. + by split=> //; exists a. +by exists a. +Qed. + +Lemma ex_andr A (P : Prop) (Q : A -> Prop) : + (exists a, P /\ Q a) = (P /\ (exists a, Q a)). +Proof. +under eq_exists do rewrite andC. +by rewrite ex_andl andC. +Qed. + +Lemma ex_eqr A (a' : A) (P : A -> Prop) : + (exists a, P a /\ a = a') = P a'. +Proof. by apply/propeqP; split=> [[a [Pa <-//]] | Pa']; exists a'. Qed. + +Lemma ex_eqr_sym A (a' : A) (P : A -> Prop) : + (exists a, P a /\ a' = a) = P a'. +Proof. by apply/propeqP; split=> [[a [Pa ->//]] | Pa']; exists a'. Qed. + +Lemma ex2_eqr A B (a' : A) (P : A -> B -> Prop) : + (exists a b, P a b /\ a = a') = (exists b, P a' b). +Proof. by rewrite ex2C; apply: eq_exists => b; rewrite ex_eqr. Qed. + +Lemma ex2_eqr_sym A B (a' : A) (P : A -> B -> Prop) : + (exists a b, P a b /\ a' = a) = (exists b, P a' b). +Proof. by rewrite ex2C; apply: eq_exists => b; rewrite ex_eqr_sym. Qed.