# Zulip Chat Archive

## 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`

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

#### 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`

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

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`. -/
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 (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_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 (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?

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

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?

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

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