Proving recursive application is decreasing?

Stream: new members

[Harrison Grodin]

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]

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]

Isn't flip just foo.symm?

[Eric Wieser]

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]

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

[Mario Carneiro]

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]

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]

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