elab goals for concrete arith

Stream: lean4

[Daniel Selsam]

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]

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

This seems... disruptive

[Mario Carneiro]

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

[Mario Carneiro]

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

[Daniel Selsam]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

I thought this issue was fixed?

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

[Daniel Selsam]

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

[Daniel Selsam]

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.