Zulip Chat Archive

Stream: general

Topic: custom well-founded


view this post on Zulip Kenny Lau (Apr 19 2018 at 05:37):

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?

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:37):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:38):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:38):

it's in the wrong direction though

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:38):

swap red.step then

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:39):

what is swap?

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:39):

exactly what it sounds like

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:40):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:40):

oh, I guess it is in function ns

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:40):

right

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:40):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:42):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:42):

No, except perhaps locally if you like

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:42):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:42):

and then I can use recursion?

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:42):

yes

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:43):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:43):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 05:43):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:44):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:44):

I will be doing recurison much

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:46):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 05:46):

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

view this post on Zulip Johannes Hölzl (Apr 19 2018 at 05:53):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:35):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:35):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:35):

@Mario Carneiro

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:37):

try exact this as the tactic instead

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:40):

can I not change the tactic ;_;

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:42):

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

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:42):

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₄

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:43):

keru mouri

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:45):

@Mario Carneiro sauva mi

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:46):

You should use using_well_founded like I said

view this post on Zulip Kenny Lau (Apr 19 2018 at 06:46):

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

view this post on Zulip Mario Carneiro (Apr 19 2018 at 06:46):

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

view this post on Zulip Chris Hughes (Apr 20 2018 at 21:09):

@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.

view this post on Zulip Kenny Lau (Apr 20 2018 at 23:51):

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

view this post on Zulip Kenny Lau (Apr 20 2018 at 23:52):

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)

Last updated: May 16 2021 at 05:21 UTC