dec_trivial for zmod 8

Stream: new members

[Damiano Testa]

Dear All,

I do not know anything about computability, but I would have thought that the lemma below should be provable "automatically". I do not mind if you change the set to something more "decidable", but I would like to get Lean to check for me that the sum of 4 numbers that are all either 0 or 1 can be divisible by 8 iff each of the numbers is 0.

I would prefer a solution that "teaches" me how to work with decidable. Something along the lines of "oh, you have to write this, to get a decidable instance on all props of this form...", ideally!

Thanks!

import data.zmod.basic

lemma zmod.sq_mod_eight_sum (a b c d : zmod 8)
  (h : a + b + c + d = 0) (se : ({a, b, c, d} : set (zmod 8)) ⊆ {0, 1}) :
  a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0 :=
by dec_trivial!  --fails, since it does not have a decidable instance:
failed to synthesize type class instance for
⊢ decidable
    (∀ (a b c d : zmod 8), a + b + c + d = 0 → {a, b, c, d} ⊆ {0, 1} → a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0)

[Yakov Pechersky]

norm_fin and norm_num should help here, or they should be taught to understand zmod

[Alex J. Best]

Like you say, you just have to change set to something more decidable, in this case finset works. I'm not sure I can teach anything other than that finite sets are inherently more decidable than infinite!
You can see the instance used via

#check (by apply_instance : decidable ((({0} : finset (zmod 8)) ⊆ {0}))

the analogous thing for set isn't found, however I think it is checking membership that makes the difference, compare

#check (by apply_instance : decidable (0 ∈ ({1,0} : finset (zmod 8))))

#check (by apply_instance : decidable (0 ∈ ({1,0} : set (zmod 8))))

curiously the second version works for singletons though

#check (by apply_instance : decidable (0 ∈ ({1} : set (zmod 8))))

[Damiano Testa]

Yakov, by norm_num says failed to simplify. norm_fin might require an import that I do not have...

[Damiano Testa]

Alex, thanks! This is already good! I will try to produce a finset instead of a set, then (or possibly try to stick with singletons :wink: ).

[Yakov Pechersky]

Here's what I mean

import data.zmod.basic
import tactic.norm_fin

lemma zmod.sq_mod_eight_sum (a b c d : fin 8)
  (h : a + b + c + d = 0) (se : ({a, b, c, d} : finset (fin 8)) ⊆ {0, 1}) :
  a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0 :=
begin
  have : ∀ (x : fin 8), x ∈ ({a, b, c, d} : finset (fin 8)) →  x = 0 ∨ x = 1,
  { intros x hx,
    simpa using se hx },
  have ha := this a,
  have hb := this b,
  have hc := this c,
  have hd := this d,
  simp only [true_or, eq_self_iff_true, forall_true_left, or_true, finset.mem_insert,
    finset.mem_singleton] at ha hb hc hd,
  rcases ha with rfl|rfl;
  rcases hb with rfl|rfl;
  rcases hc with rfl|rfl;
  rcases hd with rfl|rfl,
  { simp }, -- the first goal is all zeros
  any_goals {
    contrapose! h,
    norm_num  } -- norm_num can figure out
end

[Damiano Testa]

Yakov, thanks a lot! I will take a close look at your solution, although it feels a little long, given what it is trying to prove!

Alternatively,

lemma zmod.sq_mod_eight_sum (a b c d : zmod 8)
  (h : a + b + c + d = 0) (se : ({a, b, c, d} : finset (zmod 8)) ⊆ {0, 1}) :
  a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0 :=
by dec_trivial!

actually works, but is a little slow, I think!

[Damiano Testa]

Yakov, thanks a lot! I looked at your code and I understand better what is going on.

I have a follow up question: you used fin 8 instead of zmod 8 to be able to use norm_fin? (I had never seen norm_fin before.)

[Johan Commelin]

@Damiano Testa My guess is that dec_trivial! has to loop through (zmod 8)^4.

[Johan Commelin]

If you phrase it as a b c d : nat and add assumptions a <= 1 etc..., then there are only 2 ^ 4 options. That should be reasonably fast.

[Johan Commelin]

And from the nat-version to the zmod 8 version shouldn't be too much work either.

[Damiano Testa]

I see, thanks for the suggestion, Johan! There is also a further issue is that this was (partially) minimized: I really care about a, b, c, d being squares modulo 8, so they can also be 4 [in which case, they all are either 0 or 4, of course]. Still, it might be more efficient to use a <= 4 (but not 2 or 3), than what I was trying.

Thanks a lot!

[Mario Carneiro]

If you use \forall a b c d \in [0, 1, 4] it will only go through 3^4 options

[Yakov Pechersky]

@Mario Carneiro should norm_fin be extended to work on zmod automatically?

[Damiano Testa]

Mario, thanks for the comment! I think that I got it to work in 12secs. Honestly, I do not know if this is fast or slow! :upside_down:

[Yakov Pechersky]

That's pretty slow. You could help it along to instead phrase the proof as something about the cardinality of finset zmod bit0 k less than bit0 k, where the finset is a subset of 0, 1, k

[Mario Carneiro]

Yakov Pechersky said:

Mario Carneiro should norm_fin be extended to work on zmod automatically?

Sure, but like norm_num it's not intended for quantified statements like this example

[Mario Carneiro]

Also you can solve for d to make it only 3^3 options

[Damiano Testa]

Ok, I can see how these suggestions will cut down the number of computations. I am happy that such case bashes are rare in the kind of arguments that I usually think about!