Tactic Proof not Responding. Overflow?

Stream: new members

[ROCKY KAMEN-RUBIO]

Hi everyone! I'm trying to do a tactic proof that ends with a very long proposition that should simplify to false. Rather than going through it manually, I'm trying to use simp, finish, norm_num, etc. The problem is that the window with the goal state just goes to "updating" indefinitely. Have I reached the limit of what these tactics can do, or am I doing something wrong? Thanks!

import init.data.nat.basic
import init.algebra.ring
import init.algebra.norm_num
import tactic
set_option class.instance_max_depth 15000000

def myIsEven (n : ℕ) : Prop := n = (n/2)*2
def myIsOdd (n : ℕ) : Prop := ¬ (n = (n/2)*2)

--Alice only sees r and Bob only sees c. The strategy isn't (r,c) → (...) but two maps, r→(r1 r2 r3) and c → (c1 c2 c3)
--I'm using 0 and 1 instead of Green and Red as the two options to fill squares. This makes checking parity of strategies easier

def checkStrategyrc (r c : ℕ) (strategy : ((ℕ → ℕ × ℕ × ℕ) × (ℕ → ℕ × ℕ × ℕ))) : Prop :=
        --functionalize this with lists.
        let r1 := (strategy.1 r).1,
        r2 := (strategy.1 r).2.1,
        r3 := (strategy.1 r).2.2,
        c1 := (strategy.2 c).1,
        c2 := (strategy.2 c).2.1,
        c3 := (strategy.2 c).2.2

        in myIsEven(r1 + r2 + r3) ∧ myIsOdd(c1 + c2 + c3) ∧
        ((r = 1 ∧ c = 1 ∧ r1 = c1) ∨ (r = 1 ∧ c = 2 ∧ r2 = c1) ∨ (r = 1 ∧ c = 3 ∧ r3 = c1)
        ∨(r = 2 ∧ c = 1 ∧ r1 = c2) ∨ (r = 2 ∧ c = 2 ∧ r2 = c2) ∨ (r = 2 ∧ c = 3 ∧ r3 = c2)
        ∨(r = 3 ∧ c = 1 ∧ r1 = c3) ∨ (r = 3 ∧ c = 2 ∧ r2 = c3) ∨ (r = 3 ∧ c = 3 ∧ r3 = c3))

--checks all three conditions are met for the strategy
def checkStrategy (strategy : ((ℕ → ℕ × ℕ × ℕ) × (ℕ → ℕ × ℕ × ℕ))) : Prop :=
    (checkStrategyrc 1 1 strategy) ∧ (checkStrategyrc 1 2 strategy) ∧ (checkStrategyrc 1 3 strategy) ∧
    (checkStrategyrc 2 1 strategy) ∧ (checkStrategyrc 2 2 strategy) ∧ (checkStrategyrc 2 3 strategy) ∧
    (checkStrategyrc 3 1 strategy) ∧ (checkStrategyrc 3 2 strategy) ∧ (checkStrategyrc 3 3 strategy)

--someone on Zulip said to try putting this not directly after the import statements. This seems to have helped
open_locale classical
--given a strategy, we can't have it satisfy all the conditions
theorem noStrategy2 (strategy : ((ℕ → ℕ × ℕ × ℕ) × (ℕ → ℕ × ℕ × ℕ))) : ¬ (checkStrategy (strategy)) :=
begin
intro s,
rw checkStrategy at s,
repeat {rw checkStrategyrc at s},
simp at s,
revert s,
end

[Johan Commelin]

@ROCKY KAMEN-RUBIO Pro tip: If you wrap your code in

```lean
code goes here
```

then you'll get pretty formatting with syntax highlighting.

[ROCKY KAMEN-RUBIO]

Thank you!!! I was trying to figure out how to do that.

[Johan Commelin]

@ROCKY KAMEN-RUBIO Instead of repeat { rw foobar at s }, you could do simp only [foobar] at s.

[Johan Commelin]

I would also simp myIsEven and myIsOdd away.

[Johan Commelin]

Be sure to use simp only, because without the only Lean might try lots of other stuff as well.

[Johan Commelin]

In fact, you could even use dsimp only.

[Johan Commelin]

After that, I would try feeding it to tauto.

[Johan Commelin]

But really, here an external solver would be very helpful. Some people are working on this, but atm it isn't easy to use.

