CoCalc Logo Icon
StoreFeaturesDocsShareSupportNewsAboutSign UpSign In

Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

| Download

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Project: Xena
Views: 18536
License: APACHE
Tweet
Share
Share
/-
Tests for norm_cast
-/

import tactic.norm_cast
import data.complex.basic -- ℕ, ℤ, ℚ, ℝ, ℂ
import data.zmod.basic

constants (an bn cn dn : ℕ) (az bz cz dz : ℤ) (aq bq cq dq : ℚ)
constants (ar br cr dr : ℝ) (ac bc cc dc : ℂ)

example : (an : ℤ) = bn → an = bn := λ h, by exact_mod_cast h -- by simp
example : an = bn → (an : ℤ) = bn := λ h, by exact_mod_cast h -- by simp
example : az = bz ↔ (az : ℚ) = bz := by norm_cast -- by simp

example : (aq : ℝ) = br ↔ (aq : ℂ) = br := by norm_cast
example : (an : ℚ) = bz ↔ (an : ℂ) = bz := by norm_cast
example : (((an : ℤ) : ℚ) : ℝ) = bq ↔ ((an : ℚ) : ℂ) = (bq : ℝ) :=
by norm_cast

example : (an : ℤ) < bn ↔ an < bn             := by norm_cast -- by simp
example : (an : ℚ) < bz ↔ (an : ℝ) < bz       := by norm_cast
example : ((an : ℤ) : ℝ) < bq ↔ (an : ℚ) < bq := by norm_cast
example : (an : ℤ) ≠ (bn : ℤ) ↔ an ≠ bn := by norm_cast -- by simp

-- zero and one cause special problems
example : 0 < (bq : ℝ) ↔ 0 < bq := by norm_cast -- by simp
example : az > (1 : ℕ) ↔ az > 1 := by norm_cast -- by simp
example : az > (0 : ℕ) ↔ az > 0 := by norm_cast -- by simp
example : (an : ℤ) ≠ 0 ↔ an ≠ 0 := by norm_cast -- by simp
example : aq < (1 : ℕ) ↔ (aq : ℝ) < (1 : ℤ) := by norm_cast

example : (an : ℤ) + bn = (an + bn : ℕ)   := by norm_cast -- by simp
example : (an : ℂ) + bq = ((an + bq) : ℚ) := by norm_cast -- by simp
example : (((an : ℤ) : ℚ) : ℝ) + bn = (an + (bn : ℤ)) := by norm_cast -- by simp

example : (((((an : ℚ) : ℝ) * bq) + (cq : ℝ) ^ dn) : ℂ) = (an : ℂ) * (bq : ℝ) + cq ^ dn :=
by norm_cast -- by simp
example : ((an : ℤ) : ℝ) < bq ∧ (cr : ℂ) ^ 2 = dz ↔ (an : ℚ) < bq ∧ ((cr ^ 2) : ℂ) = dz :=
by norm_cast

example : (an : ℤ) = 1 → an = 1 := λ h, by exact_mod_cast h
example : (an : ℤ) < 5 → an < 5 := λ h, by exact_mod_cast h
example : an < 5 → (an : ℤ) < 5 := λ h, by exact_mod_cast h
example : (an + 5) < 10 → (an : ℤ) + 5 < 10 := λ h, by exact_mod_cast h
example : (an : ℤ) + 5 < 10 → (an + 5) < 10 := λ h, by exact_mod_cast h
example : ((an + 5 : ℕ) : ℤ) < 10 → an + 5 < 10 := λ h, by exact_mod_cast h
example : an + 5 < 10 → ((an + 5 : ℕ) : ℤ) < 10 := λ h, by exact_mod_cast h

example (h : bn ≤ an) : an - bn = 1 ↔ (an - bn : ℤ) = 1 :=
by norm_cast
example (h : (cz : ℚ) = az / bz) : (cz : ℝ) = az / bz :=
by assumption_mod_cast
example : aq * bq = rat.mk (aq.num * bq.num) (↑aq.denom * ↑bq.denom) :=
by rw_mod_cast rat.mul_num_denom
example (h : an = 0) : (an : ℝ) = (bn : ℂ).im :=
by exact_mod_cast h

example (k : ℕ) {x y : ℕ} :
  (x * x + y * y : ℤ) - ↑((x * y + 1) * k) = ↑y * ↑y - ↑k * ↑x * ↑y + (↑x * ↑x - ↑k) :=
begin
  push_cast,
  ring
end

example (k : ℕ) {x y : ℕ} (h : ((x + y + k : ℕ) : ℤ) = 0) : x + y + k = 0 :=
begin
  push_cast at h,
  guard_hyp h := (x : ℤ) + y + k = 0,
  assumption_mod_cast
end