fix(tactic/omega): reify non-constant ints and nats

[skbaek]

Make omega treat any non-constant integers and natural numbers as variables

[robertylewis]

@skbaek thanks! Does this address both of the new bug reports in #1484 or only the one? If both, could you add the second as a test?

The Travis failure is because of missing documentation. Since this is a big refactor and omega is grandfathered in, I won't insist on you documenting the whole thing (although that would be wonderful, and would make it easier for me to make these kinds of fixes myself). Instead, you can add doc strings to as many declarations as you're willing. Focus on ones that are important or confusing. Then, run mk_nolint.lean in the scripts directory to regenerate nolints.txt. (You'll need to build all oleans and run scripts/mk_all.sh first.)

[bryangingechen]

I've changed the PR name to "fix(tactic/omega)", assuming that "tactic/ring" is a typo.

[skbaek]

@bryangingechen Right, I was copying and pasting the PR format and forgot to change that, thanks.

[skbaek]

@robertylewis I added the fintype example and it's working for both that and the list.length example, if that's what you meant by the two new reports. I've added some comments for the parts modified in this PR, but there are many more to go according to the nolints.txt generated. Is there a way to tell which of these omissions are critical and making Travis fail?

[cipher1024]

Docstring syntax is /-- ... -/

[robertylewis]

@robertylewis I added the fintype example and it's working for both that and the list.length example, if that's what you meant by the two new reports.

Yep, that's what I meant, thanks!

I've added some comments for the parts modified in this PR, but there are many more to go according to the nolints.txt generated. Is there a way to tell which of these omissions are critical and making Travis fail?

Travis will fail if there is any declaration named d such that (1) d is a def, (2) d is missing a doc string, and (3) no definition named d existed before this PR. Because this PR renames a bunch of things, they appear to be new declarations to Travis.

You should do the following:

• Change your existing doc strings to use /-- ... -/ instead of /- ... -/, as Simon points out.
• Add doc strings to as many definitions as you're willing. For auxiliary definitions or things that are very clearly internal, you could mark them private instead. (Doc strings are preferable, since marking them private doesn't help others to maintain your code, but it at least keeps them out of the doc generation and tab-complete search.)
• It looks like your latest commit deletes nolints.txt from the repository? Revert that, it needs to stay.
• Update the PR to be based on the head commit to master.
• Regenerate nolints.txt. This should remove the declaration names that no longer exist, and add the ones that are missing doc strings.
• Commit the changes to nolints.txt.

[robertylewis]

If you do the first two steps, I'm happy to take care of the rest.

[sgouezel]

We've just been discussing this PR in a maintainers' meeting. We all think it is a very important and useful PR, but unfortunately none of us is able to add the missing documentation as we don't really understand the tactic. Do you think you could add the documentation, and then we'll be happy to take care of the rest?

[sgouezel]

I think a lot of documentation is still missing: the linter output of travis gives

-- tactic/omega/nat/sub_elim.lean

#print omega.nat.preform.sub_terms /- def missing doc string -/

#print omega.nat.preform.sub_subst /- def missing doc string -/

-- tactic/omega/nat/main.lean

#print omega.nat.to_exprterm /- def missing doc string -/

#print omega.nat.exprterm.to_preterm /- def missing doc string -/

#print omega.nat.wff /- def missing doc string -/

#print omega.nat.to_exprform /- def missing doc string -/

#print omega.nat.prove /- def missing doc string -/

#print omega.nat.exprform.to_preform /- def missing doc string -/

#print omega.nat.exprform.exprs /- def missing doc string -/

#print omega.nat.wfx /- def missing doc string -/

#print omega.nat.intro_nats_core /- def missing doc string -/

#print omega.nat.intro_nats /- def missing doc string -/

#print omega.nat.eq_nat /- def missing doc string -/

#print omega.nat.exprterm.exprs /- def missing doc string -/

#print omega.nat.to_preform /- def missing doc string -/

-- tactic/omega/nat/form.lean

#print omega.nat.preform.repr /- def missing doc string -/

#print omega.nat.preform.sub_free /- def missing doc string -/

#print omega.nat.preform /- constant missing doc string -/

#print omega.nat.preform.fresh_index /- def missing doc string -/

#print omega.nat.preform.implies /- def missing doc string -/

#print omega.nat.preform.sat /- def missing doc string -/

#print omega.nat.exprform /- constant missing doc string -/

#print omega.nat.preform.valid /- def missing doc string -/

#print omega.nat.preform.unsat /- def missing doc string -/

#print omega.nat.preform.equiv /- def missing doc string -/

#print omega.nat.preform.neg_free /- def missing doc string -/

-- tactic/omega/misc.lean

#print omega.app_first /- def missing doc string -/

#print omega.intro_fresh /- def missing doc string -/

-- tactic/omega/main.lean

#print omega.determine_domain /- def missing doc string -/

-- tactic/omega/int/main.lean

#print omega.int.exprform.to_preform /- def missing doc string -/

#print omega.int.to_exprterm /- def missing doc string -/