[ROCKY KAMEN-RUBIO]

dsimp only is giving me a "failed to simplify state" error, and tauto is updating forever.

[Kevin Buzzard]

Setting the class instance max depth to such a high value might well cause timeout problems. Why are you changing the max depth at all?

[Kevin Buzzard]

Actually you don't even seem to be using any typeclasses :-)

[ROCKY KAMEN-RUBIO]

I was getting class instance max depth exceeded errors so I increased the max depth. I'm still pretty new to lean so I don't fully understand the best practices. Any suggestions would be very much appreciated!

[Kevin Buzzard]

I'm a bit confused by this because your code doesn't have any typeclasses in.

[Kevin Buzzard]

What's the human-readable argument that proves this theorem?

[Kevin Buzzard]

theorem noStrategy2 (strategy : ((ℕ → ℕ × ℕ × ℕ) × (ℕ → ℕ × ℕ × ℕ))) : ¬ (checkStrategy (strategy)) :=
begin
intro s,
rw checkStrategy at s,
repeat {rw checkStrategyrc at s},
simp at s,
revert s,
unfold myIsEven,
unfold myIsOdd,
rw (show 1 = 2 ↔ false, by norm_num),
rw (show 2 = 1 ↔ false, by norm_num),
rw (show 3 = 1 ↔ false, by norm_num),
rw (show 1 = 3 ↔ false, by norm_num),
rw (show 3 = 2 ↔ false, by norm_num),
rw (show 2 = 3 ↔ false, by norm_num),
simp only [false_and, false_or],
tauto!, -- fails
end

[Kevin Buzzard]

⊢ ((strategy.fst 1).fst + ((strategy.fst 1).snd.fst + (strategy.fst 1).snd.snd) =
         ((strategy.fst 1).fst + ((strategy.fst 1).snd.fst + (strategy.fst 1).snd.snd)) / 2 * 2 ∧
       ¬(strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd) =
             ((strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd)) / 2 * 2 ∧
         ((strategy.fst 1).fst = (strategy.snd 1).fst ∨ false)) ∧
    ((strategy.fst 1).fst + ((strategy.fst 1).snd.fst + (strategy.fst 1).snd.snd) =
           ((strategy.fst 1).fst + ((strategy.fst 1).snd.fst + (strategy.fst 1).snd.snd)) / 2 * 2 ∧
         ¬(strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd) =
               ((strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd)) / 2 * 2 ∧
           ((strategy.fst 1).snd.fst = (strategy.snd 2).fst ∨ false)) ∧
      ((strategy.fst 1).fst + ((strategy.fst 1).snd.fst + (strategy.fst 1).snd.snd) =
             ((strategy.fst 1).fst + ((strategy.fst 1).snd.fst + (strategy.fst 1).snd.snd)) / 2 * 2 ∧
           ¬(strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd) =
                 ((strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd)) / 2 * 2 ∧
             ((strategy.fst 1).snd.snd = (strategy.snd 3).fst ∨ false)) ∧
        ((strategy.fst 2).fst + ((strategy.fst 2).snd.fst + (strategy.fst 2).snd.snd) =
               ((strategy.fst 2).fst + ((strategy.fst 2).snd.fst + (strategy.fst 2).snd.snd)) / 2 * 2 ∧
             ¬(strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd) =
                   ((strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd)) / 2 * 2 ∧
               ((strategy.fst 2).fst = (strategy.snd 1).snd.fst ∨ false)) ∧
          ((strategy.fst 2).fst + ((strategy.fst 2).snd.fst + (strategy.fst 2).snd.snd) =
                 ((strategy.fst 2).fst + ((strategy.fst 2).snd.fst + (strategy.fst 2).snd.snd)) / 2 * 2 ∧
               ¬(strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd) =
                     ((strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd)) / 2 * 2 ∧
                 ((strategy.fst 2).snd.fst = (strategy.snd 2).snd.fst ∨ false)) ∧
            ((strategy.fst 2).fst + ((strategy.fst 2).snd.fst + (strategy.fst 2).snd.snd) =
                   ((strategy.fst 2).fst + ((strategy.fst 2).snd.fst + (strategy.fst 2).snd.snd)) / 2 * 2 ∧
                 ¬(strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd) =
                       ((strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd)) / 2 * 2 ∧
                   ((strategy.fst 2).snd.snd = (strategy.snd 3).snd.fst ∨ false)) ∧
              ((strategy.fst 3).fst + ((strategy.fst 3).snd.fst + (strategy.fst 3).snd.snd) =
                     ((strategy.fst 3).fst + ((strategy.fst 3).snd.fst + (strategy.fst 3).snd.snd)) / 2 * 2 ∧
                   ¬(strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd) =
                         ((strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd)) / 2 * 2 ∧
                     ((strategy.fst 3).fst = (strategy.snd 1).snd.snd ∨ false)) ∧
                ((strategy.fst 3).fst + ((strategy.fst 3).snd.fst + (strategy.fst 3).snd.snd) =
                       ((strategy.fst 3).fst + ((strategy.fst 3).snd.fst + (strategy.fst 3).snd.snd)) / 2 * 2 ∧
                     ¬(strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd) =
                           ((strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd)) / 2 * 2 ∧
                       ((strategy.fst 3).snd.fst = (strategy.snd 2).snd.snd ∨ false)) ∧
                  (strategy.fst 3).fst + ((strategy.fst 3).snd.fst + (strategy.fst 3).snd.snd) =
                      ((strategy.fst 3).fst + ((strategy.fst 3).snd.fst + (strategy.fst 3).snd.snd)) / 2 * 2 ∧
                    ¬(strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd) =
                          ((strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd)) / 2 * 2 ∧
                      (strategy.fst 3).snd.snd = (strategy.snd 3).snd.snd →
  false

