Unfolding let bindings in hypotheses

Stream: Is there code for X?

[Eric Wieser]

It seems that intro (but not rintro) is able to unfold let bindings in goals:

import algebra.group
import data.nat.basic

def some_def (i j : ℕ) (x : fin $ i + j) (y : fin $ j + i) :=
let h1 := add_comm j i, h2 := (congr_arg fin h1) in x = h2.mp y

lemma as_goal : some_def 2 3 1 1 :=
begin
  unfold some_def,
  assume h1 h2,
  exact eq_mp_rfl,
end

However, the same does not seem to be true of hypotheses:

lemma as_hyp (hs : some_def 2 3 1 1) : 1 = 2 :=
begin
  unfold some_def at hs,
  obtain ⟨h1, h2,, rest⟩ := hs,
  -- `hs`, `h1`, and `h2` are gone?
  sorry
end

Is there a tactic that can do this?

[Mario Carneiro]

I don't think any such tactic exists; most tactics just unfold lets or don't know what to do with them

[Eric Wieser]

Presumably since intro can do it on goals, it should be possible to do it on hypotheses somehow too?

[Mario Carneiro]

this needs a tactic that can "hoist" lets out of an expression

[Mario Carneiro]

no, there's a missing piece

[Mario Carneiro]

(although you used a really annoying example because of all the _ in the goal)

[Eric Wieser]

(Pretend I used let h1 := add_comm j i, h2 := (congr_arg fin h1) in x = h2.mp y)

[Mario Carneiro]

lemma as_hyp (hs : some_def 2 3 1 1) : 1 = 2 :=
begin
  unfold some_def at hs,
  revert hs,
  -- before
  show (let h : 3 + 2 = 2 + 3 := add_comm 3 2 in 1 = (some_def._proof_1 2 3).mp 1) → 1 = 2,
  -- after
  show let h : 3 + 2 = 2 + 3 := add_comm 3 2 in 1 = (some_def._proof_1 2 3).mp 1 → 1 = 2,
  -- now intro
  intro h,
  -- put hs back
  intro hs
end

[Mario Carneiro]

you need a tactic that will do the equivalent of the show lines

[Mario Carneiro]

It's a little unrealistic to be using let with proofs anyway

[Mario Carneiro]

these should be have

[Eric Wieser]

My original idea behind the let was that as_goal could start assume h1 h2, substs h1 h2 to eliminate eq.mp from the goal, but for reasons I don't understand that doesn't work

[Eric Wieser]

And exact eq_mp_rfl doesn't actually work for my real case

[Mario Carneiro]

This kind of looks like an #xy problem though

[Mario Carneiro]

as_goal can be proved by rfl straight off

[Eric Wieser]

The original problem is just exploring ways to express equalities between indexed types. I'm currently using something like (a : A i) (b : A (i + 0)) : (⟨_, a⟩: Σ i, A i) = ⟨_, b⟩), but its ugly to work with, as both the caller and the prover need to supply the zero_add proof

[Eric Wieser]

Evidently my mwe was enough for the original question but too reduced for the follow-up

[Eric Wieser]

But a let-bindings introducing tactic would still be sane for data, right?

[Mario Carneiro]

well like I said there is a missing operation here, a let hoisting operation that can be performed by change if it is constructed appropriately

[Mario Carneiro]

the only thing lean knows to do with lets is unfold them or put them in the context with intro when the goal happens to be a let (because this is a no-op internally)

[Mario Carneiro]

it is a bit reminiscent of generalize_proofs, which does the same hoisting operation but for proofs instead of lets

[Eric Wieser]

generalize_proofs gives me the proof that fin (i + j) = fin (j + i), but not the proof that i + j = j + i - and for a general indexed type, the former does not imply the latter.

[Mario Carneiro]

True, but once the hypothesis is named it's easier to replace it by defeq with congr_arg fin h'

[Mario Carneiro]

In this particular case you should probably be using the eq.mp lemma specific to fin

