def breaks things

Stream: general

[Chris Hughes]

The following definition works as a lemma but not as a def. What's the problem?

import data.fintype group_theory.order_of_element data.nat.enat data.zmod.basic

universes u v
open equiv function fintype finset
variables {α : Type u} {β : Type v}

namespace equiv.perm
variable [decidable_eq α]

open list
lemma list_to_cycle (l : list α) (hl : l.nodup) : perm α :=
let f : ℤ → α → α := λ n a,
  if h : a ∈ l then
      let ll : ℕ+ := ⟨l.length, nat.pos_of_ne_zero $ mt list.length_eq_zero.1
        $ λ hl, list.not_mem_nil a $ hl ▸ h⟩ in
      l.nth_le (list.index_of a l + n : zmod ll).1 (list.index_of a l + n : zmod ll).2
    else a in
have ∀ n : ℤ, left_inverse (f n) (f (-n)),
  from λ n a, if h : a ∈ l
    then
    let ll : ℕ+ := ⟨l.length, nat.pos_of_ne_zero $ mt list.length_eq_zero.1
        $ λ hl, list.not_mem_nil a $ hl ▸ h⟩ in
    begin
      suffices : nth_le l ((↑(index_of a l) : zmod ll).val) _ = a,
      { simpa [f, h, nth_le_mem, nth_le_index_of hl] },
      { conv { to_rhs, rw ← index_of_nth_le (index_of_lt_length.2 h)},
        congr,
        erw [zmod.val_cast_nat, nat.mod_eq_of_lt (index_of_lt_length.2 h)] },
    end
    else by simp [h, f],
{ to_fun := f 1,
  inv_fun := f (-1),
  left_inv := this (-1),
  right_inv := this 1 }

[Simon Hudon]

What do you get as an error message?

[Chris Hughes]

type mismatch at definition 'equiv.perm.list_to_cycle._proof_3', has type ∀ {α : Type u} [_inst_1 : decidable_eq α] (l : list α), (ℤ → α → α) → (∀ (n : ℤ), left_inverse ((λ (n : ℤ) (a : α), dite (a ∈ l) (λ (h : a ∈ l), let ll : ℕ+ := ⟨length l, list_to_cycle._proof_1 α l a h⟩ in nth_le l ((↑(index_of a l) + ↑n).val) (list_to_cycle._proof_2 α _inst_1 l n a h)) (λ (h : a ∉ l), a)) n) ((λ (n : ℤ) (a : α), dite (a ∈ l) (λ (h : a ∈ l), let ll : ℕ+ := ⟨length l, list_to_cycle._proof_1 α l a h⟩ in nth_le l ((↑(index_of a l) + ↑n).val) (list_to_cycle._proof_2 α _inst_1 l n a h)) (λ (h : a ∉ l), a)) (-n))) → left_inverse ((λ (n : ℤ) (a : α), dite (a ∈ l) (λ (h : a ∈ l), let ll : ℕ+ := ⟨length l, list_to_cycle._proof_1 α l a h⟩ in nth_le l ((↑(index_of a l) + ↑n).val) (list_to_cycle._proof_2 α _inst_1 l n a h)) (λ (h : a ∉ l), a)) (-1)) ((λ (n : ℤ) (a : α), dite (a ∈ l) (λ (h : a ∈ l), let ll : ℕ+ := ⟨length l, list_to_cycle._proof_1 α l a h⟩ in nth_le l ((↑(index_of a l) + ↑n).val) (list_to_cycle._proof_2 α _inst_1 l n a h)) (λ (h : a ∉ l), a)) (- -1)) but is expected to have type ∀ {α : Type u} [_inst_1 : decidable_eq α] (l : list α) (f : ℤ → α → α), (∀ (n : ℤ), left_inverse ((λ (n : ℤ) (a : α), dite (a ∈ l) (λ (h : a ∈ l), let ll : ℕ+ := ⟨length l, list_to_cycle._proof_1 α l a h⟩ in nth_le l ((↑(index_of a l) + ↑n).val) (list_to_cycle._proof_2 α _inst_1 l n a h)) (λ (h : a ∉ l), a)) n) ((λ (n : ℤ) (a : α), dite (a ∈ l) (λ (h : a ∈ l), let ll : ℕ+ := ⟨length l, list_to_cycle._proof_1 α l a h⟩ in nth_le l ((↑(index_of a l) + ↑n).val) (list_to_cycle._proof_2 α _inst_1 l n a h)) (λ (h : a ∉ l), a)) (-n))) → left_inverse (f (-1)) (f (- -1))

[Simon Hudon]

That's probably a bug in the equation compiler. @Sebastian Ullrich, what do you think?

[Mario Carneiro]

looks like a problem with the let, although set_option eqn_compiler.zeta true doesn't seem to help. I suggest making the function f an auxiliary definition