simplifying divisor statements

Stream: new members

[Kevin Lacker]

Pretty mundane question but I can't figure it out - is there some tactic that will automatically prove that 11 is not a divisor of 100? (couldnt quite get the lean code to display in zulip.) \not (11 \| 100)

[Kyle Miller]

norm_num works

[Kyle Miller]

import tactic

example : ¬ (11 ∣ 100) :=
begin
  norm_num,
end

[Kevin Lacker]

nice thanks

[Kevin Lacker]

ok similar question. i have a function defined as def sum_of_squares (L : list ℕ) : ℕ := L.foldr (λ x y, x*x + y) 0. I would like to just automatically expand this out on a given list to have it be able to solve that, for example, sum_of_squares [1, 1, 0] = 2. is there any tactic that can do this?

[Kevin Lacker]

well, i figured this out by trial and error, first norm_num then ring can do it

[Kevin Lacker]

hmm, but if the statement is mildly more complicated - 10 \ne sum_of_squares [1, 1, 0] - then ring cannot solve it

[Kevin Lacker]

i feel like i must be solving this the wrong way, i am just stabbing around seeing what these tactics can automatically solve

[Kevin Lacker]

whereas i want to be expressing, hey this sum_of_squares function can just be simplified wherever it occurs in an expression

[Alex J. Best]

def sum_of_squares (L : list ℕ) : ℕ := L.foldr (λ x y, x*x + y) 0
example :10 ≠ sum_of_squares [1, 1, 0] :=
begin
  norm_num [sum_of_squares],
end

[Alex J. Best]

If you give the def to norm_num it will pass it on to the simplifier and then do all the arithmetic.

[Heather Macbeth]

You can mark a definition @[reducible], also:
https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html

[Heather Macbeth]

And there is unfold sum_of_squares (optionally at ...) to get rid of it just in one place.

[Kevin Lacker]

reducible does not seem to enable norm_num to solve it here, but passing along the definition explicitly does

[Kevin Lacker]

okay, this is a more complicated question. I have an expression a \or b, and I know that one of a or b is provable by norm_num, but I don't know which. is there a way to say, try it out on both of them, and as long as it works on one of them, then the proof is fine?

[Bryan Gin-ge Chen]

How do you know that one of them is provable by norm_num? Is that "meta" knowledge, or is it something in the context?

[Kevin Lacker]

well only one of them is true

[Kevin Lacker]

i mean, I personally know it. lean doesn't know anything of the sort

[Mario Carneiro]

Don't use reducible for recursive definitions, that only makes sense for "abbreviation" style definitions

[Mario Carneiro]

If you have a \or b and norm_num can solve one of them then it can solve the or

[Mario Carneiro]

because it passes all that along to simp and simp will simplify true \or p to true

[Kevin Lacker]

ok, excellent

[Kevin Lacker]

and presumably i can pass irrelevant functions to norm_num and it'll happily ignore them

[Yakov Pechersky]

Why not do a <|> with or something with try?

[Mario Carneiro]

it just calls simp with the passed arguments

[Kevin Lacker]

maybe I shoudl be doing that. <|> is just yet more lean syntax i have not heard of

[Mario Carneiro]

you should prefer simp over norm_num unless you have some numerical calculations to do in the middle

[Kevin Lacker]

simp doesn't seem to work

[Mario Carneiro]

<|> is a tactic combinator that lets you try one tactic and then another if the first fails

[Kevin Lacker]

cool

[Mario Carneiro]

for example {left, norm_num} <|> {right, norm_num} would do what you suggested