## Stream: Is there code for X?

### Topic: Unfolding let bindings in hypotheses

#### Eric Wieser (Feb 15 2021 at 23:44):

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 (Feb 15 2021 at 23:48):

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

#### Eric Wieser (Feb 15 2021 at 23:49):

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

#### Mario Carneiro (Feb 15 2021 at 23:49):

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

#### Mario Carneiro (Feb 15 2021 at 23:49):

no, there's a missing piece

#### Mario Carneiro (Feb 15 2021 at 23:50):

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

#### Eric Wieser (Feb 15 2021 at 23:51):

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

#### Mario Carneiro (Feb 15 2021 at 23:51):

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 (Feb 15 2021 at 23:52):

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

#### Mario Carneiro (Feb 15 2021 at 23:52):

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

#### Mario Carneiro (Feb 15 2021 at 23:52):

these should be have

#### Eric Wieser (Feb 15 2021 at 23:54):

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 (Feb 15 2021 at 23:55):

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

#### Mario Carneiro (Feb 15 2021 at 23:55):

This kind of looks like an #xy problem though

#### Mario Carneiro (Feb 15 2021 at 23:55):

as_goal can be proved by rfl straight off

#### Eric Wieser (Feb 15 2021 at 23:58):

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 (Feb 15 2021 at 23:58):

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

#### Eric Wieser (Feb 15 2021 at 23:59):

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

#### Mario Carneiro (Feb 15 2021 at 23:59):

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 (Feb 16 2021 at 00:00):

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 (Feb 16 2021 at 00:01):

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

#### Eric Wieser (Feb 16 2021 at 00:03):

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 (Feb 16 2021 at 00:04):

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

#### Mario Carneiro (Feb 16 2021 at 00:06):

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

docs#fin.cast

#### Eric Wieser (Feb 16 2021 at 00:06):

fin was solely for the case of this mwe

#### Mario Carneiro (Feb 16 2021 at 00:06):

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

#### Eric Wieser (Feb 16 2021 at 00:07):

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

#### Mario Carneiro (Feb 16 2021 at 00:08):

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

#### Eric Wieser (Feb 16 2021 at 00:08):

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

#### Mario Carneiro (Feb 16 2021 at 00:09):

No, it uses type equalities which are to be avoided

#### Mario Carneiro (Feb 16 2021 at 00:09):

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

#### Eric Wieser (Feb 16 2021 at 00:09):

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

you should

#### Mario Carneiro (Feb 16 2021 at 00:10):

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

#### Mario Carneiro (Feb 16 2021 at 00:10):

in particular one side has to be a variable

#### Eric Wieser (Feb 16 2021 at 00:11):

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

#### Mario Carneiro (Feb 16 2021 at 00:11):

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

#### Mario Carneiro (Feb 16 2021 at 00:11):

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

#### Mario Carneiro (Feb 16 2021 at 00:12):

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

#### Eric Wieser (Feb 16 2021 at 00:15):

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 (Feb 16 2021 at 00:16):

(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 (Feb 16 2021 at 00:52):

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. -/
(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 (Feb 16 2021 at 00:53):

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

#### Eric Wieser (Feb 16 2021 at 01:02):

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

#### Mario Carneiro (Feb 16 2021 at 01:08):

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_submonoids. -/
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 (Feb 16 2021 at 01:21):

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

#### Mario Carneiro (Feb 16 2021 at 01:31):

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 (Feb 16 2021 at 01:31):

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

#### Mario Carneiro (Feb 16 2021 at 01:32):

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 (Feb 16 2021 at 01:33):

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

#### Mario Carneiro (Feb 16 2021 at 01:33):

that way you never have to see a dependent type

#### Eric Wieser (Feb 16 2021 at 10:16):

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 (Feb 16 2021 at 10:18):

Does that lemma not yet exist? :shock:

#### Eric Wieser (Feb 16 2021 at 10:20):

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

#### Eric Wieser (Feb 16 2021 at 10:24):

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 (Feb 16 2021 at 10:39):

#6257 for sigma.subtype_ext and three variants.

#### Mario Carneiro (Feb 16 2021 at 18:45):

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

#### Mario Carneiro (Feb 16 2021 at 18:47):

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 (Feb 16 2021 at 18:49):

What do you mean by a single key?

#### Kevin Buzzard (Feb 16 2021 at 18:50):

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?

snap

#### Eric Wieser (Feb 16 2021 at 18:52):

@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 (Feb 16 2021 at 19:07):

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 (Feb 16 2021 at 19:08):

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 (Feb 16 2021 at 19:09):

Why does the PR not break anything then?

#### Mario Carneiro (Feb 16 2021 at 19:09):

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

#### Eric Wieser (Feb 16 2021 at 19:09):

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 (Feb 16 2021 at 19:09):

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

#### Eric Wieser (Feb 16 2021 at 19:09):

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

yes, if it fails

#### Mario Carneiro (Feb 16 2021 at 19:10):

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

#### Eric Wieser (Feb 16 2021 at 19:10):

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 (Feb 16 2021 at 19:11):

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

#### Eric Wieser (Feb 16 2021 at 19:12):

Not if file B imports file A anyway

#### Eric Wieser (Feb 16 2021 at 19:12):

Which in all the cases that came up, it does

#### Mario Carneiro (Feb 16 2021 at 19:12):

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

#### Mario Carneiro (Feb 16 2021 at 19:13):

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

#### Eric Wieser (Feb 16 2021 at 19:13):

#5200 is the PR I'm referring to

#### Eric Wieser (Feb 16 2021 at 19:15):

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 (Feb 22 2021 at 18:17):

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

Last updated: May 19 2021 at 00:40 UTC