# Zulip Chat Archive

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