Sync with cvc5 main and latest Lean version.

Smt/Reconstruct.lean

@@ -120,7 +120,7 @@ def incCount : ReconstructM Nat :=
 def withAssums (as : Array Expr) (k : ReconstructM α) : ReconstructM α := do
   modify fun state => { state with currAssums := state.currAssums ++ as }
   let r ← k
-  modify fun state => { state with currAssums := state.currAssums.shrink (state.currAssums.size - as.size) }
+  modify fun state => { state with currAssums := state.currAssums.take (state.currAssums.size - as.size) }
   return r
 
 def findAssumWithType? (t : Expr) : ReconstructM (Option Expr) := do

Smt/Reconstruct/Int.lean

@@ -296,10 +296,10 @@ def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     Meta.mkLambdaFVars hs h
   addThm q(andN $ps → $q) q(Builtin.scopes $h)
 where
-  go vs ts hs map ka (a : Q(Int)) (ha : Expr) i : ReconstructM Expr := do
+  go vs ts hs map (ka : cvc5.Kind) (a : Q(Int)) (ha : Expr) i : ReconstructM Expr := do
     if hi : i < vs.size then
       let b : Q(Int) ← reconstructTerm vs[i]
-      let k := ts[map[vs[i]]!]!.getKind
+      let k : cvc5.Kind := ts[map[vs[i]]!]!.getKind
       if ka == .LT && k == .LT then
         let ha : Q($a < 0) := ha
         let hb : Q($b < 0) := hs[map[vs[i]]!]!

Smt/Reconstruct/Prop.lean

@@ -83,27 +83,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .BOOL_OR_TRUE =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_true) args)
-  | .BOOL_OR_FALSE =>
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_false) args)
   | .BOOL_OR_FLATTEN =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_flatten) args)
-  | .BOOL_OR_DUP =>
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_dup) args)
-  | .BOOL_AND_TRUE =>
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_true) args)
   | .BOOL_AND_FALSE =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_false) args)
   | .BOOL_AND_FLATTEN =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_flatten) args)
-  | .BOOL_AND_DUP =>
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_dup) args)
   | .BOOL_AND_CONF =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_conf) args)
@@ -126,6 +114,9 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .BOOL_AND_DE_MORGAN =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_de_morgan) args)
+  | .BOOL_OR_AND_DISTRIB =>
+    let args ← reconstructArgs pf.getArguments[1:]
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_and_distrib) args)
   | .BOOL_XOR_REFL =>
     let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     addThm q(XOr $p $p = False) q(@Prop.bool_xor_refl $p)
@@ -150,10 +141,14 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
     addThm q((¬XOr $p $q) = ($p = $q)) q(@Prop.bool_not_xor_elim $p $q)
-  | .BOOL_NOT_EQ_ELIM =>
+  | .BOOL_NOT_EQ_ELIM1 =>
     let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
-    addThm q((¬$p = $q) = ((¬$p) = $q)) q(@Prop.bool_not_eq_elim $p $q)
+    addThm q((¬$p = $q) = ((¬$p) = $q)) q(@Prop.bool_not_eq_elim1 $p $q)
+  | .BOOL_NOT_EQ_ELIM2 =>
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    addThm q((¬$p = $q) = ($p = (¬$q))) q(@Prop.bool_not_eq_elim2 $p $q)
   | .ITE_NEG_BRANCH =>
     let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
@@ -201,6 +196,12 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
     let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
     addThm q(ite $c $p (¬$c) = ite $c $p True) q(@Prop.ite_else_lookahead_not_self $c $p $h)
+  | .ITE_EXPAND =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let q : Q(Prop) ← reconstructTerm pf.getArguments[3]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $p $q = ((¬$c ∨ $p) ∧ ($c ∨ $q))) q(@Prop.ite_expand $c $p $q $h)
   | .BOOL_NOT_ITE_ELIM =>
     let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
@@ -356,8 +357,8 @@ def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : Rec
     addThm (← reconstructTerm pf.getResult) q(@Prop.and_elim _ $hps $i $hi)
   | .AND_INTRO =>
     let cpfs := pf.getChildren
-    let q : Q(Prop) ← reconstructTerm cpfs.back.getResult
-    let hq : Q($q) ← reconstructProof cpfs.back
+    let q : Q(Prop) ← reconstructTerm cpfs.back!.getResult
+    let hq : Q($q) ← reconstructProof cpfs.back!
     let f := fun pf ⟨q, hq⟩ => do
       let p : Q(Prop) ← reconstructTerm pf.getResult
       let hp : Q($p) ← reconstructProof pf

