Compression.lean

1 import Mathlib.Data.Set.Function
2 
3 namespace ProofPath
4 
5 /-- Task sufficiency is factorization, not the length of an encoding. -/
6 def Sufficient {A B C : Type*} (encode : A → B) (task : A → C) : Prop :=
7   ∃ decode : B → C, ∀ a, decode (encode a) = task a
8 
9 theorem collision_obstructs_sufficiency {A B C : Type*}
10     (encode : A → B) (task : A → C) {a b : A}
11     (hc : encode a = encode b) (ht : task a ≠ task b) :
12     ¬ Sufficient encode task := by
13   rintro ⟨decode, hd⟩
14   exact ht ((hd a).symm.trans ((congrArg decode hc).trans (hd b)))
15 
16 /-- Losslessness means injectivity. It does not require identical bytes. -/
17 theorem all_predicates_sufficient_iff_injective {A B : Type*} (encode : A → B) :
18     (∀ task : A → Prop, Sufficient encode task) ↔ Function.Injective encode := by
19   constructor
20   · intro h a b he
21     obtain ⟨d, hd⟩ := h (fun x => x = a)
22     have hba : (b = a) = (a = a) := (hd b).symm.trans ((congrArg d he.symm).trans (hd a))
23     exact (Eq.mp hba.symm rfl).symm
24   · intro hi task
25     refine ⟨fun b => ∃ a, encode a = b ∧ task a, ?_⟩
26     intro a
27     apply propext
28     constructor
29     · rintro ⟨a', he, ht⟩
30       exact hi he ▸ ht
31     · exact fun ht => ⟨a, rfl, ht⟩
32 
33 end ProofPath

Back to source controls