Initialize Lean project

.github/workflows/lean.yml

@@ -0,0 +1,53 @@
+name: Lean (build)
+
+on:
+  push:
+  pull_request:
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+permissions:
+  contents: write # to submit generated documentation to GitHub Pages
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - name: '🧰 Install elan'
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.5/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: '📥 Checkout repository'
+        uses: actions/checkout@v3
+
+      - name: '👝 Cache .lake/'
+        id: cache-lake
+        uses: actions/cache@v3
+        with:
+          path: .lake/
+          key: ${{ runner.os }}-${{ hashFiles('lakefile.lean', 'lake-manifest.json') }}-lake
+
+      - name: '⚙️ Resolve dependencies (inluding docs)'
+        if: steps.cache-lake.outputs.cache-hit != 'true'
+        run: |
+          lake -R -Kenv=dev update
+
+      - name: '🔨 Build Lean package'
+        run: lake build -Kwerror
+
+      - name: '🔨 Generate documentation'
+        run: |
+          lake -R -Kenv=dev build PhiCalculus:docs
+
+      - name: '🚀 Publish Documentation'
+        if: ${{ github.ref_name == 'main' && github.event_name == 'push' }}
+        uses: JamesIves/github-pages-deploy-action@v4
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+          folder: .lake/build/doc
+          target-folder: docs
+          single-commit: true

.gitignore

@@ -0,0 +1,3 @@
+build/
+lake-packages/
+.lake/

Minimal/Calculus.lean

@@ -0,0 +1,102 @@
+set_option autoImplicit false
+
+@[reducible]
+def Attr := String
+
+mutual
+  inductive OptionalAttr where
+    | attached : Term → OptionalAttr
+    | void : OptionalAttr
+
+  inductive Term : Type where
+    | loc : Nat → Term
+    | dot : Term → Attr → Term
+    | app : Term → Attr → Term → Term
+    | obj : (List (Attr × OptionalAttr)) → Term
+end
+open OptionalAttr
+open Term
+
+def mapObj : (Term → Term) → (List (Attr × OptionalAttr)) → (List (Attr × OptionalAttr))
+  := λ f o =>
+  let f' := λ (attr_name, attr_body) =>
+      match attr_body with
+        | void => (attr_name, void)
+        | attached x => (attr_name, attached (f x))
+  (f' <$> o)
+
+partial def incLocatorsFrom : Nat → Term → Term
+  := λ k term => match term with
+    | loc n => if n ≥ k then loc (n+1) else loc n
+    | dot t a => dot (incLocatorsFrom k t) a
+    | app t a u => app (incLocatorsFrom k t) a (incLocatorsFrom k u)
+    | obj o => (obj (mapObj (incLocatorsFrom (k+1)) o))
+
+
+partial def incLocators : Term → Term
+  := incLocatorsFrom 0
+
+
+partial def substituteLocator : Int × Term → Term → Term
+  := λ (k, v) term => match term with
+    | obj o => obj (mapObj (substituteLocator (k + 1, incLocators v)) o)
+    | dot t a => dot (substituteLocator (k, v) t) a
+    | app t a u => app (substituteLocator (k, v) t) a (substituteLocator (k, v) u)
+    | loc n =>
+      if (n < k) then (loc n)
+      else if (n == k) then v
+      else loc (n-1)
+
+-- def checkUniqueAttributes : (List (Attr × OptionalAttr)) → Bool
+--   | _ => true
+
+def lookup : (List (Attr × OptionalAttr)) → Attr → Option OptionalAttr
+  := λ l a => match l with
+    | [] => none
+    | List.cons (name, term) tail =>
+        if (name == a) then term
+        else lookup tail a
+
+def insert : (List (Attr × OptionalAttr)) → Attr → OptionalAttr → (List (Attr × OptionalAttr))
+  := λ l a u => match l with
+    | [] => []
+    | List.cons (name, term) tail =>
+        if (name == a) then List.cons (name, u) tail
+        else List.cons (name, term) (insert tail a u)
+
+
+partial def whnf : Term → Term
+  | loc n => loc n
+  | obj o => obj o
+  | app t a u => match (whnf t) with
+    | obj o => match lookup o a with
+      | none => app (obj o) a u
+      | some (attached _) => app (obj o) a u
+      | some void => obj (insert o a (attached (incLocators u)))
+    | t' => app t' a u
+  | dot t a => match (whnf t) with
+    | obj o => match lookup o a with
+      | some (attached u) => whnf (substituteLocator (0, obj o) u)
+      | some void => dot (obj o) a
+      | none => match lookup o "φ" with
+        | some _ => dot (dot (obj o) "φ") a
+        | none => dot (obj o) a
+    | t' => dot t' a
+
+partial def nf : Term → Term
+  | loc n => loc n
+  | obj o => obj (mapObj nf o)
+  | app t a u => match (whnf t) with
+    | obj o => match lookup o a with
+      | none => app (nf (obj o)) a (nf u)
+      | some (attached _) => app (nf (obj o)) a (nf u)
+      | some void => nf (obj (insert o a (attached (incLocators u))))
+    | t' => app (nf t') a (nf u)
+  | dot t a => match (whnf t) with
+    | obj o => match lookup o a with
+      | some (attached u) => nf (substituteLocator (0, obj o) u)
+      | some void => dot (nf (obj o)) a
+      | none => match lookup o "φ" with
+        | some _ => nf (dot (dot (obj o) "φ") a)
+        | none => dot (nf (obj o)) a
+    | t' => dot (nf t') a