Smt/Reconstruct/Prop/Rewrites.lean

@@ -38,23 +38,13 @@ theorem bool_impl_elim : (t → s) = (¬t ∨ s) :=
 
 theorem bool_or_true : (xs ∨ True ∨ ys) = True :=
   (true_or _).symm ▸ or_true _
-theorem bool_or_false : (xs ∨ False ∨ ys) = (xs ∨ ys) :=
-  (false_or _).symm ▸ rfl
 theorem bool_or_flatten : (xs ∨ (b ∨ ys) ∨ zs) = (xs ∨ b ∨ ys ∨ zs) :=
   propext (@or_assoc b ys zs) ▸ rfl
-theorem bool_or_dup : (xs ∨ b ∨ ys ∨ b ∨ zs) = (xs ∨ b ∨ ys ∨ zs) :=
-  propext (@or_assoc ys b zs) ▸ propext (@Or.comm ys b) ▸ propext (@or_assoc b _ zs) ▸
-  propext (@or_assoc b b ys) ▸ or_self _ ▸ propext (@or_assoc b ys zs) ▸ rfl
 
-theorem bool_and_true : (xs ∧ True ∧ ys) = (xs ∧ ys) :=
-  (true_and _).symm ▸ rfl
 theorem bool_and_false : (xs ∧ False ∧ ys) = False :=
   (false_and _).symm ▸ and_false _
 theorem bool_and_flatten : (xs ∧ (b ∧ ys) ∧ zs) = (xs ∧ b ∧ ys ∧ zs) :=
   propext (@and_assoc b ys zs) ▸ rfl
-theorem bool_and_dup : (xs ∧ b ∧ ys ∧ b ∧ zs) = (xs ∧ b ∧ ys ∧ zs) :=
-  propext (@and_assoc ys b zs) ▸ propext (@And.comm ys b) ▸ propext (@and_assoc b _ zs) ▸
-  propext (@and_assoc b b ys) ▸ and_self _ ▸ propext (@and_assoc b ys zs) ▸ rfl
 
 theorem bool_and_conf : (xs ∧ w ∧ ys ∧ ¬w ∧ zs) = False :=
   propext ⟨fun ⟨_, hw, _, hnw, _⟩ => absurd hw hnw, False.elim⟩
@@ -74,6 +64,9 @@ theorem bool_implies_de_morgan : (¬(x → y)) = (x ∧ ¬y) :=
 theorem bool_and_de_morgan : (¬(x ∧ y ∧ zs)) = (¬x ∨ ¬(y ∧ zs)) :=
   propext Classical.not_and_iff_or_not_not
 
+theorem bool_or_and_distrib : (y₁ ∧ y₂ ∧ ys ∨ zs) = ((y₁ ∨ zs) ∧ (y₂ ∧ ys ∨ zs)) :=
+  propext and_or_right ▸ rfl
+
 theorem bool_xor_refl : XOr x x = False :=
   propext ⟨(·.elim absurd (flip absurd)), False.elim⟩
 theorem bool_xor_nrefl : (XOr x ¬x) = True :=
@@ -97,13 +90,20 @@ theorem bool_not_xor_elim : (¬XOr x y) = (x = y) :=
        (fun hy => Classical.byContradiction (hnxy $ XOr.inr · hy))))
     fun hxy => hxy ▸ fun hxx => hxx.elim (fun hx hnx => hnx hx) (· ·))
 
-theorem bool_not_eq_elim : (¬x = y) = ((¬x) = y) :=
+theorem bool_not_eq_elim1 : (¬x = y) = ((¬x) = y) :=
   propext
     (Iff.intro (bool_not_xor_elim ▸ fun hnnxy => (Classical.not_not.mp hnnxy).elim
       (fun hx hny => propext ⟨(absurd hx ·), (absurd · hny)⟩)
       (fun hnx hy => propext ⟨const _ hy, const _ hnx⟩))
     (@iff_not_self x $ · ▸ · ▸ Iff.rfl))
 
