equality vs decide equality

Stream: lean4

[Shreyas Srinivas]

I have a goal as follows:

(match decide (n % 2 = 1) with
  | true => 1
  | false => 0) =
  n % 2

When I use cases (decide (n%2) = 1), I get two cases:

unsolved goals
case false
n: ℕ
⊢ (match false with
  | true => 1
  | false => 0) =
  n % 2


case true
n: ℕ
⊢ (match true with
  | true => 1
  | false => 0) =
  n % 2

[Shreyas Srinivas]

This seems in line with the way cases works as a tactic. But how do I get lean to recognize that n%2 is either 1 or not 1. More generally how should I close a goal like this with decide around an equality.

[Shreyas Srinivas]

In lean 3 there is a lemma cond_to_bool_mod_two for nat. I can't find the lean4 equivalent

[Eric Wieser]

I think you need cases h : decide (n%2 = 1) if you want to avoid a dead end

[Reid Barton]

Does split help?

[Shreyas Srinivas]

If I apply split, I am left with two goals:

ase h_1
n: ℕ
⊢ 1 = n % 2


case h_2
n: ℕ
⊢ 0 = n % 2

with no hypothesis to close them with.

[Shreyas Srinivas]

The cases method gives me two hypothesis inside decide

case false
n: ℕ
h: decide (n % 2 = 1) = false
⊢ 0 = n % 2


case true
n: ℕ
h: decide (n % 2 = 1) = true
⊢ 1 = n % 2

[Sebastian Ullrich]

Did you use split instead of cases?

[Shreyas Srinivas]

yes

[Shreyas Srinivas]

I applied them separately

[Shreyas Srinivas]

About nat.cond_to_bool_mod_two, in lean 3, it is found in core/init.data.nat.lemmas (source : lean 3 docs ). Most of the lemmas here seem to have moved to std.data.nat.lemmas (source : lean 4 docs ), but I cannot the lemma for cond in the lean4 version

[Eric Wieser]

Perhaps it's worth pointing out that match decide (n % 2 = 1) with ... is a very strange way to spell if n % 2 = 1 then ...

[Eric Wieser]

So it's no surprise that you can't find many lemmas to help you

[Shreyas Srinivas]

It is a mathport thing

[Shreyas Srinivas]

In lean 3 there was a theorem with the goal bitvec.to_nat (to_bool (n % 2 = 1) ::ᵥ nil) = n % 2
Mathport changed that to Bitvec.toNat (decide (n % 2 = 1) ::ᵥ nil) = n % 2

[Eric Wieser]

Shreyas Srinivas said:

About nat.cond_to_bool_mod_two, in lean 3, it is found in core/init.data.nat.lemmas (source : lean 3 docs ). Most of the lemmas here seem to have moved to std.data.nat.lemmas (source : lean 4 docs ), but I cannot the lemma for cond in the lean4 version

Then you should port this lemma to Mathlib/Init/Data/Nat/Lemmas

[Eric Wieser]

Shreyas Srinivas said:

The cases method gives me two hypothesis inside decide

This looks like you're at least still at a provable goal.

[Shreyas Srinivas]

Found a note in the file here

[Shreyas Srinivas]

Eric Wieser said:

Shreyas Srinivas said:

The cases method gives me two hypothesis inside decide

This looks like you're at least still at a provable goal.

I am not familiar with how to use something inside a decide call yet.

[Shreyas Srinivas]

throwingrw or simp at it doesn't seem to work.

[Eric Wieser]

There should be a lemma that says decide p = true iff p

[Shreyas Srinivas]

I am not sure that can be an iff. not all propositions are decidable.

[Eric Wieser]

Is there a reason you can't do by_cases h : x % 2 = 1, like the Lean3 proof?

[Shreyas Srinivas]

The original proof is

 simp [bits_to_nat_to_list],
  unfold bits_to_nat add_lsb list.foldl cond,
  simp [cond_to_bool_mod_two],

[Shreyas Srinivas]

I'll try by_cases now