[Mario Carneiro]

docs#fin.cast

[Eric Wieser]

fin was solely for the case of this mwe

[Mario Carneiro]

then you should be using the eq.mp lemma specific to that type

[Eric Wieser]

It doesn't have a specific eq.mp lemma because the type is A : ι → Type* and A i

[Mario Carneiro]

I think eq.rec A (h : i = j) will work in that case

[Eric Wieser]

Yes, it does - I had in my head that mp was "simpler" and therefore might be easier to prove things about

[Mario Carneiro]

No, it uses type equalities which are to be avoided

[Mario Carneiro]

eq.rec makes the motive explicit and puts the equality in the type you actually want

[Eric Wieser]

Ultimately my thought was that if I had a goal of the form h.rec a = b, then I could use subst h in tactic mode to reduce it to a = b

[Mario Carneiro]

you should

[Mario Carneiro]

that doesn't work if h is a composite term though

[Mario Carneiro]

in particular one side has to be a variable

[Eric Wieser]

Right, therein lies the problem, 0 + i = i is apparently not a legal form for h in my case

[Mario Carneiro]

you have to generalize everything about 0 + i to j first

[Mario Carneiro]

once you can make your theorem typecheck with j in place of 0+i you are done

[Mario Carneiro]

I can't say more specifically without an MWE that has these features

[Eric Wieser]

I don't have a super minimal example, but the head commit of branch#direct_sum_graded-mwe shows the tiny change that I was exploring (the previous commit has everything working, but is ugly)

[Eric Wieser]

(the branch only adds a single new file, so you should be able to just copy that file locally to try it out, if it's not too big to make that undesirable)

[Mario Carneiro]

Not a complete fix, but this cleans up the statements using the sigma type approach a lot

/-! ### Typeclasses -/
section defs

/-- A graded version of `has_one`, which must be of grade 0. -/
class ghas_one [has_zero ι] :=
(one : A 0)

/-- A graded version of `has_one` that also subsumes `distrib` and `mul_zero_class` by requiring
the multiplication be an `add_monoid_hom`. Multiplication combines grades additively, like
`add_monoid_algebra`. -/
class ghas_mul [add_monoid ι] [∀ i, add_comm_monoid (A i)] :=
(mul {i j} : A i →+ A j →+ A (i + j))

def g_one [has_zero ι] [ghas_one A] : Σ i, A i := ⟨_, ghas_one.one⟩

def g_mul [add_monoid ι] [∀ i, add_comm_monoid (A i)] [ghas_mul A] : ∀ (x y : Σ i, A i), Σ i, A i
| ⟨i, x⟩ ⟨j, y⟩ := ⟨i + j, ghas_mul.mul x y⟩

end defs

local notation `ᵍ1` := g_one _
local infix ` ᵍ* `:70 := g_mul _
local prefix `ᵍ↑`:70 := (sigma.mk _ : _ → Σ i, A i)

section defs

/-- A graded version of `monoid`. -/
class gmonoid [add_monoid ι] [∀ i, add_comm_monoid (A i)] extends ghas_mul A, ghas_one A :=
(one_mul (a : Σ i, A i) : ᵍ1 ᵍ* a = a)
(mul_one (a : Σ i, A i) : a ᵍ* ᵍ1 = a)
(mul_assoc (a b c : Σ i, A i) : a ᵍ* b ᵍ* c = a ᵍ* (b ᵍ* c))

/-- A graded version of `comm_monoid`. -/
class gcomm_monoid [add_comm_monoid ι] [∀ i, add_comm_monoid (A i)] extends gmonoid A :=
(mul_comm (a b : Σ i, A i) : a ᵍ* b = b ᵍ* a)

end defs

[Mario Carneiro]

I think the axioms are basically just the monoid axioms this way

[Eric Wieser]

Thanks, I'll see how the proofs further down the file deal with those changes tomorrow

[Mario Carneiro]

This proof isn't perfect but it works

/-- Build a `gmonoid` instance for a collection of `add_submonoids`. -/
def gmonoid.of_submonoids {R : Type*} [semiring R] [add_monoid ι]
  (carriers : ι → add_submonoid R)
  (one_mem : (1 : R) ∈ carriers 0)
  (mul_mem : ∀ ⦃i j⦄ (gi : carriers i) (gj : carriers j), (gi * gj : R) ∈ carriers (i + j)) :
  gmonoid (λ i, carriers i) :=
{ one_mul := λ ⟨i, a, h⟩, begin
    suffices : ∀ j h', j = i → (⟨j, 1 * a, h'⟩ : Σ i, carriers i) = ⟨i, a, h⟩,
    { exact this _ _ (zero_add _) },
    rintro _ _ rfl, simp,
  end,
  mul_one := λ ⟨i, a, h⟩, begin
    suffices : ∀ j h', j = i → (⟨j, a * 1, h'⟩ : Σ i, carriers i) = ⟨i, a, h⟩,
    { exact this _ _ (add_zero _) },
    rintro _ _ rfl, simp,
  end,
  mul_assoc := λ ⟨i, a, ha⟩ ⟨j, b, hb⟩ ⟨k, c, hc⟩, begin
    suffices : ∀ n h h', n = i+(j+k) → (⟨n, a*b*c, h⟩ : Σ i, carriers i) = ⟨i+(j+k), a*(b*c), h'⟩,
    { exact this _ _ _ (add_assoc _ _ _) },
    rintro _ _ _ rfl, simp [mul_assoc],
  end,
  ..ghas_one.of_submonoids carriers one_mem,
  ..ghas_mul.of_submonoids carriers mul_mem }

