Zulip Chat Archive

Stream: new members

Topic: simplifying divisor statements


Kevin Lacker (Sep 30 2020 at 22:43):

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 (Sep 30 2020 at 22:44):

norm_num works

Kyle Miller (Sep 30 2020 at 22:44):

import tactic

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

Kevin Lacker (Sep 30 2020 at 22:46):

nice thanks

Kevin Lacker (Sep 30 2020 at 22:56):

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 (Sep 30 2020 at 23:01):

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

Kevin Lacker (Sep 30 2020 at 23:09):

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

Kevin Lacker (Sep 30 2020 at 23:09):

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 (Sep 30 2020 at 23:10):

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 (Sep 30 2020 at 23:11):

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 (Sep 30 2020 at 23:12):

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

Heather Macbeth (Sep 30 2020 at 23:13):

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

Heather Macbeth (Sep 30 2020 at 23:14):

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

Kevin Lacker (Sep 30 2020 at 23:15):

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

Kevin Lacker (Sep 30 2020 at 23:21):

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 (Sep 30 2020 at 23:23):

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 (Sep 30 2020 at 23:23):

well only one of them is true

Kevin Lacker (Sep 30 2020 at 23:23):

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

Mario Carneiro (Sep 30 2020 at 23:24):

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

Mario Carneiro (Sep 30 2020 at 23:24):

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

Mario Carneiro (Sep 30 2020 at 23:25):

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

Kevin Lacker (Sep 30 2020 at 23:25):

ok, excellent

Kevin Lacker (Sep 30 2020 at 23:25):

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

Yakov Pechersky (Sep 30 2020 at 23:25):

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

Mario Carneiro (Sep 30 2020 at 23:25):

it just calls simp with the passed arguments

Kevin Lacker (Sep 30 2020 at 23:26):

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

Mario Carneiro (Sep 30 2020 at 23:26):

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

Kevin Lacker (Sep 30 2020 at 23:26):

simp doesn't seem to work

Mario Carneiro (Sep 30 2020 at 23:26):

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

Kevin Lacker (Sep 30 2020 at 23:27):

cool

Mario Carneiro (Sep 30 2020 at 23:27):

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


Last updated: Dec 20 2023 at 11:08 UTC