logo
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import defaults
from proveit import f, m, n, x, y, A
from proveit.logic import InSet, NotEquals
from proveit.logic.sets.functions.bijections import bijective_by_uniqueness
from proveit.physics.quantum.QPE import (_t, _s, _t_in_natural_pos, _s_in_nat_pos,
                                         _sample_space_def)
In [2]:
%proving _sample_space_bijection
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_sample_space_bijection:
(see dependencies)
In [3]:
_sample_space_def

We want to use $\Omega$ as our shorthand for the sample space:

In [4]:
defaults.replacements = set([_sample_space_def.derive_reversed()])
defaults.replacements:
In [5]:
lambda_map = _sample_space_bijection.element
lambda_map:
In [6]:
domain = _sample_space_bijection.domain.domain
domain:

In order to show that the image of the map is a bijection, we want to show that distinct elements of the domain map to distinct quantum circuits.

In [7]:
assumptions = [InSet(m, domain), InSet(n, domain), NotEquals(m, n)]
assumptions:
In [8]:
NotEquals(lambda_map.apply(m), lambda_map.apply(n)).prove(
    assumptions=assumptions)
, ,  ⊢  
In [9]:
bijective_by_uniqueness
In [10]:
bijective_by_uniqueness.instantiate(
    {f:lambda_map, A:domain, x:m, y:n}).derive_consequent()
_sample_space_bijection has been proven.  Now simply execute "%qed".
In [11]:
%qed
proveit.physics.quantum.QPE._sample_space_bijection has been proven.
Out[11]:
 step typerequirementsstatement
0modus ponens1, 2  ⊢  
1instantiation3, 4*, 5*  ⊢  
  : , : , : , :
2generalization6  ⊢  
3conjecture  ⊢  
 proveit.logic.sets.functions.bijections.bijective_by_uniqueness
4instantiation7, 8*, ,  ⊢  
  : , :
5instantiation9, 10*  ⊢  
  : , :
6axiom  ⊢  
 proveit.logic.booleans.true_axiom
7axiom  ⊢  
 proveit.logic.equality.not_equals_def
8instantiation11, 12, ,  ⊢  
  :
9axiom  ⊢  
 proveit.logic.sets.functions.images.set_image_def
10instantiation133, 13  ⊢  
  : , :
11axiom  ⊢  
 proveit.logic.booleans.eq_true_intro
12instantiation14, 15, ,  ⊢  
  : , :
13axiom  ⊢  
 proveit.physics.quantum.QPE._sample_space_def
14theorem  ⊢  
 proveit.logic.equality.unfold_not_equals
15modus ponens16, 17, ,  ⊢  
16instantiation18, 69, 136, 19, 20, 21, 22, 23, 24, 25  ⊢  
  : , : , : , :
17instantiation26, 69, 27, 28, 29, ,  ⊢  
  : , : , :
18conjecture  ⊢  
 proveit.physics.quantum.circuits.qcircuit_neq
19instantiation117, 30, 32, 33  ⊢  
  : , : , : , :
20instantiation117, 31, 32, 33  ⊢  
  : , : , : , :
21instantiation117, 34, 77, 37  ⊢  
  : , : , : , :
22instantiation117, 35, 77, 37  ⊢  
  : , : , : , :
23instantiation117, 36, 77, 37  ⊢  
  : , : , : , :
24instantiation117, 75, 77, 37  ⊢  
  : , : , : , :
25instantiation117, 76, 77, 37  ⊢  
  : , : , : , :
26conjecture  ⊢  
 proveit.core_expr_types.expr_arrays.varray_neq_via_any_elem_neq
27instantiation179  ⊢  
  : , : , : , :
28instantiation179  ⊢  
  : , : , : , :
29instantiation38, 127, 200, 39, 201, 40, 41, 42, 43, 44, ,  ⊢  
  : , : , : , : , :
30instantiation89, 46, 45, 48, 49, 92, 93, 57, 50*  ⊢  
  : , : , : , :
31instantiation89, 46, 47, 48, 49, 92, 93, 57, 50*  ⊢  
  : , : , : , :
32instantiation133, 51  ⊢  
  : , :
33instantiation133, 52  ⊢  
  : , :
34instantiation89, 90, 53, 159, 148, 92, 93, 108*, 151*  ⊢  
  : , : , : , :
35instantiation89, 90, 54, 55, 56, 92, 57, 108*, 84*  ⊢  
  : , : , : , :
36instantiation89, 90, 58, 159, 148, 92, 93, 108*, 151*  ⊢  
  : , : , : , :
37instantiation133, 59  ⊢  
  : , :
38conjecture  ⊢  
 proveit.logic.booleans.disjunction.or_if_any
39instantiation153  ⊢  
  : , : , :
40instantiation207  ⊢  
  : , :
41instantiation207  ⊢  
  : , :
42instantiation207  ⊢  
  : , :
43instantiation207  ⊢  
  : , :
44instantiation60, 61, 62, 63, 64, 65, ,  ⊢  
  : , : , :
45instantiation97  ⊢  
  : , : , : , : , : , : , : , :
46conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat8
47instantiation97  ⊢  
  : , : , : , : , : , : , : , :
48instantiation97  ⊢  
  : , : , : , : , : , : , : , :
49instantiation97  ⊢  
  : , : , : , : , : , : , : , :
50instantiation220, 66, 67  ⊢  
  : , : , :
51instantiation156, 257, 255, 200, 148, 201, 132, 193, 181  ⊢  
  : , : , : , : , : , :
52instantiation68, 69, 70, 111  ⊢  
  : , : , :
53instantiation216  ⊢  
  : , :
54instantiation216  ⊢  
  : , :
55instantiation216  ⊢  
  : , :
56instantiation216  ⊢  
  : , :
57instantiation109, 163, 84  ⊢  
  : , : , :
58instantiation216  ⊢  
  : , :
59instantiation110, 111  ⊢  
  : , :
60conjecture  ⊢  
 proveit.core_expr_types.tuples.tuple_neq_via_any_elem_neq
61instantiation224, 71, 72  ⊢  
  : , :
62instantiation220, 73, 74  ⊢  
  : , : , :
63instantiation117, 75, 77, 78  ⊢  
  : , : , : , :
64instantiation117, 76, 77, 78  ⊢  
  : , : , : , :
65instantiation95, 167, 163, 200, 142, 139, 201, 79, ,  ⊢  
  : , : , : , : , : , :
66instantiation80, 81, 82, 83, 108, 151, 84  ⊢  
  : , : , : , :
67instantiation117, 85, 86, 87  ⊢  
  : , : , : , :
68conjecture  ⊢  
 proveit.core_expr_types.tuples.len_of_ranges_with_repeated_indices_from_1
69conjecture  ⊢  
 proveit.numbers.numerals.decimals.posnat4
70instantiation166, 215  ⊢  
  : , :
71instantiation109, 260, 108  ⊢  
  : , : , :
72instantiation109, 223, 151  ⊢  
  : , : , :
73instantiation239, 108  ⊢  
  : , : , :
74instantiation239, 151  ⊢  
  : ,