Zulip Chat Archive

Stream: maths

Topic: mul_left_cancel


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?

Kenny Lau (Apr 08 2020 at 20:36):

induction on a

Kenny Lau (Apr 08 2020 at 20:37):

after revert ha

Kenny Lau (Apr 08 2020 at 20:37):

or prove it for succ a first by induction

Kenny Lau (Apr 08 2020 at 20:37):

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

Kenny Lau (Apr 08 2020 at 20:38):

oh wait that doesn't work

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

Kenny Lau (Apr 08 2020 at 20:39):

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

Valentin Tolmer (Apr 08 2020 at 20:39):

I don't have ordering yet

Valentin Tolmer (Apr 08 2020 at 20:40):

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

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

Kenny Lau (Apr 08 2020 at 20:41):

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

Kevin Buzzard (Apr 08 2020 at 20:43):

Yeah this level trips everyone up

Valentin Tolmer (Apr 08 2020 at 20:43):

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

Valentin Tolmer (Apr 08 2020 at 20:43):

let me see where that leads me

Kevin Buzzard (Apr 08 2020 at 20:46):

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

Valentin Tolmer (Apr 08 2020 at 20:49):

Thanks!

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?

Kenny Lau (Apr 08 2020 at 20:53):

specialize g d

Kenny Lau (Apr 08 2020 at 20:53):

have gd := g d

Kenny Lau (Apr 08 2020 at 20:54):

or just use g d in your next line

Valentin Tolmer (Apr 08 2020 at 20:54):

Ah, have! Thanks

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.

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.

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

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!

Kevin Buzzard (Apr 08 2020 at 21:01):

This level should come with a health warning.

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

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.

Valentin Tolmer (Apr 08 2020 at 21:09):

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

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 :(

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.

Valentin Tolmer (Apr 08 2020 at 21:13):

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

Patrick Massot (Apr 08 2020 at 21:14):

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

Kevin Buzzard (Apr 08 2020 at 21:14):

After revert b, do induction on c.

Kenny Lau (Apr 08 2020 at 21:15):

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

Kevin Buzzard (Apr 08 2020 at 21:16):

Welcome to mathematics!

Patrick Massot (Apr 08 2020 at 21:25):

Yes, that's definitely another aspect of mathematics.

Valentin Tolmer (Apr 08 2020 at 21:52):

Finally did it! Probably in a somewhat roundabout way

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!)

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?

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?

Patrick Massot (Apr 09 2020 at 08:28):

It's a core tactic.

Kevin Buzzard (Apr 09 2020 at 08:28):

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

Patrick Massot (Apr 09 2020 at 08:28):

I think we should document it anyway.

Patrick Massot (Apr 09 2020 at 08:29):

It should be doable using the new command adding tactic documentation

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.

Kevin Buzzard (Apr 09 2020 at 08:29):

Shall I open an issue?

Rob Lewis (Apr 09 2020 at 08:30):

What's the core tactics link in the docs?

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.

Patrick Massot (Apr 09 2020 at 08:30):

You should open a PR.

Patrick Massot (Apr 09 2020 at 08:30):

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

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...

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.

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

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"] }

Patrick Massot (Apr 09 2020 at 08:34):

@Kevin Buzzard :this:

Kevin Buzzard (Apr 09 2020 at 08:34):

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

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.

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.

Kevin Buzzard (Apr 09 2020 at 08:35):

How do I test it?

Kevin Buzzard (Apr 09 2020 at 08:35):

How do I list all tactics in core?

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.

Kevin Buzzard (Apr 09 2020 at 08:36):

Where can I see examples of tags for tactics?

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.

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

Kevin Buzzard (Apr 09 2020 at 08:37):

OK I'm on it

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!

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.

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.

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.

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.

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.

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"

Rob Lewis (Apr 09 2020 at 09:01):

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

Kevin Buzzard (Apr 09 2020 at 09:02):

rw docstring is an abbreviation for rewrite

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.

Kevin Buzzard (Apr 09 2020 at 09:14):

Actually, admit and sorry both work :-)

Mario Carneiro (Apr 09 2020 at 09:20):

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

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

Kevin Buzzard (Apr 09 2020 at 09:21):

so my proof has a hole?

Mario Carneiro (Apr 09 2020 at 09:21):

we need an import core.all

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.

Kevin Buzzard (Apr 09 2020 at 09:22):

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

Mario Carneiro (Apr 09 2020 at 09:22):

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

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

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

Kevin Buzzard (Apr 09 2020 at 09:26):

This is all beyond me.

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

Kevin Buzzard (Apr 09 2020 at 09:26):

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

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

Mario Carneiro (Apr 09 2020 at 09:27):

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

Mario Carneiro (Apr 09 2020 at 09:27):

that's a whole story right there

Mario Carneiro (Apr 09 2020 at 09:28):

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

Kevin Buzzard (Apr 09 2020 at 09:29):

Do we want those documented in the API docs?

Mario Carneiro (Apr 09 2020 at 09:30):

they get used inside begin [smt_tactic] end blocks

Patrick Massot (Apr 09 2020 at 09:30):

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

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

Mario Carneiro (Apr 09 2020 at 09:30):

even though I have epsilon experience with it

Mario Carneiro (Apr 09 2020 at 09:31):

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

Mario Carneiro (Apr 09 2020 at 09:31):

it's kind of like finish

Kevin Buzzard (Apr 09 2020 at 09:32):

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

Patrick Massot (Apr 09 2020 at 09:33):

No. But init is mentioned there.

Kevin Buzzard (Apr 09 2020 at 09:33):

oh, fair enough

Patrick Massot (Apr 09 2020 at 09:33):

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

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.

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?

Rob Lewis (Apr 09 2020 at 09:45):

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

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: Dec 20 2023 at 11:08 UTC