Minimal/Test.lean

@@ -0,0 +1,37 @@
+import Minimal.calculus
+
+set_option autoImplicit false
+
+open OptionalAttr
+open Term
+
+
+mutual
+partial def termToString : Term → String
+  | Term.loc n => s!"ρ{n}"
+  | Term.dot t s => s!"{termToString t}.{s}"
+  | Term.app t a u => s!"{termToString t}({a} ↦ {termToString u})"
+  | Term.obj o =>
+    "〚" ++ listToString o ++ "〛"
+
+partial def listToString : List (Attr × OptionalAttr) → String
+      | [] => ""
+      | [(a, t)] => s!"{a} ↦ {attrToString t}"
+      | List.cons (a, t) l => s!"{a} ↦ {attrToString t}, " ++ (listToString l)
+
+partial def attrToString : OptionalAttr → String
+  | attached x => termToString x
+  | void => "∅"
+end
+
+
+instance : ToString OptionalAttr where
+  toString := attrToString
+
+instance : ToString Term where
+  toString := termToString
+
+
+#eval whnf (app (dot (obj [("x", attached (obj [("y", void)]))]) "x") "y" (dot (obj [("z", attached (loc 3)), ("w", void)]) "z"))
+
+#eval nf (app (dot (obj [("x", attached (obj [("y", void)]))]) "x") "y" (dot (obj [("z", attached (loc 3)), ("w", void)]) "z"))

PhiCalculus.lean

@@ -0,0 +1,6 @@
+import Minimal.Calculus
+
+def main : IO Unit :=
+  IO.println "Lean 4!"
+
+#eval main

README.md

@@ -1 +1,28 @@
-Proof of 𝜑-calculus confluence.
+# Confluence for 𝜑-calculus
+
+Formalization of 𝜑-calculus variants and corresponding confluence results.
+
+## About
+
+We aim to formalize, using a computer proof assistant Lean 4,
+𝜑-calculus and the rewrite rules for normalization
+of 𝜑-programs (see <https://github.com/objectionary/normalizer>).
+We are particularly interested in the confluence of the rewrite system.
+To formalize this, we first focus on the minimal version of the calculus[^1],
+and then gradually add features to match [EO](https://github.com/objectionary/eo)[^2].
+
+## Installation
+
+If you use VS Code, get [lean4 extension](https://github.com/leanprover/vscode-lean4).
+Otherwise, install [`elan`](https://github.com/leanprover/elan), version manager for Lean.
+
+In VScode, make sure to open the root directory of the project.
+Then run the following from the Terminal:
+
+```sh
+lake build
+```
+
+[^1]: Nikolai Kudasov and Violetta Sim. 2023. _Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects._ In Proceedings of the 24th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP '22). Association for Computing Machinery, New York, NY, USA, 29–36. <https://doi.org/10.1145/3611096.3611103>
+
+[^2]: Yegor Bugayenko. 2022. _EOLANG and φ-calculus._ <https://arxiv.org/abs/2111.13384>

lake-manifest.json

@@ -0,0 +1,95 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "7d065f253ed92e9c3b45751cdfc52bc1e9507561",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.24",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "fb3fd7cd7a0004f3d9bc0daf99c3d767cf6e7600",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/xubaiw/CMark.lean",
+   "type": "git",
+   "subDir": null,
+   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+   "name": "CMark",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/hargonix/LeanInk",
+   "type": "git",
+   "subDir": null,
+   "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
+   "name": "leanInk",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "doc-gen",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "«phi-calculus»",
+ "lakeDir": ".lake"}

lakefile.lean

@@ -0,0 +1,17 @@
+import Lake
+open Lake DSL
+
+package «phi-calculus»
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+
+require std from git "https://github.com/leanprover/std4" @ "main"
+
+meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
+
+@[default_target]
+lean_lib PhiCalculus
+
+lean_lib Minimal

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.5.0-rc1