## Stream: new members

### Topic: Idiomatic/easiest way to deal with vectors

#### Mukesh Tiwari (Sep 18 2020 at 13:48):

Hi everyone,
I am wondering what could be the easiest way to prove this lemma (mwe) [1]. The proof is fairly trivial (pen and paper). Since ms and rs

ms: vector (zmod p) n_n.succ
rs: vector (zmod q) n_n.succ


of length (n + 1), I can have ms = msh :: mstail for some msh and mstail, and similarly for rs. After this, I can substitute (rewrite) these values in the goal. Also, I would be happy with any other comment about the code to make it more better/idiomatic.

#### Reid Barton (Sep 18 2020 at 16:59):

One way to handle this would be to define a custom induction principle like (I didn't see it in mathlib already)

import data.vector
import tactic.basic

@[elab_as_eliminator]
protected def vector.induction {α : Type*} {n : ℕ} {C : vector α (n+1) → Prop}
(h : ∀ (hd : α) (tl : vector α n), C (vector.cons hd tl)) : ∀ (v : vector α (n+1)), C v :=
begin
intro v,
simp
end


#### Reid Barton (Sep 18 2020 at 17:04):

Then you should be able to write something like induction ms using vector.induction with msh mstail

#### Reid Barton (Sep 18 2020 at 17:04):

or an equivalent series of steps using revert, apply vector.induction, intro

#### Mukesh Tiwari (Sep 19 2020 at 07:47):

Thanks Reid Barton . It appears that working with vector is not very easy, so I switched to list. So far everything is good, except at the line 222 [1] I can not apply the lemma elgamal_enc_dec_identity. I am getting this error:

invalid apply tactic, failed to synthesize type class instance


I don't understand why it fails to synthesize type class instance. Any idea how to resolve this issue?

#### Johan Commelin (Sep 19 2020 at 07:50):

Do you have any idea which type class it failed to synth?

#### Kenny Lau (Sep 19 2020 at 07:51):

most probably it can't find k

#### Kenny Lau (Sep 19 2020 at 07:52):

since you included all those hypotheses on L145

#### Shing Tak Lam (Sep 19 2020 at 07:55):

For the variables L32-36, are all of those supposed to be [...]? Since Lean then tries to use the typeclass search to find those.

#### Mukesh Tiwari (Sep 19 2020 at 07:59):

Johan Commelin No, I have no idea that why it fails to synthesize?
Shing Tak Lam My understanding of [...] making the assumptions implicit, but I don't have crystal clear idea about typeclass in Lean.

#### Shing Tak Lam (Sep 19 2020 at 08:01):

      apply @elgamal_enc_dec_identity _ _ _ _ _ _ _ Hp Hq Hdiv H₁ H₂ H₃ H₄,
/-    ^                                       ^^^^^^^^^^^^^^^^^^^^^^
Make everything explicit,                             |
Lean can't figure out any of these arguments
-/


#### Ruben Van de Velde (Sep 19 2020 at 08:02):

If you want implicit arguments, use {}, not []

#### Mukesh Tiwari (Sep 19 2020 at 09:33):

Thanks everyone. It was great help.

Last updated: May 08 2021 at 04:14 UTC