well_founded_of_finite

Stream: general

[Johan Commelin]

I feel like the following is true and useful:

import data.set.finite

variables {α : Type*} (r : α → α → Prop)

lemma well_founded_of_finite (h : ∀ a₀, set.finite {a | r a a₀}) :
  well_founded r :=
begin
  sorry
end

How should I go about proving this?

[Mario Carneiro]

it's false

[Mario Carneiro]

total relation on unit

[Johan Commelin]

Hmm, is there a way to make this true?

[Mario Carneiro]

not sure what you are going for exactly

[Johan Commelin]

How about if r is irrefl?

[Mario Carneiro]

it has to be at least acyclic

[Johan Commelin]

transitive and irrefl?

[Mario Carneiro]

sure

[Chris Hughes]

There's a proof that transitive irrefl relations of fintypes are well founded, that can probably be generalised.

[Johan Commelin]

Basically, I have a type that is order isomorphic to nat, but writing down the order isomorphism is a huge pain, whereas proving that {x | x < y} is finite for all y is easy.

[Mario Carneiro]

or applied?

[Mario Carneiro]

The easiest thing would be to prove that it is an order embedding to nat

[Mario Carneiro]

it doesn't need to be an isomorphism

[Johan Commelin]

Even the order embedding is annoying

[Mario Carneiro]

but maybe the trouble is identifying which nat you want to map to

[Johan Commelin]

I'm looking at the lex order on { l : list nat // l.length = n } for a given n.

[Mario Carneiro]

Is the lex order on list nat well ordered?

[Johan Commelin]

But I feel like it's most natural to get a theorem somewhat like my mnwe posted above.

[Johan Commelin]

Is the lex order on list nat well ordered?

I don't know...

[Mario Carneiro]

It is if you read the lists one way and not if you read the lists in reverse

[Mario Carneiro]

there is a counterexample sequence like [1],[0,1],[0,0,1],...

[Mario Carneiro]

You could prove it by induction on n, using the prod well order

[Mario Carneiro]

because the map itself (between nat * vector nat n and vector nat (n+1)) is pretty easy to define

[Johan Commelin]

Aah right, I had that counterexample at some point

[Johan Commelin]

Ooh, sorry. I'm actually looking at { l : list nat // l.sorted \and l.length = n }

[Johan Commelin]

And in that case, all downsets are finite

[Mario Carneiro]

wait, how

[Mario Carneiro]

oh, you beat me to it

[Mario Carneiro]

your proof method would not have worked on vector nat n

[Mario Carneiro]

But you can still use the method I am proposing for that set

[Mario Carneiro]

prove that vector nat n is well ordered and then carve out your subset

[Johan Commelin]

Is the lemma I proposed true? (After adding trans and irrefl hyps)

[Chris Hughes]

lemma well_founded_of_finite [is_irrefl α r] [is_trans α r]
  (h : ∀ a₀, set.finite {a | r a a₀}) : well_founded r :=
⟨λ a₀, acc.intro _ (λ b hb, begin
  cases h a₀ with fint,
  refine @well_founded.fix {a | r a a₀} (λ b, acc r b) (λ x y : {a | r a a₀}, r x y)
    (@fintype.well_founded_of_trans_of_irrefl _ fint
      (λ x y : {a | r a a₀}, r x y) ⟨λ x y z h₁ h₂, trans h₁ h₂⟩
      ⟨λ x, irrefl x⟩) _ ⟨b, hb⟩,
  rintros ⟨b, hb⟩ ih,
  exact acc.intro _ (λ y hy, ih ⟨y, trans hy hb⟩ hy)
end)⟩

[Johan Commelin]

@Chris Hughes Awesome! Thanks!

[Bhavik Mehta]

Is it possible to get the order isomorphism from the above result? I was thinking about similar things for the colex ordering but never got round to actually trying it

[Chris Hughes]

You'd need totality as well for there to be an isomorphism. I don't think it could be done constructively from the above result. The above result is basically proven by defining the map into nat given by the cardinality of the set {a | r a b}.