Zulip Chat Archive

Stream: general

Topic: well-founded exists


view this post on Zulip Sean Leather (Sep 12 2018 at 11:44):

Can I prove that a recursive definition T → Prop is well-founded if a clause wraps the recursive call with an exists (i.e. f <pattern> := ∃ .., f <subpattern>)? If so, how would I begin to do this?

view this post on Zulip Sean Leather (Sep 12 2018 at 11:45):

Oh, actually, it's not a strict subpattern, it's a function that uses a subpattern. Maybe that's my issue, not the exists.

view this post on Zulip Sean Leather (Sep 12 2018 at 11:47):

So, should I have something like have sizeof (function-calling-subpattern) < sizeof pattern here?

view this post on Zulip Sean Leather (Sep 12 2018 at 11:52):

Okay, never mind, I think I figured out what I need to solve.

view this post on Zulip Sean Leather (Sep 12 2018 at 11:52):

I always get confused with these well-founded proofs.

view this post on Zulip Sean Leather (Sep 12 2018 at 14:40):

So I finally figured out how to prove that my recursion is well-founded. But I think it could be better.

def lc' : exp V  Prop
  | (var fb _)     := fb
  | (app ef ea)    :=
    have depth ef < depth (app ef ea) := by simp,
    have depth ea < depth (app ef ea) := by simp,
    lc' ef  lc' ea
  | (lam v eb)     :=
     (L : finset (tagged V)),
    have depth (open_fresh v L eb) < depth (lam v eb) := by simp [nat.pos_iff_ne_zero'],
    lc' (open_fresh v L eb)
  | (let_ v ed eb) :=
    have depth ed < depth (let_ v ed eb) := by simp,
    lc' ed 
     (L : finset (tagged V)),
    have depth (open_fresh v L eb) < depth (let_ v ed eb) := by simp,
    lc' (open_fresh v L eb)
  using_well_founded {
    dec_tac := tactic.assumption,
    rel_tac := λ_ _, `[exact ⟨_, measure_wf depth] }

It would be nice if I could, say, use simp for the well-founded condition instead of all of those have ... := simps. Also, I tried instance : has_sizeof (exp V) := ⟨depth⟩ so that I wouldn't need to specify rel_tac := λ_ _, `[exact ⟨_, measure_wf depth⟩], but that didn't seem to work. Any suggestions?

view this post on Zulip Simon Hudon (Sep 12 2018 at 14:48):

For the have, what if you had:

 dec_tac := `[simp] >> tactic.assumption,

in your using_well_founded clause?

view this post on Zulip Sean Leather (Sep 12 2018 at 17:14):

@Simon Hudon Good idea, but, unfortunately, that doesn't work.

view this post on Zulip Sean Leather (Sep 12 2018 at 18:01):

@Mario Carneiro Do you have any thoughts on the above in this thread? Basically, I want to write lc' without haveing to redeclare all of these theorems locally. Ideally, I would like to avoid using_well_founded at all, but that's secondary.

view this post on Zulip Mario Carneiro (Sep 12 2018 at 18:03):

did Simon's suggestion work?

view this post on Zulip Sean Leather (Sep 12 2018 at 18:03):

No.

view this post on Zulip Kenny Lau (Sep 12 2018 at 18:03):

what is exp?

view this post on Zulip Mario Carneiro (Sep 12 2018 at 18:04):

Why not? If all your proofs are by simp then it should work as a discharger

view this post on Zulip Sean Leather (Sep 12 2018 at 18:04):

assumption tactic failed
state:
V : Type,
_inst_1 : decidable_eq V,
lc' : exp V  Prop,
lc' : Π (_x : exp V), (Π (_y : exp V), has_well_founded.r _y _x  Prop)  Prop,
ef ea : exp V,
_F : Π (_y : exp V), has_well_founded.r _y (app ef ea)  Prop
 measure depth ef (app ef ea)

view this post on Zulip Mario Carneiro (Sep 12 2018 at 18:04):

actually you should just use `[simp] as the discharger

view this post on Zulip Sean Leather (Sep 12 2018 at 18:05):

That was what I initially tried, too. No luck.

view this post on Zulip Mario Carneiro (Sep 12 2018 at 18:05):

make that simp [measure, inv_image]

view this post on Zulip Sean Leather (Sep 12 2018 at 18:05):

assumption tactic failed
state:
V : Type,
_inst_1 : decidable_eq V,
lc' : exp V  Prop,
lc' : Π (_x : exp V), (Π (_y : exp V), has_well_founded.r _y _x  Prop)  Prop,
ef ea : exp V,
_F : Π (_y : exp V), has_well_founded.r _y (app ef ea)  Prop
 inv_image has_lt.lt depth ef (app ef ea)

view this post on Zulip Kenny Lau (Sep 12 2018 at 18:06):

I searched inductive.*exp but nothing came up

view this post on Zulip Mario Carneiro (Sep 12 2018 at 18:06):

it's in sean's repo

view this post on Zulip Sean Leather (Sep 12 2018 at 18:06):

`[simp [measure, inv_image]] >> tactic.assumption,
assumption tactic failed
state:
no goals

view this post on Zulip Mario Carneiro (Sep 12 2018 at 18:07):

and drop the asssumption

view this post on Zulip Sean Leather (Sep 12 2018 at 18:07):

Kenny, it's an inductive. But it's not relevant to the issue.

view this post on Zulip Sean Leather (Sep 12 2018 at 18:07):

Ah ha!

view this post on Zulip Sean Leather (Sep 12 2018 at 18:09):

That works. Thanks! Any way to simplify away the using_well_founded?

view this post on Zulip Sean Leather (Sep 12 2018 at 18:10):

Can I define my own instance of...?

class has_well_founded (α : Sort u) : Type u :=
(r : α  α  Prop) (wf : well_founded r)

view this post on Zulip Sean Leather (Sep 12 2018 at 18:11):

I mean, will defining an instance of has_well_founded allow me to remove using_well_founded?

view this post on Zulip Simon Hudon (Sep 13 2018 at 14:09):

I think so. You may also have to set the priority of has_well_founded_of_has_sizeof to 0

view this post on Zulip Chris Hughes (Sep 13 2018 at 14:12):

I did this for polynomials. I had to write dec_tac := tactic.assumption everywhere, but other than that it worked.


Last updated: May 08 2021 at 19:11 UTC