From 9c27186a16a73c7e6b4c30efc2933ae842351ca6 Mon Sep 17 00:00:00 2001 From: 4ever2 <3417013+4ever2@users.noreply.github.com> Date: Thu, 11 Jul 2024 12:24:18 +0200 Subject: [PATCH] Add SSProve prefix to logpaths --- _CoqProject | 6 +++--- theories/Crypt/Casts.v | 2 +- theories/Crypt/Main.v | 2 +- theories/Crypt/Package.v | 2 +- theories/Crypt/Prelude.v | 2 +- theories/Crypt/choice_type.v | 6 +++--- theories/Crypt/examples/AsymScheme.v | 4 ++-- theories/Crypt/examples/DDH.v | 4 ++-- theories/Crypt/examples/ElGamal.v | 6 +++--- theories/Crypt/examples/Executor.v | 4 ++-- theories/Crypt/examples/KEMDEM.v | 4 ++-- theories/Crypt/examples/MACCCA.v | 6 +++--- theories/Crypt/examples/OTP.v | 4 ++-- theories/Crypt/examples/OVN.v | 4 ++-- theories/Crypt/examples/PRF.v | 6 +++--- theories/Crypt/examples/PRFMAC.v | 6 +++--- theories/Crypt/examples/PRFPRG.v | 6 +++--- theories/Crypt/examples/PRPCCA.v | 6 +++--- theories/Crypt/examples/RandomOracle.v | 4 ++-- theories/Crypt/examples/Schnorr.v | 6 +++--- theories/Crypt/examples/SecretSharing.v | 6 +++--- theories/Crypt/examples/ShamirSecretSharing.v | 6 +++--- theories/Crypt/examples/SigmaProtocol.v | 4 ++-- theories/Crypt/examples/StretchPRG.v | 6 +++--- theories/Crypt/examples/SymmRatchet.v | 6 +++--- theories/Crypt/examples/interpreter_test.v | 2 +- theories/Crypt/examples/package_usage_example.v | 2 +- theories/Crypt/package/pkg_advantage.v | 8 ++++---- theories/Crypt/package/pkg_composition.v | 6 +++--- theories/Crypt/package/pkg_core_definition.v | 6 +++--- theories/Crypt/package/pkg_distr.v | 8 ++++---- theories/Crypt/package/pkg_heap.v | 8 ++++---- theories/Crypt/package/pkg_interpreter.v | 2 +- theories/Crypt/package/pkg_invariants.v | 8 ++++---- theories/Crypt/package/pkg_lookup.v | 8 ++++---- theories/Crypt/package/pkg_notation.v | 2 +- theories/Crypt/package/pkg_rhl.v | 8 ++++---- theories/Crypt/package/pkg_semantics.v | 8 ++++---- theories/Crypt/package/pkg_tactics.v | 2 +- theories/Crypt/package/pkg_user_util.v | 2 +- theories/Crypt/rhl_semantics/ChoiceAsOrd.v | 6 +++--- theories/Crypt/rhl_semantics/free_monad/FreeProbProg.v | 6 +++--- .../Crypt/rhl_semantics/free_monad/UniversalFreeMap.v | 6 +++--- .../rhl_semantics/more_categories/InitialRelativeMonad.v | 2 +- theories/Crypt/rhl_semantics/more_categories/LaxComp.v | 4 ++-- .../rhl_semantics/more_categories/LaxFunctorsAndTransf.v | 6 +++--- .../more_categories/LaxMorphismOfRelAdjunctions.v | 6 +++--- .../more_categories/OrderEnrichedRelativeAdjunctions.v | 4 ++-- .../more_categories/RelativeMonadMorph_prod.v | 2 +- .../rhl_semantics/more_categories/TransformingLaxMorph.v | 6 +++--- theories/Crypt/rhl_semantics/only_prob/Couplings.v | 6 +++--- theories/Crypt/rhl_semantics/only_prob/SubDistr.v | 4 ++-- theories/Crypt/rhl_semantics/only_prob/ThetaDex.v | 4 ++-- theories/Crypt/rhl_semantics/only_prob/Theta_dens.v | 6 +++--- theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v | 6 +++--- theories/Crypt/rhl_semantics/state_prob/LiftStateful.v | 6 +++--- .../state_prob/OrderEnrichedRelativeAdjunctionsExamples.v | 6 +++--- .../Crypt/rhl_semantics/state_prob/StateTransfThetaDens.v | 6 +++--- .../rhl_semantics/state_prob/StateTransformingLaxMorph.v | 8 ++++---- theories/Crypt/rules/RulesProb.v | 6 +++--- theories/Crypt/rules/RulesStateProb.v | 6 +++--- theories/Crypt/rules/UniformDistr.v | 6 +++--- theories/Crypt/rules/UniformDistrLemmas.v | 6 +++--- theories/Crypt/rules/UniformStateProb.v | 6 +++--- theories/Mon/DijkstraMonadExamples.v | 6 +++--- theories/Mon/FiniteProbabilities.v | 6 +++--- theories/Mon/MonadExamples.v | 4 ++-- theories/Mon/Monoid.v | 4 ++-- theories/Mon/SPropBase.v | 2 +- theories/Mon/SPropMonadicStructures.v | 4 ++-- theories/Mon/SpecificationMonads.v | 4 ++-- theories/Relational/Category.v | 4 ++-- theories/Relational/Commutativity.v | 6 +++--- theories/Relational/EnrichedSetting.v | 4 ++-- theories/Relational/GenericRulesSimple.v | 8 ++++---- theories/Relational/OrderEnrichedCategory.v | 4 ++-- theories/Relational/OrderEnrichedRelativeMonadExamples.v | 6 +++--- theories/Relational/Rel.v | 6 +++--- theories/Relational/RelativeMonads.v | 4 ++-- 79 files changed, 200 insertions(+), 200 deletions(-) diff --git a/_CoqProject b/_CoqProject index 2da21a23..5e78903e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,6 +1,6 @@ --Q theories/Mon Mon --Q theories/Relational Relational --Q theories/Crypt Crypt +-Q theories/Mon SSProve.Mon +-Q theories/Relational SSProve.Relational +-Q theories/Crypt SSProve.Crypt theories/Mon/Base.v theories/Mon/SPropBase.v diff --git a/theories/Crypt/Casts.v b/theories/Crypt/Casts.v index 4efd278c..9fa691ff 100644 --- a/theories/Crypt/Casts.v +++ b/theories/Crypt/Casts.v @@ -3,7 +3,7 @@ From mathcomp Require Import ssreflect ssrbool ssrnat choice fintype. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fmap. -From Crypt Require Import Prelude. +From SSProve.Crypt Require Import Prelude. From HB Require Import structures. diff --git a/theories/Crypt/Main.v b/theories/Crypt/Main.v index 4d395341..cea47c91 100644 --- a/theories/Crypt/Main.v +++ b/theories/Crypt/Main.v @@ -1,5 +1,5 @@ From Coq Require Import Utf8. -From Crypt Require pkg_composition pkg_advantage PRF ElGamal pkg_rhl +From SSProve.Crypt Require pkg_composition pkg_advantage PRF ElGamal pkg_rhl UniformStateProb RulesStateProb KEMDEM SigmaProtocol Schnorr. (* Notation to chain lets and end with 0 *) diff --git a/theories/Crypt/Package.v b/theories/Crypt/Package.v index 910fde76..b489b43b 100644 --- a/theories/Crypt/Package.v +++ b/theories/Crypt/Package.v @@ -1,4 +1,4 @@ -From Crypt Require Export +From SSProve.Crypt Require Export choice_type pkg_core_definition pkg_tactics pkg_semantics pkg_lookup pkg_advantage pkg_heap pkg_distr pkg_invariants pkg_rhl pkg_user_util pkg_notation pkg_interpreter. diff --git a/theories/Crypt/Prelude.v b/theories/Crypt/Prelude.v index 7898b94b..ca012f76 100644 --- a/theories/Crypt/Prelude.v +++ b/theories/Crypt/Prelude.v @@ -8,7 +8,7 @@ Set Warnings "notation-overridden". From HB Require Import structures. From extructures Require Import ord fset. From Equations Require Import Equations. -From Mon Require SPropBase. +From SSProve.Mon Require SPropBase. Set Bullet Behavior "Strict Subproofs". Set Default Goal Selector "!". diff --git a/theories/Crypt/choice_type.v b/theories/Crypt/choice_type.v index ed58c95c..4f420fab 100644 --- a/theories/Crypt/choice_type.v +++ b/theories/Crypt/choice_type.v @@ -7,7 +7,7 @@ From Coq Require Import Utf8 Lia. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples GenericRulesSimple. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". @@ -16,10 +16,10 @@ From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From HB Require Import structures. -From Crypt Require Import Prelude Axioms Casts. +From SSProve.Crypt Require Import Prelude Axioms Casts. From deriving Require Import deriving. From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. +From SSProve.Mon Require Import SPropBase. Require Equations.Prop.DepElim. From Equations Require Import Equations. diff --git a/theories/Crypt/examples/AsymScheme.v b/theories/Crypt/examples/AsymScheme.v index 2d65eee1..4fd4308f 100644 --- a/theories/Crypt/examples/AsymScheme.v +++ b/theories/Crypt/examples/AsymScheme.v @@ -12,14 +12,14 @@ *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/DDH.v b/theories/Crypt/examples/DDH.v index 2585e24f..a4161e23 100644 --- a/theories/Crypt/examples/DDH.v +++ b/theories/Crypt/examples/DDH.v @@ -1,4 +1,4 @@ -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths,-notation-incompatible-format". From mathcomp Require Import all_ssreflect all_algebra reals distr @@ -6,7 +6,7 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr seq. Set Warnings "notation-overridden,ambiguous-paths,notation-incompatible-format". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb Package Prelude pkg_composition. diff --git a/theories/Crypt/examples/ElGamal.v b/theories/Crypt/examples/ElGamal.v index 40a9829b..191b4282 100644 --- a/theories/Crypt/examples/ElGamal.v +++ b/theories/Crypt/examples/ElGamal.v @@ -4,7 +4,7 @@ *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum @@ -12,9 +12,9 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr realsum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. +From SSProve.Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude AsymScheme. diff --git a/theories/Crypt/examples/Executor.v b/theories/Crypt/examples/Executor.v index edad8f38..b59a20da 100644 --- a/theories/Crypt/examples/Executor.v +++ b/theories/Crypt/examples/Executor.v @@ -1,11 +1,11 @@ -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude RandomOracle. diff --git a/theories/Crypt/examples/KEMDEM.v b/theories/Crypt/examples/KEMDEM.v index 9df1e822..f94aab69 100644 --- a/theories/Crypt/examples/KEMDEM.v +++ b/theories/Crypt/examples/KEMDEM.v @@ -8,7 +8,7 @@ its security relative to that of the KEM and the DEM. *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths,-notation-incompatible-format". From mathcomp Require Import all_ssreflect all_algebra reals distr @@ -16,7 +16,7 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr seq. Set Warnings "notation-overridden,ambiguous-paths,notation-incompatible-format". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb Package Prelude pkg_composition. diff --git a/theories/Crypt/examples/MACCCA.v b/theories/Crypt/examples/MACCCA.v index a0bb7a7f..cdeb002c 100644 --- a/theories/Crypt/examples/MACCCA.v +++ b/theories/Crypt/examples/MACCCA.v @@ -10,15 +10,15 @@ negligible by assumption, hence the scheme is secure. *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/OTP.v b/theories/Crypt/examples/OTP.v index 8cf2f8c5..131b5437 100644 --- a/theories/Crypt/examples/OTP.v +++ b/theories/Crypt/examples/OTP.v @@ -2,7 +2,7 @@ OTP example *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths,-notation-incompatible-format". From mathcomp Require Import all_ssreflect all_algebra reals distr @@ -10,7 +10,7 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr seq. Set Warnings "notation-overridden,ambiguous-paths,notation-incompatible-format". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/OVN.v b/theories/Crypt/examples/OVN.v index 0f687225..33974f14 100644 --- a/theories/Crypt/examples/OVN.v +++ b/theories/Crypt/examples/OVN.v @@ -1,5 +1,5 @@ -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum @@ -7,7 +7,7 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr realsum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_composition Package Prelude SigmaProtocol Schnorr DDH Canonicals. diff --git a/theories/Crypt/examples/PRF.v b/theories/Crypt/examples/PRF.v index 1487be96..f46986cb 100644 --- a/theories/Crypt/examples/PRF.v +++ b/theories/Crypt/examples/PRF.v @@ -10,15 +10,15 @@ *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/PRFMAC.v b/theories/Crypt/examples/PRFMAC.v index 16621b63..bc064cc0 100644 --- a/theories/Crypt/examples/PRFMAC.v +++ b/theories/Crypt/examples/PRFMAC.v @@ -13,15 +13,15 @@ negligible in [n]. *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/PRFPRG.v b/theories/Crypt/examples/PRFPRG.v index 9fe35fcb..f68a6f2d 100644 --- a/theories/Crypt/examples/PRFPRG.v +++ b/theories/Crypt/examples/PRFPRG.v @@ -8,15 +8,15 @@ make it a hypothesis of the final statement [security_based_on_prf]. *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/PRPCCA.v b/theories/Crypt/examples/PRPCCA.v index d630f541..93817cc2 100644 --- a/theories/Crypt/examples/PRPCCA.v +++ b/theories/Crypt/examples/PRPCCA.v @@ -14,15 +14,15 @@ by SSProve. *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/RandomOracle.v b/theories/Crypt/examples/RandomOracle.v index faa83932..ccd71d45 100644 --- a/theories/Crypt/examples/RandomOracle.v +++ b/theories/Crypt/examples/RandomOracle.v @@ -1,11 +1,11 @@ -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/Schnorr.v b/theories/Crypt/examples/Schnorr.v index a1633071..75c091f4 100644 --- a/theories/Crypt/examples/Schnorr.v +++ b/theories/Crypt/examples/Schnorr.v @@ -1,5 +1,5 @@ -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum @@ -7,9 +7,9 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr realsum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. +From SSProve.Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude SigmaProtocol Casts. diff --git a/theories/Crypt/examples/SecretSharing.v b/theories/Crypt/examples/SecretSharing.v index ee9887ac..364cd5b9 100644 --- a/theories/Crypt/examples/SecretSharing.v +++ b/theories/Crypt/examples/SecretSharing.v @@ -11,15 +11,15 @@ (non-inclusive). *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/ShamirSecretSharing.v b/theories/Crypt/examples/ShamirSecretSharing.v index 5fff74f9..4b967c3b 100644 --- a/theories/Crypt/examples/ShamirSecretSharing.v +++ b/theories/Crypt/examples/ShamirSecretSharing.v @@ -23,15 +23,15 @@ [p]. *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/SigmaProtocol.v b/theories/Crypt/examples/SigmaProtocol.v index bb5ae4b1..84d71830 100644 --- a/theories/Crypt/examples/SigmaProtocol.v +++ b/theories/Crypt/examples/SigmaProtocol.v @@ -1,5 +1,5 @@ -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum @@ -7,7 +7,7 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr realsum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude RandomOracle Casts. diff --git a/theories/Crypt/examples/StretchPRG.v b/theories/Crypt/examples/StretchPRG.v index c365384d..531dc030 100644 --- a/theories/Crypt/examples/StretchPRG.v +++ b/theories/Crypt/examples/StretchPRG.v @@ -4,15 +4,15 @@ It is simple and easy to follow. *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/SymmRatchet.v b/theories/Crypt/examples/SymmRatchet.v index 8d4e641e..95a8dfa0 100644 --- a/theories/Crypt/examples/SymmRatchet.v +++ b/theories/Crypt/examples/SymmRatchet.v @@ -5,15 +5,15 @@ The one part we cannot prove is the *) -From Relational Require Import OrderEnrichedCategory GenericRulesSimple. +From SSProve.Relational Require Import OrderEnrichedCategory GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude. diff --git a/theories/Crypt/examples/interpreter_test.v b/theories/Crypt/examples/interpreter_test.v index 55103e17..499c0f68 100644 --- a/theories/Crypt/examples/interpreter_test.v +++ b/theories/Crypt/examples/interpreter_test.v @@ -2,7 +2,7 @@ Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Prelude choice_type Package. +From SSProve.Crypt Require Import Prelude choice_type Package. From Coq Require Import Utf8. From extructures Require Import ord fset fmap. diff --git a/theories/Crypt/examples/package_usage_example.v b/theories/Crypt/examples/package_usage_example.v index 5e7928d8..c5c5c57f 100644 --- a/theories/Crypt/examples/package_usage_example.v +++ b/theories/Crypt/examples/package_usage_example.v @@ -8,7 +8,7 @@ Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-forma From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Crypt Require Import RulesStateProb Package Prelude. +From SSProve.Crypt Require Import RulesStateProb Package Prelude. Import PackageNotation. From Equations Require Import Equations. diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v index 42d42347..ad993965 100644 --- a/theories/Crypt/package/pkg_advantage.v +++ b/theories/Crypt/package/pkg_advantage.v @@ -2,15 +2,15 @@ From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup. @@ -18,7 +18,7 @@ Require Import Equations.Prop.DepElim. From Equations Require Import Equations. (* Must come after importing Equations.Equations, who knows why. *) -From Crypt Require Import FreeProbProg. +From SSProve.Crypt Require Import FreeProbProg. Import Num.Theory. diff --git a/theories/Crypt/package/pkg_composition.v b/theories/Crypt/package/pkg_composition.v index b469896d..fae23832 100644 --- a/theories/Crypt/package/pkg_composition.v +++ b/theories/Crypt/package/pkg_composition.v @@ -9,13 +9,13 @@ From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssreflect eqtype choice seq ssrfun ssrbool ssrnat. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd StateTransformingLaxMorph choice_type pkg_core_definition RulesStateProb. From Equations Require Import Equations. diff --git a/theories/Crypt/package/pkg_core_definition.v b/theories/Crypt/package/pkg_core_definition.v index b5b1e94f..aadc3cb0 100644 --- a/theories/Crypt/package/pkg_core_definition.v +++ b/theories/Crypt/package/pkg_core_definition.v @@ -8,13 +8,13 @@ *) From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssreflect eqtype choice seq ssrfun ssrbool. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph choice_type Casts. Require Import Equations.Prop.DepElim. diff --git a/theories/Crypt/package/pkg_distr.v b/theories/Crypt/package/pkg_distr.v index f486dc16..9c820ac1 100644 --- a/theories/Crypt/package/pkg_distr.v +++ b/theories/Crypt/package/pkg_distr.v @@ -5,15 +5,15 @@ From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage. @@ -21,7 +21,7 @@ Require Import Equations.Prop.DepElim. From Equations Require Import Equations. (* Must come after importing Equations.Equations, who knows why. *) -From Crypt Require Import FreeProbProg. +From SSProve.Crypt Require Import FreeProbProg. Import Num.Theory. diff --git a/theories/Crypt/package/pkg_heap.v b/theories/Crypt/package/pkg_heap.v index cc2c63c3..6bfa430f 100644 --- a/theories/Crypt/package/pkg_heap.v +++ b/theories/Crypt/package/pkg_heap.v @@ -5,15 +5,15 @@ From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition. @@ -21,7 +21,7 @@ Require Import Equations.Prop.DepElim. From Equations Require Import Equations. (* Must come after importing Equations.Equations, who knows why. *) -From Crypt Require Import FreeProbProg. +From SSProve.Crypt Require Import FreeProbProg. Set Equations With UIP. Set Equations Transparent. diff --git a/theories/Crypt/package/pkg_interpreter.v b/theories/Crypt/package/pkg_interpreter.v index bcb4f058..4995f402 100644 --- a/theories/Crypt/package/pkg_interpreter.v +++ b/theories/Crypt/package/pkg_interpreter.v @@ -2,7 +2,7 @@ Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Prelude choice_type +From SSProve.Crypt Require Import Prelude choice_type pkg_core_definition pkg_tactics pkg_distr pkg_notation. From Coq Require Import Utf8. diff --git a/theories/Crypt/package/pkg_invariants.v b/theories/Crypt/package/pkg_invariants.v index 05fa0d66..ed13bfa5 100644 --- a/theories/Crypt/package/pkg_invariants.v +++ b/theories/Crypt/package/pkg_invariants.v @@ -5,7 +5,7 @@ From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype @@ -15,8 +15,8 @@ Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From HB Require Import structures. From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage. @@ -24,7 +24,7 @@ Require Import Equations.Prop.DepElim. From Equations Require Import Equations. (* Must come after importing Equations.Equations, who knows why. *) -From Crypt Require Import FreeProbProg. +From SSProve.Crypt Require Import FreeProbProg. Import Num.Theory. diff --git a/theories/Crypt/package/pkg_lookup.v b/theories/Crypt/package/pkg_lookup.v index a4445e43..32388609 100644 --- a/theories/Crypt/package/pkg_lookup.v +++ b/theories/Crypt/package/pkg_lookup.v @@ -2,15 +2,15 @@ From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics. @@ -18,7 +18,7 @@ Require Import Equations.Prop.DepElim. From Equations Require Import Equations. (* Must come after importing Equations.Equations, who knows why. *) -From Crypt Require Import FreeProbProg. +From SSProve.Crypt Require Import FreeProbProg. Import Num.Theory. diff --git a/theories/Crypt/package/pkg_notation.v b/theories/Crypt/package/pkg_notation.v index ae5ec90d..0770d90a 100644 --- a/theories/Crypt/package/pkg_notation.v +++ b/theories/Crypt/package/pkg_notation.v @@ -99,7 +99,7 @@ From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq. Set Warnings "notation-overridden,ambiguous-paths". From extructures Require Import ord fset fmap. -From Crypt Require Import Prelude Axioms ChoiceAsOrd RulesStateProb +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd RulesStateProb choice_type pkg_core_definition pkg_composition. diff --git a/theories/Crypt/package/pkg_rhl.v b/theories/Crypt/package/pkg_rhl.v index b3393a5a..24cbfda4 100644 --- a/theories/Crypt/package/pkg_rhl.v +++ b/theories/Crypt/package/pkg_rhl.v @@ -6,15 +6,15 @@ From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage @@ -23,7 +23,7 @@ Require Import Equations.Prop.DepElim. From Equations Require Import Equations. (* Must come after importing Equations.Equations, who knows why. *) -From Crypt Require Import FreeProbProg. +From SSProve.Crypt Require Import FreeProbProg. Import Num.Theory. diff --git a/theories/Crypt/package/pkg_semantics.v b/theories/Crypt/package/pkg_semantics.v index a090bc77..ee83dcca 100644 --- a/theories/Crypt/package/pkg_semantics.v +++ b/theories/Crypt/package/pkg_semantics.v @@ -5,15 +5,15 @@ From Coq Require Import Utf8. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Mon Require Import SPropBase. -From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings +From SSProve.Mon Require Import SPropBase. +From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap. @@ -21,7 +21,7 @@ Require Import Equations.Prop.DepElim. From Equations Require Import Equations. (* Must come after importing Equations.Equations, who knows why. *) -From Crypt Require Import FreeProbProg. +From SSProve.Crypt Require Import FreeProbProg. Set Equations With UIP. Set Equations Transparent. diff --git a/theories/Crypt/package/pkg_tactics.v b/theories/Crypt/package/pkg_tactics.v index ab3bb655..fe0f1c32 100644 --- a/theories/Crypt/package/pkg_tactics.v +++ b/theories/Crypt/package/pkg_tactics.v @@ -31,7 +31,7 @@ From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq eqtype choice. Set Warnings "notation-overridden,ambiguous-paths". From extructures Require Import ord fset fmap. -From Crypt Require Import Prelude pkg_core_definition +From SSProve.Crypt Require Import Prelude pkg_core_definition pkg_composition pkg_notation choice_type RulesStateProb. From Coq Require Import Utf8 FunctionalExtensionality diff --git a/theories/Crypt/package/pkg_user_util.v b/theories/Crypt/package/pkg_user_util.v index 03fd9e6c..983d50f8 100644 --- a/theories/Crypt/package/pkg_user_util.v +++ b/theories/Crypt/package/pkg_user_util.v @@ -75,7 +75,7 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr seq. Set Warnings "notation-overridden,ambiguous-paths,notation-incompatible-format". From extructures Require Import ord fset fmap. -From Crypt Require Import Axioms Prelude pkg_core_definition pkg_composition +From SSProve.Crypt Require Import Axioms Prelude pkg_core_definition pkg_composition pkg_notation RulesStateProb pkg_advantage pkg_lookup pkg_semantics pkg_heap pkg_invariants pkg_distr pkg_rhl pkg_tactics choice_type. From Coq Require Import Utf8 FunctionalExtensionality diff --git a/theories/Crypt/rhl_semantics/ChoiceAsOrd.v b/theories/Crypt/rhl_semantics/ChoiceAsOrd.v index 1e59e3cb..9a70f023 100644 --- a/theories/Crypt/rhl_semantics/ChoiceAsOrd.v +++ b/theories/Crypt/rhl_semantics/ChoiceAsOrd.v @@ -1,6 +1,6 @@ -From Mon Require Import SPropBase. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Crypt Require Import Casts. +From SSProve.Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Crypt Require Import Casts. Set Warnings "-notation-overridden". From mathcomp Require Import all_ssreflect. Set Warnings "notation-overridden". diff --git a/theories/Crypt/rhl_semantics/free_monad/FreeProbProg.v b/theories/Crypt/rhl_semantics/free_monad/FreeProbProg.v index 9c4cfb43..a4fca59d 100644 --- a/theories/Crypt/rhl_semantics/free_monad/FreeProbProg.v +++ b/theories/Crypt/rhl_semantics/free_monad/FreeProbProg.v @@ -1,9 +1,9 @@ Set Warnings "-notation-overridden". From mathcomp Require Import all_ssreflect boolp. Set Warnings "notation-overridden". -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Crypt Require Import ChoiceAsOrd choice_type. -From Crypt Require Import SubDistr. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Crypt Require Import ChoiceAsOrd choice_type. +From SSProve.Crypt Require Import SubDistr. (*so that Next Obligation doesnt introduce variables by itself:*) diff --git a/theories/Crypt/rhl_semantics/free_monad/UniversalFreeMap.v b/theories/Crypt/rhl_semantics/free_monad/UniversalFreeMap.v index a745ec4c..e90bf9aa 100644 --- a/theories/Crypt/rhl_semantics/free_monad/UniversalFreeMap.v +++ b/theories/Crypt/rhl_semantics/free_monad/UniversalFreeMap.v @@ -1,9 +1,9 @@ -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Mon Require Import SPropBase. Set Warnings "-notation-overridden". From mathcomp Require Import all_ssreflect. Set Warnings "notation-overridden". -From Crypt Require Import FreeProbProg ChoiceAsOrd. +From SSProve.Crypt Require Import FreeProbProg ChoiceAsOrd. Import SPropNotations. diff --git a/theories/Crypt/rhl_semantics/more_categories/InitialRelativeMonad.v b/theories/Crypt/rhl_semantics/more_categories/InitialRelativeMonad.v index f118eed6..3cd877ca 100644 --- a/theories/Crypt/rhl_semantics/more_categories/InitialRelativeMonad.v +++ b/theories/Crypt/rhl_semantics/more_categories/InitialRelativeMonad.v @@ -1,4 +1,4 @@ -From Relational Require Import OrderEnrichedCategory. +From SSProve.Relational Require Import OrderEnrichedCategory. (*In this file we devise a relative monad morphism Id -> M having the unit of M as carrier*) diff --git a/theories/Crypt/rhl_semantics/more_categories/LaxComp.v b/theories/Crypt/rhl_semantics/more_categories/LaxComp.v index 364a3391..58ddae1a 100644 --- a/theories/Crypt/rhl_semantics/more_categories/LaxComp.v +++ b/theories/Crypt/rhl_semantics/more_categories/LaxComp.v @@ -1,6 +1,6 @@ From Coq Require Import ssreflect. -From Mon Require Import SPropBase. -From Relational Require Import OrderEnrichedCategory. +From SSProve.Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory. Import SPropNotations. diff --git a/theories/Crypt/rhl_semantics/more_categories/LaxFunctorsAndTransf.v b/theories/Crypt/rhl_semantics/more_categories/LaxFunctorsAndTransf.v index 9e4f59ad..5255eaaa 100644 --- a/theories/Crypt/rhl_semantics/more_categories/LaxFunctorsAndTransf.v +++ b/theories/Crypt/rhl_semantics/more_categories/LaxFunctorsAndTransf.v @@ -1,10 +1,10 @@ From Coq Require Import Morphisms. -From Relational Require Import OrderEnrichedCategory. -From Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory. +From SSProve.Mon Require Import SPropBase. Set Warnings "-notation-overridden". From mathcomp Require Import all_ssreflect boolp. Set Warnings "notation-overridden". -From Crypt Require Import Axioms. +From SSProve.Crypt Require Import Axioms. Obligation Tactic := try (Tactics.program_simpl ; fail) ; simpl. diff --git a/theories/Crypt/rhl_semantics/more_categories/LaxMorphismOfRelAdjunctions.v b/theories/Crypt/rhl_semantics/more_categories/LaxMorphismOfRelAdjunctions.v index 73cb3bb8..9a49b6d5 100644 --- a/theories/Crypt/rhl_semantics/more_categories/LaxMorphismOfRelAdjunctions.v +++ b/theories/Crypt/rhl_semantics/more_categories/LaxMorphismOfRelAdjunctions.v @@ -1,9 +1,9 @@ -From Relational Require Import OrderEnrichedCategory. -From Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory. +From SSProve.Mon Require Import SPropBase. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect boolp. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf. +From SSProve.Crypt Require Import Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf. Import SPropNotations. (* diff --git a/theories/Crypt/rhl_semantics/more_categories/OrderEnrichedRelativeAdjunctions.v b/theories/Crypt/rhl_semantics/more_categories/OrderEnrichedRelativeAdjunctions.v index cf86188b..18f09b5d 100644 --- a/theories/Crypt/rhl_semantics/more_categories/OrderEnrichedRelativeAdjunctions.v +++ b/theories/Crypt/rhl_semantics/more_categories/OrderEnrichedRelativeAdjunctions.v @@ -1,6 +1,6 @@ From Coq Require Import Relation_Definitions Morphisms. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Mon Require Import SPropBase. Set Warnings "-notation-overridden". From mathcomp Require Import all_ssreflect boolp. Set Warnings "notation-overridden". diff --git a/theories/Crypt/rhl_semantics/more_categories/RelativeMonadMorph_prod.v b/theories/Crypt/rhl_semantics/more_categories/RelativeMonadMorph_prod.v index 8d9417ce..80ffb288 100644 --- a/theories/Crypt/rhl_semantics/more_categories/RelativeMonadMorph_prod.v +++ b/theories/Crypt/rhl_semantics/more_categories/RelativeMonadMorph_prod.v @@ -1,4 +1,4 @@ -From Relational Require Import OrderEnrichedCategory. +From SSProve.Relational Require Import OrderEnrichedCategory. Set Warnings "-notation-overridden". From mathcomp Require Import all_ssreflect. Set Warnings "notation-overridden". diff --git a/theories/Crypt/rhl_semantics/more_categories/TransformingLaxMorph.v b/theories/Crypt/rhl_semantics/more_categories/TransformingLaxMorph.v index 2f01d5ba..7176d1ee 100644 --- a/theories/Crypt/rhl_semantics/more_categories/TransformingLaxMorph.v +++ b/theories/Crypt/rhl_semantics/more_categories/TransformingLaxMorph.v @@ -1,10 +1,10 @@ From Coq Require Import Relation_Definitions. -From Relational Require Import OrderEnrichedCategory. -From Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory. +From SSProve.Mon Require Import SPropBase. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect boolp. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions. +From SSProve.Crypt Require Import Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions. Import SPropNotations. diff --git a/theories/Crypt/rhl_semantics/only_prob/Couplings.v b/theories/Crypt/rhl_semantics/only_prob/Couplings.v index bef9ea2d..c16333f7 100644 --- a/theories/Crypt/rhl_semantics/only_prob/Couplings.v +++ b/theories/Crypt/rhl_semantics/only_prob/Couplings.v @@ -1,10 +1,10 @@ -From Mon Require Import FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities. +From SSProve.Mon Require Import FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities. From Coq Require Import RelationClasses Morphisms. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms ChoiceAsOrd only_prob.SubDistr. +From SSProve.Crypt Require Import Axioms ChoiceAsOrd only_prob.SubDistr. Import SPropNotations. Import Num.Theory. diff --git a/theories/Crypt/rhl_semantics/only_prob/SubDistr.v b/theories/Crypt/rhl_semantics/only_prob/SubDistr.v index 503eaeec..b36e57a9 100644 --- a/theories/Crypt/rhl_semantics/only_prob/SubDistr.v +++ b/theories/Crypt/rhl_semantics/only_prob/SubDistr.v @@ -2,8 +2,8 @@ From Coq Require Import Relation_Definitions Morphisms. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra distr reals realsum. Set Warnings "notation-overridden,ambiguous-paths". -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Crypt Require Import ChoiceAsOrd Axioms. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Crypt Require Import ChoiceAsOrd Axioms. Import Num.Theory. Import Order.POrderTheory. diff --git a/theories/Crypt/rhl_semantics/only_prob/ThetaDex.v b/theories/Crypt/rhl_semantics/only_prob/ThetaDex.v index 3a9e807a..f0259bef 100644 --- a/theories/Crypt/rhl_semantics/only_prob/ThetaDex.v +++ b/theories/Crypt/rhl_semantics/only_prob/ThetaDex.v @@ -1,5 +1,5 @@ -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Crypt Require Import Theta_dens Theta_exCP SubDistr LaxComp ChoiceAsOrd RelativeMonadMorph_prod. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Crypt Require Import Theta_dens Theta_exCP SubDistr LaxComp ChoiceAsOrd RelativeMonadMorph_prod. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect. Set Warnings "notation-overridden,ambiguous-paths". diff --git a/theories/Crypt/rhl_semantics/only_prob/Theta_dens.v b/theories/Crypt/rhl_semantics/only_prob/Theta_dens.v index ab5f6485..dc4687f9 100644 --- a/theories/Crypt/rhl_semantics/only_prob/Theta_dens.v +++ b/theories/Crypt/rhl_semantics/only_prob/Theta_dens.v @@ -1,9 +1,9 @@ -From Mon Require Import FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity. +From SSProve.Mon Require Import FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import ChoiceAsOrd Axioms RelativeMonadMorph_prod FreeProbProg SubDistr choice_type. +From SSProve.Crypt Require Import ChoiceAsOrd Axioms RelativeMonadMorph_prod FreeProbProg SubDistr choice_type. Import SPropNotations. diff --git a/theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v b/theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v index a9275d9d..e6ad222a 100644 --- a/theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v +++ b/theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v @@ -1,9 +1,9 @@ Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra boolp distr reals realsum. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SpecificationMonads SPropBase SPropMonadicStructures. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Crypt Require Import ChoiceAsOrd SubDistr Couplings Axioms Casts. +From SSProve.Mon Require Import SpecificationMonads SPropBase SPropMonadicStructures. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Crypt Require Import ChoiceAsOrd SubDistr Couplings Axioms Casts. From HB Require Import structures. Import SPropNotations. diff --git a/theories/Crypt/rhl_semantics/state_prob/LiftStateful.v b/theories/Crypt/rhl_semantics/state_prob/LiftStateful.v index e4433d48..2731f028 100644 --- a/theories/Crypt/rhl_semantics/state_prob/LiftStateful.v +++ b/theories/Crypt/rhl_semantics/state_prob/LiftStateful.v @@ -2,9 +2,9 @@ From Coq Require Import Morphisms. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Crypt Require Import OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd. +From SSProve.Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Crypt Require Import OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples ChoiceAsOrd. Import SPropNotations. diff --git a/theories/Crypt/rhl_semantics/state_prob/OrderEnrichedRelativeAdjunctionsExamples.v b/theories/Crypt/rhl_semantics/state_prob/OrderEnrichedRelativeAdjunctionsExamples.v index 3a364056..854ff3ed 100644 --- a/theories/Crypt/rhl_semantics/state_prob/OrderEnrichedRelativeAdjunctionsExamples.v +++ b/theories/Crypt/rhl_semantics/state_prob/OrderEnrichedRelativeAdjunctionsExamples.v @@ -2,9 +2,9 @@ From Coq Require Import Morphisms. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_algebra all_ssreflect boolp. Set Warnings "notation-overridden,ambiguous-paths". -From Mon Require Import SPropBase Base. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Crypt Require Import OrderEnrichedRelativeAdjunctions FreeProbProg ChoiceAsOrd Couplings Theta_exCP SubDistr. +From SSProve.Mon Require Import SPropBase Base. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Crypt Require Import OrderEnrichedRelativeAdjunctions FreeProbProg ChoiceAsOrd Couplings Theta_exCP SubDistr. Import SPropNotations. diff --git a/theories/Crypt/rhl_semantics/state_prob/StateTransfThetaDens.v b/theories/Crypt/rhl_semantics/state_prob/StateTransfThetaDens.v index 864b28c3..771ee0da 100644 --- a/theories/Crypt/rhl_semantics/state_prob/StateTransfThetaDens.v +++ b/theories/Crypt/rhl_semantics/state_prob/StateTransfThetaDens.v @@ -1,10 +1,10 @@ From Coq Require Import RelationClasses. -From Mon Require Import SPropBase. +From SSProve.Mon Require Import SPropBase. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect. Set Warnings "notation-overridden,ambiguous-paths". -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Crypt Require Import ChoiceAsOrd OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples TransformingLaxMorph SubDistr Theta_dens LaxFunctorsAndTransf UniversalFreeMap FreeProbProg StateTransformingLaxMorph LaxComp. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Crypt Require Import ChoiceAsOrd OrderEnrichedRelativeAdjunctions OrderEnrichedRelativeAdjunctionsExamples TransformingLaxMorph SubDistr Theta_dens LaxFunctorsAndTransf UniversalFreeMap FreeProbProg StateTransformingLaxMorph LaxComp. Import SPropNotations. diff --git a/theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v b/theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v index 6db7e7aa..22b223b5 100644 --- a/theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v +++ b/theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v @@ -1,12 +1,12 @@ (* From Coq Require Import Program.Wf. *) From Coq Require Import Relation_Definitions. -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. -From Mon Require Import SPropBase. +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Mon Require Import SPropBase. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect (*boolp*). Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions TransformingLaxMorph OrderEnrichedRelativeAdjunctionsExamples ThetaDex SubDistr Theta_exCP ChoiceAsOrd FreeProbProg UniversalFreeMap RelativeMonadMorph_prod LaxComp choice_type Casts. -(* From Crypt Require Import only_prob.Rules. *) +From SSProve.Crypt Require Import Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions TransformingLaxMorph OrderEnrichedRelativeAdjunctionsExamples ThetaDex SubDistr Theta_exCP ChoiceAsOrd FreeProbProg UniversalFreeMap RelativeMonadMorph_prod LaxComp choice_type Casts. +(* From SSProve.Crypt Require Import only_prob.Rules. *) Import SPropNotations. diff --git a/theories/Crypt/rules/RulesProb.v b/theories/Crypt/rules/RulesProb.v index c65e13ae..cd65ec9f 100644 --- a/theories/Crypt/rules/RulesProb.v +++ b/theories/Crypt/rules/RulesProb.v @@ -1,13 +1,13 @@ From Coq Require Import RelationClasses Morphisms Utf8. -From Mon Require Import +From SSProve.Mon Require Import FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase. -From Relational Require Import +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity @@ -22,7 +22,7 @@ From mathcomp Require Import realsum. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr diff --git a/theories/Crypt/rules/RulesStateProb.v b/theories/Crypt/rules/RulesStateProb.v index d14e9b25..ff247dd4 100644 --- a/theories/Crypt/rules/RulesStateProb.v +++ b/theories/Crypt/rules/RulesStateProb.v @@ -1,9 +1,9 @@ From Coq Require Import RelationClasses Morphisms Utf8. -From Mon Require Import SPropMonadicStructures SpecificationMonads MonadExamples +From SSProve.Mon Require Import SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". @@ -11,7 +11,7 @@ From mathcomp Require Import all_ssreflect all_algebra reals distr realsum finset finmap.finmap xfinmap . Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings Theta_dens +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod StateTransformingLaxMorph choice_type Casts. diff --git a/theories/Crypt/rules/UniformDistr.v b/theories/Crypt/rules/UniformDistr.v index 7baf4d30..396f6422 100644 --- a/theories/Crypt/rules/UniformDistr.v +++ b/theories/Crypt/rules/UniformDistr.v @@ -1,13 +1,13 @@ From Coq Require Import RelationClasses Morphisms. -From Mon Require Import +From SSProve.Mon Require Import FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase. -From Relational Require Import +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity @@ -22,7 +22,7 @@ From mathcomp Require Import realsum. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr diff --git a/theories/Crypt/rules/UniformDistrLemmas.v b/theories/Crypt/rules/UniformDistrLemmas.v index 95bdd3b9..e3ff5ea2 100644 --- a/theories/Crypt/rules/UniformDistrLemmas.v +++ b/theories/Crypt/rules/UniformDistrLemmas.v @@ -1,14 +1,14 @@ From Coq Require Import Relation_Definitions RelationClasses Morphisms Utf8. -From Mon Require Import +From SSProve.Mon Require Import FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase. -From Relational Require Import +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity @@ -23,7 +23,7 @@ From mathcomp Require Import realsum. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr diff --git a/theories/Crypt/rules/UniformStateProb.v b/theories/Crypt/rules/UniformStateProb.v index d4f8c044..6b204d83 100644 --- a/theories/Crypt/rules/UniformStateProb.v +++ b/theories/Crypt/rules/UniformStateProb.v @@ -1,14 +1,14 @@ -From Mon Require Import FiniteProbabilities SPropMonadicStructures +From SSProve.Mon Require Import FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr realsum. Set Warnings "notation-overridden,ambiguous-paths". -From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings Theta_dens +From SSProve.Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg UniformDistrLemmas Prelude choice_type StateTransformingLaxMorph RulesStateProb. diff --git a/theories/Mon/DijkstraMonadExamples.v b/theories/Mon/DijkstraMonadExamples.v index 52b0af48..b8113c10 100644 --- a/theories/Mon/DijkstraMonadExamples.v +++ b/theories/Mon/DijkstraMonadExamples.v @@ -1,6 +1,6 @@ From Coq Require Import ssreflect ssrfun. -From Mon Require Export Base. -From Mon Require Import SPropBase SPropMonadicStructures Monoid SpecificationMonads MonadExamples. +From SSProve.Mon Require Export Base. +From SSProve.Mon Require Import SPropBase SPropMonadicStructures Monoid SpecificationMonads MonadExamples. Set Implicit Arguments. Unset Strict Implicit. @@ -341,7 +341,7 @@ End SumOfTheories. (** Deactivated temporarily *) (* From Equations Require Import Equations. *) -(* From Mon Require Import WellFounded. *) +(* From SSProve.Mon Require Import WellFounded. *) (* Derive NoConfusion for FreeF. *) (* Derive Subterm for FreeF. *) diff --git a/theories/Mon/FiniteProbabilities.v b/theories/Mon/FiniteProbabilities.v index c9311c9d..868d9147 100644 --- a/theories/Mon/FiniteProbabilities.v +++ b/theories/Mon/FiniteProbabilities.v @@ -1,13 +1,13 @@ From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require FunctionalExtensionality List. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq Require Import Relation_Definitions Morphisms. -From Mon Require Import SPropBase SPropMonadicStructures MonadExamples SpecificationMonads Monoid DijkstraMonadExamples. +From SSProve.Mon Require Import SPropBase SPropMonadicStructures MonadExamples SpecificationMonads Monoid DijkstraMonadExamples. Set Warnings "-notation-overridden,-ambiguous-paths". From mathcomp Require Import all_ssreflect all_algebra reals distr. Set Warnings "notation-overridden,ambiguous-paths". -From Relational Require Import Commutativity. +From SSProve.Relational Require Import Commutativity. Import GRing.Theory Num.Theory. Import Order.POrderTheory. diff --git a/theories/Mon/MonadExamples.v b/theories/Mon/MonadExamples.v index 1f4ccc04..216517f6 100644 --- a/theories/Mon/MonadExamples.v +++ b/theories/Mon/MonadExamples.v @@ -1,6 +1,6 @@ From Coq Require Import ssreflect List. -From Mon Require Export Base. -From Mon Require Import SPropBase SPropMonadicStructures Monoid. +From SSProve.Mon Require Export Base. +From SSProve.Mon Require Import SPropBase SPropMonadicStructures Monoid. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Mon/Monoid.v b/theories/Mon/Monoid.v index 781c4c40..c59b8534 100644 --- a/theories/Mon/Monoid.v +++ b/theories/Mon/Monoid.v @@ -1,8 +1,8 @@ From Coq Require Import ssreflect ssrfun ssrbool List. From Coq Require Import FunctionalExtensionality. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq Require Import Relation_Definitions Morphisms. -From Mon Require Import SPropBase SPropMonadicStructures. +From SSProve.Mon Require Import SPropBase SPropMonadicStructures. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Mon/SPropBase.v b/theories/Mon/SPropBase.v index f11e2cfd..6cde375c 100644 --- a/theories/Mon/SPropBase.v +++ b/theories/Mon/SPropBase.v @@ -1,6 +1,6 @@ (*From Coq Require Export Logic.StrictProp.*) (*This file was originally referring to SProp. Not anymore*) -From Mon Require Import Base. +From SSProve.Mon Require Import Base. From mathcomp Require Import ssreflect. diff --git a/theories/Mon/SPropMonadicStructures.v b/theories/Mon/SPropMonadicStructures.v index 7b7b67ed..b18bc827 100644 --- a/theories/Mon/SPropMonadicStructures.v +++ b/theories/Mon/SPropMonadicStructures.v @@ -1,6 +1,6 @@ From Coq Require Import ssreflect ssrfun FunctionalExtensionality. -From Mon Require Export Base. -From Mon Require Import SPropBase. +From SSProve.Mon Require Export Base. +From SSProve.Mon Require Import SPropBase. From Coq Require Import Relation_Definitions Morphisms. Set Implicit Arguments. diff --git a/theories/Mon/SpecificationMonads.v b/theories/Mon/SpecificationMonads.v index 937617e9..0fd51124 100644 --- a/theories/Mon/SpecificationMonads.v +++ b/theories/Mon/SpecificationMonads.v @@ -1,7 +1,7 @@ From Coq Require Import ssreflect. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq Require Import Relation_Definitions Morphisms. -From Mon Require Import SPropBase SPropMonadicStructures Monoid. +From SSProve.Mon Require Import SPropBase SPropMonadicStructures Monoid. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Relational/Category.v b/theories/Relational/Category.v index 4b7d5af8..e101501e 100644 --- a/theories/Relational/Category.v +++ b/theories/Relational/Category.v @@ -1,8 +1,8 @@ From Coq Require Import ssreflect ssrfun. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq.Relations Require Import Relation_Definitions. From Coq.Classes Require Import RelationClasses Morphisms. -From Mon Require Import SPropBase. +From SSProve.Mon Require Import SPropBase. Set Primitive Projections. Set Universe Polymorphism. diff --git a/theories/Relational/Commutativity.v b/theories/Relational/Commutativity.v index 89bdd3ee..9dadf719 100644 --- a/theories/Relational/Commutativity.v +++ b/theories/Relational/Commutativity.v @@ -1,11 +1,11 @@ From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require FunctionalExtensionality. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq Require Import Relation_Definitions Morphisms. -From Mon Require Import SPropBase SPropMonadicStructures +From SSProve.Mon Require Import SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples. -From Relational Require Import OrderEnrichedCategory +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Section Commutations. diff --git a/theories/Relational/EnrichedSetting.v b/theories/Relational/EnrichedSetting.v index 8f796411..044890cf 100644 --- a/theories/Relational/EnrichedSetting.v +++ b/theories/Relational/EnrichedSetting.v @@ -1,7 +1,7 @@ From Coq Require Import ssreflect ssrfun. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq.Classes Require Import RelationClasses Morphisms. -From Relational Require Import Category. +From SSProve.Relational Require Import Category. Set Primitive Projections. Set Universe Polymorphism. diff --git a/theories/Relational/GenericRulesSimple.v b/theories/Relational/GenericRulesSimple.v index 544c9aa9..617fde4e 100644 --- a/theories/Relational/GenericRulesSimple.v +++ b/theories/Relational/GenericRulesSimple.v @@ -1,10 +1,10 @@ From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require FunctionalExtensionality. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq Require Import Relation_Definitions Morphisms. -From Mon Require Import SPropBase SPropMonadicStructures. -(* From Relational Require Import Category RelativeMonads RelativeMonadExamples. *) -From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. +From SSProve.Mon Require Import SPropBase SPropMonadicStructures. +(* From SSProve.Relational Require Import Category RelativeMonads RelativeMonadExamples. *) +From SSProve.Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples. Set Primitive Projections. Set Universe Polymorphism. diff --git a/theories/Relational/OrderEnrichedCategory.v b/theories/Relational/OrderEnrichedCategory.v index 2b7bb23a..28b24fe4 100644 --- a/theories/Relational/OrderEnrichedCategory.v +++ b/theories/Relational/OrderEnrichedCategory.v @@ -1,6 +1,6 @@ From Coq Require Import ssreflect ssrfun. -From Mon Require Export Base. -From Mon Require Import SPropBase. +From SSProve.Mon Require Export Base. +From SSProve.Mon Require Import SPropBase. From Coq Require Import RelationClasses Morphisms Relation_Definitions. diff --git a/theories/Relational/OrderEnrichedRelativeMonadExamples.v b/theories/Relational/OrderEnrichedRelativeMonadExamples.v index 9cdbfc84..df8a51e4 100644 --- a/theories/Relational/OrderEnrichedRelativeMonadExamples.v +++ b/theories/Relational/OrderEnrichedRelativeMonadExamples.v @@ -1,9 +1,9 @@ From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require Import FunctionalExtensionality. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq Require Import Relation_Definitions Morphisms RelationPairs. -From Mon Require Import SPropBase SPropMonadicStructures. -From Relational Require Import OrderEnrichedCategory Rel. +From SSProve.Mon Require Import SPropBase SPropMonadicStructures. +From SSProve.Relational Require Import OrderEnrichedCategory Rel. Set Primitive Projections. Set Universe Polymorphism. diff --git a/theories/Relational/Rel.v b/theories/Relational/Rel.v index ae2f0578..39703d2b 100644 --- a/theories/Relational/Rel.v +++ b/theories/Relational/Rel.v @@ -1,9 +1,9 @@ From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require FunctionalExtensionality. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq Require Import Relation_Definitions Morphisms. -From Mon Require Import SPropBase. -From Relational Require Import Category RelativeMonads EnrichedSetting. +From SSProve.Mon Require Import SPropBase. +From SSProve.Relational Require Import Category RelativeMonads EnrichedSetting. Set Primitive Projections. Set Universe Polymorphism. diff --git a/theories/Relational/RelativeMonads.v b/theories/Relational/RelativeMonads.v index d6190d19..87070abe 100644 --- a/theories/Relational/RelativeMonads.v +++ b/theories/Relational/RelativeMonads.v @@ -1,7 +1,7 @@ From Coq Require Import ssreflect ssrfun. -From Mon Require Export Base. +From SSProve.Mon Require Export Base. From Coq.Classes Require Import RelationClasses Morphisms. -From Relational Require Import Category. +From SSProve.Relational Require Import Category. Set Primitive Projections. Set Universe Polymorphism.