Optional argmin

Stream: new members

[Rémi Bottinelli]

Hey! I asked a similar question some time ago, but I don't think I got it right yet. I'm looking for a way to do the following:

constants X Y : Type*
constant f : X → ℕ
constant g : Y → set X

def optional_least (y : Y) : option X :=
if h : (g y).nonempty then
  some $ argmin_on f _ (g y) h
else
  none

def optional_least_isleast (y : Y) :
  ∀ x ∈ (g y), f (optional_least y).unwrap ≤ x

That is, I have a function g : Y \to set X mapping some type Y to subsets in some other type X, and a "ranking" function f: X \to \N on that latter type. Essentially, I want to extract a minimal witness of non-emptiness, if it exists.
I understand this is probably non computable, but I cannot find a way to make it typecheck…