max + 1 not in finset

Stream: new members

[Patrick Thomas]

I was wondering if someone might be able to give me a hint in proving the admit here?

import data.finset

-- a computable function to find an element not in a finset.
def variant : ℕ → finset ℕ → ℕ
| x vars :=
if h : x ∈ vars
then vars.max' (exists.intro x h) + 1
else x

-- a proof that the function returns an element not in the finset.
lemma variant_not_mem (x : ℕ) (s : finset ℕ) : variant x s ∉ s :=
begin
  unfold variant, split_ifs,
  admit,
  assumption
end

[Patrick Thomas]

Or a proof of something equivalent.

[Patrick Thomas]

I think this may be called generating a fresh variable in substitution.

[Ruben Van de Velde]

I would start with contrapose! h

[Patrick Thomas]

I get:

failed to infer type, unexpected bound variable occurrence
state:
2 goals
x : ℕ,
s : finset ℕ
⊢ ∀ (h : x ∈ s), s.max' _ + 1 ∉ s

x : ℕ,
s : finset ℕ,
h : x ∉ s
⊢ x ∉ s

[Ruben Van de Velde]

Hmm. And intros h con?

[Patrick Thomas]

Sorry, no, different error.

[Ruben Van de Velde]

That's all I have while I'm not at lean, maybe something with generalize_proofs will work?

[Ruben Van de Velde]

This seems to work here:

lemma variant_not_mem (x : ℕ) (s : finset ℕ) : variant x s ∉ s :=
begin
  unfold variant, split_ifs,
  { intro con,
    exact (s.le_max' _ con).not_lt (nat.lt_succ_self _) },
  { assumption }
end