[Shreyas Srinivas]

okay that works.

[Eric Wieser]

Why did you write your own proof instead of using the mathport one?

[Eric Wieser]

If you're porting stuff, you should use the mathport output

[Shreyas Srinivas]

I did. The last step was the issue. I am just replacing that one

[Shreyas Srinivas]

simp [cond_to_bool_mod_two] does nothing in lean4 because the lemma doesn't exist yet.

[Shreyas Srinivas]

Btw, I put this in lean4, because the question of how to handle equalities inside decide seemed like it might be of general interest.

[Kyle Miller]

Shreyas Srinivas said:

I am not sure that can be an iff. not all propositions are decidable.

docs4#decide_eq_true_iff

[Shreyas Srinivas]

Ah okay, so there is a Decidable instance on p and it works.

[Shreyas Srinivas]

This one is on #queue4 now (Data.Bitvec.Core)

[Eric Wieser]

Shreyas Srinivas said:

simp [cond_to_bool_mod_two] does nothing in lean4 because the lemma doesn't exist yet.

Right, so at that point you should find cond_to_bool_mod_two in mathport rather than looking for a different proof!

[Shreyas Srinivas]

It was not there.
Shreyas Srinivas said:

Found a note in the file here

This theorem is a todo

[Eric Wieser]

Great, sounds like now is the time to do it

[Eric Wieser]

Should just need copying in from https://github.com/leanprover-community/lean3port/blob/44b836ec48e1882103ab9ac0fea4dce2bf402797/Leanbin/Init/Data/Nat/Lemmas.lean#L1502-L1508

[Shreyas Srinivas]

Eric Wieser said:

Should just need copying in from https://github.com/leanprover-community/lean3port/blob/44b836ec48e1882103ab9ac0fea4dce2bf402797/Leanbin/Init/Data/Nat/Lemmas.lean#L1502-L1508

Got it. done and pushed.

[Shreyas Srinivas]

It actually breaks the proof. Do I need to add the @[simp] attribute to the theorem.

[Shreyas Srinivas]

That did not fix it either.

[Shreyas Srinivas]

@Eric Wieser the proof is broken again.

[Eric Wieser]

Broken in what way? The cache isn't available yet so I can't try it myself

[Shreyas Srinivas]

simp [Nat.cond_decide_mod_two] does nothing

[Shreyas Srinivas]

Shreyas Srinivas said:

simp [Nat.cond_decide_mod_two] does nothing

This is the lean4 equivalent of lean3's simp [cond_to_bool_mod_two],

[Eric Wieser]

(deleted)

[Eric Wieser]

simp [Nat.cond_decide_mod_two, -Bool.cond_decide] works

[Eric Wieser]

Remember to add a porting note when you use that, because it's not what mathlib3 had

[Shreyas Srinivas]

changing Init.Data.Nat.Lemmas leads to a very long build time. Is it because lake is rebuilding all downstream packages ?

[Shreyas Srinivas]

Eric Wieser said:

simp [Nat.cond_decide_mod_two, -Bool.cond_decide] works

Doesn't work.
I still have the following state:

unsolved goals
n: ℕ
⊢ (match decide (n % 2 = 1) with
  | true => 1
  | false => 0) =
  n % 2

[Eric Wieser]

Sorry, I keep getting tricked by the error appearing on the by line

[Shreyas Srinivas]

The proof I had plugged in was working. Should I plug it back in?

[Eric Wieser]

No, I think it would be better to understand why the old proof doesn't work

[Eric Wieser]

You could work that our by using simp? in mathlib3 and 4, and seeing what changed

[Eric Wieser]

This works I think?

theorem bits_toNat_decide (n : ℕ) : Bitvec.toNat (decide (n % 2 = 1) ::ᵥ nil) = n % 2 := by
  simp [bitsToNat_toList]
  unfold bitsToNat addLsb List.foldl
  simp [Nat.cond_decide_mod_two, -Bool.cond_decide]

[Shreyas Srinivas]

yeah that works