[ROCKY KAMEN-RUBIO]

The argument goes something like: Alice and Bob need both of their strategies to be consistent. This means that we can think of their strategies as sampling from a single coloring of the 3x3 board with Green/Red tiles (represented by 1 and 0). If we impose the condition that each row has an even number of green tiles, and each column has an odd number of tiles, then the total number of green tiles should be even by summing the rows, but odd by summing the columns, which is impossible.

My strategy is more of a brute force approach though. I figured this would be easier to implement in lean and once i got this working I'd go to more complex arguments.

[Kevin Buzzard]

I don't know anything about the board or tiles or strategy that you're talking about so I don't understand your argument.

[Yury G. Kudryashov]

Could you please describe the game in English? I can try to decode Lean but it takes some time.

[Kevin Buzzard]

theorem noStrategy2 (strategy : ((ℕ → ℕ × ℕ × ℕ) × (ℕ → ℕ × ℕ × ℕ))) : ¬ (checkStrategy (strategy)) :=
begin
intro s,
rw checkStrategy at s,
repeat {rw checkStrategyrc at s},
simp at s,
revert s,
rw (show 1 = 2 ↔ false, by norm_num),
rw (show 2 = 1 ↔ false, by norm_num),
rw (show 3 = 1 ↔ false, by norm_num),
rw (show 1 = 3 ↔ false, by norm_num),
rw (show 3 = 2 ↔ false, by norm_num),
rw (show 2 = 3 ↔ false, by norm_num),
simp only [false_and, false_or, or_false],
have h : myIsOdd = myIsOdd' := rfl,
rw h,
unfold myIsOdd',
intro s,
rcases s with ⟨⟨s1, t1, u1⟩, ⟨s2, t2, u2⟩, ⟨s3, t3, u3⟩,
               ⟨s4, t4, u4⟩, ⟨s5, t5, u5⟩, ⟨s6, t6, u6⟩,
               ⟨s7, t7, u7⟩, ⟨s8, t8, u8⟩, ⟨s9, t9, u9⟩⟩,
rw u1 at *,
rw u2 at *,
rw u3 at *,
rw u4 at *,
rw u5 at *,
rw u6 at *,
rw u7 at *,
rw u8 at *,
rw u9 at *,
sorry
end

gets us to

