custom well-founded

Stream: general

[Kenny Lau]

inductive red.step : list (α × bool) → list (α × bool) → Prop
| bnot {L₁ L₂ x b} : red.step (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂)

How do I tell Lean that whenever red.step L1 L2 is true, it is also true that list.sizeof L2 < list.sizeof L1?

[Kenny Lau]

I don't want to provide a custom proof at the end of every recursion

[Mario Carneiro]

You could prove that red.step itself is well-founded...

[Kenny Lau]

it's in the wrong direction though

[Mario Carneiro]

swap red.step then

[Kenny Lau]

what is swap?

[Mario Carneiro]

exactly what it sounds like

[Mario Carneiro]

it's defined in init.function and swaps a binary operator (aka relation converse)

[Mario Carneiro]

oh, I guess it is in function ns

[Kenny Lau]

right

[Kenny Lau]

so if I prove that swap red.step is well-founded, then I won't have to worry about anything?

[Kenny Lau]

do you suppose I prove has_well_founded (list (α × bool))?

[Mario Carneiro]

No, except perhaps locally if you like

[Kenny Lau]

I mean, is it has_well_founded (list (α × bool)) that I should prove?

[Kenny Lau]

and then I can use recursion?

[Mario Carneiro]

yes

[Kenny Lau]

because "prove well-founded" is kinda vague of an instruction

[Mario Carneiro]

you can also define a well_founded proof and then refer to it in your wf definition using using_well_founded

[Mario Carneiro]

there are several examples of that in mathlib, just look for the keyword

[Kenny Lau]

as I said, I don't want to write a custom proof at the end of every recursion

[Kenny Lau]

I will be doing recurison much

[Kenny Lau]

how would I prove that red.step is well-founded?

[Kenny Lau]

I don't know how to use list lengths to prove that it is well-founded

[Johannes Hölzl]

my first idea would be to use subrelation.wf and inv_image.wf.

[Kenny Lau]

H1 : step L₁ L₄,
⊢ function.swap step L₄ L₁

[Kenny Lau]

Lean's automater couldn't match this with "assumption"

[Kenny Lau]

@Mario Carneiro

[Mario Carneiro]

try exact this as the tactic instead

[Kenny Lau]

can I not change the tactic ;_;

[Kenny Lau]

Now I used λ L₁ L₂, red.step L₂ L₁ as the well-founded relation instead and Lean is giving me ths ;_;

[Kenny Lau]

match failed
state:
α : Type u,
L₃ : list (α × bool),
red.trans : ∀ (_p : Σ' {L₁ L₂ : list (α × bool)} (a : red L₁ L₂), red L₂ L₃), red (_p.fst) L₃,
L₁ L₂ L₄ : list (α × bool),
H1 : step L₁ L₄,
H2 : red L₄ L₂,
H23 : red L₂ L₃
⊢ step L₁ L₄

[Kenny Lau]

keru mouri

[Kenny Lau]

@Mario Carneiro sauva mi

[Mario Carneiro]

You should use using_well_founded like I said

[Kenny Lau]

I don’t want to use it after every single recursion ;_;

[Mario Carneiro]

it's just one line, which you can copy around

[Chris Hughes]

@Kenny Lau

def red : list α → list α → Prop := sorry

axiom red_length (l₁ l₂ : list α) : red l₁ l₂ → l₁.length < l₂.length

lemma red_well_founded : well_founded (@red α) := subrelation.wf red_length
(measure_wf list.length)

This might help if you haven't already worked it out.

[Kenny Lau]

@Chris Hughes thanks, but it still bugs me to provide a proof of well-foundedness

[Kenny Lau]

so in the end I proved

theorem red.sizeof : ∀ {L₁ L₂ : list (α × bool)}, red.step L₁ L₂ → L₂.sizeof < L₁.sizeof

and then in recursions I do:

theorem red.append : ∀ {L₁ L₂ L₃ L₄ : list (α × bool)},
  red L₁ L₃ → red L₂ L₄ → red (L₁ ++ L₂) (L₃ ++ L₄)
| _ _ _ _ red.refl red.refl := red.refl
| _ _ _ _ red.refl (red.step_trans H3 H4) := have _ := red.sizeof H3,
  red.step_trans (red.step.append_left H3) (red.append red.refl H4)
| _ _ _ _ (red.step_trans H1 H2) H3 := have _ := red.sizeof H1,
  red.step_trans (red.step.append_right H1) (red.append H2 H3)