#print omega.int.eq_int /- def missing doc string -/

#print omega.int.intro_ints_core /- def missing doc string -/

#print omega.int.prove /- def missing doc string -/

#print omega.int.to_exprform /- def missing doc string -/

#print omega.int.exprterm.exprs /- def missing doc string -/

#print omega.int.wfx /- def missing doc string -/

#print omega.int.intro_ints /- def missing doc string -/

#print omega.int.exprterm.to_preterm /- def missing doc string -/

#print omega.int.wff /- def missing doc string -/

#print omega.int.exprform.exprs /- def missing doc string -/

#print omega.int.to_preform /- def missing doc string -/

-- tactic/omega/int/form.lean

#print omega.int.preform.sat /- def missing doc string -/

#print omega.int.preform.holds /- def missing doc string -/

#print omega.int.preform.implies /- def missing doc string -/

#print omega.int.preform.unsat /- def missing doc string -/

#print omega.int.exprform /- constant missing doc string -/

#print omega.int.preform.equiv /- def missing doc string -/

#print omega.int.preform /- constant missing doc string -/

#print omega.int.preform.valid /- def missing doc string -/

#print omega.int.preform.repr /- def missing doc string -/

#print omega.int.preform.fresh_index /- def missing doc string -/

[robertylewis]

@skbaek Do you know if or when you'll have time to return to this?

[skbaek]

@robertylewis I made a PR but realized I was working on the wrong branch and closed it. I'll move the docs here

[robertylewis]

@skbaek It looks like there was a problem with the merge. The git history here is pretty complicated, maybe you can rebase only the relevant (non-merge) commits onto master? I hope there wouldn't be too many conflicts since omega hasn't been changed much.

[robertylewis]

Oh, I see there are some conflicts with derived instances added in #1898 that will complicate things.

[robertylewis]

@skbaek : @fpvandoorn made an attempt to extract the intended changes from this PR, https://github.com/leanprover-community/mathlib/tree/seul_omega

We're not sure if it's exactly right. An example is failing that worked with the old omega:

example (k : ℕ) : ¬1 + (1 + 2 * 2) = k * 2 ∨ k = 3 :=
by omega

A little debugging turns up

example (k : ℕ) : ¬1 + (1 + 2 * 2) = k * 2 ∨ k = 3 :=
by do desugar, preprocess, e ← target >>= to_preform, trace e, skip

which traces (¬((1 + (1 + 2*x0)) = 2*x1) ∨ (1*x1 = 3)). to_preform seems to treat one of the 2s in 2*2 as a variable. Indeed, https://github.com/leanprover-community/mathlib/blob/seul_omega/src/tactic/omega/nat/main.lean#L116 looks fishy to me, but I'm surprised it produces 2*x0 instead of x0*2.

[fpvandoorn]

It is very possible that it is because of a bad resolution of a merge conflict. I didn't know the code, but hopefully @skbaek can figure out what went wrong.

[skbaek]

@robertylewis I've rebased the commits to master. I think the commit history should be more manageable now.

As for the failing example, omega supports multiplication only in limited ways. Right now the shadow syntax can only encode multiplication for terms of the form k * x, where k is a constant and x is a variable. I'm a bit surprised that this example used to work before - I'll look into the previous version of omega to see what happened.

[robertylewis]

@skbaek I'm afraid this is still reverting changes made to master since the original PR. For instance, a number of @[derive inhabited] attributes were added in #1898 that your PR is removing.

I suppose the failing example would work with a call to norm_num first. Morally, this kind of thing feels like it should be within the scope of omega, but I'd rather get this merged before more conflicts arise than wait for a fix.

[sgouezel]

Could we try to get this merged? As far as I understand, the example that is now failing has never been really in the scope of omega, so the success in the first version was more of a coincidence, so this shouldn't be counted as a regression.

[sgouezel]

I have added various fixes and cleanups in a branch sgouezel_my_omega (based on current master, restoring the missing inhabited instances, fixing the failing proof and some typos).

[robertylewis]

@sgouezel Your branch is accepted if it passes CI. I'll merge it into this PR (if I have permissions) so that @skbaek gets the commit credit.

[sgouezel]

My branch didn't pass the linter, since there are still a few missing docstrings. Way less than in the first PRs, but still...

/- DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- tactic/omega/int/form.lean
#print omega.int.preform.repr /- def missing doc string -/

-- tactic/omega/int/main.lean
#print simp_attr.sugar /- def missing doc string -/
#print omega.int.intro_ints /- def missing doc string -/

-- tactic/omega/nat/form.lean
#print omega.nat.preform.repr /- def missing doc string -/

-- tactic/omega/nat/main.lean
#print simp_attr.sugar_nat /- def missing doc string -/
#print omega.nat.intro_nats /- def missing doc string -/

Do you want to merge it anyway (and update nolint.txt), saying that this is already a big improvement over the previous situation? Or would you rather wait for the missing docstrings?

[robertylewis]

Closed with 19a9bdc. I did the squash and merge manually so that @skbaek would get the author credit. Thanks Sebastien for the cleanup!