Misbehavior of the termination checker?

Stream: new members

[Jasmin Blanchette]

I have stumbled on a strange case. The termination checker accepts the following code. I don't see why it should, since there's an infinite recursion.

lemma my_lemma :
  ∀x y : ℕ, x ^ 2 = 2 * y ^ 2 → x = 0 ∧ y = 0
| x y x_eq_y :=
  begin
    let z := 200,
    have z_eq_z : z ^ 2 = 2 * z ^ 2 := sorry,
    have := my_lemma _ _ z_eq_z,
    sorry
  end

[Rob Lewis]

If you #print my_lemma afterward, the recursive call doesn't appear. have x : t := e, v is more or less sugar for (λ x : t, v) e in term mode, and I guess it's the same in tactic mode. It's probably getting beta reduced away before the well-foundedness check happens.

[Rob Lewis]

Strange behavior though.

[Chris Hughes]

I think it's because in tactic mode, a have doesn't appear in the proof term unless it's used.

This thing fails

import tactic.norm_num

lemma my_lemma :
  ∀x y : ℕ, x ^ 2 = 2 * y ^ 2 → x = 0 ∧ y = 0
| x y x_eq_y :=
  begin
    let z := 200,
    have z_eq_z : z ^ 2 = 2 * z ^ 2 := sorry,
    exact absurd (my_lemma _ _ z_eq_z) (by dsimp [z]; norm_num)
  end

[Rob Lewis]

Or, this is another instance of the badly behaving tactic let you showed me yesterday that wipes the haves from the context. I'm not sure if that was explainable in the same way.

[Jasmin Blanchette]

Thanks. That explains it.