[SOLVED] Propagate `requires` in lambda functions in Dafny

Propagate `requires` in lambda functions in Dafny

How do I prove something about the assumption of a lambda function? I would like to prove the following

lemma propagate_requires(f: int --> int,y:int)
ensures ((x: int) requires f.requires(x) => f(x)).requires(y) == f.requires(y)

This should be obviously true from my understanding. However, Dafny does not propagate the assumption.

How are these requires actually handled by Dafny?

Solution

It is verifiable in one direction but not in opposite direction. This verifies

lemma propagate_requires(f: int --> int,y:int)
  ensures ((x: int) requires f.requires(x) => f(x)).requires(y) <== f.requires(y)
{}

This does n't verify

lemma propagate_requires(f: int --> int,y:int)
  ensures ((x: int) requires f.requires(x) => f(x)).requires(y) ==> f.requires(y)
{}