## Stream: general

### Topic: well-founded exists

#### 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?

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

#### Sean Leather (Sep 12 2018 at 11:47):

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

#### Sean Leather (Sep 12 2018 at 11:52):

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

#### Sean Leather (Sep 12 2018 at 11:52):

I always get confused with these well-founded proofs.

#### 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?

#### 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?

#### Sean Leather (Sep 12 2018 at 17:14):

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

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

#### Mario Carneiro (Sep 12 2018 at 18:03):

did Simon's suggestion work?

No.

#### Kenny Lau (Sep 12 2018 at 18:03):

what is exp?

#### Mario Carneiro (Sep 12 2018 at 18:04):

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

#### 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)


#### Mario Carneiro (Sep 12 2018 at 18:04):

actually you should just use  [simp] as the discharger

#### Sean Leather (Sep 12 2018 at 18:05):

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

#### Mario Carneiro (Sep 12 2018 at 18:05):

make that simp [measure, inv_image]

#### 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)


#### Kenny Lau (Sep 12 2018 at 18:06):

I searched inductive.*exp but nothing came up

#### Mario Carneiro (Sep 12 2018 at 18:06):

it's in sean's repo

#### Sean Leather (Sep 12 2018 at 18:06):

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

assumption tactic failed
state:
no goals


#### Mario Carneiro (Sep 12 2018 at 18:07):

and drop the asssumption

#### Sean Leather (Sep 12 2018 at 18:07):

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

Ah ha!

#### Sean Leather (Sep 12 2018 at 18:09):

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

#### 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)


#### 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?

#### 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

#### 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: Dec 20 2023 at 11:08 UTC