Construct instances

[joneugster]

One way to construct algebraic structures (in Tactic-mode) could be the following:

Statement
"Zeige, dass $\\mathbb{R}$ ein $\\mathbb{Q}$-Modul ist."
    : Module ℚ ℝ := by
  refine {
    smul := fun a r => ↑a * r
    smul_zero := ?smul_zero
    zero_smul := ?zero_smul
    one_smul := ?one_smul
    smul_add := ?smul_add
    add_smul := ?add_smul
    mul_smul := ?mul_smul }

  -- Now there are 6 goals which can be proved
  sorry

We should figure way/notation to make that first step easier.

[abentkamp]

I played a bit with it and came up with this:

import Mathlib

example : Module ℚ ℝ := by
    apply Module.ofCore
    constructor
    case H.toSMul =>
      exact SMul.mk fun a r => ↑a * r
    repeat sorry

Not sure if this is any better.

[joneugster]

Apparently mathlib3 also knew refine_struct which seems to be on the way into mathlib4 (Zulip).

That might work as a solution.

instance semigroup [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
begin
  refine_struct { .. },
  exact λ x y , x * y, -- 1st field
  sorry -- 2nd field
end

[joneugster]

I'll see if it's possible that this would work:

import Mathlib

example : Module ℚ ℝ := by
    refine_struct
    exact fun a r => ↑a * r
    repeat sorry

[joneugster]

With a4d1130 the syntax is currently

refine { ?..! }

But long-term we would probably think about how to do that in-game in the nicest way possible as that syntax is a bit cryptic for beginners.

[joneugster]

We settled on using either refine' { smul := fun a r => ↑a * r, .. } or using the (preample := refine' { smul := fun a r => ↑a * r, .. }) option of Statement which hides some preprocessing steps from the player.