diff --git a/.gitattributes b/.gitattributes index 127caa6eff2a0002d5a8c4cc895c47e238404c64..bcb177e24bbb3512896a25949ea8ea2f8a88585a 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1483,3 +1483,83 @@ backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/proofmode/class backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/real_closed/complex.vo filter=lfs diff=lfs merge=lfs -text backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/TwoSphere.vo filter=lfs diff=lfs merge=lfs -text backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/bi/monpred.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_complete.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_correct.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Main.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_complete.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_safe.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/BasicAst.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/config.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Environment.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentReflect.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentTyping.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Kernames.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/MonadBasicAst.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Reflect.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/uGraph.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Universes.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/UniversesDec.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EArities.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAst.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAstUtils.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/ECoInductiveToInductive.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EConstructorsAsBlocks.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EDeps.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpanded.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpandedFix.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericGlobalMap.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericMapEnv.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EImplementBox.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EInduction.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gfunctor.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/qpoly.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/view.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/spin_lock.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Paths.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/automorphism.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/implementations/semiring_pairs.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Interval/Transcend.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pFiber.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gseries.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Displayed.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/ticket_lock.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rationals.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Prod.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Integral_helper.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Card.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_ops.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/rat.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/base.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/fingroup.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/ind.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/lib/gmap_view.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances/order.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Language/Lang_expr.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/bi/lib/fixpoint.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Yoneda.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/hall.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Interval_helper.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Sigma.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/No/Addition.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_stdz.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/program_logic/adequacy.vo filter=lfs diff=lfs merge=lfs -text +backend/core/.rustup/downloads/371a98be3e239f760a7f0e87793ad0a871cdc2e607590cc47514d91fd8d1383c filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rings.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pMap.vo filter=lfs diff=lfs merge=lfs -text +backend/core/alphageometry/meliad_lib/meliad/transformer/vocabs/pg19train_bpe_32000.model filter=lfs diff=lfs merge=lfs -text +backend/core/.rustup/downloads/8c0a40a5411746ff6600d93acd16652fef56702196bb25b940ff399d7e107f40 filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/DisplayedEquiv.vo filter=lfs diff=lfs merge=lfs -text +backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/jordanholder.vo filter=lfs diff=lfs merge=lfs -text diff --git a/backend/core/.rustup/downloads/371a98be3e239f760a7f0e87793ad0a871cdc2e607590cc47514d91fd8d1383c b/backend/core/.rustup/downloads/371a98be3e239f760a7f0e87793ad0a871cdc2e607590cc47514d91fd8d1383c new file mode 100644 index 0000000000000000000000000000000000000000..a3174a6bc8f89854d251fb19fc32d194d59b9e1c --- /dev/null +++ b/backend/core/.rustup/downloads/371a98be3e239f760a7f0e87793ad0a871cdc2e607590cc47514d91fd8d1383c @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:371a98be3e239f760a7f0e87793ad0a871cdc2e607590cc47514d91fd8d1383c +size 3805000 diff --git a/backend/core/.rustup/downloads/8c0a40a5411746ff6600d93acd16652fef56702196bb25b940ff399d7e107f40 b/backend/core/.rustup/downloads/8c0a40a5411746ff6600d93acd16652fef56702196bb25b940ff399d7e107f40 new file mode 100644 index 0000000000000000000000000000000000000000..62e705b437f263e01a5f0845bbac92b550a09c7b --- /dev/null +++ b/backend/core/.rustup/downloads/8c0a40a5411746ff6600d93acd16652fef56702196bb25b940ff399d7e107f40 @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:8c0a40a5411746ff6600d93acd16652fef56702196bb25b940ff399d7e107f40 +size 9163172 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.vo new file mode 100644 index 0000000000000000000000000000000000000000..8004bddac1fd792cf56ce37bc47fa7b8e91478ed --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:9f997e28fe542a0840c686b61edce8af6fa4a4a388c7eba24bc9c34cd15acf08 +size 369181 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.vo new file mode 100644 index 0000000000000000000000000000000000000000..b7ac1b6fe19604df65bee4c301bddcc45355c544 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ff1b7ced14aedd5c31c212ce24c392981b2d7b53923131968daa8455e4242702 +size 522748 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.vo new file mode 100644 index 0000000000000000000000000000000000000000..aafbd56fd01d51ba6b298896a2b2e370fb9a1822 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:32cba916ed4a7ba98c795207dbc59e6f6ae9f2daad94881930238dcbea70e6dd +size 273119 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.vo new file mode 100644 index 0000000000000000000000000000000000000000..a498965c93c3f02881fcd7f5b554854fa05ea0ae --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:af5cb481d146c5672bd4647a1a12116978ac2a74cf32c1e9bc669ab242155490 +size 159937 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.vo new file mode 100644 index 0000000000000000000000000000000000000000..8ba00e7621b74a87f02fb276d5545b89063b1cb8 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:0a962a0ce6eb50553bf702355d1e3d1b06e0d2092bce08db3f259a27c4a812d1 +size 114642 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.vo new file mode 100644 index 0000000000000000000000000000000000000000..425fdf9f3330c3658531f7d08b630055121342eb --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:28322028ba1d17fd8bf3250a915a1ac6399ce227878c06cab3fa2fd7b67dde11 +size 1539801 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.vo new file mode 100644 index 0000000000000000000000000000000000000000..44f048f4e8ae4c0b8266900348ffd1440a992e9d --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:6adb8d3bb8a10d07bbf0e69a75f639da0c029685adfc44b32685e181392964b9 +size 1271043 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.vo new file mode 100644 index 0000000000000000000000000000000000000000..eed5ec25ac2bfb54fa7bea3ff1dc401b5ea5dde4 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:24c7899a221d5106d59cad716070d89155d3069afe39b16d4b07f80f90c4d055 +size 220502 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Sequence.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Sequence.v new file mode 100644 index 0000000000000000000000000000000000000000..27c3ce26dc9808da19bb72e63763cb308e1b33ba --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Sequence.v @@ -0,0 +1,52 @@ +Require Import Basics. +Require Import Diagrams.Graph. +Require Import Diagrams.Diagram. + +Local Open Scope nat_scope. +Local Open Scope path_scope. + +(** * Sequence *) + +(** A Sequence is a sequence of maps from [X(n)] to [X(n+1)]. *) + +Definition sequence_graph : Graph. +Proof. + srapply (Build_Graph nat). + intros n m; exact (S n = m). +Defined. + +Definition Sequence := Diagram sequence_graph. + +Definition Build_Sequence + (X : nat -> Type) + (f : forall n, X n -> X n.+1) + : Sequence. +Proof. + srapply Build_Diagram. + 1: exact X. + intros ? ? p. + destruct p. + apply f. +Defined. + +(** A useful lemma to show than two sequences are equivalent. *) + +Definition equiv_sequence (D1 D2 : Sequence) + (H0 : (D1 0) <~> (D2 0)) + (Hn: forall n (e: (D1 n) <~> (D2 n)), + {e' : (D1 n.+1) <~> (D2 n.+1) & (D2 _f 1) o e == e' o (D1 _f 1)}) + : D1 ~d~ D2. +Proof. + srapply (Build_diagram_equiv (Build_DiagramMap _ _)); intro n; simpl. + - apply equiv_fun. + induction n. + + apply H0. + + exact (Hn n IHn).1. + - intros m q; destruct q. + induction n; simpl. + + exact (Hn 0 H0).2. + + simple refine (Hn n.+1 _).2. + - induction n; simpl. + + apply H0. + + apply (Hn n _ ).1. +Defined. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Sequence.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Sequence.vo new file mode 100644 index 0000000000000000000000000000000000000000..6d392259166a4a6d46afcfb11e8a3a11192f42a3 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Sequence.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Span.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Span.v new file mode 100644 index 0000000000000000000000000000000000000000..c222890451ffe4b574f678bfa9c15135d4e63e94 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Span.v @@ -0,0 +1,36 @@ +Require Import Basics. +Require Import Types. +Require Import Diagrams.Graph. +Require Import Diagrams.Diagram. + +(** The underlying graph of a span. *) + +Definition span_graph : Graph. +Proof. + srapply (Build_Graph (Unit + Bool)). + intros [i|i] [j|j]. + 2: exact Unit. + all: exact Empty. +Defined. + +Section Span. + + Context {A B C : Type}. + + (** A span is a diagram: + f g + B <-- A --> C *) + + Definition span (f : A -> B) (g : A -> C) : Diagram span_graph. + Proof. + srapply Build_Diagram. + - intros [i|i]. + + exact A. + + exact (if i then B else C). + - intros [i|i] [j|j] u; cbn; try contradiction. + destruct j. + + exact f. + + exact g. + Defined. + +End Span. \ No newline at end of file diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Span.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Span.vo new file mode 100644 index 0000000000000000000000000000000000000000..76ec4921ad46f67a3fe8da41b913b1353e9b3596 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Span.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/BiInv.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/BiInv.v new file mode 100644 index 0000000000000000000000000000000000000000..3861cbfe5c98b3b447ca4dc3c73918e69f7c9af3 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/BiInv.v @@ -0,0 +1,55 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import HoTT.Basics HoTT.Types. + +Local Open Scope path_scope. +Generalizable Variables A B f. + +(** * Bi-invertible maps *) + +(** A map is "bi-invertible" if it has both a section and a retraction, not necessarily the same. This definition of equivalence was proposed by Andre Joyal. *) + +Definition BiInv `(f : A -> B) : Type + := {g : B -> A & g o f == idmap} * {h : B -> A & f o h == idmap}. + +(** It seems that the easiest way to show that bi-invertibility is equivalent to being an equivalence is also to show that both are h-props and that they are logically equivalent. *) + +Definition isequiv_biinv `(f : A -> B) + : BiInv f -> IsEquiv f. +Proof. + intros [[g s] [h r]]. + exact (isequiv_adjointify f g + (fun x => ap f (ap g (r x)^ @ s (h x)) @ r x) + s). +Defined. + +Definition biinv_isequiv `(f : A -> B) + : IsEquiv f -> BiInv f. +Proof. + intros [g s r adj]. + exact ((g; r), (g; s)). +Defined. + +Definition iff_biinv_isequiv `(f : A -> B) + : BiInv f <-> IsEquiv f. +Proof. + split. + - apply isequiv_biinv. + - apply biinv_isequiv. +Defined. + +Global Instance ishprop_biinv `{Funext} `(f : A -> B) : IsHProp (BiInv f) | 0. +Proof. + apply hprop_inhabited_contr. + intros bif; pose (fe := isequiv_biinv f bif). + apply @contr_prod. + (* For this, we've done all the work already. *) + - by apply contr_retr_equiv. + - by apply contr_sect_equiv. +Defined. + +Definition equiv_biinv_isequiv `{Funext} `(f : A -> B) + : BiInv f <~> IsEquiv f. +Proof. + apply equiv_iff_hprop_uncurried, iff_biinv_isequiv. +Defined. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/BiInv.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/BiInv.vo new file mode 100644 index 0000000000000000000000000000000000000000..e47bf16a2dab1a25d7d729c6bcaba50d90c1f09d Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/BiInv.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/PathSplit.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/PathSplit.v new file mode 100644 index 0000000000000000000000000000000000000000..b861351f7bd8c4ef7f1b6442691a724a984cc9cb --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/PathSplit.v @@ -0,0 +1,126 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import HoTT.Basics HoTT.Types. + +Local Open Scope nat_scope. +Local Open Scope path_scope. + +Generalizable Variables A B f. + +Section AssumeFunext. +Context `{Funext}. + +(** * n-Path-split maps. + +A map is n-path-split if its induced maps on the first n iterated path-spaces are split surjections. Thus every map is 0-path-split, the 1-path-split maps are the split surjections, and so on. It turns out that for n>1, being n-path-split is the same as being an equivalence. *) + +Fixpoint PathSplit (n : nat) `(f : A -> B) : Type + := match n with + | 0 => Unit + | S n => (forall a, hfiber f a) * + forall (x y : A), PathSplit n (@ap _ _ f x y) + end. + +Definition isequiv_pathsplit (n : nat) `{f : A -> B} +: PathSplit n.+2 f -> IsEquiv f. +Proof. + intros [g k]. + pose (h := fun x y p => (fst (k x y) p).1). + pose (hs := fun x y => (fun p => (fst (k x y) p).2) + : (ap f) o (h x y) == idmap). + clearbody hs; clearbody h; clear k. + apply isequiv_contr_map; intros b. + apply contr_inhabited_hprop. + 2:exact (g b). + apply hprop_allpath; intros [a p] [a' p']. + refine (path_sigma' _ (h a a' (p @ p'^)) _). + refine (transport_paths_Fl _ _ @ _). + refine ((inverse2 (hs a a' (p @ p'^)) @@ 1) @ _). + refine ((inv_pp p p'^ @@ 1) @ _). + refine (concat_pp_p _ _ _ @ _). + refine ((1 @@ concat_Vp _) @ _). + exact ((inv_V p' @@ 1) @ concat_p1 _). +Defined. + +Global Instance contr_pathsplit_isequiv + (n : nat) `(f : A -> B) `{IsEquiv _ _ f} +: Contr (PathSplit n f). +Proof. + generalize dependent B; revert A. + simple_induction n n IHn; intros A B f ?. + - exact _. + - apply contr_prod. +Defined. + +Global Instance ishprop_pathsplit (n : nat) `(f : A -> B) +: IsHProp (PathSplit n.+2 f). +Proof. + apply hprop_inhabited_contr; intros ps. + pose (isequiv_pathsplit n ps). + exact _. +Defined. + +Definition equiv_pathsplit_isequiv (n : nat) `(f : A -> B) +: PathSplit n.+2 f <~> IsEquiv f. +Proof. + refine (equiv_iff_hprop _ _). + - apply isequiv_pathsplit. + - intros ?; refine (center _). +Defined. + +(** Path-splitness transfers across commutative squares of equivalences. *) +Lemma equiv_functor_pathsplit (n : nat) {A B C D} + (f : A -> B) (g : C -> D) (h : A <~> C) (k : B <~> D) + (p : g o h == k o f) +: PathSplit n f <~> PathSplit n g. +Proof. + destruct n as [|n]. + 1:apply equiv_idmap. + destruct n as [|n]. + - simpl. + refine (_ *E equiv_contr_contr). + refine (equiv_functor_forall' k^-1 _); intros d. + unfold hfiber. + refine (equiv_functor_sigma' h _); intros a. + refine (equiv_concat_l (p a) d oE _). + simpl; apply equiv_moveR_equiv_M. + - refine (_ oE equiv_pathsplit_isequiv n f). + refine ((equiv_pathsplit_isequiv n g)^-1 oE _). + apply equiv_iff_hprop; intros e. + + refine (isequiv_commsq f g h k (fun a => (p a)^)). + + refine (isequiv_commsq' f g h k p). +Defined. + +(** A map is oo-path-split if it is n-path-split for all n. This is also equivalent to being an equivalence. *) + +Definition ooPathSplit `(f : A -> B) : Type + := forall n, PathSplit n f. + +Definition isequiv_oopathsplit `{f : A -> B} +: ooPathSplit f -> IsEquiv f + := fun ps => isequiv_pathsplit 0 (ps 2). + +Global Instance contr_oopathsplit_isequiv + `(f : A -> B) `{IsEquiv _ _ f} +: Contr (ooPathSplit f). +Proof. + apply contr_forall. +Defined. + +Global Instance ishprop_oopathsplit `(f : A -> B) +: IsHProp (ooPathSplit f). +Proof. + apply hprop_inhabited_contr; intros ps. + pose (isequiv_oopathsplit ps). + exact _. +Defined. + +Definition equiv_oopathsplit_isequiv `(f : A -> B) +: ooPathSplit f <~> IsEquiv f. +Proof. + refine (equiv_iff_hprop _ _). + - apply isequiv_oopathsplit. + - intros ?; refine (center _). +Defined. + +End AssumeFunext. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/PathSplit.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/PathSplit.vo new file mode 100644 index 0000000000000000000000000000000000000000..67615b10f4c1b63a5db0d92a74b8874c027c7c21 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/PathSplit.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/Relational.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/Relational.v new file mode 100644 index 0000000000000000000000000000000000000000..b5c75cec50ba9a8fd1ab3626ca04e771894683e4 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/Relational.v @@ -0,0 +1,68 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +Require Import HoTT.Basics HoTT.Types. + +Local Open Scope nat_scope. +Local Open Scope path_scope. + +Generalizable Variables A B f. + +(** * Relational equivalences *) + +(** This definition is due to Peter LeFanu Lumsdaine on the HoTT mailing list. This definition gives more judgmental properties, though has the downside of jumping universe levels. *) + +Record RelEquiv A B := + { equiv_rel : A -> B -> Type; + relequiv_contr_f : forall a, Contr { b : B & equiv_rel a b }; + relequiv_contr_g : forall b, Contr { a : A & equiv_rel a b } }. + +Arguments equiv_rel {A B} _ _ _. +Global Existing Instance relequiv_contr_f. +Global Existing Instance relequiv_contr_g. + +Definition issig_relequiv {A B} + : { equiv_rel : A -> B -> Type + | { f : forall a, Contr { b : B & equiv_rel a b } + | forall b, Contr { a : A & equiv_rel a b } } } + <~> RelEquiv A B. +Proof. + issig. +Defined. + +Definition relequiv_of_equiv {A B} (e : A <~> B) : RelEquiv A B. +Proof. + refine {| equiv_rel a b := e a = b |}. + (** The rest is found by typeclass inference! *) +Defined. + +Definition equiv_of_relequiv {A B} (e : RelEquiv A B) : A <~> B. +Proof. + refine (equiv_adjointify + (fun a => (center { b : B & equiv_rel e a b}).1) + (fun b => (center { a : A & equiv_rel e a b}).1) + _ _); + intro x; cbn. + { refine (ap pr1 (contr _) : _.1 = (x; _).1). + exact (center {a : A & equiv_rel e a x}).2. } + { refine (ap pr1 (contr _) : _.1 = (x; _).1). + exact (center {b : B & equiv_rel e x b}).2. } +Defined. + +Definition RelIsEquiv {A B} (f : A -> B) + := { r : RelEquiv A B | forall x, (center { b : B & equiv_rel r x b }).1 = f x }. + +(** TODO: Prove [ishprop_relisequiv `{Funext} {A B} f : IsHProp (@RelIsEquiv A B f)] *) + +(** * Judgmental property *) +Definition inverse_relequiv {A B} (e : RelEquiv A B) : RelEquiv B A + := {| equiv_rel a b := equiv_rel e b a |}. + +Definition reinv_V {A B} (e : RelEquiv A B) + : inverse_relequiv (inverse_relequiv e) = e + := 1. + +(** TODO: Is there a definition of this that makes [inverse_relequiv (relequiv_idmap A)] be [relequiv_idmap A], judgmentally? *) +Definition relequiv_idmap A : RelEquiv A A + := {| equiv_rel a b := a = b |}. + +(** TODO: Define composition; we probably need truncation to do this? *) diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/Relational.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/Relational.vo new file mode 100644 index 0000000000000000000000000000000000000000..ac02d14c554823dd9e24bdde941f5b3cd2e8e371 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/Relational.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Flattening.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Flattening.v new file mode 100644 index 0000000000000000000000000000000000000000..d9f41a8afe461c028cc734d99f30a97d77535aae --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Flattening.v @@ -0,0 +1,209 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +(** * The flattening lemma. *) + +Require Import HoTT.Basics. +Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe. +Local Open Scope path_scope. +Require Import HoTT.Colimits.Coeq. + +(** The base HIT [W] is just a homotopy coequalizer [Coeq]. *) + +(** TODO: Make the names in this file more usable, move it into [Coeq.v], and use it to derive corresponding flattening lemmas for [pushout], etc. *) + +(** Now we define the flattened HIT which will be equivalent to the total space of a fibration over [W]. *) + +Module Export FlattenedHIT. + +Private Inductive Wtil (A B : Type) (f g : B -> A) + (C : A -> Type) (D : forall b, C (f b) <~> C (g b)) + : Type := +| cct : forall a, C a -> Wtil A B f g C D. + +Arguments cct {A B f g C D} a c. + +Axiom ppt : forall {A B f g C D} (b:B) (y:C (f b)), + @cct A B f g C D (f b) y = cct (g b) (D b y). + +Definition Wtil_ind {A B f g C D} (Q : Wtil A B f g C D -> Type) + (cct' : forall a x, Q (cct a x)) + (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y)) + : forall w, Q w + := fun w => match w with cct a x => fun _ => cct' a x end ppt'. + +Axiom Wtil_ind_beta_ppt + : forall {A B f g C D} (Q : Wtil A B f g C D -> Type) + (cct' : forall a x, Q (cct a x)) + (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y)) + (b:B) (y : C (f b)), + apD (Wtil_ind Q cct' ppt') (ppt b y) = ppt' b y. + +End FlattenedHIT. + +Definition Wtil_rec {A B f g C} {D : forall b, C (f b) <~> C (g b)} + (Q : Type) (cct' : forall a (x : C a), Q) + (ppt' : forall b (y : C (f b)), cct' (f b) y = cct' (g b) (D b y)) + : Wtil A B f g C D -> Q + := Wtil_ind (fun _ => Q) cct' (fun b y => transport_const _ _ @ ppt' b y). + +Definition Wtil_rec_beta_ppt + {A B f g C} {D : forall b, C (f b) <~> C (g b)} + (Q : Type) (cct' : forall a (x : C a), Q) + (ppt' : forall (b:B) (y : C (f b)), cct' (f b) y = cct' (g b) (D b y)) + (b:B) (y: C (f b)) + : ap (@Wtil_rec A B f g C D Q cct' ppt') (ppt b y) = ppt' b y. +Proof. + unfold Wtil_rec. + eapply (cancelL (transport_const (ppt (C:=C) b y) _)). + refine ((apD_const + (@Wtil_ind A B f g C D (fun _ => Q) cct' _) (ppt b y))^ @ _). + refine (Wtil_ind_beta_ppt (fun _ => Q) _ _ _ _). +Defined. + + + +(** Now we define the fibration over it that we will be considering the total space of. *) + +Section AssumeAxioms. +Context `{Univalence}. + +Context {B A : Type} {f g : B -> A}. +Context {C : A -> Type} {D : forall b, C (f b) <~> C (g b)}. + +Let W' := Coeq f g. + +Let P : W' -> Type + := Coeq_rec Type C (fun b => path_universe (D b)). + + + +(** Now we give the total space the same structure as [Wtil]. *) + +Let sWtil := { w:W' & P w }. + +Let scct (a:A) (x:C a) : sWtil := (exist P (coeq a) x). + +Let sppt (b:B) (y:C (f b)) : scct (f b) y = scct (g b) (D b y) + := path_sigma' P (cglue b) + (transport_path_universe' P (cglue b) (D b) + (Coeq_rec_beta_cglue Type C (fun b0 => path_universe (D b0)) b) y). + +(** Here is the dependent eliminator *) +Definition sWtil_ind (Q : sWtil -> Type) + (scct' : forall a x, Q (scct a x)) + (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y)) + : forall w, Q w. +Proof. + apply sig_ind. + refine (Coeq_ind (fun w => forall x:P w, Q (w;x)) + (fun a x => scct' a x) _). + intros b. + apply (dpath_forall P (fun a b => Q (a;b)) _ _ (cglue b) + (scct' (f b)) (scct' (g b))). + intros y. + set (q := transport_path_universe' P (cglue b) (D b) + (Coeq_rec_beta_cglue Type C (fun b0 : B => path_universe (D b0)) b) y). + rewrite transportD_is_transport. + refine (_ @ apD (scct' (g b)) q^). + refine (moveL_transport_V (fun x => Q (scct (g b) x)) q _ _ _). + rewrite transport_compose, <- transport_pp. + refine (_ @ sppt' b y). + apply ap10, ap. + refine (whiskerL _ (ap_exist P (coeq (g b)) _ _ q) @ _). + exact ((path_sigma_p1_1p' _ _ _)^). +Defined. + +(** The eliminator computes on the point constructor. *) +Definition sWtil_ind_beta_cct (Q : sWtil -> Type) + (scct' : forall a x, Q (scct a x)) + (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y)) + (a:A) (x:C a) + : sWtil_ind Q scct' sppt' (scct a x) = scct' a x + := 1. + +(** This would be its propositional computation rule on the path constructor... *) +(** +<< +Definition sWtil_ind_beta_ppt (Q : sWtil -> Type) + (scct' : forall a x, Q (scct a x)) + (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y)) + (b:B) (y:C (f b)) + : apD (sWtil_ind Q scct' sppt') (sppt b y) = sppt' b y. +Proof. + unfold sWtil_ind. + (** ... but it's a doozy! *) +Abort. +>> +*) + +(** Fortunately, it turns out to be enough to have the computation rule for the *non-dependent* eliminator! *) + +(** We could define that in terms of the dependent one, as usual... +<< +Definition sWtil_rec (P : Type) + (scct' : forall a (x : C a), P) + (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y)) + : sWtil -> P + := sWtil_ind (fun _ => P) scct' (fun b y => transport_const _ _ @ sppt' b y). +>> +*) + +(** ...but if we define it diindly, then it's easier to reason about. *) +Definition sWtil_rec (Q : Type) + (scct' : forall a (x : C a), Q) + (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y)) + : sWtil -> Q. +Proof. + apply sig_ind. + refine (Coeq_ind (fun w => P w -> Q) (fun a x => scct' a x) _). + intros b. + refine (dpath_arrow P (fun _ => Q) _ _ _ _). + intros y. + refine (transport_const _ _ @ _). + refine (sppt' b _ @ ap _ _). + refine ((transport_path_universe' P (cglue b) (D b) _ _)^). + exact (Coeq_rec_beta_cglue _ _ _ _). +Defined. + +Open Scope long_path_scope. + +Definition sWtil_rec_beta_ppt (Q : Type) + (scct' : forall a (x : C a), Q) + (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y)) + (b:B) (y: C (f b)) + : ap (sWtil_rec Q scct' sppt') (sppt b y) = sppt' b y. +Proof. + unfold sWtil_rec, sppt. + refine (@ap_sig_rec_path_sigma W' P Q _ _ (cglue b) _ _ _ _ @ _); simpl. + rewrite (@Coeq_ind_beta_cglue B A f g). + rewrite (ap10_dpath_arrow P (fun _ => Q) (cglue b) _ _ _ y). + repeat rewrite concat_p_pp. + (** Now everything cancels! *) + rewrite ap_V, concat_pV_p, concat_pV_p, concat_pV_p, concat_Vp. + by apply concat_1p. +Qed. + +Close Scope long_path_scope. + +(** Woot! *) +Definition equiv_flattening : Wtil A B f g C D <~> sWtil. +Proof. + (** The maps back and forth are obtained easily from the non-dependent eliminators. *) + refine (equiv_adjointify + (Wtil_rec _ scct sppt) + (sWtil_rec _ cct ppt) + _ _). + (** The two homotopies are completely symmetrical, using the *dependent* eliminators, but only the computation rules for the non-dependent ones. *) + - refine (sWtil_ind _ (fun a x => 1) _). intros b y. + apply dpath_path_FFlr. + rewrite concat_1p, concat_p1. + rewrite sWtil_rec_beta_ppt. + by symmetry; apply (@Wtil_rec_beta_ppt A B f g C D). + - refine (Wtil_ind _ (fun a x => 1) _). intros b y. + apply dpath_path_FFlr. + rewrite concat_1p, concat_p1. + rewrite Wtil_rec_beta_ppt. + by symmetry; apply sWtil_rec_beta_ppt. +Defined. + +End AssumeAxioms. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.v new file mode 100644 index 0000000000000000000000000000000000000000..f80293dc40b43364009535453f8aa6a549d8d62b --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.v @@ -0,0 +1,102 @@ +(* -*- mode: coq; mode: visual-line -*- *) +Require Import HoTT.Basics HoTT.Types. +Require Import Spaces.Int Spaces.Circle. +Require Import Colimits.Coeq HIT.Flattening Truncations.Core Truncations.Connectedness. + +Local Open Scope path_scope. + +(** * Quotients by free actions of [Int] *) + +(** We will show that if [Int] acts freely on a set, then the set-quotient of that action can be defined without a 0-truncation, giving it a universal property for mapping into all types. *) + +Section FreeIntAction. + + Context `{Univalence}. + Context (R : Type) `{IsHSet R}. + + (** A free action by [Int] is the same as a single autoequivalence [f] (the action of [1]) whose iterates are all pointwise distinct. *) + Context (f : R <~> R) + (f_free : forall (r : R) (n m : Int), + (int_iter f n r = int_iter f m r) -> (n = m)). + + (** We can then define the quotient to be the coequalizer of [f] and the identity map. This gives it the desired universal property for all types; it remains to show that this definition gives a set. *) + Let RmodZ := Coeq f idmap. + + (** Together, [R] and [f] define a fibration over [Circle]. By the flattening lemma, its total space is equivalent to the quotient. *) + Global Instance isset_RmodZ : IsHSet RmodZ. + Proof. + nrefine (istrunc_equiv_istrunc + { z : Circle & Circle_rec Type R (path_universe f) z} + (_ oE (@equiv_flattening _ Unit Unit idmap idmap + (fun _ => R) (fun _ => f))^-1 + oE _)); + try exact _. + - unshelve rapply equiv_adjointify. + + simple refine (Wtil_rec _ _ _). + * intros u r; exact (coeq r). + * intros u r; cbn. exact ((cglue r)^). + + simple refine (Coeq_rec _ _ _). + * exact (cct tt). + * intros r; exact ((ppt tt r)^). + + refine (Coeq_ind _ (fun a => 1) _); cbn; intros b. + rewrite transport_paths_FlFr, concat_p1, ap_idmap. + apply moveR_Vp; rewrite concat_p1. + rewrite ap_compose. + rewrite (Coeq_rec_beta_cglue + (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) + (cct tt) (fun r => (ppt tt r)^) b). + rewrite ap_V; symmetry. + refine (inverse2 + (Wtil_rec_beta_ppt + RmodZ (unit_name (fun r => coeq r)) + (unit_name (fun r => (cglue r)^)) tt b) @ inv_V _). + + simple refine (Wtil_ind _ _ _); cbn. + { intros [] ?; reflexivity. } + intros [] r; cbn. + rewrite transport_paths_FlFr, concat_p1, ap_idmap. + apply moveR_Vp; rewrite concat_p1. + rewrite ap_compose. + refine (_ @ ap (ap _) (Wtil_rec_beta_ppt + RmodZ (unit_name (fun r => coeq r)) + (unit_name (fun r => (cglue r)^)) tt r)^). + rewrite ap_V. + rewrite (Coeq_rec_beta_cglue + (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f)) + (cct tt) (fun r0 : R => (ppt tt r0)^) r). + symmetry; apply inv_V. + - apply equiv_functor_sigma_id; intros x. + apply equiv_path. + revert x; refine (Circle_ind _ 1 _); cbn. + rewrite transport_paths_FlFr, concat_p1. + apply moveR_Vp; rewrite concat_p1. + rewrite Circle_rec_beta_loop. + unfold loop. + exact (Coeq_rec_beta_cglue _ _ _ _). + - apply istrunc_S. + intros xu yv. + nrefine (istrunc_equiv_istrunc (n := -1) _ (equiv_path_sigma _ xu yv)). + destruct xu as [x u], yv as [y v]; cbn. + apply hprop_allpath. + intros [p r] [q s]. + set (P := Circle_rec Type R (path_universe f)) in *. + assert (forall z, IsHSet (P z)). + { simple refine (Circle_ind _ _ _); cbn beta. + - exact _. + - apply path_ishprop. } + apply path_sigma_hprop; cbn. + assert (t := r @ s^); clear r s. + assert (xb := merely_path_is0connected Circle base x). + assert (yb := merely_path_is0connected Circle base y). + strip_truncations. destruct xb, yb. + revert p q t. + equiv_intro (equiv_loopCircle_int^-1) n. + equiv_intro (equiv_loopCircle_int^-1) m. + subst P. + rewrite !Circle_action_is_iter. + intros p. apply ap. + exact (f_free u n m p). + Qed. + + (** TODO: Prove that this [RmodZ] is equivalent to the set-quotient of [R] by a suitably defined equivalence relation. *) + +End FreeIntAction. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.vo new file mode 100644 index 0000000000000000000000000000000000000000..eaa027160dc022e696e5a3b66bda7daef00ebd50 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Interval.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Interval.v new file mode 100644 index 0000000000000000000000000000000000000000..195e1c666753b63deac91e20a711b0960d65027f --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Interval.v @@ -0,0 +1,52 @@ +(* -*- mode: coq; mode: visual-line -*- *) + +(** * Theorems about the homotopical interval. *) + +Require Import Basics.Overture Basics.PathGroupoids. +Require Import Types.Paths. + +Local Open Scope path_scope. + + +Module Export Interval. + +Private Inductive interval : Type0 := + | zero : interval + | one : interval. + +Axiom seg : zero = one. + +Definition interval_ind (P : interval -> Type) + (a : P zero) (b : P one) (p : seg # a = b) + : forall x:interval, P x + := fun x => (match x return _ -> P x with + | zero => fun _ => a + | one => fun _ => b + end) p. + +Axiom interval_ind_beta_seg : forall (P : interval -> Type) + (a : P zero) (b : P one) (p : seg # a = b), + apD (interval_ind P a b p) seg = p. + +End Interval. + +Definition interval_rec (P : Type) (a b : P) (p : a = b) + : interval -> P + := interval_ind (fun _ => P) a b (transport_const _ _ @ p). + +Definition interval_rec_beta_seg (P : Type) (a b : P) (p : a = b) + : ap (interval_rec P a b p) seg = p. +Proof. + refine (cancelL (transport_const seg a) _ _ _). + refine ((apD_const (interval_ind (fun _ => P) a b _) seg)^ @ _). + refine (interval_ind_beta_seg (fun _ => P) _ _ _). +Defined. + +(** ** The interval is contractible. *) + +Global Instance contr_interval : Contr interval | 0. +Proof. + apply (Build_Contr _ zero). + refine (interval_ind _ 1 seg _). + refine (transport_paths_r _ _ @ concat_1p _). +Defined. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Interval.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Interval.vo new file mode 100644 index 0000000000000000000000000000000000000000..b89df7261d17711efe55c282e3f681984d01b8d2 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Interval.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/SetCone.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/SetCone.v new file mode 100644 index 0000000000000000000000000000000000000000..5c787a7fe69a2f0e6257c9021df8601ea4461377 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/SetCone.v @@ -0,0 +1,16 @@ +(* -*- mode: coq; mode: visual-line -*- *) +Require Import HoTT.Basics Types.Unit. +Require Import Colimits.Pushout. +Require Import Truncations.Core. + +(** * Cones of HSets *) + +Section SetCone. + Context {A B : HSet} (f : A -> B). + + Definition setcone := Trunc 0 (Pushout@{_ _ Set _} f (const_tt A)). + + Global Instance istrunc_setcone : IsHSet setcone := _. + + Definition setcone_point : setcone := tr (push (inr tt)). +End SetCone. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/SetCone.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/SetCone.vo new file mode 100644 index 0000000000000000000000000000000000000000..dc1edc968b63dca23c6188ebde229c0ee3149058 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/SetCone.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/epi.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/epi.v new file mode 100644 index 0000000000000000000000000000000000000000..ac4e2684f3c99e7d7f3748251dbd65705952a0bf --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/epi.v @@ -0,0 +1,182 @@ +Require Import Basics. +Require Import Types. +Require Import TruncType. +Require Import ReflectiveSubuniverse. +Require Import Colimits.Pushout Truncations.Core HIT.SetCone. + +Local Open Scope path_scope. + +Section AssumingUA. +Context `{ua:Univalence}. + +(** We will now prove that for sets, epis and surjections are equivalent.*) +Definition isepi {X Y} `(f:X->Y) := forall Z: HSet, + forall g h: Y -> Z, g o f = h o f -> g = h. + +Definition isepi_funext {X Y : Type} (f : X -> Y) + := forall Z : HSet, forall g0 g1 : Y -> Z, g0 o f == g1 o f -> g0 == g1. + +Definition isepi' {X Y} `(f : X -> Y) := + forall (Z : HSet) (g : Y -> Z), Contr { h : Y -> Z | g o f = h o f }. + +Lemma equiv_isepi_isepi' {X Y} f : @isepi X Y f <~> @isepi' X Y f. +Proof. + unfold isepi, isepi'. + apply (@equiv_functor_forall' _ _ _ _ _ (equiv_idmap _)); intro Z. + apply (@equiv_functor_forall' _ _ _ _ _ (equiv_idmap _)); intro g. + unfold equiv_idmap; simpl. + refine (transitivity (@equiv_sig_ind _ (fun h : Y -> Z => g o f = h o f) (fun h => g = h.1)) _). + (** TODO(JasonGross): Can we do this entirely by chaining equivalences? *) + apply equiv_iff_hprop. + { intro hepi. + nrapply (Build_Contr _ (g; idpath)). + intro xy; specialize (hepi xy). + apply path_sigma_uncurried. + exists hepi. + apply path_ishprop. } + { intros hepi xy. + exact (ap pr1 ((contr (g; 1))^ @ contr xy)). } +Defined. + +Definition equiv_isepi_isepi_funext {X Y : Type} (f : X -> Y) + : isepi f <~> isepi_funext f. +Proof. + apply equiv_iff_hprop. + - intros e ? g0 g1 h. + apply equiv_path_arrow. + apply e. + by apply path_arrow. + - intros e ? g0 g1 p. + apply path_arrow. + apply e. + by apply equiv_path_arrow. +Defined. + +Section cones. + Lemma isepi'_contr_cone `{Funext} {A B : HSet} (f : A -> B) : isepi' f -> Contr (setcone f). + Proof. + intros hepi. + apply (Build_Contr _ (setcone_point _)). + pose (alpha1 := @pglue A B Unit f (const_tt _)). + pose (tot:= { h : B -> setcone f & tr o push o inl o f = h o f }). + transparent assert (l : tot). + { simple refine (tr o _ o inl; _). + { refine push. } + { refine idpath. } } + pose (r := (@const B (setcone f) (setcone_point _); (ap (fun f => @tr 0 _ o f) (path_forall _ _ alpha1))) : tot). + subst tot. + assert (X : l = r). + { let lem := constr:(fun X push' => hepi (Build_HSet (setcone f)) (tr o push' o @inl _ X)) in + pose (lem _ push). + refine (path_contr l r). } + subst l r. + + pose (I0 b := ap10 (X ..1) b). + refine (Trunc_ind _ _). + pose (fun a : B + Unit => (match a as a return setcone_point _ = tr (push a) with + | inl a' => (I0 a')^ + | inr tt => idpath + end)) as I0f. + refine (Pushout_ind _ (fun a' => I0f (inl a')) (fun u => (I0f (inr u))) _). + + simpl. subst alpha1. intros. + unfold setcone_point. + subst I0. simpl. + pose (X..2) as p. simpl in p. + rewrite (transport_precompose f _ _ X..1) in p. + assert (H':=concat (ap (fun x => ap10 x a) p) (ap10_ap_postcompose tr (path_arrow (pushl o f) (pushr o const_tt _) pglue) _)). + rewrite ap10_path_arrow in H'. + clear p. + (** Apparently [pose; clearbody] is only ~.8 seconds, while [pose proof] is ~4 seconds? *) + pose (concat (ap10_ap_precompose f (X ..1) a)^ H') as p. + clearbody p. + simpl in p. + rewrite p. + rewrite transport_paths_Fr. + apply concat_Vp. + Qed. +End cones. + +Lemma issurj_isepi {X Y} (f:X->Y): IsSurjection f -> isepi f. +Proof. +intros sur ? ? ? ep. apply path_forall. intro y. +specialize (sur y). pose (center (merely (hfiber f y))). +apply (Trunc_rec (n:=-1) (A:=(sig (fun x : X => f x = y)))); + try assumption. +intros [x p]. set (p0:=apD10 ep x). +transitivity (g (f x)). +- by apply ap. +- transitivity (h (f x));auto with path_hints. by apply ap. +Qed. + +Corollary issurj_isepi_funext {X Y} (f:X->Y) : IsSurjection f -> isepi_funext f. +Proof. + intro s. + apply equiv_isepi_isepi_funext. + by apply issurj_isepi. +Defined. + +(** Old-style proof using polymorphic Omega. Needs resizing for the isepi proof to live in the + same universe as X and Y (the Z quantifier is instantiated with an HSet at a level higher) +<< +Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> issurj f. +Proof. + intros epif y. + set (g :=fun _:Y => Unit_hp). + set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))). + assert (X1: g o f = h o f ). + - apply path_forall. intro x. apply path_equiv_biimp_rec;[|done]. + intros _ . apply min1. exists tt. by (exists x). + - specialize (epif _ g h). + specialize (epif X1). clear X1. + set (p:=apD10 epif y). + apply (@minus1Trunc_map (sig (fun _ : Unit => sig (fun x : X => y = f x)))). + + intros [ _ [x eq]]. + exists x. + by symmetry. + + apply (transport hproptype p tt). +Defined. +>> +*) + +Section isepi_issurj. + Context {X Y : HSet} (f : X -> Y) (Hisepi : isepi f). + Definition epif := equiv_isepi_isepi' _ Hisepi. + Definition fam (c : setcone f) : HProp. + Proof. + pose (fib y := hexists (fun x : X => f x = y)). + apply (fun f => @Trunc_rec _ _ HProp _ f c). + refine (Pushout_rec HProp fib (fun _ => Unit_hp) (fun x => _)). + (** Prove that the truncated sigma is equivalent to Unit *) + pose (contr_inhabited_hprop (fib (f x)) (tr (x; idpath))) as i. + apply path_hprop. simpl. simpl in i. + apply (equiv_contr_unit). + Defined. + + Lemma isepi_issurj : IsSurjection f. + Proof. + intros y. + pose (i := isepi'_contr_cone _ epif). + + assert (X0 : forall x : setcone f, fam x = fam (setcone_point f)). + { intros. apply contr_dom_equiv. apply i. } + specialize (X0 (tr (push (inl y)))). simpl in X0. + unfold IsConnected. + refine (transport (fun A => Contr A) (ap trunctype_type X0)^ _); exact _. + Defined. +End isepi_issurj. + +Lemma isepi_isequiv X Y (f : X -> Y) `{IsEquiv _ _ f} +: isepi f. +Proof. + intros ? g h H'. + apply ap10 in H'. + apply path_forall. + intro x. + transitivity (g (f (f^-1 x))). + - by rewrite eisretr. + - transitivity (h (f (f^-1 x))). + * apply H'. + * by rewrite eisretr. +Qed. +End AssumingUA. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/epi.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/epi.vo new file mode 100644 index 0000000000000000000000000000000000000000..0e5fbb8c625f69e1cd8748ac5033d256bec5059a Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/epi.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/iso.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/iso.v new file mode 100644 index 0000000000000000000000000000000000000000..090eb2abc6a43c5e1cf48160908a5cc134e19345 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/iso.v @@ -0,0 +1,41 @@ +Require Import HoTT.Basics. +Require Import Types.Universe. +Require Import HSet. +Require Import HIT.epi HIT.unique_choice. + +Local Open Scope path_scope. + +(** We prove that [epi + mono <-> IsEquiv] *) +Section iso. + Context `{Univalence}. + Variables X Y : HSet. + Variable f : X -> Y. + + Lemma atmost1P_isinj (injf : isinj f) + : forall y : Y, atmost1P (fun x => f x = y). + Proof. + unfold isinj, atmost1P in *. + intros. + apply injf. + path_induction. + reflexivity. + Defined. + + Definition isequiv_isepi_ismono (epif : isepi f) (monof : ismono f) + : IsEquiv f. + Proof. + pose proof (@isepi_issurj _ _ _ f epif) as surjf. + pose proof (isinj_ismono _ monof) as injf. + pose proof (unique_choice + (fun y x => f x = y) + _ + (fun y => (@center _ (surjf y), atmost1P_isinj injf y))) + as H_unique_choice. + apply (isequiv_adjointify _ H_unique_choice.1). + - intro. + apply H_unique_choice.2. + - intro. + apply injf. + apply H_unique_choice.2. + Defined. +End iso. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/iso.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/iso.vo new file mode 100644 index 0000000000000000000000000000000000000000..d5c1ac7be7f90949a722443d0f7d1b43d23e99fb Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/iso.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/quotient.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/quotient.v new file mode 100644 index 0000000000000000000000000000000000000000..428e05ffc5039f925b3e65d8fb8728d60d72a62c --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/quotient.v @@ -0,0 +1,328 @@ +(* -*- mode: coq; mode: visual-line -*- *) +Require Import HoTT.Basics HoTT.Types. +Require Import HSet TruncType. +Require Import Truncations.Core. + +Local Open Scope path_scope. + +(** * The set-quotient of a type by an hprop-valued relation + +We aim to model: +<< +Inductive quotient : Type := + | class_of : A -> quotient + | related_classes_eq : forall x y, (R x y), class_of x = class_of y + | quotient_set : IsHSet quotient +>> +*) + +(** TODO: This development should be further connected with the sections in the book; see below. And it should be merged with Colimits.Quotient. Currently this file is only used in Classes/implementations/natpair_integers.v and Classes/implementations/field_of_fractions.v, so it shouldn't be too hard to switch to Colimits.Quotient. *) + +Module Export Quotient. + + Section Domain. + + Universes i j u. + Constraint i <= u, j <= u. + + Context {A : Type@{i}} (R : Relation@{i j} A) {sR: is_mere_relation _ R}. + + (** We choose to let the definition of quotient depend on the proof that [R] is a set-relations. Alternatively, we could have defined it for all relations and only develop the theory for set-relations. The former seems more natural. + +We do not require [R] to be an equivalence relation, but implicitly consider its transitive-reflexive closure. *) + + (** This definition has a parameter [sR] that shadows the ambient one in the Context in order to ensure that it actually ends up depending on everything in the Context when the section is closed, since its definition doesn't actually refer to any of them. *) + Private Inductive quotient {sR: is_mere_relation _ R} : Type@{u} := + | class_of : A -> quotient. + + (** The path constructors. *) + Axiom related_classes_eq + : forall {x y : A}, R x y -> + class_of x = class_of y. + + Axiom quotient_set : IsHSet (@quotient sR). + Global Existing Instance quotient_set. + + Definition quotient_ind (P : (@quotient sR) -> Type) {sP : forall x, IsHSet (P x)} + (dclass : forall x, P (class_of x)) + (dequiv : (forall x y (H : R x y), (related_classes_eq H) # (dclass x) = dclass y)) + : forall q, P q + := fun q => match q with class_of a => fun _ _ => dclass a end sP dequiv. + + Definition quotient_ind_compute {P sP} dclass dequiv x + : @quotient_ind P sP dclass dequiv (class_of x) = dclass x. + Proof. + reflexivity. + Defined. + + (** Again equality of paths needs to be postulated *) + Axiom quotient_ind_compute_path + : forall P sP dclass dequiv, + forall x y (H : R x y), + apD (@quotient_ind P sP dclass dequiv) (related_classes_eq H) + = dequiv x y H. + + End Domain. + +End Quotient. + +Section Equiv. + + Context `{Univalence}. + + Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R} + {Htrans : Transitive R} {Hsymm : Symmetric R}. + + Lemma quotient_path2 : forall {x y : quotient R} (p q : x=y), p=q. + Proof. + apply @hset_path2. apply _. + Defined. + + Definition in_class : quotient R -> A -> HProp. + Proof. + refine (quotient_ind R (fun _ => A -> HProp) (fun a b => Build_HProp (R a b)) _). + intros. eapply concat;[apply transport_const|]. + apply path_forall. intro z. apply path_hprop; simpl. + apply @equiv_iff_hprop; eauto. + Defined. + + Context {Hrefl : Reflexive R}. + + Lemma in_class_pr : forall x y, (in_class (class_of R x) y : Type) = R x y. + Proof. + reflexivity. + Defined. + + Lemma quotient_ind_prop (P : quotient R -> Type) + `{forall x, IsHProp (P x)} : + forall dclass : forall x, P (class_of R x), + forall q, P q. + Proof. + intros. apply (quotient_ind R P dclass). + intros. apply path_ishprop. + Defined. + + Global Instance decidable_in_class `{forall x y, Decidable (R x y)} + : forall x a, Decidable (in_class x a). + Proof. + refine (quotient_ind_prop _ _). + intros a b; exact (transport Decidable (in_class_pr a b) _). + Defined. + + Lemma class_of_repr : forall q x, in_class q x -> q = class_of R x. + Proof. + apply (quotient_ind R + (fun q : quotient R => forall x, in_class q x -> q = class_of _ x) + (fun x y H => related_classes_eq R H)). + intros. + apply path_forall. intro z. + apply path_forall;intro H'. + apply quotient_path2. + Defined. + + Lemma classes_eq_related : forall x y, + class_of R x = class_of R y -> R x y. + Proof. + intros x y H'. + pattern (R x y). + eapply transport. + - apply in_class_pr. + - pattern (class_of R x). apply (transport _ (H'^)). + apply Hrefl. + Defined. + + (** Thm 10.1.8 *) + Theorem sets_exact : forall x y, (class_of R x = class_of R y) <~> R x y. + intros ??. apply equiv_iff_hprop. + - apply classes_eq_related. + - apply related_classes_eq. + Defined. + + Definition quotient_rec {B : Type} {sB : IsHSet B} + (dclass : (forall x : A, B)) + (dequiv : (forall x y, R x y -> dclass x = dclass y)) + : quotient R -> B. + Proof. + apply (quotient_ind R (fun _ : quotient _ => B)) with dclass. + intros ?? H'. destruct (related_classes_eq R H'). by apply dequiv. + Defined. + + Definition quotient_rec2 {B : HSet} {dclass : (A -> A -> B)}: + forall dequiv : (forall x x', R x x' -> forall y y', R y y' -> + dclass x y = dclass x' y'), + quotient R -> quotient R -> B. + Proof. + intro. + assert (dequiv0 : forall x x0 y : A, R x0 y -> dclass x x0 = dclass x y) + by (intros ? ? ? Hx; apply dequiv;[apply Hrefl|done]). + refine (quotient_rec + (fun x => quotient_rec (dclass x) (dequiv0 x)) _). + intros x x' Hx. + apply path_forall. red. + assert (dequiv1 : forall y : A, + quotient_rec (dclass x) (dequiv0 x) (class_of _ y) = + quotient_rec (dclass x') (dequiv0 x') (class_of _ y)) + by (intros; by apply dequiv). + refine (quotient_ind R (fun q => + quotient_rec (dclass x) (dequiv0 x) q = + quotient_rec (dclass x') (dequiv0 x') q) dequiv1 _). + intros. apply path_ishprop. + Defined. + + Definition quotient_ind_prop' : forall P : quotient R -> Type, + forall (Hprop' : forall x, IsHProp (P (class_of _ x))), + (forall x, P (class_of _ x)) -> forall y, P y. + Proof. + intros ? ? dclass. apply quotient_ind with dclass. + - simple refine (quotient_ind R (fun x => IsHSet (P x)) _ _); cbn beta; try exact _. + intros; apply path_ishprop. + - intros. apply path_ishprop. + Defined. + + (** From Ch6 *) + Theorem quotient_surjective: IsSurjection (class_of R). + Proof. + apply BuildIsSurjection. + apply (quotient_ind_prop (fun y => merely (hfiber (class_of R) y))); try exact _. + intro x. apply tr. by exists x. + Defined. + + (** From Ch10 *) + Definition quotient_ump' (B:HSet): (quotient R -> B) -> + (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))). + intro f. exists (compose f (class_of R) ). + intros. f_ap. by apply related_classes_eq. + Defined. + + Definition quotient_ump'' (B:HSet): (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))) + -> quotient R -> B. + intros [f H']. + apply (quotient_rec _ H'). + Defined. + + Theorem quotient_ump (B:HSet): (quotient R -> B) <~> + (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))). + Proof. + refine (equiv_adjointify (quotient_ump' B) (quotient_ump'' B) _ _). + - intros [f Hf]. + by apply equiv_path_sigma_hprop. + - intros f. + apply path_forall. + red. apply quotient_ind_prop';[apply _|reflexivity]. + Defined. + + (** Missing + + The equivalence with VVquotient [A//R]. + + This should lead to the unnamed theorem: + + 10.1.10. Equivalence relations are effective and there is an equivalence [A/R<~>A//R]. *) + + (** + The theory of canonical quotients is developed by C.Cohen: + http://perso.crans.org/cohen/work/quotients/ + *) + +End Equiv. + +Section Functoriality. + + Definition quotient_functor + {A : Type} (R : Relation A) {sR: is_mere_relation _ R} + {B : Type} (S : Relation B) {sS: is_mere_relation _ S} + (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y)) + : quotient R -> quotient S. + Proof. + refine (quotient_rec R (class_of S o f) _). + intros x y r. + apply related_classes_eq, fresp, r. + Defined. + + Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R} + {B : Type} (S : Relation B) {sS: is_mere_relation _ S}. + + Global Instance quotient_functor_isequiv + (f : A -> B) (fresp : forall x y, R x y <-> S (f x) (f y)) + `{IsEquiv _ _ f} + : IsEquiv (quotient_functor R S f (fun x y => fst (fresp x y))). + Proof. + simple refine (isequiv_adjointify _ (quotient_functor S R f^-1 _) + _ _). + - intros u v s. + apply (snd (fresp _ _)). + abstract (do 2 rewrite eisretr; apply s). + - intros x; revert x; simple refine (quotient_ind S _ _ _). + + intros b; simpl. apply ap, eisretr. + + intros; apply path_ishprop. + - intros x; revert x; simple refine (quotient_ind R _ _ _). + + intros a; simpl. apply ap, eissect. + + intros; apply path_ishprop. + Defined. + + Definition quotient_functor_equiv + (f : A -> B) (fresp : forall x y, R x y <-> S (f x) (f y)) + `{IsEquiv _ _ f} + : quotient R <~> quotient S + := Build_Equiv _ _ + (quotient_functor R S f (fun x y => fst (fresp x y))) _. + + Definition quotient_functor_equiv' + (f : A <~> B) (fresp : forall x y, R x y <-> S (f x) (f y)) + : quotient R <~> quotient S + := quotient_functor_equiv f fresp. + +End Functoriality. + +Section Kernel. + + (** ** Quotients of kernels of maps to sets give a surjection/mono factorization. *) + + Context {fs : Funext}. + + (** A function we want to factor. *) + Context {A B : Type} `{IsHSet B} (f : A -> B). + + (** A mere relation equivalent to its kernel. *) + Context (R : Relation A) {sR : is_mere_relation _ R}. + Context (is_ker : forall x y, f x = f y <~> R x y). + + Theorem quotient_kernel_factor + : exists (C : Type) (e : A -> C) (m : C -> B), + IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e). + Proof. + pose (C := quotient R). + (* We put this explicitly in the context so that typeclass resolution will pick it up. *) + assert (IsHSet C) by (unfold C; apply _). + exists C. + pose (e := class_of R). + exists e. + transparent assert (m : (C -> B)). + { apply quotient_ind with f; try exact _. + intros x y H. transitivity (f x). + - apply transport_const. + - exact ((is_ker x y) ^-1 H). } + exists m. + split;[split;[split|]|]. + - assumption. + - apply quotient_surjective. + - intro u. + apply hprop_allpath. + assert (H : forall (x y : C) (p : m x = u) (p' : m y = u), x = y). + { simple refine (quotient_ind R _ _ _). + - intro a. + simple refine (quotient_ind R _ _ _). + + intros a' p p'; fold e in p, p'. + * apply related_classes_eq. + refine (is_ker a a' _). + change (m (e a) = m (e a')). + exact (p @ p'^). + + intros; apply path_ishprop. + - intros; apply path_ishprop. } + intros [x p] [y p']. + apply path_sigma_hprop; simpl. + exact (H x y p p'). + - reflexivity. + Defined. + +End Kernel. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/surjective_factor.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/surjective_factor.v new file mode 100644 index 0000000000000000000000000000000000000000..21c46c02112dd921654e354cc95ba405a9fc6ea7 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/surjective_factor.v @@ -0,0 +1,37 @@ +Require Import + HoTT.Types + HoTT.Basics + HoTT.Truncations.Core Modalities.Modality. + +(** Definition by factoring through a surjection. *) + +Section surjective_factor. + Context `{Funext}. + Context {A B C} `{IsHSet C} `(f : A -> C) `(g : A -> B) {Esurj : IsSurjection g}. + Variable (Eg : forall x y, g x = g y -> f x = f y). + + Lemma ishprop_surjective_factor_aux : forall b, IsHProp (exists c : C, forall a, g a = b -> f a = c). + Proof. + intros. apply Sigma.ishprop_sigma_disjoint. + intros c1 c2 E1 E2. + generalize (@center _ (Esurj b)); apply (Trunc_ind _). + intros [a p];destruct p. + path_via (f a). + Qed. + + Definition surjective_factor_aux := + @conn_map_elim + _ _ _ _ Esurj (fun b => exists c : C, forall a, g a = b -> f a = c) + ishprop_surjective_factor_aux + (fun a => exist (fun c => forall a, _ -> _ = c) (f a) (fun a' => Eg a' a)). + + Definition surjective_factor : B -> C + := fun b => (surjective_factor_aux b).1. + + Lemma surjective_factor_pr : f == compose surjective_factor g. + Proof. + intros a. + apply (surjective_factor_aux (g a)).2. trivial. + Qed. + +End surjective_factor. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/surjective_factor.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/surjective_factor.vo new file mode 100644 index 0000000000000000000000000000000000000000..1113e486592ab9fccc19c166f035091740024fbe Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/surjective_factor.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/unique_choice.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/unique_choice.v new file mode 100644 index 0000000000000000000000000000000000000000..08dad3ca89d23326d94823a16152eb7aa5ff6cef --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/unique_choice.v @@ -0,0 +1,31 @@ +Require Import HoTT.Basics HoTT.Truncations.Core. + +Definition atmost1 X:=(forall x1 x2:X, (x1 = x2)). +Definition atmost1P {X} (P:X->Type):= + (forall x1 x2:X, P x1 -> P x2 -> (x1 = x2)). +Definition hunique {X} (P:X->Type):=(hexists P) * (atmost1P P). + +Lemma atmost {X} {P : X -> Type}: + (forall x, IsHProp (P x)) -> (atmost1P P) -> atmost1 (sig P). +intros H H0 [x p] [y q]. +specialize (H0 x y p q). +induction H0. +assert (H0: (p =q)) by apply path_ishprop. +now induction H0. +Qed. + +Lemma iota {X} (P:X-> Type): + (forall x, IsHProp (P x)) -> (hunique P) -> sig P. +Proof. +intros H1 [H H0]. +apply (@Trunc_rec (-1) (sig P) );auto. +by apply hprop_allpath, atmost. +Qed. + +Lemma unique_choice {X Y} (R:X->Y->Type) : + (forall x y, IsHProp (R x y)) -> (forall x, (hunique (R x))) + -> {f : X -> Y & forall x, (R x (f x))}. +intros X0 X1. +exists (fun x:X => (pr1 (iota _ (X0 x) (X1 x)))). +intro x. apply (pr2 (iota _ (X0 x) (X1 x))). +Qed. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/unique_choice.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/unique_choice.vo new file mode 100644 index 0000000000000000000000000000000000000000..4a5d0d14a99e389f17cb47f6d1c6685bf89a88b3 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/unique_choice.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pFiber.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pFiber.vo new file mode 100644 index 0000000000000000000000000000000000000000..ab9a1e4ed3d9e1c22f18cf2f6031bc87deb9abe5 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pFiber.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:f24569b0e96de2846b8733568c9546aed28b23136c49dfc7e0abf14fbc7c4af2 +size 199966 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pMap.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pMap.vo new file mode 100644 index 0000000000000000000000000000000000000000..e7f3a59257d6c9935385b48a92f94ccfd33125e2 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pMap.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:c1d5a4c5f776b9c8bce55f80839cbe0fa73869130a2c443e987ea1a7f89646a9 +size 391923 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.v new file mode 100644 index 0000000000000000000000000000000000000000..a6adf27ff38827a3dab6397dca8dfb1cd02319d1 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.v @@ -0,0 +1,445 @@ +(* -*- mode: coq; mode: visual-line -*- *) +Require Import HoTT.Basics HoTT.Types. +Require Import Constant. +Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness. +Require Import Spaces.BAut. +Require Import Pointed.Core. + +Local Open Scope trunc_scope. +Local Open Scope path_scope. +Local Open Scope pointed_scope. + +(** * BAut(Bool) *) + +Section AssumeUnivalence. + Context `{Univalence}. + + (** ** Nontrivial central homotopy *) + + (** The equivalence [Bool <~> (Bool <~> Bool)], and particularly its consequence [abelian_aut_bool], implies that [BAut Bool] has a nontrivial center. *) + + Definition negb_center_baut_bool + : forall (Z:BAut Bool), Z = Z. + Proof. + apply center_baut; try exact _. + exists equiv_negb. + intros g; apply abelian_aut_bool. + Defined. + + Definition nontrivial_negb_center_baut_bool + : negb_center_baut_bool <> (fun Z => idpath Z). + Proof. + intros oops. + pose (p := ap10_equiv + ((ap (center_baut Bool))^-1 + (oops @ (id_center_baut Bool)^))..1 true). + exact (false_ne_true p). + Defined. + + (** In particular, every element of [BAut Bool] has a canonical flip automorphism. *) + Definition negb_baut_bool (Z : BAut Bool) : Z <~> Z + := equiv_path Z Z (negb_center_baut_bool Z)..1. + + Definition negb_baut_bool_ne_idmap (Z : BAut Bool) + : negb_baut_bool Z <> equiv_idmap Z. + Proof. + intros oops. + apply nontrivial_negb_center_baut_bool. + apply path_forall; intros Z'. + pose (p := merely_path_component Z Z'). + clearbody p. strip_truncations. + destruct p. + unfold negb_baut_bool in oops. + apply moveL_equiv_V in oops. + refine (_ @ ap (equiv_path_sigma_hprop _ _) + (oops @ path_universe_1) @ _). + - symmetry. + refine (eisretr (equiv_path_sigma_hprop Z Z) _). + - apply moveR_equiv_M; reflexivity. + Defined. + + (** If [Z] is [Bool], then the flip is the usual one. *) + Definition negb_baut_bool_bool_negb + : negb_baut_bool pt = equiv_negb. + Proof. + pose (c := aut_bool_idmap_or_negb (negb_baut_bool pt)). + destruct c. + - pose (negb_baut_bool_ne_idmap pt p). + contradiction. + - assumption. + Defined. + + Definition ap_pr1_negb_baut_bool_bool + : (negb_center_baut_bool pt)..1 = path_universe negb. + Proof. + apply moveL_equiv_V. + apply negb_baut_bool_bool_negb. + Defined. + + (** Moreover, we can show that every automorphism of a [Z : BAut Bool] must be either the flip or the identity. *) + Definition aut_baut_bool_idmap_or_negb (Z : BAut Bool) (e : Z <~> Z) + : (e = equiv_idmap Z) + (e = negb_baut_bool Z). + Proof. + assert (IsHProp ((e = equiv_idmap Z) + (e = negb_baut_bool Z))). + { apply ishprop_sum; try exact _. + intros p q; exact (negb_baut_bool_ne_idmap Z (q^ @ p)). } + baut_reduce. + case (aut_bool_idmap_or_negb e). + - intros p; exact (inl p). + - intros q; apply inr. + exact (q @ negb_baut_bool_bool_negb^). + Defined. + + (** ** Connectedness *) + + Global Instance isminusoneconnected_baut_bool `{Funext} (Z : BAut Bool) + : IsConnected (-1) Z. + Proof. + baut_reduce. + apply contr_inhabited_hprop; try exact _. + exact (tr true). + Defined. + + Definition merely_inhab_baut_bool `{Funext} (Z : BAut Bool) + : merely Z + := center (merely Z). + + (** ** Equivalence types *) + + (** As soon as an element of [BAut Bool] is inhabited, it is (purely) equivalent to [Bool]. (Of course, every element of [BAut Bool] is *merely* inhabited, since [Bool] is.) In fact, it is equivalent in two canonical ways. + +First we define the function that will be the equivalence. *) + Definition inhab_baut_bool_from_bool (t : Bool) + (Z : BAut Bool) (z : Z) + : Bool -> Z + := fun b => if t then + if b then z else negb_baut_bool Z z + else + if b then negb_baut_bool Z z else z. + + (** We compute this in the case when [Z] is [Bool]. *) + Definition inhab_baut_bool_from_bool_bool (t : Bool) + : inhab_baut_bool_from_bool t pt = + fun (z : point (BAut Bool)) (b : Bool) => + if t then + if b then z else negb z + else + if b then negb z else z. + Proof. + apply path_forall; intros z'; simpl in z'. + apply path_forall; intros b. + destruct z', b, t; simpl; + try reflexivity; + try apply (ap10_equiv negb_baut_bool_bool_negb). + Defined. + + (** Now we show that it is an equivalence. *) + Global Instance isequiv_inhab_baut_bool_from_bool (t : Bool) + (Z : BAut Bool) (z : Z) + : IsEquiv (inhab_baut_bool_from_bool t Z z). + Proof. + baut_reduce. + refine (transport IsEquiv (ap10 (inhab_baut_bool_from_bool_bool t)^ z) _). + simpl in z; destruct z, t; simpl. + - refine (isequiv_homotopic idmap _); intros []; reflexivity. + - apply isequiv_negb. + - apply isequiv_negb. + - refine (isequiv_homotopic idmap _); intros []; reflexivity. + Defined. + + Definition equiv_inhab_baut_bool_bool (t : Bool) + (Z : BAut Bool) (z : Z) + : Bool <~> Z + := Build_Equiv _ _ (inhab_baut_bool_from_bool t Z z) _. + + Definition path_baut_bool_inhab (Z : BAut Bool) (z : Z) + : (point (BAut Bool)) = Z. + Proof. + apply path_baut. + exact (equiv_inhab_baut_bool_bool true Z z). (** [true] is a choice! *) + Defined. + + (** In fact, the map sending [z:Z] to this equivalence [Bool <~> Z] is also an equivalence. To assist with computing the result when [Z] is [Bool], we prove it with an extra parameter first. *) + Definition isequiv_equiv_inhab_baut_bool_bool_lemma + (t : Bool) (Z : BAut Bool) (m : merely (pt = Z)) + : IsEquiv (equiv_inhab_baut_bool_bool t Z). + Proof. + strip_truncations. destruct m. + refine (isequiv_adjointify _ (fun (e : Bool <~> Bool) => e t) _ _). + + intros e. + apply path_equiv. + refine (ap10 (inhab_baut_bool_from_bool_bool t) (e t) @ _). + apply path_arrow; intros []; destruct t. + * reflexivity. + * refine (abelian_aut_bool equiv_negb e false). + * refine (abelian_aut_bool equiv_negb e true). + * reflexivity. + + intros z. + refine (ap10 (ap10 (inhab_baut_bool_from_bool_bool t) z) t @ _). + destruct t; reflexivity. + Defined. + + Global Instance isequiv_equiv_inhab_baut_bool_bool + (t : Bool) (Z : BAut Bool) + : IsEquiv (equiv_inhab_baut_bool_bool t Z). + Proof. + exact (isequiv_equiv_inhab_baut_bool_bool_lemma t Z + (merely_path_component _ _)). + Defined. + + (** The names are getting pretty ridiculous; below we suggest a better name for this. *) + Definition equiv_equiv_inhab_baut_bool_bool (t : Bool) + (Z : BAut Bool) + : Z <~> (Bool <~> Z) + := Build_Equiv _ _ (equiv_inhab_baut_bool_bool t Z) _. + + (** We compute its inverse in the case of [Bool]. *) + Definition equiv_equiv_inhab_baut_bool_bool_bool_inv (t : Bool) + (e : Bool <~> Bool) + : equiv_inverse (equiv_equiv_inhab_baut_bool_bool t pt) e = e t. + Proof. + pose (alt := Build_Equiv _ _ (equiv_inhab_baut_bool_bool t pt) + (isequiv_equiv_inhab_baut_bool_bool_lemma + t pt (tr 1))). + assert (p : equiv_equiv_inhab_baut_bool_bool t pt = alt). + { apply (ap (fun i => Build_Equiv _ _ _ i)). + apply (ap (isequiv_equiv_inhab_baut_bool_bool_lemma t pt)). + apply path_ishprop. } + exact (ap10_equiv (ap equiv_inverse p) e). + Defined. + + (** ** Group structure *) + + (** Homotopically, [BAut Bool] is a [K(Z/2,1)]. In particular, it has a (coherent) abelian group structure induced from that of [Z/2]. With our definition of [BAut Bool], we can construct this operation as follows. *) + + Definition baut_bool_pairing : BAut Bool -> BAut Bool -> BAut Bool. + Proof. + intros Z W. + exists (Z <~> W). + baut_reduce; simpl. + apply tr, symmetry. + exact (path_universe equiv_bool_aut_bool). + Defined. + + Declare Scope baut_bool_scope. + Notation "Z ** W" := (baut_bool_pairing Z W) : baut_bool_scope. + Local Open Scope baut_bool_scope. + + (** Now [equiv_equiv_inhab_baut_bool_bool] is revealed as simply the left unit law of this pairing. *) + Definition baut_bool_pairing_1Z Z : pt ** Z = Z. + Proof. + apply path_baut, equiv_inverse, equiv_equiv_inhab_baut_bool_bool. + exact true. (** This is a choice! *) + Defined. + + (** The pairing is obviously symmetric. *) + Definition baut_bool_pairing_symm Z W : Z ** W = W ** Z. + Proof. + apply path_baut, equiv_equiv_inverse. + Defined. + + (** Whence we get the right unit law as well. *) + Definition baut_bool_pairing_Z1 Z : Z ** pt = Z + := baut_bool_pairing_symm Z pt @ baut_bool_pairing_1Z Z. + + (** Every element is its own inverse. *) + Definition baut_bool_pairing_ZZ Z : Z ** Z = pt. + Proof. + apply symmetry, path_baut_bool_inhab. + apply equiv_idmap. (** A choice! Could be the flip. *) + Defined. + + (** Associativity is easiest to think about in terms of "curried 2-variable equivalences". We start with some auxiliary lemmas. *) + Definition baut_bool_pairing_ZZ_Z_symm_part1 {Y Z W} + (e : Y ** (Z ** W)) (z : Z) + : Y ** W. + Proof. + simple refine (equiv_adjointify _ _ _ _). + + exact (fun y => e y z). + + intros w. + destruct (path_baut_bool_inhab W w). + destruct (path_baut_bool_inhab Z z). + (** It might be tempting to just say [e^-1 (equiv_idmap _)] here, but for the rest of the proof to work, we actually need to choose between [idmap] and [negb] based on whether [z] and [w] are equal or not. *) + destruct (dec (z=w)). + * exact (e^-1 (equiv_idmap _)). + * exact (e^-1 equiv_negb). + + intros w. + destruct (path_baut_bool_inhab W w). + destruct (path_baut_bool_inhab Z z). + simpl. + destruct z,w; simpl; refine (ap10_equiv (eisretr e _) _). + + intros y. + destruct (path_baut_bool_inhab Y y). + destruct (path_baut_bool_inhab Z z). + destruct (path_baut_bool_inhab W (e y z)). + simpl. + case (dec (z = e y z)); intros p; apply moveR_equiv_V; + destruct (aut_bool_idmap_or_negb (e y)) as [q|q]. + * symmetry; assumption. + * case (not_fixed_negb z (p @ ap10_equiv q z)^). + * case (p (ap10_equiv q z)^). + * symmetry; assumption. + Defined. + + Definition baut_bool_pairing_ZZ_Z_symm_lemma {Y Z W} + (e : Y ** (Z ** W)) (f : Y ** W) + : merely Y -> Z. + Proof. + pose (k := (fun y => (e y)^-1 (f y))). + refine (merely_rec_hset k); intros y1 y2. + destruct (path_baut_bool_inhab Y y1). + destruct (path_baut_bool_inhab W (f y1)). + destruct (path_baut_bool_inhab Z (k y1)). + destruct (aut_bool_idmap_or_negb f) as [p|p]; + refine (ap (e y1)^-1 (ap10_equiv p y1) @ _); + refine (_ @ (ap (e y2)^-1 (ap10_equiv p y2))^); + clear p f k; simpl. + + destruct (dec (y1=y2)) as [p|p]. + { exact (ap (fun y => (e y)^-1 y) p). } + destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1]; + destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2]. + * case (p ((ap e)^-1 (q1 @ q2^))). + * rewrite q1, q2. exact (negb_ne p). + * rewrite q1, q2. symmetry. exact (negb_ne (fun r => p r^)). + * case (p ((ap e)^-1 (q1 @ q2^))). + + destruct (dec (y1=y2)) as [p|p]. + { exact (ap (fun y => (e y)^-1 (negb y)) p). } + destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1]; + destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2]. + * case (p ((ap e)^-1 (q1 @ q2^))). + * rewrite q1, q2. + exact (negb_ne (fun r => p ((ap negb)^-1 r))). + * rewrite q1, q2. symmetry. + exact (negb_ne (fun r => p ((ap negb)^-1 r)^)). + * case (p ((ap e)^-1 (q1 @ q2^))). + Defined. + + Definition baut_bool_pairing_ZZ_Z_symm_map Y Z W + : Y ** (Z ** W) -> Z ** (Y ** W). + Proof. + intros e. + simple refine (equiv_adjointify (baut_bool_pairing_ZZ_Z_symm_part1 e) + _ _ _). + - intros f. + exact (baut_bool_pairing_ZZ_Z_symm_lemma e f + (merely_inhab_baut_bool Y)). + - intros f. + apply path_equiv, path_arrow; intros y. + change ((e y) + (baut_bool_pairing_ZZ_Z_symm_lemma e f + (merely_inhab_baut_bool Y)) = f y). + refine (ap (e y o baut_bool_pairing_ZZ_Z_symm_lemma e f) + (path_ishprop _ (tr y)) @ _). + simpl. apply eisretr. + - intros z. + assert (IsHSet Z) by exact _. + refine (Trunc_rec _ (merely_inhab_baut_bool Y)); intros y. + refine (ap (baut_bool_pairing_ZZ_Z_symm_lemma e _) + (path_ishprop _ (tr y)) @ _). + simpl. refine (eissect _ _). + Defined. + + Definition baut_bool_pairing_ZZ_Z_symm_inv Y Z W + : baut_bool_pairing_ZZ_Z_symm_map Y Z W + o baut_bool_pairing_ZZ_Z_symm_map Z Y W + == idmap. + Proof. + intros e. + apply path_equiv, path_arrow; intros z. + apply path_equiv, path_arrow; intros y. + reflexivity. + Defined. + + Definition baut_bool_pairing_ZZ_Z_symm Y Z W + : Y ** (Z ** W) <~> Z ** (Y ** W). + Proof. + refine (equiv_adjointify + (baut_bool_pairing_ZZ_Z_symm_map Y Z W) + (baut_bool_pairing_ZZ_Z_symm_map Z Y W) + (baut_bool_pairing_ZZ_Z_symm_inv Y Z W) + (baut_bool_pairing_ZZ_Z_symm_inv Z Y W)). + Defined. + + (** Finally, we can prove associativity. *) + Definition baut_bool_pairing_ZZ_Z Z W Y + : (Z ** W) ** Y = Z ** (W ** Y). + Proof. + refine (baut_bool_pairing_symm (Z ** W) Y @ _). + refine (_ @ ap (fun X => Z ** X) (baut_bool_pairing_symm Y W)). + apply path_baut, baut_bool_pairing_ZZ_Z_symm. + Defined. + + (** Since [BAut Bool] is not a set, we ought to have some coherence for these operations too, but we'll leave that for another time. *) + + (** ** Automorphisms of [BAut Bool] *) + + (** Interestingly, like [Bool] itself, [BAut Bool] is equivalent to its own automorphism group. *) + + (** An initial lemma: every automorphism of [BAut Bool] and its inverse are "adjoint" with respect to the pairing. *) + Definition aut_baut_bool_moveR_pairing_V + (e : BAut Bool <~> BAut Bool) (Z W : BAut Bool) + : (e^-1 Z ** W) = (Z ** e W). + Proof. + apply path_baut; simpl. + refine ((equiv_equiv_path _ _) oE _ oE (equiv_equiv_path _ _)^-1). + refine (_ oE (@equiv_moveL_equiv_M _ _ e _ W Z) oE _). + - apply equiv_inverse, equiv_path_sigma_hprop. + - apply equiv_path_sigma_hprop. + Defined. + + Definition equiv_baut_bool_aut_baut_bool + : BAut Bool <~> (BAut Bool <~> BAut Bool). + Proof. + simple refine (equiv_adjointify _ _ _ _). + - intros Z. + refine (equiv_involution (fun W => Z ** W) _). + intros W. + refine ((baut_bool_pairing_ZZ_Z Z Z W)^ @ _). + refine (_ @ baut_bool_pairing_1Z W). + apply (ap (fun Y => Y ** W)). + apply baut_bool_pairing_ZZ. + - intros e. + exact (e^-1 pt). + - intros e. + apply path_equiv, path_arrow; intros Z; simpl. + refine (aut_baut_bool_moveR_pairing_V e pt Z @ _). + apply baut_bool_pairing_1Z. + - intros Z. + apply baut_bool_pairing_Z1. + Defined. + + (** ** [BAut (BAut Bool)] *) + + (** Putting all of this together, we can construct a nontrivial 2-central element of [BAut (BAut Bool)]. *) + + Definition center_baut_bool_central + (g : BAut Bool <~> BAut Bool) (W : BAut Bool) + : ap g (negb_center_baut_bool W) = negb_center_baut_bool (g W). + Proof. + revert g; equiv_intro equiv_baut_bool_aut_baut_bool Z. + simpl. + baut_reduce. + refine (_ @ apD negb_center_baut_bool (baut_bool_pairing_1Z pt)^). + rewrite transport_paths_lr, inv_V. + apply moveL_pV. + exact (concat_A1p baut_bool_pairing_1Z (negb_center_baut_bool pt)). + Qed. + + Definition negb_center2_baut_baut_bool + : forall B : BAut (BAut Bool), (idpath B) = (idpath B). + Proof. + refine (center2_baut (BAut Bool) _). + exists negb_center_baut_bool. + apply center_baut_bool_central. + Defined. + + Definition nontrivial_negb_center_baut_baut_bool + : negb_center2_baut_baut_bool <> (fun Z => idpath (idpath Z)). + Proof. + intros oops. + exact (nontrivial_negb_center_baut_bool + (((ap (center2_baut (BAut Bool)))^-1 + (oops @ (id_center2_baut (BAut Bool))^))..1)). + Defined. + +End AssumeUnivalence. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.vo new file mode 100644 index 0000000000000000000000000000000000000000..37d20ce9c0965017e27300218c31d8b51a46397b --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:c7c607cb704205feab678f03d1834a68d2fa1172391fb4a6dc92859aae452894 +size 774082 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.vo new file mode 100644 index 0000000000000000000000000000000000000000..6195945e351ea1796988c30ebda5c540eea4dbf6 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:198b31d1593267436f37848c33810d3ebcce5546564ee533e6116870a6c5db06 +size 218157 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Card.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Card.vo new file mode 100644 index 0000000000000000000000000000000000000000..38d036d08982650849493c147c8ccc33b024b29f --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Card.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:e2c14871cc113b0348353e9439588f0b43043538ce26b0fa0ccb4b875538323b +size 679382 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/No/Addition.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/No/Addition.vo new file mode 100644 index 0000000000000000000000000000000000000000..019d039ec66b88b1bc77bd619cb4a03570c71bf1 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/No/Addition.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:9266083f75cc26c616b1d2ca86b7152613302544130103a34b7221ce4f4e8bba +size 1189062 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Universe.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Universe.v new file mode 100644 index 0000000000000000000000000000000000000000..b25416df6905e94b645b899389203137b66c7968 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Universe.v @@ -0,0 +1,217 @@ +(* -*- mode: coq; mode: visual-line -*- *) +Require Import Basics Types. +Require Import HoTT.Truncations. +Require Import Spaces.BAut Spaces.BAut.Rigid. +Require Import ExcludedMiddle. + +Local Open Scope trunc_scope. +Local Open Scope path_scope. + +(** * The universe *) + +(** ** Automorphisms of the universe *) + +(** See "Parametricity, automorphisms of the universe, and excluded middle" by Booij, Escardo, Lumsdaine, Shulman. *) + +(** If two inequivalent types have equivalent automorphism oo-groups, then assuming LEM we can swap them and leave the rest of the universe untouched. *) +Section SwapTypes. + (** Amusingly, this does not actually require univalence! But of course, to verify [BAut A <~> BAut B] in any particular example does require univalence. *) + Context `{Funext} `{ExcludedMiddle}. + Context (A B : Type) (ne : ~(A <~> B)) (e : BAut A <~> BAut B). + + Definition equiv_swap_types : Type <~> Type. + Proof. + refine (((equiv_decidable_sum (fun X:Type => merely (X=A)))^-1) + oE _ oE + (equiv_decidable_sum (fun X:Type => merely (X=A)))). + refine ((equiv_functor_sum_l + (equiv_decidable_sum (fun X => merely (X.1=B)))^-1) + oE _ oE + (equiv_functor_sum_l + (equiv_decidable_sum (fun X => merely (X.1=B))))). + refine ((equiv_sum_assoc _ _ _) + oE _ oE + (equiv_sum_assoc _ _ _)^-1). + apply equiv_functor_sum_r. + assert (q : BAut B <~> {x : {x : Type & ~ merely (x = A)} & + merely (x.1 = B)}). + { refine (equiv_sigma_assoc _ _ oE _). + apply equiv_functor_sigma_id; intros X. + apply equiv_iff_hprop. + - intros p. + refine (fun q => _ ; p). + strip_truncations. + destruct q. + exact (ne (equiv_path X B p)). + - exact pr2. } + refine (_ oE equiv_sum_symm _ _). + apply equiv_functor_sum'. + - exact (e^-1 oE q^-1). + - exact (q oE e). + Defined. + + Definition equiv_swap_types_swaps : merely (equiv_swap_types A = B). + Proof. + assert (ea := (e (point _)).2). cbn in ea. + strip_truncations; apply tr. + unfold equiv_swap_types. + apply moveR_equiv_V. + rewrite (equiv_decidable_sum_l + (fun X => merely (X=A)) A (tr 1)). + assert (ne' : ~ merely (B=A)) + by (intros p; strip_truncations; exact (ne (equiv_path A B p^))). + rewrite (equiv_decidable_sum_r + (fun X => merely (X=A)) B ne'). + cbn. + apply ap, path_sigma_hprop; cbn. + exact ea. + Defined. + + Definition equiv_swap_types_not_id + : equiv_swap_types <> equiv_idmap. + Proof. + intros p. + assert (q := equiv_swap_types_swaps). + strip_truncations. + apply ne. + apply equiv_path. + rewrite p in q; exact q. + Qed. + +End SwapTypes. + +(** In particular, we can swap any two distinct rigid types. *) + +Definition equiv_swap_rigid `{Univalence} `{ExcludedMiddle} + (A B : Type) `{IsRigid A} `{IsRigid B} (ne : ~(A <~> B)) + : Type <~> Type. +Proof. + refine (equiv_swap_types A B ne _). + apply equiv_contr_contr. +Defined. + +(** Such as [Empty] and [Unit]. *) + +Definition equiv_swap_empty_unit `{Univalence} `{ExcludedMiddle} + : Type <~> Type + := equiv_swap_rigid Empty Unit (fun e => e^-1 tt). + +(** In this case we get an untruncated witness of the swapping. *) + +Definition equiv_swap_rigid_swaps `{Univalence} `{ExcludedMiddle} + (A B : Type) `{IsRigid A} `{IsRigid B} (ne : ~(A <~> B)) + : equiv_swap_rigid A B ne A = B. +Proof. + unfold equiv_swap_rigid, equiv_swap_types. + apply moveR_equiv_V. + rewrite (equiv_decidable_sum_l + (fun X => merely (X=A)) A (tr 1)). + assert (ne' : ~ merely (B=A)) + by (intros p; strip_truncations; exact (ne (equiv_path A B p^))). + rewrite (equiv_decidable_sum_r + (fun X => merely (X=A)) B ne'). + cbn. + apply ap, path_sigma_hprop; cbn. + exact ((path_contr (center (BAut B)) (point (BAut B)))..1). +Defined. + +(** We can also swap the products of two rigid types with another type [X], under a connectedness/truncatedness assumption. *) + +Definition equiv_swap_prod_rigid `{Univalence} `{ExcludedMiddle} + (X A B : Type) (n : trunc_index) (ne : ~(X*A <~> X*B)) + `{IsRigid A} `{IsConnected n.+1 A} + `{IsRigid B} `{IsConnected n.+1 B} + `{IsTrunc n.+1 X} + : Type <~> Type. +Proof. + refine (equiv_swap_types (X*A) (X*B) ne _). + transitivity (BAut X). + - symmetry; exact (baut_prod_rigid_equiv X A n). + - exact (baut_prod_rigid_equiv X B n). +Defined. + +(** Conversely, from some nontrivial automorphisms of the universe we can deduce nonconstructive consequences. *) + +Definition lem_from_aut_type_unit_empty `{Univalence} + (f : Type <~> Type) (eu : f Unit = Empty) + : ExcludedMiddle_type. +Proof. + apply DNE_to_LEM, DNE_from_allneg; intros P ?. + exists (f P); split. + - intros p. + assert (Contr P) by (apply contr_inhabited_hprop; assumption). + assert (q : Unit = P) + by (apply path_universe_uncurried, equiv_contr_contr). + destruct q. + rewrite eu. + auto. + - intros nfp. + assert (q : f P = Empty) + by (apply path_universe_uncurried, equiv_to_empty, nfp). + rewrite <- eu in q. + apply ((ap f)^-1) in q. + rewrite q; exact tt. +Defined. + +Lemma equiv_hprop_idprod `{Univalence} + (A : Type) (P : Type) (a : merely A) `{IsHProp P} + : P <-> (P * A = A). +Proof. + split. + - intros p; apply path_universe with snd. + apply isequiv_adjointify with (fun a => (p,a)). + + intros x; reflexivity. + + intros [p' x]. + apply path_prod; [ apply path_ishprop | reflexivity ]. + - intros q. + strip_truncations. + apply equiv_path in q. + exact (fst (q^-1 a)). +Defined. + +Definition lem_from_aut_type_inhabited_empty `{Univalence} + (f : Type <~> Type) + (A : Type) (a : merely A) (eu : f A = Empty) + : ExcludedMiddle_type. +Proof. + apply DNE_to_LEM, DNE_from_allneg; intros P ?. + exists (f (P * A)); split. + - intros p. + assert (q := fst (equiv_hprop_idprod A P a) p). + apply (ap f) in q. + rewrite eu in q. + rewrite q; auto. + - intros q. + apply equiv_to_empty in q. + apply path_universe_uncurried in q. + rewrite <- eu in q. + apply ((ap f)^-1) in q. + exact (snd (equiv_hprop_idprod A P a) q). +Defined. + +(** If you can derive a constructive taboo from an automorphism of the universe such that [g X <> X], then you get [X]-many beers; see . *) + +Definition zero_beers `{Univalence} + (g : Type <~> Type) (ge : g Empty <> Empty) + : ~~ExcludedMiddle_type. +Proof. + pose (f := equiv_inverse g). + intros nlem. + apply ge. + apply path_universe_uncurried, equiv_to_empty; intros gz. + apply nlem. + apply (lem_from_aut_type_inhabited_empty f (g Empty) (tr gz)). + unfold f; apply eissect. +Defined. + +Definition lem_beers `{Univalence} + (g : Type <~> Type) (ge : g ExcludedMiddle_type <> ExcludedMiddle_type) + : ~~ExcludedMiddle_type. +Proof. + intros nlem. + pose (nlem' := equiv_to_empty nlem). + apply path_universe_uncurried in nlem'. + rewrite nlem' in ge. + apply (zero_beers g) in ge. + exact (ge nlem). +Defined. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Paths.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Paths.vo new file mode 100644 index 0000000000000000000000000000000000000000..56b67d0b3ddadad20d304eeed811e49c0b1cc174 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Paths.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:4eee41d70e1adcab6668f5b03e740ceaf5aa8177e1a05e93ca1d51bac7c672fc +size 291077 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Prod.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Prod.vo new file mode 100644 index 0000000000000000000000000000000000000000..9165ba30c43a3aa10a4ac71af9891f5b1201c9c7 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Prod.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ea1d9baa225e7f06c2d4edd131b6ba9dc1f73f00e431c23dc622dabb487f024d +size 238829 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Sigma.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Sigma.vo new file mode 100644 index 0000000000000000000000000000000000000000..844e537d7459eff66e4065599d93bfb490a82cca --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Sigma.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:60403f0eb098c40babbad07b97512d756594e58e1145fa714adef9b861adb217 +size 264842 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.vo new file mode 100644 index 0000000000000000000000000000000000000000..89000f6686184fc13c311f7abe946064cacdc719 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:087c4ac8fcac3bd4ae96e02abba50b82b5f44cfcee2376daf165024133416471 +size 142313 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Displayed.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Displayed.vo new file mode 100644 index 0000000000000000000000000000000000000000..088ffe6a558fe00998d85643d1199ef2727b0006 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Displayed.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:dd585c4f7cdc6e73587d2f4a294edc868e8269531a0621953b8d97a3fffab0f7 +size 285568 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/DisplayedEquiv.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/DisplayedEquiv.vo new file mode 100644 index 0000000000000000000000000000000000000000..e6b43d8140d6ecb8c5eee996fa6b9ae6776b9f0a --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/DisplayedEquiv.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:5816adb6d8a54ff93d0d1d123f1c807d7a4c39dbfdaca330d6e9eee36e76a798 +size 2044596 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.vo new file mode 100644 index 0000000000000000000000000000000000000000..f152e91dccb29f5152a5ba5018d47cbac1920db3 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:5ffb3d511c8fad77d526a85c157ab023280a6179edcee1a5256a6ae78eaeda35 +size 120627 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Yoneda.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Yoneda.vo new file mode 100644 index 0000000000000000000000000000000000000000..88242b7cdd20593ba7ebec99464a99e87c9a1e04 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Yoneda.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:8f5a485f6beff76d9cbdf4fa4ef2859061a1e789fc57be4b1622a4a4e12f734b +size 332541 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_ops.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_ops.vo new file mode 100644 index 0000000000000000000000000000000000000000..92c4d09cd37af6d2e2f4731dd6f5244642089840 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_ops.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:23958fc1bbba6cabb611bcc53801d81fe6ad176ff485eca23e99352e4049d88a +size 257110 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_stdz.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_stdz.vo new file mode 100644 index 0000000000000000000000000000000000000000..aabf8355c4bb4c311a98ac5f1f34f7dbb1126c00 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_stdz.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:624a8d26be7801f1239d4de480eeebd8ef70f4808a9467419cc75994d7d794f8 +size 121479 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Interval/Transcend.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Interval/Transcend.vo new file mode 100644 index 0000000000000000000000000000000000000000..bcdf8f36070177f264e96805122563604d61e8e4 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Interval/Transcend.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:be9779ecf7c61ab6742385ce427ddf234f23bab6c97d95d1889cc75d226c2faa +size 336661 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Language/Lang_expr.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Language/Lang_expr.vo new file mode 100644 index 0000000000000000000000000000000000000000..9c6d6aa4ec25aefae2a6359df682469f2bf0f362 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Language/Lang_expr.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:4b42c45e191a2e3a86da077539001a359c37cf6489a510d8511c89088f54688f +size 582806 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Integral_helper.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Integral_helper.vo new file mode 100644 index 0000000000000000000000000000000000000000..24814f205f639c9a68bd9fbba010ff85e4c8d3a1 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Integral_helper.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:662506abaaab197f6d2a7a780cef551d4d710640346b5452787603bfe457c100 +size 794707 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Interval_helper.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Interval_helper.vo new file mode 100644 index 0000000000000000000000000000000000000000..4baaadaa81a1e57388e7bde7d0294a1e466dfa73 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Interval_helper.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:50b17ee1d0458090f1663603ce9fa1909ed3c99e798f9430f1dcc56d8f54751e +size 390577 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/implementations/semiring_pairs.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/implementations/semiring_pairs.vo new file mode 100644 index 0000000000000000000000000000000000000000..90ba1d1344a28c8065297614ad600a888accc221 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/implementations/semiring_pairs.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:6545ebc298c3002e3655f2ef7c0c6a147aae67d9dbfcc35da9c6a1326eb70729 +size 114953 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rationals.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rationals.vo new file mode 100644 index 0000000000000000000000000000000000000000..32a167cd7b677b3f5fbd44c71d32baa9cfcfc332 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rationals.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:caf20c3a4b544be48ad7f2986e704308917b68fbd01bf51bc4f450d6250e9abe +size 170651 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rings.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rings.vo new file mode 100644 index 0000000000000000000000000000000000000000..ce43486e8549c26f51bd5ddd113faf2425e3ed0f --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rings.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:12c81b40f0d7c5aa7172dd689a1ee92a5bd2785172e892b021cb6f5ba07a38bd +size 129396 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_complete.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_complete.vo new file mode 100644 index 0000000000000000000000000000000000000000..bf6a001071781986c747e6ed62511ae12ad735e9 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_complete.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:743fb9be27f42ce9aaaaeb947986f3d424f96c4e21b8a63a72a5236276028bf7 +size 1344969 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_correct.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_correct.vo new file mode 100644 index 0000000000000000000000000000000000000000..d10075e2a2e5eb361a52c73a951de68a20c427bd --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_correct.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:a49114803a2631f20037c4b0b110e59ea7d10b17d55c7a5e4a8404278626ebb0 +size 246885 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Main.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Main.vo new file mode 100644 index 0000000000000000000000000000000000000000..7168cbf6e12c6d607b59f46575e675a23dcb8ea0 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Main.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:4bfe989cdc91917f255e7cc2a8dd25823c0fbd5d9a6a12cf2c054880e31fc097 +size 1235335 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_complete.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_complete.vo new file mode 100644 index 0000000000000000000000000000000000000000..85b1fe851542ac6451693402322dad60359ecf3e --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_complete.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:c6c55e761f487033b75110151cde7d61e81dfb634e94e03ad6878a859af44267 +size 1032266 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_safe.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_safe.vo new file mode 100644 index 0000000000000000000000000000000000000000..df52e0ef1f57bc6ba6577d23329d238d287989c9 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_safe.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:94e38b1e26ddce9903f91e8b0142a3dac6082864a4e8713af6937e90fb2df48a +size 138732 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/BasicAst.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/BasicAst.vo new file mode 100644 index 0000000000000000000000000000000000000000..0e86f2e7a705be86ece6067c3c803645c6f4d85f --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/BasicAst.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:3cac5272cd5685977812eac94e22ceecb2780ae5eaedeb99981b1b453006ffe6 +size 351391 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Environment.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Environment.vo new file mode 100644 index 0000000000000000000000000000000000000000..4f6949d9caa8ae934a55800e5fb1607dfbb46ef1 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Environment.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:87535b754e53dde6f49730c615c1b6592355a7846d57ca5827495dcca60d62ae +size 1333477 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentReflect.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentReflect.vo new file mode 100644 index 0000000000000000000000000000000000000000..2ed86792ca05764bc7f4f33cb03f94124d2659e1 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentReflect.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:a70fbc6609fd05086ed80c04e432edc3d8fd0feeb22d26cd8ce323c808398d47 +size 606884 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentTyping.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentTyping.vo new file mode 100644 index 0000000000000000000000000000000000000000..8678911848d0bd39cb83e9fdebe11a7fa0edb5a4 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentTyping.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:81a4dc0eb910151185c5efccf451ed7a3a5dff0f3aed0a947be6d56c79bc05fc +size 10807606 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Kernames.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Kernames.vo new file mode 100644 index 0000000000000000000000000000000000000000..ee7dc06f0c6e240c75d1b9410256720a9b62cd4f --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Kernames.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:57225e9b7758aedea1486c683b4744193849fb9961d8e0c511f38de161294ec2 +size 3299378 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/MonadBasicAst.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/MonadBasicAst.vo new file mode 100644 index 0000000000000000000000000000000000000000..8d2e308335bcc8e4a70a6e77fb7b2f681516354b --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/MonadBasicAst.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:5ad939e0f755211eb322d9f5ad85119217e46b65d8a5252d16c823b1857b7ae1 +size 104763 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Reflect.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Reflect.vo new file mode 100644 index 0000000000000000000000000000000000000000..e7d9f86969cc313c660ca6585254477b5f708815 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Reflect.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:57199cc2d232d6712981d0cff2b69d4342c44699005bff392842131061da649e +size 289374 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Universes.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Universes.vo new file mode 100644 index 0000000000000000000000000000000000000000..4404b4935912cf8d7cbece73965dd8546584881a --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Universes.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:74b5f844ce3adad8641612e71ae6d13639d9af6dbbd462cabcfe432544363bd6 +size 2694147 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/UniversesDec.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/UniversesDec.vo new file mode 100644 index 0000000000000000000000000000000000000000..e300c6f9e78631950a7ef9cdfefed5db85de0678 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/UniversesDec.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:2cebe8f2575b1d3744809c7489c84473d92b19a8465d6f6b9824226febe030c1 +size 567770 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/config.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/config.vo new file mode 100644 index 0000000000000000000000000000000000000000..2c5004d84d4d69a9f872a2d30c048a65f24c2d5f --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/config.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:cdbbf98291944bb19afa20bb598118ef28a8c1aef4eb2b57defb9f535839b9e5 +size 116941 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/uGraph.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/uGraph.vo new file mode 100644 index 0000000000000000000000000000000000000000..c2b9fe423e0f611662cc9ff14250654334c11bbe --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/uGraph.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:4bee25d99a4dda7f26c513d60ced1431f76e7869a00d48436f2c6c802b49e37e +size 2716161 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EArities.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EArities.vo new file mode 100644 index 0000000000000000000000000000000000000000..3029ae1f344960378191c01cdde02d72a6716917 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EArities.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:0d71eb35f4f974e4fd56f2471efd705669bced14646a3e2fe6dac2982709dc9f +size 328240 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAst.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAst.vo new file mode 100644 index 0000000000000000000000000000000000000000..d53a43350b7bb2000d1e2623721db4b2c3a44e8c --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAst.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:4f4fc255d4205a7107a5eb7568abd062c06ccd870cab1dd5abe6107edd30241a +size 293110 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAstUtils.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAstUtils.vo new file mode 100644 index 0000000000000000000000000000000000000000..04fa3e233ec13fda0a45c4c339450453899aa5dc --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAstUtils.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:efc8d4da580a7b720ba20523b1e010eb614e25c1fc44dd89729e68e71443ca1a +size 135325 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/ECoInductiveToInductive.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/ECoInductiveToInductive.vo new file mode 100644 index 0000000000000000000000000000000000000000..2ceed0968be3aa380bdf9bd682c8b2e2ee51f108 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/ECoInductiveToInductive.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:7bc2d5a7f312f5fc24e0c163985437949c7a0c3e8cd79c51ff4d9bbe7fdf2f2c +size 384273 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EConstructorsAsBlocks.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EConstructorsAsBlocks.vo new file mode 100644 index 0000000000000000000000000000000000000000..7a31295681b73cbf86279d020ccd95be7cbbc9f8 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EConstructorsAsBlocks.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:d597c0e91468579dea02b4928fd9eee254b8dcb1d368648c4c00ebb895f55902 +size 913374 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EDeps.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EDeps.vo new file mode 100644 index 0000000000000000000000000000000000000000..2f336e55071494d2adf888f904e62c99471ba619 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EDeps.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:321f895b7f053231d5333a448a59f1dfae1a3b6096b6d56a1370f4d67972309c +size 856886 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpanded.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpanded.vo new file mode 100644 index 0000000000000000000000000000000000000000..bf55095404a2fc69850875d115191dd8fe49145f --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpanded.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:b417163d4305200ff989ec4d88aaf55946d2c458a296c2c023859006ac6b65af +size 472076 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpandedFix.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpandedFix.vo new file mode 100644 index 0000000000000000000000000000000000000000..968bab17ec8caba8785fb27fe5e76732134fb305 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpandedFix.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:996362f50b3679766f3bf6f5333b54ad28d9fd526edcdf8025c4a223624b97db +size 1682133 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericGlobalMap.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericGlobalMap.vo new file mode 100644 index 0000000000000000000000000000000000000000..0774f24a50310eac18363dba23ae72c610f94add --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericGlobalMap.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:14bf40a51694efeef50cfd55739d2010f901d4788a637ac7853b3b7a537325cd +size 189491 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericMapEnv.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericMapEnv.vo new file mode 100644 index 0000000000000000000000000000000000000000..cfa659d19430daa0ea4b7c9796d832aab8edc76b --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericMapEnv.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:8d07fbacbd3e2962bba730dbca733423699e1cee0836f178add60cf8a775dc4a +size 158254 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EImplementBox.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EImplementBox.vo new file mode 100644 index 0000000000000000000000000000000000000000..a7fad8700cc214cae7511b6eadb963514e936ea2 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EImplementBox.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:f1205073614434c4ddd62bec01ba7498527831e9e68af08dcc30fcf88c559fb0 +size 358643 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EInduction.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EInduction.vo new file mode 100644 index 0000000000000000000000000000000000000000..29cb5b13cfb3802de4a05dc0c20bfebdba9ac9c7 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EInduction.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:e1b2ffced6c201e5a825e8e7aa4b2ec9c8cf7862a5ccd61ee388f37b0f30dce0 +size 424916 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/base.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/base.vo new file mode 100644 index 0000000000000000000000000000000000000000..096bb0ba7e18b0f4a03fa38175dead0a211bf89e --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/base.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:e6511e20d9f1b9331405a9c153a25017f496c14001baa15637ae8d5808245b26 +size 300212 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/ind.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/ind.vo new file mode 100644 index 0000000000000000000000000000000000000000..5f751bcf5746831e883b86598a44ee95c17d4429 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/ind.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:af4174fd89eff7c1f1be3cabc53a207542b9d342381292c6edf0f8a842db0f5d +size 269499 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances.vo new file mode 100644 index 0000000000000000000000000000000000000000..a32986cfd7e43a63732a3806002f6a42cd8e8384 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:943719f514267cfdc77654c070831c3bf119e5cdf3ce95ea2d690e40c3da0087 +size 703282 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances/order.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances/order.vo new file mode 100644 index 0000000000000000000000000000000000000000..8666efaa6b743cddaf911f8bd89465e22bedd804 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances/order.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:bceddea04a5ce027a442821ae1b2f1f47b943261c39e1b2839b6b4d1206a80c1 +size 141626 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/lib/gmap_view.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/lib/gmap_view.vo new file mode 100644 index 0000000000000000000000000000000000000000..b6dd926c43ffe0a28f9f2eacb9529086416adc85 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/lib/gmap_view.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:592a997a9b9ff73333a1bb7820da2c88a1d299893c12c33efce9fd0fd1539032 +size 276115 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/view.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/view.vo new file mode 100644 index 0000000000000000000000000000000000000000..bb3d8f692ca11942eefd126ff7affc9b7306a9ab --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/view.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:c35a56635750efe72b7959ab05c90419400326497c842340f8010ddf9eaf468c +size 279290 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/bi/lib/fixpoint.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/bi/lib/fixpoint.vo new file mode 100644 index 0000000000000000000000000000000000000000..3863ce2807410ec6dc94c164c5b5a8385e2c0c12 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/bi/lib/fixpoint.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:8314178c1a9646877077a628d144131ddd707ae224256f56f71990666fc6c9f6 +size 118285 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/atomic_heap.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/atomic_heap.v new file mode 100644 index 0000000000000000000000000000000000000000..055e10fc6d30bfd83f03b1d52581438742b2980d --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/atomic_heap.v @@ -0,0 +1,221 @@ +From iris.bi.lib Require Import fractional. +From iris.proofmode Require Import proofmode. +From iris.program_logic Require Export atomic. +From iris.heap_lang Require Export derived_laws. +From iris.heap_lang Require Import notation proofmode. +From iris.prelude Require Import options. + +(** A general logically atomic interface for a heap. All parameters are +implicit, since it is expected that there is only one [heapGS_gen] in scope that +could possibly apply. For example: + + Context `{!heapGS_gen hlc Σ, !atomic_heap}. + +Or, for libraries that require later credits: + + Context `{!heapGS Σ, !atomic_heap}. + +Only one instance of this class should ever be in scope. To write a library that +is generic over the lock, just add a [`{!atomic_heap}] implicit parameter around +the code and [`{!atomic_heapGS Σ}] around the proofs. To use a particular atomic +heap instance, use [Local Existing Instance ]. + +When writing an instance of this class, please take care not to shadow the class +projections (e.g., either use [Local Definition alloc] or avoid the name [alloc] +altogether), and do not register an instance -- just make it a [Definition] that +others can register later. +*) +Class atomic_heap := AtomicHeap { + (* -- operations -- *) + alloc : val; + free : val; + load : val; + store : val; + cmpxchg : val; + (** * Ghost state *) + (** The assumptions about [Σ], and the singleton [gname]s (if needed) *) + atomic_heapGS : gFunctors → Type; + (* -- predicates -- *) + pointsto `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (dq: dfrac) (v : val) : iProp Σ; + (* -- pointsto properties -- *) + #[global] pointsto_timeless `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v :: + Timeless (pointsto (H:=H) l q v); + #[global] pointsto_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v :: + Fractional (λ (q : Qp), pointsto (H:=H) l (DfracOwn q) v); + #[global] pointsto_persistent `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v :: + Persistent (pointsto (H:=H) l DfracDiscarded v); + #[global] pointsto_as_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v :: + AsFractional (pointsto (H:=H) l (DfracOwn q) v) (λ q, pointsto (H:=H) l (DfracOwn q) v) q; + pointsto_agree `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l dq1 dq2 v1 v2 : + pointsto (H:=H) l dq1 v1 -∗ pointsto (H:=H) l dq2 v2 -∗ ⌜v1 = v2⌝; + pointsto_persist `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l dq v : + pointsto (H:=H) l dq v ==∗ pointsto (H:=H) l DfracDiscarded v; + (* -- operation specs -- *) + alloc_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (v : val) : + {{{ True }}} alloc v {{{ l, RET #l; pointsto (H:=H) l (DfracOwn 1) v }}}; + free_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (v : val) : + {{{ pointsto (H:=H) l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}}; + load_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) : + ⊢ <<{ ∀∀ (v : val) q, pointsto (H:=H) l q v }>> + load #l @ ∅ + <<{ pointsto (H:=H) l q v | RET v }>>; + store_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w : val) : + ⊢ <<{ ∀∀ v, pointsto (H:=H) l (DfracOwn 1) v }>> store #l w @ ∅ + <<{ pointsto (H:=H) l (DfracOwn 1) w | RET #() }>>; + (* This spec is slightly weaker than it could be: It is sufficient for [w1] + *or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed] + is outside the atomic triple, which makes it much easier to use -- and the + spec is still good enough for all our applications. + The postcondition deliberately does not use [bool_decide] so that users can + [destruct (decide (a = b))] and it will simplify in both places. *) + cmpxchg_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w1 w2 : val) : + val_is_unboxed w1 → + ⊢ <<{ ∀∀ v, pointsto (H:=H) l (DfracOwn 1) v }>> cmpxchg #l w1 w2 @ ∅ + <<{ if decide (v = w1) + then pointsto (H:=H) l (DfracOwn 1) w2 else pointsto (H:=H) l (DfracOwn 1) v + | RET (v, #if decide (v = w1) then true else false) }>>; +}. + +Global Arguments alloc : simpl never. +Global Arguments free : simpl never. +Global Arguments load : simpl never. +Global Arguments store : simpl never. +Global Arguments cmpxchg : simpl never. +Global Arguments pointsto : simpl never. + +Existing Class atomic_heapGS. +Global Hint Mode atomic_heapGS + + : typeclass_instances. +Global Hint Extern 0 (atomic_heapGS _) => progress simpl : typeclass_instances. + +Local Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)). + +Definition faa_atomic `{!atomic_heap} : val := + rec: "faa" "l" "n" := + let: "m" := load "l" in + if: CAS "l" "m" ("m" + "n") then "m" else "faa" "l" "n". + +(** Notation for heap primitives, in a module so you can import it separately. *) +Module notation. + Notation "l ↦ dq v" := (pointsto l dq v) + (at level 20, dq custom dfrac at level 1, format "l ↦ dq v") : bi_scope. + + Notation "'ref' e" := (alloc e) : expr_scope. + Notation "! e" := (load e) : expr_scope. + Notation "e1 <- e2" := (store e1 e2) : expr_scope. + + Notation CAS e1 e2 e3 := (Snd (cmpxchg e1 e2 e3)). + Notation FAA e1 e2 := (faa_atomic e1 e2). +End notation. + +Section derived. + Context `{!heapGS_gen hlc Σ, !atomic_heap, !atomic_heapGS Σ}. + + Import notation. + + Lemma cas_spec (l : loc) (w1 w2 : val) : + val_is_unboxed w1 → + ⊢ <<{ ∀∀ v, pointsto l (DfracOwn 1) v }>> + CAS #l w1 w2 @ ∅ + <<{ if decide (v = w1) + then pointsto l (DfracOwn 1) w2 else pointsto l (DfracOwn 1) v + | RET #if decide (v = w1) then true else false }>>. + Proof. + iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done. + iApply (aacc_aupd_commit with "AU"); first done. + iIntros (v) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame. + iIntros "$ !> HΦ !>". wp_pures. done. + Qed. + + Lemma faa_spec (l : loc) (i2 : Z) : + ⊢ <<{ ∀∀ i1 : Z, pointsto l (DfracOwn 1) #i1 }>> + FAA #l #i2 @ ∅ + <<{ pointsto l (DfracOwn 1) #(i1 + i2) | RET #i1 }>>. + Proof. + iIntros (Φ) "AU". rewrite /faa_atomic. iLöb as "IH". + wp_pures. awp_apply load_spec. + iApply (aacc_aupd_abort with "AU"); first done. + iIntros (i1) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame. + iIntros "$ !> AU !>". wp_pures. + awp_apply cas_spec; first done. + iApply (aacc_aupd with "AU"); first done. + iIntros (m) "Hl". + iAaccIntro with "Hl"; first by eauto with iFrame. + iIntros "Hl"; destruct (decide (#m = #i1)); simplify_eq. + - iModIntro. iRight. iFrame. iIntros "Hpost". iModIntro. by wp_pures. + - iModIntro. iLeft. iFrame. iIntros "AU". iModIntro. wp_pure. + by iApply "IH". + Qed. + +End derived. + +(** Proof that the primitive physical operations of heap_lang satisfy said interface. *) +Definition primitive_alloc : val := + λ: "v", ref "v". +Definition primitive_free : val := + λ: "v", Free "v". +Definition primitive_load : val := + λ: "l", !"l". +Definition primitive_store : val := + λ: "l" "x", "l" <- "x". +Definition primitive_cmpxchg : val := + λ: "l" "e1" "e2", CmpXchg "l" "e1" "e2". + +Section proof. + Context `{!heapGS_gen hlc Σ}. + + Lemma primitive_alloc_spec (v : val) : + {{{ True }}} primitive_alloc v {{{ l, RET #l; l ↦ v }}}. + Proof. + iIntros (Φ) "_ HΦ". wp_lam. wp_alloc l. iApply "HΦ". done. + Qed. + + Lemma primitive_free_spec (l : loc) (v : val) : + {{{ l ↦ v }}} primitive_free #l {{{ l, RET #l; True }}}. + Proof. + iIntros (Φ) "Hl HΦ". wp_lam. wp_free. iApply "HΦ". done. + Qed. + + Lemma primitive_load_spec (l : loc) : + ⊢ <<{ ∀∀ (v : val) q, l ↦{q} v }>> primitive_load #l @ ∅ + <<{ l ↦{q} v | RET v }>>. + Proof. + iIntros (Φ) "AU". wp_lam. + iMod "AU" as (v q) "[H↦ [_ Hclose]]". + wp_load. iMod ("Hclose" with "H↦") as "HΦ". done. + Qed. + + Lemma primitive_store_spec (l : loc) (w : val) : + ⊢ <<{ ∀∀ v, l ↦ v }>> primitive_store #l w @ ∅ + <<{ l ↦ w | RET #() }>>. + Proof. + iIntros (Φ) "AU". wp_lam. wp_let. + iMod "AU" as (v) "[H↦ [_ Hclose]]". + wp_store. iMod ("Hclose" with "H↦") as "HΦ". done. + Qed. + + Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) : + val_is_unboxed w1 → + ⊢ <<{ ∀∀ (v : val), l ↦ v }>> + primitive_cmpxchg #l w1 w2 @ ∅ + <<{ if decide (v = w1) then l ↦ w2 else l ↦ v + | RET (v, #if decide (v = w1) then true else false) }>>. + Proof. + iIntros (? Φ) "AU". wp_lam. wp_pures. + iMod "AU" as (v) "[H↦ [_ Hclose]]". + destruct (decide (v = w1)) as [Heq|Hne]; + [wp_cmpxchg_suc|wp_cmpxchg_fail]; + iMod ("Hclose" with "H↦") as "HΦ"; done. + Qed. +End proof. + +(* NOT an instance because users should choose explicitly to use it + (using [Explicit Instance]). *) +Definition primitive_atomic_heap : atomic_heap := + {| atomic_heapGS _ := TCTrue; + alloc_spec _ _ _ _ := primitive_alloc_spec; + free_spec _ _ _ _ := primitive_free_spec; + load_spec _ _ _ _ := primitive_load_spec; + store_spec _ _ _ _ := primitive_store_spec; + cmpxchg_spec _ _ _ _ := primitive_cmpxchg_spec; + pointsto_persist _ _ _ _ := primitive_laws.pointsto_persist; + pointsto_agree _ _ _ _ := primitive_laws.pointsto_agree |}. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/clairvoyant_coin.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/clairvoyant_coin.v new file mode 100644 index 0000000000000000000000000000000000000000..89adf062e460b2107c844fb7a3f40b4ad41bff8f --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/clairvoyant_coin.v @@ -0,0 +1,81 @@ +From iris.base_logic Require Export invariants. +From iris.program_logic Require Export weakestpre. +From iris.heap_lang Require Export lang proofmode notation. +From iris.heap_lang.lib Require Export nondet_bool. +From iris.prelude Require Import options. + +(** The clairvoyant coin predicts all the values that it will +*non-deterministically* choose throughout the execution of the +program. This can be seen in the spec. The predicate [coin c bs] +expresses that [bs] is the list of all the values of the coin in the +future. The [read_coin] operation always returns the head of [bs] and the +[toss_coin] operation takes the [tail] of [bs]. *) + +Definition new_coin: val := + λ: <>, (ref (nondet_bool #()), NewProph). + +Definition read_coin : val := λ: "cp", !(Fst "cp"). + +Definition toss_coin : val := + λ: "cp", + let: "c" := Fst "cp" in + let: "p" := Snd "cp" in + let: "r" := nondet_bool #() in + "c" <- "r";; resolve_proph: "p" to: "r";; #(). + +Section proof. + Context `{!heapGS Σ}. + + Definition prophecy_to_list_bool (vs : list (val * val)) : list bool := + (λ v, bool_decide (v = #true)) ∘ snd <$> vs. + + Definition coin (cp : val) (bs : list bool) : iProp Σ := + ∃ (c : loc) (p : proph_id) (vs : list (val * val)), + ⌜cp = (#c, #p)%V⌝ ∗ + ⌜bs ≠ []⌝ ∗ ⌜tail bs = prophecy_to_list_bool vs⌝ ∗ + proph p vs ∗ + from_option (λ b : bool, c ↦ #b) (∃ b : bool, c ↦ #b) (head bs). + + Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c bs, RET c; coin c bs }}}. + Proof. + iIntros (Φ) "_ HΦ". + wp_lam. + wp_apply wp_new_proph as (vs p) "Hp"; first done. + wp_apply nondet_bool_spec as (b) "_"; first done. + wp_alloc c as "Hc". + wp_pair. + iApply ("HΦ" $! (#c, #p)%V (b :: prophecy_to_list_bool vs)). + rewrite /coin; eauto 10 with iFrame. + Qed. + + Lemma read_coin_spec cp bs : + {{{ coin cp bs }}} + read_coin cp + {{{b bs', RET #b; ⌜bs = b :: bs'⌝ ∗ coin cp bs }}}. + Proof. + iIntros (Φ) "Hc HΦ". + iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]". + destruct bs as [|b bs]; simplify_eq/=. + wp_lam. wp_load. + iApply "HΦ"; iSplitR; first done. + rewrite /coin; eauto 10 with iFrame. + Qed. + + Lemma toss_coin_spec cp bs : + {{{ coin cp bs }}} + toss_coin cp + {{{b bs', RET #(); ⌜bs = b :: bs'⌝ ∗ coin cp bs' }}}. + Proof. + iIntros (Φ) "Hc HΦ". + iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]". + destruct bs as [|b bs]; simplify_eq/=. + wp_lam. do 2 (wp_proj; wp_let). + wp_apply nondet_bool_spec as (r) "_"; first done. + wp_store. + wp_apply (wp_resolve_proph with "[Hp]") as (ws) "[-> Hp]"; first done. + wp_seq. + iApply "HΦ"; iSplitR; first done. + destruct r; rewrite /coin; eauto 10 with iFrame. + Qed. + +End proof. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/clairvoyant_coin.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/clairvoyant_coin.vo new file mode 100644 index 0000000000000000000000000000000000000000..3cd8fb6a3d9a4647f99ca3d3c589122bf5e31fcc Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/clairvoyant_coin.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/counter.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/counter.v new file mode 100644 index 0000000000000000000000000000000000000000..f32bd01b31f5b722ac6e557d49e0c8501a0cee78 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/counter.v @@ -0,0 +1,170 @@ +From iris.algebra Require Import lib.frac_auth numbers auth. +From iris.proofmode Require Import proofmode. +From iris.base_logic.lib Require Export invariants. +From iris.program_logic Require Export weakestpre. +From iris.heap_lang Require Export lang. +From iris.heap_lang Require Import proofmode notation. +From iris.prelude Require Import options. + +Definition newcounter : val := λ: <>, ref #0. +Definition incr : val := rec: "incr" "l" := + let: "n" := !"l" in + if: CAS "l" "n" (#1 + "n") then #() else "incr" "l". +Definition read : val := λ: "l", !"l". + +(** Monotone counter *) +Class mcounterG Σ := MCounterG { mcounter_inG : inG Σ (authR max_natUR) }. +Local Existing Instance mcounter_inG. + +Definition mcounterΣ : gFunctors := #[GFunctor (authR max_natUR)]. + +Global Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ. +Proof. solve_inG. Qed. + +Section mono_proof. + Context `{!heapGS Σ, !mcounterG Σ} (N : namespace). + + Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ := + ∃ n, own γ (● (MaxNat n)) ∗ l ↦ #n. + + Definition mcounter (l : loc) (n : nat) : iProp Σ := + ∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (MaxNat n)). + + (** The main proofs. *) + Global Instance mcounter_persistent l n : Persistent (mcounter l n). + Proof. apply _. Qed. + + Lemma newcounter_mono_spec : + {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}. + Proof. + iIntros (Φ) "_ HΦ". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl". + iMod (own_alloc (● (MaxNat O) ⋅ ◯ (MaxNat O))) as (γ) "[Hγ Hγ']"; + first by apply auth_both_valid_discrete. + iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]"). + { iNext. iExists 0. by iFrame. } + iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10. + Qed. + + Lemma incr_mono_spec l n : + {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}. + Proof. + iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec. + iDestruct "Hl" as (γ) "[#? Hγf]". + wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]". + wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. + wp_pures. wp_bind (CmpXchg _ _ _). + iInv N as (c') ">[Hγ Hl]". + destruct (decide (c' = c)) as [->|]. + - iCombine "Hγ Hγf" + gives %[?%max_nat_included _]%auth_both_valid_discrete. + iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]". + { apply auth_update, (max_nat_local_update _ _ (MaxNat (S c))). simpl. auto. } + wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ". + { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } + wp_pures. iApply "HΦ". iModIntro. iExists γ; repeat iSplit; eauto. + iApply (own_mono with "Hγf"). + (* FIXME: FIXME(Coq #6294): needs new unification *) + apply: auth_frag_mono. by apply max_nat_included, le_n_S. + - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro. + iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. + wp_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto. + rewrite {3}/mcounter; eauto 10. + Qed. + + Lemma read_mono_spec l j : + {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝ ∧ mcounter l i }}}. + Proof. + iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]". + rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". + wp_load. + iCombine "Hγ Hγf" + gives %[?%max_nat_included _]%auth_both_valid_discrete. + iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]". + { apply auth_update, (max_nat_local_update _ _ (MaxNat c)); auto. } + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. + iApply ("HΦ" with "[-]"). rewrite /mcounter; eauto 10. + Qed. +End mono_proof. + +(** Counter with contributions *) +Class ccounterG Σ := + CCounterG { ccounter_inG : inG Σ (frac_authR natR) }. +Local Existing Instance ccounter_inG. + +Definition ccounterΣ : gFunctors := + #[GFunctor (frac_authR natR)]. + +Global Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ. +Proof. solve_inG. Qed. + +Section contrib_spec. + Context `{!heapGS Σ, !ccounterG Σ} (N : namespace). + + Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ := + ∃ n, own γ (●F n) ∗ l ↦ #n. + + Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ := + inv N (ccounter_inv γ l). + + Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ := + own γ (◯F{q} n). + + (** The main proofs. *) + Lemma ccounter_op γ q1 q2 n1 n2 : + ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1 ∗ ccounter γ q2 n2. + Proof. by rewrite /ccounter frac_auth_frag_op -own_op. Qed. + + Lemma newcounter_contrib_spec (R : iProp Σ) : + {{{ True }}} newcounter #() + {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}. + Proof. + iIntros (Φ) "_ HΦ". rewrite /newcounter /=. wp_lam. wp_alloc l as "Hl". + iMod (own_alloc (●F O ⋅ ◯F 0)) as (γ) "[Hγ Hγ']"; + first by apply auth_both_valid_discrete. + iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]"). + { iNext. iExists 0. by iFrame. } + iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10. + Qed. + + Lemma incr_contrib_spec γ l q n : + {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} incr #l + {{{ RET #(); ccounter γ q (S n) }}}. + Proof. + iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec. + wp_bind (! _)%E. iInv N as (c) ">[Hγ Hl]". + wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. + wp_pures. wp_bind (CmpXchg _ _ _). + iInv N as (c') ">[Hγ Hl]". + destruct (decide (c' = c)) as [->|]. + - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]". + { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. } + wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ". + { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. } + wp_pures. by iApply "HΦ". + - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]). + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|]. + wp_pures. by iApply ("IH" with "[Hγf] [HΦ]"); auto. + Qed. + + Lemma read_contrib_spec γ l q n : + {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} read #l + {{{ c, RET #c; ⌜n ≤ c⌝ ∧ ccounter γ q n }}}. + Proof. + iIntros (Φ) "[#? Hγf] HΦ". + rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load. + iCombine "Hγ Hγf" gives % ?%frac_auth_included_total%nat_included. + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. + iApply ("HΦ" with "[-]"); rewrite /ccounter; eauto 10. + Qed. + + Lemma read_contrib_spec_1 γ l n : + {{{ ccounter_ctx γ l ∗ ccounter γ 1 n }}} read #l + {{{ RET #n; ccounter γ 1 n }}}. + Proof. + iIntros (Φ) "[#? Hγf] HΦ". + rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load. + iCombine "Hγ Hγf" gives % <-%frac_auth_agree_L. + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|]. + by iApply "HΦ". + Qed. +End contrib_spec. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/diverge.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/diverge.v new file mode 100644 index 0000000000000000000000000000000000000000..ae976727843aa63b4866208ad1d4c704aed153de --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/diverge.v @@ -0,0 +1,27 @@ +From iris.proofmode Require Import proofmode. +From iris.program_logic Require Export weakestpre. +From iris.heap_lang Require Export lang. +From iris.heap_lang Require Import proofmode notation. +From iris.prelude Require Import options. + +(** This library provides a [diverge] function that goes into an infinite loop +when provided with an (arbitrary) argument value. This function can be used to +let the program diverge in corner cases that one wants to omit in proofs. This +mechanism should be used with care and communicated clearly, obviously. + +Note that this mechanism only works when establishing partial correctness with +the ordinary version of weakest preconditions, and not when establishing total +correctness using the total version of weakest preconditions. + +A typical application for [diverge] is insertion functions for data structures +having a fixed capacity. In such cases, we can choose divergence instead of an +explicit error handling when the full capacity has already been reached. *) + +Definition diverge : val := + rec: "diverge" "v" := "diverge" "v". + +Lemma wp_diverge `{!heapGS Σ} s E (Φ : val → iProp Σ) (v : val) : + ⊢ WP diverge v @ s;E {{ Φ }}. +Proof. + iLöb as "IH". wp_lam. iApply "IH". +Qed. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/diverge.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/diverge.vo new file mode 100644 index 0000000000000000000000000000000000000000..3bc9dc2558a7e362358d931f114f6282c076a2c9 Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/diverge.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/increment.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/increment.v new file mode 100644 index 0000000000000000000000000000000000000000..e385bde3591a7783a29624ac2679273725f04525 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/increment.v @@ -0,0 +1,187 @@ +From iris.bi.lib Require Import fractional. +From iris.proofmode Require Import proofmode. +From iris.base_logic.lib Require Export invariants. +From iris.program_logic Require Export atomic. +From iris.heap_lang Require Import proofmode notation atomic_heap par. +From iris.prelude Require Import options. + +(** Show that implementing fetch-and-add on top of CAS preserves logical +atomicity. *) + +(** First: logically atomic increment directly on top of the physical heap. *) + +Section increment_physical. + Context `{!heapGS Σ}. + + Definition incr_phy : val := + rec: "incr" "l" := + let: "oldv" := !"l" in + if: CAS "l" "oldv" ("oldv" + #1) + then "oldv" (* return old value if success *) + else "incr" "l". + + Lemma incr_phy_spec (l: loc) : + ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr_phy #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>. + Proof. + iIntros (Φ) "AU". iLöb as "IH". wp_lam. + (* [iMod] knows how to eliminate [AU] assertions. They are mask-changing + though so we first need to bind to make sure we have an atomic expression. + Out of the [AU], we then get the atomic precondition as well as the + closing updates. There's two closing updates, one to "abort" the update + and one to "commit"; in this case, we only need the "abort". *) + wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]". + wp_load. iMod ("Hclose" with "Hl") as "AU". + iModIntro. wp_pures. + (* As above, but this time we need both the "abort" and "commit" updates. *) + wp_bind (CmpXchg _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]". + destruct (decide (#v = #w)) as [[= ->]|Hx]. + - wp_cmpxchg_suc. iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ". + iModIntro. wp_pures. done. + - wp_cmpxchg_fail. iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU". + iModIntro. wp_pures. iApply "IH". done. + Qed. +End increment_physical. + +(** Next: logically atomic increment on top of an arbitrary logically atomic heap *) + +Section increment. + Context `{!atomic_heap}. + + Import atomic_heap.notation. + + Definition incr : val := + rec: "incr" "l" := + let: "oldv" := !"l" in + if: CAS "l" "oldv" ("oldv" + #1) + then "oldv" (* return old value if success *) + else "incr" "l". + + Context `{!heapGS Σ, !atomic_heapGS Σ}. + + (** A proof of the incr specification that unfolds the definition of atomic + accessors. This is the style that most logically atomic proofs take. *) + Lemma incr_spec_direct (l: loc) : + ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>. + Proof. + iIntros (Φ) "AU". iLöb as "IH". wp_lam. + awp_apply load_spec. + (* Prove the atomic update for load *) + (* To [iMod] a *mask-changing* update (like "AU"), we have to unfold + [atomic_acc] in the goal. + Note that non-mask-changing [iMod] and [iInv] would work here without + unfolding, i.e., an [AACC] in the goal supports eliminating + non-mask-changing updates and accessors but it does not support + eliminating mask-changing updates. *) + rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]". + (* Usually, we would use [iAaccIntro], but here we cannot because we + unfolded [atomic_acc], so we do it by hand. *) + iModIntro. iExists _, _. iFrame "Hl". iSplit. + { (* abort case *) done. } + iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro. + (* Now go on *) + wp_pures. awp_apply cas_spec; first done. + (* Prove the atomic update for CAS. We want to prove the precondition of + that update (the ↦) as quickly as possible because every step we take + along the way has to be "reversible" to prove the "abort" update. *) + rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]". + iModIntro. iExists _. iFrame "Hl". iSplit. + { (* abort case *) iDestruct "Hclose" as "[? _]". done. } + (* Good, we proved the precondition, now we can proceed "as normal". *) + iIntros "Hl". simpl. destruct (decide (#w = #v)) as [[= ->]|Hx]. + - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ". + iIntros "!>". wp_if. by iApply "HΦ". + - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU". + iIntros "!>". wp_if. iApply "IH". done. + Qed. + + (** A proof of the incr specification that uses lemmas ([aacc_aupd_*]) to + avoid reasoning with the definition of atomic accessors. These lemmas are + only usable here because the atomic update we have and the one we try to + prove are in 1:1 correspondence; most logically atomic proofs will not be + able to use them. *) + Lemma incr_spec (l: loc) : + ⊢ <<{ ∀∀ (v : Z), l ↦ #v }>> incr #l @ ∅ <<{ l ↦ #(v + 1) | RET #v }>>. + Proof. + iIntros (Φ) "AU". iLöb as "IH". wp_lam. + awp_apply load_spec. + (* Prove the atomic update for load *) + iApply (aacc_aupd_abort with "AU"); first done. + iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame. + iIntros "$ !> AU !>". + (* Now go on *) + wp_pures. awp_apply cas_spec; first done. + (* Prove the atomic update for CAS *) + iApply (aacc_aupd with "AU"); first done. + iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame. + iIntros "H↦ !>". + simpl. destruct (decide (#x' = #x)) as [[= ->]|Hx]. + - iRight. iFrame. iIntros "HΦ !>". + wp_if. by iApply "HΦ". + - iLeft. iFrame. iIntros "AU !>". + wp_if. iApply "IH". done. + Qed. + + (** A "weak increment": assumes that there is no race *) + Definition weak_incr: val := + rec: "weak_incr" "l" := + let: "oldv" := !"l" in + "l" <- ("oldv" + #1);; + "oldv" (* return old value *). + + (** Logically atomic spec for weak increment. Also an example for what TaDA + calls "private precondition". *) + (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-pointsto" + connective that works on [option Qp] (the type of 1-q). *) + Lemma weak_incr_spec (l: loc) (v : Z) : + l ↦{#1/2} #v -∗ + <<{ ∀∀ (v' : Z), l ↦{#1/2} #v' }>> + weak_incr #l @ ∅ + <<{ ⌜v = v'⌝ ∗ l ↦ #(v + 1) + | RET #v }>>. + Proof. + iIntros "Hl" (Φ) "AU". wp_lam. + wp_apply (atomic_wp_seq $! (load_spec _) with "Hl") as "Hl". + wp_pures. awp_apply store_spec. + (* Prove the atomic update for store *) + iApply (aacc_aupd_commit with "AU"); first done. + iIntros (x) "H↦". + iDestruct (pointsto_agree with "Hl H↦") as %[= <-]. + iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl". + { iIntros "[$ $]"; eauto. } + iIntros "$ !>". iSplit; first done. + iIntros "HΦ !>". wp_seq. done. + Qed. + +End increment. + +Section increment_client. + Context `{!heapGS Σ, !spawnG Σ}. + + Local Existing Instance primitive_atomic_heap. + + Definition incr_client : val := + λ: "x", + let: "l" := ref "x" in + incr "l" ||| incr "l". + + Lemma incr_client_safe (x: Z): + ⊢ WP incr_client #x {{ _, True }}. + Proof using Type*. + wp_lam. wp_alloc l as "Hl". + iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto. + (* FIXME: I am only using persistent stuff, so I should be allowed + to move this to the persisten context even without the additional □. *) + iAssert (□ WP incr #l {{ _, True }})%I as "#Aupd". + { iIntros "!>". awp_apply incr_spec. clear x. + iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10. + iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10. + (* The continuation: From after the atomic triple to the postcondition of the WP *) + done. + } + wp_smart_apply wp_par. + - iAssumption. + - iAssumption. + - iIntros (??) "_ !>". done. + Qed. + +End increment_client. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lazy_coin.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lazy_coin.v new file mode 100644 index 0000000000000000000000000000000000000000..141b1955dedcd00e9a940c2c5d9c682270eda0f8 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lazy_coin.v @@ -0,0 +1,69 @@ +From iris.base_logic Require Export invariants. +From iris.program_logic Require Export weakestpre. +From iris.heap_lang Require Export lang proofmode notation. +From iris.heap_lang.lib Require Export nondet_bool. +From iris.prelude Require Import options. + +Definition new_coin: val := λ: <>, (ref NONE, NewProph). + +Definition read_coin : val := + λ: "cp", + let: "c" := Fst "cp" in + let: "p" := Snd "cp" in + match: !"c" with + NONE => let: "r" := nondet_bool #() in + "c" <- SOME "r";; resolve_proph: "p" to: "r";; "r" + | SOME "b" => "b" + end. + +Section proof. + Context `{!heapGS Σ}. + + Definition val_to_bool (v : val) : bool := bool_decide (v = #true). + + Definition prophecy_to_bool (vs : list (val * val)) : bool := + default false (val_to_bool ∘ snd <$> head vs). + + Lemma prophecy_to_bool_of_bool (b : bool) v vs : + prophecy_to_bool ((v, #b) :: vs) = b. + Proof. by destruct b. Qed. + + Definition coin (cp : val) (b : bool) : iProp Σ := + ∃ (c : loc) (p : proph_id) (vs : list (val * val)), + ⌜cp = (#c, #p)%V⌝ ∗ proph p vs ∗ + (c ↦ SOMEV #b ∨ (c ↦ NONEV ∗ ⌜b = prophecy_to_bool vs⌝)). + + Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c b, RET c; coin c b }}}. + Proof. + iIntros (Φ) "_ HΦ". + wp_lam. + wp_apply wp_new_proph; first done. + iIntros (vs p) "Hp". + wp_alloc c as "Hc". + wp_pair. + iApply ("HΦ" $! (#c, #p)%V ). + rewrite /coin; eauto 10 with iFrame. + Qed. + + Lemma read_coin_spec cp b : + {{{ coin cp b }}} read_coin cp {{{ RET #b; coin cp b }}}. + Proof. + iIntros (Φ) "Hc HΦ". + iDestruct "Hc" as (c p vs ->) "[Hp [Hc | [Hc ->]]]". + - wp_lam. wp_load. wp_match. + iApply "HΦ". + rewrite /coin; eauto 10 with iFrame. + - wp_lam. wp_load. wp_match. + wp_apply nondet_bool_spec; first done. + iIntros (r) "_". + wp_let. + wp_store. + wp_apply (wp_resolve_proph with "[Hp]"); first done. + iIntros (ws) "[-> Hws]". + rewrite !prophecy_to_bool_of_bool. + wp_seq. + iApply "HΦ". + rewrite /coin; eauto 10 with iFrame. + Qed. + +End proof. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lazy_coin.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lazy_coin.vo new file mode 100644 index 0000000000000000000000000000000000000000..b128b685e1c0a39d8e869130fdf6d8f87667581d Binary files /dev/null and b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lazy_coin.vo differ diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lock.v b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lock.v new file mode 100644 index 0000000000000000000000000000000000000000..d7010e93c6c29c36438ff7a831a279b82269aa86 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/lock.v @@ -0,0 +1,72 @@ +From iris.base_logic.lib Require Export invariants. +From iris.heap_lang Require Import proofmode notation. +From iris.prelude Require Import options. + +(** A general interface for a lock. + +All parameters are implicit, since it is expected that there is only one +[heapGS_gen] in scope that could possibly apply. + +Only one instance of this class should ever be in scope. To write a library that +is generic over the lock, just add a [`{!lock}] implicit parameter around the +code and [`{!lockG Σ}] around the proofs. To use a particular lock instance, use +[Local Existing Instance ]. + +When writing an instance of this class, please take care not to shadow the class +projections (e.g., either use [Local Definition newlock] or avoid the name +[newlock] altogether), and do not register an instance -- just make it a +[Definition] that others can register later. *) +Class lock := Lock { + (** * Operations *) + newlock : val; + acquire : val; + release : val; + (** * Ghost state *) + (** The assumptions about [Σ] *) + lockG : gFunctors → Type; + (** [name] is used to associate [locked] with [is_lock] *) + lock_name : Type; + (** * Predicates *) + (** No namespace [N] parameter because we only expose program specs, which + anyway have the full mask. *) + is_lock `{!heapGS_gen hlc Σ} {L : lockG Σ} (γ: lock_name) (lock: val) (R: iProp Σ) : iProp Σ; + locked `{!heapGS_gen hlc Σ} {L : lockG Σ} (γ: lock_name) : iProp Σ; + (** * General properties of the predicates *) + #[global] is_lock_persistent `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R :: + Persistent (is_lock (L:=L) γ lk R); + is_lock_iff `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R1 R2 : + is_lock (L:=L) γ lk R1 -∗ ▷ □ (R1 ∗-∗ R2) -∗ is_lock (L:=L) γ lk R2; + #[global] locked_timeless `{!heapGS_gen hlc Σ} {L : lockG Σ} γ :: + Timeless (locked (L:=L) γ); + locked_exclusive `{!heapGS_gen hlc Σ} {L : lockG Σ} γ : + locked (L:=L) γ -∗ locked (L:=L) γ -∗ False; + (** * Program specs *) + newlock_spec `{!heapGS_gen hlc Σ} {L : lockG Σ} (R : iProp Σ) : + {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock (L:=L) γ lk R }}}; + acquire_spec `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R : + {{{ is_lock (L:=L) γ lk R }}} acquire lk {{{ RET #(); locked (L:=L) γ ∗ R }}}; + release_spec `{!heapGS_gen hlc Σ} {L : lockG Σ} γ lk R : + {{{ is_lock (L:=L) γ lk R ∗ locked (L:=L) γ ∗ R }}} release lk {{{ RET #(); True }}} +}. + +Global Arguments newlock : simpl never. +Global Arguments acquire : simpl never. +Global Arguments release : simpl never. +Global Arguments is_lock : simpl never. +Global Arguments locked : simpl never. + +Existing Class lockG. +Global Hint Mode lockG + + : typeclass_instances. +Global Hint Extern 0 (lockG _) => progress simpl : typeclass_instances. + +Global Instance is_lock_contractive `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk : + Contractive (is_lock γ lk). +Proof. + apply (uPred.contractive_internal_eq (M:=iResUR Σ)). + iIntros (P Q) "#HPQ". iApply prop_ext. iIntros "!>". + iSplit; iIntros "H"; iApply (is_lock_iff with "H"); + iNext; iRewrite "HPQ"; auto. +Qed. + +Global Instance is_lock_proper `{!heapGS_gen hlc Σ, !lock, !lockG Σ} γ lk : + Proper ((≡) ==> (≡)) (is_lock γ lk) := ne_proper _. diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/spin_lock.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/spin_lock.vo new file mode 100644 index 0000000000000000000000000000000000000000..de5dfc19022e903081989b864733e51507a2d8d4 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/spin_lock.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:e389aefc2cfdc66da1870a8ae94e8e8ad59a6e3feb604b752bec16c8e971bf6f +size 100220 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/ticket_lock.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/ticket_lock.vo new file mode 100644 index 0000000000000000000000000000000000000000..2490bfc0a7afacf293bcc62c75f5b7d6af122494 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/ticket_lock.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:91ebb738f774532c4c2865221765d2c82dbe3bfaff115b85e19bf0231d7dac40 +size 201710 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/program_logic/adequacy.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/program_logic/adequacy.vo new file mode 100644 index 0000000000000000000000000000000000000000..347d66ed91ff657b354bc45fe0cef1751e02040a --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/program_logic/adequacy.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:f671389ef735bbd4dade07f9814e20dfdea18717d82276c61292f903602ff381 +size 291768 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/qpoly.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/qpoly.vo new file mode 100644 index 0000000000000000000000000000000000000000..b96cc27e34a3529d04e7e11e6ba75dc6f6c17e50 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/qpoly.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:43b3bba30dd373742dacfff0b4e7cebabcf06e59b453b2b6b0307f35ef8134d5 +size 480082 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/rat.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/rat.vo new file mode 100644 index 0000000000000000000000000000000000000000..e8eb1f6deb71635518171a6642e65125acfe9e06 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/rat.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:22948896e880f9bade457be575b67e7a114ba86b5960b36759ff7d1da48bdc65 +size 449183 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/automorphism.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/automorphism.vo new file mode 100644 index 0000000000000000000000000000000000000000..5749d9888249ae410aba2f11f5cf5d43e439c3a3 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/automorphism.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:1c70ee7d1cf841be77a892cc7f52907af5da9e17483a63d573e741c1c27ff7d6 +size 167435 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/fingroup.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/fingroup.vo new file mode 100644 index 0000000000000000000000000000000000000000..8fe51c1a653aeaf3af698905b400eecacc835ee9 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/fingroup.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:52cacd8f7a921b9ee527b6a8f5d635f680c098b59996c8c8bfaf8a430d25254d +size 1018508 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gfunctor.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gfunctor.vo new file mode 100644 index 0000000000000000000000000000000000000000..7dac8e87148756d33747f2ae50ee9473f5bbf771 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gfunctor.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:43a8a701099c546dffd93d241cc49b223a273a0a6064285b7877cadaf53d4e5e +size 128815 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gseries.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gseries.vo new file mode 100644 index 0000000000000000000000000000000000000000..f199e765bdaedc03c610989186833c3c12bfc53c --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gseries.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:7115c14a4980bd41028f073bcbcb5d4fbfc3e7b8b9ee997123f1a16810d1dd68 +size 202662 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/hall.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/hall.vo new file mode 100644 index 0000000000000000000000000000000000000000..4e360c5b53878fb9f76bb2ef43d6796c37790a02 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/hall.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:193473c54f14d3c2b4ef7541c6ad021a816adde12e56ac907d55fc7abe72ad5e +size 435296 diff --git a/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/jordanholder.vo b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/jordanholder.vo new file mode 100644 index 0000000000000000000000000000000000000000..b241334d0f074bbcbb017b775abed7dd843e7a10 --- /dev/null +++ b/backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/jordanholder.vo @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:f8cfb1b13e95335828f3a0691cbd606435cd9e8ff773ae9527b26f8178981540 +size 237235 diff --git a/backend/core/ag4masses/alphageometry/numericals_test.py b/backend/core/ag4masses/alphageometry/numericals_test.py new file mode 100644 index 0000000000000000000000000000000000000000..0780df4118aa11195ebf71bd88e9df28f96bd1bc --- /dev/null +++ b/backend/core/ag4masses/alphageometry/numericals_test.py @@ -0,0 +1,313 @@ +# Copyright 2023 DeepMind Technologies Limited +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +# ============================================================================== + +"""Unit testing for the geometry numericals code.""" + +import unittest + +from absl.testing import absltest +import numericals as nm + +np = nm.np + +unif = nm.unif +Point = nm.Point +Line = nm.Line +Circle = nm.Circle +HalfLine = nm.HalfLine + +line_circle_intersection = nm.line_circle_intersection +line_line_intersection = nm.line_line_intersection + +check_coll = nm.check_coll +check_eqangle = nm.check_eqangle + +random_points = nm.random_points +ang_between = nm.ang_between +head_from = nm.head_from + + +class NumericalTest(unittest.TestCase): + + def test_sketch_ieq_triangle(self): + a, b, c = nm.sketch_ieq_triangle([]) + self.assertAlmostEqual(a.distance(b), b.distance(c)) + self.assertAlmostEqual(c.distance(a), b.distance(c)) + + def test_sketch_2l1c(self): + p = nm.Point(0.0, 0.0) + pi = np.pi + anga = unif(-0.4 * pi, 0.4 * pi) + a = Point(np.cos(anga), np.sin(anga)) + angb = unif(0.6 * pi, 1.4 * pi) + b = Point(np.cos(angb), np.sin(angb)) + + angc = unif(anga + 0.05 * pi, angb - 0.05 * pi) + c = Point(np.cos(angc), np.sin(angc)) * unif(0.2, 0.8) + + x, y, z, i = nm.sketch_2l1c([a, b, c, p]) + self.assertTrue(check_coll([x, c, a])) + self.assertTrue(check_coll([y, c, b])) + self.assertAlmostEqual(z.distance(p), 1.0) + self.assertTrue(check_coll([p, i, z])) + self.assertTrue(Line(i, x).is_perp(Line(c, a))) + self.assertTrue(Line(i, y).is_perp(Line(c, b))) + self.assertAlmostEqual(i.distance(x), i.distance(y)) + self.assertAlmostEqual(i.distance(x), i.distance(z)) + + def test_sketch_3peq(self): + a, b, c = random_points(3) + x, y, z = nm.sketch_3peq([a, b, c]) + + self.assertTrue(check_coll([a, b, x])) + self.assertTrue(check_coll([a, c, y])) + self.assertTrue(check_coll([b, c, z])) + self.assertTrue(check_coll([x, y, z])) + self.assertAlmostEqual(z.distance(x), z.distance(y)) + + def test_sketch_aline(self): + a, b, c, d, e = random_points(5) + ex = nm.sketch_aline([a, b, c, d, e]) + self.assertIsInstance(ex, HalfLine) + self.assertEqual(ex.tail, e) + x = ex.head + self.assertAlmostEqual(ang_between(b, a, c), ang_between(e, d, x)) + + def test_sketch_amirror(self): + a, b, c = random_points(3) + bx = nm.sketch_amirror([a, b, c]) + self.assertIsInstance(bx, HalfLine) + assert bx.tail == b + x = bx.head + + ang1 = ang_between(b, a, c) + ang2 = ang_between(b, c, x) + self.assertAlmostEqual(ang1, ang2) + + def test_sketch_bisect(self): + a, b, c = random_points(3) + line = nm.sketch_bisect([a, b, c]) + self.assertAlmostEqual(b.distance(line), 0.0) + + l = a.perpendicular_line(line) + x = line_line_intersection(l, Line(b, c)) + self.assertAlmostEqual(a.distance(line), x.distance(line)) + + d, _ = line_circle_intersection(line, Circle(b, radius=1)) + ang1 = ang_between(b, a, d) + ang2 = ang_between(b, d, c) + self.assertAlmostEqual(ang1, ang2) + + def test_sketch_bline(self): + a, b = random_points(2) + l = nm.sketch_bline([a, b]) + self.assertTrue(Line(a, b).is_perp(l)) + self.assertAlmostEqual(a.distance(l), b.distance(l)) + + def test_sketch_cc_tangent(self): + o = Point(0.0, 0.0) + w = Point(1.0, 0.0) + + ra = unif(0.0, 0.6) + rb = unif(0.4, 1.0) + + a = unif(0.0, np.pi) + b = unif(0.0, np.pi) + + a = o + ra * Point(np.cos(a), np.sin(a)) + b = w + rb * Point(np.sin(b), np.cos(b)) + + x, y, z, t = nm.sketch_cc_tangent([o, a, w, b]) + xy = Line(x, y) + zt = Line(z, t) + self.assertAlmostEqual(o.distance(xy), o.distance(a)) + self.assertAlmostEqual(o.distance(zt), o.distance(a)) + self.assertAlmostEqual(w.distance(xy), w.distance(b)) + self.assertAlmostEqual(w.distance(zt), w.distance(b)) + + def test_sketch_circle(self): + a, b, c = random_points(3) + circle = nm.sketch_circle([a, b, c]) + self.assertAlmostEqual(circle.center.distance(a), 0.0) + self.assertAlmostEqual(circle.radius, b.distance(c)) + + def test_sketch_e5128(self): + b = Point(0.0, 0.0) + c = Point(0.0, 1.0) + ang = unif(-np.pi / 2, 3 * np.pi / 2) + d = head_from(c, ang, 1.0) + a = Point(unif(0.5, 2.0), 0.0) + + e, g = nm.sketch_e5128([a, b, c, d]) + ang1 = ang_between(a, b, d) + ang2 = ang_between(e, a, g) + self.assertAlmostEqual(ang1, ang2) + + def test_sketch_eq_quadrangle(self): + a, b, c, d = nm.sketch_eq_quadrangle([]) + self.assertAlmostEqual(a.distance(d), c.distance(b)) + ac = Line(a, c) + assert ac.diff_side(b, d), (ac(b), ac(d)) + bd = Line(b, d) + assert bd.diff_side(a, c), (bd(a), bd(c)) + + def test_sketch_eq_trapezoid(self): + a, b, c, d = nm.sketch_eq_trapezoid([]) + assert Line(a, b).is_parallel(Line(c, d)) + self.assertAlmostEqual(a.distance(d), b.distance(c)) + + def test_sketch_eqangle3(self): + points = random_points(5) + x = nm.sketch_eqangle3(points).sample_within(points)[0] + a, b, d, e, f = points + self.assertTrue(check_eqangle([x, a, x, b, d, e, d, f])) + + def test_sketch_eqangle2(self): + a, b, c = random_points(3) + x = nm.sketch_eqangle2([a, b, c]) + ang1 = ang_between(a, b, x) + ang2 = ang_between(c, x, b) + self.assertAlmostEqual(ang1, ang2) + + def test_sketch_edia_quadrangle(self): + a, b, c, d = nm.sketch_eqdia_quadrangle([]) + assert Line(a, c).diff_side(b, d) + assert Line(b, d).diff_side(a, c) + self.assertAlmostEqual(a.distance(c), b.distance(d)) + + def test_sketch_isos(self): + a, b, c = nm.sketch_isos([]) + self.assertAlmostEqual(a.distance(b), a.distance(c)) + self.assertAlmostEqual(ang_between(b, a, c), ang_between(c, b, a)) + + def test_sketch_quadrange(self): + a, b, c, d = nm.sketch_quadrangle([]) + self.assertTrue(Line(a, c).diff_side(b, d)) + self.assertTrue(Line(b, d).diff_side(a, c)) + + def test_sketch_r_trapezoid(self): + a, b, c, d = nm.sketch_r_trapezoid([]) + self.assertTrue(Line(a, b).is_perp(Line(a, d))) + self.assertTrue(Line(a, b).is_parallel(Line(c, d))) + self.assertTrue(Line(a, c).diff_side(b, d)) + self.assertTrue(Line(b, d).diff_side(a, c)) + + def test_sketch_r_triangle(self): + a, b, c = nm.sketch_r_triangle([]) + self.assertTrue(Line(a, b).is_perp(Line(a, c))) + + def test_sketch_rectangle(self): + a, b, c, d = nm.sketch_rectangle([]) + self.assertTrue(Line(a, b).is_perp(Line(b, c))) + self.assertTrue(Line(b, c).is_perp(Line(c, d))) + self.assertTrue(Line(c, d).is_perp(Line(d, a))) + + def test_sketch_reflect(self): + a, b, c = random_points(3) + x = nm.sketch_reflect([a, b, c]) + self.assertTrue(Line(a, x).is_perp(Line(b, c))) + self.assertAlmostEqual(x.distance(Line(b, c)), a.distance(Line(b, c))) + + def test_sketch_risos(self): + a, b, c = nm.sketch_risos([]) + self.assertAlmostEqual(a.distance(b), a.distance(c)) + self.assertTrue(Line(a, b).is_perp(Line(a, c))) + + def test_sketch_rotaten90(self): + a, b = random_points(2) + x = nm.sketch_rotaten90([a, b]) + self.assertAlmostEqual(a.distance(x), a.distance(b)) + self.assertTrue(Line(a, x).is_perp(Line(a, b))) + d = Point(0.0, 0.0) + e = Point(0.0, 1.0) + f = Point(1.0, 0.0) + self.assertAlmostEqual(ang_between(d, e, f), ang_between(a, b, x)) + + def test_sketch_rotatep90(self): + a, b = random_points(2) + x = nm.sketch_rotatep90([a, b]) + self.assertAlmostEqual(a.distance(x), a.distance(b)) + self.assertTrue(Line(a, x).is_perp(Line(a, b))) + d = Point(0.0, 0.0) + e = Point(0.0, 1.0) + f = Point(1.0, 0.0) + self.assertAlmostEqual(ang_between(d, f, e), ang_between(a, b, x)) + + def test_sketch_s_angle(self): + a, b = random_points(2) + y = unif(0.0, np.pi) + bx = nm.sketch_s_angle([a, b, y / np.pi * 180]) + self.assertIsInstance(bx, HalfLine) + self.assertEqual(bx.tail, b) + x = bx.head + + d = Point(1.0, 0.0) + e = Point(0.0, 0.0) + f = Point(np.cos(y), np.sin(y)) + self.assertAlmostEqual(ang_between(e, d, f), ang_between(b, a, x)) + + def test_sketch_shift(self): + a, b, c = random_points(3) + x = nm.sketch_shift([a, b, c]) + self.assertTrue((b - a).close(x - c)) + + def test_sketch_square(self): + a, b = random_points(2) + c, d = nm.sketch_square([a, b]) + self.assertTrue(Line(a, b).is_perp(Line(b, c))) + self.assertTrue(Line(b, c).is_perp(Line(c, d))) + self.assertTrue(Line(c, d).is_perp(Line(d, a))) + self.assertAlmostEqual(a.distance(b), b.distance(c)) + + def test_sketch_isquare(self): + a, b, c, d = nm.sketch_isquare([]) + self.assertTrue(Line(a, b).is_perp(Line(b, c))) + self.assertTrue(Line(b, c).is_perp(Line(c, d))) + self.assertTrue(Line(c, d).is_perp(Line(d, a))) + self.assertAlmostEqual(a.distance(b), b.distance(c)) + + def test_sketch_trapezoid(self): + a, b, c, d = nm.sketch_trapezoid([]) + self.assertTrue(Line(a, b).is_parallel(Line(c, d))) + self.assertTrue(Line(a, c).diff_side(b, d)) + self.assertTrue(Line(b, d).diff_side(a, c)) + + def test_sketch_triangle(self): + a, b, c = nm.sketch_triangle([]) + self.assertFalse(check_coll([a, b, c])) + + def test_sketch_triangle12(self): + a, b, c = nm.sketch_triangle12([]) + self.assertAlmostEqual(a.distance(b) * 2, a.distance(c)) + + def test_sketch_trisect(self): + a, b, c = random_points(3) + x, y = nm.sketch_trisect([a, b, c]) + self.assertAlmostEqual(ang_between(b, a, x), ang_between(b, x, y)) + self.assertAlmostEqual(ang_between(b, x, y), ang_between(b, y, c)) + self.assertAlmostEqual(ang_between(b, a, x) * 3, ang_between(b, a, c)) + + def test_sketch_trisegment(self): + a, b = random_points(2) + x, y = nm.sketch_trisegment([a, b]) + self.assertAlmostEqual( + a.distance(x) + x.distance(y) + y.distance(b), a.distance(b) + ) + self.assertAlmostEqual(a.distance(x), x.distance(y)) + self.assertAlmostEqual(x.distance(y), y.distance(b)) + + +if __name__ == '__main__': + absltest.main() diff --git a/backend/core/ag4masses/alphageometry/pretty.py b/backend/core/ag4masses/alphageometry/pretty.py new file mode 100644 index 0000000000000000000000000000000000000000..cd69b029be07f4ba4499a58cfd70703f9125b3b8 --- /dev/null +++ b/backend/core/ag4masses/alphageometry/pretty.py @@ -0,0 +1,216 @@ +# Copyright 2023 DeepMind Technologies Limited +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +# ============================================================================== + +"""Utilities for string manipulation in the DSL.""" + +MAP_SYMBOL = { + 'T': 'perp', + 'P': 'para', + 'D': 'cong', + 'S': 'simtri', + 'I': 'circle', + 'M': 'midp', + 'O': 'cyclic', + 'C': 'coll', + '^': 'eqangle', + '/': 'eqratio', + '%': 'eqratio', + '=': 'contri', + 'X': 'collx', + 'A': 'acompute', + 'R': 'rcompute', + 'Q': 'fixc', + 'E': 'fixl', + 'V': 'fixb', + 'H': 'fixt', + 'Z': 'fixp', + 'Y': 'ind', +} + + +def map_symbol(c: str) -> str: + return MAP_SYMBOL[c] + + +def map_symbol_inv(c: str) -> str: + return {v: k for k, v in MAP_SYMBOL.items()}[c] + + +def _gcd(x: int, y: int) -> int: + while y: + x, y = y, x % y + return x + + +def simplify(n: int, d: int) -> tuple[int, int]: + g = _gcd(n, d) + return (n // g, d // g) + + +def pretty2r(a: str, b: str, c: str, d: str) -> str: + if b in (c, d): + a, b = b, a + + if a == d: + c, d = d, c + + return f'{a} {b} {c} {d}' + + +def pretty2a(a: str, b: str, c: str, d: str) -> str: + if b in (c, d): + a, b = b, a + + if a == d: + c, d = d, c + + return f'{a} {b} {c} {d}' + + +def pretty_angle(a: str, b: str, c: str, d: str) -> str: + if b in (c, d): + a, b = b, a + if a == d: + c, d = d, c + + if a == c: + return f'\u2220{b}{a}{d}' + return f'\u2220({a}{b}-{c}{d})' + + +def pretty_nl(name: str, args: list[str]) -> str: + """Natural lang formatting a predicate.""" + if name == 'aconst': + a, b, c, d, y = args + return f'{pretty_angle(a, b, c, d)} = {y}' + if name == 'rconst': + a, b, c, d, y = args + return f'{a}{b}:{c}{d} = {y}' + if name == 'acompute': + a, b, c, d = args + return f'{pretty_angle(a, b, c, d)}' + if name in ['coll', 'C']: + return '' + ','.join(args) + ' are collinear' + if name == 'collx': + return '' + ','.join(list(set(args))) + ' are collinear' + if name in ['cyclic', 'O']: + return '' + ','.join(args) + ' are concyclic' + if name in ['midp', 'midpoint', 'M']: + x, a, b = args + return f'{x} is midpoint of {a}{b}' + if name in ['eqangle', 'eqangle6', '^']: + a, b, c, d, e, f, g, h = args + return f'{pretty_angle(a, b, c, d)} = {pretty_angle(e, f, g, h)}' + if name in ['eqratio', 'eqratio6', '/']: + return '{}{}:{}{} = {}{}:{}{}'.format(*args) + if name == 'eqratio3': + a, b, c, d, o, o = args # pylint: disable=redeclared-assigned-name + return f'S {o} {a} {b} {o} {c} {d}' + if name in ['cong', 'D']: + a, b, c, d = args + return f'{a}{b} = {c}{d}' + if name in ['perp', 'T']: + if len(args) == 2: # this is algebraic derivation. + ab, cd = args # ab = 'd( ... )' + return f'{ab} \u27c2 {cd}' + a, b, c, d = args + return f'{a}{b} \u27c2 {c}{d}' + if name in ['para', 'P']: + if len(args) == 2: # this is algebraic derivation. + ab, cd = args # ab = 'd( ... )' + return f'{ab} \u2225 {cd}' + a, b, c, d = args + return f'{a}{b} \u2225 {c}{d}' + if name in ['simtri2', 'simtri', 'simtri*']: + a, b, c, x, y, z = args + return f'\u0394{a}{b}{c} is similar to \u0394{x}{y}{z}' + if name in ['contri2', 'contri', 'contri*']: + a, b, c, x, y, z = args + return f'\u0394{a}{b}{c} is congruent to \u0394{x}{y}{z}' + if name in ['circle', 'I']: + o, a, b, c = args + return f'{o} is the circumcenter of \\Delta {a}{b}{c}' + if name == 'foot': + a, b, c, d = args + return f'{a} is the foot of {b} on {c}{d}' + + +def pretty(txt: str) -> str: + """Pretty formating a predicate string.""" + if isinstance(txt, str): + txt = txt.split(' ') + name, *args = txt + if name == 'ind': + return 'Y ' + ' '.join(args) + if name in ['fixc', 'fixl', 'fixb', 'fixt', 'fixp']: + return map_symbol_inv(name) + ' ' + ' '.join(args) + if name == 'acompute': + a, b, c, d = args + return 'A ' + ' '.join(args) + if name == 'rcompute': + a, b, c, d = args + return 'R ' + ' '.join(args) + if name == 'aconst': + a, b, c, d, y = args + return f'^ {pretty2a(a, b, c, d)} {y}' + if name == 'rconst': + a, b, c, d, y = args + return f'/ {pretty2r(a, b, c, d)} {y}' + if name == 'coll': + return 'C ' + ' '.join(args) + if name == 'collx': + return 'X ' + ' '.join(args) + if name == 'cyclic': + return 'O ' + ' '.join(args) + if name in ['midp', 'midpoint']: + x, a, b = args + return f'M {x} {a} {b}' + if name == 'eqangle': + a, b, c, d, e, f, g, h = args + return f'^ {pretty2a(a, b, c, d)} {pretty2a(e, f, g, h)}' + if name == 'eqratio': + a, b, c, d, e, f, g, h = args + return f'/ {pretty2r(a, b, c, d)} {pretty2r(e, f, g, h)}' + if name == 'eqratio3': + a, b, c, d, o, o = args # pylint: disable=redeclared-assigned-name + return f'S {o} {a} {b} {o} {c} {d}' + if name == 'cong': + a, b, c, d = args + return f'D {a} {b} {c} {d}' + if name == 'perp': + if len(args) == 2: # this is algebraic derivation. + ab, cd = args # ab = 'd( ... )' + return f'T {ab} {cd}' + a, b, c, d = args + return f'T {a} {b} {c} {d}' + if name == 'para': + if len(args) == 2: # this is algebraic derivation. + ab, cd = args # ab = 'd( ... )' + return f'P {ab} {cd}' + a, b, c, d = args + return f'P {a} {b} {c} {d}' + if name in ['simtri2', 'simtri', 'simtri*']: + a, b, c, x, y, z = args + return f'S {a} {b} {c} {x} {y} {z}' + if name in ['contri2', 'contri', 'contri*']: + a, b, c, x, y, z = args + return f'= {a} {b} {c} {x} {y} {z}' + if name == 'circle': + o, a, b, c = args + return f'I {o} {a} {b} {c}' + if name == 'foot': + a, b, c, d = args + return f'F {a} {b} {c} {d}' + return ' '.join(txt) diff --git a/backend/core/ag4masses/alphageometry/problem.py b/backend/core/ag4masses/alphageometry/problem.py new file mode 100644 index 0000000000000000000000000000000000000000..82ed76aa4e80317d3690caebf93adcf231a42a3c --- /dev/null +++ b/backend/core/ag4masses/alphageometry/problem.py @@ -0,0 +1,1133 @@ +# Copyright 2023 DeepMind Technologies Limited +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +# ============================================================================== + +"""Implements objects to represent problems, theorems, proofs, traceback.""" + +from __future__ import annotations + +from collections import defaultdict # pylint: disable=g-importing-member +from typing import Any + +import geometry as gm +import pretty as pt + + +# pylint: disable=protected-access +# pylint: disable=unused-variable +# pylint: disable=unused-argument +# pylint: disable=unused-assignment + + +def reshape(l: list[Any], n: int = 1) -> list[list[Any]]: + assert len(l) % n == 0 + columns = [[] for i in range(n)] + for i, x in enumerate(l): + columns[i % n].append(x) + return zip(*columns) + + +def isint(x: str) -> bool: + try: + int(x) + return True + except: # pylint: disable=bare-except + return False + + +class Construction: + """One predicate.""" + + @classmethod + def from_txt(cls, data: str) -> Construction: + data = data.split(' ') + return Construction(data[0], data[1:]) + + def __init__(self, name: str, args: list[str]): + self.name = name + self.args = args + + def translate(self, mapping: dict[str, str]) -> Construction: + args = [a if isint(a) else mapping[a] for a in self.args] + return Construction(self.name, args) + + def txt(self) -> str: + return ' '.join([self.name] + list(self.args)) + + +class Clause: + """One construction (>= 1 predicate).""" + + @classmethod + def from_txt(cls, data: str) -> Clause: + if data == ' =': + return Clause([], []) + points, constructions = data.split(' = ') + return Clause( + points.split(' '), + [Construction.from_txt(c) for c in constructions.split(', ')], + ) + + def __init__(self, points: list[str], constructions: list[Construction]): + self.points = [] + self.nums = [] + + for p in points: + num = None + if isinstance(p, str) and '@' in p: + p, num = p.split('@') + x, y = num.split('_') + num = float(x), float(y) + self.points.append(p) + self.nums.append(num) + + self.constructions = constructions + + def translate(self, mapping: dict[str, str]) -> Clause: + points0 = [] + for p in self.points: + pcount = len(mapping) + 1 + name = chr(96 + pcount) + if name > 'z': # pcount = 26 -> name = 'z' + name = chr(97 + (pcount - 1) % 26) + str((pcount - 1) // 26) + + p0 = mapping.get(p, name) + mapping[p] = p0 + points0.append(p0) + return Clause(points0, [c.translate(mapping) for c in self.constructions]) + + def add(self, name: str, args: list[str]) -> None: + self.constructions.append(Construction(name, args)) + + def txt(self) -> str: + return ( + ' '.join(self.points) + + ' = ' + + ', '.join(c.txt() for c in self.constructions) + ) + + +def _gcd(x: int, y: int) -> int: + while y: + x, y = y, x % y + return x + + +def simplify(n: int, d: int) -> tuple[int, int]: + g = _gcd(n, d) + return (n // g, d // g) + + +def compare_fn(dep: Dependency) -> tuple[Dependency, str]: + return (dep, pt.pretty(dep)) + + +def sort_deps(deps: list[Dependency]) -> list[Dependency]: + return sorted(deps, key=compare_fn) + + +class Problem: + """Describe one problem to solve.""" + + @classmethod + def from_txt_file( + cls, fname: str, to_dict: bool = False, translate: bool = True + ): + """Load a problem from a text file.""" + with open(fname, 'r') as f: + lines = f.read().split('\n') + + lines = [l for l in lines if l] + data = [ + cls.from_txt(url + '\n' + problem, translate) + for (url, problem) in reshape(lines, 2) + ] + if to_dict: + return cls.to_dict(data) + return data + + @classmethod + def from_txt(cls, data: str, translate: bool = True) -> Problem: + """Load a problem from a str object.""" + url = '' + if '\n' in data: + url, data = data.split('\n') + + if ' ? ' in data: + clauses, goal = data.split(' ? ') + goal = Construction.from_txt(goal) + else: + clauses, goal = data, None + + clauses = clauses.split('; ') + problem = Problem( + url=url, clauses=[Clause.from_txt(c) for c in clauses], goal=goal + ) + if translate: + return problem.translate() + return problem + + @classmethod + def to_dict(cls, data: list[Problem]) -> dict[str, Problem]: + return {p.url: p for p in data} + + def __init__(self, url: str, clauses: list[Clause], goal: Construction): + self.url = url + self.clauses = clauses + self.goal = goal + + def copy(self) -> Problem: + return Problem(self.url, list(self.clauses), self.goal) + + def translate(self) -> Problem: # to single-char point names + """Translate point names into alphabetical.""" + mapping = {} + clauses = [] + + for clause in self.clauses: + clauses.append(clause.translate(mapping)) + + if self.goal: + goal = self.goal.translate(mapping) + else: + goal = self.goal + + p = Problem(self.url, clauses, goal) + p.mapping = mapping + return p + + def txt(self) -> str: + return ( + '; '.join([c.txt() for c in self.clauses]) + ' ? ' + self.goal.txt() + if self.goal + else '' + ) + + def setup_str_from_problem(self, definitions: list[Definition]) -> str: + """Construct the string from Problem object.""" + ref = 0 + + string = [] + for clause in self.clauses: + group = {} + p2deps = defaultdict(list) + for c in clause.constructions: + cdef = definitions[c.name] + + if len(c.args) != len(cdef.construction.args): + assert len(c.args) + len(clause.points) == len(cdef.construction.args) + c.args = clause.points + c.args + + mapping = dict(zip(cdef.construction.args, c.args)) + for points, bs in cdef.basics: + points = tuple([mapping[x] for x in points]) + for p in points: + group[p] = points + + for b in bs: + args = [mapping[a] for a in b.args] + name = b.name + if b.name in ['s_angle', 'aconst']: + x, y, z, v = args + name = 'aconst' + v = int(v) + + if v < 0: + v = -v + x, z = z, x + + m, n = simplify(int(v), 180) + args = [y, z, y, x, f'{m}pi/{n}'] + + p2deps[points].append(hashed_txt(name, args)) + + for k, v in p2deps.items(): + p2deps[k] = sort_deps(v) + + points = clause.points + while points: + p = points[0] + gr = group[p] + points = [x for x in points if x not in gr] + + deps_str = [] + for dep in p2deps[gr]: + ref_str = '{:02}'.format(ref) + dep_str = pt.pretty(dep) + + if dep[0] == 'aconst': + m, n = map(int, dep[-1].split('pi/')) + mn = f'{m}. pi / {n}.' + dep_str = ' '.join(dep_str.split()[:-1] + [mn]) + + deps_str.append(dep_str + ' ' + ref_str) + ref += 1 + + string.append(' '.join(gr) + ' : ' + ' '.join(deps_str)) + + string = '{S} ' + ' ; '.join([s.strip() for s in string]) + goal = self.goal + string += ' ? ' + pt.pretty([goal.name] + goal.args) + return string + + +def parse_rely(s: str) -> dict[str, str]: + result = {} + if not s: + return result + s = [x.strip() for x in s.split(',')] + for x in s: + a, b = x.split(':') + a, b = a.strip().split(), b.strip().split() + result.update({m: b for m in a}) + return result + + +class Definition: + """Definitions of construction statements.""" + + @classmethod + def from_txt_file(cls, fname: str, to_dict: bool = False) -> Definition: + with open(fname, 'r') as f: + lines = f.read() + return cls.from_string(lines, to_dict) + + @classmethod + def from_string(cls, string: str, to_dict: bool = False) -> Definition: + lines = string.split('\n') + data = [cls.from_txt('\n'.join(group)) for group in reshape(lines, 6)] + if to_dict: + return cls.to_dict(data) + return data + + @classmethod + def to_dict(cls, data: list[Definition]) -> dict[str, Definition]: + return {d.construction.name: d for d in data} + + @classmethod + def from_txt(cls, data: str) -> Definition: + """Load definitions from a str object.""" + construction, rely, deps, basics, numerics, _ = data.split('\n') + basics = [] if not basics else [b.strip() for b in basics.split(';')] + + levels = [] + for bs in basics: + if ':' in bs: + points, bs = bs.split(':') + points = points.strip().split() + else: + points = [] + if bs.strip(): + bs = [Construction.from_txt(b.strip()) for b in bs.strip().split(',')] + else: + bs = [] + levels.append((points, bs)) + + numerics = [] if not numerics else numerics.split(', ') + + return Definition( + construction=Construction.from_txt(construction), + rely=parse_rely(rely), + deps=Clause.from_txt(deps), + basics=levels, + numerics=[Construction.from_txt(c) for c in numerics], + ) + + def __init__( + self, + construction: Construction, + rely: dict[str, str], + deps: Clause, + basics: list[tuple[list[str], list[Construction]]], + numerics: list[Construction], + ): + self.construction = construction + self.rely = rely + self.deps = deps + self.basics = basics + self.numerics = numerics + + args = set() + for num in numerics: + args.update(num.args) + + self.points = [] + self.args = [] + for p in self.construction.args: + if p in args: + self.args.append(p) + else: + self.points.append(p) + + +class Theorem: + """Deduction rule.""" + + @classmethod + def from_txt_file(cls, fname: str, to_dict: bool = False) -> Theorem: + with open(fname, 'r') as f: + theorems = f.read() + return cls.from_string(theorems, to_dict) + + @classmethod + def from_string(cls, string: str, to_dict: bool = False) -> Theorem: + """Load deduction rule from a str object.""" + theorems = string.split('\n') + theorems = [l for l in theorems if l and not l.startswith('#')] + theorems = [cls.from_txt(l) for l in theorems] + + for i, th in enumerate(theorems): + th.rule_name = 'r{:02}'.format(i) + + if to_dict: + result = {} + for t in theorems: + if t.name in result: + t.name += '_' + result[t.rule_name] = t + + return result + + return theorems + + @classmethod + def from_txt(cls, data: str) -> Theorem: + premises, conclusion = data.split(' => ') + premises = premises.split(', ') + conclusion = conclusion.split(', ') + return Theorem( + premise=[Construction.from_txt(p) for p in premises], + conclusion=[Construction.from_txt(c) for c in conclusion], + ) + + def __init__( + self, premise: list[Construction], conclusion: list[Construction] + ): + if len(conclusion) != 1: + raise ValueError('Cannot have more than one conclusion') + self.name = '_'.join([p.name for p in premise + conclusion]) + self.premise = premise + self.conclusion = conclusion + self.is_arg_reduce = False + + assert len(self.conclusion) == 1 + con = self.conclusion[0] + + if con.name in [ + 'eqratio3', + 'midp', + 'contri', + 'simtri', + 'contri2', + 'simtri2', + 'simtri*', + 'contri*', + ]: + return + + prem_args = set(sum([p.args for p in self.premise], [])) + con_args = set(con.args) + if len(prem_args) <= len(con_args): + self.is_arg_reduce = True + + def txt(self) -> str: + premise_txt = ', '.join([clause.txt() for clause in self.premise]) + conclusion_txt = ', '.join([clause.txt() for clause in self.conclusion]) + return f'{premise_txt} => {conclusion_txt}' + + def conclusion_name_args( + self, mapping: dict[str, gm.Point] + ) -> tuple[str, list[gm.Point]]: + mapping = {arg: p for arg, p in mapping.items() if isinstance(arg, str)} + c = self.conclusion[0] + args = [mapping[a] for a in c.args] + return c.name, args + + +def why_eqratio( + d1: gm.Direction, + d2: gm.Direction, + d3: gm.Direction, + d4: gm.Direction, + level: int, +) -> list[Dependency]: + """Why two ratios are equal, returns a Dependency objects.""" + all12 = list(gm.all_ratios(d1, d2, level)) + all34 = list(gm.all_ratios(d3, d4, level)) + + min_why = None + for ang12, d1s, d2s in all12: + for ang34, d3s, d4s in all34: + why0 = gm.why_equal(ang12, ang34, level) + if why0 is None: + continue + d1_, d2_ = ang12._l + d3_, d4_ = ang34._l + why1 = gm.bfs_backtrack(d1, [d1_], d1s) + why2 = gm.bfs_backtrack(d2, [d2_], d2s) + why3 = gm.bfs_backtrack(d3, [d3_], d3s) + why4 = gm.bfs_backtrack(d4, [d4_], d4s) + why = why0 + why1 + why2 + why3 + why4 + if min_why is None or len(why) < len(min_why[0]): + min_why = why, ang12, ang34, why0, why1, why2, why3, why4 + + if min_why is None: + return None + + _, ang12, ang34, why0, why1, why2, why3, why4 = min_why + d1_, d2_ = ang12._l + d3_, d4_ = ang34._l + + if d1 == d1_ and d2 == d2_ and d3 == d3_ and d4 == d4_: + return why0 + + (a_, b_), (c_, d_) = d1_._obj.points, d2_._obj.points + (e_, f_), (g_, h_) = d3_._obj.points, d4_._obj.points + deps = [] + if why0: + dep = Dependency('eqratio', [a_, b_, c_, d_, e_, f_, g_, h_], '', level) + dep.why = why0 + deps.append(dep) + + (a, b), (c, d) = d1._obj.points, d2._obj.points + (e, f), (g, h) = d3._obj.points, d4._obj.points + for why, (x, y), (x_, y_) in zip( + [why1, why2, why3, why4], + [(a, b), (c, d), (e, f), (g, h)], + [(a_, b_), (c_, d_), (e_, f_), (g_, h_)], + ): + if why: + dep = Dependency('cong', [x, y, x_, y_], '', level) + dep.why = why + deps.append(dep) + + return deps + + +def why_eqangle( + d1: gm.Direction, + d2: gm.Direction, + d3: gm.Direction, + d4: gm.Direction, + level: int, + verbose: bool = False, +) -> list[Dependency]: + """Why two angles are equal, returns a Dependency objects.""" + all12 = list(gm.all_angles(d1, d2, level)) + all34 = list(gm.all_angles(d3, d4, level)) + + min_why = None + for ang12, d1s, d2s in all12: + for ang34, d3s, d4s in all34: + why0 = gm.why_equal(ang12, ang34, level) + if why0 is None: + continue + d1_, d2_ = ang12._d + d3_, d4_ = ang34._d + why1 = gm.bfs_backtrack(d1, [d1_], d1s) + why2 = gm.bfs_backtrack(d2, [d2_], d2s) + why3 = gm.bfs_backtrack(d3, [d3_], d3s) + why4 = gm.bfs_backtrack(d4, [d4_], d4s) + why = why0 + why1 + why2 + why3 + why4 + if min_why is None or len(why) < len(min_why[0]): + min_why = why, ang12, ang34, why0, why1, why2, why3, why4 + + if min_why is None: + return None + + _, ang12, ang34, why0, why1, why2, why3, why4 = min_why + why0 = gm.why_equal(ang12, ang34, level) + d1_, d2_ = ang12._d + d3_, d4_ = ang34._d + + if d1 == d1_ and d2 == d2_ and d3 == d3_ and d4 == d4_: + return (d1_, d2_, d3_, d4_), why0 + + (a_, b_), (c_, d_) = d1_._obj.points, d2_._obj.points + (e_, f_), (g_, h_) = d3_._obj.points, d4_._obj.points + deps = [] + if why0: + dep = Dependency('eqangle', [a_, b_, c_, d_, e_, f_, g_, h_], '', None) + dep.why = why0 + deps.append(dep) + + (a, b), (c, d) = d1._obj.points, d2._obj.points + (e, f), (g, h) = d3._obj.points, d4._obj.points + for why, d_xy, (x, y), d_xy_, (x_, y_) in zip( + [why1, why2, why3, why4], + [d1, d2, d3, d4], + [(a, b), (c, d), (e, f), (g, h)], + [d1_, d2_, d3_, d4_], + [(a_, b_), (c_, d_), (e_, f_), (g_, h_)], + ): + xy, xy_ = d_xy._obj, d_xy_._obj + if why: + if xy == xy_: + name = 'collx' + else: + name = 'para' + dep = Dependency(name, [x_, y_, x, y], '', None) + dep.why = why + deps.append(dep) + + return (d1_, d2_, d3_, d4_), deps + + +CONSTRUCTION_RULE = 'c0' + + +class EmptyDependency: + """Empty dependency predicate ready to get filled up.""" + + def __init__(self, level: int, rule_name: str): + self.level = level + self.rule_name = rule_name or '' + self.empty = True + self.why = [] + self.trace = None + + def populate(self, name: str, args: list[gm.Point]) -> Dependency: + dep = Dependency(name, args, self.rule_name, self.level) + dep.trace2 = self.trace + dep.why = list(self.why) + return dep + + def copy(self) -> EmptyDependency: + other = EmptyDependency(self.level, self.rule_name) + other.why = list(self.why) + return other + + def extend( + self, + g: Any, + name0: str, + args0: list[gm.Point], + name: str, + args: list[gm.Point], + ) -> EmptyDependency: + """Extend the dependency list by (name, args).""" + dep0 = self.populate(name0, args0) + deps = EmptyDependency(level=self.level, rule_name=None) + dep = Dependency(name, args, None, deps.level) + deps.why = [dep0, dep.why_me_or_cache(g, None)] + return deps + + def extend_many( + self, + g: Any, + name0: str, + args0: list[gm.Point], + name_args: list[tuple[str, list[gm.Point]]], + ) -> EmptyDependency: + """Extend the dependency list by many name_args.""" + if not name_args: + return self + dep0 = self.populate(name0, args0) + deps = EmptyDependency(level=self.level, rule_name=None) + deps.why = [dep0] + for name, args in name_args: + dep = Dependency(name, args, None, deps.level) + deps.why += [dep.why_me_or_cache(g, None)] + return deps + + +def maybe_make_equal_pairs( + a: gm.Point, + b: gm.Point, + c: gm.Point, + d: gm.Point, + m: gm.Point, + n: gm.Point, + p: gm.Point, + q: gm.Point, + ab: gm.Line, + mn: gm.Line, + g: Any, + level: int, +) -> list[Dependency]: + """Make a-b:c-d==m-n:p-q in case a-b==m-n or c-d==p-q.""" + if ab != mn: + return + why = [] + eqname = 'para' if isinstance(ab, gm.Line) else 'cong' + colls = [a, b, m, n] + if len(set(colls)) > 2 and eqname == 'para': + dep = Dependency('collx', colls, None, level) + dep.why_me(g, level) + why += [dep] + + dep = Dependency(eqname, [c, d, p, q], None, level) + dep.why_me(g, level) + why += [dep] + return why + + +class Dependency(Construction): + """Dependency is a predicate that other predicates depend on.""" + + def __init__( + self, name: str, args: list[gm.Point], rule_name: str, level: int + ): + super().__init__(name, args) + self.rule_name = rule_name or '' + self.level = level + self.why = [] + + self._stat = None + self.trace = None + + def _find(self, dep_hashed: tuple[str, ...]) -> Dependency: + for w in self.why: + f = w._find(dep_hashed) + if f: + return f + if w.hashed() == dep_hashed: + return w + + def remove_loop(self) -> Dependency: + f = self._find(self.hashed()) + if f: + return f + return self + + def copy(self) -> Dependency: + dep = Dependency(self.name, self.args, self.rule_name, self.level) + dep.trace = self.trace + dep.why = list(self.why) + return dep + + def why_me_or_cache(self, g: Any, level: int) -> Dependency: + if self.hashed() in g.cache: + return g.cache[self.hashed()] + self.why_me(g, level) + return self + + def populate(self, name: str, args: list[gm.Point]) -> Dependency: + assert self.rule_name == CONSTRUCTION_RULE, self.rule_name + dep = Dependency(self.name, self.args, self.rule_name, self.level) + dep.why = list(self.why) + return dep + + def why_me(self, g: Any, level: int) -> None: + """Figure out the dependencies predicates of self.""" + name, args = self.name, self.args + + hashed_me = hashed(name, args) + if hashed_me in g.cache: + dep = g.cache[hashed_me] + self.why = dep.why + self.rule_name = dep.rule_name + return + + if self.name == 'para': + a, b, c, d = self.args + if {a, b} == {c, d}: + self.why = [] + return + + ab = g._get_line(a, b) + cd = g._get_line(c, d) + if ab == cd: + if {a, b} == {c, d}: + self.why = [] + self.rule_name = '' + return + dep = Dependency('coll', list({a, b, c, d}), 't??', None) + self.why = [dep.why_me_or_cache(g, level)] + return + + for (x, y), xy in zip([(a, b), (c, d)], [ab, cd]): + x_, y_ = xy.points + if {x, y} == {x_, y_}: + continue + d = Dependency('collx', [x, y, x_, y_], None, level) + self.why += [d.why_me_or_cache(g, level)] + + whypara = g.why_equal(ab, cd, None) + self.why += whypara + + elif self.name == 'midp': + m, a, b = self.args + ma = g._get_segment(m, a) + mb = g._get_segment(m, b) + dep = Dependency('coll', [m, a, b], None, None).why_me_or_cache(g, None) + self.why = [dep] + g.why_equal(ma, mb, level) + + elif self.name == 'perp': + a, b, c, d = self.args + ab = g._get_line(a, b) + cd = g._get_line(c, d) + for (x, y), xy in zip([(a, b), (c, d)], [ab, cd]): + x_, y_ = xy.points + if {x, y} == {x_, y_}: + continue + d = Dependency('collx', [x, y, x_, y_], None, level) + self.why += [d.why_me_or_cache(g, level)] + + _, why = why_eqangle(ab._val, cd._val, cd._val, ab._val, level) + a, b = ab.points + c, d = cd.points + + if hashed(self.name, [a, b, c, d]) != self.hashed(): + d = Dependency(self.name, [a, b, c, d], None, level) + d.why = why + why = [d] + + self.why += why + + elif self.name == 'cong': + a, b, c, d = self.args + ab = g._get_segment(a, b) + cd = g._get_segment(c, d) + + self.why = g.why_equal(ab, cd, level) + + elif self.name == 'coll': + _, why = gm.line_of_and_why(self.args, level) + self.why = why + + elif self.name == 'collx': + if g.check_coll(self.args): + args = list(set(self.args)) + hashed_me = hashed('coll', args) + if hashed_me in g.cache: + dep = g.cache[hashed_me] + self.why = [dep] + self.rule_name = '' + return + _, self.why = gm.line_of_and_why(args, level) + else: + self.name = 'para' + self.why_me(g, level) + + elif self.name == 'cyclic': + _, why = gm.circle_of_and_why(self.args, level) + self.why = why + + elif self.name == 'circle': + o, a, b, c = self.args + oa = g._get_segment(o, a) + ob = g._get_segment(o, b) + oc = g._get_segment(o, c) + self.why = g.why_equal(oa, ob, level) + g.why_equal(oa, oc, level) + + elif self.name in ['eqangle', 'eqangle6']: + a, b, c, d, m, n, p, q = self.args + + ab, why1 = g.get_line_thru_pair_why(a, b) + cd, why2 = g.get_line_thru_pair_why(c, d) + mn, why3 = g.get_line_thru_pair_why(m, n) + pq, why4 = g.get_line_thru_pair_why(p, q) + + if ab is None or cd is None or mn is None or pq is None: + if {a, b} == {m, n}: + d = Dependency('para', [c, d, p, q], None, level) + self.why = [d.why_me_or_cache(g, level)] + if {a, b} == {c, d}: + d = Dependency('para', [p, q, m, n], None, level) + self.why = [d.why_me_or_cache(g, level)] + if {c, d} == {p, q}: + d = Dependency('para', [a, b, m, n], None, level) + self.why = [d.why_me_or_cache(g, level)] + if {p, q} == {m, n}: + d = Dependency('para', [a, b, c, d], None, level) + self.why = [d.why_me_or_cache(g, level)] + return + + for (x, y), xy, whyxy in zip( + [(a, b), (c, d), (m, n), (p, q)], + [ab, cd, mn, pq], + [why1, why2, why3, why4], + ): + x_, y_ = xy.points + if {x, y} == {x_, y_}: + continue + d = Dependency('collx', [x, y, x_, y_], None, level) + d.why = whyxy + self.why += [d] + + a, b = ab.points + c, d = cd.points + m, n = mn.points + p, q = pq.points + diff = hashed(self.name, [a, b, c, d, m, n, p, q]) != self.hashed() + + whyeqangle = None + if ab._val and cd._val and mn._val and pq._val: + whyeqangle = why_eqangle(ab._val, cd._val, mn._val, pq._val, level) + + if whyeqangle: + (dab, dcd, dmn, dpq), whyeqangle = whyeqangle + if diff: + d = Dependency('eqangle', [a, b, c, d, m, n, p, q], None, level) + d.why = whyeqangle + whyeqangle = [d] + self.why += whyeqangle + + else: + if (ab == cd and mn == pq) or (ab == mn and cd == pq): + self.why += [] + elif ab == mn: + self.why += maybe_make_equal_pairs( + a, b, c, d, m, n, p, q, ab, mn, g, level + ) + elif cd == pq: + self.why += maybe_make_equal_pairs( + c, d, a, b, p, q, m, n, cd, pq, g, level + ) + elif ab == cd: + self.why += maybe_make_equal_pairs( + a, b, m, n, c, d, p, q, ab, cd, g, level + ) + elif mn == pq: + self.why += maybe_make_equal_pairs( + m, n, a, b, p, q, c, d, mn, pq, g, level + ) + elif g.is_equal(ab, mn) or g.is_equal(cd, pq): + dep1 = Dependency('para', [a, b, m, n], None, level) + dep1.why_me(g, level) + dep2 = Dependency('para', [c, d, p, q], None, level) + dep2.why_me(g, level) + self.why += [dep1, dep2] + elif g.is_equal(ab, cd) or g.is_equal(mn, pq): + dep1 = Dependency('para', [a, b, c, d], None, level) + dep1.why_me(g, level) + dep2 = Dependency('para', [m, n, p, q], None, level) + dep2.why_me(g, level) + self.why += [dep1, dep2] + elif ab._val and cd._val and mn._val and pq._val: + self.why = why_eqangle(ab._val, cd._val, mn._val, pq._val, level) + + elif self.name in ['eqratio', 'eqratio6']: + a, b, c, d, m, n, p, q = self.args + ab = g._get_segment(a, b) + cd = g._get_segment(c, d) + mn = g._get_segment(m, n) + pq = g._get_segment(p, q) + + if ab is None or cd is None or mn is None or pq is None: + if {a, b} == {m, n}: + d = Dependency('cong', [c, d, p, q], None, level) + self.why = [d.why_me_or_cache(g, level)] + if {a, b} == {c, d}: + d = Dependency('cong', [p, q, m, n], None, level) + self.why = [d.why_me_or_cache(g, level)] + if {c, d} == {p, q}: + d = Dependency('cong', [a, b, m, n], None, level) + self.why = [d.why_me_or_cache(g, level)] + if {p, q} == {m, n}: + d = Dependency('cong', [a, b, c, d], None, level) + self.why = [d.why_me_or_cache(g, level)] + return + + if ab._val and cd._val and mn._val and pq._val: + self.why = why_eqratio(ab._val, cd._val, mn._val, pq._val, level) + + if self.why is None: + self.why = [] + if (ab == cd and mn == pq) or (ab == mn and cd == pq): + self.why = [] + elif ab == mn: + self.why += maybe_make_equal_pairs( + a, b, c, d, m, n, p, q, ab, mn, g, level + ) + elif cd == pq: + self.why += maybe_make_equal_pairs( + c, d, a, b, p, q, m, n, cd, pq, g, level + ) + elif ab == cd: + self.why += maybe_make_equal_pairs( + a, b, m, n, c, d, p, q, ab, cd, g, level + ) + elif mn == pq: + self.why += maybe_make_equal_pairs( + m, n, a, b, p, q, c, d, mn, pq, g, level + ) + elif g.is_equal(ab, mn) or g.is_equal(cd, pq): + dep1 = Dependency('cong', [a, b, m, n], None, level) + dep1.why_me(g, level) + dep2 = Dependency('cong', [c, d, p, q], None, level) + dep2.why_me(g, level) + self.why += [dep1, dep2] + elif g.is_equal(ab, cd) or g.is_equal(mn, pq): + dep1 = Dependency('cong', [a, b, c, d], None, level) + dep1.why_me(g, level) + dep2 = Dependency('cong', [m, n, p, q], None, level) + dep2.why_me(g, level) + self.why += [dep1, dep2] + elif ab._val and cd._val and mn._val and pq._val: + self.why = why_eqangle(ab._val, cd._val, mn._val, pq._val, level) + + elif self.name in ['diff', 'npara', 'nperp', 'ncoll', 'sameside']: + self.why = [] + + elif self.name == 'simtri': + a, b, c, x, y, z = self.args + dep1 = Dependency('eqangle', [a, b, a, c, x, y, x, z], '', level) + dep1.why_me(g, level) + dep2 = Dependency('eqangle', [b, a, b, c, y, x, y, z], '', level) + dep2.why_me(g, level) + self.rule_name = 'r34' + self.why = [dep1, dep2] + + elif self.name == 'contri': + a, b, c, x, y, z = self.args + dep1 = Dependency('cong', [a, b, x, y], '', level) + dep1.why_me(g, level) + dep2 = Dependency('cong', [b, c, y, z], '', level) + dep2.why_me(g, level) + dep3 = Dependency('cong', [c, a, z, x], '', level) + dep3.why_me(g, level) + self.rule_name = 'r32' + self.why = [dep1, dep2, dep3] + + elif self.name == 'ind': + pass + + elif self.name == 'aconst': + a, b, c, d, ang0 = self.args + + measure = ang0._val + + for ang in measure.neighbors(gm.Angle): + if ang == ang0: + continue + d1, d2 = ang._d + l1, l2 = d1._obj, d2._obj + (a1, b1), (c1, d1) = l1.points, l2.points + + if not g.check_para_or_coll([a, b, a1, b1]) or not g.check_para_or_coll( + [c, d, c1, d1] + ): + continue + + self.why = [] + for args in [(a, b, a1, b1), (c, d, c1, d1)]: + if g.check_coll(args): + if len(set(args)) > 2: + dep = Dependency('coll', args, None, None) + self.why.append(dep.why_me_or_cache(g, level)) + else: + dep = Dependency('para', args, None, None) + self.why.append(dep.why_me_or_cache(g, level)) + + self.why += gm.why_equal(ang, ang0) + break + + elif self.name == 'rconst': + a, b, c, d, rat0 = self.args + + val = rat0._val + + for rat in val.neighbors(gm.Ratio): + if rat == rat0: + continue + l1, l2 = rat._l + s1, s2 = l1._obj, l2._obj + (a1, b1), (c1, d1) = list(s1.points), list(s2.points) + + if not g.check_cong([a, b, a1, b1]) or not g.check_cong([c, d, c1, d1]): + continue + + self.why = [] + for args in [(a, b, a1, b1), (c, d, c1, d1)]: + if len(set(args)) > 2: + dep = Dependency('cong', args, None, None) + self.why.append(dep.why_me_or_cache(g, level)) + + self.why += gm.why_equal(rat, rat0) + break + + else: + raise ValueError('Not recognize', self.name) + + def hashed(self, rename: bool = False) -> tuple[str, ...]: + return hashed(self.name, self.args, rename=rename) + + +def hashed( + name: str, args: list[gm.Point], rename: bool = False +) -> tuple[str, ...]: + if name == 's_angle': + args = [p.name if not rename else p.new_name for p in args[:-1]] + [ + str(args[-1]) + ] + else: + args = [p.name if not rename else p.new_name for p in args] + return hashed_txt(name, args) + + +def hashed_txt(name: str, args: list[str]) -> tuple[str, ...]: + """Return a tuple unique to name and args upto arg permutation equivariant.""" + + if name in ['const', 'aconst', 'rconst']: + a, b, c, d, y = args + a, b = sorted([a, b]) + c, d = sorted([c, d]) + return name, a, b, c, d, y + + if name in ['npara', 'nperp', 'para', 'cong', 'perp', 'collx']: + a, b, c, d = args + + a, b = sorted([a, b]) + c, d = sorted([c, d]) + (a, b), (c, d) = sorted([(a, b), (c, d)]) + + return (name, a, b, c, d) + + if name in ['midp', 'midpoint']: + a, b, c = args + b, c = sorted([b, c]) + return (name, a, b, c) + + if name in ['coll', 'cyclic', 'ncoll', 'diff', 'triangle']: + return (name,) + tuple(sorted(list(set(args)))) + + if name == 'circle': + x, a, b, c = args + return (name, x) + tuple(sorted([a, b, c])) + + if name in ['eqangle', 'eqratio', 'eqangle6', 'eqratio6']: + a, b, c, d, e, f, g, h = args + a, b = sorted([a, b]) + c, d = sorted([c, d]) + e, f = sorted([e, f]) + g, h = sorted([g, h]) + if tuple(sorted([a, b, e, f])) > tuple(sorted([c, d, g, h])): + a, b, e, f, c, d, g, h = c, d, g, h, a, b, e, f + if (a, b, c, d) > (e, f, g, h): + a, b, c, d, e, f, g, h = e, f, g, h, a, b, c, d + + if name == 'eqangle6': + name = 'eqangle' + if name == 'eqratio6': + name = 'eqratio' + return (name,) + (a, b, c, d, e, f, g, h) + + if name in ['contri', 'simtri', 'simtri2', 'contri2', 'contri*', 'simtri*']: + a, b, c, x, y, z = args + (a, x), (b, y), (c, z) = sorted([(a, x), (b, y), (c, z)], key=sorted) + (a, b, c), (x, y, z) = sorted([(a, b, c), (x, y, z)], key=sorted) + return (name, a, b, c, x, y, z) + + if name in ['eqratio3']: + a, b, c, d, o, o = args # pylint: disable=redeclared-assigned-name + (a, c), (b, d) = sorted([(a, c), (b, d)], key=sorted) + (a, b), (c, d) = sorted([(a, b), (c, d)], key=sorted) + return (name, a, b, c, d, o, o) + + if name in ['sameside', 's_angle']: + return (name,) + tuple(args) + + raise ValueError(f'Not recognize {name} to hash.') diff --git a/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/gh2848.f90 b/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/gh2848.f90 new file mode 100644 index 0000000000000000000000000000000000000000..bd748996d58227327d56a6b4fca9a40d5dee7bcb --- /dev/null +++ b/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/gh2848.f90 @@ -0,0 +1,13 @@ + subroutine gh2848( & + ! first 2 parameters + par1, par2,& + ! last 2 parameters + par3, par4) + + integer, intent(in) :: par1, par2 + integer, intent(out) :: par3, par4 + + par3 = par1 + par4 = par2 + + end subroutine gh2848 diff --git a/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/operators.f90 b/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/operators.f90 new file mode 100644 index 0000000000000000000000000000000000000000..83481c8e228cb78fdbb1fae50c309b6602d9e1b7 --- /dev/null +++ b/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/operators.f90 @@ -0,0 +1,49 @@ +module foo + type bar + character(len = 32) :: item + end type bar + interface operator(.item.) + module procedure item_int, item_real + end interface operator(.item.) + interface operator(==) + module procedure items_are_equal + end interface operator(==) + interface assignment(=) + module procedure get_int, get_real + end interface assignment(=) +contains + function item_int(val) result(elem) + integer, intent(in) :: val + type(bar) :: elem + + write(elem%item, "(I32)") val + end function item_int + + function item_real(val) result(elem) + real, intent(in) :: val + type(bar) :: elem + + write(elem%item, "(1PE32.12)") val + end function item_real + + function items_are_equal(val1, val2) result(equal) + type(bar), intent(in) :: val1, val2 + logical :: equal + + equal = (val1%item == val2%item) + end function items_are_equal + + subroutine get_real(rval, item) + real, intent(out) :: rval + type(bar), intent(in) :: item + + read(item%item, *) rval + end subroutine get_real + + subroutine get_int(rval, item) + integer, intent(out) :: rval + type(bar), intent(in) :: item + + read(item%item, *) rval + end subroutine get_int +end module foo diff --git a/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/privatemod.f90 b/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/privatemod.f90 new file mode 100644 index 0000000000000000000000000000000000000000..ad88a2ead99e5406f036cafc2b182a7292cd0098 --- /dev/null +++ b/backend/core/alphageometry/.venv-ag/Lib/site-packages/numpy/f2py/tests/src/crackfortran/privatemod.f90 @@ -0,0 +1,11 @@ +module foo + private + integer :: a + public :: setA + integer :: b +contains + subroutine setA(v) + integer, intent(in) :: v + a = v + end subroutine setA +end module foo diff --git a/backend/core/alphageometry/meliad_lib/meliad/transformer/vocabs/pg19train_bpe_32000.model b/backend/core/alphageometry/meliad_lib/meliad/transformer/vocabs/pg19train_bpe_32000.model new file mode 100644 index 0000000000000000000000000000000000000000..29ae2677df1db3ac8d9b5e6f93334867552a66b5 --- /dev/null +++ b/backend/core/alphageometry/meliad_lib/meliad/transformer/vocabs/pg19train_bpe_32000.model @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:1a66e287ef65061abd6dd850d4484bd7b745bc6c44311365bb0cbbce2bb3d4da +size 1662867