induction tactic is nondeterministic

Stream: general

[Eric Wieser]

I've run into a pair of nasty issues here:

import algebra.monoid_algebra

namespace add_monoid_algebra

variables {k G : Type*} [semiring k] [add_monoid G]

@[recursor 6]  -- comment / delete this line with a single edit action
lemma induction_on
  {p : add_monoid_algebra k G → Prop} (f : add_monoid_algebra k G)
  (hM : ∀ g, p (of k G (multiplicative.of_add g)))
  (hadd : ∀ f g : add_monoid_algebra k G, p f → p g → p (f + g))
  (hsmul : ∀ (r : k) f, p f → p (r • f)) : p f :=
begin
  refine finsupp.induction_linear f _ (λ f g hf hg, hadd f g hf hg) (λ g r, _),
  { simpa using hsmul 0 (of k G (multiplicative.of_add 0)) (hM 0) },
  { convert hsmul r (of k G (multiplicative.of_add g)) (hM g),
    simp only [mul_one, to_add_of_add, finsupp.smul_single', of_apply] },
end

example (x : add_monoid_algebra k G) : x = 0 := begin
  induction x using add_monoid_algebra.induction_on,
  sorry,
  sorry,
  sorry,
end

end add_monoid_algebra

The first nasty issue is that the induction tactic has swapped k and G, and gotten its types in a muddle.

To reproduce the non-determinism:

1. Paste the code into a fresh editor pane and restart the lean server. A nasty type error appears under the word example
2. Comment out line 7 with Ctrl+/ (so as to do so in a single keystroke). The error remains where it is
3. Type a single space somewhere in the file. The error moves to the induction tactic`.

[Eric Wieser]

The first issue goes away if I use attribute [irreducible] add_monoid_algebra before example

[Kevin Buzzard]

Very nice -- I can reproduce.

[Kevin Buzzard]

PS ctrl+X deletes the line with a single keystroke and ctrl-Z brings it back (and makes the error jump)

[Kevin Buzzard]

Just alternating between C-x and C-z makes the error jump around randomly

[Gabriel Ebner]

I only get the following error, even after commenting it out and un again:

induction tactic failed, major premise type is ill-formed

[Kevin Buzzard]

I sometimes have to do it about 10 times before there's a switch. The other error is with the red squiggle on example and error

type mismatch at application
  @induction_on G k
    (@mul_zero_class.to_has_zero k
       (@mul_zero_one_class.to_mul_zero_class k
          (@monoid_with_zero.to_mul_zero_one_class k (@semiring.to_monoid_with_zero k _inst_1))))
term
  @mul_zero_class.to_has_zero k
    (@mul_zero_one_class.to_mul_zero_class k
       (@monoid_with_zero.to_mul_zero_one_class k (@semiring.to_monoid_with_zero k _inst_1)))
has type
  has_zero k
but is expected to have type
  semiring G

(VS Code 1.55.2, lean and lean4 extensions installed, lean extension 0.16.26, ubuntu linux)

[Kevin Buzzard]

On command line I always seem to get induction tactic failed

[Kevin Buzzard]

Continually restarting Lean in VS Code I consistently get type mismatch at application

[Eric Wieser]

I assume there's some stale cache sticking around on the lean server that doesn't make it to the olean files, which would explain why the command line is deterministic?

[Kevin Buzzard]

(this is with the [recursor 6] line)

[Gabriel Ebner]

lean#569 #mwe

inductive foo (α β : Type)

def bar (β α) := foo α β

@[recursor 4]
lemma bar.induction_on {β α} {C : bar β α → Prop} (x : bar β α) : C x :=
by cases x

example {β α} (x : bar β α) : x = x :=
by induction x using bar.induction_on