coding_theory.lean

import tactic
import .hamming

open_locale hamm

-- I've created this as a class though I'm not sure about this, with the idea that
-- per the advice in the embedding_like documentation, this will allow me to extend
-- the notion of embedding.
class block_code_class (F : Type*) (X Y : out_param $ Type*) (n : ℕ)
  extends embedding_like F X 𝓗[Y, n]

structure block_code (X Y : Type*) (n : ℕ) :=
(to_fun : X → 𝓗[Y, n])
(injective' : function.injective to_fun)

namespace block_code
variables (X Y : Type*) (n : ℕ)

instance : block_code_class (block_code X Y n) X Y n:=
{ coe := block_code.to_fun,
  coe_injective' := λ f g h, by cases f; cases g; congr',
  injective' := block_code.injective' }

instance : has_coe_to_fun (block_code X Y n) (λ _, X → (fin n → Y)) := ⟨block_code.to_fun⟩

@[simp] lemma to_fun_eq_coe {f : block_code X Y n} : f.to_fun = (f : X → (fin n → Y)) := rfl

@[ext] theorem ext {C C' : block_code X Y n} (h : ∀ x, C x = C' x) : C = C' := fun_like.ext C C' h

protected def copy (C : block_code X Y n) (C' : X → (fin n → Y)) (h : C' = ⇑C) : block_code X Y n :=
{ to_fun := C',
  injective' := h.symm ▸ C.injective', }

def codewords (C : block_code X Y n) : set (𝓗[Y, n]) := set.range C

/-
We technically could do with something that works a bit like a set_like structure here - in particular there is a 
notion of "subcode" which could at least be reflected in codes inheriting the partial
order on their codeword sets.

Notice that this induces a notion of "equality" (that is to say, equal codeword sets) that
is NOT the same =.
-/

/-
I want a structure here that represents a "block_code_hom". Given:
* A block_code X Y n
* An embedding X' ↪ X
* An embedding Y ↪ Y'

I want to construct a block_code X' Y' n in the obvious diagram-chasing way.

This is itself an embedding_like
-/

/-
A block_code_equiv should be the same but X ≃ X', Y ≃ Y'.
-/


/-
It should be true that given two equivalent block codes, their codewords are equivalent under the
equivalency composition, and similarly for the block_code_hom.
-/

/-
Also (and this is possibly the same as the above notions) there is a notion of "preserving the Hamming distances on 
codewords". 
-/
end block_code

/-
Want something like this for a linear block code, which somehow adds on that the codewords have a submodule structure.

structure linear_code (X Y : Type*) (n : ℕ)
  extends block_code X Y n :=
-/

/-
Linear codes also want notions of "code homs" and "code equivs" but which preserve the Hamming distance and/or are linear?
-/