Recovery.lean

1 import ProofPath.Compression
2 
3 /-!
4 Recovery on the attained image. This is the decoder domain used by the monograph.
5 The old total-codomain definition stays available and is compared explicitly.
6 -/
7 namespace ProofPath
8 namespace Recovery
9 
10 variable {A B C D : Type*}
11 
12 def Image (encode : A → B) := {b : B // ∃ a : A, encode a = b}
13 
14 def observed (encode : A → B) (a : A) : Image encode := ⟨encode a, a, rfl⟩
15 
16 def Sufficient (encode : A → B) (task : A → C) : Prop :=
17   ∃ decode : Image encode → C, ∀ a, decode (observed encode a) = task a
18 
19 def FiberConstant (encode : A → B) (task : A → C) : Prop :=
20   ∀ a a', encode a = encode a' → task a = task a'
21 
22 theorem sufficient_iff_fiber_constant (encode : A → B) (task : A → C) :
23     Sufficient encode task ↔ FiberConstant encode task := by
24   constructor
25   · rintro ⟨d, hd⟩ a a' he
26     have hh : observed encode a = observed encode a' := Subtype.ext he
27     exact (hd a).symm.trans ((congrArg d hh).trans (hd a'))
28   · intro h
29     classical
30     let pick : Image encode → A := fun b => Classical.choose b.property
31     have hp : ∀ b : Image encode, encode (pick b) = b.val :=
32       fun b => Classical.choose_spec b.property
33     refine ⟨fun b => task (pick b), ?_⟩
34     intro a
35     exact h (pick (observed encode a)) a (hp (observed encode a))
36 
37 theorem total_implies_attained (encode : A → B) (task : A → C)
38     (h : ProofPath.Sufficient encode task) : Sufficient encode task := by
39   rcases h with ⟨d, hd⟩
40   exact ⟨fun b => d b.val, hd⟩
41 
42 /-- A nonempty answer type supplies values for unattained representations. -/
43 theorem attained_iff_total [Nonempty C] (encode : A → B) (task : A → C) :
44     Sufficient encode task ↔ ProofPath.Sufficient encode task := by
45   constructor
46   · rintro ⟨d, hd⟩
47     classical
48     refine ⟨fun b => if h : ∃ a, encode a = b then d ⟨b, h⟩ else Classical.choice inferInstance, ?_⟩
49     intro a
50     simp only [dite_eq_left (show ∃ a', encode a' = encode a from ⟨a, rfl⟩)]
51     exact hd a
52   · exact total_implies_attained encode task
53 
54 theorem decoder_unique (encode : A → B) (task : A → C)
55     (d e : Image encode → C)
56     (hd : ∀ a, d (observed encode a) = task a)
57     (he : ∀ a, e (observed encode a) = task a) : d = e := by
58   funext b
59   obtain ⟨a, ha⟩ := b.property
60   have hb : observed encode a = b := Subtype.ext ha
61   rw [← hb, hd, he]
62 
63 /-- The complete obstruction is an identified pair with different task answers. -/
64 theorem not_sufficient_iff_collision (encode : A → B) (task : A → C) :
65     ¬ Sufficient encode task ↔ ∃ a a', encode a = encode a' ∧ task a ≠ task a' := by
66   rw [sufficient_iff_fiber_constant]
67   unfold FiberConstant
68   push Not
69   rfl
70 
71 def Recovers (coarse : A → B) (fine : A → C) : Prop := Sufficient fine coarse
72 
73 theorem recovers_refl (encode : A → B) : Recovers encode encode := by
74   apply (sufficient_iff_fiber_constant _ _).mpr
75   exact fun _ _ h => h
76 
77 theorem task_transport (coarse : A → B) (fine : A → C) (task : A → D)
78     (hr : Recovers coarse fine) (ht : Sufficient coarse task) : Sufficient fine task := by
79   apply (sufficient_iff_fiber_constant _ _).mpr
80   have h1 := (sufficient_iff_fiber_constant _ _).mp hr
81   have h2 := (sufficient_iff_fiber_constant _ _).mp ht
82   exact fun a b h => h2 a b (h1 a b h)
83 
84 theorem recovers_trans (r : A → B) (s : A → C) (t : A → D)
85     (hrs : Recovers r s) (hst : Recovers s t) : Recovers r t :=
86   task_transport s t r hst hrs
87 
88 /-- A tagged portfolio recovers each of its coordinates. -/
89 theorem portfolio_left (r : A → B) (s : A → C) :
90     Recovers r (fun a => (r a, s a)) := by
91   apply (sufficient_iff_fiber_constant _ _).mpr
92   exact fun _ _ h => congrArg Prod.fst h
93 
94 theorem portfolio_right (r : A → B) (s : A → C) :
95     Recovers s (fun a => (r a, s a)) := by
96   apply (sufficient_iff_fiber_constant _ _).mpr
97   exact fun _ _ h => congrArg Prod.snd h
98 
99 /-- Joint tasks supply the least information required by the entire task family. -/
100 theorem joint_sufficient_iff {I : Type*} {Y : I → Type*}
101     (encode : A → B) (tasks : (i : I) → A → Y i) :
102     Sufficient encode (fun a i => tasks i a) ↔ ∀ i, Sufficient encode (tasks i) := by
103   constructor
104   · intro h i
105     apply (sufficient_iff_fiber_constant _ _).mpr
106     intro a b hab
107     exact congrFun ((sufficient_iff_fiber_constant _ _).mp h a b hab) i
108   · intro h
109     apply (sufficient_iff_fiber_constant _ _).mpr
110     intro a b hab
111     funext i
112     exact (sufficient_iff_fiber_constant _ _).mp (h i) a b hab
113 
114 theorem injective_sufficient (encode : A → B) (task : A → C)
115     (hi : Function.Injective encode) : Sufficient encode task := by
116   apply (sufficient_iff_fiber_constant _ _).mpr
117   exact fun _ _ h => congrArg task (hi h)
118 
119 /-- Attained and total decoding differ when an empty archive has an empty answer type. -/
120 theorem empty_attained_not_total :
121     Sufficient (fun a : Empty => Empty.elim a : Empty → Unit) (id : Empty → Empty) ∧
122     ¬ ProofPath.Sufficient (fun a : Empty => Empty.elim a : Empty → Unit) (id : Empty → Empty) := by
123   constructor
124   · apply (sufficient_iff_fiber_constant _ _).mpr
125     intro a
126     exact Empty.elim a
127   · rintro ⟨d, _⟩
128     exact Empty.elim (d ())
129 
130 /-- Hashing cannot repair a distinction already lost by serialization. -/
131 theorem serialized_collision_persists (serialize : A → B) (hash : B → C)
132     {a b : A} (h : serialize a = serialize b) :
133     hash (serialize a) = hash (serialize b) := congrArg hash h
134 
135 /-- Every task recoverable from a digest was already recoverable from its bytes. -/
136 theorem hash_task_data_processing (serialize : A → B) (hash : B → C)
137     (task : A → D) (h : Sufficient (hash ∘ serialize) task) :
138     Sufficient serialize task := by
139   apply (sufficient_iff_fiber_constant _ _).mpr
140   intro a b he
141   exact (sufficient_iff_fiber_constant _ _).mp h a b (congrArg hash he)
142 
143 /-- Injectivity only on attained serializations is sufficient to lose no further tasks. -/
144 theorem hash_preserves_tasks (serialize : A → B) (hash : B → C)
145     (hi : Set.InjOn hash (Set.range serialize)) (task : A → D) :
146     Sufficient (hash ∘ serialize) task ↔ Sufficient serialize task := by
147   constructor
148   · exact hash_task_data_processing serialize hash task
149   · intro h
150     apply (sufficient_iff_fiber_constant _ _).mpr
151     intro a b he
152     apply (sufficient_iff_fiber_constant _ _).mp h a b
153     exact hi ⟨a, rfl⟩ ⟨b, rfl⟩ he
154 
155 end Recovery
156 end ProofPath

Back to source controls