Smt rw tac: Added the import to Smt.Reconstruction.Certifying

[mhk119]

No description provided.

[tomaz1502]

This is looking good! Two comments about the last commit (please make a PR before pushing to main, so its easier to review):

• It's not necessary to do replaceMainGoal [mv] at the end of evalSMTRw. The goal is already closed when you do mv'.refl
• The variable m inside both for-loops in smtRw does not need to be mutable

[tomaz1502]

Also, in smtRw you could iterate through arrays instead of indices to avoid unsafe operations, like:

  for innerArr in arr do
    let m := innerArr.size
    if m > 1 then
      for j in [: m-1] do
        let r ← mv'.rewrite (← mv'.getType) (mkAppN assoc #[innerArr[m-j-2]!]) true
        mv' ← mv'.replaceTargetEq r.eNew r.eqProof

You could also iterate through the Exprs in innerArr.reverse instead of the indices.
It looks like you are always skipping the last element of each array? if j = 0 then m - j - 2 = m - 2, whereas the last element is at position m - 1

[mhk119]

This is looking good! Two comments about the last commit (please make a PR before pushing to main, so its easier to review):

• It's not necessary to do replaceMainGoal [mv] at the end of evalSMTRw. The goal is already closed when you do mv'.refl
• The variable m inside both for-loops in smtRw does not need to be mutable

Oh thanks. This is nicer.

[mhk119]

Also, in smtRw you could iterate through arrays instead of indices to avoid unsafe operations, like:

  for innerArr in arr do
    let m := innerArr.size
    if m > 1 then
      for j in [: m-1] do
        let r ← mv'.rewrite (← mv'.getType) (mkAppN assoc #[innerArr[m-j-2]!]) true
        mv' ← mv'.replaceTargetEq r.eNew r.eqProof

You could also iterate through the Exprs in innerArr.reverse instead of the indices. It looks like you are always skipping the last element of each array? if j = 0 then m - j - 2 = m - 2, whereas the last element is at position m - 1

Yes. I am skipping the last element deliberately. This is also why I iterated over indices instead. I can try iterating through arrays though.

[tomaz1502]

This is no big deal, but I believe it would be better if opsAssocNull returned
a pair with the two Expr instead of an Array, unless you're planning to extend
this function to return more constants in the future. Then you can do
let (assoc, null) := opsAssocNull op at smtRw.
(sorry I forgot to publish the comment before)

[mhk119]

Yes, I plan to add more operators.