Friction around simp lemma simplifying easy statement

Stream: general

[l1mey]

I have these definitions of a positive natural (parts copied from Mathlib), and iN, which is an LLVM style integer without undef.

def PNat := { n : Nat // 0 < n } deriving DecidableEq

@[coe]
def PNat.val : PNat → Nat := Subtype.val

instance : OfNat PNat (n + 1) where
  ofNat := ⟨n + 1, by simp⟩

instance : Coe PNat Nat :=
  ⟨PNat.val⟩

@[simp]
theorem PNat.ne_zero (n : PNat) : ↑n ≠ (0 : Nat) := by
  exact Nat.ne_of_gt n.property

inductive iN (bits : PNat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

I am trying to prove a couple trivial theorems, and I've been having trouble helping the simplifier work on it. It must be due to my convoluted definitions but it just seems like iN doesn't play well with BitVecs.

protected def iN.shlNswClean {n : PNat} (a : BitVec n) (b : BitVec n) : iN n :=
  let s := b.toNat

  if b = 0 then
    bitvec a
  else if s ≥ n then
    poison
  else
    let res := a <<< s
    -- does the sign bit of the result differ from the sign bit of the original number?
    if a.msb ≠ res.msb then
      poison
    else
      bitvec res

protected def iN.shlNsw {n} : iN n → iN n → iN n
  | poison, _ => poison
  | _, poison => poison
  | bitvec a, bitvec b => iN.shlNswClean a b

theorem test_clean {n : PNat} (x : BitVec n): iN.shlNswClean x 0 = bitvec x := by
  unfold iN.shlNswClean
  simp

theorem test_without {n} (x : iN n): iN.shlNsw x 0 = x := by
  unfold iN.shlNsw
  split <;> try simp [*] at *
  /-
  case h_3
  n : PNat
  x✝¹ x✝ : iN n
  a✝ b✝ : BitVec ↑n
  heq✝ : 0 = bitvec b✝
  ⊢ iN.shlNswClean a✝ b✝ = bitvec a✝
  -/
  sorry

The implementation of iN.shlNswClean isn't particularly important. After the unfold iN.shlNsw and removal of the poison cases (unfold + split), it should be that test_clean and test_without be functionally equivalent. But there seems to be this bunch of hypotheses that I can't get rid of.

I know that without PNat.ne_zero, the goal of test_clean fails to be simplified and proved. This is the only simp lemma I have for PNat:

@[simp]
theorem PNat.ne_zero (n : PNat) : ↑n ≠ (0 : Nat) := by
  exact Nat.ne_of_gt n.property

Simp is also unable to dispell another goal. I was suggested creating an injectivity simp lemma but that didn't work either:

@[simp] theorem bitvec_inj {n : PNat} {a b : BitVec (↑n)} :
  iN.bitvec a = iN.bitvec b ↔ a = b := by
  constructor <;> intro h <;> cases h <;> rfl

theorem iN.bitvec_eq_zero_iff {n : PNat} {b : BitVec n} : (iN.bitvec b = 0) ↔ (b = 0) := by
  simp
  /-
  n : PNat
  b : BitVec ↑n
  ⊢ bitvec b = 0 ↔ b = 0#↑n
  -/
  sorry

Like PNat.ne_zero, it seems like there needs to be a lot of simp lemmas for me to create. There is a lot of needless friction after replacing Nat with PNat in the definition, like what I had before:

inductive iN (bits : Nat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

Positive bitwidth is necessary, otherwise I would have to go down the path of defining (0 : iN 0) / 0 and so on (does it return poison or not?).

[Kyle Miller]

Could you make a #mwe?

[Kyle Miller]

General advice I have for this is that it's expected that it will take writing a good number of lemmas to fully characterize your definitions.

[l1mey]

Here is my MWE: mwe.lean. I believe that Lean being unable to solve iN.bitvec_eq_zero_iff is due to Lean not unwrapping OfNat?

[l1mey]

I edited the question to include the definition of PNat which I accidentally left out. It is:

def PNat := { n : Nat // 0 < n } deriving DecidableEq

[l1mey]

Instead of writing a theorem for iN.bitvec_eq_zero_iff, that proves (iN.bitvec b = 0) ↔ (b = 0), it would be better to make it general and show it for every OfNat literal. However, I wouldn't know how express that.

[Kyle Miller]

Are you rolling your own PNat, or is this Mathlib's docs#PNat and you've extracted it for the mwe? (It's ok importing mathlib for this sort of mwe.)

[l1mey]

This has been extracted from Mathlib, just a couple lines from the file PNat/Notation.lean. I have decided to roll my own in my code and that is reflected in the MWE.

[Kyle Miller]

Here's a quick way to deal with bitvec_eq_zero_iff:

theorem iN.bitvec_zero_eq_zero (n : PNat): bitvec (0 : BitVec n) = 0 := rfl

theorem iN.bitvec_eq_zero_iff {n : PNat} {b : BitVec n} : iN.bitvec b = 0 ↔ b = 0 := by
  simp [← bitvec_zero_eq_zero]

The first lemma could be a simp lemma I think.

[l1mey]

I found that this theorem solves it in the general case for zero iff:

@[simp]
theorem iN.bitvec_eq_ofNat_iff {n : PNat} {b : BitVec n} (val : Nat) :
    (iN.bitvec b = bitvec (val : BitVec n)) ↔ (b = val) := by
  simp

But this seems quite a bit finicky. Other than that, I am still left with ⊢ iN.shlNswClean a✝ b✝ = bitvec a✝ in test_without which is a bit tricky.

[Kyle Miller]

This expresses that theorem using OfNat literals:

theorem iN.ofnat_eq_zero_iff {n : PNat} (k : Nat) : (OfNat.ofNat k : iN n) = 0 ↔ (OfNat.ofNat k : BitVec n) = 0 :=
  iN.bitvec_eq_zero_iff

It's probably missing no_index annotations around the literals for simp to apply it

[l1mey]

That is good, I looked around for no_index and found a couple. So I am normalising the iN literal representation and that problem is solved. However, I still want to deal with test_without:

/-- Theorem for normalizing the iN literal representation. -/
-- This will perform rewrites of `0 => 0 = bitvec (OfNat.ofNat 0)`, which is just a `BitVec` literal.
@[simp]
theorem ofNat_eq_bitvec {n : PNat} (val : Nat) :
  ((no_index OfNat.ofNat val) : iN n) = bitvec (no_index OfNat.ofNat val) := rfl

@[simp]
theorem solve_current {n: PNat} {b : BitVec ↑n} {h : (no_index BitVec.ofNat ↑n val) = b}
    : b = (no_index BitVec.ofNat ↑n val) := by

  rw [← h]

theorem test_without {n} (x : iN n): iN.shlNsw x 0 = x := by
  unfold iN.shlNsw
  split <;> try simp [*] at *
  /-
  case h_3
  n : PNat
  x✝¹ x✝ : iN n
  a✝ b✝ : BitVec ↑n
  heq✝ : 0#↑n = b✝
  ⊢ iN.shlNswClean a✝ b✝ = bitvec a✝
  -/

Still the same issue. I tried to create the solve_current theorem to see if I could get simp to solve this.