Quantum Computing

Stream: Program verification

[Duckki Oe]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Or write:

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Duckki Oe]

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

[Duckki Oe]

@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]

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]

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

[Eric Wieser]

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