porting data.sigma.basic

Stream: mathlib4

[Kevin Buzzard]

Mathlib3 has

-- we generate this manually as `@[derive has_reflect]` fails
@[instance]
protected meta def {u v} sigma.reflect [reflected_univ.{u}] [reflected_univ.{v}]
  {α : Type u} (β : α → Type v)
  [reflected _ α] [reflected _ β] [hα : has_reflect α] [hβ : Π i, has_reflect (β i)] :
  has_reflect (Σ a, β a) :=
λ ⟨a, b⟩, (by reflect_name : reflected _ @sigma.mk.{u v}).subst₄ `(α) `(β) `(a) `(b)

in data.sigma.basic; this has been translated to

-- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:66:14: unsupported tactic `reflect_name #[]
-- we generate this manually as `@[derive has_reflect]` fails
@[instance]
protected unsafe def sigma.reflect.{u, v} [reflected_univ.{u}] [reflected_univ.{v}] {α : Type u} (β : α → Type v)
    [reflected _ α] [reflected _ β] [hα : has_reflect α] [hβ : ∀ i, has_reflect (β i)] : has_reflect (Σa, β a) :=
  fun ⟨a, b⟩ =>
  (by trace "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:66:14: unsupported tactic `reflect_name #[]" :
        reflected _ @Sigma.mk.{u, v}).subst₄
    (quote.1 α) (quote.1 β) (quote.1 a) (quote.1 b)

in mathlib4, which fails with the error invalid use of explicit universe parameters, 'reflected_univ' is a local. This is meta code in mathlib3 so it's beyond my pay grade. How do I ask for help here?

[Scott Morrison]

This is all meta stuff, so I would suggest just deleting it all and assuming that it is no longer relevant. :-)

[Scott Morrison]

If you're feeling cautious, add a

-- Porting note: I have deleted an instance of `has_reflect (Σ a, β a)` here.

[Scott Morrison]

Even more cautious, also leave the mathport generated code, commented out.

[Kevin Buzzard]

In mathlib3 this code

-- Lean 3
universes u v

structure psigma' {α : Sort u} (β : α → Sort v) :=
mk :: (fst : α) (snd : β fst)

#check psigma'.mk.inj
-- psigma'.mk.inj : {fst := ?M_3, snd := ?M_4} = {fst := ?M_5, snd := ?M_6} → ?M_3 = ?M_5 ∧ ?M_4 == ?M_6

generates a mk.inj lemma. I can't find the analogue of this lemma in Lean 4 (there is PSigma.mk and PSigma.mkSkipLeft and PSigma.mk.sizeOf_spec and a couple of other things which aren't right). Am I supposed to prove it myself (if so, where do I put it?) or just come up with another proof?

[Scott Morrison]

Seriously, when there is meta stuff in the main theory files, it's just not your problem for porting.

[Kevin Buzzard]

OK.

[Scott Morrison]

Re: mk.inj, I've run into this too, and would like to know the answer.

[Mario Carneiro]

There is no analogue for that has_reflect instance because we don't have the reflected typeclass. (has_reflect is now ToExpr.) I agree with Scott, just remove it and hope it doesn't matter anymore

[Eric Rodriguez]

Cc @Eric Wieser who wrote this I tbink

[Mario Carneiro]

Injectivity theorems are no longer generated by default. They can be requested like so:

gen_injective_theorems% PSigma

#print PSigma.mk.inj
-- theorem PSigma.mk.inj.{u, v} : ∀ {α : Sort u} {β : α → Sort v} {fst : α} {snd : β fst} {fst_1 : α} {snd_1 : β fst_1},
--   { fst := fst, snd := snd } = { fst := fst_1, snd := snd_1 } → fst = fst_1 ∧ HEq snd snd_1

[Mario Carneiro]

although because use of gen_injective_theorems% PSigma declares theorems in the PSigma namespace that can clash with other calls to the command, I would recommend PRing this to lean core if you find a definition from Init that lacks injective theorems.

[Mario Carneiro]

Actually I take it back, injectivity theorems are generated by default:

structure psigma' {α : Sort u} (β : α → Sort v) :=
mk :: (fst : α) (snd : β fst)

#print psigma'.mk.inj
-- theorem psigma'.mk.inj.{u, v} : ∀ {α : Sort u} {β : α → Sort v} {fst : α} {snd : β fst} {fst_1 : α} {snd_1 : β fst_1},
--   { fst := fst, snd := snd } = { fst := fst_1, snd := snd_1 } → fst = fst_1 ∧ HEq snd snd_1

PSigma is just special because it is declared very early, when not all theorems required for the injectivity proof are available. gen_injective_theorems% is only required for these specific foundational inductives. There is a block of them in Init.Core but PSigma isn't on the list

[Scott Morrison]

@Kevin Buzzard, obviously it's annoying to run into these problems, but what Mario just found here is part of the payoff of starting porting!

[Mario Carneiro]

If you need to get unstuck, just add gen_injective_theorems% PSigma somewhere appropriate in mathlib4 but this will probably be upstreamed at some point

[Eric Wieser]

Shouldn't has_reflect become ToExpr then via #align or something?

[Scott Morrison]

No, because this is meta stuff, which we don't attempt to #align.

[Scott Morrison]

It's a whole new world. :-)

[Mario Carneiro]

We can align it, but it's kind of pointless since you immediately run into much worse errors (see the lovely mathport error smuggled in a string literal above)

[Eric Wieser]

I would expect it to follow the pattern of docs4#Lean.instToExprProd... but that implementation looks like it's invalid in universes other than 0!

[Mario Carneiro]

Indeed it is. The whole typeclass doesn't really work for universes other than 0, it would need a level in addition to a type expression

[Mario Carneiro]

(I tried writing it based on instToExprProd, the issue is that you don't have an expr for beta and without some magic to synthesize reflected it's kind of pointless to assume you are given one.)

[Eric Wieser]

So perhaps we need to forward-port mathlib3's docs#reflected_univ to lean4 core?

[Mario Carneiro]

If lean4 core isn't using it already, it probably isn't needed

[Mario Carneiro]

The Qq library is a much better approach to this kind of thing

[Eric Wieser]

Well it's needed to make the existing instances not garbage. I guess removing the broken universe polymorphism from src4#Lean.instToExprProd (and a bunch of other toExpr instances), and leaving universes to Qq would also make that a non-issue.

[Mario Carneiro]

The typeclass itself can't be used if you care about reflecting expressions in other universes - it's not just the instances, the typeclass does not have enough data in it to implement sensible instances

[Mario Carneiro]

but I'm not sure when that would ever come up

[Kevin Buzzard]

mathlib4#479