Zulip Chat Archive

Stream: new members

Topic: Idiomatic/easiest way to deal with vectors


view this post on Zulip 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.

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

view this post on Zulip 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,
  convert h v.head v.tail,
  simp
end

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 18 2020 at 17:04):

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

view this post on Zulip 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?

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

view this post on Zulip Johan Commelin (Sep 19 2020 at 07:50):

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

view this post on Zulip Kenny Lau (Sep 19 2020 at 07:51):

most probably it can't find k

view this post on Zulip Kenny Lau (Sep 19 2020 at 07:52):

since you included all those hypotheses on L145

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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
      -/

view this post on Zulip Ruben Van de Velde (Sep 19 2020 at 08:02):

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

view this post on Zulip Mukesh Tiwari (Sep 19 2020 at 09:33):

Thanks everyone. It was great help.


Last updated: May 08 2021 at 04:14 UTC