From ca3f83d186c423da138824988e6b23fc2861b3a7 Mon Sep 17 00:00:00 2001 From: Matei Adriel Date: Sun, 29 Oct 2023 00:02:10 +0200 Subject: [PATCH] Move stuff around + add lean and idris experiments --- README.md | 4 +- idris/learning/README.md | 13 + idris/learning/flake.lock | 575 ++++++++++++++++++ idris/learning/flake.nix | 28 + idris/learning/sandbox.ipkg | 10 + idris/learning/src/My/Integers.idr | 207 +++++++ idris/learning/src/My/Nats.idr | 206 +++++++ idris/learning/src/My/Signs.idr | 53 ++ idris/learning/src/My/Structures.idr | 79 +++ idris/learning/src/My/Syntax/Rewrite.idr | 19 + idris/learning/test/Tests.idr | 6 + idris/learning/test/runTests.ipkg | 8 + lean/learning/.gitignore | 1 + lean/learning/LeanSandbox.lean | 1 + lean/learning/LeanSandbox/Integers.lean | 397 ++++++++++++ lean/learning/LeanSandbox/Nat.lean | 55 ++ lean/learning/LeanSandbox/Noob.lean | 289 +++++++++ lean/learning/Main.lean | 4 + lean/learning/lakefile.lean | 6 + .../abilities}/.gitignore | 0 {abilities => purescript/abilities}/a.txt | 0 {abilities => purescript/abilities}/b.txt | 0 .../abilities}/packages.dhall | 0 .../abilities}/spago.dhall | 0 .../abilities}/src/Abilities.purs | 0 .../abilities}/src/Ask.js | 0 .../abilities}/src/Ask.purs | 0 .../abilities}/src/Io.purs | 0 .../abilities}/src/Main.purs | 0 .../abilities}/test/Main.purs | 0 {bug => purescript/bug}/.gitignore | 0 {bug => purescript/bug}/packages.dhall | 0 {bug => purescript/bug}/spago.dhall | 0 {bug => purescript/bug}/src/Main.purs | 0 {bug => purescript/bug}/src/other/spago.dhall | 0 .../bug}/src/other/src/Foo.purs | 0 {bug => purescript/bug}/test/Main.purs | 0 {compose => purescript/compose}/.gitignore | 0 .../compose}/packages.dhall | 0 {compose => purescript/compose}/spago.dhall | 0 .../compose}/src/Compose.purs | 0 {compose => purescript/compose}/src/Main.purs | 0 .../compose}/test/Main.purs | 0 {ecs => purescript/ecs}/.gitignore | 0 {ecs => purescript/ecs}/package.json | 0 {ecs => purescript/ecs}/packages.dhall | 0 {ecs => purescript/ecs}/pnpm-lock.yaml | 0 {ecs => purescript/ecs}/spago.dhall | 0 {ecs => purescript/ecs}/src/Main.purs | 0 {ecs => purescript/ecs}/src/Types.js | 0 {ecs => purescript/ecs}/src/Types.purs | 0 {ecs => purescript/ecs}/src/Utils/Keys.purs | 0 {ecs => purescript/ecs}/test/Main.purs | 0 {ecs => purescript/ecs}/tsconfig.json | 0 .../existentials-blog}/.gitignore | 0 .../existentials-blog}/packages.dhall | 0 .../existentials-blog}/spago.dhall | 0 .../existentials-blog}/src/Exists.purs | 0 .../existentials-blog}/src/Main.purs | 0 .../existentials-blog}/test/Main.purs | 0 .../existentials}/packages.dhall | 0 .../existentials}/spago.dhall | 0 .../existentials}/src/Main.purs | 0 {gadts => purescript/gadts}/.gitignore | 0 {gadts => purescript/gadts}/packages.dhall | 0 {gadts => purescript/gadts}/spago.dhall | 0 {gadts => purescript/gadts}/src/Ast.purs | 0 {gadts => purescript/gadts}/src/Main.purs | 0 {gadts => purescript/gadts}/src/RunLift.purs | 0 {gadts => purescript/gadts}/test/Main.purs | 0 {lune => purescript/lune}/.gitignore | 0 {lune => purescript/lune}/packages.dhall | 0 {lune => purescript/lune}/spago.dhall | 0 {lune => purescript/lune}/src/Handle.js | 0 {lune => purescript/lune}/src/Handle.purs | 0 {lune => purescript/lune}/src/Lists.purs | 0 {lune => purescript/lune}/src/Main.purs | 0 {lune => purescript/lune}/test/Main.purs | 0 {maps => purescript/maps}/.gitignore | 0 {maps => purescript/maps}/packages.dhall | 0 {maps => purescript/maps}/spago.dhall | 0 {maps => purescript/maps}/src/Composable.purs | 0 {maps => purescript/maps}/src/Main.purs | 0 {maps => purescript/maps}/src/Map.purs | 0 {maps => purescript/maps}/test/Main.purs | 0 {proofs => purescript/proofs}/.gitignore | 0 {proofs => purescript/proofs}/packages.dhall | 0 {proofs => purescript/proofs}/spago.dhall | 0 {proofs => purescript/proofs}/src/Main.purs | 0 {proofs => purescript/proofs}/src/Nats.purs | 0 .../proofs}/src/ValueLevelNaturals.purs | 0 {proofs => purescript/proofs}/test/Main.purs | 0 .../purpleflow}/.gitignore | 0 .../purpleflow}/packages.dhall | 0 .../packages/core/src/Data/AST.purs | 0 .../packages/core/src/Data/CST.purs | 0 .../packages/parsing-codec/src/Parser.purs | 0 .../purpleflow}/spago.dhall | 0 {purpleflow => purescript/purpleflow}/todo | 0 {sprint => purescript/sprint}/.gitignore | 0 {sprint => purescript/sprint}/packages.dhall | 0 {sprint => purescript/sprint}/spago.dhall | 0 {sprint => purescript/sprint}/src/Main.purs | 0 {sprint => purescript/sprint}/src/Sprint.purs | 0 {sprint => purescript/sprint}/test/Main.purs | 0 {streams => purescript/streams}/.gitignore | 0 .../streams}/packages.dhall | 0 {streams => purescript/streams}/spago.dhall | 0 {streams => purescript/streams}/src/Main.purs | 0 .../streams}/test/Main.purs | 0 .../typelevel}/.gitignore | 0 .../typelevel}/.vscode/settings.json | 0 .../typelevel}/packages.dhall | 0 .../typelevel}/spago.dhall | 0 .../typelevel}/src/Ast.purs | 0 .../typelevel}/src/Fin.purs | 0 .../typelevel}/src/Main.purs | 0 .../typelevel}/src/Num.purs | 0 .../typelevel}/src/Ordering.purs | 0 .../typelevel}/src/Term.purs | 0 .../typelevel}/src/Vec.purs | 0 .../typelevel}/test/Main.purs | 0 122 files changed, 1959 insertions(+), 2 deletions(-) create mode 100644 idris/learning/README.md create mode 100644 idris/learning/flake.lock create mode 100644 idris/learning/flake.nix create mode 100644 idris/learning/sandbox.ipkg create mode 100644 idris/learning/src/My/Integers.idr create mode 100644 idris/learning/src/My/Nats.idr create mode 100644 idris/learning/src/My/Signs.idr create mode 100644 idris/learning/src/My/Structures.idr create mode 100644 idris/learning/src/My/Syntax/Rewrite.idr create mode 100644 idris/learning/test/Tests.idr create mode 100644 idris/learning/test/runTests.ipkg create mode 100644 lean/learning/.gitignore create mode 100644 lean/learning/LeanSandbox.lean create mode 100644 lean/learning/LeanSandbox/Integers.lean create mode 100644 lean/learning/LeanSandbox/Nat.lean create mode 100644 lean/learning/LeanSandbox/Noob.lean create mode 100644 lean/learning/Main.lean create mode 100644 lean/learning/lakefile.lean rename {abilities => purescript/abilities}/.gitignore (100%) rename {abilities => purescript/abilities}/a.txt (100%) rename {abilities => purescript/abilities}/b.txt (100%) rename {abilities => purescript/abilities}/packages.dhall (100%) rename {abilities => purescript/abilities}/spago.dhall (100%) rename {abilities => purescript/abilities}/src/Abilities.purs (100%) rename {abilities => purescript/abilities}/src/Ask.js (100%) rename {abilities => purescript/abilities}/src/Ask.purs (100%) rename {abilities => purescript/abilities}/src/Io.purs (100%) rename {abilities => purescript/abilities}/src/Main.purs (100%) rename {abilities => purescript/abilities}/test/Main.purs (100%) rename {bug => purescript/bug}/.gitignore (100%) rename {bug => purescript/bug}/packages.dhall (100%) rename {bug => purescript/bug}/spago.dhall (100%) rename {bug => purescript/bug}/src/Main.purs (100%) rename {bug => purescript/bug}/src/other/spago.dhall (100%) rename {bug => purescript/bug}/src/other/src/Foo.purs (100%) rename {bug => purescript/bug}/test/Main.purs (100%) rename {compose => purescript/compose}/.gitignore (100%) rename {compose => purescript/compose}/packages.dhall (100%) rename {compose => purescript/compose}/spago.dhall (100%) rename {compose => purescript/compose}/src/Compose.purs (100%) rename {compose => purescript/compose}/src/Main.purs (100%) rename {compose => purescript/compose}/test/Main.purs (100%) rename {ecs => purescript/ecs}/.gitignore (100%) rename {ecs => purescript/ecs}/package.json (100%) rename {ecs => purescript/ecs}/packages.dhall (100%) rename {ecs => purescript/ecs}/pnpm-lock.yaml (100%) rename {ecs => purescript/ecs}/spago.dhall (100%) rename {ecs => purescript/ecs}/src/Main.purs (100%) rename {ecs => purescript/ecs}/src/Types.js (100%) rename {ecs => purescript/ecs}/src/Types.purs (100%) rename {ecs => purescript/ecs}/src/Utils/Keys.purs (100%) rename {ecs => purescript/ecs}/test/Main.purs (100%) rename {ecs => purescript/ecs}/tsconfig.json (100%) rename {existentials-blog => purescript/existentials-blog}/.gitignore (100%) rename {existentials-blog => purescript/existentials-blog}/packages.dhall (100%) rename {existentials-blog => purescript/existentials-blog}/spago.dhall (100%) rename {existentials-blog => purescript/existentials-blog}/src/Exists.purs (100%) rename {existentials-blog => purescript/existentials-blog}/src/Main.purs (100%) rename {existentials-blog => purescript/existentials-blog}/test/Main.purs (100%) rename {existentials => purescript/existentials}/packages.dhall (100%) rename {existentials => purescript/existentials}/spago.dhall (100%) rename {existentials => purescript/existentials}/src/Main.purs (100%) rename {gadts => purescript/gadts}/.gitignore (100%) rename {gadts => purescript/gadts}/packages.dhall (100%) rename {gadts => purescript/gadts}/spago.dhall (100%) rename {gadts => purescript/gadts}/src/Ast.purs (100%) rename {gadts => purescript/gadts}/src/Main.purs (100%) rename {gadts => purescript/gadts}/src/RunLift.purs (100%) rename {gadts => purescript/gadts}/test/Main.purs (100%) rename {lune => purescript/lune}/.gitignore (100%) rename {lune => purescript/lune}/packages.dhall (100%) rename {lune => purescript/lune}/spago.dhall (100%) rename {lune => purescript/lune}/src/Handle.js (100%) rename {lune => purescript/lune}/src/Handle.purs (100%) rename {lune => purescript/lune}/src/Lists.purs (100%) rename {lune => purescript/lune}/src/Main.purs (100%) rename {lune => purescript/lune}/test/Main.purs (100%) rename {maps => purescript/maps}/.gitignore (100%) rename {maps => purescript/maps}/packages.dhall (100%) rename {maps => purescript/maps}/spago.dhall (100%) rename {maps => purescript/maps}/src/Composable.purs (100%) rename {maps => purescript/maps}/src/Main.purs (100%) rename {maps => purescript/maps}/src/Map.purs (100%) rename {maps => purescript/maps}/test/Main.purs (100%) rename {proofs => purescript/proofs}/.gitignore (100%) rename {proofs => purescript/proofs}/packages.dhall (100%) rename {proofs => purescript/proofs}/spago.dhall (100%) rename {proofs => purescript/proofs}/src/Main.purs (100%) rename {proofs => purescript/proofs}/src/Nats.purs (100%) rename {proofs => purescript/proofs}/src/ValueLevelNaturals.purs (100%) rename {proofs => purescript/proofs}/test/Main.purs (100%) rename {purpleflow => purescript/purpleflow}/.gitignore (100%) rename {purpleflow => purescript/purpleflow}/packages.dhall (100%) rename {purpleflow => purescript/purpleflow}/packages/core/src/Data/AST.purs (100%) rename {purpleflow => purescript/purpleflow}/packages/core/src/Data/CST.purs (100%) rename {purpleflow => purescript/purpleflow}/packages/parsing-codec/src/Parser.purs (100%) rename {purpleflow => purescript/purpleflow}/spago.dhall (100%) rename {purpleflow => purescript/purpleflow}/todo (100%) rename {sprint => purescript/sprint}/.gitignore (100%) rename {sprint => purescript/sprint}/packages.dhall (100%) rename {sprint => purescript/sprint}/spago.dhall (100%) rename {sprint => purescript/sprint}/src/Main.purs (100%) rename {sprint => purescript/sprint}/src/Sprint.purs (100%) rename {sprint => purescript/sprint}/test/Main.purs (100%) rename {streams => purescript/streams}/.gitignore (100%) rename {streams => purescript/streams}/packages.dhall (100%) rename {streams => purescript/streams}/spago.dhall (100%) rename {streams => purescript/streams}/src/Main.purs (100%) rename {streams => purescript/streams}/test/Main.purs (100%) rename {typelevel => purescript/typelevel}/.gitignore (100%) rename {typelevel => purescript/typelevel}/.vscode/settings.json (100%) rename {typelevel => purescript/typelevel}/packages.dhall (100%) rename {typelevel => purescript/typelevel}/spago.dhall (100%) rename {typelevel => purescript/typelevel}/src/Ast.purs (100%) rename {typelevel => purescript/typelevel}/src/Fin.purs (100%) rename {typelevel => purescript/typelevel}/src/Main.purs (100%) rename {typelevel => purescript/typelevel}/src/Num.purs (100%) rename {typelevel => purescript/typelevel}/src/Ordering.purs (100%) rename {typelevel => purescript/typelevel}/src/Term.purs (100%) rename {typelevel => purescript/typelevel}/src/Vec.purs (100%) rename {typelevel => purescript/typelevel}/test/Main.purs (100%) diff --git a/README.md b/README.md index 164c713..781f436 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,3 @@ -# Purescript experiments +# The _solar sandbox_ -Random stuff I try in purescript +This is a repository containing random things I am messing around with which don't deserve their own repository. diff --git a/idris/learning/README.md b/idris/learning/README.md new file mode 100644 index 0000000..4e9db93 --- /dev/null +++ b/idris/learning/README.md @@ -0,0 +1,13 @@ +# Idris learning + +This directory contains my experiments when first learning idris. + +## File structure + +| File | Description | +| ---------------------------------------------------------- | --------------------------------------------- | +| [./src/My/Nats.idr](./src/My/Nats.idr) | Natural numbers | +| [./src/My/Signs.idr](./src/My/Signs.idr) | Signs (essentially $\mathbb Z / 2 \mathbb Z$) | +| [./src/My/Integers.idr](./src/My/Integers.idr) | Integers as differences of naturals | +| [./src/My/Structures.idr](./src/My/Structures.idr) | Setoids, semigroups, monoids and groups | +| [./src/My/Syntax/Rewrite.idr](./src/My/Syntax/Rewrite.idr) | Coping with the lack of tactics | diff --git a/idris/learning/flake.lock b/idris/learning/flake.lock new file mode 100644 index 0000000..cfbfd7d --- /dev/null +++ b/idris/learning/flake.lock @@ -0,0 +1,575 @@ +{ + "nodes": { + "Prettier": { + "flake": false, + "locked": { + "lastModified": 1639310097, + "narHash": "sha256-+eSLEJDuy2ZRkh1h0Y5IF6RUeHEcWhAHpWhwdwW65f0=", + "owner": "Z-snails", + "repo": "prettier", + "rev": "4a90663b1d586f6d6fce25873aa0f0d7bc633b89", + "type": "github" + }, + "original": { + "owner": "Z-snails", + "repo": "prettier", + "type": "github" + } + }, + "collie": { + "flake": false, + "locked": { + "lastModified": 1631011321, + "narHash": "sha256-goYctB+WBoLgsbjA0DlqGjD8i9wr1K0lv0agqpuwflU=", + "owner": "ohad", + "repo": "collie", + "rev": "ed2eda5e04fbd02a7728e915d396e14cc7ec298e", + "type": "github" + }, + "original": { + "owner": "ohad", + "repo": "collie", + "type": "github" + } + }, + "comonad": { + "flake": false, + "locked": { + "lastModified": 1638093386, + "narHash": "sha256-kxmN6XuszFLK2i76C6LSGHe5XxAURFu9NpzJbi3nodk=", + "owner": "stefan-hoeck", + "repo": "idris2-comonad", + "rev": "06d6b551db20f1f940eb24c1dae051c957de97ad", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-comonad", + "type": "github" + } + }, + "dom": { + "flake": false, + "locked": { + "lastModified": 1639041519, + "narHash": "sha256-4ZYc0qaUEVARxhWuH3JgejIeT+GEDNxdS6zIGhBCk34=", + "owner": "stefan-hoeck", + "repo": "idris2-dom", + "rev": "01ab52d0ffdb3b47481413a949b8f0c0688c97e4", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-dom", + "type": "github" + } + }, + "dot-parse": { + "flake": false, + "locked": { + "lastModified": 1638264571, + "narHash": "sha256-VJQITz+vuQgl5HwR5QdUGwN8SRtGcb2/lJaAVfFbiSk=", + "owner": "CodingCellist", + "repo": "idris2-dot-parse", + "rev": "48fbda8bf8adbaf9e8ebd6ea740228e4394154d9", + "type": "github" + }, + "original": { + "owner": "CodingCellist", + "repo": "idris2-dot-parse", + "type": "github" + } + }, + "effect": { + "flake": false, + "locked": { + "lastModified": 1637477153, + "narHash": "sha256-Ta2Vogg/IiSBkfhhD57jjPTEf3S4DOiVRmof38hmwlM=", + "owner": "russoul", + "repo": "idris2-effect", + "rev": "ea1daf53b2d7e52f9917409f5653adc557f0ee1a", + "type": "github" + }, + "original": { + "owner": "russoul", + "repo": "idris2-effect", + "type": "github" + } + }, + "elab-util": { + "flake": false, + "locked": { + "lastModified": 1639041013, + "narHash": "sha256-K61s/xifFiTDXJTak5NZmZL6757CTYCY+TGywRZMD7M=", + "owner": "stefan-hoeck", + "repo": "idris2-elab-util", + "rev": "7a381c7c5dc3adb7b97c8b8be17e4fb4cc63027d", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-elab-util", + "type": "github" + } + }, + "flake-utils": { + "locked": { + "lastModified": 1644229661, + "narHash": "sha256-1YdnJAsNy69bpcjuoKdOYQX0YxZBiCYZo4Twxerqv7k=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "3cecb5b042f7f209c56ffd8371b2711a290ec797", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "flake-utils_2": { + "locked": { + "lastModified": 1638122382, + "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "74f7e4319258e287b0f9cb95426c9853b282730b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "frex": { + "flake": false, + "locked": { + "lastModified": 1637410704, + "narHash": "sha256-BthU1t++n0ZvS76p0fCHsE33QSoXYxf0hMUSKajDY8w=", + "owner": "frex-project", + "repo": "idris-frex", + "rev": "22c480e879c757a5cebca7bb555ec3d21ae3ac28", + "type": "github" + }, + "original": { + "owner": "frex-project", + "repo": "idris-frex", + "type": "github" + } + }, + "fvect": { + "flake": false, + "locked": { + "lastModified": 1633247988, + "narHash": "sha256-zElIze03XpcrYL4H5Aj0ZGNplJGbtOx+iWnivJMzHm0=", + "owner": "mattpolzin", + "repo": "idris-fvect", + "rev": "1c5e3761e0cd83e711a3535ef9051bea45e6db3f", + "type": "github" + }, + "original": { + "owner": "mattpolzin", + "repo": "idris-fvect", + "type": "github" + } + }, + "hashable": { + "flake": false, + "locked": { + "lastModified": 1633965157, + "narHash": "sha256-Dggf5K//RCZ7uvtCyeiLNJS6mm+8/n0RFW3zAc7XqPg=", + "owner": "z-snails", + "repo": "idris2-hashable", + "rev": "d6fec8c878057909b67f3d4da334155de4f37907", + "type": "github" + }, + "original": { + "owner": "z-snails", + "repo": "idris2-hashable", + "type": "github" + } + }, + "hedgehog": { + "flake": false, + "locked": { + "lastModified": 1639041435, + "narHash": "sha256-893cPy7gGSQpVmm9co3QCpWsgjukafZHy8YFk9xts30=", + "owner": "stefan-hoeck", + "repo": "idris2-hedgehog", + "rev": "a66b1eb0bf84c4a7b743cfb217be69866bc49ad8", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-hedgehog", + "type": "github" + } + }, + "idrall": { + "flake": false, + "locked": { + "lastModified": 1636495701, + "narHash": "sha256-aOdCRd4XsSxwqVGta1adlZBy8TVTxTwFDnJ1dyMZK8M=", + "owner": "alexhumphreys", + "repo": "idrall", + "rev": "13ef174290169d05c9e9abcd77c53412e3e0c944", + "type": "github" + }, + "original": { + "owner": "alexhumphreys", + "ref": "13ef174", + "repo": "idrall", + "type": "github" + } + }, + "idris-server": { + "flake": false, + "locked": { + "lastModified": 1634507315, + "narHash": "sha256-ulo23yLJXsvImoMB/1C6yRRTqmn/Odo+aUaVi+tUhJo=", + "owner": "avidela", + "repo": "idris-server", + "rev": "661a4ecf0fadaa2bd79c8e922c2d4f79b0b7a445", + "type": "gitlab" + }, + "original": { + "owner": "avidela", + "repo": "idris-server", + "type": "gitlab" + } + }, + "idris2": { + "flake": false, + "locked": { + "lastModified": 1639427352, + "narHash": "sha256-C1K2FM1Kio8vi9FTrivdacYCX4cywIsLBeNCsZ6ft4g=", + "owner": "idris-lang", + "repo": "idris2", + "rev": "36918e618646177b1e0c2fd01f21cc8d04d9da30", + "type": "github" + }, + "original": { + "owner": "idris-lang", + "repo": "idris2", + "type": "github" + } + }, + "idris2-pkgs": { + "inputs": { + "Prettier": "Prettier", + "collie": "collie", + "comonad": "comonad", + "dom": "dom", + "dot-parse": "dot-parse", + "effect": "effect", + "elab-util": "elab-util", + "flake-utils": "flake-utils_2", + "frex": "frex", + "fvect": "fvect", + "hashable": "hashable", + "hedgehog": "hedgehog", + "idrall": "idrall", + "idris-server": "idris-server", + "idris2": "idris2", + "indexed": "indexed", + "inigo": "inigo", + "ipkg-to-json": "ipkg-to-json", + "json": "json", + "katla": "katla", + "lsp": "lsp", + "nixpkgs": "nixpkgs", + "odf": "odf", + "pretty-show": "pretty-show", + "python": "python", + "rhone": "rhone", + "rhone-js": "rhone-js", + "snocvect": "snocvect", + "sop": "sop", + "tailrec": "tailrec", + "xml": "xml" + }, + "locked": { + "lastModified": 1642030375, + "narHash": "sha256-J1uXnpPR72mjFjLBuYcvDHStBxVya6/MjBNNwqxGeD0=", + "owner": "claymager", + "repo": "idris2-pkgs", + "rev": "ac33a49d4d4bd2b50fddb040cd889733a02c8f09", + "type": "github" + }, + "original": { + "owner": "claymager", + "repo": "idris2-pkgs", + "type": "github" + } + }, + "indexed": { + "flake": false, + "locked": { + "lastModified": 1638685238, + "narHash": "sha256-FceB7o88yKYzjTfRC6yfhOL6oDPMmCQAsJZu/pjE2uA=", + "owner": "mattpolzin", + "repo": "idris-indexed", + "rev": "ff3ba99b0063da6a74c96178e7f3c58a4ac1693e", + "type": "github" + }, + "original": { + "owner": "mattpolzin", + "repo": "idris-indexed", + "type": "github" + } + }, + "inigo": { + "flake": false, + "locked": { + "lastModified": 1637596767, + "narHash": "sha256-LNx30LO0YWDVSPTxRLWGTFL4f3d5ANG6c60WPdmiYdY=", + "owner": "idris-community", + "repo": "Inigo", + "rev": "57f5b5c051222d8c630010a0a3cf7d7138910127", + "type": "github" + }, + "original": { + "owner": "idris-community", + "repo": "Inigo", + "type": "github" + } + }, + "ipkg-to-json": { + "flake": false, + "locked": { + "lastModified": 1634937414, + "narHash": "sha256-LhSmWRpI7vyIQE7QTo38ZTjlqYPVSvV/DIpIxzPmqS0=", + "owner": "claymager", + "repo": "ipkg-to-json", + "rev": "2969b6b83714eeddc31e41577a565778ee5922e6", + "type": "github" + }, + "original": { + "owner": "claymager", + "repo": "ipkg-to-json", + "type": "github" + } + }, + "json": { + "flake": false, + "locked": { + "lastModified": 1639041459, + "narHash": "sha256-TP/V1jBBP1hFPm/cJ5O2EJiaNoZ19KvBOAI0S9lvAR4=", + "owner": "stefan-hoeck", + "repo": "idris2-json", + "rev": "7c0c028acad0ba0b63b37b92199f37e6ec73864a", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-json", + "type": "github" + } + }, + "katla": { + "flake": false, + "locked": { + "lastModified": 1636542431, + "narHash": "sha256-X83NA/P3k1iPcBa8g5z8JldEmFEz/jxVeViJX0/FikY=", + "owner": "idris-community", + "repo": "katla", + "rev": "d841ec243f96b4762074211ee81033e28884c858", + "type": "github" + }, + "original": { + "owner": "idris-community", + "repo": "katla", + "type": "github" + } + }, + "lsp": { + "flake": false, + "locked": { + "lastModified": 1639486283, + "narHash": "sha256-po396FnUu8iqiipwPxqpFZEU4rtpX3jnt3cySwjLsH8=", + "owner": "idris-community", + "repo": "idris2-lsp", + "rev": "7ebb6caf6bb4b57c5107579aba2b871408e6f183", + "type": "github" + }, + "original": { + "owner": "idris-community", + "repo": "idris2-lsp", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1639213685, + "narHash": "sha256-Evuobw7o9uVjAZuwz06Al0fOWZ5JMKOktgXR0XgWBtg=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "453bcb8380fd1777348245b3c44ce2a2b93b2e2d", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "nixpkgs-21.11-darwin", + "repo": "nixpkgs", + "type": "github" + } + }, + "odf": { + "flake": false, + "locked": { + "lastModified": 1638184051, + "narHash": "sha256-usSdPx+UqOGImHHdHcrytdzi2LXtIRZuUW0fkD/Wwnk=", + "owner": "madman-bob", + "repo": "idris2-odf", + "rev": "d2f532437321c8336f1ca786b44b6ebef4117126", + "type": "github" + }, + "original": { + "owner": "madman-bob", + "repo": "idris2-odf", + "type": "github" + } + }, + "pretty-show": { + "flake": false, + "locked": { + "lastModified": 1639041411, + "narHash": "sha256-BzEe1fpX+lqGEk8b1JZoQT1db5I7s7SZnLCttRVGXdY=", + "owner": "stefan-hoeck", + "repo": "idris2-pretty-show", + "rev": "a4bc6156b9dac43699f87504cbdb8dada5627863", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-pretty-show", + "type": "github" + } + }, + "python": { + "flake": false, + "locked": { + "lastModified": 1635936936, + "narHash": "sha256-c9mcMApN0qgu0AXQVu0V+NXt2poP258wCPkyvtQvv4I=", + "owner": "madman-bob", + "repo": "idris2-python", + "rev": "0eab028933c65bebe744e879881416f5136d6943", + "type": "github" + }, + "original": { + "owner": "madman-bob", + "repo": "idris2-python", + "type": "github" + } + }, + "rhone": { + "flake": false, + "locked": { + "lastModified": 1639041532, + "narHash": "sha256-2g43shlWQIT/1ogesUBUBV9N8YiD3RwaCbbhdKLVp1s=", + "owner": "stefan-hoeck", + "repo": "idris2-rhone", + "rev": "c4d828b0b8efea495d9a5f1e842a9c67cad57724", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-rhone", + "type": "github" + } + }, + "rhone-js": { + "flake": false, + "locked": { + "lastModified": 1639041546, + "narHash": "sha256-ddWVsSRbfA6ghmwiRMzDpHBPM+esGdutuqm1qQZgs88=", + "owner": "stefan-hoeck", + "repo": "idris2-rhone-js", + "rev": "520dd59549f5b14075045314b6805c7492ed636e", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-rhone-js", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "idris2-pkgs": "idris2-pkgs", + "nixpkgs": [ + "idris2-pkgs", + "nixpkgs" + ] + } + }, + "snocvect": { + "flake": false, + "locked": { + "lastModified": 1641633224, + "narHash": "sha256-6zTU4sDzd/R/dFCTNZaX41H4L3/USGLFghMS0Oc9liY=", + "owner": "mattpolzin", + "repo": "idris-snocvect", + "rev": "ff1e7afba360a62f7e522e9bbb856096a79702c4", + "type": "github" + }, + "original": { + "owner": "mattpolzin", + "repo": "idris-snocvect", + "type": "github" + } + }, + "sop": { + "flake": false, + "locked": { + "lastModified": 1639041379, + "narHash": "sha256-PDTf1Wx6EygiWszguvoVPiqIISYFLabI4e0lXHlrjcA=", + "owner": "stefan-hoeck", + "repo": "idris2-sop", + "rev": "e4354d1883cd73616019457cb9ebf864d99df6a0", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-sop", + "type": "github" + } + }, + "tailrec": { + "flake": false, + "locked": { + "lastModified": 1637146655, + "narHash": "sha256-0yi7MQIrISPvAwkgDC1M5PHDEeVyIaISF0HjKDaT0Rw=", + "owner": "stefan-hoeck", + "repo": "idris2-tailrec", + "rev": "dd0bc6381b3a2e69aa37f9a8c1b165d4b1516ad7", + "type": "github" + }, + "original": { + "owner": "stefan-hoeck", + "repo": "idris2-tailrec", + "type": "github" + } + }, + "xml": { + "flake": false, + "locked": { + "lastModified": 1637939752, + "narHash": "sha256-yYJBhPfwYoi7amlHmeNGrVCOAc3BjZpKTCd9wDs3XEM=", + "owner": "madman-bob", + "repo": "idris2-xml", + "rev": "1292ccfcd58c551089ef699e4560343d5c473d64", + "type": "github" + }, + "original": { + "owner": "madman-bob", + "repo": "idris2-xml", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/idris/learning/flake.nix b/idris/learning/flake.nix new file mode 100644 index 0000000..6b73cdd --- /dev/null +++ b/idris/learning/flake.nix @@ -0,0 +1,28 @@ +{ + description = "My Idris 2 package"; + + inputs = { + flake-utils.url = "github:numtide/flake-utils"; + idris2-pkgs.url = "github:claymager/idris2-pkgs"; + nixpkgs.follows = "idris2-pkgs/nixpkgs"; + }; + + outputs = { self, nixpkgs, idris2-pkgs, flake-utils }: + flake-utils.lib.eachSystem [ "x86_64-darwin" "x86_64-linux" "i686-linux" ] (system: + let + pkgs = import nixpkgs { inherit system; overlays = [ idris2-pkgs.overlay ]; }; + inherit (pkgs.idris2-pkgs._builders) idrisPackage devEnv; + mypkg = idrisPackage ./. { }; + runTests = idrisPackage ./test { extraPkgs.mypkg = mypkg; }; + in + { + defaultPackage = mypkg; + + packages = { inherit mypkg runTests; }; + + devShell = pkgs.mkShell { + buildInputs = [ (devEnv mypkg) ]; + }; + } + ); +} diff --git a/idris/learning/sandbox.ipkg b/idris/learning/sandbox.ipkg new file mode 100644 index 0000000..3146dd0 --- /dev/null +++ b/idris/learning/sandbox.ipkg @@ -0,0 +1,10 @@ +package mypkg + +-- modules = Main +-- main = Main + +depends = contrib + +executable = mypkg + +sourcedir = "src" diff --git a/idris/learning/src/My/Integers.idr b/idris/learning/src/My/Integers.idr new file mode 100644 index 0000000..0818a1f --- /dev/null +++ b/idris/learning/src/My/Integers.idr @@ -0,0 +1,207 @@ +module My.Integers + +import My.Nats +import My.Structures +import Syntax.PreorderReasoning +import My.Syntax.Rewrite +import My.Signs + +%default total + +public export +ℤ : Type +ℤ = (ℕ, ℕ) + +public export +addIntegers : ℤ -> ℤ -> ℤ +addIntegers (x, y) (z, w) = (x + z, y + w) + +public export +toNat : ℤ -> (Sign, ℕ) +toNat (Z, S x) = (Negative, S x) +toNat (x, Z) = (Positive, x) +toNat ((S x), (S y)) = toNat $ assert_smaller (S x, S y) (x, y) + +public export +multiplyIntegers : ℤ -> ℤ -> ℤ +multiplyIntegers (x, y) (z, w) = (x * z + y * w, x * w + y * z) + +public export +negateInteger : ℤ -> ℤ +negateInteger (x, y) = (y, x) + +public export +substractIntegers : ℤ -> ℤ -> ℤ +substractIntegers a b = (?l, ?r) + +public export +normalForm : ℤ -> ℤ +normalForm ((S x), (S y)) = normalForm (assert_smaller (S x, S y) (x, y)) +normalForm a = a + +-- absoluteValue : ℤ -> ℕ +-- absoluteValue (Z, b) = b +-- absoluteValue ((S x), y) = absoluteValue (x, y) + +public export +fromNat : ℕ -> ℤ +fromNat n = (n, Z) + +public export +fromActualInteger : Integer -> ℤ +fromActualInteger 0 = (Z, Z) +fromActualInteger n = + if n > 0 then + fromNat (fromInteger n) + else + negateInteger (fromNat (fromInteger (-n))) + +public export +Num ℤ where + (+) = addIntegers + (*) = multiplyIntegers + fromInteger = fromActualInteger + +public export +Neg ℤ where + negate = negateInteger + (-) = substractIntegers + +---------- Equivalence +public export +integersAreEquivalent : ℤ -> ℤ -> Type +integersAreEquivalent (x, y) (z, w) = x + w = z + y + +public export +equivalenceIsReflexive : integersAreEquivalent a a +equivalenceIsReflexive {a = (x, y)} = Refl + +public export +equivalenceIsTransitive : {a, b, c: ℤ} -> integersAreEquivalent a b -> integersAreEquivalent b c -> integersAreEquivalent a c +equivalenceIsTransitive {a = (z, w)} {b = (v, s)} {c = (t, u)} zsISvw vuISts = id + $ … (z + u = t + w) + $ My.Nats.substractionPreservesEquality s + $ … ((z + u) + s = (t + w) + s) + $ rewrite My.Nats.additionIsCommutative z u + in …l ((u + z) + s) + $ rewrite My.Nats.additionIsAssociative u z s + in …l (u + (z + s)) + $ rewrite zsISvw + in …l (u + (v + w)) + $ rewrite sym $ My.Nats.additionIsAssociative u v w + in …l ((u + v) + w) + $ rewrite My.Nats.additionIsCommutative t w + in …r ((w + t) + s) + $ rewrite My.Nats.additionIsAssociative w t s + in …r (w + (t + s)) + $ rewrite My.Nats.additionIsCommutative w (t + s) + in …r ((t + s) + w) + $ My.Nats.additionPreservesEquality w + $ … (u + v = t + s) + $ rewrite My.Nats.additionIsCommutative u v + in …l (v + u) + $ vuISts + +public export +equivalenceIsSymmetric : {a, b: ℤ} -> integersAreEquivalent a b -> integersAreEquivalent b a +equivalenceIsSymmetric {a = (y, z)} {b = (w, v)} x = sym x + +public export +My.Structures.Setoid ℤ where + (<->) = integersAreEquivalent + reflexivity = equivalenceIsReflexive + transitivity = equivalenceIsTransitive + symmetry = equivalenceIsSymmetric + +---------- Addition proofs +public export +additionIsCommutative : CommutativityProof My.Integers.addIntegers +additionIsCommutative (Z, y) (x, z) = (x + (z + y) = (x + 0) + (y + z)) + .... rewrite My.Nats.additionRightIdentity x in (x + (z + y) = x + (y + z)) + .... rewrite My.Nats.additionIsCommutative y z in (x + (z + y) = x + (z + y)) + .... Refl +additionIsCommutative ((S x), y) (z, w) = id + $ … (1 + ((x + z) + (w + y)) = (z + (1 + x)) + (y + w)) + $ rewrite My.Nats.additionIsCommutative y w + in …r ((z + (1 + x)) + (w + y)) + $ rewrite My.Nats.additionIsCommutative z (1 + x) + in …r (1 + (x + z) + (w + y)) + $ Refl + +public export +additionIsAssociative : AssociativityProof My.Integers.addIntegers +additionIsAssociative (x, y) (z, w) (v, s) = id + $ … ((((x + z) + v) + (y + (w + s))) = ((x + (z + v) + ((y + w) + s)))) + $ rewrite My.Nats.additionIsAssociative x z v + in …l ((x + (z + v) + (y + (w + s)))) + $ rewrite My.Nats.additionIsAssociative y w s + in …r ((x + (z + v) + (y + (w + s)))) + $ Refl + +public export +additionRightIdentity : RightIdentityProof My.Integers.addIntegers 0 +additionRightIdentity (x, y) = id + $ … ((x + 0) + y = x + (y + 0)) + $ rewrite My.Nats.additionRightIdentity x + in …l (x + y) + $ rewrite My.Nats.additionRightIdentity y + in …r (x + y) + $ Refl + +public export +additionLeftIdentity : LeftIdentityProof My.Integers.addIntegers 0 +additionLeftIdentity (x, y) = Refl + +---------- Multiplication proofs +multiplyToNatResults : (Sign, ℕ) -> (Sign, ℕ) -> (Sign, ℕ) +multiplyToNatResults (x, z) (y, w) = (multiplySigns x y, z * w) + +ToNatDistributesMultiplication : ℤ -> ℤ -> Type +ToNatDistributesMultiplication a b = toNat (a * b) = multiplyToNatResults (toNat a) (toNat b) + +toNatDistributesMultiplication : (a, b: ℤ) -> ToNatDistributesMultiplication a b +toNatDistributesMultiplication (Z, Z) (Z, Z) = Refl +toNatDistributesMultiplication (Z, Z) (Z, (S x)) = ?toNatDistributesMultiplication_rhs_9 + +toNatDistributesMultiplication (Z, Z) ((S x), w) = ?toNatDistributesMultiplication_rhs_7 + +toNatDistributesMultiplication (Z, (S x)) (z, w) = ?toNatDistributesMultiplication_rhs_5 + +toNatDistributesMultiplication ((S x), y) (z, w) = ?toNatDistributesMultiplication_rhs_3 + + + +multiplicationIsAssociative : AssociativityProof My.Integers.multiplyIntegers +multiplicationIsAssociative 0 b c = ?multiplicationIsAssociative_rhs +multiplicationIsAssociative a b c = ?multiplicationIsAssociative_rhs_1 + + +---------- Interface implementations +public export +[additionSemigroup] My.Structures.Semigroup ℤ where + ∘ = addIntegers + associativityProof = additionIsAssociative + + +public export +[additionMonoid] My.Structures.Monoid ℤ using My.Integers.additionSemigroup where + empty = 0 + rightIdentityProof = My.Integers.additionRightIdentity + leftIdentityProof = My.Integers.additionLeftIdentity + +[multiplicationSemigroup] My.Structures.Semigroup ℤ where + ∘ = multiplyIntegers + associativityProof = multiplicationIsAssociative + +---------- Constants to play around with +seven : ℤ +seven = 7 + +minusFour : ℤ +minusFour = -4 + +three : ℤ +three = 3 + +three' : ℤ +three' = minusFour + seven diff --git a/idris/learning/src/My/Nats.idr b/idris/learning/src/My/Nats.idr new file mode 100644 index 0000000..8613772 --- /dev/null +++ b/idris/learning/src/My/Nats.idr @@ -0,0 +1,206 @@ +module My.Nats + +import My.Structures + +%default total +%hide Z +%hide S + + +public export +data ℕ : Type where + Z : ℕ + S : ℕ -> ℕ + +public export +fromIntegerNat : Integer -> ℕ +fromIntegerNat 0 = Z +fromIntegerNat n = + if (n > 0) then + S (fromIntegerNat (assert_smaller n (n - 1))) + else + Z + +one : ℕ +one = S Z + +public export +add : ℕ -> ℕ -> ℕ +add Z a = a +add (S a) b = S (add a b) + +public export +multiply : ℕ -> ℕ -> ℕ +multiply Z a = Z +multiply (S a) b = add b (multiply a b) + +public export +raiseToPower : ℕ -> ℕ -> ℕ +raiseToPower a Z = one +raiseToPower a (S b) = multiply a (raiseToPower a b) + +public export +monus : ℕ -> ℕ -> ℕ +monus (S a) (S b) = monus a b +monus a Z = a +monus _ (S _) = Z + +public export +naturalInduction : (P: ℕ -> Type) -> P Z -> ({x: ℕ} -> P x -> P (S x)) -> (x: ℕ) -> P x +naturalInduction p base recurse Z = base +naturalInduction p base recurse (S a) = recurse (naturalInduction p base recurse a) + +public export +Num ℕ where + fromInteger = fromIntegerNat + (+) = add + (*) = multiply + +public export +%hint +setoidNats : My.Structures.Setoid ℕ +setoidNats = trivialSetoid ℕ + +---------- Proofs +public export +succCommutesAddition : (a, b: ℕ) -> add (S a) b = add a (S b) +succCommutesAddition Z a = Refl +succCommutesAddition (S c) b = let + rec = succCommutesAddition c b + in rewrite rec in Refl + +public export +additionIsAssociative : AssociativityProof My.Nats.add +additionIsAssociative Z b c = Refl +additionIsAssociative (S a) b c = let + rec = additionIsAssociative a b c + in rewrite rec in Refl + +public export +additionRightIdentity : RightIdentityProof My.Nats.add 0 +additionRightIdentity Z = Refl +additionRightIdentity (S x) = rewrite additionRightIdentity x in Refl + +public export +additionIsCommutative : CommutativityProof My.Nats.add +additionIsCommutative Z b = sym (additionRightIdentity b) +additionIsCommutative (S x) Z = rewrite additionIsCommutative x Z in Refl +additionIsCommutative (S x) (S y) = + rewrite sym (succCommutesAddition x y) in + rewrite additionIsCommutative y (S x) in + Refl + +----- Multiplication proofs +public export +multiplicationRightNullification : (a: ℕ) -> multiply a 0 = 0 +multiplicationRightNullification Z = Refl +multiplicationRightNullification (S x) = rewrite multiplicationRightNullification x in Refl + +public export +multiplicationRightIdentity : (a: ℕ) -> a * 1 = a +multiplicationRightIdentity Z = Refl +multiplicationRightIdentity (S x) = rewrite multiplicationRightIdentity x in Refl + +public export +multiplicationLeftIdentity : (a: ℕ) -> a = 1 * a +multiplicationLeftIdentity a = rewrite additionRightIdentity a in Refl + +public export +multiplicationDistributesAddition : (a, b, c: ℕ) -> a * (b + c) = a * b + a * c +multiplicationDistributesAddition Z b c = Refl +multiplicationDistributesAddition (S x) b c + = let rec = multiplicationDistributesAddition x b c + in rewrite rec + in rewrite additionIsAssociative b c ((x * b) + (x * c)) + in rewrite additionIsAssociative b (x * b) (c + (x * c)) + in rewrite additionIsCommutative (x * b) (c + (x * c)) + in rewrite additionIsAssociative c (x * c) (x * b) + in rewrite additionIsCommutative (x * b) (x * c) + in Refl + +public export +succIsPlusOne : (a: ℕ) -> S a = a + 1 +succIsPlusOne Z = Refl +succIsPlusOne (S x) = rewrite additionIsCommutative x 1 in Refl + +public export +multiplicationisCommutative : CommutativityProof My.Nats.multiply +multiplicationisCommutative Z b = sym (multiplicationRightNullification b) +multiplicationisCommutative (S x) b = + rewrite succIsPlusOne x in + rewrite multiplicationDistributesAddition b x 1 in + rewrite multiplicationRightIdentity b in + rewrite additionIsCommutative b (x * b) in + rewrite multiplicationisCommutative x b in + Refl + + +public export +multiplicationIsAssociative : AssociativityProof My.Nats.multiply +multiplicationIsAssociative Z b c = Refl +multiplicationIsAssociative (S x) y c = + rewrite multiplicationisCommutative (y + (x * y)) c in + rewrite multiplicationDistributesAddition c y (x * y) in + rewrite multiplicationisCommutative y c in + rewrite sym (multiplicationIsAssociative c x y) in + rewrite sym (multiplicationIsAssociative x c y) in + rewrite sym (multiplicationisCommutative x c) in + Refl + +---------- Monus proofs +public export +xMinusXIsZero : (a: ℕ) -> (monus a a) = 0 +xMinusXIsZero Z = Refl +xMinusXIsZero (S x) = xMinusXIsZero x + +public export +additionNullifiesMonus : (a, b: ℕ) -> (monus (a + b) b) = a +additionNullifiesMonus Z b = xMinusXIsZero b +additionNullifiesMonus (S x) Z = rewrite additionRightIdentity x in Refl +additionNullifiesMonus x (S y) = rewrite sym $ succCommutesAddition x y in additionNullifiesMonus x y + +---------- Equality proofs +public export +additionPreservesEquality : {a, b: ℕ} -> (c: ℕ) -> (a = b) -> (a + c = b + c) +additionPreservesEquality c prf = cong (+c) prf + +public export +substractionPreservesEquality : {a, b: ℕ} -> (c: ℕ) -> (a + c = b + c) -> (a = b) +substractionPreservesEquality c prf = let + middle : (monus (a + c) c = monus (b + c) c) + middle = cong (\e => monus e c) prf + + left : (a = monus (a + c) c) + left = sym $ additionNullifiesMonus a c + + right : (monus (b + c) c = b) + right = additionNullifiesMonus b c + in (left `trans` middle) `trans` right + +public export +multiplicationPreservesEquality : {a, b: ℕ} -> (c: ℕ) -> (a = b) -> (a * c = b * c) +multiplicationPreservesEquality c prf = cong (*c) prf + +---------- Interace implementations +public export +[additionSemigroup] My.Structures.Semigroup ℕ where + ∘ = add + associativityProof = additionIsAssociative + +public export +[additionMonoid] My.Structures.Monoid ℕ using additionSemigroup where + empty = 0 + rightIdentityProof a = additionRightIdentity a + leftIdentityProof a = Refl + +public export +[multiplicationSemigroup] My.Structures.Semigroup ℕ where + ∘ = multiply + associativityProof = multiplicationIsAssociative + +public export +[multiplicationMonoid] My.Structures.Monoid ℕ using multiplicationSemigroup where + empty = 1 + rightIdentityProof = multiplicationRightIdentity + leftIdentityProof = multiplicationLeftIdentity + diff --git a/idris/learning/src/My/Signs.idr b/idris/learning/src/My/Signs.idr new file mode 100644 index 0000000..638470a --- /dev/null +++ b/idris/learning/src/My/Signs.idr @@ -0,0 +1,53 @@ +module My.Signs + +import My.Structures + +public export +data Sign = Positive | Negative + +public export +negateSign : Sign -> Sign +negateSign Positive = Negative +negateSign Negative = Positive + +public export +multiplySigns : Sign -> Sign -> Sign +multiplySigns Positive b = b +multiplySigns Negative b = negateSign b + +public export +%hint +setoidSign : My.Structures.Setoid Sign +setoidSign = trivialSetoid Sign + +doubleNegationIdentity : (a: Sign) -> negateSign (negateSign a) = a +doubleNegationIdentity Positive = Refl +doubleNegationIdentity Negative = Refl + +multiplicationIsAssociative : AssociativityProof My.Signs.multiplySigns +multiplicationIsAssociative Positive b c = Refl +multiplicationIsAssociative Negative Positive c = Refl +multiplicationIsAssociative Negative Negative c = sym $ doubleNegationIdentity c + +multiplicationRightIdentity : RightIdentityProof My.Signs.multiplySigns Positive +multiplicationRightIdentity Positive = Refl +multiplicationRightIdentity Negative = Refl + +multiplicationLeftIdentity : LeftIdentityProof My.Signs.multiplySigns Positive +multiplicationLeftIdentity _ = Refl + +multiplicationIsCommutative : CommutativityProof My.Signs.multiplySigns +multiplicationIsCommutative Positive b = sym $ multiplicationRightIdentity b +multiplicationIsCommutative Negative Positive = Refl +multiplicationIsCommutative Negative Negative = Refl + +public export +My.Structures.Semigroup Sign where + ∘ = multiplySigns + associativityProof = multiplicationIsAssociative + +public export +My.Structures.Monoid Sign where + empty = Positive + rightIdentityProof = multiplicationRightIdentity + leftIdentityProof = multiplicationLeftIdentity diff --git a/idris/learning/src/My/Structures.idr b/idris/learning/src/My/Structures.idr new file mode 100644 index 0000000..402a5c6 --- /dev/null +++ b/idris/learning/src/My/Structures.idr @@ -0,0 +1,79 @@ +module My.Structures + +%hide Semigroup +%hide Monoid +%hide empty + +infix 5 <-> + +public export +interface Setoid t where + constructor MkSetoid + (<->) : t -> t -> Type + reflexivity : {0 a: t} -> a <-> a + transitivity : {a,b,c: t} -> (a <-> b) -> (b <-> c) -> (a <-> c) + symmetry : {a, b: t} -> (a <-> b) -> (b <-> a) + +public export +trivialSetoid : (t: Type) -> Setoid t +trivialSetoid _ = MkSetoid Equal Refl (\a,b => trans a b) (\a => sym a) + +public export +AssociativityProof : {x: Type} -> Setoid x => (x -> x -> x) -> Type +AssociativityProof {x} t = (a, b, c: x) -> (t (t a b) c) <-> (t a (t b c)) + +public export +RightIdentityProof : {x: Type} -> Setoid x => (x -> x -> x) -> x -> Type +RightIdentityProof t e = (a: x) -> t a e <-> a + +public export +LeftIdentityProof : {x: Type} -> Setoid x => (x -> x -> x) -> x -> Type +LeftIdentityProof t e = (a: x) -> a <-> t e a + +public export +RightInverseProof : {x: Type} -> Setoid x => (x -> x -> x) -> (x -> x) -> x -> Type +RightInverseProof t inverse e = (a: x) -> t a (inverse a) <-> e + +public export +LeftInverseProof : {x: Type} -> Setoid x => (x -> x -> x) -> (x -> x) -> x -> Type +LeftInverseProof t inverse e = (a: x) -> t (inverse a) a <-> e + +public export +CommutativityProof : {x: Type} -> Setoid x => (x -> x -> x) -> Type +CommutativityProof t = (a, b: x) -> t a b <-> t b a + +public export +rightToLeftIdentity : + {x: Type} -> Setoid x => + (f: x -> x -> x) -> (e: x) -> + CommutativityProof f -> + RightIdentityProof f e -> + LeftIdentityProof f e +rightToLeftIdentity f e commutativity rightIdentity x = symmetry $ transitivity (commutativity e x) (rightIdentity x) + +public export +leftToRightIdentity : + {x: Type} -> Setoid x => + (f: x -> x -> x) -> (e: x) -> + CommutativityProof f -> + LeftIdentityProof f e -> + RightIdentityProof f e +leftToRightIdentity f e commutativity leftIdentity x = symmetry $ transitivity (leftIdentity x) (commutativity e x) + +public export +interface Setoid t => Semigroup t where + ∘ : t -> t -> t + associativityProof : AssociativityProof ∘ + +public export +interface Semigroup t => Monoid t where + empty : t + rightIdentityProof : RightIdentityProof ∘ empty + leftIdentityProof : LeftIdentityProof ∘ empty + +public export +interface Monoid t => Group t where + ⁻¹ : t -> t + rightInverseProof : RightInverseProof ∘ (⁻¹) My.Structures.empty + leftInverseProof : LeftInverseProof ∘ (⁻¹) My.Structures.empty + diff --git a/idris/learning/src/My/Syntax/Rewrite.idr b/idris/learning/src/My/Syntax/Rewrite.idr new file mode 100644 index 0000000..238ceb0 --- /dev/null +++ b/idris/learning/src/My/Syntax/Rewrite.idr @@ -0,0 +1,19 @@ +module My.Syntax.Rewrite + +infix 1 .... + +public export +(....) : (0 a : Type) -> a -> a +(....) _ a = a + +public export +… : (0 a : Type) -> a -> a +… _ a = a + +public export +…l : (0 a : t) -> {0 b : t} -> a = b -> a = b +…l _ a = a + +public export +…r : {0 a : t} -> (0 b : t) -> a = b -> a = b +…r _ a = a diff --git a/idris/learning/test/Tests.idr b/idris/learning/test/Tests.idr new file mode 100644 index 0000000..735b3d9 --- /dev/null +++ b/idris/learning/test/Tests.idr @@ -0,0 +1,6 @@ +module Tests + +import Main + +main : IO () +main = putStrLn "tests passed" diff --git a/idris/learning/test/runTests.ipkg b/idris/learning/test/runTests.ipkg new file mode 100644 index 0000000..152e96f --- /dev/null +++ b/idris/learning/test/runTests.ipkg @@ -0,0 +1,8 @@ +package runTests + +depends = mypkg + +modules = Tests +main = Tests + +executable = runTests diff --git a/lean/learning/.gitignore b/lean/learning/.gitignore new file mode 100644 index 0000000..378eac2 --- /dev/null +++ b/lean/learning/.gitignore @@ -0,0 +1 @@ +build diff --git a/lean/learning/LeanSandbox.lean b/lean/learning/LeanSandbox.lean new file mode 100644 index 0000000..e99d3a6 --- /dev/null +++ b/lean/learning/LeanSandbox.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/lean/learning/LeanSandbox/Integers.lean b/lean/learning/LeanSandbox/Integers.lean new file mode 100644 index 0000000..d984d58 --- /dev/null +++ b/lean/learning/LeanSandbox/Integers.lean @@ -0,0 +1,397 @@ +import LeanSandbox.Nat + +macro "nat_ring_all" : tactic => `(simp_all [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm, Nat.left_distrib, Nat.right_distrib]) +macro "nat_ring" : tactic => `(simp [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm, Nat.left_distrib, Nat.right_distrib]) +macro "quotient_madness" : tactic => `(simp [Quotient.mk', Quotient.mk, Quotient.liftOn₂, Quotient.lift₂, Quotient.lift]) + +structure RawInt where + pos : Nat + neg : Nat + deriving Repr + +private def eqv : (x y: RawInt) → Prop + | ⟨a, b⟩, ⟨c, d⟩ => a + d = c + b + +infix:50 " ~ " => eqv + +private theorem eqv.refl (x: RawInt) : x ~ x := rfl +private theorem eqv.symm {x y: RawInt} (xy: x ~ y): y ~ x := Eq.symm xy +/- +a - b c - d e - f +a + d = c + b +c + f = e + d + => a + f = e + b -- the target + +a + d + c + f = c + b + e + d +a + f + e + b -- done +-/ +private theorem eqv.trans {x y z: RawInt} (xy: x ~ y) (yz: y ~ z): x ~ z := by + have summed: _ := Nat.add_equations xy yz + apply @Nat.add_right_cancel _ (y.pos + y.neg) _ + nat_ring_all + +private theorem is_equivalence: Equivalence eqv := + { refl := eqv.refl, symm := eqv.symm, trans := eqv.trans } + +instance rawIntSetoid: Setoid RawInt where + r := eqv + iseqv := is_equivalence + +def MyInt: Type := + Quotient rawIntSetoid + +private theorem eqv.sound: x ~ y → Quotient.mk' x = Quotient.mk' y := Quot.sound + +@[simp] +def MyInt.mk (pos neg: Nat): MyInt := Quotient.mk' ⟨pos, neg⟩ + +notation "{ " a₁ ", " a₂ " }" => MyInt.mk a₁ a₂ + +@[simp, inline] +private def MyInt.ofRawInt(raw: RawInt) := MyInt.mk raw.pos raw.neg + +@[simp, inline] +private def RawInt.ofNat(nat: Nat): RawInt := ⟨nat, 0⟩ + +@[simp, inline] +private def MyInt.ofNat(nat: Nat): MyInt := {nat, 0} + +private instance rawIntOfNat: OfNat RawInt n where + ofNat := RawInt.ofNat n + +instance myIntOfNat: OfNat MyInt n where + ofNat := MyInt.ofNat n + +namespace MyInt + private def negateRawInt: RawInt → MyInt + | ⟨pos, neg⟩ => {neg, pos} + + /- + a - b = c - d + a + d = c + b + + b + c = d + a + b - a = d - c + -/ + private theorem negateRawInt.respects {x y: RawInt} (xy: x ~ y): negateRawInt x = negateRawInt y := by + apply eqv.sound + simp_all [eqv, Nat.add_comm] + + def negate (τ: MyInt): MyInt := + Quotient.liftOn τ negateRawInt @negateRawInt.respects + + instance negMyInt: Neg MyInt where + neg := negate + + private theorem double_neg_elim: ∀x, x = negate (negate x) := by + intro x + induction x using Quotient.ind + rfl + + private def addRawInts: RawInt → RawInt → MyInt + | ⟨a, b⟩, ⟨c, d⟩ => {a + c, b + d} + + private theorem addRawInts.respects + {a b c d: RawInt} + (ac: a ~ c) + (bd: b ~ d): addRawInts a b = addRawInts c d := by + have summed: _ := Nat.add_equations ac bd + apply eqv.sound + simp [eqv] at summed ⊢ + nat_ring_all + + private theorem addRawInts.comm (a b: RawInt): addRawInts a b = addRawInts b a := by + simp_all [addRawInts, Nat.add_comm] + + def add (τ β: MyInt): MyInt := + Quotient.liftOn₂ τ β addRawInts @addRawInts.respects + + private instance hAddRawInts: HAdd RawInt RawInt MyInt where + hAdd := addRawInts + instance addMyInts: Add MyInt where + add := add + + def sub (a b: MyInt): MyInt := a + (-b) + + instance subMyInt: Sub MyInt where + sub := sub + + @[simp] + theorem sub.x_minus_x_is_zero (a: MyInt): a - a = 0 := by + simp_all [HSub.hSub, sub, HAdd.hAdd, add, negate, Neg.neg, MyInt.ofNat] + induction a using Quotient.ind + apply eqv.sound + simp [eqv] + apply Nat.add_comm + + theorem add.comm: ∀x y: MyInt, x + y = y + x := by + intro x y + simp_all [HAdd.hAdd, add] + induction x, y using Quotient.ind₂ + quotient_madness + apply addRawInts.comm + + theorem add.assoc(x y z: MyInt): x + (y + z) = (x + y) + z := by + simp_all [HAdd.hAdd, add] + + induction x, y using Quotient.ind₂ + induction z using Quotient.ind + + apply eqv.sound + simp [eqv] + nat_ring_all + + @[simp] + theorem add.zero(x: MyInt): x + 0 = x := by + simp_all [HAdd.hAdd, add] + induction x using Quotient.ind + apply eqv.sound + simp [eqv] + + /- + (a - b) * (c - d) + ac - bc - ad + bd + -/ + private def multiplyRawInts: RawInt → RawInt → MyInt + | ⟨a, b⟩, ⟨c, d⟩ => {a * c + b * d, b * c + a * d} + + /- + ac : c.neg + a.pos = a.neg + c.pos + bd : d.neg + b.pos = b.neg + d.pos + ⊢ a.neg * b.neg + (a.pos * b.pos + (c.pos * d.neg + c.neg * d.pos)) = + c.neg * d.neg + (a.pos * b.neg + (a.neg * b.pos + c.pos * d.pos)) + + a - b c - d e - f g - h + + f + a = b + e + h + c = d + g + + bd + ac + eh + fg = fh + ad + bc + eg + + bd + ac + fc + eh + fg + ec = fh + ad + bc + ec + eg + fc + + cf + ce + bd + c(a + f) + eh + fg + ec = fh + ad + c(b + e) + eg + fc + bd + eh + fg + ec = fh + ad + eg + fc + bd + e(h + c) + fg = f(h + c) + ad + eg + + bg + ag + b(d + g) + e(h + c) + fg + ag = f(h + c) + a(d + g) + bg + eg + (h + c)(b + e) + g(a + f) = (h + c)(f + a) + g(b + e) + -/ + private theorem multiplyRawInts.respects: ∀ + {x y z w: RawInt} + (xz: x ~ z) + (yw: y ~ w), (multiplyRawInts x y = multiplyRawInts z w) + | ⟨a, b⟩, ⟨c, d⟩, ⟨e, f⟩, ⟨g, h⟩ => by + intro xz yw + apply eqv.sound + simp_all [eqv] + + have first: (c + h) * (b + e) + g * (a + f) + c * (a + f) + = (c + h) * (f + a) + g * (b + e) + c * (b + e) := by + simp [Nat.add_comm, xz, yw] + + have second: b * (d + g) + e * (c + h) + c * (a + f) + f * g + a * g + = f * (c + h) + a * (d + g) + c * (b + e) + b * g + e * g := by + simp [yw, xz] at first ⊢ + conv at first in g * (e + b) => rw [<-xz] + conv at first => tactic => nat_ring + nat_ring + exact first + + conv at second => tactic => nat_ring + apply @Nat.subtract_to_equation_left _ _ + (a * g + b * g + c * f + c * e) + + nat_ring_all + + def multiply (τ β: MyInt): MyInt := + Quotient.liftOn₂ τ β multiplyRawInts @multiplyRawInts.respects + + private instance hMulRawInt: HMul RawInt RawInt MyInt where + hMul := multiplyRawInts + instance mulMyInt: Mul MyInt where + mul := multiply + + private theorem multiplyRawInts.comm (a b: RawInt): a * b = b * a := by + apply eqv.sound + simp [eqv] + simp_all [multiplyRawInts, Nat.mul_comm] + nat_ring_all + + theorem multiply.comm (a b: MyInt): a * b = b * a := by + simp_all [Mul.mul, multiply] + induction a, b using Quotient.ind₂ + quotient_madness + apply multiplyRawInts.comm + + theorem multiply.assoc(x y z: MyInt): x * (y * z) = (x * y) * z := by + simp_all [Mul.mul, multiply] + + induction x, y using Quotient.ind₂ + induction z using Quotient.ind + + apply eqv.sound + simp [eqv] + nat_ring_all + + @[simp] + theorem multiply.one(x: MyInt): x * 1 = 1 * x := by + simp_all [Mul.mul, multiply] + induction x using Quotient.ind + apply eqv.sound + simp [eqv] + + @[simp] + theorem multiply.zero(x: MyInt): x * 0 = 0 := by + simp_all [Mul.mul, multiply] + induction x using Quotient.ind + apply eqv.sound + simp [eqv] + + theorem left_distrib(x y z: MyInt): x * (y + z) = x * y + x * z := by + simp_all [Mul.mul, Add.add, add, multiply] + + induction x, y using Quotient.ind₂ + induction z using Quotient.ind + + apply eqv.sound + simp [eqv] + nat_ring_all + + theorem right_distrib(x y z: MyInt): (x + y) * z = x * z + y * z := by + simp_all [Mul.mul, Add.add, add, multiply] + + induction x, y using Quotient.ind₂ + induction z using Quotient.ind + + apply eqv.sound + simp [eqv] + nat_ring_all + + /- + notes on division? + t * (c - d) + r = a - b + t * c + b + r = a + t * d + -/ + @[simp] + def is_even(x: MyInt) := ∃h, h + h = x + @[simp] + def is_odd(x: MyInt) := ∃h, h + h + 1 = x + + theorem double_is_even(x: MyInt): is_even (2 * x) := by + simp + exists x + induction x using Quotient.ind + apply eqv.sound + simp [eqv, Nat.double.addition_is_multiplication] + + theorem raw_int_induction + (P: MyInt → Prop) + (pz: P 0) + (pn: ∀k, P k ↔ P (k + 1)): + (x: RawInt) → ∃k, k ~ x ∧ P (MyInt.ofRawInt k) + | ⟨0, 0⟩ => ⟨0, ⟨rfl, pz⟩⟩ + | ⟨Nat.succ a, 0⟩ => by + have ⟨⟨kp, kn⟩, pk⟩ := raw_int_induction P pz pn ⟨a, 0⟩ + exists (⟨kp + 1, kn⟩ : RawInt) + apply And.intro + . simp [eqv, Nat.succ_add] + rw [<-pk.left] + simp [Nat.add_zero] + . apply (@pn {kp, kn}).mp + exact pk.right + | ⟨Nat.succ a, Nat.succ b⟩ => by + have ⟨k, pk⟩ := raw_int_induction P pz pn ⟨a, b⟩ + exists k + apply And.intro + . simp [eqv, Nat.succ_add] + rw [<-pk.left] + simp_arith + . exact pk.right + | ⟨0, Nat.succ a⟩ => by + have ⟨⟨kp, kn⟩, pk⟩ := raw_int_induction P pz pn ⟨0, a⟩ + exists (⟨kp, kn + 1⟩ : RawInt) + apply And.intro + . have pkl := pk.left + simp [eqv, Nat.succ_add, Nat.add_zero] at pkl ⊢ + rw [<-pkl] + simp_arith + . have recurse := (@pn {kp, kn + 1}).mpr + have rewriter: {kp, kn + 1} + 1 = {kp, kn} := by + apply eqv.sound + simp [eqv] + simp_arith + rw [rewriter] at recurse + exact (recurse pk.right) + + theorem int_induction + (P: MyInt → Prop) + (zero: P 0) + (succ: ∀k, P k ↔ P (k + 1)): + ∀k, P k := by + intro k + induction k using Quotient.ind + rename RawInt => kRaw + have ⟨e, ⟨eIsK, proof⟩⟩ := raw_int_induction P zero succ kRaw + have eIsKQuot : MyInt.ofRawInt e = MyInt.ofRawInt kRaw := by + exact (eqv.sound eIsK) + simp [Quotient.mk'] at eIsKQuot + rw [<-eIsKQuot] + exact proof + + theorem add_left_cancel {a b c: MyInt}: a + b = a + c → b = c := by + intro hip + induction b, c using Quotient.ind₂ + induction a using Quotient.ind + rename RawInt => c + simp_all [HAdd.hAdd, Add.add, add] + conv at hip => tactic => quotient_madness + /- apply eqv.sound -/ + /- simp [eqv] -/ + /- nat_ring -/ + simp_all [MyInt.addRawInts, Quotient.mk', Quotient.mk] + sorry + +/- induction a using int_induction with -/ +/- | zero => -/ +/- rw [add.comm 0 c, add.comm 0 b] -/ +/- simp_all -/ +/- | succ k => -/ +/- apply Iff.intro -/ +/- . intro win -/ +/- intro previous -/ +/- have p: k + b = k + c := by -/ +/- rw [add.comm k 1] at previous -/ +/- induction b, c using Quotient.ind₂ -/ +/- induction k using Quotient.ind -/ +/- rename RawInt => c -/ +/- simp [HAdd.hAdd, Add.add, add] -/ +/- apply eqv.sound -/ +/- simp [eqv] -/ +/- nat_ring -/ +/- -/ +/- sorry -/ +/- exact (win p) -/ +/- . sorry -/ +/- -/ + + theorem odd_and_even_contradict(x: MyInt): ¬(is_odd x ∧ is_even x) + | ⟨⟨h₁, oddProof⟩, ⟨h₂, evenProof⟩⟩ => by + have wrong: (1: MyInt) = 0 := by + apply @add_left_cancel (h₁ + h₂) + exact oddProof.trans evenProof.symm + sorry + contradiction + + theorem odds_not_even(x: MyInt): is_odd x ↔ ¬(is_even x) := by + apply Iff.intro + case mp => + intro oddProof + intro evenProof + apply odd_and_even_contradict x + exact ⟨oddProof, evenProof⟩ + case mpr => + simp [is_even, is_odd] + sorry + +end MyInt diff --git a/lean/learning/LeanSandbox/Nat.lean b/lean/learning/LeanSandbox/Nat.lean new file mode 100644 index 0000000..e750847 --- /dev/null +++ b/lean/learning/LeanSandbox/Nat.lean @@ -0,0 +1,55 @@ +namespace Nat + theorem add_equations: ∀{a b c d: Nat}, a = b → c = d → a + c = b + d := by + intro a b c d ab cd + rw [ab, cd] + + theorem add_to_equation_right: ∀{a b c: Nat}, a = b → a + c = b + c := by + intro a b c ab + exact add_equations ab rfl + + theorem succ_equation : ∀{a b: Nat}, Nat.succ a = Nat.succ b → a = b := by + intro a b + apply Eq.mp -- (a + 1 = b + 1) = a + b + apply Nat.succ.injEq -- this was already here? + + inductive A : Nat -> Type + | ooo: (n: Nat) → A n + + theorem subtract_to_equation_right: ∀{a b c: Nat}, a + c = b + c → a = b := by + intro a b c acbc + induction c with + | zero => + repeat rw [Nat.add_zero] at acbc + exact acbc + | succ pc inner => + /- + a + S pc = b + S pc -- comm + S pc + a = S pc + b -- addition definition + S (pc + a) = S (pc + b) -- injective constructor + pc + a = pc + b + -/ + rw [Nat.add_comm a (Nat.succ pc), Nat.add_comm b (Nat.succ pc)] at acbc + simp [Nat.succ_add, Nat.add_comm] at acbc + exact (inner acbc) + + theorem subtract_to_equation_left: ∀{a b c: Nat}, c + a = c + b → a = b := by + intro a b c cacb + rw [Nat.add_comm c a, Nat.add_comm c b] at cacb + exact (subtract_to_equation_right cacb) + + theorem add_equation_both_sides_right: ∀{a b c: Nat}, (a = b) ↔ (a + c = b + c) := by + intro a b c + apply Iff.intro + . exact add_to_equation_right + . exact subtract_to_equation_right + + theorem multiply_equation_left: ∀{a b c: Nat}, (a = b) → (c * a = c * b) := by + intro a b c ab + rw [ab] + + theorem double.addition_is_multiplication (x: Nat): 2 * x = x + x := by + induction x with + | zero => simp + | succ px ic => + simp [<-Nat.add_one, Nat.left_distrib, ic, Nat.add_left_comm, Nat.add_assoc] +end Nat diff --git a/lean/learning/LeanSandbox/Noob.lean b/lean/learning/LeanSandbox/Noob.lean new file mode 100644 index 0000000..894dae1 --- /dev/null +++ b/lean/learning/LeanSandbox/Noob.lean @@ -0,0 +1,289 @@ +-- single line comment +universe u + +def m: Nat := 1 + +#check m +#check m + +#check (m + m) +#eval (m + m) + +#check Nat × Nat + +def Γ := 2 + m + + +def double (a: Nat) := a + a + +#eval double (double 3) + +section composition + variable (α β γ: Type) + + def compose (f: α → β) (g: β → γ): (α -> γ) := fun x: α => g (f x) +end composition + +def quadruble := compose _ _ _ double double + +#print compose + +section composition' + variable (α β γ : Type) + variable (g : β → γ) (f : α → β) (h : α → α) + variable (x : α) + + def compose' := g (f x) + def doTwice := h (h x) + def doThrice := h (h (h x)) +end composition' + +def a: Nat := 3 + +#eval double a +#print compose' +#check (Nat : Sort 1) +#check (Prop : Sort 1) +#check (Prop : Type) + + +section proofs + theorem hmm (α: Prop) (β: Prop): Prop := α + theorem hmm2 : Prop -> Prop -> Prop := + fun α β => show Prop from α + + theorem hmm3 (hm: α): α := hm + + axiom myProof: Prop + + #check hmm + #check hmm2 + #check hmm3 myProof + #check @hmm3 + #check @hmm3 myProof +end proofs + +section logic + variable {α β π: Prop} + variable (ha: α) (hb: β) + + theorem pair: α -> β -> α ∧ β := fun a b => And.intro a b + theorem unpair: (α → β → π) → α ∧ β → π := fun f a => + show π from f (And.left a) (And.right a) + + theorem pairsCommute: (α ∧ β) → (β ∧ α) := fun p => + show (β ∧ α) from And.intro (And.right p) (And.left p) + + example (h: α ∧ β): β ∧ α := ⟨h.right, h.left⟩ + + theorem thrice: (f: α) -> α ∧ α ∧ α := fun f => ⟨ f, f, f ⟩ + + theorem negateFunc: (β → α) → ¬α → ¬β := + fun f notₐ b => + show False from notₐ (f b) + + #print pairsCommute + #check (⟨ha, hb⟩: α ∧ β) + + theorem exFalso: (α ∧ ¬ α) → β := + fun contradiction => + show β from (contradiction.right contradiction.left).elim + + theorem pairIso: α ∧ β ↔ β ∧ α := ⟨ pairsCommute, pairsCommute ⟩ +end logic + +section classical + open Classical + + variable (α : Prop) + + def dneT: Prop := ¬¬α → α + + theorem doubleNegation: α ↔ ¬¬α := + suffices l: α → ¬¬α from + suffices r: ¬¬α → α from ⟨ l, r ⟩ + show dneT α from fun doubleNegA => (em α).elim + (fun p: α => p) + (fun p: ¬α => absurd p doubleNegA) + show α → ¬¬α from (fun a f => f a) + + #print byCases + + theorem dne: dneT α := fun nnₚ => + byCases id + (fun nₚ => (nnₚ nₚ).elim) + + #print byContradiction + + theorem dne': dneT α := fun nnₚ => + byContradiction fun nₚ => nnₚ nₚ +end classical + +section exercises + variable (p q r : Prop) + + theorem noContradictions : ¬(p ↔ ¬p) := + fun contradiction => + suffices someP: p from contradiction.mp someP someP + suffices someNotP: ¬p from show p from contradiction.mpr someNotP + show ¬p from fun p => contradiction.mp p p +end exercises + +section quantifiers + variable (α: Type) (r: α → α → Prop) + variable (transitivity: ∀x y z, r x y → r y z → r x z) + variable (n: Nat) + + variable (trans2: ∀x y z, r x y → r y z → r x z) + variable (trans3: ∀τ β ω, r τ β → r β ω → r τ ω) + + axiom someA: α + + #print someA + #check transitivity + + #print Eq.subst + + theorem substTest: (a b c: Nat) → (myProp: Nat -> Prop) → + (a + b = c) → myProp c → myProp (a + b) := + fun a b c myProp p₁ l => @Eq.subst Nat (fun a => myProp a) c (a + b) p₁.symm l + theorem substTest': {a b c: Nat} → {myProp: Nat -> Prop} → + (a + b = c) → myProp c → myProp (a + b) := + fun p₁ l => p₁ ▸ l + + #check @congr + #print congrArg + #print congrFun + + theorem congrArgTest: {a b: Nat} → (c: Nat) → (a = b) → (a + c = b + c) := + fun c p₁ => congrArg (fun a => a + c) p₁ + +end quantifiers + +section calc_ + variable (a b c d e : Nat) + variable (h1 : a = b) + variable (h2 : b = c + 1) + variable (h3 : c = d) + variable (h4 : e = 1 + d) + + theorem T : a = e := + calc + a = b := h1 + _ = c + 1 := h2 + _ = d + 1 := congrArg Nat.succ h3 + _ = 1 + d := Nat.add_comm d 1 + _ = e := h4.symm + + theorem T₂ : a = e := + calc + a = b := h1 + _ = c + 1 := h2 + _ = d + 1 := by rw [h3] + _ = 1 + d := by rw [Nat.add_comm] + _ = e := by rw [h4] + + theorem T₃ : a = e := + by rw [h1, h2, h3, Nat.add_comm, h4] + + theorem T₄ : a = e := + by simp [h1, h2, h3, Nat.add_comm, h4] + + example (a b c d : Nat) (h1 : a = b) (h2 : b ≤ c) (h3 : c + 1 < d) : a < d := + calc + a = b := h1 + _ < b + 1 := Nat.lt_succ_self b + _ ≤ c + 1 := Nat.succ_le_succ h2 + _ < d := h3 + + variable (x y: Nat) + + theorem A₁: (x + y) * (x + y) = x * x + y * x + x * y + y * y := + calc + (x + y) * (x + y) = (x + y) * x + (x + y) * y := by rw [Nat.mul_add] + _ = x * x + y * x + (x * y + y * y) := by simp [Nat.add_mul] + _ = x * x + y * x + x * y + y * y := by rw [←Nat.add_assoc] + + theorem A₂: (x + y) * (x + y) = x * x + y * x + x * y + y * y := + by simp [Nat.add_mul, Nat.mul_add, Nat.add_assoc] + + axiom forallTest: ¬(∀a: Nat, a + a = a + 1) + + theorem existsOne: ∃a: Nat, a + a = a + 1 := ⟨ 1, rfl ⟩ + theorem existsBiggerThanOne: ∃a: Nat, a > 1 := + have r: 1 < 2 := Nat.succ_lt_succ (Nat.zero_lt_succ 0) + ⟨ 2, r ⟩ + + example (x : Nat) (h : x > 0) : ∃ y, y < x := + ⟨ 0, h ⟩ +end calc_ + +section exists_print + variable (g : Nat → Nat → Nat) + variable (hg : g 0 0 = 0) + + theorem gex1 : ∃ x, g x x = x := ⟨0, hg⟩ + theorem gex2 : ∃ x, g x 0 = x := ⟨0, hg⟩ + theorem gex3 : ∃ x, g 0 0 = x := ⟨0, hg⟩ + theorem gex4 : ∃ x, g x x = 0 := ⟨0, hg⟩ + + theorem gex5 : ∃ x, g x x = 0 := ⟨0, hg⟩ + theorem gex6 : ∃ x, g x x = 0 := ⟨0, hg⟩ + theorem gex7 : ∃ x, g x x = 0 := ⟨0, hg⟩ + + set_option pp.explicit true -- display implicit arguments + #print gex1 + #print gex2 + #print gex3 + #print gex4 +end exists_print + +section existentials + variable (α : Type) (p q : α → Prop) + + example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x := + match h with + | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩ + + theorem _matches : (n: Nat) → n + 1 = 1 + n := fun n => + match n with + | Nat.succ w => calc + Nat.succ w + 1 = Nat.succ (w + 1) := rfl + _ = Nat.succ (1 + w) := by rw [_matches w] + _ = 1 + Nat.succ w := rfl + | Nat.zero => rfl +end existentials + +section tactics + theorem test (p q : Prop) (hp: p) (hq: q): p ∧ q ∧ p := by + apply And.intro + case left => + exact hp + case right => + apply And.intro hq hp + + #print test + + theorem test₂ (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by + apply Iff.intro + . intro h + apply Or.elim h.right + . intro hq + apply Or.inl + exact ⟨h.left, hq⟩ + . intro hr + apply Or.inr + exact ⟨h.left, hr⟩ + . intro h + apply Or.elim h + . intro pq + apply And.intro + . exact pq.left + . exact Or.inl pq.right + . intro pr + apply And.intro + . exact pr.left + . exact Or.inr pr.right + + #print test₂ +end tactics diff --git a/lean/learning/Main.lean b/lean/learning/Main.lean new file mode 100644 index 0000000..f42a224 --- /dev/null +++ b/lean/learning/Main.lean @@ -0,0 +1,4 @@ +import LeanSandbox + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/lean/learning/lakefile.lean b/lean/learning/lakefile.lean new file mode 100644 index 0000000..ddc3fb0 --- /dev/null +++ b/lean/learning/lakefile.lean @@ -0,0 +1,6 @@ +import Lake +open Lake DSL + +package «lean-sandbox» { + -- add configuration options here +} diff --git a/abilities/.gitignore b/purescript/abilities/.gitignore similarity index 100% rename from abilities/.gitignore rename to purescript/abilities/.gitignore diff --git a/abilities/a.txt b/purescript/abilities/a.txt similarity index 100% rename from abilities/a.txt rename to purescript/abilities/a.txt diff --git a/abilities/b.txt b/purescript/abilities/b.txt similarity index 100% rename from abilities/b.txt rename to purescript/abilities/b.txt diff --git a/abilities/packages.dhall b/purescript/abilities/packages.dhall similarity index 100% rename from abilities/packages.dhall rename to purescript/abilities/packages.dhall diff --git a/abilities/spago.dhall b/purescript/abilities/spago.dhall similarity index 100% rename from abilities/spago.dhall rename to purescript/abilities/spago.dhall diff --git a/abilities/src/Abilities.purs b/purescript/abilities/src/Abilities.purs similarity index 100% rename from abilities/src/Abilities.purs rename to purescript/abilities/src/Abilities.purs diff --git a/abilities/src/Ask.js b/purescript/abilities/src/Ask.js similarity index 100% rename from abilities/src/Ask.js rename to purescript/abilities/src/Ask.js diff --git a/abilities/src/Ask.purs b/purescript/abilities/src/Ask.purs similarity index 100% rename from abilities/src/Ask.purs rename to purescript/abilities/src/Ask.purs diff --git a/abilities/src/Io.purs b/purescript/abilities/src/Io.purs similarity index 100% rename from abilities/src/Io.purs rename to purescript/abilities/src/Io.purs diff --git a/abilities/src/Main.purs b/purescript/abilities/src/Main.purs similarity index 100% rename from abilities/src/Main.purs rename to purescript/abilities/src/Main.purs diff --git a/abilities/test/Main.purs b/purescript/abilities/test/Main.purs similarity index 100% rename from abilities/test/Main.purs rename to purescript/abilities/test/Main.purs diff --git a/bug/.gitignore b/purescript/bug/.gitignore similarity index 100% rename from bug/.gitignore rename to purescript/bug/.gitignore diff --git a/bug/packages.dhall b/purescript/bug/packages.dhall similarity index 100% rename from bug/packages.dhall rename to purescript/bug/packages.dhall diff --git a/bug/spago.dhall b/purescript/bug/spago.dhall similarity index 100% rename from bug/spago.dhall rename to purescript/bug/spago.dhall diff --git a/bug/src/Main.purs b/purescript/bug/src/Main.purs similarity index 100% rename from bug/src/Main.purs rename to purescript/bug/src/Main.purs diff --git a/bug/src/other/spago.dhall b/purescript/bug/src/other/spago.dhall similarity index 100% rename from bug/src/other/spago.dhall rename to purescript/bug/src/other/spago.dhall diff --git a/bug/src/other/src/Foo.purs b/purescript/bug/src/other/src/Foo.purs similarity index 100% rename from bug/src/other/src/Foo.purs rename to purescript/bug/src/other/src/Foo.purs diff --git a/bug/test/Main.purs b/purescript/bug/test/Main.purs similarity index 100% rename from bug/test/Main.purs rename to purescript/bug/test/Main.purs diff --git a/compose/.gitignore b/purescript/compose/.gitignore similarity index 100% rename from compose/.gitignore rename to purescript/compose/.gitignore diff --git a/compose/packages.dhall b/purescript/compose/packages.dhall similarity index 100% rename from compose/packages.dhall rename to purescript/compose/packages.dhall diff --git a/compose/spago.dhall b/purescript/compose/spago.dhall similarity index 100% rename from compose/spago.dhall rename to purescript/compose/spago.dhall diff --git a/compose/src/Compose.purs b/purescript/compose/src/Compose.purs similarity index 100% rename from compose/src/Compose.purs rename to purescript/compose/src/Compose.purs diff --git a/compose/src/Main.purs b/purescript/compose/src/Main.purs similarity index 100% rename from compose/src/Main.purs rename to purescript/compose/src/Main.purs diff --git a/compose/test/Main.purs b/purescript/compose/test/Main.purs similarity index 100% rename from compose/test/Main.purs rename to purescript/compose/test/Main.purs diff --git a/ecs/.gitignore b/purescript/ecs/.gitignore similarity index 100% rename from ecs/.gitignore rename to purescript/ecs/.gitignore diff --git a/ecs/package.json b/purescript/ecs/package.json similarity index 100% rename from ecs/package.json rename to purescript/ecs/package.json diff --git a/ecs/packages.dhall b/purescript/ecs/packages.dhall similarity index 100% rename from ecs/packages.dhall rename to purescript/ecs/packages.dhall diff --git a/ecs/pnpm-lock.yaml b/purescript/ecs/pnpm-lock.yaml similarity index 100% rename from ecs/pnpm-lock.yaml rename to purescript/ecs/pnpm-lock.yaml diff --git a/ecs/spago.dhall b/purescript/ecs/spago.dhall similarity index 100% rename from ecs/spago.dhall rename to purescript/ecs/spago.dhall diff --git a/ecs/src/Main.purs b/purescript/ecs/src/Main.purs similarity index 100% rename from ecs/src/Main.purs rename to purescript/ecs/src/Main.purs diff --git a/ecs/src/Types.js b/purescript/ecs/src/Types.js similarity index 100% rename from ecs/src/Types.js rename to purescript/ecs/src/Types.js diff --git a/ecs/src/Types.purs b/purescript/ecs/src/Types.purs similarity index 100% rename from ecs/src/Types.purs rename to purescript/ecs/src/Types.purs diff --git a/ecs/src/Utils/Keys.purs b/purescript/ecs/src/Utils/Keys.purs similarity index 100% rename from ecs/src/Utils/Keys.purs rename to purescript/ecs/src/Utils/Keys.purs diff --git a/ecs/test/Main.purs b/purescript/ecs/test/Main.purs similarity index 100% rename from ecs/test/Main.purs rename to purescript/ecs/test/Main.purs diff --git a/ecs/tsconfig.json b/purescript/ecs/tsconfig.json similarity index 100% rename from ecs/tsconfig.json rename to purescript/ecs/tsconfig.json diff --git a/existentials-blog/.gitignore b/purescript/existentials-blog/.gitignore similarity index 100% rename from existentials-blog/.gitignore rename to purescript/existentials-blog/.gitignore diff --git a/existentials-blog/packages.dhall b/purescript/existentials-blog/packages.dhall similarity index 100% rename from existentials-blog/packages.dhall rename to purescript/existentials-blog/packages.dhall diff --git a/existentials-blog/spago.dhall b/purescript/existentials-blog/spago.dhall similarity index 100% rename from existentials-blog/spago.dhall rename to purescript/existentials-blog/spago.dhall diff --git a/existentials-blog/src/Exists.purs b/purescript/existentials-blog/src/Exists.purs similarity index 100% rename from existentials-blog/src/Exists.purs rename to purescript/existentials-blog/src/Exists.purs diff --git a/existentials-blog/src/Main.purs b/purescript/existentials-blog/src/Main.purs similarity index 100% rename from existentials-blog/src/Main.purs rename to purescript/existentials-blog/src/Main.purs diff --git a/existentials-blog/test/Main.purs b/purescript/existentials-blog/test/Main.purs similarity index 100% rename from existentials-blog/test/Main.purs rename to purescript/existentials-blog/test/Main.purs diff --git a/existentials/packages.dhall b/purescript/existentials/packages.dhall similarity index 100% rename from existentials/packages.dhall rename to purescript/existentials/packages.dhall diff --git a/existentials/spago.dhall b/purescript/existentials/spago.dhall similarity index 100% rename from existentials/spago.dhall rename to purescript/existentials/spago.dhall diff --git a/existentials/src/Main.purs b/purescript/existentials/src/Main.purs similarity index 100% rename from existentials/src/Main.purs rename to purescript/existentials/src/Main.purs diff --git a/gadts/.gitignore b/purescript/gadts/.gitignore similarity index 100% rename from gadts/.gitignore rename to purescript/gadts/.gitignore diff --git a/gadts/packages.dhall b/purescript/gadts/packages.dhall similarity index 100% rename from gadts/packages.dhall rename to purescript/gadts/packages.dhall diff --git a/gadts/spago.dhall b/purescript/gadts/spago.dhall similarity index 100% rename from gadts/spago.dhall rename to purescript/gadts/spago.dhall diff --git a/gadts/src/Ast.purs b/purescript/gadts/src/Ast.purs similarity index 100% rename from gadts/src/Ast.purs rename to purescript/gadts/src/Ast.purs diff --git a/gadts/src/Main.purs b/purescript/gadts/src/Main.purs similarity index 100% rename from gadts/src/Main.purs rename to purescript/gadts/src/Main.purs diff --git a/gadts/src/RunLift.purs b/purescript/gadts/src/RunLift.purs similarity index 100% rename from gadts/src/RunLift.purs rename to purescript/gadts/src/RunLift.purs diff --git a/gadts/test/Main.purs b/purescript/gadts/test/Main.purs similarity index 100% rename from gadts/test/Main.purs rename to purescript/gadts/test/Main.purs diff --git a/lune/.gitignore b/purescript/lune/.gitignore similarity index 100% rename from lune/.gitignore rename to purescript/lune/.gitignore diff --git a/lune/packages.dhall b/purescript/lune/packages.dhall similarity index 100% rename from lune/packages.dhall rename to purescript/lune/packages.dhall diff --git a/lune/spago.dhall b/purescript/lune/spago.dhall similarity index 100% rename from lune/spago.dhall rename to purescript/lune/spago.dhall diff --git a/lune/src/Handle.js b/purescript/lune/src/Handle.js similarity index 100% rename from lune/src/Handle.js rename to purescript/lune/src/Handle.js diff --git a/lune/src/Handle.purs b/purescript/lune/src/Handle.purs similarity index 100% rename from lune/src/Handle.purs rename to purescript/lune/src/Handle.purs diff --git a/lune/src/Lists.purs b/purescript/lune/src/Lists.purs similarity index 100% rename from lune/src/Lists.purs rename to purescript/lune/src/Lists.purs diff --git a/lune/src/Main.purs b/purescript/lune/src/Main.purs similarity index 100% rename from lune/src/Main.purs rename to purescript/lune/src/Main.purs diff --git a/lune/test/Main.purs b/purescript/lune/test/Main.purs similarity index 100% rename from lune/test/Main.purs rename to purescript/lune/test/Main.purs diff --git a/maps/.gitignore b/purescript/maps/.gitignore similarity index 100% rename from maps/.gitignore rename to purescript/maps/.gitignore diff --git a/maps/packages.dhall b/purescript/maps/packages.dhall similarity index 100% rename from maps/packages.dhall rename to purescript/maps/packages.dhall diff --git a/maps/spago.dhall b/purescript/maps/spago.dhall similarity index 100% rename from maps/spago.dhall rename to purescript/maps/spago.dhall diff --git a/maps/src/Composable.purs b/purescript/maps/src/Composable.purs similarity index 100% rename from maps/src/Composable.purs rename to purescript/maps/src/Composable.purs diff --git a/maps/src/Main.purs b/purescript/maps/src/Main.purs similarity index 100% rename from maps/src/Main.purs rename to purescript/maps/src/Main.purs diff --git a/maps/src/Map.purs b/purescript/maps/src/Map.purs similarity index 100% rename from maps/src/Map.purs rename to purescript/maps/src/Map.purs diff --git a/maps/test/Main.purs b/purescript/maps/test/Main.purs similarity index 100% rename from maps/test/Main.purs rename to purescript/maps/test/Main.purs diff --git a/proofs/.gitignore b/purescript/proofs/.gitignore similarity index 100% rename from proofs/.gitignore rename to purescript/proofs/.gitignore diff --git a/proofs/packages.dhall b/purescript/proofs/packages.dhall similarity index 100% rename from proofs/packages.dhall rename to purescript/proofs/packages.dhall diff --git a/proofs/spago.dhall b/purescript/proofs/spago.dhall similarity index 100% rename from proofs/spago.dhall rename to purescript/proofs/spago.dhall diff --git a/proofs/src/Main.purs b/purescript/proofs/src/Main.purs similarity index 100% rename from proofs/src/Main.purs rename to purescript/proofs/src/Main.purs diff --git a/proofs/src/Nats.purs b/purescript/proofs/src/Nats.purs similarity index 100% rename from proofs/src/Nats.purs rename to purescript/proofs/src/Nats.purs diff --git a/proofs/src/ValueLevelNaturals.purs b/purescript/proofs/src/ValueLevelNaturals.purs similarity index 100% rename from proofs/src/ValueLevelNaturals.purs rename to purescript/proofs/src/ValueLevelNaturals.purs diff --git a/proofs/test/Main.purs b/purescript/proofs/test/Main.purs similarity index 100% rename from proofs/test/Main.purs rename to purescript/proofs/test/Main.purs diff --git a/purpleflow/.gitignore b/purescript/purpleflow/.gitignore similarity index 100% rename from purpleflow/.gitignore rename to purescript/purpleflow/.gitignore diff --git a/purpleflow/packages.dhall b/purescript/purpleflow/packages.dhall similarity index 100% rename from purpleflow/packages.dhall rename to purescript/purpleflow/packages.dhall diff --git a/purpleflow/packages/core/src/Data/AST.purs b/purescript/purpleflow/packages/core/src/Data/AST.purs similarity index 100% rename from purpleflow/packages/core/src/Data/AST.purs rename to purescript/purpleflow/packages/core/src/Data/AST.purs diff --git a/purpleflow/packages/core/src/Data/CST.purs b/purescript/purpleflow/packages/core/src/Data/CST.purs similarity index 100% rename from purpleflow/packages/core/src/Data/CST.purs rename to purescript/purpleflow/packages/core/src/Data/CST.purs diff --git a/purpleflow/packages/parsing-codec/src/Parser.purs b/purescript/purpleflow/packages/parsing-codec/src/Parser.purs similarity index 100% rename from purpleflow/packages/parsing-codec/src/Parser.purs rename to purescript/purpleflow/packages/parsing-codec/src/Parser.purs diff --git a/purpleflow/spago.dhall b/purescript/purpleflow/spago.dhall similarity index 100% rename from purpleflow/spago.dhall rename to purescript/purpleflow/spago.dhall diff --git a/purpleflow/todo b/purescript/purpleflow/todo similarity index 100% rename from purpleflow/todo rename to purescript/purpleflow/todo diff --git a/sprint/.gitignore b/purescript/sprint/.gitignore similarity index 100% rename from sprint/.gitignore rename to purescript/sprint/.gitignore diff --git a/sprint/packages.dhall b/purescript/sprint/packages.dhall similarity index 100% rename from sprint/packages.dhall rename to purescript/sprint/packages.dhall diff --git a/sprint/spago.dhall b/purescript/sprint/spago.dhall similarity index 100% rename from sprint/spago.dhall rename to purescript/sprint/spago.dhall diff --git a/sprint/src/Main.purs b/purescript/sprint/src/Main.purs similarity index 100% rename from sprint/src/Main.purs rename to purescript/sprint/src/Main.purs diff --git a/sprint/src/Sprint.purs b/purescript/sprint/src/Sprint.purs similarity index 100% rename from sprint/src/Sprint.purs rename to purescript/sprint/src/Sprint.purs diff --git a/sprint/test/Main.purs b/purescript/sprint/test/Main.purs similarity index 100% rename from sprint/test/Main.purs rename to purescript/sprint/test/Main.purs diff --git a/streams/.gitignore b/purescript/streams/.gitignore similarity index 100% rename from streams/.gitignore rename to purescript/streams/.gitignore diff --git a/streams/packages.dhall b/purescript/streams/packages.dhall similarity index 100% rename from streams/packages.dhall rename to purescript/streams/packages.dhall diff --git a/streams/spago.dhall b/purescript/streams/spago.dhall similarity index 100% rename from streams/spago.dhall rename to purescript/streams/spago.dhall diff --git a/streams/src/Main.purs b/purescript/streams/src/Main.purs similarity index 100% rename from streams/src/Main.purs rename to purescript/streams/src/Main.purs diff --git a/streams/test/Main.purs b/purescript/streams/test/Main.purs similarity index 100% rename from streams/test/Main.purs rename to purescript/streams/test/Main.purs diff --git a/typelevel/.gitignore b/purescript/typelevel/.gitignore similarity index 100% rename from typelevel/.gitignore rename to purescript/typelevel/.gitignore diff --git a/typelevel/.vscode/settings.json b/purescript/typelevel/.vscode/settings.json similarity index 100% rename from typelevel/.vscode/settings.json rename to purescript/typelevel/.vscode/settings.json diff --git a/typelevel/packages.dhall b/purescript/typelevel/packages.dhall similarity index 100% rename from typelevel/packages.dhall rename to purescript/typelevel/packages.dhall diff --git a/typelevel/spago.dhall b/purescript/typelevel/spago.dhall similarity index 100% rename from typelevel/spago.dhall rename to purescript/typelevel/spago.dhall diff --git a/typelevel/src/Ast.purs b/purescript/typelevel/src/Ast.purs similarity index 100% rename from typelevel/src/Ast.purs rename to purescript/typelevel/src/Ast.purs diff --git a/typelevel/src/Fin.purs b/purescript/typelevel/src/Fin.purs similarity index 100% rename from typelevel/src/Fin.purs rename to purescript/typelevel/src/Fin.purs diff --git a/typelevel/src/Main.purs b/purescript/typelevel/src/Main.purs similarity index 100% rename from typelevel/src/Main.purs rename to purescript/typelevel/src/Main.purs diff --git a/typelevel/src/Num.purs b/purescript/typelevel/src/Num.purs similarity index 100% rename from typelevel/src/Num.purs rename to purescript/typelevel/src/Num.purs diff --git a/typelevel/src/Ordering.purs b/purescript/typelevel/src/Ordering.purs similarity index 100% rename from typelevel/src/Ordering.purs rename to purescript/typelevel/src/Ordering.purs diff --git a/typelevel/src/Term.purs b/purescript/typelevel/src/Term.purs similarity index 100% rename from typelevel/src/Term.purs rename to purescript/typelevel/src/Term.purs diff --git a/typelevel/src/Vec.purs b/purescript/typelevel/src/Vec.purs similarity index 100% rename from typelevel/src/Vec.purs rename to purescript/typelevel/src/Vec.purs diff --git a/typelevel/test/Main.purs b/purescript/typelevel/test/Main.purs similarity index 100% rename from typelevel/test/Main.purs rename to purescript/typelevel/test/Main.purs