Elaboration goals for concrete arithmetic (no mathlib dependency)

ElabArithGoalsNoMathlib.lean

-- Fail annotations refer to e70e924327c3b42d28dd8a59340a89cbafb3d5b6
namespace ElabArithGoalsNoMathlib

constant Rat     : Type
constant Real    : Type
constant Complex : Type

notation "ℕ" => Nat
notation "ℤ" => Int
notation "ℚ" => Rat
notation "ℝ" => Real
notation "ℂ" => Complex

@[instance] axiom Rat.add : Add ℚ
@[instance] axiom Rat.sub : Sub ℚ
@[instance] axiom Rat.mul : Mul ℚ
@[instance] axiom Rat.pow : Pow ℚ
@[instance] axiom Rat.div : Div ℚ

@[instance] axiom Real.add : Add ℝ
@[instance] axiom Real.sub : Sub ℝ
@[instance] axiom Real.mul : Mul ℝ
@[instance] axiom Real.pow : Pow ℝ
@[instance] axiom Real.div : Div ℝ

@[instance] axiom Complex.add : Add ℂ
@[instance] axiom Complex.sub : Sub ℂ
@[instance] axiom Complex.mul : Mul ℂ
@[instance] axiom Complex.pow : Pow ℂ
@[instance] axiom Complex.div : Div ℂ

@[instance] axiom Int.coeRat      : Coe ℤ ℚ
@[instance] axiom Rat.coeReal     : Coe ℚ ℝ
@[instance] axiom Real.coeComplex : Coe ℝ ℂ

instance [CoeHTCT α β] [Pow β] : HPow α β β where
  hPow a b := Pow.pow a b

instance [CoeHTCT α β] [Pow β] : HPow β α β where
  hPow a b := Pow.pow a b

@[defaultInstance high]
instance (priority := high) : HSub Nat Nat Int where
  hSub a b :=  (a : Int) - (b : Int)

def natPow [OfNat α 1] [Mul α] (x : α) : Nat →  α
  | 0   => 1
  | 1   => x
  | n+1 => x * natPow x n

instance [OfNat α 1] [Mul α] [Div α] : HPow α Int α where
  hPow (x : α)
    | Int.ofNat n   => natPow x n
    | Int.negSucc n => 1 / (natPow x (n+1))

@[defaultInstance high]
instance (priority := high) [OfNat α 1] [Mul α] : HPow α Nat α where
  hPow := natPow

@[defaultInstance high]
noncomputable instance (priority := high) : HPow ℚ Int ℚ where
  hPow x k := @HPow.hPow ℚ Int ℚ _ x k

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 -- ℤ
#check n + q -- ℚ
#check n + x -- ℝ

-- 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 : ℤ)
#check (n + q : ℚ)
#check (n + x : ℝ)

-- 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₂ : ℤ)
#check (n₁ + n₂ : ℚ)
#check (n₁ + n₂ : ℝ)
#check (z₁ + z₂ : ℚ)
#check (z₁ + z₂ : ℝ)
#check (q₁ + q₂ : ℝ)

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

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

-- 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)
#check (n - n₁ : ℕ) -- (should fail)

-- Subtracting numerals should coerce them at least to ℤ (without expected type)
#check n - 1
#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)
#check n^2
#check z^2
#check q^2
#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
#check q^q
#check x^x

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

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

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

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

-- II. Polynomials
universe u
constant Polynomial : Type u → Type u := id

variable {α : Type u} {β : Type v}

axiom X : Polynomial α
axiom C : α → Polynomial α -- TODO: simplification of mathlib's

@[instance] axiom Polynomial.ofNat [inst : OfNat α n] : OfNat (Polynomial α) n
@[instance] axiom Polynomial.add [Add α] : Add (Polynomial α)
@[instance] axiom Polynomial.sub [Sub α] : Sub (Polynomial α)
@[instance] axiom Polynomial.mul [Mul α] : Mul (Polynomial α)
@[instance] axiom Polynomial.coe [Coe α β] : Coe (Polynomial α) (Polynomial β)

-- 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 ℂ)

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

-- Adding coerced constants with no expected type
#check C n + C z

-- Adding coerced constants with expected type
#check (C n + C z : Polynomial ℤ)

-- 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 n * X + C x₂ : Polynomial ℂ) -- fails
#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₂

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

end ElabArithGoalsNoMathlib