Idiomatic/easiest way to deal with vectors

Stream: new members

[Mukesh Tiwari]

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.

[1] https://gist.github.com/mukeshtiwari/df502c75eaffb201b5fbf878b9035b56#file-gistfile1-txt-L177

[Reid Barton]

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,
  convert h v.head v.tail,
  simp
end

[Reid Barton]

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

[Reid Barton]

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

[Mukesh Tiwari]

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?

[1] https://gist.github.com/mukeshtiwari/df502c75eaffb201b5fbf878b9035b56#file-gistfile1-txt-L222

[Johan Commelin]

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

[Kenny Lau]

most probably it can't find k

[Kenny Lau]

since you included all those hypotheses on L145

[Shing Tak Lam]

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]

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]

      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]

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

[Mukesh Tiwari]

Thanks everyone. It was great help.