From ab84edc72e91d9863f28a005e71d53583d1c2e78 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 24 Oct 2024 12:02:23 +0900 Subject: [PATCH] rebase --- theories/lang_syntax.v | 10 +++++----- theories/lang_syntax_examples.v | 15 +++++++-------- theories/lang_syntax_table_game.v | 12 ++++++------ theories/lang_syntax_toy.v | 6 +++--- theories/lang_syntax_util.v | 4 ++-- theories/prob_lang.v | 8 ++++---- theories/prob_lang_wip.v | 6 +++--- 7 files changed, 30 insertions(+), 31 deletions(-) diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v index 0f5268a19..957d7c5e8 100644 --- a/theories/lang_syntax.v +++ b/theories/lang_syntax.v @@ -1,13 +1,13 @@ Require Import String. From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import lra. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop. -Require Import signed reals ereal topology normedtype sequences esum exp. -Require Import measure lebesgue_measure numfun lebesgue_integral itv kernel ftc. -Require Import probability. -Require Import derive realfun charge prob_lang lang_syntax_util. -From mathcomp Require Import lra. +From mathcomp Require Import signed reals ereal topology normedtype sequences. +From mathcomp Require Import esum exp derive realfun measure lebesgue_measure. +From mathcomp Require Import numfun lebesgue_integral itv kernel ftc. +From mathcomp Require Import probability charge prob_lang lang_syntax_util. (**md**************************************************************************) (* # Syntax and Evaluation for a Probabilistic Programming Language *) diff --git a/theories/lang_syntax_examples.v b/theories/lang_syntax_examples.v index 62afa9581..1a9f43e33 100644 --- a/theories/lang_syntax_examples.v +++ b/theories/lang_syntax_examples.v @@ -1,14 +1,13 @@ -Require Import String. +From Coq Require Import String. From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. From mathcomp.classical Require Import mathcomp_extra boolp. -From mathcomp Require Import ring. -From mathcomp Require Import classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. -Require Import signed reals ereal topology normedtype sequences esum measure. -Require Import lebesgue_measure numfun lebesgue_integral kernel probability. -Require Import prob_lang lang_syntax_util lang_syntax. -From mathcomp Require Import lra. +From mathcomp Require Import ring lra. +From mathcomp Require Import classical_sets functions cardinality fsbigop. +From mathcomp Require Import signed reals ereal topology normedtype sequences. +From mathcomp Require Import esum measure lebesgue_measure numfun. +From mathcomp Require Import lebesgue_integral kernel probability prob_lang. +From mathcomp Require Import lang_syntax_util lang_syntax. (**md**************************************************************************) (* # Examples using the Probabilistic Programming Language of lang_syntax.v *) diff --git a/theories/lang_syntax_table_game.v b/theories/lang_syntax_table_game.v index 46fc62cef..a9d6c26dd 100644 --- a/theories/lang_syntax_table_game.v +++ b/theories/lang_syntax_table_game.v @@ -1,13 +1,13 @@ Require Import String. From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. -From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. -Require Import signed reals ereal topology normedtype sequences esum measure. -Require Import charge lebesgue_measure numfun lebesgue_integral kernel. -Require Import probability. -Require Import prob_lang lang_syntax_util lang_syntax lang_syntax_examples. From mathcomp Require Import ring lra. +From mathcomp Require Import mathcomp_extra boolp classical_sets. +From mathcomp Require Import functions cardinality fsbigop. +From mathcomp Require Import signed reals ereal topology normedtype sequences. +From mathcomp Require Import esum measure charge lebesgue_measure numfun. +From mathcomp Require Import lebesgue_integral kernel probability prob_lang. +From mathcomp Require Import lang_syntax_util lang_syntax lang_syntax_examples. (**md**************************************************************************) (* # Eddy's table game example *) diff --git a/theories/lang_syntax_toy.v b/theories/lang_syntax_toy.v index 2c2f57267..ae6463adb 100644 --- a/theories/lang_syntax_toy.v +++ b/theories/lang_syntax_toy.v @@ -1,9 +1,9 @@ -Require Import String Classical. +From Coq Require Import String Classical. From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg. From mathcomp Require Import mathcomp_extra boolp. -Require Import signed reals topology normedtype. -Require Import lang_syntax_util. +From mathcomp Require Import signed reals topology normedtype. +From mathcomp Require Import lang_syntax_util. (******************************************************************************) (* Intrinsically-typed concrete syntax for a toy language *) diff --git a/theories/lang_syntax_util.v b/theories/lang_syntax_util.v index 608d25e7e..253c1d8ff 100644 --- a/theories/lang_syntax_util.v +++ b/theories/lang_syntax_util.v @@ -1,8 +1,8 @@ -Require Import String. +From Coq Require Import String. From HB Require Import structures. Require Import Classical_Prop. (* NB: to compile with Coq 8.17 *) From mathcomp Require Import all_ssreflect. -Require Import signed. +From mathcomp Require Import signed. (******************************************************************************) (* Shared by lang_syntax_*.v files *) diff --git a/theories/prob_lang.v b/theories/prob_lang.v index fceadacfb..e009899ed 100644 --- a/theories/prob_lang.v +++ b/theories/prob_lang.v @@ -2,12 +2,12 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import rat archimedean. +From mathcomp Require Import lra. From mathcomp Require Import mathcomp_extra boolp classical_sets. From mathcomp Require Import functions cardinality fsbigop. -Require Import reals ereal signed topology normedtype sequences esum measure. -Require Import lebesgue_measure numfun lebesgue_integral exp kernel. -Require Import probability. -From mathcomp Require Import lra. +From mathcomp Require Import reals ereal signed topology normedtype sequences. +From mathcomp Require Import esum measure lebesgue_measure numfun. +From mathcomp Require Import lebesgue_integral exp kernel probability. (**md**************************************************************************) (* # Semantics of a probabilistic programming language using s-finite kernels *) diff --git a/theories/prob_lang_wip.v b/theories/prob_lang_wip.v index 8a7bedb31..f2e247835 100644 --- a/theories/prob_lang_wip.v +++ b/theories/prob_lang_wip.v @@ -3,9 +3,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import rat. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop. -Require Import signed reals ereal topology normedtype sequences esum measure. -Require Import lebesgue_measure numfun lebesgue_integral exp kernel trigo. -Require Import realfun charge prob_lang. +From mathcomp Require Import signed reals ereal topology normedtype sequences. +From mathcomp Require Import esum measure lebesgue_measure numfun exp trigo. +From mathcomp Require Import realfun lebesgue_integral kernel charge prob_lang. (******************************************************************************) (* Semantics of a probabilistic programming language using s-finite kernels *)