how to show mutual theorem

Stream: general

[Asei Inoue]

How to show this?

mutual

inductive Even : Nat → Prop where
  | zero : Even 0
  | succ {n : Nat} (h : Odd n) : Even (n + 1)

inductive Odd : Nat → Prop where
  | succ {n : Nat} (h : Even n) : Odd (n + 1)
end


mutual

variable {n : Nat}

theorem Even.exists (h : Even n) : ∃ a, n = 2 * a := by
  cases h with
  | zero => exists 0
  | @succ n h =>
    obtain ⟨a, ha⟩ := h.exists -- Environment does not contain `Odd.exists`
    exists (a + 1)
    grind

theorem Odd.exists (h : Odd n) : ∃ a, n = 2 * a + 1 := by
  cases h with
  | @succ n h =>
    obtain ⟨a, ha⟩ := Even.exists h
    exists a
    grind

end

[Aaron Liu]

somehow the problem is the variable {n : Nat}, if you inline it then it's fine

[Jakub Nowak]

Iirc if you use variable then it will use the same variable in the recursive calls. In your case n does change between recursive calls, so you shouldn't be using variable for it.

[Niklas Halonen]

Hmm there is indeed something fishy going on with variables in mutual blocks (I didn't even know they were allowed!)

This works (due to autoimplicits), but uncommenting either of the variable declarations will make it fail with the most weirdest of errors

mutual

inductive Even : Nat → Prop where
  | zero : Even 0
  | succ {n : Nat} (h : Odd n) : Even (n + 1)

inductive Odd : Nat → Prop where
  | succ {n : Nat} (h : Even n) : Odd (n + 1)
end


-- variable {n m : Nat}
mutual
-- variable {n m : Nat}

theorem Even.exists (h : Even n) : ∃ a, n = 2 * a := match h with
  | .zero => by exists 0
  | @Even.succ n h => by
    obtain ⟨a, ha⟩ := h.exists
    exists (a + 1)
    grind

theorem Odd.exists (h : Odd m) : ∃ a, m = 2 * a + 1 := match h with
  | @Odd.succ n h => by
    obtain ⟨a, ha⟩ := Even.exists h
    exists a
    grind

end

The error says unknown free variable `_fvar.189` .
Not only this, but using n as the variable name in the latter theorem yields more strange errors when a variable declaration is uncommented...

[Jakub Nowak]

I don't think the problem is with mutual. Look at this example:

variable (n : Nat)

/--
error: Function expected at
  pred
but this term has type
  Nat

Note: Expected a function because this term is being applied to the argument
  n
-/
#guard_msgs in
def pred : Nat :=
  match n with
  | 0 => 0
  | n + 1 => @pred n

/-- info: pred (n : Nat) : Nat -/
#guard_msgs in
#check pred

Inside pred the type of pred is just Nat. Not Nat → Nat. Lean won't let you change the value of n between recursive calls. Implicit variables work the same. It's not possible to change them between recursive calls. This is intended behaviour.

[Niklas Halonen]

You are correct, this is really surprising to me as I always thought variables are simply "prepended to the list of arguments", i.e. that variable (n : Nat) desugars as

def pred (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => @pred n

But this to me doesn't explain why having variables n and m in the mutual block leads to the weird error.

[Jakub Nowak]

Hm, the code wouldn't work anyway, but yeah, it doesn't make sense why the error is "Unknown identifier".