Elaboration goals for concrete arithmetic

ElabArithGoals.lean

import Mathlib.all
import PostPort

namespace ElabArithGoals

open Mathlib hiding coe

variable (k k₁ k₂ k₃ : ℕ)
variable (n n₁ n₂ n₃ : ℕ)
variable (z z₁ z₂ z₃ : ℤ)
variable (q q₁ q₂ q₃ : ℚ)
variable (x x₁ x₂ x₃ : ℝ)
variable (y y₁ y₂ y₃ : ℂ)

-- Coercing individual terms
#check (n : ℤ)
#check (n : ℚ)
#check (n : ℝ)
#check (z : ℚ)
#check (z : ℝ)
#check (q : ℝ)

-- Adding with one-side coercion on the left, no expected type
#check n + z -- ℤ -- fails
#check n + q -- ℚ -- fails
#check n + x -- ℝ -- fails

-- Adding with one-side coercion on the right, no expected type
#check z + n -- ℤ
#check q + n -- ℚ
#check x + n -- ℝ

-- Adding with one-side coercion on the left, regular expected type
#check (n + z : ℤ) -- fails
#check (n + q : ℚ) -- fails
#check (n + x : ℝ) -- fails

-- Adding with one-side coercion on the right, regular expected type
#check (z + n : ℤ)
#check (q + n : ℚ)
#check (q + z : ℚ)
#check (x + n : ℝ)

-- Adding same type with coerced expected type
#check (n₁ + n₂ : ℤ) -- fails
#check (n₁ + n₂ : ℚ) -- fails
#check (n₁ + n₂ : ℝ) -- fails
#check (z₁ + z₂ : ℚ) -- fails
#check (z₁ + z₂ : ℝ) -- fails
#check (q₁ + q₂ : ℝ) -- fails

-- Adding with one-side coercion on the right, coerced expected type
#check (z + n : ℚ) -- fails
#check (z + n : ℝ) -- fails
#check (q + n : ℝ) -- fails

-- Adding with one-side coercion on the left, coerced expected type
#check (n + z : ℚ) -- fails
#check (n + z : ℝ) -- fails
#check (n + q : ℝ) -- fails

-- Adding numerals on the right, no expected type
#check n + 1
#check z + 1
#check q + 1
#check x + 1

-- Adding numerals on the left, no expected type
#check 1 + n
#check 1 + z
#check 1 + q
#check 1 + x

-- Adding numerals on the right, regular expected type
#check (n + 1 : ℕ)
#check (z + 1 : ℤ)
#check (q + 1 : ℚ)
#check (x + 1 : ℝ)

-- Adding numerals on the right, regular expected type
#check (1 + n : ℕ)
#check (1 + z : ℤ)
#check (1 + q : ℚ)
#check (1 + x : ℝ)

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

-- Subtracting numerals should coerce them at least to ℤ (without expected type)
#check n - 1  -- (should have type ℤ but has type ℕ)
#check z - 1
#check q - 1
#check x - 1

-- Subtracting nats should coerce them to at least to ℤ (without expected type)
#check n - n₁ -- (should have type ℤ but has type ℕ)
#check z - n₁
#check q - n₁
#check x - n₁

-- Raising to numeral powers (no expected type)
-- TODO: are there (or should there be) special int-power instances?
#check n^2
#check z^2 -- fails
#check q^2 -- fails
#check x^2

-- Raising to natural powers (no expected type)
#check n^k
#check z^k
#check q^k
#check x^k

-- Raising to same-type powers (no expected type)
#check n^n
#check z^z -- fails
#check q^q -- fails
#check x^x

-- Raising numerals to powers (no expected type)
#check 2^n
#check 2^z -- fails
#check 2^q -- fails
#check 2^x

-- Raising nats to powers (no expected type)
#check k^n
#check k^z -- fails
#check k^q -- fails
#check k^x -- fails

-- 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
#check (n / 2 : ℝ) -- fails
#check (z / 2 : ℚ) -- fails
#check (z / 2 : ℝ) -- fails
#check (q / 2 : ℚ)
#check (q / 2 : ℝ) -- fails
#check (x / 2 : ℚ) -- fails

-- Dividing by nats (with expected type ≥ ℚ)
#check (n / k : ℚ) -- fails
#check (n / k : ℝ) -- fails
#check (z / k : ℚ) -- fails
#check (z / k : ℝ) -- fails
#check (q / k : ℚ)
#check (q / k : ℝ) -- fails
#check (x / k : ℚ) -- fails

-- II. Polynomials
open Mathlib.polynomial (C X)

-- Variables should work with expected type
#check (X : polynomial ℝ)
#check (X : polynomial ℂ)

-- Constants should work without expected type
#check C n
#check C z
#check C q
#check C x

-- Constants should work with coerced expected type
#check (C n : polynomial ℤ)
#check (C n : polynomial ℝ)
#check (C z : polynomial ℂ)

-- Adding constants and variables should work without expected type
#check C x + X
#check X + C x

-- Variables to numeral powers should work with expected type
#check (X^2 : polynomial ℂ) -- fails

-- Variables to nat powers should work with expected type
#check (X^k : polynomial ℂ) -- fails

-- Standard-form polynomials should work with regular expected type
#check (X^2 + C x₁ * X + C x₂ : polynomial ℝ) -- fails

-- Standard-form polynomials should work with coerced expected type
#check (X^2 + C x₁ * X + C x₂ : polynomial ℂ) -- fails

-- Standard-form polynomials should work without expected type
#check X^2 + C x₁ * X + C x₂ -- fails

-- Standard-form polynomials should work with coerced constants without expected type
#check X^2 + C n * X + C x -- fails

end ElabArithGoals