Can't use induction tactic nor generalize

Stream: new members

[Roberto Pettinau]

Hi, I'm working on a proof for a simple calculus in which I try to prove monotonicity of some transformer by induction on the syntax of the calculus. Unfortunately I can't get the induction tactic to work (even when using generalize). I reduced the problem to the following MWE:

inductive A where
  | a1 : A

inductive B : A -> Type where
  | b1 : B x

inductive C : (List A × A) -> Type where
  | c1 : B y -> C x
  | c2 : C x -> C x

def count : C (xs,x) -> Int
  | C.c1 _ => 0
  | C.c2 c' => 1 + count c'

theorem foo (c: C (xs,x)) : @count xs x c ≥ 0 :=
  by
    -- generalize (xs, x) = X at c
    induction c
    sorry

When running induction c by itself, Lean tells me that

index in target's type is not a variable (consider using the `cases` tactic instead)
  (xs, x)

When uncommenting generalize, Lean instead tells me that

tactic 'generalize' failed, result is not type correct

I'm not really sure what's going on, and seemingly random changes like removing the type index from B make everything work. Does anybody have an explanation of what's the problem, and how to approach this type of issues on more complicated examples?

I also tried to do a proof with C.recOn, and that works fine:

import Std.Data.Int.Order

theorem foo' (c: C (xs, x)) : @count xs x c ≥ 0 :=
  @C.recOn (fun (xs,x) c => @count xs x c ≥ 0) _ c
    (by intro a (xs,x) b; unfold count; simp)
    (by intro (xs,x) c h; unfold count; simp at h; simp_all [Int.add_nonneg _ h])

Thanks in advance!

[Matt Diamond]

I think the problem is your reliance on autoImplicit

[Matt Diamond]

I would suggest adding set_option autoImplicit false to the top of your file and adding the implicit variables

[Matt Diamond]

when I do that in the MWE you provided, the issue goes away and induction is successful

[Matt Diamond]

just want to take this opportunity to say that the design decision to make autoImplicit enabled by default is terrible and I hope the developers will rethink this

[Roberto Pettinau]

Thank you for the answer! Was that your only change? I can't seem to be able to replicate it, whether I make the variables explicit or implicit:

set_option autoImplicit false

inductive A where
  | a1 : A

inductive B : A -> Type where
  | b1 : ∀x, B x

inductive C : (List A × A) -> Type where
  | c1 : ∀y x, B y -> C x
  | c2 : ∀x, C x -> C x

def count (xs: List A) (x: A): C (xs,x) -> Int
  | C.c1 _ _ _ => 0
  | C.c2 _ c' => 1 + count xs x c'

theorem foo (xs: List A) (x: A) (c: C (xs,x)) : count xs x c ≥ 0 :=
  by induction c -- error

[Matt Diamond]

here's what I did:

set_option autoImplicit false

inductive A where
  | a1 : A

inductive B : A -> Type where
  | b1 {x} : B x

inductive C : (List A × A) -> Type where
  | c1 {x y} : B y -> C x
  | c2 {x} : C x -> C x

def count {xs x} : C (xs, x) -> Int
  | C.c1 _ => 0
  | C.c2 c' => 1 + count c'

theorem foo {xs x} (c : C (xs, x)) : @count xs x c ≥ 0 :=
  by
    -- generalize (xs, x) = X at c
    induction c <;> sorry

[Matt Diamond]

basically just the minimum amount of hints so that Lean knows what goes where

[Roberto Pettinau]

Okay that works for me, thank you. What I find so strange is that by just changing c1 {x y} to c1 {y x} everything just stops working

[Matt Diamond]

That's interesting... btw I played around with it and Lean only really needs a single implicit variable to avoid the issue, so clearly that's the key line:

inductive A where
  | a1 : A

inductive B : A -> Type where
  | b1 : B x

inductive C : (List A × A) -> Type where
  | c1 {y} : B y -> C x -- if you remove {y}, induction breaks
  | c2 : C x -> C x

def count : C (xs, x) -> Int
  | C.c1 _ => 0
  | C.c2 c' => 1 + count c'

theorem foo (c : C (xs, x)) : @count xs x c ≥ 0 :=
  by
    induction c <;> sorry

[Roberto Pettinau]

Yeah, it really seems like the only important thing is the order of parameters in c1, for some reason (with {y} it becomes second)

[Matt Diamond]

I'm not knowledgeable enough to explain why that's necessary, but perhaps someone else here can chime in

[Roberto Pettinau]

I gave this another look today. Apparently swapping x and y completely changes how the recursor is generated: when x is first, the motive depends on a fixed x, while when y is first, the motive has to depend on some arbitrary x.

inductive C1 : List (List A × A) -> Type where
  | c1 {x y}: B y -> C1 x

-- C1.rec.{u} {a✝ : List (List A × A)} {motive : C1 a✝ → Sort u}
--  (c1 : {y : A} → (a : B y) → motive (C1.c1 a))
--  (t : C1 a✝) : motive t

inductive C2 : List (List A × A) -> Type where
  | c2 {y x}: B y -> C2 x

-- C2.rec.{u} {motive : (a : List (List A × A)) → C2 a → Sort u}
--  (c2 : {y : A} → {x : List (List A × A)} → (a : B y) → motive x (C2.c2 a))
--  {a✝ : List (List A × A)} (t : C2 a✝) : motive a✝ t

I'm not sure I understand why this would be the case at all, as x and y do not depend on each other in any way. I guess that Lean does not see that x remains constant when recursing over C2?

[Mario Carneiro]

The parameters to an inductive type have to appear in the constructors in the same order as the type and before all the regular constructor arguments. (For this reason they are generally defined left of the colon and not specified in the constructor at all since they are already in scope. But allowing them to be specified in the constructor is useful for e.g. changing the names or binding modes of the parameters in the constructor.) So when you reverse the order of the arguments it becomes no longer possible to promote it to a parameter.