Improve pointwise LUB

francescoo22 · Jul 16, 2024 · c895191 · c895191
1 parent 9aa7bd2
commit c895191
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 56 deletions.
diff --git a/src/annotation-system/formalization.typ b/src/annotation-system/formalization.typ
@@ -140,7 +140,6 @@ If $p_1 subset.sq p_2$ holds, we say that
   Ctx-Lub-Empty, Ctx-Lub-Sym,
   Ctx-Lub-1, "",
   Ctx-Lub-2, "",
-  Ctx-Lub-3, "",
   Remove-Locals-Base, Remove-Locals-Keep,
   Remove-Locals-Discard, "",
   Unify, ""

diff --git a/src/annotation-system/rules/unification.typ b/src/annotation-system/rules/unification.typ
@@ -3,50 +3,6 @@
 
 // *********** Unify ***********
 
-// #let U-Empty = prooftree(
-//   axiom($$),
-//   rule(label: "U-Empty", $unify(Delta, dot, dot) = dot$),
-// )
-
-// #let U-Sym = prooftree(
-//   axiom($$),
-//   rule(label: "U-Sym", $unify(Delta, Delta_1, Delta_2) = unify(Delta, Delta_2, Delta_1)$),
-// )
-
-// #let U-Local = {
-//   let a1 = $root(p) = x$
-//   let a2 = $x in.not Delta$
-//   let a3 = $unify(Delta, Delta_1, Delta_2) = Delta'$
-//   prooftree(
-//     stacked-axiom(
-//       (a1, a2),
-//       (a3, ),
-//     ),
-//     rule(label: "U-Local", $unify(Delta, (p: alpha beta, Delta_1), Delta_2) = Delta'$),
-//   )
-// }
-
-// #let U-Rec = {
-//   let a1 = $root(p) = x$
-//   let a2 = $x in Delta$
-//   let a3 = $Delta_1 without p = Delta'_1$
-//   let a4 = $Delta_2 without p = Delta'_2$
-//   let a5 = $Delta_1(p) = alpha_1 beta_1$
-//   let a6 = $Delta_2(p) = alpha_2 beta_2$
-//   let a7 = $Lub{alpha_1 beta_1, alpha_2 beta_2} = alpha' beta'$
-//   let a8 = $unify(Delta, Delta'_1, Delta'_2) = Delta'$
-//   prooftree(
-//     stacked-axiom(
-//       (a1, a2),
-//       (a3, a4),
-//       (a5, a6),
-//       (a7, a8)
-//     ),
-//     rule(label: "U-Rec", $unify(Delta, (p: alpha beta, Delta'_1), Delta'_2) = p: alpha' beta', Delta'$),
-//   )
-// }
-
-
 #let Ctx-Lub-Empty = prooftree(
   axiom($$),
   rule(label: "Ctx-Lub-Empty", $dot space lub space dot space = space dot$),
@@ -58,11 +14,11 @@
 )
 
 #let Ctx-Lub-1 = prooftree(
-  axiom($Delta_2 inangle(p.f) = alpha'' beta''$),
-  axiom($Delta_2 without p.f = Delta'_2$),
+  axiom($Delta_2 inangle(p) = alpha'' beta''$),
+  axiom($Delta_2 without p = Delta'_2$),
   axiom($Delta_1 lub Delta'_2 = Delta'$),
   axiom($Lub{alpha beta, alpha'' beta''} = alpha' beta'$),
-  rule(n:4, label: "Ctx-Lub-1", $(p.f : alpha beta, Delta_1) lub Delta_2 = p.f : alpha' beta', Delta'$),
+  rule(n:4, label: "Ctx-Lub-1", $(p : alpha beta, Delta_1) lub Delta_2 = p : alpha' beta', Delta'$),
 )
 
 #let Ctx-Lub-2 = prooftree(
@@ -71,14 +27,6 @@
   rule(n:2, label: "Ctx-Lub-2", $(x : alpha beta, Delta_1) lub Delta_2 = x : top, Delta'$),
 )
 
-#let Ctx-Lub-3 = prooftree(
-  axiom($Delta_2 inangle(x) = alpha'' beta''$),
-  axiom($Delta_2 without x = Delta'_2$),
-  axiom($Delta_1 lub Delta'_2 = Delta'$),
-  axiom($Lub{alpha beta, alpha'' beta''} = alpha' beta'$),
-  rule(n:4, label: "Ctx-Lub-3", $(x : alpha beta, Delta_1) lub Delta_2 = x : alpha' beta', Delta'$),
-)
-
 #let Remove-Locals-Base = prooftree(
   axiom($$),
   rule(label: "Remove-Locals-Base", $dot triangle.filled.small.l Delta = dot$),