Zulip Chat Archive

Stream: maths

Topic: mul_left_cancel


view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:36):

Hi! I'm trying to find the proof of mul_left_cancel in https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/, or in other words:
theorem mul_left_cancel (a b c : mynat) (ha : a ≠ 0) : a * b = a * c → b = c :=

I'm in constructivist logic, so I was trying by induction, but both inductions on a and b lead me to useless implications. Anyone has a hint?

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:36):

induction on a

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:37):

after revert ha

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:37):

or prove it for succ a first by induction

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:37):

or cases a first to turn it into succ a and then start induction

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:38):

oh wait that doesn't work

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:39):

but that gives me ab + b = ac + c, given that ab = ac => b = c
From this we can get ab + b = ac + b => b = c -> ac + c = ac + b => b = c -> b = c => b = c which leads me to believe that the implication is useless

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:39):

I'm thinking about proving b < c implies a * b < a * c first

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:39):

I don't have ordering yet

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:40):

from the layout of the game, it shouldn't be needed

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:41):

It would be nice to be able to write "there is n such that b = c + n", but I can't really do that

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:41):

I can't even think of a maths proof without ordering

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 20:43):

Yeah this level trips everyone up

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:43):

ah, the hint (that I somehow skipped) is to start with revert b

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:43):

let me see where that leads me

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 20:46):

https://github.com/ImperialCollegeLondon/natural_number_game/issues/63

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:49):

Thanks!

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:52):

When I have g : ∀ (b : mynat), succ a * b + b = succ a * c + b → b = c, how do I say that it's true in particular for b = d?

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:53):

specialize g d

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:53):

have gd := g d

view this post on Zulip Kenny Lau (Apr 08 2020 at 20:54):

or just use g d in your next line

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:54):

Ah, have! Thanks

view this post on Zulip Patrick Massot (Apr 08 2020 at 20:54):

Kevin Buzzard said:

https://github.com/ImperialCollegeLondon/natural_number_game/issues/63

Don't forget to read the comments of that issue.

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 20:55):

Thanks Patrick -- I remember you told me that before but that was before I was using issues to organise the repo.

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 20:58):

Argh! I still can't figure it out, I'm running in circles!
I have:
g : ∀ (b : mynat), succ a * b + b = succ a * c + b → b = c, h : succ a * d + d = succ a * c + c,
trying to prove c = d

view this post on Zulip Patrick Massot (Apr 08 2020 at 21:00):

Valentin Tolmer said:

Argh! I still can't figure it out, I'm running in circles!

Welcome to mathematics!

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 21:01):

This level should come with a health warning.

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 21:02):

I want to prove it by embedding everything into Q\mathbb{Q} but I'm not 100% sure that I can do this rigorously because maybe the proof that Z\mathbb{Z} is an integral domain uses this? shrug

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 21:08):

from my hypotheses, I can turn my implication into d = c => d = c, which makes me think that the implication is useless here, in which case I'm missing something to solve the problem.

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 21:09):

The original revert b (or generalizing) doesn't seem to have helped

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 21:10):

Patrick Massot said:

Valentin Tolmer said:

Argh! I still can't figure it out, I'm running in circles!

Welcome to mathematics!

That's not my first bout with mathematics, or even with Peano, but somehow this specific problem eludes me! The rest came relatively easy :(

view this post on Zulip Patrick Massot (Apr 08 2020 at 21:11):

Sorry, my goal was not to imply you are ignorant, I only wanted to write something funny about mathematics.

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 21:13):

yeah, no worries, I was just lamenting on my fate... Any hint?

view this post on Zulip Patrick Massot (Apr 08 2020 at 21:14):

Sorry, I began Lean so long ago that I never went through the natural number game.

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 21:14):

After revert b, do induction on c.

view this post on Zulip Kenny Lau (Apr 08 2020 at 21:15):

ah, now that you say it I can instantly see why it works

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 21:16):

Welcome to mathematics!

view this post on Zulip Patrick Massot (Apr 08 2020 at 21:25):

Yes, that's definitely another aspect of mathematics.

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 21:52):

Finally did it! Probably in a somewhat roundabout way

view this post on Zulip Valentin Tolmer (Apr 08 2020 at 22:01):

Okay, I deserve to go to bed, it's midnight. Thank you for your gracious help, gentlemen (and ladies!)

view this post on Zulip Eric (Apr 08 2020 at 23:58):

Patrick Massot said:

Kevin Buzzard said:

https://github.com/ImperialCollegeLondon/natural_number_game/issues/63

Don't forget to read the comments of that issue.

sorry to bother, but what do you mean by this? how would you use generalizing? what does it do?

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:28):

Instead of revert a, induction b, intro a I think the idea is that you do induction b generalizing a. I've just checked this by looking at the induction docstring in VS Code and was going to link to the docs but apparently induction isn't in the docs?

view this post on Zulip Patrick Massot (Apr 09 2020 at 08:28):

