Zulip Chat Archive

Stream: new members

Topic: Proving recursive application is decreasing?

Harrison Grodin (Sep 08 2020 at 05:30):

I'm attempting to write the flip function on the following inductive type:

inductive foo : nat  nat  Prop
| refl     :  M, foo M M
| symm     :  M M', foo M M'  foo M' M
| trans    :  M M' M'', foo M M'  foo M' M''  foo M M''

def flip :  n m : nat, foo n m  foo m n
| _ _ (foo.refl M) := foo.refl M
| _ _ (foo.symm M M' h) := foo.symm M' M (flip M M' h)
| _ _ (foo.trans M M' M'' h h') := foo.trans M'' M' M (flip M' M'' h') (flip M M' h)

However, I end up with failed to prove recursive application is decreasing, well founded relation in the symm and trans cases, requesting that I prove M' < M and (even more problematically) M < M.

Does anyone have an idea as to how I could fix this? I tried using_well_founded, but I couldn't get it to work.

Anne Baanen (Sep 08 2020 at 10:04):

By default equation compiler will try to prove your definition terminates by mapping the tuple of all arguments to a natural number using has_sizeof, and showing that number strictly decreases between recursive calls. Unfortunately, we can't assign a has_sizeof to foo by pattern-matching because again we cannot yet prove it will terminate.

The solution is to use the recursion principle of foo directly, which is called foo.rec_on.

Donald Sebastian Leung (Sep 09 2020 at 01:49):

Isn't flip just foo.symm?

Eric Wieser (Dec 22 2021 at 17:27):

It seems that the default well_founded tactic doesn't know how to deal with inductive props, since their sizeof is 0:

inductive foo :     Prop
| zero_one : foo 0 1
| symm {x y} : foo x y  foo y x

lemma easy :  x, foo x 1  x = 0
| x (foo.zero_one) := rfl
| x (foo.symm (foo.symm h)) := easy x h

gives the error:

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (Σ' (x : ), foo x 1)
    (@has_well_founded_of_has_sizeof (Σ' (x : ), foo x 1) (default_has_sizeof (Σ' (x : ), foo x 1)))
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
default_dec_tac failed
easy :  (_p : Σ' (x : ), foo x 1), _p.fst = 0,
x : ,
h : foo x 1
 0 < 0

Is this really nonterminating, suggesting that a prop can actually be constructed using an infinite sequence of constructors? Or is this just a flaw in the equation compiler?

Eric Wieser (Dec 22 2021 at 17:33):

If I change foo to be a Type, then Lean is happy

Mario Carneiro (Dec 22 2021 at 21:20):

This is a flaw in the default well founded proof strategy. For inductive props that aren't simply recursive, I usually find it easier to use induction instead, which gives better control over what to do induction on

Mario Carneiro (Dec 22 2021 at 21:23):

It is possible to construct a well founded relation (not a sizeof function) which is useful for inductions over foo x y, but it is basically a more verbose and complicated version of just using the induction principle for foo

Mario Carneiro (Dec 22 2021 at 21:34):

lemma easy :  x, foo x 1  x = 0 :=
  suffices :  x y, foo x y  (y = 1  x = 0)  (x = 1  y = 0),
  from λ x H, (this _ _ H).1 rfl,
  intros x y H, induction H with _ _ _ IH, {simp},
  exact IH.symm

This proof is a bit different than the original, in that it does not depend on course of values recursion. You can write a course of values recursion lemma for this inductive but it's more work than just proving the theorem

Last updated: Dec 20 2023 at 11:08 UTC