well-founded exists

Stream: general

[Sean Leather]

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?

[Sean Leather]

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

[Sean Leather]

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

[Sean Leather]

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

[Sean Leather]

I always get confused with these well-founded proofs.

[Sean Leather]

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?

[Simon Hudon]

For the have, what if you had:

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

in your using_well_founded clause?

[Sean Leather]

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

[Sean Leather]

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

[Mario Carneiro]

did Simon's suggestion work?

[Sean Leather]

No.

[Kenny Lau]

what is exp?

[Mario Carneiro]

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

[Sean Leather]

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)

[Mario Carneiro]

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

[Sean Leather]

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

[Mario Carneiro]

make that simp [measure, inv_image]

[Sean Leather]

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)

[Kenny Lau]

I searched inductive.*exp but nothing came up

[Mario Carneiro]

it's in sean's repo

[Sean Leather]

`[simp [measure, inv_image]] >> tactic.assumption,

assumption tactic failed
state:
no goals

[Mario Carneiro]

and drop the asssumption

[Sean Leather]

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

[Sean Leather]

Ah ha!

[Sean Leather]

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

[Sean Leather]

Can I define my own instance of...?

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

[Sean Leather]

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

[Simon Hudon]

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

[Chris Hughes]

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