equality in sigma-types

Stream: Is there code for X?

[Heather Macbeth]

I haven't worked with sigma-types before. How do I rewrite a fact by an equality in the type? Something like this:

example {ι : Type*} {α : ι → Type*} (P : (Σ i, α i) → Prop) {i i' : ι} (hi : i = i')
  (H : ∀ a : α i, P ⟨i, a⟩)  :
  ∀ a : α i', P ⟨i', a⟩ :=
sorry

[Yury G. Kudryashov]

subst hi?

[Heather Macbeth]

Aha! Thank you!

[Yury G. Kudryashov]

This only works if i or i' is a variable, not an expression.

[Heather Macbeth]

It works in my use case, anyway.

[Kyle Miller]

cases hi is sometimes useful, too.

[Kevin Buzzard]

nice trick! (spoiler alert: turns i = i' into i = i)

[Kevin Buzzard]

In fact is this how subst works? I always imagined it would be super-complicated!

[Kevin Buzzard]

meta def subst (h : expr) : tactic unit :=
(do guard h.is_local_constant,
    some (α, lhs, β, rhs) ← expr.is_heq <$> infer_type h,
    is_def_eq α β,
    new_h_type ← mk_app `eq [lhs, rhs],
    new_h_pr   ← mk_app `eq_of_heq [h],
    new_h ← assertv h.local_pp_name new_h_type new_h_pr,
    try (clear h),
    subst_core new_h)
<|> subst_core h
end tactic

(this is tactic.subst, what tactic.interactive.subst uses). It's at this point I wish I understood meta stuff :-/

[Eric Wieser]

Note that tactic#subst can also often be replaced with a pattern-match, in this case by moving i i' h right of the colon and matching on _ _ rfl

[Kyle Miller]

Kevin Buzzard said:

In fact is this how subst works? I always imagined it would be super-complicated!

I had the same question, and I got as far as finding it ends up being written in C++, which these meta constants all are:

/- Given a local constant t, if t has type (lhs = rhs) apply substitution.
   Otherwise, try to find a local constant that has type of the form (t = t') or (t' = t).
   The tactic fails if the given expression is not a local constant. -/
meta constant subst_core     : expr → tactic unit

[Kevin Buzzard]

lol lean#646

[Kevin Buzzard]

So where can we see the actual definition subst_core in the repo? I've never gone this deep before.

[Kevin Buzzard]

found it, thanks git grep -- it's presumably this

[Kevin Buzzard]

actually judging by this it's actually this?

[Kevin Buzzard]

right so i think it's a C++ program which literally recurses into the expression and replaces one term by the other? Is this part of the fabled "kernel" I've heard so much about? Or are we not there yet?

[Kyle Miller]

This is the elaborator -- there are things like mk_eq_drec to create the rewrites that show up in the proof term that the tactic proof creates. This all gets shipped off to the kernel to do a final check that everything was created correctly.

[Kyle Miller]

(I'm not actually sure how to classify which part of Lean this is, other than we're not at the kernel yet. This is specifically some C++ code implementing a tactic, and I think in principle it could be written in Lean.)

[Scott Morrison]

And indeed is written in Lean in Lean 4.