assumption not used in wf recursion

Stream: new members

[Horatiu Cheval]

I hit a problem I dont't understand and don't know how to solve ina well founded recursion. The code is the following, the definition that doesn't work is the recursor case in the substitute function.

import tactic


inductive term
| app : term → term → term
| recursor : term → term → term → term

namespace term
  @[simp]
  def size : term → ℕ
  | (app t u) := t.size + u.size
  | (recursor n t₀ t) := n.size + t₀.size + t.size

  @[simp]
  lemma size_pos_iff_true (t : term) : 0 < t.size ↔ true := sorry

  def substitute : term → string → term → term
  | (app t u) y s := app (t.substitute y s) (u.substitute y s)
  | (recursor n t₀ t) y s :=
    have h₁ : 0 < n.size + t₀.size := sorry,
    have h₂ : n.size < n.size + t₀.size + t.size := sorry,
    have h₃ : t₀.size < n.size + t₀.size + t.size := sorry,
    recursor (n.substitute y s) (t₀.substitute y s) (t.substitute y s)
  using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ x, term.size x.1)⟩]}

end term

I basically just added all goals Lean required me to prove for showing the application is decreasing as hypothesis, and then I am stuck with proof states like:

    /-
    failed to prove recursive application is decreasing, well founded relation
      @has_well_founded.r (Σ' (ᾰ : term) (ᾰ : string), term)
        (@has_well_founded.mk (Σ' (ᾰ : term) (ᾰ : string), term)
           (@measure (Σ' (ᾰ : term) (ᾰ : string), term) (λ (x : Σ' (ᾰ : term) (ᾰ : string), term), x.fst.size))
           _)
    The nested exception contains the failure state for the decreasing tactic.
    nested exception message:
    default_dec_tac failed
    state:
    substitute : (Σ' (ᾰ : term) (ᾰ : string), term) → term,
    n t₀ t : term,
    y : string,
    s : term,
    h₁ : 0 < n.size + t₀.size,
    h₂ : n.size < n.size + t₀.size + t.size,
    h₃ : t₀.size < n.size + t₀.size + t.size
    ⊢ t₀.size < n.size + t₀.size + t.size
    -/

where the goal should be solvable by assumption. I think normally the termination checker (if that's the right word) would manage to solve the goal with a hypothesis by itself, but now I don't know how to proceed.

Also, weirdly enough, everything works fine for the other case app, which is mostly identical to the problematic one.

Could someone give me an indication on how to proceed?

[Anne Baanen]

I tried writing a custom dec_tac:

import tactic


inductive term
| app : term → term → term
| recursor : term → term → term → term

namespace term
  @[simp]
  def size : term → ℕ
  | (app t u) := t.size + u.size
  | (recursor n t₀ t) := n.size + t₀.size + t.size

  @[simp]
  lemma size_pos_iff_true (t : term) : 0 < t.size ↔ true := sorry

  def substitute : term → string → term → term
  | (app t u) y s := app (t.substitute y s) (u.substitute y s)
  | (recursor n t₀ t) y s :=
    have h₁ : 0 < n.size + t₀.size := sorry,
    have h₂ : n.size < n.size + t₀.size + t.size := sorry,
    have h₃ : t₀.size < n.size + t₀.size + t.size := sorry,
    recursor (n.substitute y s) (t₀.substitute y s) (t.substitute y s)
  using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ x, term.size x.1)⟩],
                      dec_tac := `[simp only [has_well_founded.r, measure, inv_image]; assumption]}

end term

However, now there's an error on def substitute: "failed to create auxiliary definition". I suspect it's to do with the sorrys.

[kana]

btw it will work without using_well_founded at all, the recursion is structural. But I guess it is just a simplified example

[Horatiu Cheval]

Indeed, the cases for which I actually need well founded recursion are not included in this mwe.

[Horatiu Cheval]

Anne, thanks for your suggestion, but it still gave failed to create auxiliary definition even after filling all the sorrys

[Horatiu Cheval]

I ended up solving this by proving all those goals as simp lemmas (i.e. simp lemmas with <-> true) before the definition. Not very elegant, but it worked