1 goal
strategy : (ℕ → ℕ × ℕ × ℕ) × (ℕ → ℕ × ℕ × ℕ),
h : myIsOdd = myIsOdd',
t1 : ¬myIsEven ((strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd)),
u1 : (strategy.fst 1).fst = (strategy.snd 1).fst,
t2 : ¬myIsEven ((strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd)),
u2 : (strategy.fst 1).snd.fst = (strategy.snd 2).fst,
t3 : ¬myIsEven ((strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd)),
u3 : (strategy.fst 1).snd.snd = (strategy.snd 3).fst,
t4 : ¬myIsEven ((strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd)),
u4 : (strategy.fst 2).fst = (strategy.snd 1).snd.fst,
t5 : ¬myIsEven ((strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd)),
u5 : (strategy.fst 2).snd.fst = (strategy.snd 2).snd.fst,
t6 : ¬myIsEven ((strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd)),
u6 : (strategy.fst 2).snd.snd = (strategy.snd 3).snd.fst,
t7 : ¬myIsEven ((strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd)),
u7 : (strategy.fst 3).fst = (strategy.snd 1).snd.snd,
t8 : ¬myIsEven ((strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd)),
u8 : (strategy.fst 3).snd.fst = (strategy.snd 2).snd.snd,
t9 : ¬myIsEven ((strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd)),
u9 : (strategy.fst 3).snd.snd = (strategy.snd 3).snd.snd,
s1 s2 s3 : myIsEven ((strategy.snd 1).fst + ((strategy.snd 2).fst + (strategy.snd 3).fst)),
s4 s5 s6 : myIsEven ((strategy.snd 1).snd.fst + ((strategy.snd 2).snd.fst + (strategy.snd 3).snd.fst)),
s7 s8 s9 : myIsEven ((strategy.snd 1).snd.snd + ((strategy.snd 2).snd.snd + (strategy.snd 3).snd.snd))
⊢ false

[ROCKY KAMEN-RUBIO]

Sorry, I don't think I've been very clear. Here is a more detailed explanation:

The Game: Alice is assigned a row and Bob is assigned a column of a 3x3 board. Neither knows the assignment of the other. The task is for each of them to color their respective row/column with Green and Red tiles (aka 1s and 0s) while meeting the following criteria:

1. Rows must have an even number of Green tiles
2. Columns must have an odd number of Green tiles
3. The two colorings must be consistent - they must agree on the color of the shared tile

They can plan a strategy beforehand but can't communicate after each gets their respective assignment.

My goal is to prove that there is no guaranteed successful strategy.

Lean Proof We can think of a strategy as a pair of maps, one from a row number to a triple of values we use to fill that row, the other from a column number to a triple of values we use to fill that column. checkStrategyrc checks that a given strategy works for a specific row r and column c by showing that the row sum is even, the column sum is odd, and the two agree at the intersection. checkStrategy calls checkStrategy on every combination of r and c in the 3x3 grid. Now we just need to show that no strategy passes checkStrategy.

More Intuitive proof (This is what I would like to implement next) Since Alice and Bob must agree on the value of the intersection of their respective row/column, and the location of this intersection is arbitrary, we can think of their strategies as sampling from a single tiled 3x3 board. Summing the values in the rows of this single board we get an even number, but summing the values in the columns we get an odd number. The sums of the values in all the tiles should be the same whether we do it by rows or columns, so we get a contradiction.

[Kevin Buzzard]

And now it seems to me that you might be able to prove it by observing that something like t1,t2,t3 (or whatever) together say that the sum of 9 terms is odd, and s1,s4,s7 (or whatever) say that the sum of the same 9 terms is even. But you can't expect Lean to figure this argument out because it knows no properties at all about your myIsEven and myIsOdd

[ROCKY KAMEN-RUBIO]

I also want to add that there are probably a number of ways to do what I'm attempting to do in much more efficient ways, both mathematically and in lean. I am open to any/all suggestions.

[Kevin Buzzard]

So this is why it gets stuck, I suspect. Your proof involves summing all nine entries of the board. But no tactic will even prove myIsEven(x) \and myIsEven(y) -> myIsEven(x+y)

[Kevin Buzzard]

If you want Lean to reason about your myIsEven you're going to have to train it or guide it.

[Kevin Buzzard]

So the next thing to need to do is to prove things like this. Alternatively you can use Lean's built in predicates, where this stuff might well be proved already.

[Kevin Buzzard]