It's a core tactic.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:28):

I know. So we don't document it in the API?

view this post on Zulip Patrick Massot (Apr 09 2020 at 08:28):

I think we should document it anyway.

view this post on Zulip Patrick Massot (Apr 09 2020 at 08:29):

It should be doable using the new command adding tactic documentation

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:29):

I've just clicked on the core tactics link in the docs and it sends me to ch6 of TPIL, which is great if you are trying to figure out the basics but I just wanted a link to the docstring.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:29):

Shall I open an issue?

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:30):

What's the core tactics link in the docs?

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:30):

I only say this because I've just been reading mathlib issues and PR's, I'm trying to get my head around the way the github site runs.

view this post on Zulip Patrick Massot (Apr 09 2020 at 08:30):

You should open a PR.

view this post on Zulip Patrick Massot (Apr 09 2020 at 08:30):

running https://leanprover-community.github.io/mathlib_docs/commands.html#add_tactic_doc

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:31):

I mean the link at the top of the page at
https://leanprover-community.github.io/mathlib_docs/tactics.html

Mathlib tactics

In addition to `the tactics found in the core library`, mathlib...

view this post on Zulip Patrick Massot (Apr 09 2020 at 08:31):

This documentation split is becoming more and more ridiculous now that mathlib has ten times more tactics than core.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:32):

Oh Patrick I can't open a PR, I don't understand anything about add_tactic_doc even if I read the docs

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:33):

In general, it's very easy to add docs for tactics in core. There's not a natural place for it right now but we could add one. For now, the bottom of https://github.com/leanprover-community/mathlib/blob/master/src/tactic/doc_commands.lean is probably right.

