## 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
state:
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 :=
begin
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
end


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