Zulip Chat Archive

Stream: new members

Topic: Standard well-founded tactics on later argument


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 15:16):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 15:20):

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

view this post on Zulip 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 :)

view this post on Zulip Reid Barton (Feb 16 2020 at 16:56):

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

view this post on Zulip Reid Barton (Feb 16 2020 at 16:57):

Or pattern matching let/in or lambda

view this post on Zulip 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) ] }

view this post on Zulip 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")

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Feb 16 2020 at 17:26):

It probably doesn't unfold the id_rhs

view this post on Zulip 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