OracleCopyOperations.lean

1 import RealizationBoundaries.ComputablePresentations
2 
3 /-!
4 # All group operations in a genuinely coded oracle copy
5 
6 Inversion is not silently omitted from the computable-copy contract. Given the
7 proved bijective Nat naming and actual computable addition, search for a right
8 inverse terminates and returns the literal inverse under the naming map.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace RealizationBoundaries
13 namespace OracleGroupCopy
14 variable {X : ℕ → Bool} {H : Type*} [AddGroup H]
15 
16 /-- Zero is a finite natural constant, hence requires no extra oracle. -/
17 theorem zero_computable (c : OracleGroupCopy X H) :
18     OracleComputable X (fun _ => c.zero) := OracleComputable.const c.zero
19 
20 /-- Ordinary equality of natural names is the actual equality of named elements. -/
21 theorem names_equal_iff (c : OracleGroupCopy X H) (i j : ℕ) :
22     c.names i = c.names j ↔ i = j := c.names.injective.eq_iff
23 
24 /-- A zero-valued test for a candidate right inverse. -/
25 def inverseTest (c : OracleGroupCopy X H) (k : ℕ) : ℕ :=
26   if c.add k.unpair.1 k.unpair.2 = c.zero then 0 else 1
27 
28 theorem inverseTest_correct (c : OracleGroupCopy X H) (n t : ℕ) :
29     c.inverseTest (Nat.pair n t) = 0 ↔ c.names t = -c.names n := by
30   have he : c.add n t = c.zero ↔ c.names n + c.names t = 0 := by
31     rw [← c.add_spec, ← c.zero_spec, c.names.injective.eq_iff]
32   simp only [inverseTest, Nat.unpair_pair, ite_eq_left_iff, one_ne_zero,
33     imp_false, not_not]
34   exact he.trans ⟨eq_neg_of_add_eq_zero_right, fun h => by rw [h, add_neg_cancel]⟩
35 
36 theorem inverseTest_computable (c : OracleGroupCopy X H) :
37     OracleComputable X c.inverseTest := by
38   have ht : Computable (fun m : ℕ => if m = c.zero then 0 else 1) :=
39     (Primrec.ite (Primrec.eq.comp Primrec.id (Primrec.const c.zero))
40       (Primrec.const 0) (Primrec.const 1)).to_comp
41   exact (OracleComputable.of_computable ht).comp c.add_computable
42 
43 /-- Termination is justified by actual group inversion and surjectivity of the
44 names, without assuming that the inverse naming function is computable. -/
45 theorem inverseTest_total (c : OracleGroupCopy X H) (n : ℕ) :
46     ∃ t, c.inverseTest (Nat.pair n t) = 0 := by
47   refine ⟨c.names.symm (-c.names n), (c.inverseTest_correct n _).mpr ?_⟩
48   exact c.names.apply_symm_apply _
49 
50 /-- The actual terminating inverse algorithm on Nat names. -/
51 def inverse (c : OracleGroupCopy X H) (n : ℕ) : ℕ :=
52   Nat.find (c.inverseTest_total n)
53 
54 theorem inverse_spec (c : OracleGroupCopy X H) (n : ℕ) :
55     c.names (c.inverse n) = -c.names n :=
56   (c.inverseTest_correct n _).mp (Nat.find_spec (c.inverseTest_total n))
57 
58 /-- Native relative inversion follows from native addition by proved total
59 minimization; it is not an additional assumption on the copy. -/
60 theorem inverse_computable (c : OracleGroupCopy X H) :
61     OracleComputable X c.inverse :=
62   OracleComputable.find c.inverseTest_computable c.inverseTest_total
63 
64 @[simp] theorem inverse_inverse (c : OracleGroupCopy X H) (n : ℕ) :
65     c.inverse (c.inverse n) = n := by
66   apply c.names.injective
67   rw [c.inverse_spec, c.inverse_spec, neg_neg]
68 
69 @[simp] theorem inverse_zero (c : OracleGroupCopy X H) : c.inverse c.zero = c.zero := by
70   apply c.names.injective
71   rw [c.inverse_spec, c.zero_spec, neg_zero]
72 
73 theorem add_inverse (c : OracleGroupCopy X H) (n : ℕ) :
74     c.add n (c.inverse n) = c.zero := by
75   apply c.names.injective
76   rw [c.add_spec, c.inverse_spec, c.zero_spec, add_neg_cancel]
77 
78 theorem inverse_add (c : OracleGroupCopy X H) (n : ℕ) :
79     c.add (c.inverse n) n = c.zero := by
80   apply c.names.injective
81   rw [c.add_spec, c.inverse_spec, c.zero_spec, neg_add_cancel]
82 
83 /-- Subtraction is then also a genuine relative computation on names. -/
84 def subtract (c : OracleGroupCopy X H) (i j : ℕ) : ℕ := c.add i (c.inverse j)
85 
86 theorem subtract_spec (c : OracleGroupCopy X H) (i j : ℕ) :
87     c.names (c.subtract i j) = c.names i - c.names j := by
88   rw [subtract, c.add_spec, c.inverse_spec, sub_eq_add_neg]
89 
90 theorem subtract_computable (c : OracleGroupCopy X H) :
91     OracleComputable X (fun k => c.subtract k.unpair.1 k.unpair.2) :=
92   c.add_computable.comp
93     (OracleComputable.left.pair (c.inverse_computable.comp OracleComputable.right))
94     |>.of_eq (fun k => by simp [subtract])
95 
96 end OracleGroupCopy
97 end RealizationBoundaries

Back to source controls