t1 : ¬myIsEven ((strategy.snd 1).fst + ((strategy.snd 1).snd.fst + (strategy.snd 1).snd.snd)),
t2 : ¬myIsEven ((strategy.snd 2).fst + ((strategy.snd 2).snd.fst + (strategy.snd 2).snd.snd)),
t3 : ¬myIsEven ((strategy.snd 3).fst + ((strategy.snd 3).snd.fst + (strategy.snd 3).snd.snd)),
s1 : myIsEven ((strategy.snd 1).fst + ((strategy.snd 2).fst + (strategy.snd 3).fst)),
s4 : myIsEven ((strategy.snd 1).snd.fst + ((strategy.snd 2).snd.fst + (strategy.snd 3).snd.fst)),
s7 : myIsEven ((strategy.snd 1).snd.snd + ((strategy.snd 2).snd.snd + (strategy.snd 3).snd.snd))

Lean can't get from there to the end (these are facts from my session above). To get from there to the end you'll need ¬myIsEven x \and ¬myIsEven y -> myIsEven (x + y), ¬myIsEven x \and myIsEven y -> ¬myIsEven (x + y) and myIsEven x \and myIsEven y -> myIsEven (x + y). Note that the first of these is not at all obvious, you'll need some argument that says that every integer has remainder 0 or 1 when divided by 2 -- there is some content here. This is why Lean can't solve your problem. Once you have these three lemmas you'll be done modulo the fact that you'll have to prove (a+b+c)+(d+e+f)+(g+h+i)=(a+d+g)+(b+e+h)+(c+f+i) but the ring tactic will do this once you've isolated this as the thing to prove.

[Yury G. Kudryashov]

Are you sure you want to use your own myIsEven instead of nat.even from data/nat/parity in mathlib?

[Bryan Gin-ge Chen]

By the way, you don't need to explicitly import anything that starts with init, all of those files are automatically imported by Lean unless you tell it not to by starting the file with prelude.

[ROCKY KAMEN-RUBIO]

That makes sense. I was having trouble importing mathlib so I thought I'd just define my own even/odd functions. I finally got it working though so I think you're right and that would be much easier.

[Kevin Buzzard]

examples in mathlib? o_O

[Kevin Buzzard]

ROCKY KAMEN-RUBIO said:

I was having trouble importing mathlib so I thought I'd just define my own even/odd functions.

That's fine, but you then also have to prove every theorem about even and odd numbers which you need ;-)

[Kevin Buzzard]

not_even_one is currently my favourite mathlib theorem name :-)

[Yury G. Kudryashov]

I'd prove this for any pair of odd numbers (n, m) instead of (3, 3). Then strategies will have the types fin m → fin n → nat and fin n → fin m → nat, respectively, and you can use ∀ i, (finset.univ.sum (f i)).even.

[Yury G. Kudryashov]

You can also make your functions take the values in zmod 2, then it will be ∀ i, finset.univ.sum (f i) = 0 and ∀ j, finset.univ.sum (g j) = 1.

[Yury G. Kudryashov]

zmod 2 is defined as fin 2={n : nat | n < 2} with 1+1=0.

[Kevin Buzzard]

Here's a proof of your result with your even/odd modulo the standard facts:

theorem noStrategy2 (strategy : ((ℕ → ℕ × ℕ × ℕ) × (ℕ → ℕ × ℕ × ℕ))) : ¬ (checkStrategy (strategy)) :=
begin
intro s,
rw checkStrategy at s,
repeat {rw checkStrategyrc at s},
simp at s,
revert s,
rw (show 1 = 2 ↔ false, by norm_num),
rw (show 2 = 1 ↔ false, by norm_num),
rw (show 3 = 1 ↔ false, by norm_num),
rw (show 1 = 3 ↔ false, by norm_num),
rw (show 3 = 2 ↔ false, by norm_num),
rw (show 2 = 3 ↔ false, by norm_num),
simp only [false_and, false_or, or_false],
intro s,
rcases s with ⟨⟨s1, t1, u1⟩, ⟨s2, t2, u2⟩, ⟨s3, t3, u3⟩,
               ⟨s4, t4, u4⟩, ⟨s5, t5, u5⟩, ⟨s6, t6, u6⟩,
               ⟨s7, t7, u7⟩, ⟨s8, t8, u8⟩, ⟨s9, t9, u9⟩⟩,
rw u1 at *,
rw u2 at *,
rw u3 at *,
rw u4 at *,
rw u5 at *,
rw u6 at *,
rw u7 at *,
rw u8 at *,
rw u9 at *,
apply odd_add_even t1 (odd_add_odd t2 t3),
convert even_add_even s1 (even_add_even s4 s7) using 1,
ring,
congr' 2,
ring,
end

