## Stream: new members

### Topic: Standard well-founded tactics on later argument

#### Anton Lorenzen (Feb 16 2020 at 15:15):

I have a function that takes several arguments and I have to pattern match on all of them. When I try to use recursion, Lean tries to prove well-foundedness on the first argument, but I want to use the standard well-foundedness (by size) on the last argument (of six). Do you know how I can configure my rel_tac to achieve that?

#### Kevin Buzzard (Feb 16 2020 at 15:16):

All I know is this but there are people who know more

#### Chris Hughes (Feb 16 2020 at 15:17):

Does using_well_founded { rel_tac := λ _ _, [exact ⟨_, measure_wf (λ x, x.2.2.2.2.2.sizeof)⟩ ] } work?

#### Kevin Buzzard (Feb 16 2020 at 15:20):

using_well_founded
{ rel_tac := λ _ _, [exact ⟨_, measure_wf (λ x, x.2.2.2.2.2.sizeof)⟩ ] }


#### Anton Lorenzen (Feb 16 2020 at 15:37):

Yep, it did! I am using a type family so I had to specify the arguments to sizeof as in:

using_well_founded { rel_tac := λ _ _, [exact ⟨_, measure_wf (λ j, begin
cases j with g j, cases j with x j, cases j with a j, cases j with b j,
cases j with t j, exact Judgement.sizeof g (Exp.pi x a b) t j, end)⟩ ] }


Thanks :)

#### Reid Barton (Feb 16 2020 at 16:56):

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#rcases

#### Reid Barton (Feb 16 2020 at 16:57):

Or pattern matching let/in or lambda

#### Anton Lorenzen (Feb 16 2020 at 17:10):

Thanks. It is a bit weird though. Lean is happy with this:

using_well_founded { rel_tac := λ _ _, [exact ⟨_, measure_wf (λ j, begin
rcases j with ⟨g, ⟨x, ⟨a, ⟨b, ⟨t, j⟩⟩⟩⟩⟩, exact Judgement.sizeof g (Exp.pi x a b) t j, end)⟩ ] }


But not with:

using_well_founded { rel_tac := λ _ _, [exact ⟨_, measure_wf
(λ ⟨g, ⟨x, ⟨a, ⟨b, ⟨t, j⟩⟩⟩⟩⟩, Judgement.sizeof g (Exp.pi x a b) t j)⟩ ] }


#### Anton Lorenzen (Feb 16 2020 at 17:11):

It says it can't show

⊢ id_rhs ℕ (Judgement.sizeof g (Exp.pi x a b) _x tr) <
id_rhs ℕ
(Context.sizeof g +
(Exp.sizeof a +
(Exp.sizeof b +
(Exp.sizeof t +
(Exp.sizeof _x +
(PTSSort.sizeof _x +
(string.length x +
(BetaExp.sizeof _x t _x +
(2 +
(Judgement.sizeof g t (Exp.sort _x) _x +
Judgement.sizeof g (Exp.pi x a b) _x tr))))))))))


(Which is true since the lhs term occurs on the rhs too and there is a "+2")

#### Anton Lorenzen (Feb 16 2020 at 17:21):

What is the policy on Lean bug reports btw? Should I report something like this to the github.com/lean-community/lean repo?

#### Chris Hughes (Feb 16 2020 at 17:26):

It probably doesn't unfold the id_rhs

#### Floris van Doorn (Feb 17 2020 at 21:33):

Yes, the best place for bug reports about Lean (if it is not related to mathlib) is https://github.com/leanprover-community/lean/issues

Last updated: May 16 2021 at 05:21 UTC