Last active
May 11, 2021 15:19
-
-
Save kbuzzard/999fd7d54af7e37c91b1c13122daf941 to your computer and use it in GitHub Desktop.
rw is painfully slow without hints
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
universe u | |
set_option old_structure_cmd true | |
/- 0,+ -/ | |
class add_zero_class (M : Type u) extends has_zero M, has_add M := | |
(zero_add : ∀ (a : M), 0 + a = a) | |
(add_zero : ∀ (a : M), a + 0 = a) | |
class add_semigroup (G : Type u) extends has_add G := | |
(add_assoc : ∀ a b c : G, a + b + c = a + (b + c)) | |
class add_monoid (M : Type u) extends add_semigroup M, add_zero_class M. | |
class add_comm_semigroup (G : Type u) extends add_semigroup G := | |
(add_comm : ∀ a b : G, a + b = b + a) | |
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M | |
/- 1,* -/ | |
class mul_one_class (M : Type u) extends has_one M, has_mul M := | |
(one_mul : ∀ (a : M), 1 * a = a) | |
(mul_one : ∀ (a : M), a * 1 = a) | |
class semigroup (G : Type u) extends has_mul G := | |
(mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)) | |
class comm_semigroup (G : Type u) extends semigroup G := | |
(mul_comm : ∀ a b : G, a * b = b * a) | |
def npow_rec {M : Type*} [has_one M] [has_mul M] : ℕ → M → M | |
| 0 a := 1 | |
| (n+1) a := a * npow_rec n a | |
class monoid (M : Type u) extends semigroup M, mul_one_class M := | |
(npow : ℕ → M → M := npow_rec) | |
class comm_monoid (M : Type u) extends monoid M, comm_semigroup M | |
instance monoid.has_pow {M : Type u} [monoid M] : has_pow M ℕ := ⟨λ x n, monoid.npow n x⟩ | |
/- 0 1 * -/ | |
class mul_zero_class (M₀ : Type*) extends has_mul M₀, has_zero M₀ := | |
(zero_mul : ∀ a : M₀, 0 * a = 0) | |
(mul_zero : ∀ a : M₀, a * 0 = 0) | |
class semigroup_with_zero (S₀ : Type*) extends semigroup S₀, mul_zero_class S₀. | |
class mul_zero_one_class (M₀ : Type*) extends mul_one_class M₀, mul_zero_class M₀. | |
class monoid_with_zero (M₀ : Type*) extends monoid M₀, mul_zero_one_class M₀. | |
/- 0 1 + * -/ | |
class distrib (R : Type*) extends has_mul R, has_add R := | |
(left_distrib : ∀ a b c : R, a * (b + c) = (a * b) + (a * c)) | |
(right_distrib : ∀ a b c : R, (a + b) * c = (a * c) + (b * c)) | |
class non_unital_non_assoc_semiring (α : Type u) extends | |
add_comm_monoid α, distrib α, mul_zero_class α | |
class non_unital_semiring (α : Type u) extends | |
non_unital_non_assoc_semiring α, semigroup_with_zero α | |
class non_assoc_semiring (α : Type u) extends | |
non_unital_non_assoc_semiring α, mul_zero_one_class α | |
class semiring (α : Type u) extends non_unital_semiring α, non_assoc_semiring α, monoid_with_zero α | |
class comm_semiring (α : Type u) extends semiring α, comm_monoid α | |
/- Morphisms -/ | |
structure zero_hom (M : Type*) (N : Type*) [has_zero M] [has_zero N] := | |
(to_fun : M → N) | |
(map_zero' : to_fun 0 = 0) | |
structure add_hom (M : Type*) (N : Type*) [has_add M] [has_add N] := | |
(to_fun : M → N) | |
(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y) | |
structure add_monoid_hom (M : Type*) (N : Type*) [add_zero_class M] [add_zero_class N] | |
extends zero_hom M N, add_hom M N | |
structure one_hom (M : Type*) (N : Type*) [has_one M] [has_one N] := | |
(to_fun : M → N) | |
(map_one' : to_fun 1 = 1) | |
structure mul_hom (M : Type*) (N : Type*) [has_mul M] [has_mul N] := | |
(to_fun : M → N) | |
(map_mul' : ∀ x y, to_fun (x * y) = to_fun x * to_fun y) | |
structure monoid_hom (M : Type*) (N : Type*) [mul_one_class M] [mul_one_class N] | |
extends one_hom M N, mul_hom M N | |
structure monoid_with_zero_hom (M : Type*) (N : Type*) [mul_zero_one_class M] [mul_zero_one_class N] | |
extends zero_hom M N, monoid_hom M N | |
structure ring_hom (α : Type*) (β : Type*) [semiring α] [semiring β] | |
extends monoid_hom α β, add_monoid_hom α β, monoid_with_zero_hom α β | |
infixr ` →+* `:25 := ring_hom | |
instance ring_hom.has_coe_to_fun {α : Type*} {β : Type*} {rα : semiring α} {rβ : semiring β} : | |
has_coe_to_fun (α →+* β) := ⟨_, ring_hom.to_fun⟩ | |
def ring_hom.id (α : Type*) [semiring α] : α →+* α := | |
{ to_fun := id, | |
map_zero' := sorry, | |
map_one' := sorry, | |
map_add' := sorry, | |
map_mul' := sorry } | |
def ring_hom.comp {α β γ : Type*} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} | |
(hnp : β →+* γ) (hmn : α →+* β) : α →+* γ := | |
{ to_fun := hnp ∘ hmn, | |
map_zero' := sorry, | |
map_one' := sorry, | |
map_add' := sorry, | |
map_mul' := sorry } | |
theorem ring_hom.ext {α β : Type*} {rα : semiring α} {rβ : semiring β} ⦃f g : α →+* β⦄ | |
(h : ∀ x, f x = g x) : f = g := sorry | |
/- subobjects -/ | |
structure add_submonoid (M : Type*) [add_zero_class M] := | |
(carrier : set M) | |
(zero_mem' : (0 : M) ∈ carrier) | |
(add_mem' {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier) | |
structure submonoid (M : Type*) [mul_one_class M] := | |
(carrier : set M) | |
(one_mem' : (1 : M) ∈ carrier) | |
(mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier) | |
structure subsemiring (R : Type u) [semiring R] extends submonoid R, add_submonoid R | |
/- nat and facts -/ | |
class fact (p : Prop) : Prop := (out [] : p) | |
def nat.prime (p : ℕ) := 2 ≤ p ∧ ∀ m ∣ p, m = 1 ∨ m = p | |
protected def nat.cast {α : Type*} [has_zero α] [has_one α] [has_add α] : ℕ → α | |
| 0 := 0 | |
| (n+1) := nat.cast n + 1 | |
@[priority 900] instance nat.cast_coe {α : Type*} [_inst_1 : has_zero α] [_inst_2 : has_one α] | |
[_inst_3 : has_add α] : has_coe_t ℕ α := ⟨nat.cast⟩ | |
class char_p (R : Type*) [add_monoid R] [has_one R] (p : ℕ) : Prop := | |
(cast_eq_zero_iff [] : ∀ x:ℕ, (x:R) = 0 ↔ p ∣ x) | |
/- Pi -/ | |
namespace pi | |
universes v | |
variable {I : Type u} -- The indexing type | |
variable {f : I → Type v} -- The family of types already equipped with instances | |
variables (x y : Π i, f i) (i : I) | |
instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ _, 1⟩ | |
instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) := ⟨λ _, 0⟩ | |
instance has_add [∀ i, has_add $ f i] : has_add (Π i : I, f i) := ⟨λ f g i, f i + g i⟩ | |
instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ f g i, f i * g i⟩ | |
instance mul_one_class [∀ i, mul_one_class $ f i] : mul_one_class (Π i : I, f i) := | |
{ one := (1 : Π i, f i), mul := (*), one_mul := sorry, mul_one := sorry } | |
instance semiring [∀ i, semiring $ f i] : semiring (Π i : I, f i) := | |
{ zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), | |
add_assoc := sorry, | |
zero_add := sorry, | |
add_zero := sorry, | |
add_comm := sorry, | |
left_distrib := sorry, | |
right_distrib := sorry, | |
zero_mul := sorry, | |
mul_zero := sorry, | |
mul_assoc := sorry, | |
one_mul := sorry, | |
mul_one := sorry, | |
} | |
instance comm_semiring [∀ i, comm_semiring $ f i] : comm_semiring (Π i : I, f i) := | |
{ zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), | |
add_assoc := sorry, | |
zero_add := sorry, | |
add_zero := sorry, | |
add_comm := sorry, | |
left_distrib := sorry, | |
right_distrib := sorry, | |
zero_mul := sorry, | |
mul_zero := sorry, | |
mul_assoc := sorry, | |
one_mul := sorry, | |
mul_one := sorry, | |
mul_comm := sorry } | |
end pi | |
/- setlike -/ | |
class set_like (A : Type*) (B : out_param $ Type*) := | |
(coe : A → set B) | |
(coe_injective' : function.injective coe) | |
instance submonoid.set_like {M : Type*} [mul_one_class M] : set_like (submonoid M) M := | |
⟨submonoid.carrier, sorry⟩ | |
instance add_submonoid.set_like {M : Type*} [add_zero_class M] : set_like (add_submonoid M) M := | |
⟨add_submonoid.carrier, sorry⟩ | |
instance subsemiring.set_like {R : Type*} [semiring R] : set_like (subsemiring R) R := | |
⟨subsemiring.carrier, sorry⟩ | |
namespace set_like | |
variables {A : Type*} {B : Type*} [i : set_like A B] | |
include i | |
instance : has_coe_t A (set B) := ⟨set_like.coe⟩ | |
@[priority 100] | |
instance : has_mem B A := ⟨λ x p, x ∈ (p : set B)⟩ | |
-- `dangerous_instance` does not know that `B` is used only as an `out_param` | |
instance : has_coe_to_sort A := ⟨_, λ p, {x : B // x ∈ p}⟩ | |
end set_like | |
/- coercion from subobject to object -/ | |
theorem subtype.coe_injective {α : Type*} {p : α → Prop} : | |
function.injective (coe : subtype p → α) := sorry | |
protected def function.injective.add_semigroup {M₁ : Type*} {M₂ : Type*} [has_add M₁] [add_semigroup M₂] | |
(f : M₁ → M₂) (hf : function.injective f) | |
(add : ∀ x y, f (x + y) = f x + f y) : | |
add_semigroup M₁ := | |
{ add_assoc := sorry, | |
..‹has_add M₁› } | |
protected def function.injective.semigroup {M₁ : Type*} {M₂ : Type*} [has_mul M₁] [semigroup M₂] (f : M₁ → M₂) | |
(hf : function.injective f) | |
(mul : ∀ x y, f (x * y) = f x * f y) : | |
semigroup M₁ := | |
{ mul_assoc := sorry, | |
..‹has_mul M₁› } | |
protected def function.injective.add_comm_semigroup {M₁ : Type*} {M₂ : Type*} [has_add M₁] | |
[add_comm_semigroup M₂] (f : M₁ → M₂) (hf : function.injective f) | |
(add : ∀ x y, f (x + y) = f x + f y) : | |
add_comm_semigroup M₁ := | |
{ add_comm := sorry, | |
.. hf.add_semigroup f add } | |
protected def function.injective.add_zero_class {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁] | |
[add_zero_class M₂] (f : M₁ → M₂) (hf : function.injective f) | |
(zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) : | |
add_zero_class M₁ := | |
{ zero_add := sorry, | |
add_zero := sorry, | |
..‹has_zero M₁›, ..‹has_add M₁› } | |
protected def function.injective.mul_one_class {M₁ : Type*} {M₂ : Type*} [has_one M₁] [has_mul M₁] [mul_one_class M₂] (f : M₁ → M₂) (hf : function.injective f) | |
(one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : | |
mul_one_class M₁ := | |
{ one_mul := sorry, | |
mul_one := sorry, | |
..‹has_one M₁›, ..‹has_mul M₁› } | |
protected def function.injective.add_monoid {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁] [add_monoid M₂] | |
(f : M₁ → M₂) (hf : function.injective f) | |
(zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) : | |
add_monoid M₁ := | |
{ .. hf.add_semigroup f add, .. hf.add_zero_class f zero add } | |
protected def function.injective.monoid {M₁ : Type*} {M₂ : Type*} [has_one M₁] [has_mul M₁] [monoid M₂] | |
(f : M₁ → M₂) (hf : function.injective f) | |
(one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) : | |
monoid M₁ := | |
{ .. hf.semigroup f mul, .. hf.mul_one_class f one mul } | |
protected def function.injective.add_comm_monoid {M₁ : Type*} {M₂ : Type*} [has_zero M₁] [has_add M₁] | |
[add_comm_monoid M₂] (f : M₁ → M₂) (hf : function.injective f) | |
(zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y) : | |
add_comm_monoid M₁ := | |
{ .. hf.add_comm_semigroup f add, .. hf.add_monoid f zero add } | |
instance add_submonoid.has_zero {M : Type*} [add_zero_class M] (S : add_submonoid M): has_zero S := ⟨⟨0, sorry⟩⟩ | |
instance submonoid.has_one {M : Type*} [mul_one_class M] (S : submonoid M): has_one S := ⟨⟨1, sorry⟩⟩ | |
instance submonoid.has_add {M : Type*} [add_zero_class M] (S : add_submonoid M): has_add S := ⟨λ a b, ⟨a.1 + b.1, sorry⟩⟩ | |
instance submonoid.has_mul {M : Type*} [mul_one_class M] (S : submonoid M): has_mul S := ⟨λ a b, ⟨a.1 * b.1, sorry⟩⟩ | |
instance submonoid.to_monoid {M : Type*} [monoid M] (S : submonoid M) : monoid S := | |
subtype.coe_injective.monoid coe sorry sorry | |
instance add_submonoid.to_add_comm_monoid {M} [add_comm_monoid M] (S : add_submonoid M) : add_comm_monoid S := | |
subtype.coe_injective.add_comm_monoid coe rfl (λ _ _, rfl) | |
instance subsemiring.to_semiring {R : Type u} [semiring R] (s : subsemiring R) : semiring s := | |
{ mul_zero := sorry, | |
zero_mul := sorry, | |
right_distrib := sorry, | |
left_distrib := sorry, | |
.. s.to_submonoid.to_monoid, .. s.to_add_submonoid.to_add_comm_monoid } | |
instance subsemiring.to_comm_semiring {R} [comm_semiring R] (s : subsemiring R) : comm_semiring s := | |
{ mul_comm := sorry, ..s.to_semiring} | |
/- char p ring theory -/ | |
def monoid.perfection (M : Type*) [comm_monoid M] (p : ℕ) : submonoid (ℕ → M) := | |
{ carrier := { f | ∀ n, f (n + 1) ^ p = f n }, | |
one_mem' := sorry, | |
mul_mem' := sorry } | |
def ring.perfection (R : Type*) [comm_semiring R] | |
(p : ℕ) [hp : fact p.prime] [char_p R p] : | |
subsemiring (ℕ → R) := | |
{ zero_mem' := sorry, | |
add_mem' := sorry, | |
.. monoid.perfection R p } | |
instance char_p.subsemiring (R : Type u) [semiring R] (p : ℕ) [char_p R p] (S : subsemiring R) : | |
char_p S p := ⟨sorry⟩ | |
instance char_p.pi (ι : Type u) [hi : nonempty ι] (R : Type*) [semiring R] (p : ℕ) [char_p R p] : | |
char_p (ι → R) p := ⟨sorry⟩ | |
def frobenius (R : Type*) [comm_semiring R] (p : ℕ) [fact p.prime] [char_p R p] : R →+* R := | |
{ to_fun := λ x, x^p, | |
map_one' := sorry, | |
map_mul' := sorry, | |
map_zero' := sorry, | |
map_add' := sorry } | |
def perfection.coeff (R : Type*) [comm_semiring R] (p : ℕ) [hp : fact (nat.prime p)] | |
[_inst_2 : char_p R p] (n : ℕ) : ring.perfection R p →+* R := | |
{ to_fun := λ f, f.1 n, | |
map_one' := rfl, | |
map_mul' := λ f g, rfl, | |
map_zero' := rfl, | |
map_add' := λ f g, rfl } | |
lemma perfection.ext {R : Type*} [comm_semiring R] {p : ℕ} [hp : fact (nat.prime p)] [_inst_2 : char_p R p] | |
{f g : ring.perfection R p} (h : ∀ n, perfection.coeff R p n f = perfection.coeff R p n g) : f = g := | |
sorry | |
/-- The `p`-th root of an element of the perfection. -/ | |
def perfection.pth_root (R : Type*) [comm_semiring R] (p : ℕ) [hp : fact (nat.prime p)] [char_p R p] : | |
ring.perfection R p →+* ring.perfection R p := | |
{ to_fun := λ f, ⟨λ n, perfection.coeff R p (n + 1) f, λ n, f.2 _⟩, | |
map_one' := rfl, | |
map_mul' := λ f g, rfl, | |
map_zero' := rfl, | |
map_add' := λ f g, rfl } | |
lemma ring_hom.comp_apply {α β γ : Type*} [rα : semiring α] [rβ : semiring β] {rγ : semiring γ} | |
(hnp : β →+* γ) (hmn : α →+* β) (x : α) : (hnp.comp hmn) x = hnp (hmn x) := sorry | |
lemma ring_hom.id_apply {α : Type*} [rα : semiring α] (x : α) : (ring_hom.id α) x = x := sorry | |
lemma ring_hom.map_frobenius {R : Type*} [_inst_1 : comm_semiring R] {S : Type*} | |
[comm_semiring S] (g : R →+* S) (p : ℕ) | |
[fact (nat.prime p)] [char_p R p] [char_p S p] (x : R) : | |
g ((frobenius R p) x) = (frobenius S p) (g x) := sorry | |
lemma perfection.coeff_pth_root {R : Type*} [comm_semiring R] {p : ℕ} [hp : fact (nat.prime p)] | |
[char_p R p] (f : (ring.perfection R p)) (n : ℕ) : | |
(perfection.coeff R p n) ((perfection.pth_root R p) f) = (perfection.coeff R p (n + 1)) f := sorry | |
lemma perfection.coeff_frobenius {R : Type u} [comm_semiring R] {p : ℕ} [hp : fact (nat.prime p)] | |
[char_p R p] (f : (ring.perfection R p)) (n : ℕ) : | |
(perfection.coeff R p (n + 1)) ((frobenius (ring.perfection R p) p) f) = (perfection.coeff R p n) f := sorry | |
set_option profiler true | |
-- elaboration of pth_root_frobenius_quick took 96.9ms | |
lemma pth_root_frobenius_quick {R : Type u} [comm_semiring R] {p : ℕ} [hp : fact (nat.prime p)] | |
[char_p R p] : (perfection.pth_root R p).comp (frobenius _ p) = ring_hom.id _ := | |
ring_hom.ext $ λ f, perfection.ext $ λ n, begin | |
rw [ring_hom.comp_apply, ring_hom.id_apply, perfection.coeff_pth_root], | |
rw perfection.coeff_frobenius f -- | |
end | |
-- elaboration of pth_root_frobenius_slow took 1.67s | |
lemma pth_root_frobenius_slow {R : Type u} [comm_semiring R] {p : ℕ} [hp : fact (nat.prime p)] | |
[char_p R p] : (perfection.pth_root R p).comp (frobenius _ p) = ring_hom.id _ := | |
ring_hom.ext $ λ f, perfection.ext $ λ n, begin | |
rw [ring_hom.comp_apply, ring_hom.id_apply, perfection.coeff_pth_root], | |
-- ⊢ ⇑(perfection.coeff R p (n + 1)) (⇑(frobenius ↥(ring.perfection R p) p) x) = ⇑(perfection.coeff R p n) x | |
-- the LHS of the goal literally matches the LHS of the lemma. | |
rw perfection.coeff_frobenius -- no f, costs us 1.5 seconds | |
end | |
-- elaboration of frobenius_pth_root_quick took 266ms | |
lemma frobenius_pth_root_quick {R : Type u} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] : | |
(frobenius (ring.perfection R p) p).comp (perfection.pth_root R p) = ring_hom.id (ring.perfection R p) := | |
ring_hom.ext $ λ f, perfection.ext $ λ n, | |
begin | |
rw ring_hom.comp_apply, | |
rw ring_hom.id_apply, | |
rw ring_hom.map_frobenius, | |
rw perfection.coeff_pth_root f, | |
rw ← ring_hom.map_frobenius, | |
rw perfection.coeff_frobenius f, | |
end | |
-- elaboration of frobenius_pth_root_slow took 4.88s | |
lemma frobenius_pth_root_slow {R : Type u} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] : | |
(frobenius (ring.perfection R p) p).comp (perfection.pth_root R p) = ring_hom.id (ring.perfection R p) := | |
ring_hom.ext $ λ f, perfection.ext $ λ n, | |
begin | |
rw ring_hom.comp_apply, | |
rw ring_hom.id_apply, | |
rw ring_hom.map_frobenius, | |
rw perfection.coeff_pth_root, -- no f | |
rw ← ring_hom.map_frobenius, | |
rw perfection.coeff_frobenius, -- no f | |
end | |
-- edit this comment a few times and you'll be in trouble | |
lemma I_can_break_lean {R : Type u} {p : ℕ} [comm_semiring R] [hp : fact (nat.prime p)] [char_p R p] : | |
(frobenius (ring.perfection R p) p).comp (perfection.pth_root R p) = ring_hom.id (ring.perfection R p) := | |
ring_hom.ext $ λ f, perfection.ext $ λ n, | |
begin | |
rw ring_hom.comp_apply, | |
rw ring_hom.id_apply, | |
rw ring_hom.map_frobenius, | |
rw perfection.coeff_pth_root, -- no f | |
rw ← perfection.coeff_pth_root, -- no f | |
rw perfection.coeff_pth_root, -- no f | |
rw ← perfection.coeff_pth_root, -- no f | |
rw perfection.coeff_pth_root, -- no f | |
rw ← perfection.coeff_pth_root, -- no f | |
rw perfection.coeff_pth_root, -- no f | |
rw ← perfection.coeff_pth_root, -- no f | |
rw perfection.coeff_pth_root, -- no f | |
rw ← perfection.coeff_pth_root, -- no f | |
rw perfection.coeff_pth_root, -- no f | |
rw ← perfection.coeff_pth_root, -- no f | |
sorry | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment