Real polynorm (#157)

* Implement Real polynorm. * Explicit casts.
ufmg-smite · Dec 17, 2024 · 9ad1c39 · 9ad1c39
1 parent ed0b650
commit 9ad1c39
Show file tree

Hide file tree

Showing 4 changed files with 397 additions and 36 deletions.
diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean
@@ -413,7 +413,7 @@ where
     if !pf.getResult[0]!.getSort.isInteger then return none
     let a : Q(Int) ← reconstructTerm pf.getResult[0]!
     let b : Q(Int) ← reconstructTerm pf.getResult[1]!
-    addTac q($a = $b) Int.nativePolyNorm
+    addTac q($a = $b) Int.polyNorm
   | .ARITH_POLY_NORM_REL =>
     if !pf.getChildren[0]!.getResult[0]![0]!.getSort.isInteger then return none
     reconstructArithPolyNormRel pf

diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean
@@ -413,7 +413,7 @@ where
     if pf.getResult[0]!.getSort.isInteger then return none
     let a : Q(Rat) ← reconstructTerm pf.getResult[0]!
     let b : Q(Rat) ← reconstructTerm pf.getResult[1]!
-    addTac q($a = $b) Rat.nativePolyNorm
+    addTac q($a = $b) Rat.polyNorm
   | .ARITH_POLY_NORM_REL =>
     if pf.getChildren[0]!.getResult[0]![0]!.getSort.isInteger then return none
     reconstructArithPolyNormRel pf

diff --git a/Smt/Reconstruct/Rat/Polynorm.lean b/Smt/Reconstruct/Rat/Polynorm.lean
@@ -400,7 +400,7 @@ end Smt.Reconstruct.Rat.Tactic
 example (x y z : Rat) : 1 * (x + y) * z / 4 = 1 / (2 * 2) * (z * y + x * z) := by
   poly_norm
 
-example (x y : Int) (z : Rat) : 1 * (x + y) * z / 4 = 1 / (2 * 2) * (z * y + x * z) := by
+example (x y : Int) (z : Rat) : 1 * (↑x + ↑y) * z / 4 = 1 / (2 * 2) * (z * ↑y + ↑x * z) := by
   poly_norm
 
 example (x y : Int) (z : Rat) : 1 * ↑(x + y) * z / 4 = 1 / (2 * 2) * (z * ↑y + ↑x * z) := by