Targeted Unfolding in a Hypothesis or Goal

Stream: new members

[Joao Bregunci]

I was working a little bit with lists and a few things that I currently working and I found the following goal.

⊢interp I (foldl_head has_inf.inf (sigma' δ₁ :: list.map sigma' Δ₂)) ⊆
  interp I (foldl_head has_sup.sup (sigma' γ :: list.map sigma' (γ₁ :: Γ₂)))

All these functions are implemented in a project by me, but there is not much need to understand this. What I was wondering is if it is possible to use unfold tactic only in a certain portion of the goal. Let's say that I only way to unfold the foldl_head in the second set or only the interp in the first set. I am asking this, because I have a hypothesis that has only one of the terms unfolded and I think that it would be much more easy if I could unfold one of the terms.

And also on the same idea, can this be done for other tactics such as rewrite? This may sound silly, but I have been puzzled by this...

[Yakov Pechersky]

What would you want to unfold? You can write a side lemma saying that foldl_head has_inf.inf ... = ... and use that to rewrite.

[Yakov Pechersky]

If foldl_head is defined casing on the [] and '::`, then you can also try rewriting at the state you have right now. A targeted rewrite is possible via conv mode or nth_rewrite

[Joao Bregunci]

I would want to unfold the second fold_head, so that it would expand to interp I (sigma' γ (has_sup.sup) foldl_head has_sup.sup ( list.map sigma' (γ₁ :: Γ₂))). Which in turn I would want to use my unfolding definition of the second interp to get a hypothesis that I have.

Please what is this conv mode?

[Joao Bregunci]

And this nth_rewrite

[Yakov Pechersky]

https://leanprover-community.github.io/extras/conv.html

[Yakov Pechersky]

conv_rhs { rw [foldl_head] }

[Yakov Pechersky]

https://leanprover-community.github.io/mathlib_docs/tactics.html#nth_rewrite%20/%20nth_rewrite_lhs%20/%20nth_rewrite_rhs

[Yakov Pechersky]

nth_rewrite_rhs 0 [foldl_head]

[Yakov Pechersky]

Do you have a lemma about how foldl_head works on x :: xs?

[Yakov Pechersky]

like

lemma foldl_head_cons (f) (x : α) (xs : list α) : foldl_head f (x :: xs) = f x (foldl_head f xs) := rfl

or whatever your proof would be

[Joao Bregunci]

I defined foldl_head, as actually a foldr :P in which my seed is already an element of the list.

def foldl_head {α} : (α → α → α) → list α → α
  | f (a::ls) := f a (foldl_head f (ls))

[Yakov Pechersky]

Then you could also do rw foldl_head_cons _ (sigma' γ) to do a targeted rewrite

[Joao Bregunci]

Cool, so I just need to use this auxiliary lemma and use nth_rewrite. Thanks :)

[Yakov Pechersky]

If you prove the auxiliary lemma, then you don't even need nth_rewrite, because foldl_head_cons _ (sigma' γ) will only match on the term on the RHS

[Joao Bregunci]

