Stream: quantum computing

Topic: AFP Submission


view this post on Zulip Hanna Lachnitt (Oct 07 2020 at 20:09):

Basics.thy:

lemma [simp]:
shows "2 * (cmod (1 / complex_of_real (sqrt 2)))⇧2 = 1"
using cmod_def by (simp add: power_divide)

I suggest two_div_sqr_of_cmd_sqrt_two to stay within the name convention used for the other lemmas in the theory but shorter names are welcome.

view this post on Zulip Hanna Lachnitt (Oct 07 2020 at 21:28):

Tensor.thy:
line 461. Fact linordered_field_class.sign_simps(4) cannot be found. Proof can be replaced with

by (smt ab_semigroup_mult_class.mult_ac(1) length_greater_0_conv length_mat_to_cols_list
mat_to_cols_list_is_mat mult.Tensor.simps(1) mult.Tensor_null plus_mult_cpx plus_mult_def)

view this post on Zulip Hanna Lachnitt (Oct 09 2020 at 20:46):

Changed one metis proof in Deutsch_Joza by one that requires less time.

view this post on Zulip Hanna Lachnitt (Oct 09 2020 at 21:01):

Theory No_Cloning line 193. Assumptions have [simp] attributes. Do they need a name too? I am not sure what the [simp] does here.

view this post on Zulip Hanna Lachnitt (Oct 16 2020 at 18:48):

Added Measurement to ROOT since all theory files of the submission must be contained in at least one session.


Last updated: Sep 25 2022 at 23:25 UTC