From 6ba92b5e4d17874c5d6a1cf919057a50a68cafa0 Mon Sep 17 00:00:00 2001
From: Anatolay <nihonvasserman228@gmail.com>
Date: Fri, 6 Dec 2024 23:48:23 +0300
Subject: [PATCH] Add examples of different reductions for the term presented
 after Definition 3.1

---
 Minimal/Examples.lean | 146 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 146 insertions(+)

diff --git a/Minimal/Examples.lean b/Minimal/Examples.lean
index 62c282e9..b7a1aae4 100644
--- a/Minimal/Examples.lean
+++ b/Minimal/Examples.lean
@@ -4,6 +4,17 @@ open Term
 open OptionalAttr
 open Reduce
 
+/-!
+# Confluence of minimal φ-calculus
+
+This file contains examples of minimal φ-calculus terms and their reductions.
+
+## References
+
+* [Nikolai Kudasov and Violetta Sim. 2023. Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects.][KS22]
+-/
+
+
 -- ⟦ a ↦ ⟦ ⟧ ⟧.a
 def example1 : Term :=
   dot
@@ -36,3 +47,138 @@ def test1_red1 : example1 ⇝ example1' := by
 def test1 : example1 ⇝* example1' := ReflTransGen.head
   test1_red1
   ReflTransGen.refl
+
+/-- Examples/tests of different term reductions presented after Definition 3.1 [KS22]
+⟦x ↦ ⟦y ↦ ∅⟧⟧.x(y ↦ ⟦z ↦ w⟧.z)
+-/
+def w : Term := obj Bindings.nil
+def example_graph_init : Term :=
+  app
+    (dot
+      (obj
+        (.cons "x" (by simp) (attached (obj (.cons "y" (by simp) void .nil))) .nil)
+      )
+      "x"
+    )
+    "y"
+    (dot (obj (.cons "z" (by simp) (attached w) .nil)) "z")
+
+def example_graph_l1 : Term :=
+  app
+    (obj (.cons "y" (by simp) void .nil))
+    "y"
+    (dot (obj (.cons "z" (by simp) (attached w) .nil)) "z")
+def example_graph_r1 : Term :=
+  app
+    (dot
+      (obj
+        (.cons "x" (by simp) (attached (obj (.cons "y" (by simp) void .nil))) .nil)
+      )
+      "x"
+    )
+    "y"
+    w
+def example_graph_l2 : Term :=
+  obj
+    (.cons "y" (by simp)
+      (attached (dot (obj (.cons "z" (by simp) (attached w) .nil)) "z")) .nil
+    )
+def example_graph_r2 : Term :=
+  app
+    (obj (.cons "y" (by simp) void .nil))
+    "y"
+    w
+def example_graph_last : Term :=
+  obj (.cons "y" (by simp) (attached w) .nil)
+
+def test_graph_1 : example_graph_init ⇝ example_graph_l1
+  := congAPPₗ _ _ _ _
+    (by
+      have reduction := dot_c
+        (obj (.cons "y" (by simp) void .nil))
+        "x"
+        (.cons "x" (by simp) (attached (obj (.cons "y" (by simp) void .nil))) .nil)
+        rfl
+        (by simp [lookup])
+      simp [substitute] at reduction
+      exact reduction
+    )
+def test_graph_2 : example_graph_init ⇝ example_graph_r1
+  := congAPPᵣ _ _ _ _
+    (by
+      have reduction := dot_c
+        w
+        "z"
+        (.cons "z" (by simp) (attached w) .nil)
+        rfl
+        (by simp [lookup])
+      simp [substitute] at reduction
+      exact reduction
+    )
+def test_graph_3 : example_graph_l1 ⇝ example_graph_l2
+  := by
+    have reduction := app_c
+      (obj (.cons "y" (by simp) void .nil))
+      (dot (obj (.cons "z" (by simp) (attached w) .nil)) "z")
+      "y"
+      (.cons "y" (by simp) void .nil)
+      rfl
+      (by simp [lookup])
+    simp [insert_φ] at reduction
+    exact reduction
+def test_graph_4 : example_graph_l1 ⇝ example_graph_r2
+  := congAPPᵣ _ _ _ _
+    (by
+      have reduction := dot_c
+        w
+        "z"
+        (.cons "z" (by simp) (attached w) .nil)
+        rfl
+        (by simp [lookup])
+      simp [substitute] at reduction
+      exact reduction
+    )
+def test_graph_5 : example_graph_r1 ⇝ example_graph_r2
+  := congAPPₗ _ _ _ _
+    (by
+      have reduction := dot_c
+        (obj (.cons "y" (by simp) void .nil))
+        "x"
+        (.cons "x" (by simp) (attached (obj (.cons "y" (by simp) void .nil))) .nil)
+        rfl
+        (by simp [lookup])
+      simp [substitute] at reduction
+      exact reduction
+    )
+def test_graph_6 : example_graph_l2 ⇝ example_graph_last
+  := by
+    have reduction := congOBJ
+      "y"
+      (.cons "y" (by simp)
+        (attached (dot (obj (.cons "z" (by simp) (attached w) .nil)) "z"))
+        .nil
+      )
+      (by
+        have reduction := dot_c
+          w
+          "z"
+          (.cons "z" (by simp) (attached w) .nil)
+          rfl
+          (by simp [lookup])
+        simp [substitute] at reduction
+        exact reduction
+      )
+      (.zeroth_attached _ _ _ _)
+    simp [insert_φ] at reduction
+    exact reduction
+def test_graph_7 : example_graph_r2 ⇝ example_graph_last
+  := by
+    have reduction := app_c
+      (obj (.cons "y" (by simp) void .nil))
+      w
+      "y"
+      (.cons "y" (by simp) void .nil)
+      rfl
+      (by simp [lookup])
+    simp [insert_φ] at reduction
+    exact reduction