Match does not fold away

Stream: new members

[Tobias Grosser]

I just came across this MWE and was wondering if someone can explain me why my match does not fold away:

import Mathlib.Data.Vector
import Mathlib.Data.Bitvec.Defs

/--
i: Fin (List.length (Vector.toList (Bitvec.ofInt 1 (-1))))
⊢ List.get
    (Vector.toList
      (match 1, -1 with
      | n, Int.ofNat m => Bitvec.ofNat n m
      | n, Int.negSucc m => Bitvec.not (Bitvec.ofNat n m)))
    i =
  true
--/

theorem match_does_not_fold_away : List.get ((Bitvec.ofInt 1 (-1)).toList) i = true := by
  simp[Bitvec.ofInt]
  simp
  sorry

[Mario Carneiro]

you would need a simp lemma to reduce -1 to negSucc of something

[Mario Carneiro]

you could do simp [show -1 = negSucc 0 by rfl]

[Mario Carneiro]

probably -(succ n) = negSucc n will also work as a simp lemma here

[Tobias Grosser]

Thank you @Mario Carneiro for the quick response. I guess this is the underlying issue.

simp [show -1 = Int.negSucc 0 by rfl]

Does not work. The output remains the same.

[Mario Carneiro]

hm, you will need to give an actual MWE, this seems like it should work unless there are some hidden dependencies

[Mario Carneiro]

oh of course, you are using List.get which is a dependent function

[Tobias Grosser]

The one above is a MWE, no?

[Mario Carneiro]

is bitvec available without imports?

[Tobias Grosser]

Maybe not. How do I create a MWE that I can actually test? Do I need to build a full lake repository. It will need mathlib and the Bitvec imports.

[Mario Carneiro]

It's fine if you want to import files from mathlib, as long as they exist on master

[Tobias Grosser]

I added two import lines in the code above.

[Mario Carneiro]

I usually use a blank test file within a project set up to be able to import mathlib (either mathlib itself or a downstream project)

[Tobias Grosser]

OK. I tested the above MWE and it compiles and showes the issue.

[Mario Carneiro]

bitvec.basic not found?

[Mario Carneiro]

you can stub out anything that isn't being unfolded in the MWE

[Tobias Grosser]

.. working on it ..

[Mario Carneiro]

Oh it's Mathlib.Data.Bitvec.Defs on master

[Mario Carneiro]

It was the dependencies after all. Here's the trick:

theorem match_does_not_fold_away : List.get ((Bitvec.ofInt 1 (-1)).toList) i = true := by
  rw [← Option.some_inj, ← List.get?_eq_get]
  simp [Bitvec.ofInt]

[Tobias Grosser]

OK. That works.

[Tobias Grosser]

I am still trying to understand what is going on here.

[Mario Carneiro]

List.get is a dependent function, it has the type List.get (l : List A) (i : Fin l.length) : A. That means that you can't rewrite l without making whatever expression is in for i ill-typed

[Mario Carneiro]

there are ways to handle these kinds of situations, but when possible it's usually easier to swap it for a non-dependent function, here List.get? (l : List A) (i : Nat) : Option A, since this decouples l and i and makes it possible to rewrite them separately

[Tobias Grosser]

Now things break with:

theorem match_does_not_fold_away3 : List.get ((Bitvec.ofInt w (-1)).toList) i = true := by
  rw [← Option.some_inj, ← List.get?_eq_get]
  simp [Bitvec.ofInt]

[Tobias Grosser]

Meaning, it again does not fold away.

[Tobias Grosser]

(when introducing w)

[Tobias Grosser]

Let me think about your reply for a moment.

[Mario Carneiro]

ah, now you can apply my first suggestion

[Mario Carneiro]

I think simp was getting the 1, -1 case simply by decide, it wasn't actually unfolding the match

[Tobias Grosser]

theorem succ {n : Nat} : (-(Int.succ n) = Int.negSucc n) := by
  sorry

theorem match_does_not_fold_away3 : List.get ((Bitvec.ofInt w (-1)).toList) i = true := by
  simp [succ]
  rw [← Option.some_inj, ← List.get?_eq_get]
  simp [succ]
  simp [Bitvec.ofInt, succ]
  simp [succ]

[Mario Carneiro]

yeah that one doesn't seem to work, but the show -1 = negSucc 0 by rfl one does

[Mario Carneiro]

-1 is actually Neg.neg (OfNat.ofNat 1 : Int) which doesn't quite match the LHS of that succ theorem

[Mario Carneiro]

you could use

theorem neg_ofNat_succ : -OfNat.ofNat (Nat.succ n) = Int.negSucc n := rfl

but it's a pretty contrived lemma

[Tobias Grosser]

OK. I guess I can make progress now. That is nice. Thank you.

[Tobias Grosser]

Now I need to proof:

w: ℕ
i: Fin (List.length (Vector.toList (Bitvec.ofInt w (-1))))
⊢ List.get? (Vector.toList (Bitvec.not (Bitvec.ofNat w 0))) ↑i = some true

I have no proof strategy yet, but will play a little. Thank you so much. That was super helpful.

[Mario Carneiro]

theorem match_does_not_fold_away : List.get ((Bitvec.ofInt w (-1)).toList) i = true := by
  rw [← Option.some_inj, ← List.get?_eq_get]
  simp [Bitvec.ofInt, show -1 = Int.negSucc 0 by rfl, Bitvec.not]
  have H1 : ∀ n, Bitvec.ofNat n 0 = Vector.replicate n false := sorry
  simp [H1, Vector.replicate]; rw [List.get?_eq_get, List.get_replicate]
  simpa using i.2

[Mario Carneiro]

I was surprised not to find H1 in mathlib