mwe maker

Stream: general

[Kevin Buzzard]

There is some weird timeout issue which I'm trying to diagnose, and I know from experience that people like Gabriel and Mario are far likelier to look at such things if they are given mathlib-free MWE's. So I'm trying to make one. The issue is deep into mathlib, it's some statement about morphisms between subsemirings of products of rings in characteristic p. I'm doing it by hand. So far I have this:

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

/- 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,
}

end pi

and I've still got some way to go.

OK so this is all structured procrastination because I should be marking 318 proofs of if a_n -> b then (a_n)^3->b^3 etc, but still, this set me wondering: could there be a tool for making these MWE's, like extract_goal but on steroids? Or is this somehow asking too much for reasons I don't understand?

[Gabriel Ebner]

Jason Gross has written something like this for Coq: https://github.com/JasonGross/coq-tools
https://people.csail.mit.edu/jgross/personal-website/papers/2015-coq-bug-minimizer.pdf