Inverse rewrite rules

imbrem · Jun 22, 2024 · 8a2092d · 8a2092d
1 parent 716f3d0
commit 8a2092d
Show file tree

Hide file tree

Showing 2 changed files with 211 additions and 2 deletions.
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean b/DeBruijnSSA/BinSyntax/Syntax/Compose/Region.lean
@@ -418,6 +418,24 @@ def associator_inv : Region φ :=
   let2 (Term.var 1) $
   ret (Term.pair (Term.pair (Term.var 2) (Term.var 0)) (Term.var 1))
 
+theorem associator_append_associator_inv_def
+  : @associator φ ++ associator_inv = (let2 (Term.var 0) $
+    let2 (Term.var 0) $
+    let2 (Term.pair (Term.var 0) (Term.pair (Term.var 1) (Term.var 2))) $
+    let2 (Term.var 1) $
+    ret (Term.pair (Term.pair (Term.var 2) (Term.var 0)) (Term.var 1)))
+  := rfl
+
+def RWD.assocatior_append_associator_inv {Γ : ℕ → ε}
+  : RWD (PStepD Γ) (@associator φ ++ associator_inv) nil
+  := by
+  rw [associator_append_associator_inv_def]
+  sorry
+
+def RWD.associator_inv_append_associator {Γ : ℕ → ε}
+  : RWD (PStepD Γ) (@associator_inv φ ++ associator) nil
+  := sorry
+
 def proj_left : Region φ :=
   let2 (Term.var 0) $
   ret (Term.var 0)