Zulip Chat Archive

Stream: Program verification

Topic: Quantum Computing


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. :)

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)))))

Duckki Oe (Nov 24 2020 at 17:13):

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

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:

Duckki Oe (Nov 24 2020 at 17:21):

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

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)

Yakov Pechersky (Nov 24 2020 at 17:28):

Or write:

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

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 :)

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.

Duckki Oe (Nov 24 2020 at 22:31):

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

Duckki Oe (Nov 24 2020 at 22:34):

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

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.

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?)

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

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: Dec 20 2023 at 11:08 UTC