+theorem bool_not_eq_elim2 : (¬x = y) = (x = ¬y) :=
+  propext
+    (Iff.intro (bool_not_xor_elim ▸ fun hnnxy => (Classical.not_not.mp hnnxy).elim
+      (fun hx hny => propext ⟨const _ hny, const _ hx⟩)
+      (fun hnx hy => propext ⟨(absurd · hnx), (absurd hy ·)⟩))
+    (@iff_not_self y $ · ▸ · ▸ Iff.rfl))
+
 theorem ite_neg_branch [h : Decidable c] : x = ¬y → ite c x y = (c = x) :=
   fun hxny => hxny ▸ h.byCases
     (fun hc => if_pos hc ▸ propext ⟨(propext ⟨const _ ·, const _ hc⟩), (· ▸ hc)⟩)
@@ -138,6 +138,10 @@ theorem ite_else_lookahead_not_self [h : Decidable c] : ite c x (¬c) = ite c x
   (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
   (fun hnc => if_neg hnc ▸ if_neg hnc ▸ eq_true hnc)
 
+theorem ite_expand [h : Decidable c] : ite c x y = ((¬c ∨ x) ∧ (c ∨ y)) := h.byCases
+  (fun hc => if_pos hc ▸ propext ⟨(⟨Or.inr ·, Or.inl hc⟩), (·.left.resolve_left (not_not_intro hc))⟩)
+  (fun hnc => if_neg hnc ▸ propext ⟨(⟨Or.inl hnc, Or.inr ·⟩), (·.right.resolve_left hnc)⟩)
+
 theorem bool_not_ite_elim [h : Decidable c] : (¬ite c x y) = ite c (¬x) (¬y) := h.byCases
   (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
   (fun hnc => if_neg hnc ▸ if_neg hnc ▸ rfl)

Smt/Reconstruct/Quant.lean

@@ -141,7 +141,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let t  : Q($α) ← reconstructTerm pf.getResult[0]!
     let t' : Q($α) ← reconstructTerm pf.getResult[1]!
     addThm q($t = $t') q(Eq.refl $t)
-  | .QUANT_MINISCOPE =>
+  | .QUANT_MINISCOPE_AND =>
     let mut xs := #[]
     for x in pf.getResult[0]![0]! do
       xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
@@ -166,7 +166,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
         return (ap, aps, q(Eq.trans (forall_congr $hx) (@miniscope_andN $α $lps)))
       xs.foldrM f (b, ps, h)
     addThm (← reconstructTerm pf.getResult) h
-  | .QUANT_MINISCOPE_FV =>
+  | .QUANT_MINISCOPE_OR =>
     let mut xs := #[]
     for x in pf.getResult[0]![0]! do
       xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
@@ -198,6 +198,29 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
         return (p, ps.dropLast, ps.getLastD q(False), q :: rs, h)
       xss.foldrM fout (b, ps.dropLast, ps.getLast!, [], h)
     addThm (← reconstructTerm pf.getResult) h
+  | .QUANT_MINISCOPE_ITE =>
+    let mut xs := #[]
+    for x in pf.getResult[0]![0]! do
+      xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
+    let (_, _, _, h) ← Meta.withLocalDeclsD xs fun xs => withNewTermCache do
+      let c : Q(Prop) ← reconstructTerm pf.getResult[0]![1]![0]!
+      let p : Q(Prop) ← reconstructTerm pf.getResult[0]![1]![1]!
+      let q : Q(Prop) ← reconstructTerm pf.getResult[0]![1]![2]!
+      let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+      let h : Q((ite $c $p $q) = (ite $c $p $q)) := q(Eq.refl (ite $c $p $q))
+      let f := fun x (p, q, r, h) => do
+        let u ← Meta.getLevel (← Meta.inferType x)
+        let α : Q(Sort u) ← Meta.inferType x
+        let lp : Q($α → Prop) ← Meta.mkLambdaFVars #[x] p
+        let lq : Q($α → Prop) ← Meta.mkLambdaFVars #[x] q
+        let lr : Q($α → Prop) ← Meta.mkLambdaFVars #[x] r
+        let hx : Q(∀ x, $lr x = ite $c ($lp x) ($lq x)) ← Meta.mkLambdaFVars #[x] h
+        let ap ← Meta.mkForallFVars #[x] p
+        let aq ← Meta.mkForallFVars #[x] q
+        let ar ← Meta.mkForallFVars #[x] r
+        return (ap, aq, ar, q(Eq.trans (forall_congr $hx) (@miniscope_ite $α $c $hc $lp $lq)))
+      xs.foldrM f (p, q, q(ite $c $p $q), h)
+    addThm (← reconstructTerm pf.getResult) h
   | .QUANT_VAR_ELIM_EQ =>
     let lb := pf.getResult[0]![1]!
     if lb.getKind == .OR then

Smt/Reconstruct/Quant/Lemmas.lean

@@ -68,6 +68,12 @@ theorem miniscope_orN {ps : List Prop} {q : α → Prop} {rs : List Prop} :
   | [p]            => miniscope_or_right ▸ @miniscope_orN α [] q rs ▸ rfl
   | p₁ :: p₂ :: ps => miniscope_or_right ▸ @miniscope_orN α (p₂ :: ps) q rs ▸ rfl
 
+theorem miniscope_ite {c : Prop} [h : Decidable c] {p q : α → Prop} :
+  (∀ x, ite c (p x) (q x)) = ite c (∀ x, p x) (∀ x, q x) :=
+  h.byCases
+    (fun hc => if_pos hc ▸ propext ⟨((if_pos hc).mp $ · ·), (if_pos hc ▸ · ·)⟩)
+    (fun hnc => if_neg hnc ▸ propext ⟨((if_neg hnc).mp $ · ·), (if_neg hnc ▸ · ·)⟩)
+
 theorem var_elim_eq {t : α} : (∀ x, x ≠ t) = False :=
   propext ⟨fun hnxt => absurd rfl (hnxt t), False.elim⟩
 

Smt/Reconstruct/Rat.lean

@@ -103,10 +103,6 @@ where
 
 def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   match pf.getRewriteRule with
-  | .ARITH_DIV_BY_CONST_ELIM =>
-    let t : Q(Rat) ← reconstructTerm pf.getResult[0]![0]!
-    let c : Q(Rat) ← reconstructTerm pf.getResult[0]![1]!
-    addThm q($t / $c = $t * (1 / $c)) q(@Rewrite.div_by_const_elim $t $c)
   | .ARITH_POW_ELIM =>
     if pf.getResult[0]![0]!.getSort.isInteger then return none
     let x : Q(Rat) ← reconstructTerm pf.getResult[0]![0]!
@@ -281,10 +277,10 @@ def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     Meta.mkLambdaFVars hs h
   addThm q(andN $ps → $q) q(Builtin.scopes $h)
 where
-  go vs ts hs map ka (a : Q(Rat)) (ha : Expr) i : ReconstructM Expr := do
+  go vs ts hs map (ka : cvc5.Kind) (a : Q(Rat)) (ha : Expr) i : ReconstructM Expr := do
     if hi : i < vs.size then
       let b : Q(Rat) ← reconstructTerm vs[i]
-      let k := ts[map[vs[i]]!]!.getKind
+      let k : cvc5.Kind := ts[map[vs[i]]!]!.getKind
       if ka == .LT && k == .LT then
         let ha : Q($a < 0) := ha
         let hb : Q($b < 0) := hs[map[vs[i]]!]!

Smt/Reconstruct/Rat/Polynorm.lean

@@ -188,20 +188,20 @@ deriving Inhabited, Repr
 namespace IntExpr
 
 def toPolynomial : IntExpr → Polynomial
-  | val v => if v = 0 then [] else [{ coeff := v, vars := [] }]
-  | var v => [{ coeff := 1, vars := [⟨false, v⟩] }]
-  | neg a => a.toPolynomial.neg
-  | add a b => Polynomial.add a.toPolynomial b.toPolynomial
-  | sub a b => Polynomial.sub a.toPolynomial b.toPolynomial
-  | mul a b => Polynomial.mul a.toPolynomial b.toPolynomial
+  | .val v => if v = 0 then [] else [{ coeff := v, vars := [] }]
+  | .var v => [{ coeff := 1, vars := [⟨false, v⟩] }]
+  | .neg a => a.toPolynomial.neg
+  | .add a b => Polynomial.add a.toPolynomial b.toPolynomial
+  | .sub a b => Polynomial.sub a.toPolynomial b.toPolynomial
+  | .mul a b => Polynomial.mul a.toPolynomial b.toPolynomial
 
 def denote (ctx : IntContext) : IntExpr → Int
-  | val v => v
-  | var v => ctx v
-  | neg a => -a.denote ctx
-  | add a b => a.denote ctx + b.denote ctx
-  | sub a b => a.denote ctx - b.denote ctx
-  | mul a b => a.denote ctx * b.denote ctx
+  | .val v => v
+  | .var v => ctx v
+  | .neg a => -a.denote ctx
+  | .add a b => a.denote ctx + b.denote ctx
+  | .sub a b => a.denote ctx - b.denote ctx
+  | .mul a b => a.denote ctx * b.denote ctx
 
 theorem denote_toPolynomial {rctx : RatContext} {e : IntExpr} : e.denote ictx = e.toPolynomial.denote (fun ⟨b, n⟩ => if b then rctx n else ictx n) := by
   induction e with
@@ -237,24 +237,24 @@ deriving Inhabited, Repr
 namespace RatExpr
 
 def toPolynomial : RatExpr → Polynomial
-  | val v => if v = 0 then [] else [{ coeff := v, vars := [] }]
-  | var v => [{ coeff := 1, vars := [⟨true, v⟩] }]
-  | neg a => a.toPolynomial.neg
-  | add a b => Polynomial.add a.toPolynomial b.toPolynomial
-  | sub a b => Polynomial.sub a.toPolynomial b.toPolynomial
-  | mul a b => Polynomial.mul a.toPolynomial b.toPolynomial
-  | divConst a c => Polynomial.divConst a.toPolynomial c
-  | cast a => a.toPolynomial
+  | .val v => if v = 0 then [] else [{ coeff := v, vars := [] }]
+  | .var v => [{ coeff := 1, vars := [⟨true, v⟩] }]
+  | .neg a => a.toPolynomial.neg
+  | .add a b => Polynomial.add a.toPolynomial b.toPolynomial
+  | .sub a b => Polynomial.sub a.toPolynomial b.toPolynomial
+  | .mul a b => Polynomial.mul a.toPolynomial b.toPolynomial
+  | .divConst a c => Polynomial.divConst a.toPolynomial c
+  | .cast a => a.toPolynomial
 
 def denote (ictx : IntContext) (rctx : RatContext)  : RatExpr → Rat
-  | val v => v
-  | var v => rctx v
-  | neg a => -a.denote ictx rctx
-  | add a b => a.denote ictx rctx + b.denote ictx rctx
-  | sub a b => a.denote ictx rctx - b.denote ictx rctx
-  | mul a b => a.denote ictx rctx * b.denote ictx rctx
-  | divConst a c => a.denote ictx rctx / c
-  | cast a => a.denote ictx
+  | .val v => v
+  | .var v => rctx v
+  | .neg a => -a.denote ictx rctx
+  | .add a b => a.denote ictx rctx + b.denote ictx rctx
+  | .sub a b => a.denote ictx rctx - b.denote ictx rctx
+  | .mul a b => a.denote ictx rctx * b.denote ictx rctx
+  | .divConst a c => a.denote ictx rctx / c
+  | .cast a => a.denote ictx
 
 theorem denote_toPolynomial {e : RatExpr} : e.denote ictx rctx = e.toPolynomial.denote (fun ⟨b, n⟩ => if b then rctx n else ictx n) := by
   induction e with
@@ -297,7 +297,7 @@ def getRatIndex (e : Q(Rat)) : PolyM Nat := do
     set (is, rs.push e)
     return size
 
-def getIntIndex (e : Q(Rat)) : PolyM Nat := do
+def getIntIndex (e : Q(Int)) : PolyM Nat := do
   let ⟨is, rs⟩ ← get
   if let some i := is.findIdx? (· == e) then
     return i
@@ -397,12 +397,10 @@ open Lean.Elab Tactic in
 
 end Smt.Reconstruct.Rat.Tactic
 
-open Smt.Reconstruct.Rat.PolyNorm.RatExpr
-
-example (x y z : Rat) : 1 * (x + y) * z / 4  = 1/(2 * 2) * (z * y + x * z) := by
+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

Smt/Reconstruct/Rat/Rewrites.lean

@@ -11,9 +11,6 @@ namespace Smt.Reconstruct.Rat.Rewrite
 
 open Function
 
-theorem div_by_const_elim {t c : Rat} : t / c = t * (1 / c) :=
-  sorry
-
 -- https://github.com/cvc5/cvc5/blob/main/src/theory/arith/rewrites
 
 variable {t ts x xs : Rat}