But I used

theorem odd_add_odd {m n} : myIsOdd m → myIsOdd n → myIsEven (m + n) := sorry
theorem odd_add_even {m n} : myIsOdd m → myIsEven n → myIsOdd (m + n) := sorry
theorem even_add_even {m n} : myIsEven m → myIsEven n → myIsEven (m + n) := sorry

so now it suffices to prove these.

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

ROCKY KAMEN-RUBIO said:

I was having trouble importing mathlib so I thought I'd just define my own even/odd functions.

That's fine, but you then also have to prove every theorem about even and odd numbers which you need ;-)

I see that now. Here I was trying to be all clever thinking I could just rewrite basic natural number definitions without importing any subsequent theorems.

[ROCKY KAMEN-RUBIO]

@Yury G. Kudryashov Doing it for a board of size (m,n) for odd m and n was one of my next goals. Can I just use quantifiers like that to iterate over all the elements of fin m? I was looking for some kind of for loop structure but it makes sense that this would be the lean-ier way of doing it.

[Yury G. Kudryashov]

∀ i : fin n, ... says exactly "for every element i of type fin n the following proposition holds".

[Rocky Kamen-Rubio]

Yury G. Kudryashov said:

I'd prove this for any pair of odd numbers (n, m) instead of (3, 3). Then strategies will have the types fin m → fin n → nat and fin n → fin m → nat, respectively, and you can use ∀ i, (finset.univ.sum (f i)).even.

@Yury G. Kudryashov I'm trying to implement this and I'm getting errors on finset.univ.sum. I've imported data.finset. Do I need to convert the function (StrategyA r) into a set, or tell lean to map it first? Screen-Shot-2020-02-16-at-12.39.09-PM.png Screen-Shot-2020-02-16-at-12.39.04-PM.png Screen-Shot-2020-02-16-at-12.38.56-PM.png Screen-Shot-2020-02-16-at-12.38.49-PM.png

[Bryan Gin-ge Chen]

Could you post copy+pastable code (or a link to a github gist containing such) so that we can reproduce your errors?

[Yury G. Kudryashov]

Did you import algebra.big_operators?

[Rocky Kamen-Rubio]

Just added that and I'm still getting the same errors.

[Yury G. Kudryashov]

Please copy+paste the file from start to the first error.

[Rocky Kamen-Rubio]

import init.data.nat.basic
import init.algebra.ring
import init.algebra.norm_num
import init
import tactic
import data.nat.parity
import data.finset
import algebra.big_operators
set_option class.instance_max_depth 15000000




def checkStrategymn {m n : nat} (strategyA : fin m → fin n → nat) (strategy B: fin n → fin m → nat) : Prop :=
∀ r : fin m, (finset.univ.sum (strategyA r)).even

[Yury G. Kudryashov]

Compiles with no errors here.

[Rocky Kamen-Rubio]

Weird... Any ideas?

[Bryan Gin-ge Chen]

What version of mathlib are you using?

[Bryan Gin-ge Chen]

I just tried with an older version of mathlib and you might need to try adding import data.fintype. By the way, I think I said this before, but you can delete everything that starts with import init since all of that is imported automatically by Lean.

[Rocky Kamen-Rubio]

Ok I added import data.fintype and that seems to have resolved the issue. That's interesting the issue would be mathlib being out of date because I only downloaded it about two weeks ago. Was there an update since then? Maybe I downloaded it from the wrong source by mistake...

[Bryan Gin-ge Chen]

From playing around with commenting / uncommenting imports, it looks like something in import tactic now has data.fintype as a dependency, whereas it didn't previously.

[Bryan Gin-ge Chen]

Hah, I guess I was the culprit: see PR #1962. I added fin_cases to the imports in tactic.default, and that indeed depends on data.fintype.

[Bryan Gin-ge Chen]

mathlib is a continuously moving target, for better or worse...

[Kevin Buzzard]

Rocky Kamen-Rubio said:

Was there an update since then?

There are updates most days! You can follow #rss if you want to see the progression of the library.

[Kevin Buzzard]

In fact you might want to check you're on Lean version 3.5.1 or you'll be missing the new goodies

[Rocky Kamen-Rubio]

