Duper on v4.4.0-rc1

Stream: general

[Utensil Song]

Anyone successfully added Duper to an existing project? The demo project and the live editor are on v4.3.0-rc1 and my v4.4.0-rc1 project added Duper by

require «Duper» from git "https://github.com/leanprover-community/duper.git" @ "v0.0.4"

then import Duper gives error

Error output

error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/auto/.lake/build/lib:./.lake/packages/Duper/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/packages/auto/.lake/build/lib:./.lake/packages/Duper/.lake/build/lib:./.lake/build/lib:~/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/lib/lean:~/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/lib:./.lake/packages/auto/.lake/build/lib ~/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/bin/lean ./.lake/packages/auto/././Auto/Lib/NatExtra.lean -R ./.lake/packages/auto/./. -o ./.lake/packages/auto/.lake/build/lib/Auto/Lib/NatExtra.olean -i ./.lake/packages/auto/.lake/build/lib/Auto/Lib/NatExtra.ilean -c ./.lake/packages/auto/.lake/build/ir/Auto/Lib/NatExtra.c
error: stdout:
./.lake/packages/auto/././Auto/Lib/NatExtra.lean:112:40: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
Nat.succ ?n
a b c : Nat
⊢ max a b < c ↔ a < c ∧ b < c

./.lake/packages/auto/././Auto/Lib/Pos.lean:97:43: error: unsolved goals
n n' : Nat
x✝ : n' + 2 ≠ 0
this : 2 * n' + 2 * 2 + 1 = 2 * n' + 3 + 2
⊢ 3 % 2 = 1

error: stdout:
./.lake/packages/auto/././Auto/Lib/BinTree.lean:434:42: error: unsolved goals
α : Type u_1
l : BinTree α
x : Option α
r : BinTree α
p : α → Prop
h : ∀ (n : Nat), Option.allp p (get?' (node l x r) n)
n✝ n : Nat
h' :
Option.allp p
(match (2 * n + 3 + 2) % 2 with
| 0 => get?' (left! (node l x r)) ((2 * n + 3 + 2) / 2)
| Nat.succ n_1 => get?' (right! (node l x r)) ((2 * n + 3 + 2) / 2))
⊢ 5 % 2 = 1

./.lake/packages/auto/././Auto/Embedding/LamSystem.lean:1639:4: error: dsimp made no progress

./.lake/packages/auto/././Auto/Embedding/LamConv.lean:1610:2: error: dsimp made no progress
./.lake/packages/auto/././Auto/Embedding/LamConv.lean:1624:2: error: dsimp made no progress

and more.

[Utensil Song]

These errors can be easily fixed by (not exhaustive but all are similar)

theorem Nat.max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c := by
  rw [← Nat.lt_eq]; unfold Nat.lt; rw [← Nat.add_one]; rw [Nat.max_add]
  rw [Nat.le_eq]; rw [Nat.max_le]; apply Iff.intro id id

    have heq : (2 * n' + 3 + 2) % 2 = 1 := by
      simp [Nat.add_mod_right, Nat.add_mod, Nat.mul_mod]
      rfl

        have eq₁ : (2 * n + 5) % 2 = 1 := by
          rw [Nat.add_mod]; simp; rfl

simp_all [LamTerm.rwGenAtIfSign, LamTerm.isSign]

unfold LamTerm.mpAll?

respectively, but I wonder if these are known regression or needed migrations.

[Josh Clune]

It looks like some of the proofs in lean-auto are breaking due to various changes from v4.3.0-rc1 and v4.4.0-rc1. At first glance, I'm pretty sure that most of the spots that are breaking pertain to other lean-auto functionalities, rather than the functionalities Duper actually depends on. So I think this should be relatively easy to fix. I'll take a look and try to push a version of Duper that builds on v4.4.0-rc1 as soon as I can. Sorry for the inconvenience, and thanks for letting me know of the issue.

[Utensil Song]

Thanks, also these breaking changes are brittle and I wonder if they are discussed before, the fixes are easy, but I don't know the new idiomatic way to write them as they look idiomatic to me as how they were. Changing dsimp to unfold or even simp_all, adding rfl after simp don't seem desired.

[Utensil Song]

There are 10 errors in .lake/packages/auto/Auto/Embedding/LamBitVec.lean including rfl type mismatch, rw pattern mismatch and apply fails to unify etc. , they are less easy to fix, e.g.

  theorem toNat_shiftLeft {a : Std.BitVec n} (i : Nat) : (a <<< i).toNat = (a.toNat * (2 ^ i)) % (2 ^ n) := by
    rw [shiftLeft_def]; rcases a with ⟨⟨a, isLt⟩⟩
    dsimp [Std.BitVec.shiftLeft, Std.BitVec.toNat, Std.BitVec.ofNat, Fin.ofNat']
    rw [Nat.shiftLeft_eq]

becomes

  theorem toNat_shiftLeft {a : Std.BitVec n} (i : Nat) : (a <<< i).toNat = (a.toNat * (2 ^ i)) % (2 ^ n) := by
    rw [shiftLeft_def]; rcases a with ⟨⟨a, isLt⟩⟩
    unfold Std.BitVec.shiftLeft
    unfold Std.BitVec.toNat
    unfold Std.BitVec.ofNat
    simp only [Nat.shiftLeft_eq, Nat.and_pow_two_is_mod]

(UPDATE: moved my messages to a new topic to focus on Duper discussions in the Duper topic)

[Notification Bot]

5 messages were moved here from #general > Duper by Utensil Song.

[Jon Eugster]

I also had a look at this a few days ago and it looked to me that the definition of Std.BitVec.ofNat changed in Std recently in a commit here which seems to be the main obstactle to bump LamBitVec.lean, which seems to be the biggest task to bump lean-auto to v4.4.0-rc1

In particular toNat_ofNat is no longer rfl, and that seems to be the main issue that needs fixing there. If thats done, the rest seems to follow rather easily

[Josh Clune]

Duper v0.0.5 now builds on Lean v4.4.0-rc1. For now, I've simply sidestepped the issue of proving toNat_ofNat in lean-auto because that portion of the codebase isn't really relevant to Duper itself. I'll plan to properly address that later, but for now, I think this should work. Feel free to let me know if you run into any additional issues.