/-- Build a `gcomm_monoid` instance for a collection of `add_submonoid`s. -/
def gcomm_monoid.of_submonoids {R : Type*} [comm_semiring R] [add_comm_monoid ι]
  (carriers : ι → add_submonoid R)
  (one_mem : (1 : R) ∈ carriers 0)
  (mul_mem : ∀ ⦃i j⦄ (gi : carriers i) (gj : carriers j), (gi * gj : R) ∈ carriers (i + j)) :
  gcomm_monoid (λ i, carriers i) :=
{ mul_comm := λ ⟨i, a, ha⟩ ⟨j, b, hb⟩, begin
    suffices : ∀ n h h', n = j+i → (⟨n, a*b, h⟩ : Σ i, carriers i) = ⟨j+i, b*a, h'⟩,
    { exact this _ _ _ (add_comm _ _) },
    rintro _ _ _ rfl, simp [mul_comm],
  end,
  ..gmonoid.of_submonoids carriers one_mem mul_mem}

[Eric Wieser]

The suffices step is probably not one I would have thought of, but I can see how it solves the problem nicely

[Mario Carneiro]

It's implementing what you said here
Eric Wieser said:

Ultimately my thought was that if I had a goal of the form h.rec a = b, then I could use subst h in tactic mode to reduce it to a = b

[Mario Carneiro]

except without getting to the point of having a rec in the goal

[Mario Carneiro]

