# 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
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