Skip to content

Instantly share code, notes, and snippets.

@dselsam
Last active May 1, 2021 17:35
Show Gist options
  • Save dselsam/98f8febef01cca03a41d2dafcc876bba to your computer and use it in GitHub Desktop.
Save dselsam/98f8febef01cca03a41d2dafcc876bba to your computer and use it in GitHub Desktop.
Elaboration goals for concrete arithmetic (no mathlib dependency)
-- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment