Zulip Chat Archive

Stream: Program verification

Topic: Quantum Computing


view this post on Zulip Duckki Oe (Nov 24 2020 at 17:09):

Hi All, I posted my initial release of Quantum Computing in Lean. https://github.com/duckki/lean-quantum
I had a lot of fun and learned a lot. But, I don't think I'm using Lean right, yet. :)

view this post on Zulip Duckki Oe (Nov 24 2020 at 17:12):

I managed to prove 3 versions no-clone theorems like

theorem no_clone_1
    : ¬ ( (U : Matrix 4 4), U.unitary   s : Vector 2, U  (s  |0⟩) = s  s)

theorem no_clone_3 {n}
    : ¬ ( (U : Square (2 ^ (n + 2))) (f : (Vector 2)  Vector (2^n))
         , U.unitary
          ( s : Vector 2, s.unit  U  (s  (|0^(n+1)⟩)) = (s  (s  (f s)))))

view this post on Zulip Duckki Oe (Nov 24 2020 at 17:13):

@Logan Murphy Here's my promised post :up:

view this post on Zulip Bryan Gin-ge Chen (Nov 24 2020 at 17:19):

Congrats! Note that one way to get good feedback on your Lean code is to PR the re-usable bits of your code to mathlib :wink:

view this post on Zulip Duckki Oe (Nov 24 2020 at 17:21):

Thanks. PR to mathlib will be my next step :)

view this post on Zulip Yakov Pechersky (Nov 24 2020 at 17:27):

You might like data/matrix/notation for notation like vector.of_fn ![/√2] instead of (/√2 ::ᵥ vector.nil)

view this post on Zulip Yakov Pechersky (Nov 24 2020 at 17:28):

Or write:

def X : Matrix 2 2 := ![
![0, 1],
![1, 0]]

view this post on Zulip Eric Wieser (Nov 24 2020 at 18:07):

Don't forget to turn https://github.com/leanprover-contrib/lean-build-action on in your repo :)

view this post on Zulip Eric Wieser (Nov 24 2020 at 18:11):

One other tip - Your adjoint function was recently generalized by Scott to docs#star (and the instance it uses docs#matrix.star_ring), which gives you a bunch of lemmas for free that might replace your lemmas. You'll still need to introduce the dagger notation yourself though.

view this post on Zulip Duckki Oe (Nov 24 2020 at 22:31):

@Yakov Pechersky Thanks. I'm updating my code with the notation you suggested, right now.

view this post on Zulip Duckki Oe (Nov 24 2020 at 22:34):

@Eric Wieser star sounds good. I'll update my mathlib.

view this post on Zulip Duckki Oe (Nov 25 2020 at 00:58):

@Eric Wieser , one issue with "star" is that it expects to return the same type as the input. That works for ℂ. But, for matrix, it needs to be matrix m n a -> matrix n m a.

view this post on Zulip Wrenna Robson (Dec 10 2020 at 12:22):

Duckki Oe said:

Eric Wieser , one issue with "star" is that it expects to return the same type as the input. That works for ℂ. But, for matrix, it needs to be matrix m n a -> matrix n m a.

Perhaps part of the definition of [has_star R] should be a defined type R* which is the target of * (I guess you have a function on types R -> R, then, and you want it to be involutive, so R* = R?)

view this post on Zulip Eric Wieser (Dec 10 2020 at 13:08):

I think this is a general problem in the same way that you can't define has_mul on non-square matrices

view this post on Zulip Eric Wieser (Dec 10 2020 at 13:08):

Which means you wouldn't be able to state things like docs#star_mul anyway


Last updated: May 08 2021 at 22:13 UTC