## Stream: new members

### Topic: Can conv be used to use nested hypotheses?

#### Abhimanyu Pallavi Sudhir (Dec 04 2018 at 22:27):

The situation is as follows: I have a proof of:

convertor :
∀ (h : ℝ),
h ≠ 0 → (f (g (x + h)) - f (g h)) / h = (f (g (x + h)) - f (g h)) / (g (x + h) - g x) * (g (x + h) - g x) / h


And I have the following goal in which I need to perform a rewrite using convertor:

∀ (ε : ℝ),
ε > 0 →
(∃ (δ : ℝ) (H : δ > 0),
∀ (h : ℝ),
h ≠ 0 → abs h < δ → abs ((f (g (x + h)) - f (g x)) / h - (λ (x : ℝ), f' (g x) * g' x) x) < ε)


Within the goal, we have the nested hypothesis  ∀ (h : ℝ), h ≠ 0 which is needed to apply convertor. But I can't perform this rewrite without unfolding everything.

#### Kenny Lau (Dec 04 2018 at 22:28):

simp only [convertor]

Doesn't work.

#### Abhimanyu Pallavi Sudhir (Dec 04 2018 at 22:31):

Oh wait, there's a typo in my convertor -- nope, still doesn't work.

#### Kenny Lau (Dec 04 2018 at 22:31):

simp only [convertor] {contextual:=tt}

#### Abhimanyu Pallavi Sudhir (Dec 04 2018 at 22:33):

Still doesn't work.

#### Abhimanyu Pallavi Sudhir (Dec 04 2018 at 22:35):

What exactly would simp be doing behind the scenes here? Something involving conv? Or something else? Is there any way that I can dig into it the way simp is supposed to work?

#### Kevin Buzzard (Dec 04 2018 at 22:44):

See if forall h, h ne 0 -> X = Y can ever be used to rewrite forall h, h ne 0 -> something else -> X = Z maybe? I mean do some experiments. If the rewrite never works you could ask on #general...oh, I just noticed that you're asking on the main chat anyway :-) sorry.

#### Patrick Massot (Dec 05 2018 at 08:42):

@Abhimanyu Pallavi Sudhir this is typically a case where you need to paste a MWE if you really want help. Reluctant rewriting is a complicated topic, and the answer very much depends on the specific situation. Meanwhile you can learn a couple of important lessons:

#### Patrick Massot (Dec 05 2018 at 08:44):

When using Lean, you need to reconsider every side assumption. They will be a pain, whatever the situation, and we have all sorts of tricks to avoid them. One of Kevin's favorite ones is how division is totalized. You convertor lemma (without typos) does not need assumptions, thanks to the division trick:

lemma convertor (x : ℝ) (f g : ℝ → ℝ):
∀ (h : ℝ),
(f (g (x + h)) - f (g x)) / h = (f (g (x + h)) - f (g x)) / (g (x + h) - g x) * (g (x + h) - g x) / h :=
begin
intros,
by_cases H : g (x+h) - g x = 0,
{ rw [H, mul_zero, zero_div, eq_of_sub_eq_zero H, sub_self, zero_div] },
{ rwa div_mul_cancel },
end


#### Patrick Massot (Dec 05 2018 at 08:46):

The other lesson is that you shouldn't be doing all those computations, you should have better infrastructure. This is why I should be working on the big-O/little-o library, but I don't have enough time (but maybe you don't know yet this technology)

#### Kenny Lau (Dec 05 2018 at 09:13):

well I find it useful that f is differentiable at p iff f(p+h) = f(p) + h f1(h) for some f1 continuous at 0 with f1(0) = f'(p). Chain rule follows immediately:
1. for all h, f(p+h) = f(p) + h f1(h) with f1 continuous and f1(0) = f'(p)
2. for all h, g(f(p)+h) = g(f(p)) + h g1(h) with g1 continuous and g1(0) = g'(f(p))
3. for all h, g(f(p+h)) = g(f(p) + h f1(h)) = g(f(p)) + h f1(h) g1(h f1(h)), and then f1(h) g1(h f1(h)) is continuous at 0, and also f1(0) g1(0 f1(0)) = f'(p) g'(f(p))

#### Patrick Massot (Dec 05 2018 at 09:49):

We already discussed that trick here. What you wrote is the full extent of what it can do, and you'll have to prove this is equivalent to the usual definition (which is more convenient for everything else) anyway, so the gain is not even that large.

#### Patrick Massot (Dec 05 2018 at 09:51):

Of course all this (the explicit computation with quotient and the exotic definition of derivatives) is perfectly fine for experimentation purposes, what I'm describing is the library building point of view

#### Kevin Buzzard (Dec 05 2018 at 10:59):

Abhi is (perhaps at my suggestion) working on a simple library for differentiating functions of one real variable. I know that others have promised some much better things, but Abhi is a first year undergraduate and we are just experimenting and learning as we go. Does anyone know how this stuff is done in Coq, or any other system which implements dependent type theory in pretty much the same general way as Lean? In fact, which other systems have this property? I'm sure Isabelle will have this stuff, but my understanding is that Isabelle has a very different kind of type theory. How do I go about finding out how this stuff is implemented in Coq? Is it easiest to just ask on some Coq mailing list? Is https://github.com/coq-contribs any use? I would like to know more about what has been done before. Is Coq the only system that is similar enough to Lean to make a comparison worthwhile?

#### Abhimanyu Pallavi Sudhir (Dec 05 2018 at 11:14):

@Abhimanyu Pallavi Sudhir this is typically a case where you need to paste a MWE if you really want help. Reluctant rewriting is a complicated topic, and the answer very much depends on the specific situation. Meanwhile you can learn a couple of important lessons:

Thanks @Patrick Massot -- I tried using ring and it didn't work, so I decided that the division by zero trick didn't work for some reason. I would've posted an MWE, but it was a bit large -- I'll try the experiments @Kevin Buzzard suggested to get a better feel of contextual rewrites.

#### Patrick Massot (Dec 05 2018 at 13:26):

As I wrote, I know this is only experimentation, but I hope it's still useful to have information from the library point of view. The chain rule in Coq is at https://github.com/math-comp/analysis/blob/master/derive.v#L699-L702. I think Isabelle is already a bit too different for comparing here.

#### Patrick Massot (Dec 05 2018 at 13:28):

Well, it's more honest to point to https://github.com/math-comp/analysis/blob/master/derive.v#L687-L697

Last updated: May 11 2021 at 22:14 UTC