# Zulip Chat Archive

## Stream: lean4

### Topic: elab goals for concrete arith

#### Daniel Selsam (Apr 05 2021 at 16:26):

I have experimented with formalizing olympiad problem statements on top of the mathport `.olean`

files, and have found that elaborating concrete arithmetic expressions is the biggest pain point by far. The issues might be solvable by removing the `outParam`

annotation on the result types for the heterogeneous operators, or perhaps they will require a custom elaborator to solve. But before thinking too deeply about fixes, I thought it would be best to work out a spec of what idioms are critical to support. Here is a very preliminary proposal: https://gist.github.com/dselsam/4fbc7234db7fd4349ffa940bafd6edda Currently, only a few of the examples in the gist work. Thoughts? Missing idioms of import?

#### Mario Carneiro (Apr 05 2021 at 18:06):

```
-- There should be no subtraction on ℕ
#check (n - 1 : ℕ) -- (should fail)
#check (n - n₁ : ℕ) -- (should fail)
```

This seems... disruptive

#### Mario Carneiro (Apr 05 2021 at 18:07):

Could you mark all of the examples with an indication of whether they fail or not?

#### Mario Carneiro (Apr 05 2021 at 18:08):

alternatively, could you post a version that works without mathlib (using stubbed out instances and such)

#### Daniel Selsam (Apr 05 2021 at 18:14):

I added "fails" annotations to the gist for now. I can post a no-mathlib version this evening.

#### Mario Carneiro (Apr 05 2021 at 18:26):

Here's a list of examples that fail at least one of lean 3 and lean 4. I guess we should focus on the "fails in lean 4, not lean 3" ones; many of the "fails both" are because the relevant instance doesn't exist in mathlib

```
-- Adding with one-side coercion on the left, no expected type
#check n + z -- ℤ -- fails both
#check n + q -- ℚ -- fails both
#check n + x -- ℝ -- fails both
-- Raising to same-type powers (no expected type)
#check z^z -- fails both
#check q^q -- fails both
-- Raising numerals to powers (no expected type)
#check 2^z -- fails both
#check 2^q -- fails both
#check 2^x -- fails in lean 3, not lean 4
-- Raising nats to powers (no expected type)
#check k^z -- fails both
#check k^q -- fails both
#check k^x -- fails both
-- Dividing by numerals (with expected type ≥ ℚ)
-- TODO: different notation for nat-div and rat/real-div? (or just no notation for nat.div)
#check (n / 2 : ℚ) -- fails in lean 4, not lean 3
#check (n / 2 : ℝ) -- fails in lean 4, not lean 3
#check (z / 2 : ℚ) -- fails in lean 4, not lean 3
#check (z / 2 : ℝ) -- fails in lean 4, not lean 3
#check (q / 2 : ℝ) -- fails in lean 4, not lean 3
#check (x / 2 : ℚ) -- fails both
-- Dividing by nats (with expected type ≥ ℚ)
#check (n / k : ℚ) -- fails in lean 4, not lean 3
#check (n / k : ℝ) -- fails in lean 4, not lean 3
#check (z / k : ℚ) -- fails in lean 4, not lean 3
#check (z / k : ℝ) -- fails in lean 4, not lean 3
#check (q / k : ℝ) -- fails in lean 4, not lean 3
#check (x / k : ℚ) -- fails both
-- II. Polynomials
open polynomial (C X)
-- Constants should work with coerced expected type
#check (C n : polynomial ℤ) -- fails in lean 3, not lean 4
#check (C n : polynomial ℝ) -- fails in lean 3, not lean 4
#check (C z : polynomial ℂ) -- fails in lean 3, not lean 4
-- Variables to numeral powers should work with expected type
#check (X^2 : polynomial ℂ) -- fails in lean 4, not lean 3
-- Variables to nat powers should work with expected type
#check (X^k : polynomial ℂ) -- fails in lean 4, not lean 3
-- Standard-form polynomials should work with regular expected type
#check (X^2 + C x₁ * X + C x₂ : polynomial ℝ) -- fails in lean 4, not lean 3
-- Standard-form polynomials should work with coerced expected type
#check (X^2 + C x₁ * X + C x₂ : polynomial ℂ) -- fails both
-- Standard-form polynomials should work without expected type
#check X^2 + C x₁ * X + C x₂ -- fails in lean 4, not lean 3
-- Standard-form polynomials should work with coerced constants without expected type
#check X^2 + C n * X + C x -- fails both
```

#### Mario Carneiro (Apr 05 2021 at 18:27):

Based on the failure patterns, it seems like lean 4 is using a different order for deciding where to insert coercion arrows

#### Mario Carneiro (Apr 05 2021 at 18:28):

I thought this issue was fixed?

```
#check n + z -- ℤ -- fails both
```

#### Daniel Selsam (Apr 06 2021 at 00:17):

Here is a version that does not depend on mathlib: https://gist.github.com/dselsam/98f8febef01cca03a41d2dafcc876bba (fail annotations refer to e863376be1552562d0d7ee9c7f13fd5a2d51d9e0)

#### Daniel Selsam (Apr 06 2021 at 00:39):

Mario Carneiro said:

I thought this issue was fixed?

`#check n + z -- ℤ -- fails both`

It is fixed, and works in the gist I just posted that does not depend on mathlib. They failed in the original version that imports all of mathlib due to `Coe`

synth queries timing out.

Last updated: May 07 2021 at 12:15 UTC