Contractivity tactic #123
Description
One useful tactic in Iris is f_contractive, for proving that a given function is contractive. This tactic is commonly used in the definition of weakest preconditions, for example here.
In my experience, this tactic is somewhat fragile (see how we use it in Clutch). We could try porting it directly, but I think we could see if the existing Lean solvers like grind or appropriately defined simpproc's could help us discharge these goals automatically.