nested lambda · Beginner Questions

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

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

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

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

⋀(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):

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

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

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

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