Stream: new members

Topic: Match does not fold away

Tobias Grosser (Jun 20 2023 at 07:37):

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 (Jun 20 2023 at 07:42):

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

Mario Carneiro (Jun 20 2023 at 07:42):

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

Mario Carneiro (Jun 20 2023 at 07:45):

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

Tobias Grosser (Jun 20 2023 at 07:45):

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 (Jun 20 2023 at 07:47):

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

Mario Carneiro (Jun 20 2023 at 07:48):

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

Tobias Grosser (Jun 20 2023 at 07:48):

The one above is a MWE, no?

Mario Carneiro (Jun 20 2023 at 07:48):

is bitvec available without imports?

Tobias Grosser (Jun 20 2023 at 07:49):

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 (Jun 20 2023 at 07:49):

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

Tobias Grosser (Jun 20 2023 at 07:50):

I added two import lines in the code above.

Mario Carneiro (Jun 20 2023 at 07:50):

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 (Jun 20 2023 at 07:51):

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

Mario Carneiro (Jun 20 2023 at 07:52):

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

Tobias Grosser (Jun 20 2023 at 07:53):

.. working on it ..

Mario Carneiro (Jun 20 2023 at 07:55):

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

Mario Carneiro (Jun 20 2023 at 07:56):

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]


OK. That works.

Tobias Grosser (Jun 20 2023 at 08:00):

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

Mario Carneiro (Jun 20 2023 at 08:01):

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 (Jun 20 2023 at 08:02):

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 (Jun 20 2023 at 08:05):

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 (Jun 20 2023 at 08:05):

Meaning, it again does not fold away.

Tobias Grosser (Jun 20 2023 at 08:05):

(when introducing w)

Mario Carneiro (Jun 20 2023 at 08:06):

ah, now you can apply my first suggestion

Mario Carneiro (Jun 20 2023 at 08:06):

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

Tobias Grosser (Jun 20 2023 at 08:09):

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 (Jun 20 2023 at 08:09):

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

Mario Carneiro (Jun 20 2023 at 08:10):

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

Mario Carneiro (Jun 20 2023 at 08:11):

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 (Jun 20 2023 at 08:14):

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

Tobias Grosser (Jun 20 2023 at 08:15):

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 (Jun 20 2023 at 08:39):

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 (Jun 20 2023 at 08:39):

I was surprised not to find H1 in mathlib

Last updated: Dec 20 2023 at 11:08 UTC