It would be maybe better in this case to have a (simp) lemma that reduces equalities on \Sigma i, {x // p i x} to equalities of the first two components

[Mario Carneiro]

and then simp lemmas saying how the .1 and .2.1 components of your definitions unfold

[Mario Carneiro]

that way you never have to see a dependent type

[Eric Wieser]

Mario Carneiro said:

It would be maybe better in this case to have a (simp) lemma that reduces equalities on \Sigma i, {x // p i x} to equalities of the first two components

How about an ext lemma?

@[ext]
lemma sigma.subtype_ext {ι : Sort*} {α : Type*} {p : ι → α → Prop} : ∀
  {a b : Σ i, subtype (p i)}, a.fst = b.fst → (a.snd : α) = b.snd → a = b
| ⟨ai, a, ha⟩ ⟨bi, b, hb⟩ h₁ h₂ :=
begin
  change ai = bi at h₁,
  subst h₁,
  congr,
  exact h₂,
end

[Johan Commelin]

Does that lemma not yet exist? :shock:

[Eric Wieser]

It probably follows from docs#subtype.heq_iff_coe_eq somehow, which was my previous attempt at solving this problem

[Eric Wieser]

Yeah, here's the heq_iff_coe_eq proof:

@[ext]
lemma sigma.subtype_ext' {ι : Sort*} {α : Type*} {p : ι → α → Prop}
  {a b : Σ i, subtype (p i)} (h₁ : a.fst = b.fst) (h₂ : (a.snd : α) = b.snd) : a = b :=
begin
  ext,
  exact h₁,
  refine (heq_iff_coe_eq $ λ x, _).mpr h₂,
  exact h₁.symm ▸ iff.rfl,
end

But I think the other one is nicer

[Eric Wieser]

#6257 for sigma.subtype_ext and three variants.

[Mario Carneiro]

I don't think this can be a @[ext] lemma, it doesn't have a single key

[Mario Carneiro]

the proof is also simpler than that:

lemma sigma.subtype_ext {ι : Sort*} {α : Type*} {p : ι → α → Prop} : ∀
  {a b : Σ i, subtype (p i)}, a.fst = b.fst → (a.snd : α) = b.snd → a = b
| ⟨ai, a, ha⟩ ⟨bi, b, hb⟩ rfl rfl := rfl

[Eric Wieser]

What do you mean by a single key?

[Kevin Buzzard]

Mario Carneiro said:

I don't think this can be a @[ext] lemma, it doesn't have a single key

What does this mean? It's a criterion for deciding when two terms of a type are equal. Isn't that exactly an ext lemma?

[Kevin Buzzard]

snap

[Eric Wieser]

@Mario Carneiro, I tried to iterate towards that short proof, but the equation compiler would give an error while I still had a sorry

[Mario Carneiro]

An ext lemma needs to actually be found when you use ext, it's not just an arbitrary collection of lemmas, it's a lookup table

[Mario Carneiro]

the key of that lookup table is the constant name of the type, and the constant here is Sigma which already has an ext lemma

[Eric Wieser]

Why does the PR not break anything then?

[Mario Carneiro]

When you put multiple ext lemmas it will just try a random one, maybe you got lucky

[Eric Wieser]

And then why are lemmas like docs#linear_map.prod_ext fine, as they overlay another ext lemma on docs#linear_map.ext

[Mario Carneiro]

there isn't any priority system so I expect this will not work robustly

[Eric Wieser]

Doesn't it try all of them until it finds one that applies?

[Mario Carneiro]

yes, if it fails

[Mario Carneiro]

but Sigma.ext would succeed on goals that your new ext lemma work on

[Eric Wieser]

Also, I remember a PR where @Johan Commelin put @[priority] on a bunch of ext lemmas, and we concluded that the default priority was declaration order (and thus removed all the priority attributes again)

[Mario Carneiro]

in that case you can get different behavior depending on the order of imports, which is bad

[Eric Wieser]

Not if file B imports file A anyway

[Eric Wieser]

Which in all the cases that came up, it does

[Mario Carneiro]

Yes. Now do we want to rely on this or not?

[Mario Carneiro]

Any bug can be considered a feature if you look at it in the right way

[Eric Wieser]

#5200 is the PR I'm referring to

[Eric Wieser]

And I think we declared it a feature when writing https://leanprover-community.github.io/mathlib_docs/notes.html#partially-applied%20ext%20lemmas

[Eric Wieser]

Mario Carneiro said:

It would be maybe better in this case to have a (simp) lemma that reduces equalities on \Sigma i, {x // p i x} to equalities of the first two components

I've finally updated #6053 to use this approach, thanks for the suggestions @Mario Carneiro, that definitely ended up cleaner