fin zip

Stream: Is there code for X?

[Patrick Thomas]

Does something like this already exist in mathlib that I did not see?

def fin_zip
    {α β : Type}
    [decidable_eq α]
    (σ : α → β) : Π (n : ℕ), (fin n → α) → (fin n → β) → (α → β)
| 0 _ _ := σ
| (n + 1) xs ys :=
    function.update
        (fin_zip n (fun (i : fin n), (xs i)) (fun (i : fin n), (ys i)))
        (xs n) (ys n)

[Scott Morrison]

I'd guess not.

[Patrick Thomas]

It's supposed to be a function.update at a finite number of points. Is there a simpler way to define it?

[Scott Morrison]

The pair of tuples seems an inconvenient way to provide the data. Why not just a list (\a \times \b)? (Which you would then fold over.)

[Patrick Thomas]

Yeah, that might work. I assumed I needed tuples because I needed them in other places in the project, but they might not be necessary here.

[Patrick Thomas]

Like this?

def function.update_list
    {α β : Type}
    [decidable_eq α]
    (σ : α → β)
    (pairs : list (α × β)) :
    (α → β) :=
    list.foldl (fun (σ' : α → β) (p : α × β), function.update σ' p.fst p.snd) σ pairs

#eval (function.update_list (fun (n : ℕ), n) [(0,1), (0, 10), (1, 2)]) 0

[Patrick Thomas]

I think I still need one that takes tuples after all though.

[Eric Wieser]

You can call that function with docs#list.of_fn if you have two tuples

[Patrick Thomas]

Yeah, I guess. I was trying to make it as direct as possible because I need to deal with it in proofs.

[Patrick Thomas]

I might do that though. Thank you.

[Patrick Thomas]

Is there a good way to deal with the coercions here?

def function.update_fin
    {α β : Type}
    [decidable_eq α]
    (σ : α → β) :
    Π (n : ℕ), (fin n → α) → (fin n → β) → (α → β)
| 0 _ _ := σ
| (n + 1) f g :=
    function.update
        (function.update_fin n (fun (i : fin n), (f i)) (fun (i : fin n), (g i)))
        (f n) (g n)

#eval function.update_fin (fun (n : ℕ), n) 3 ![0, 5, 0] ![10, 8, 5] 0


example
    {α β : Type}
    [decidable_eq α]
    (σ : α → β)
    (n : ℕ)
    (xs : fin n → α)
    (nodup : function.injective xs)
    (ys : fin n → β)
    (x : α)
    (i : fin n)
    (h1 : x = xs i) :
    function.update_fin σ n xs ys x = ys i :=
begin
    induction n,
    case nat.zero
  { admit },
  case nat.succ : n ih
  {
        unfold function.update_fin,
        by_cases i = n,
        {
            subst h, rewrite h1, apply function.update_same
        },
        {
            have s1 : x ≠ xs ↑n, intro contra, apply h, rewrite h1 at contra,
            unfold function.injective at nodup, exact nodup contra,
            rewrite function.update_noteq s1,
            specialize ih (fin.init xs),

            have s2 : ∀ (i : fin n.succ), function.injective (fin.init xs), intros i',
            unfold function.injective at nodup, unfold function.injective, unfold fin.init,
            sorry,

            specialize ih (s2 i) (fin.init ys),
            cases i,
            sorry
        }
    },
end

[Patrick Thomas]

Is there a way to use the fact that i : fin n.succ != n to get i : fin n?

[Yakov Pechersky]

(deleted)