mul_left_cancel

Stream: maths

[Valentin Tolmer]

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]

induction on a

[Kenny Lau]

after revert ha

[Kenny Lau]

or prove it for succ a first by induction

[Kenny Lau]

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

[Kenny Lau]

oh wait that doesn't work

[Valentin Tolmer]

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]

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

[Valentin Tolmer]

I don't have ordering yet

[Valentin Tolmer]

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

[Valentin Tolmer]

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]

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

[Kevin Buzzard]

Yeah this level trips everyone up

[Valentin Tolmer]

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

[Valentin Tolmer]

let me see where that leads me

[Kevin Buzzard]

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

[Valentin Tolmer]

Thanks!

[Valentin Tolmer]

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]

specialize g d

[Kenny Lau]

have gd := g d

[Kenny Lau]

or just use g d in your next line

[Valentin Tolmer]

Ah, have! Thanks

[Patrick Massot]

Kevin Buzzard said:

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

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

[Kevin Buzzard]

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

[Valentin Tolmer]

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]

Valentin Tolmer said:

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

Welcome to mathematics!

[Kevin Buzzard]

This level should come with a health warning.

[Kevin Buzzard]

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

[Valentin Tolmer]

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]

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

[Valentin Tolmer]

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]

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

[Valentin Tolmer]

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

[Patrick Massot]

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

[Kevin Buzzard]

After revert b, do induction on c.

[Kenny Lau]

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

[Kevin Buzzard]

Welcome to mathematics!

[Patrick Massot]

Yes, that's definitely another aspect of mathematics.

[Valentin Tolmer]

Finally did it! Probably in a somewhat roundabout way

[Valentin Tolmer]

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

[Eric]

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]

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]

It's a core tactic.

[Kevin Buzzard]

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

[Patrick Massot]

I think we should document it anyway.

[Patrick Massot]

It should be doable using the new command adding tactic documentation

[Kevin Buzzard]

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]

Shall I open an issue?

[Rob Lewis]

What's the core tactics link in the docs?

[Kevin Buzzard]

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]

You should open a PR.

[Patrick Massot]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

@Kevin Buzzard :this:

[Kevin Buzzard]

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

[Rob Lewis]

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]

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]

How do I test it?

[Kevin Buzzard]

How do I list all tactics in core?

[Rob Lewis]

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]

Where can I see examples of tags for tactics?

[Rob Lewis]

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]

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]

OK I'm on it

[Rob Lewis]

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

[Rob Lewis]

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]

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]

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

[Patrick Massot]

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

[Rob Lewis]

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]

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]

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

[Kevin Buzzard]

rw docstring is an abbreviation for rewrite

[Kevin Buzzard]

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]

Actually, admit and sorry both work :-)

[Mario Carneiro]

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

[Mario Carneiro]

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]

so my proof has a hole?

[Mario Carneiro]

we need an import core.all

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

This is all beyond me.

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

that's a whole story right there

[Mario Carneiro]

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

[Kevin Buzzard]

Do we want those documented in the API docs?

[Mario Carneiro]

they get used inside begin [smt_tactic] end blocks

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

even though I have epsilon experience with it

[Mario Carneiro]

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

[Mario Carneiro]

it's kind of like finish

[Kevin Buzzard]

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

[Patrick Massot]

No. But init is mentioned there.

[Kevin Buzzard]

oh, fair enough

[Patrick Massot]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Mario Carneiro]

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