Zulip Chat Archive

Stream: new members

Topic: Accesibility of lexical order of lists


AHan (Nov 27 2018 at 15:19):

I've seen there are proofs for accessibility and well-founded for lexical order of product
And I also find out there is a definition for lexical order of list, but I can't find any proofs for it's accessibility and well-founded...
Are them provided in other names or just not yet proved?

And if I were going to prove the accessibility of lexical order of list, I'm not quite sure what the type of the lemma should be, and when to use functions like acc.rec_on, acc.intro....
( Is the type of the lemma like... this ?)

variables {α : Type*} (ra  : α  α  Prop)
def list_lex_acc : (ha :  a : α, acc ra a) :  a : list α, acc (list.lex ra) a := sorry

Kevin Buzzard (Nov 27 2018 at 15:58):

Nice question! If you write ```lean when quoting code then you get syntax highlighting as well. Here's a version of your question which typechecks straight out the box:

import data.list.basic

variables {α : Type*} (ra : α  α  Prop)
theorem list_lex_acc (ha :  a : α, acc ra a) :
 a : list α, acc (list.lex ra) a := sorry

Kevin Buzzard (Nov 27 2018 at 16:02):

Off the top of my head, I guess some useful lemmas would be to prove that there are no solutions to x < [], and then you could start proving that all lists of positive size were accessible by induction on first the length of the list, and secondly using well-founded induction on the first element of the list.

AHan (Nov 27 2018 at 16:04):

Thanks for the suggestion!
And are there any differences between using def and theorem here ?
Because in mathlib they used def for well_founded and accessibility of lexical order of product

AHan (Nov 27 2018 at 16:07):

"well-founded induction" do you mean something like well_founded.rec_on?

Reid Barton (Nov 27 2018 at 16:07):

I think you mean in the Lean core library (def lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) := ...)?

Reid Barton (Nov 27 2018 at 16:08):

There is a difference. I don't know why they used def, though

Kevin Buzzard (Nov 27 2018 at 16:08):

I just used theorem because the thing you want to prove has type Prop.

AHan (Nov 27 2018 at 16:09):

@Reid Barton Yes!

Kevin Buzzard (Nov 27 2018 at 16:12):

lemma not_lt_empty (ra : α  α  Prop) (a : list α) :
¬ (list.lex ra a []) := by intro H; cases H

There will be shorter proofs :-) I'm doing induction on list.lex here.

Kevin Buzzard (Nov 27 2018 at 16:13):

got it:

lemma not_lt_empty (ra : α  α  Prop) (a : list α) :
¬ (list.lex ra a []) .

Kevin Buzzard (Nov 27 2018 at 16:14):

oh no wait, lean segfaulted :D

AHan (Nov 27 2018 at 16:14):

I can solve this case by

theorem list_lex_acc (ha :  a : α, acc ra a) :  a : list α, acc (list.lex ra) a :=
λ a,
begin
    cases a,
    apply acc.intro, intros, cases a,
...
end

but I'm stuck at the second part, doing well-founded induction on the first element of the list...

Kevin Buzzard (Nov 27 2018 at 16:17):

Yeah it's messy now. I am at work and need to think about other things :-/

This . proof works for me.

import data.list.basic

variables {α : Type*} (ra : α  α  Prop)

lemma not_lt_empty (ra : α  α  Prop) (a : list α) :
¬ (list.lex ra a []) .

AHan (Nov 27 2018 at 16:20):

Wow.... what's . proof ...

Kevin Buzzard (Nov 27 2018 at 16:20):

But this exact file gives me a segfault:

import data.list.basic

variables {α : Type*} (ra : α  α  Prop)
theorem list_lex_acc (ha :  a : α, acc ra a) :
 a : list α, acc (list.lex ra) a := sorry

lemma not_lt_empty (ra : α  α  Prop) (a : list α) :
¬ (list.lex ra a []) .

with Lean (version 3.4.1, commit 17fe3decaf8a, Release).

Kevin Buzzard (Nov 27 2018 at 16:21):

The . proof says "Check all the cases...actually, can't you see that there are no cases to check?". The equation compiler looks at all the constructors for list.lex and rules out [] appearing on the right hand side.

Reid Barton (Nov 27 2018 at 16:21):

Doesn't segfault for me with the same version of lean

Kevin Buzzard (Nov 27 2018 at 16:22):

I have a blank line 9

Kevin Buzzard (Nov 27 2018 at 16:22):

I can restart Lean and consistently get it to segfault. On linux.

AHan (Nov 27 2018 at 16:24):

No segfault with the same version of lean either... (on windows

Kevin Buzzard (Nov 27 2018 at 16:26):

I restarted VS Code and the problem has gone away shrug

AHan (Nov 27 2018 at 16:35):

Oh I crashed on

import data.list.basic
variables {α : Type*} (ra  : α  α  Prop)

theorem list_lex_acc (ha :  a : α, acc ra a) :  a : list α, acc (list.lex ra) a := sorry

lemma not_lt_empty (ra : α  α  Prop) (a : list α) : ¬ (list.lex ra a []) .

but it works fine if I swap the lemma and the theorem...

import data.list.basic
variables {α : Type*} (ra  : α  α  Prop)

lemma not_lt_empty (ra : α  α  Prop) (a : list α) : ¬ (list.lex ra a []) .

theorem list_lex_acc (ha :  a : α, acc ra a) :  a : list α, acc (list.lex ra) a := sorry

Kevin Buzzard (Nov 27 2018 at 19:40):

Hmm. I think I found an infinite decreasing sequence! [1] > [0,1] > [0,0,1] > [0,0,0,1] > .... So that will be why it's not in the library.

Mario Carneiro (Nov 27 2018 at 20:20):

Interesting. I think it's well founded if you reverse the order: [] < x :: xs, and x :: xs < y :: ys if xs < ys or xs = ys and x < y

Kenny Lau (Nov 27 2018 at 20:20):

I don't recall having a "list" operation on ordinals...

Kenny Lau (Nov 27 2018 at 20:21):

it would be list(x) = 1 + x + x^2 + x^3 + ...

Mario Carneiro (Nov 27 2018 at 20:21):

I do: CNF (although I don't see the relevance)

Kenny Lau (Nov 27 2018 at 20:22):

but then it would be list(x) = x^omega but power in ordinal doesn't correspond to power in cardinal

Mario Carneiro (Nov 27 2018 at 20:23):

right, I think the list ordering I gave has order type (type A)^omega

Kenny Lau (Nov 27 2018 at 20:24):

so it wouldn't be correct

Kenny Lau (Nov 27 2018 at 20:24):

because there is no x^cardinal.omega in ordinals

Mario Carneiro (Nov 27 2018 at 20:26):

what are you talking about?

Mario Carneiro (Nov 27 2018 at 20:27):

x^omega is perfectly well defined

Mario Carneiro (Nov 27 2018 at 20:27):

it's an ordinal power

Kenny Lau (Nov 27 2018 at 20:27):

but is it in bijection with x^cardinal.omega?

Mario Carneiro (Nov 27 2018 at 20:27):

no... it's lists not infinite sequences

Kenny Lau (Nov 27 2018 at 20:27):

ah

Kenny Lau (Nov 27 2018 at 20:28):

Interesting. I think it's well founded if you reverse the order: [] < x :: xs, and x :: xs < y :: ys if xs < ys or xs = ys and x < y

feels like hilbert basis theorem now

AHan (Nov 28 2018 at 06:54):

So maybe we'll need a different definition for the lexical order of list in order to prove it's well-founded?

AHan (Nov 29 2018 at 11:19):

I ‘ve modified the lex of list as below

import data.list.basic
import data.set.lattice
open lattice

variables {α : Type*} (ra  : α  α  Prop)

inductive lex (r : α  α  Prop) : list α  list α  Prop
| nil {} {a l} : lex [] (a :: l)
| rel {a₁ a₂} (l₁ l₂ : list α) (h₁ : r a₁ a₂) (h₂ : l₁.length  l₂.length) : lex (a₁ :: l₁) (a₂ :: l₂)
| cons {a l₁ l₂} (h : lex l₁ l₂) : lex (a :: l₁) (a :: l₂)

lemma lex_acc_of_lex :  a b : list α, lex ra a b  acc (lex ra) a
| _ [] h := by cases h
| [] _ h := by apply list_nil_acc
| (a :: l₁) (b :: l₂) h :=  sorry

But I don't know how to tell lean that the recursion application will decrease....

Kenny Lau (Nov 29 2018 at 12:10):

prove it? lol


Last updated: Dec 20 2023 at 11:08 UTC