## Stream: Beginner Questions

### Topic: nested lambda

#### Max Nowak (May 02 2021 at 20:46):

I'm probably missing something simple here, but I can't figure it out on my own. I usually have statements of the form `P (do_thing a s)`, but at some point I need to prove `P (λp. do_thing a (f p) p)` instead (note how s has been replaced with `f p`). I have a helper lemma, which would give me the proof easily, but it requires `bounded s`, or in this case `bounded (f p)`, which I can provide. So, in short, I need something like this:

``````  assumes "⋀p. bounded (f p)"
and "⋀s. bounded s ⟹ P (λp. do_thing a s p)"
shows "P (λp. do_thing a (f p) p)"
``````

And I don't know how to approach this.

#### Jakub Kądziołka (May 02 2021 at 20:48):

your assumption, `⋀s. bounded s ⟹ P (λp. do_thing a s p)`, is too weak. as written, `s` is not allowed to depend on `p`

#### Max Nowak (May 02 2021 at 21:15):

I still can't figure it out. I managed to show `⋀f x. bounded (f x) ==> P (λp. do_thing a (f x) p)`, but replacing `do_thing a (f x)` with `do_thing a (f p)` and it fails to prove.

#### Mathias Fleury (May 03 2021 at 04:55):

Here is how to get the Isabelle version of @Jakub Kądziołka 's error:

``````lemma
assumes "⋀p. bounded (f p)"
and "⋀s. bounded s ⟹ P (λp. do_thing a s p)"
shows "P (λp. do_thing a (f p) p)"
supply [[unify_trace_failure]]
apply (rule assms(2))
(*
Cannot unify variable ?s (depending on bound variables )
with term f p
Term contains additional bound variable(s) p
*)
``````

#### Mathias Fleury (May 03 2021 at 05:01):

In this version `⋀f x. bounded (f x) ==> P (λp. do_thing a (f x) p)` there is still no dependency between `f x` and `p`: whatever `p` is, `f x` does not change. If you get `f p` instead, the proof will work.

#### Mathias Fleury (May 03 2021 at 05:02):

``````  assumes "⋀p. bounded (f p)"
and "⋀(f :: 'a ⇒ 'b) (x :: 'a). bounded (f x) ==> P (λp. do_thing a (f p) p)"
shows "P (λp :: 'a. do_thing a (f p) p)"
apply (rule assms(2))
apply (rule assms(1))
done
``````

#### Max Nowak (May 03 2021 at 18:32):

That's the issue though. I need to prove `⋀(f :: 'a ⇒ 'b) (x :: 'a). bounded (f x) ==> P (λp. do_thing a (f p) p)`, since I am not given that fact.

#### Jakub Kądziołka (May 03 2021 at 18:42):

``````⋀(f :: 'a ⇒ 'b) (x :: 'a). bounded (f x) ==> P (λp. do_thing a (f p) p)
``````

this statement is too strong. You're saying that if, for a specific `x`, `f x` is bounded, then `P (%p. do_thing a (f p) p)` holds, which depends on the boundedness of `f p` for many different `p`, I'd assume

#### Mathias Fleury (May 03 2021 at 18:42):

and we are telling you: without more assumption it does not work

#### Jakub Kądziołka (May 03 2021 at 18:43):

You'd want

``````⋀(f :: 'a ⇒ 'b) (⋀(x :: 'a). bounded (f x)) ==> P (λp. do_thing a (f p) p)
``````

#### Jakub Kądziołka (May 03 2021 at 18:43):

how is `bounded` and `do_thing` defined?

#### Jakub Kądziołka (May 03 2021 at 18:45):

``````  assumes "⋀p. bounded (f p)"
and "⋀s. bounded s ⟹ P (λp. do_thing a s p)"
shows "P (λp. do_thing a (f p) p)"
``````

this inference can never work. Consider `bounded x = True`, `do_thing a s p = s`, `P f = (EX c. f = %x. c)`, `f x = x`

#### Max Nowak (May 03 2021 at 18:48):

bounded is an abbreviation: `bounded r == (0 <= r /\ r <= 1)`, and roughly the `fun` `do_thing a s p = (modify p and return a similar p, same type)`

#### Max Nowak (May 03 2021 at 18:52):

The classes I took never covered ZF axioms, so I have to be honest and say that this goes over my head. I suppose I simply have to change the structure of my proof so that I don't run into this issue.

#### Max Nowak (May 03 2021 at 18:53):

Thanks for the help though!

#### Jakub Kądziołka (May 03 2021 at 18:55):

this is independent of ZF axioms, it's just logic

#### Mathias Fleury (May 03 2021 at 18:56):

maybe the example `has_a_maximum (λp. f p)` with `f p x = x` and `f p _ = p` is easier to understand

#### Max Nowak (May 03 2021 at 18:57):

What's the % syntax?

#### Mathias Fleury (May 03 2021 at 18:58):

a λ I was too lazy to seach for... but that does not type for your definition of bound

Ah, gotcha

#### Mathias Fleury (May 03 2021 at 19:00):

that is what I had in mind:

Mathias Fleury said:

maybe the example `has_a_maximum (λp. f p)` with `f p x = x` and `f p _ = p` is easier to understand

Last updated: Aug 10 2022 at 20:22 UTC