Standard well-founded tactics on later argument

Stream: new members

[Anton Lorenzen]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Anton Lorenzen]

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]

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

[Reid Barton]

Or pattern matching let/in or lambda

[Anton Lorenzen]

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]

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]

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]

It probably doesn't unfold the id_rhs

[Floris van Doorn]

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