Fascinating. This actually explains a lot...

[Rocky Kamen-Rubio]

Thank you all for you amazing support! Another potentially basic question. How do I get rid of a universal quantifier when there is a negation in front of it? It seems like generally one would use intro and then just prove the statement generally. If there's a negation though, this seems to not work, and I get stuck with a proposition with a quantifier that I can't use with rw or other common tactics.

[Bryan Gin-ge Chen]

Try rw or simp with not_forall. You might need to open_locale classical before to work with classical logic if you aren't already.

[Scott Morrison]

(we really need rw_hint... it shouldn't be hard)

[Mario Carneiro]

You probably don't need to use classical for this. Just prove a contradiction from the forall assumption, presumably by constructing a counterexample

[Rocky Kamen-Rubio]

I tried doing both rw not_forall at h, and simp only [not_forall] at h, but neither was successful. Here's a more specific minimal example of the type of situation I'm struggling with.

theorem myTheorem : ¬ (∀ x : nat, x = 2) :=
begin
intro h,
end

Edit: I've already done open_locale classical earlier in the file, so I assume that's not the issue. I feel like there's something about the way lean handles quantifiers that I'm not understanding (I remember the book talking about them being somehow equivalent to Pi functions, but the example they gave was pretty different from this)

[Yury G. Kudryashov]

After intro h you no longer have a negation in front of ∀. You can try replace h := h 1, norm_num at h.

[Scott Morrison]

Note that intro h here is doing exactly what by_contradiction h would do, which may help understand what's happening.

[Kevin Buzzard]

I don't really understand the question. Does push_neg help? This moves negations inside quantifiers

[Kevin Buzzard]

So it will turn not forall into exists not

[Patrick Massot]

Rocky, your question is a bit hard to answer without knowing whether you want a low-level answer or learn how to crush such a goal. You can still have a look at the following variations.

import tactic

example : ¬ (∀ x : nat, x = 2) :=
λ h, nat.succ_ne_zero 1 (h 0).symm

example : ¬ (∀ x : nat, x = 2) :=
begin
  intro h,
  exact nat.succ_ne_zero 1 (h 0).symm,
end

example : ¬ (∀ x : nat, x = 2) :=
begin
  intro h,
  specialize h 0,
  tauto,
end

example : ¬ (∀ x : nat, x = 2) :=
begin
  push_neg,
  use 0,
end

[Rocky Kamen-Rubio]

Thank you all for your replies! This has been very useful. Here are the two more complex cases I've been working with where I have trouble negotiating the universal quantifiers. I copied my previous post explaining what I'm trying to prove below. I'm having trouble producing a counterexample, and feel like it would be easier to use predicate logic to reduce the expression to something false, though I'm not totally sure how to best handle expressions like finset.univ.sum in cases like this. Any thoughts would be appreciate!

open_locale classical
def checkStrategyMN {m n : nat} (strategyA : fin m → fin n → nat) (strategyB: fin n → fin m → nat) : Prop :=
(∀ r : fin m, (∀ c : fin n, ((finset.univ.sum (strategyA r)).even) ∧ (¬ (finset.univ.sum (strategyB c)).even) ∧ ((strategyA r c) = (strategyB c r))))

theorem noStrategyMN {m n : nat} (strategyA : fin m → fin n → nat) (strategyB: fin n → fin m → nat) : ((¬ m.even) ∧ (¬ n.even)) → ¬ (checkStrategyMN strategyA strategyB) :=
begin
rw checkStrategyMN,
intros h1,
finish,
end

def board {m n : nat} (strategyA : fin m → fin n → nat) (strategyB: fin n → fin m → nat) : fin m → fin n → nat := strategyA --woah man...these representations are THE SAME!!!! (function that returns a vector and a matrix)

def consistent {m n : nat} (strategyA : fin m → fin n → nat) (strategyB: fin n → fin m → nat) : Prop
:= ∀ (r : fin m) (c : fin n), (strategyA r c) = (strategyB c r)

def sampleA {m n : nat} (board : fin m → fin n → nat) : fin m → fin n → nat := board

def sampleB {m n : nat} (board : fin m → fin n → nat) : fin n → fin m → nat := λ (n : fin n) (m : fin m), board m n
#check sampleA
#check sampleB

lemma board_equiv_strategy {m n : nat} (strategyA : fin m → fin n → nat) (strategyB: fin n → fin m → nat) :
(consistent strategyA strategyB) → (strategyA = ((sampleA (board strategyA strategyB))) ∧ (strategyB = (sampleB (board strategyA strategyB))))
:=
begin
intro h,
split,

rw sampleA,
rw board,

rw consistent at h,
rw sampleB,
rw board,
rw h,
end

def each_row_sum_even {m n : nat} (board : fin m → fin n → nat) : Prop := ∀ (r : fin m), (finset.univ.sum (sampleA board r)).even

def each_col_sum_odd {m n : nat} (board : fin m → fin n → nat) : Prop := ∀ (c : fin n), ¬(finset.univ.sum (sampleB board c)).even

def even_strategy {m n : nat} (strategyA : fin m → fin n → nat) : Prop := (∀ r : fin m, (∀ c : fin n, ((finset.univ.sum (strategyA r)).even)))

def odd_strategy {m n : nat} (strategyB : fin n → fin m → nat) : Prop := (∀ r : fin m, (∀ c : fin n, (¬ (finset.univ.sum (strategyB c)).even)))

lemma even_strategy_implies_even_rows {m n : nat} (strategyA : fin m → fin n → nat) (strategyB : fin n → fin m → nat)
: (even_strategy strategyA) → each_row_sum_even (board strategyA strategyB)
:=
begin
sorry
end

lemma odd_strategy_implies_odd_cols {m n : nat} (strategyA : fin m → fin n → nat) (strategyB : fin n → fin m → nat)
: (odd_strategy strategyB) → each_col_sum_odd (board strategyA strategyB)
:=
begin
sorry
end

def row_sum {m n : nat} (board : fin m → fin n → nat) : nat := (finset.univ.sum (sampleA board))

def col_sum {m n : nat} (board : fin m → fin n → nat) : nat := (finset.univ.sum (sampleB board))

lemma row_sum_eq_col_sum {m n : nat} (board : fin m → fin n → nat) : row_sum board = col_sum board
:=
begin
sorry
end

theorem noStrategyMN2 {m n : nat} (strategyA : fin m → fin n → nat) (strategyB: fin n → fin m → nat) : ¬ ((consistent strategyA strategyB) ∧  (even_strategy strategyA) ∧ (odd_strategy strategyB))
:=
begin
intro h,
cases h with c y,
cases y with even odd,
have x := even_strategy_implies_even_rows strategyA strategyB even,
have y := odd_strategy_implies_odd_cols strategyA strategyB odd,
end

The Game: Alice is assigned a row and Bob is assigned a column of a 3x3 mxn board for odd m and n. Neither knows the assignment of the other. The task is for each of them to color their respective row/column with Green and Red tiles (aka 1s and 0s) while meeting the following criteria:

1. Rows must have an even number of Green tiles
2. Columns must have an odd number of Green tiles
3. The two colorings must be consistent - they must agree on the color of the shared tile
4. They can plan a strategy beforehand but can't communicate after each gets their respective assignment.

My goal is to prove that there is no guaranteed successful strategy.

Lean Proof 1: We can think of a strategy as two maps (strategyA and strategyB) one from a row number to a map from column number to element of that row, the other from a column number to a map from row number to element in that column. checkStrategy checks that a given strategy satisfies the conditions listed.

Lean Proof 2: Since Alice and Bob must agree on the value of the intersection of their respective row/column, and the location of this intersection is arbitrary, we can think of their strategies as sampling from a single tiled 3x3 m x n board. Summing the values in the rows of this single board we get an even number, but summing the values in the columns we get an odd number. The sums of the values in all the tiles should be the same whether we do it by rows or columns, so we get a contradiction. To do this in lean, I start by defining the equivalent board, and what sampleA and sampleB would be from that board. Next, I am trying to prove board_equiv: the statement that sampling from this board is equivalent to both strategies if all the conditions are met. Next I show that the rows of the board must have even sums and the cols have odd sums, if the original strategies have even and odd sums. From here, I'm hoping showing the contradiction shouldn't be too hard, but I haven't gotten that far yet.

[Yury G. Kudryashov]

Please add "lean" after each opening of a code block. This way you'll have syntax highlighting.

[Rocky Kamen-Rubio]

Forgot about that, thanks for the reminder!