Add examples and tests (#56)

* Add a simple example

* Add examples of different reductions for the term presented after Definition 3.1

* Add tests for the infinite rewrite sequence

---------

Co-authored-by: eyihluyc <[email protected]>

Minimal/Examples.lean

@@ -4,6 +4,16 @@ 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]
+-/
+
 -- TEST 1: ⟦ x ↦ ξ.y, y ↦ ⟦ ⟧ ⟧.x ⇝* ⟦ ⟧
 
 -- bindings: x ↦ ξ.y, y ↦ ⟦ ⟧
@@ -515,3 +525,172 @@ def test5 : example5 ⇝* example5_res :=
   ReflTransGen.head
     test5_red
     ReflTransGen.refl
+
+---------------------------------
+-- TEST 6: infinite reduction sequence presented after Definition 3.1 [KS22]
+-- ⟦ x ↦ ρ⁰.y, y ↦ ρ⁰.x ⟧.x ⇝ ⟦ x ↦ ρ⁰.y, y ↦ ρ⁰.x ⟧.y
+-- ⟦ x ↦ ρ⁰.y, y ↦ ρ⁰.x ⟧.y ⇝ ⟦ x ↦ ρ⁰.y, y ↦ ρ⁰.x ⟧.x
+
+def example6_bindings : Bindings ["x", "y"] :=
+  .cons "x" (by simp) (attached (dot (loc 0) "y"))
+  (.cons "y" (by simp) (attached (dot (loc 0) "x")) .nil)
+
+def example6_obj : Term := obj example6_bindings
+
+def test6_1 : (dot example6_obj "x" ⇝ dot example6_obj "y") := by
+  have reduction :=
+    dot_c
+      (dot (loc 0) "y")
+      "x"
+      example6_bindings
+      rfl
+      (by simp [lookup])
+  simp [substitute] at reduction
+  exact reduction
+
+def test6_2 : (dot example6_obj "y" ⇝ dot example6_obj "x") := by
+  have reduction :=
+    dot_c
+      (dot (loc 0) "x")
+      "y"
+      example6_bindings
+      rfl
+      (by simp [lookup])
+  simp [substitute] at reduction
+  exact reduction
+
+---------------------------------
+-- 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