Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

to_additive fails for integer literals #4210

Closed
eric-wieser opened this issue Sep 22, 2020 · 3 comments
Closed

to_additive fails for integer literals #4210

eric-wieser opened this issue Sep 22, 2020 · 3 comments
Labels
t-meta Tactics, attributes or user commands

Comments

@eric-wieser
Copy link
Member

eric-wieser commented Sep 22, 2020 •
edited

I'm not sure what's going on here, but

import algebra.group.to_additive
@[to_additive]
def nat_one : ℕ := 1

fails with

type mismatch at application
  0
term
  nat.has_one
has type
  has_one ℕ
but is expected to have type
  has_zero ℕ
@urkud
Copy link
Member

urkud commented Sep 23, 2020

The problem here is that to_additive tries to replace each has_one with has_zero, and this shouldn't be done for nat and several other types. A proper fix is to add a list of "ignored" types (at least nat, int, equiv.perm, probably some End/Aut types) and rewrite the code in tactic/transform_decl to leave a function application unchanged if one of the arguments is in the list of "ignored" types.

@fpvandoorn fpvandoorn added the t-meta Tactics, attributes or user commands label Oct 20, 2020
@fpvandoorn
Copy link
Member

fpvandoorn commented Jan 7, 2021 •
edited

One possible check we can do (which is a hack): if the first argument of a constant is another constant (not applied to any arguments), then we don't replace it.

The assumption is that the first argument is always the type in question, and if that is another fixed (i.e. an expr.const) type, then it's probably a type like nat, int, real, ennreal, which we cannot additivize.

If the first argument is something applied to arguments, it could be something like prod G H, which we can additivize.

This does not take care of equiv.perm in @urkud's suggestion.

@fpvandoorn fpvandoorn mentioned this issue Jan 8, 2021
Closed
2 tasks
@fpvandoorn
Copy link
Member

fpvandoorn commented Jan 8, 2021 •
edited

Related Zulip threads:

bors bot pushed a commit that referenced this issue Jan 16, 2021
@fpvandoorn
feat(measure_theory/haar_measure): Prove uniqueness (#5663)
787e6b3 
Prove the uniqueness of Haar measure (up to a scalar) following  *Measure Theory* by Paul Halmos. This proof seems to contain an omission which we fix by adding an extra hypothesis to an intermediate lemma.
Add some lemmas about left invariant regular measures.
We add the file `measure_theory.prod_group` which contain various measure-theoretic properties of products of topological groups, needed for the uniqueness.
We add `@[to_additive]` to some declarations in `measure_theory`, but leave it out for many because of #4210. This causes some renamings in concepts, like `is_left_invariant` -> `is_mul_left_invariant` and `measure.conj` -> `measure.inv` (though a better naming suggestion for this one is welcome).
@fpvandoorn fpvandoorn mentioned this issue Jun 1, 2021
Closed
bors bot pushed a commit that referenced this issue Jun 15, 2021
@fpvandoorn
feat(algebra/to_additive): do not additivize operations on constant t…
bc6dec0 
…ypes (#7792)

* Fixes #4210
* Adds a heuristic to `@[to_additive]` that decides which multiplicative identifiers to replace with their additive counterparts. 
* See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_additive.20and.20fixed.20types) thread or documentation for the precise heuristic.
* We tag some types with `@[to_additive]`, so that they are handled correctly by the heurstic. These types `pempty`, `empty`, `unit` and `punit`.
* We make the following change to enable to above bullet point: you are allowed to translate a declaration to itself, only if you write its name again as argument of the attribute (if you don't specify an argument we want to raise an error, since that likely is a mistake).
* Because of this heuristic, all declarations with the `@[to_additive]` attribute should have a type with a multiplicative structure on it as its first argument. The first argument should not be an arbitrary indexing type. This means that in `finset.prod` and `finprod` we reorder the first two (implicit) arguments, so that the first argument is the codomain of the function.
* This will eliminate many (but not all) type mismatches generated by `@[to_additive]`.
* This heuristic doesn't catch all cases: for example, the declaration could have two type arguments with multiplicative structure, and the second one is `ℕ`, but the first one is a variable.



Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
@bors bors bot closed this as completed in 2c749b1 Jun 29, 2021
b-mehta pushed a commit that referenced this issue Jul 6, 2021
@fpvandoorn @b-mehta
feat(algebra/to_additive): do not additivize operations on constant t…
0e79074 
…ypes (#7792)

* Fixes #4210
* Adds a heuristic to `@[to_additive]` that decides which multiplicative identifiers to replace with their additive counterparts. 
* See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_additive.20and.20fixed.20types) thread or documentation for the precise heuristic.
* We tag some types with `@[to_additive]`, so that they are handled correctly by the heurstic. These types `pempty`, `empty`, `unit` and `punit`.
* We make the following change to enable to above bullet point: you are allowed to translate a declaration to itself, only if you write its name again as argument of the attribute (if you don't specify an argument we want to raise an error, since that likely is a mistake).
* Because of this heuristic, all declarations with the `@[to_additive]` attribute should have a type with a multiplicative structure on it as its first argument. The first argument should not be an arbitrary indexing type. This means that in `finset.prod` and `finprod` we reorder the first two (implicit) arguments, so that the first argument is the codomain of the function.
* This will eliminate many (but not all) type mismatches generated by `@[to_additive]`.
* This heuristic doesn't catch all cases: for example, the declaration could have two type arguments with multiplicative structure, and the second one is `ℕ`, but the first one is a variable.



Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
3 participants
@urkud @eric-wieser @fpvandoorn