# Zulip Chat Archive

## Stream: new members

### Topic: Targeted Unfolding in a Hypothesis or Goal

#### Joao Bregunci (Apr 12 2021 at 20:06):

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 (Apr 12 2021 at 20:19):

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 (Apr 12 2021 at 20:22):

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 (Apr 12 2021 at 20:24):

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 (Apr 12 2021 at 20:25):

And this `nth_rewrite`

#### Yakov Pechersky (Apr 12 2021 at 20:25):

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

#### Yakov Pechersky (Apr 12 2021 at 20:26):

`conv_rhs { rw [foldl_head] }`

#### Yakov Pechersky (Apr 12 2021 at 20:27):

#### Yakov Pechersky (Apr 12 2021 at 20:27):

`nth_rewrite_rhs 0 [foldl_head]`

#### Yakov Pechersky (Apr 12 2021 at 20:28):

Do you have a lemma about how `foldl_head`

works on `x :: xs`

?

#### Yakov Pechersky (Apr 12 2021 at 20:30):

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 (Apr 12 2021 at 20:30):

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 (Apr 12 2021 at 20:31):

Then you could also do `rw foldl_head_cons _ (sigma' γ)`

to do a targeted rewrite

#### Joao Bregunci (Apr 12 2021 at 20:34):

Cool, so I just need to use this auxiliary lemma and use `nth_rewrite`

. Thanks :)

#### Yakov Pechersky (Apr 12 2021 at 20:35):

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 (Apr 12 2021 at 20:37):

Oh yes, since it is already specified to match with `(sigma' γ)`

. But I also found `nth_rewrite`

lovely :)

#### Scott Morrison (Apr 12 2021 at 23:37):

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 (Apr 13 2021 at 14:25):

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 (Apr 13 2021 at 14:26):

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 (Apr 13 2021 at 14:33):

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 (Apr 13 2021 at 14:36):

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 (Apr 13 2021 at 14:38):

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 (Apr 13 2021 at 14:39):

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 (Apr 13 2021 at 14:55):

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 (Apr 13 2021 at 15:01):

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 (Apr 13 2021 at 15:03):

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 (Apr 13 2021 at 23:31):

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 (Apr 14 2021 at 00:23):

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 (Apr 14 2021 at 00:26):

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 (Apr 15 2021 at 04:17):

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.

Last updated: May 13 2021 at 22:15 UTC