## 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: May 08 2021 at 22:13 UTC