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.

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`

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.

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
*)
```

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.

```
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
```

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.

```
⋀(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

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

You'd want

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

how is `bounded`

and `do_thing`

defined?

```
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`

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)`

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.

Thanks for the help though!

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

maybe the example `has_a_maximum (λp. f p)`

with `f p x = x`

and `f p _ = p`

is easier to understand

What's the % syntax?

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

Ah, gotcha

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: Dec 07 2023 at 20:16 UTC