Zulip Chat Archive

Stream: Is there code for X?

Topic: Unfolding let bindings in hypotheses


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 15 2021 at 23:49):

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

view this post on Zulip Mario Carneiro (Feb 15 2021 at 23:49):

no, there's a missing piece

view this post on Zulip Mario Carneiro (Feb 15 2021 at 23:50):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 15 2021 at 23:52):

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

view this post on Zulip Mario Carneiro (Feb 15 2021 at 23:52):

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

view this post on Zulip Mario Carneiro (Feb 15 2021 at 23:52):

these should be have

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 15 2021 at 23:55):

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

view this post on Zulip Mario Carneiro (Feb 15 2021 at 23:55):

This kind of looks like an #xy problem though

view this post on Zulip Mario Carneiro (Feb 15 2021 at 23:55):

as_goal can be proved by rfl straight off

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 15 2021 at 23:58):

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

view this post on Zulip Eric Wieser (Feb 15 2021 at 23:59):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:06):

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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:06):

docs#fin.cast

view this post on Zulip Eric Wieser (Feb 16 2021 at 00:06):

fin was solely for the case of this mwe

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:06):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:08):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:09):

No, it uses type equalities which are to be avoided

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:09):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:09):

you should

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:10):

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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:10):

in particular one side has to be a variable

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:11):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:12):

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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 00:53):

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

view this post on Zulip Eric Wieser (Feb 16 2021 at 01:02):

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

view this post on Zulip 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}

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 01:31):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 01:33):

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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 01:33):

that way you never have to see a dependent type

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 16 2021 at 10:18):

Does that lemma not yet exist? :shock:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 16 2021 at 10:39):

#6257 for sigma.subtype_ext and three variants.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 16 2021 at 18:49):

What do you mean by a single key?

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 18:50):

snap

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 16 2021 at 19:09):

Why does the PR not break anything then?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 19:09):

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

view this post on Zulip Eric Wieser (Feb 16 2021 at 19:09):

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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 19:10):

yes, if it fails

view this post on Zulip Mario Carneiro (Feb 16 2021 at 19:10):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 16 2021 at 19:12):

Not if file B imports file A anyway

view this post on Zulip Eric Wieser (Feb 16 2021 at 19:12):

Which in all the cases that came up, it does

view this post on Zulip Mario Carneiro (Feb 16 2021 at 19:12):

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

view this post on Zulip Mario Carneiro (Feb 16 2021 at 19:13):

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

view this post on Zulip Eric Wieser (Feb 16 2021 at 19:13):

#5200 is the PR I'm referring to

view this post on Zulip 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

view this post on Zulip 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