/-- write your doc entry here -/
add_tactic_doc
{ name := "induction",
  category := doc_category.tactic,
  decl_names := [`tactic.interactive.induction],
  tags := ["whatever fits"] }

view this post on Zulip Patrick Massot (Apr 09 2020 at 08:34):

@Kevin Buzzard :this:

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:34):

So I just manually choose all the tactics I think should be documented?

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:34):

It would be a reasonable idea to add a file, importing tactic.doc_command and imported by tactic.core, that just has a bunch of doc entries for tactics in the core repo.

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:35):

If the tactics have doc strings in core, you can even skip the /-- write your doc entry here -/ line, and the doc string will be used as the doc entry.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:35):

How do I test it?

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:35):

How do I list all tactics in core?

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:36):

Kevin Buzzard said:

So I just manually choose all the tactics I think should be documented?

Yep. The choices are, which tactics to document, how to name the doc entry (usually just the name of the tactic), and which tag/tags to give it.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:36):

Where can I see examples of tags for tactics?

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:36):

There's not a convenient way to test it right now, but if the add_tactic_doc command succeeds, you probably have it right.

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:36):

Kevin Buzzard said:

Where can I see examples of tags for tactics?

https://leanprover-community.github.io/mathlib_docs/tactics.html drop down menu on the left

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:37):

OK I'm on it

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:37):

These were added fairly recently and they're still evolving, so feel free to change tags as you see fit!

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:39):

There's a tag core for tactics from the core library. I was going to say it's kind of unnecessary. But actually, I think it's good to use, so people not using mathlib can see what tactics are available.

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:40):

Kevin Buzzard said:

How do I list all tactics in core?

For an overapproximation, run #print prefix tactic.interactive in a file that doesn't import anything. There's some junk in the list but all core tactics will appear.

view this post on Zulip Rob Lewis (Apr 09 2020 at 08:41):

If/when more of core is documented, we can change the intro to the tactic doc page.

view this post on Zulip Patrick Massot (Apr 09 2020 at 08:46):

Kevin, you can also look at https://leanprover.github.io/reference/tactics.html for a good selection.

view this post on Zulip Rob Lewis (Apr 09 2020 at 09:00):

One more note: doc entries and doc strings aren't always the same. But if you're writing doc entries that could also be doc strings, for tactics that don't have doc strings, you could make a PR adding the doc strings to core.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:01):

One thing that has always annoyed me about core docstrings is the ones like ac_refl which just says "an abbreviation for something else"

view this post on Zulip Rob Lewis (Apr 09 2020 at 09:01):

I'm sure changes to those would be very welcome!

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:02):

rw docstring is an abbreviation for rewrite

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:13):

Proof that core Lean is consistent:

example : false :=
begin
abstract,
ac_refl,
ac_reflexivity,
admit,
all_goals,
any_goals,
apply,
apply_auto_param,
apply_instance,
apply_opt_param,
apply_with,
assume,
assumption,
assumption',
async,
by_cases,
by_contra,
by_contradiction,
case,
cases,
cases_arg_p,
cases_core,
cases_matching,
cases_type,
casesm,
cc,
change,
clear,
comp_val,
concat_tags,
congr,
constructor,
constructor_matching,
contradiction,
conv,
delta,
destruct,
done,
dsimp,
dunfold,
eapply,
econstructor,
erewrite,
erw,
exact,
exacts,
exacts._main,
exfalso,
existsi,
existsi._main,
fail_if_success,
fapply,
focus,
from,
funext,
generalize,
get_rule_eqn_lemmas,
guard_expr_eq,
guard_hyp,
guard_target,
have,
induction,
injection,
injections,
intro,
intros,
introv,
iterate,
left,
let,
mapply,
match_target,
min_tac,
propagate_tags,
refine,
refl,
reflexivity,
rename,
repeat,
revert,
rewrite,
right,
rsimp,
rw,
rw_rule,
rw_rule.cases_on,
rw_rule.has_reflect,
rw_rule.mk,
rw_rule.mk.inj,
rw_rule.mk.inj_arrow,
rw_rule.no_confusion,
rw_rule.no_confusion_type,
rw_rule.pos,
rw_rule.rec,
rw_rule.rec_on,
rw_rule.rule,
rw_rule.symm,
rw_rule_p,
rw_rules,
rw_rules_t,
rw_rules_t.cases_on,
rw_rules_t.end_pos,
rw_rules_t.has_reflect,
rw_rules_t.mk,
rw_rules_t.mk.inj,
rw_rules_t.mk.inj_arrow,
rw_rules_t.no_confusion,
rw_rules_t.no_confusion_type,
rw_rules_t.rec,
rw_rules_t.rec_on,
rw_rules_t.rules,
rwa,
show,
simp,
simp_core,
simp_core_aux,
simp_intros,
skip,
solve1,
sorry,
specialize,
split,
subst,
subst_vars,
success_if_fail,
suffices,
symmetry,
to_expr',
trace,
trace_simp_set,
trace_state,
transitivity,
trivial,
try,
type_check,
unfold,
unfold1,
unfold_projs,
with_cases,
end

Nothing works.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:14):

Actually, admit and sorry both work :-)

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:20):

where's eblast, or did I dream that this was a core tactic?

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:21):

Note that not all of the core library is in init so Rob's procedure won't necessarily be a completely exhaustive list

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:21):

so my proof has a hole?

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:21):

we need an import core.all

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:22):

I am not capable of creating such a file but I would be very interested in having a complete list of tactics.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:22):

I thought that all of core was imported whenever I did anything at all.

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:22):

I think you could also improve the proof by wrapping each tactic in try

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:23):

If you omit prelude at the top of the file, this is equivalent to writing import init

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:24):

I think that if you went and deleted the init folder from core you could even make your own file init/default.lean and put whatever you wanted and that would get default imported

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:26):

This is all beyond me.

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:26):

but if "the core library" is defined as the contents of library/ in the lean repo, then there is more in there than just library/init/. For example there is stuff about vector and Gabriel's data.buffer.parser parser combinator library

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:26):

I know 0 about anything here. I just want some kind of a list of tactics.

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:26):

these are things that you have to still write import to get, but you don't need mathlib to do so

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:27):

Oh I see, I looked it up and eblast is an smt_tactic

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:27):

that's a whole story right there

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:28):

you should also dump #print prefix smt_tactic.interactive to see these tactics

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:29):

Do we want those documented in the API docs?

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:30):

they get used inside begin [smt_tactic] end blocks

view this post on Zulip Patrick Massot (Apr 09 2020 at 09:30):

Kevin, you didn't read https://github.com/leanprover-community/mathlib/pull/2337 carefully enough.

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:30):

If the goal is maximum coverage of core I think the smt interactive mode is also important

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:30):

even though I have epsilon experience with it

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:31):

I know that eblast is @Jesse Michael Han 's favorite tactic

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:31):

it's kind of like finish

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:32):

Patrick I did read tools.md -- are you referring to something else?

view this post on Zulip Patrick Massot (Apr 09 2020 at 09:33):

No. But init is mentioned there.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 09:33):

oh, fair enough

view this post on Zulip Patrick Massot (Apr 09 2020 at 09:33):

Maybe I should explicitly point out the existence of other files in the code library

view this post on Zulip Rob Lewis (Apr 09 2020 at 09:44):

Mario Carneiro said:

Note that not all of the core library is in init so Rob's procedure won't necessarily be a completely exhaustive list

I see two tactics in the smt directory that aren't used, otherwise pretty sure all the tactics in core are in init.

view this post on Zulip Rob Lewis (Apr 09 2020 at 09:45):

If we document the smt mode stuff, it probably belongs in a separate doc file, like the commands and attributes. Right?

view this post on Zulip Rob Lewis (Apr 09 2020 at 09:45):

Then we can explain what smt mode is in the header.

view this post on Zulip Mario Carneiro (Apr 09 2020 at 09:49):

It should be in a separate file, but the main file should make sure to note somewhere that the other file exists


Last updated: May 09 2021 at 11:09 UTC