Oh yes, since it is already specified to match with (sigma' γ). But I also found nth_rewrite lovely :)

[Scott Morrison]

Generally speaking, you should not be using unfold yourself unless in exceptional circumstances. Nearly always it it better to rewrite (either by simp or rw, or variants).

[Joao Bregunci]

Why would rewriting and using simp would be preferable? To me it would seem that I would always to sate an auxiliary lemma such as the one that Yakov provided and then use rewrite, effectively achieving the same result and needing to create an auxiliary lemma. What advantage rw would have over unfold?

[Kevin Buzzard]

A proof with an unfold relies on the actual implementation of the definition. What if we decided to change the implementation but then replace the API? The rw proof still works, the unfold one breaks.

[Joao Bregunci]

Interesting, I think I get the idea, but I swill can't understand it very well, because in Yakov lemma, what we are actually is stating isn't that the unfold of the definition is equal to it's application? So what we are actually doing is not the same? And sorry, but I didn't understand what you mean by replacing the API (my background in Computer Science is not that strong)

[Yakov Pechersky]

The auxiliary lemma must be true if your definition performs how you think it should. If you change the definition, then you must amend your auxiliary lemma too. The proof might go from rfl to something more complicated.

[Yakov Pechersky]

Yes, the auxiliary lemma is true by rfl, which means something akin to "by definition". But in your actual main proof, you don't want to rely on "authority by definition". By API we mean here, once you make a definition, provide some simple tools with which you can state _how_ the definition actually works. The auxiliary lemma is part of that API.

[Yakov Pechersky]

You might say, well, "how the definition works" is exactly the definition itself. And for the most simple definitions, yes that is true. But here, as you can already see, your definition is complex enough that there are some layers between how you want to use it, and what you want to prove about it, and what it actually is.

[Joao Bregunci]

I am a little but confused on this sentence "You might say, well, "how the definition works" is exactly the definition itself. And for the most simple definitions, yes that is true". Is there some example that I can see on the auxiliary lemma proof not being simply refl, because I find this extremely weird that it would be hard to prove that the actual definition of something is what is defined to be problematic. I understand that you prefer to use a set of tools "API" and not exactly the definition (this reminds me of getters and setters in OOP). Can there be an example to see how this could be problematic?

[Yakov Pechersky]

In #7118, I changed

/-- Two permutations `f` and `g` are `disjoint` if their supports are disjoint, i.e.,
every element is fixed either by `f`, or by `g`. -/
def disjoint (f g : perm α) := ∀ x, f x = x ∨ g x = x

to

def disjoint (f g : perm α) := disjoint f.support g.support

Understandably, the proof for the API lemma

lemma disjoint_iff_disjoint_support :
  disjoint f g ↔ _root_.disjoint f.support g.support :=
begin
  change (∀ x, f x = x ∨ g x = x) ↔ (∀ x, x ∉ (f.support ∩ g.support)),
  simp_rw [finset.mem_inter, not_and_distrib, mem_support, not_not],
end

became simpler:

lemma disjoint_iff_disjoint_support :
  disjoint f g ↔ _root_.disjoint f.support g.support := iff.rfl

However, I know had to provide some of the old functionality, where, before, one could say

example (h : disjoint f g) : f x = x ∨ g x = x := h x -- using definition of disjoint directly

I now provide an API lemma:

lemma disjoint.def (h : disjoint f g) : ∀ (x : α), f x = x ∨ g x = x :=
begin
  intro x,
  contrapose! h,
  rw [←mem_support, ←mem_support] at h,
  exact λ H, H h
end

so that my example is now

example (h : disjoint f g) : f x = x ∨ g x = x := h.def x -- cannot use definition directly any longer

[Yakov Pechersky]

Let's say you defined foldl in terms of foldr, assuming the appropriate properties of your op, and not through direct recursion over the list. Then your auxiliary lemmas might not be rfl anymore.

[Joao Bregunci]

I think I get the idea of maintain the API, but is still a little bit weird about the original disjoint_iff_disjoint_support proof being so complicated, I don't have a intuition what about that statements requires such a messy proof. But I understand the idea, behind making these auxiliary lemmas and working with definitions, so that I only end working with the API. Out of curiosity, when changing definitions is there often a chain effect breaking many of the lemmas in the API? Couldn't this get problematic that often most of the API would have to be changed when there are changes in the definition?

[Yakov Pechersky]

Making a good definition is the hardest part about formalizing, according to many. If you have a good definition, proving the API you care about it will be easy. And a good definition is changed very rarely. And if you do have to change the definition, hopefully things that interact with it use the API, so the only things you might need to change is API right on top of it, nothing deeper.

[Yakov Pechersky]

the original disjoint_iff_disjoint_support is that "complicated" because _root_.disjoint is a statement about sets and absence of a set intersection, while the original disjoint was a statement about function equality. So there's a negation that has to be put it, and some sort of conversion from/to sets and what support means. You see the same sort of transformation in the reverse direction in my proof of disjoint.def. (The other difference is that I generalized perm.support to be set and not finset.)

[Alexandre Rademaker]

Nice discussion. Maybe a MWE showing the methodology for using lemmas as APIs to definitions would be helpful for many here. Do we have any available material about it? This is interesting because it is about lessons we learn and not about the language itself.