import HardnessReductions.Numbers.Encoding
import HardnessReductions.Numbers.Partition.FromSubsetSum.Certified
import HardnessReductions.Numbers.Knapsack.FromSubsetSum.Certified
import HardnessReductions.Numbers.BinPacking.FromPartition.Certified
import HardnessReductions.Numbers.BinPacking.FromPartition3.Adequacy
import HardnessReductions.Numbers.Partition4.FromMatching3D.Adequacy
import HardnessReductions.Numbers.Partition3.FromPartition4.Adequacy
import HardnessReductions.Sets.Representation

/-!
# Representation: the bundled number problems are their concrete encodings

The `Numbers/` instalment of the representation theorems
(`Graph/Representation.lean` explains the triangle), and the degenerate one:
here the encodings are *bijections*, and both legs are `rfl`.

That is not luck, and it is worth saying why, because it locates where the
other domains' work actually went. A bundled graph, set system or SAT instance
carries an abstract carrier type — `V`, `U`, `x.V` — with a `Fintype` or a
`DecidableEq` and nothing else, so the concrete side has to *name* its elements
by numbers, and the representation theorem is the proof that the naming loses
nothing. A `NumberTargetInstance` has no carrier: it is a list of naturals and a
target, which is already first-order data. Encoding is repackaging.

The honesty that the other domains buy with `Fintype.equivFin` is bought here
by the size model instead — numbers are charged by bit length (`Nat.size`), so
a "trivial" encoding is still not a free lunch, it is just not a *naming*
problem. Hence `decodeNumberTarget_encodeNumberTarget` and its three companions:
the four `rfl`s are the whole content, and stating them is the point.
-/

namespace Hardness
namespace Cert

/-! ## SUBSET SUM -/

/-- Encode a bundled SUBSET SUM instance: repackage the numbers and the
target. -/
def encodeNumberTarget (x : NumberTargetInstance) : NumberTargetTy.denote :=
  (x.nums, x.target)

/-- **The round trip**: decoding the encoding returns the very same instance —
not merely one isomorphic to it, as in every other domain. -/
theorem decodeNumberTarget_encodeNumberTarget (x : NumberTargetInstance) :
    decodeNumberTarget (encodeNumberTarget x) = x := rfl

/-- The other round trip: encoding the decoding returns the very same concrete
instance. The encoding is a bijection, so nothing is lost in either
direction. -/
theorem encodeNumberTarget_decodeNumberTarget (y : NumberTargetTy.denote) :
    encodeNumberTarget (decodeNumberTarget y) = y := rfl

/-- SUBSET SUM is faithfully represented by its concrete encoding. -/
def subsetSumToConcrete : SUBSET_SUM ⟶ᵣ Concrete.SUBSET_SUM :=
  ⟨encodeNumberTarget, fun _ ↦ Iff.rfl⟩

/-- Concrete SUBSET SUM interprets back: definitional. -/
def concreteToSubsetSum : Concrete.SUBSET_SUM ⟶ᵣ SUBSET_SUM :=
  ⟨decodeNumberTarget, fun _ ↦ Iff.rfl⟩

/-! ## PARTITION -/

/-- Encode a bundled PARTITION instance: its list of numbers. -/
def encodePartition (x : PartitionInstance) : PartitionTy.denote := x.nums

/-- **The round trip**: decoding the encoding returns the very same
instance. -/
theorem decodePartition_encodePartition (x : PartitionInstance) :
    decodePartition (encodePartition x) = x := rfl

/-- The other round trip: the encoding is a bijection here too. -/
theorem encodePartition_decodePartition (y : PartitionTy.denote) :
    encodePartition (decodePartition y) = y := rfl

/-- PARTITION is faithfully represented by its concrete encoding. -/
def partitionToConcrete : PARTITION ⟶ᵣ Concrete.PARTITION :=
  ⟨encodePartition, fun _ ↦ Iff.rfl⟩

/-- Concrete PARTITION interprets back: definitional. -/
def concreteToPartition : Concrete.PARTITION ⟶ᵣ PARTITION :=
  ⟨decodePartition, fun _ ↦ Iff.rfl⟩

/-! ## KNAPSACK -/

/-- Encode a bundled KNAPSACK instance: repackage the items and the two
thresholds. Carrying sizes and values as one list of pairs is what keeps this a
repackaging — two parallel lists would have to be zipped, and their length
agreement is exactly the well-formedness condition the instance type was chosen
to avoid. -/
def encodeKnapsack (x : KnapsackInstance) : KnapsackTy.denote :=
  ((x.items, x.capacity), x.goal)

/-- **The round trip**: decoding the encoding returns the very same
instance. -/
theorem decodeKnapsack_encodeKnapsack (x : KnapsackInstance) :
    decodeKnapsack (encodeKnapsack x) = x := rfl

/-- The other round trip: the encoding is a bijection here too. -/
theorem encodeKnapsack_decodeKnapsack (y : KnapsackTy.denote) :
    encodeKnapsack (decodeKnapsack y) = y := rfl

/-- KNAPSACK is faithfully represented by its concrete encoding. -/
def knapsackToConcrete : KNAPSACK ⟶ᵣ Concrete.KNAPSACK :=
  ⟨encodeKnapsack, fun _ ↦ Iff.rfl⟩

/-- Concrete KNAPSACK interprets back: definitional. -/
def concreteToKnapsack : Concrete.KNAPSACK ⟶ᵣ KNAPSACK :=
  ⟨decodeKnapsack, fun _ ↦ Iff.rfl⟩

/-! ## BIN PACKING -/

/-- Encode a bundled BIN PACKING instance: repackage the sizes, the capacity and
the number of bins. -/
def encodeBinPacking (x : BinPackingInstance) : BinPackingTy.denote :=
  (x.sizes, (x.capacity, x.bins))

/-- **The round trip**: decoding the encoding returns the very same
instance. -/
theorem decodeBinPacking_encodeBinPacking (x : BinPackingInstance) :
    decodeBinPacking (encodeBinPacking x) = x := rfl

/-- The other round trip: the encoding is a bijection here too. -/
theorem encodeBinPacking_decodeBinPacking (y : BinPackingTy.denote) :
    encodeBinPacking (decodeBinPacking y) = y := rfl

/-- BIN PACKING is faithfully represented by its concrete encoding. -/
def binPackingToConcrete : BIN_PACKING ⟶ᵣ Concrete.BIN_PACKING :=
  ⟨encodeBinPacking, fun _ ↦ Iff.rfl⟩

/-- Concrete BIN PACKING interprets back: definitional. -/
def concreteToBinPacking : Concrete.BIN_PACKING ⟶ᵣ BIN_PACKING :=
  ⟨decodeBinPacking, fun _ ↦ Iff.rfl⟩

/-! ## The unary avatar

The same instance data with every number unary-encoded
(`NumberTargetUnaryTy`), the avatar the strong-hardness chain certifies
against. Two things are different here, and both are the point.

*The encoding is no longer a bijection.* Decoding reads a number off as a
*length* and ignores the entries, so the concrete side has junk: `[true]` and
`[false]` are the same number. Only the round trip through a bundled instance
is an identity; the other composite is idempotent, not the identity.

*One leg is a program, the other is not.* Unary → binary is `unaryToNat`
applied pointwise, so the passage from the unary avatar to the binary one is
a certified reduction. The reverse passage is a Lean function like any other
(`encodeUnary` below), and `no_binary_to_unary` proves that it cannot be a
program of the builder language — the size model forbids it. The asymmetry is
the formal content of "strongly NP-hard": hardness proved against the unary
avatar transfers to the binary one, and not conversely. -/

/-- The unary encoding of a number: a list of that length. An ordinary Lean
function, and deliberately *not* a `Code` program — see `no_binary_to_unary`
for the proof that no program computes it. -/
def encodeUnary (n : ℕ) : List Bool := List.replicate n true

@[simp] theorem unaryVal_encodeUnary (n : ℕ) : unaryVal (encodeUnary n) = n :=
  List.length_replicate

/-- Encode a bundled number-target instance in unary. -/
def encodeNumberTargetUnary (x : NumberTargetInstance) :
    NumberTargetUnaryTy.denote :=
  (x.nums.map encodeUnary, encodeUnary x.target)

/-- **The round trip**: decoding the unary encoding returns the very same
instance. The reverse composite is *not* the identity — it normalizes every
entry to `true`s — which is why only this one is stated. -/
theorem decodeNumberTargetUnary_encodeNumberTargetUnary
    (x : NumberTargetInstance) :
    decodeNumberTargetUnary (encodeNumberTargetUnary x) = x := by
  unfold decodeNumberTargetUnary encodeNumberTargetUnary
  rw [List.map_map]
  have h : (unaryVal ∘ encodeUnary) = id := funext fun n ↦ unaryVal_encodeUnary n
  rw [h, List.map_id, unaryVal_encodeUnary]

/-- 4-PARTITION is faithfully represented by its concrete *unary* encoding. -/
def fourPartitionToConcreteUnary :
    FOUR_PARTITION ⟶ᵣ Concrete.FOUR_PARTITION_UNARY :=
  ⟨encodeNumberTargetUnary, fun x ↦ by
    change _ ↔ FOUR_PARTITION (decodeNumberTargetUnary
      (encodeNumberTargetUnary x))
    rw [decodeNumberTargetUnary_encodeNumberTargetUnary]⟩

/-- Concrete unary 4-PARTITION interprets back: definitional. -/
def concreteUnaryToFourPartition :
    Concrete.FOUR_PARTITION_UNARY ⟶ᵣ FOUR_PARTITION :=
  ⟨decodeNumberTargetUnary, fun _ ↦ Iff.rfl⟩

/-- 3-PARTITION is faithfully represented by its concrete *unary* encoding. -/
def threePartitionToConcreteUnary :
    THREE_PARTITION ⟶ᵣ Concrete.THREE_PARTITION_UNARY :=
  ⟨encodeNumberTargetUnary, fun x ↦ by
    change _ ↔ THREE_PARTITION (decodeNumberTargetUnary
      (encodeNumberTargetUnary x))
    rw [decodeNumberTargetUnary_encodeNumberTargetUnary]⟩

/-- Concrete unary 3-PARTITION interprets back: definitional. -/
def concreteUnaryToThreePartition :
    Concrete.THREE_PARTITION_UNARY ⟶ᵣ THREE_PARTITION :=
  ⟨decodeNumberTargetUnary, fun _ ↦ Iff.rfl⟩

/-- Windowed 3-PARTITION is faithfully represented by its concrete *unary*
encoding: the round trip returns the very same instance, so the window transfers
with the question. The form the strong-hardness chain's descendants consume. -/
def threePartitionWindowToConcreteUnary :
    THREE_PARTITION.restrict ThreePartitionWindow ⟶ᵣ
      Concrete.THREE_PARTITION_UNARY_WINDOW :=
  ⟨encodeNumberTargetUnary, fun x ↦ by
    change _ ↔ (THREE_PARTITION.restrict ThreePartitionWindow)
      (decodeNumberTargetUnary (encodeNumberTargetUnary x))
    rw [decodeNumberTargetUnary_encodeNumberTargetUnary]⟩

/-- Concrete windowed unary 3-PARTITION interprets back: definitional. -/
def concreteUnaryToThreePartitionWindow :
    Concrete.THREE_PARTITION_UNARY_WINDOW ⟶ᵣ
      THREE_PARTITION.restrict ThreePartitionWindow :=
  ⟨decodeNumberTargetUnary, fun _ ↦ Iff.rfl⟩

/-! ### Unary → binary, certified -/

/-- Read every unary number off as a binary one: `unaryToNat` under the list,
and on the target. -/
def unaryToBinaryCode : Code NumberTargetUnaryTy NumberTargetTy :=
  .pair (.comp .fst (.listMap unaryToNat)) (.comp .snd unaryToNat)

theorem decodeNumberTarget_unaryToBinaryCode (y : NumberTargetUnaryTy.denote) :
    decodeNumberTarget (unaryToBinaryCode.eval y) = decodeNumberTargetUnary y :=
  rfl

/-- **The crossing that is a program**: the unary avatar of 4-PARTITION
reduces to the binary one, certified. Hardness proved against the unary
avatar therefore holds against the binary problem as well — the transfer that
"strongly NP-hard" names. -/
def unaryToBinaryFourPartitionCertified :
    CertifiedReduction Concrete.FOUR_PARTITION_UNARY Concrete.FOUR_PARTITION where
  code := unaryToBinaryCode
  correct _ := Iff.rfl

/-- The same crossing for 3-PARTITION: the same program, and the same
transfer. -/
def unaryToBinaryThreePartitionCertified :
    CertifiedReduction Concrete.THREE_PARTITION_UNARY Concrete.THREE_PARTITION where
  code := unaryToBinaryCode
  correct _ := Iff.rfl

/-! ### The crossing that is not a program -/

/-- Exponentials outrun monomials: for every `C` and `d` there is an input
size at which `2 ^ k` exceeds the bound `polyBound C d (k + 2)`. The witness
is explicit — no asymptotics, just the bit-length arithmetic of
`Cert/Language.lean`: `2 ^ m` beats a *linear* function of `m` through
`2 ^ (a + b) ≥ (a + 1)(b + 1)`, and bit-lengths turn the monomial into a
linear function of `m`. -/
theorem exists_two_pow_gt_polyBound (C d : ℕ) :
    ∃ k : ℕ, polyBound C d (k + 2) < 2 ^ k := by
  refine ⟨2 ^ (C.size + d ^ 2 + 2 * d + 2) - 3, ?_⟩
  set m := C.size + d ^ 2 + 2 * d + 2 with hm
  set k := 2 ^ m - 3 with hk
  have h2m : 2 ^ 2 ≤ 2 ^ m := Nat.pow_le_pow_right (by omega) (by omega)
  have hk3 : k + 3 = 2 ^ m := by
    have : (2 : ℕ) ^ 2 = 4 := by norm_num
    omega
  -- the bound's own bit-length is at most `C.size + d * (m + 1) + 1`
  have hsizeb : (polyBound C d (k + 2)).size ≤ C.size + d * (m + 1) + 1 := by
    have h1 : (k + 3).size = m + 1 := by rw [hk3, Nat.size_pow]
    have h2 : ((k + 3) ^ d).size ≤ d * (k + 3).size + 1 := size_pow_le _ _
    calc (polyBound C d (k + 2)).size = (C * (k + 3) ^ d).size := rfl
      _ ≤ C.size + ((k + 3) ^ d).size := size_mul_le _ _
      _ ≤ C.size + (d * (k + 3).size + 1) := by omega
      _ = C.size + d * (m + 1) + 1 := by rw [h1]; omega
  -- and `2 ^ m` beats that linear quantity
  have hlin : C.size + d * (m + 1) + 4 ≤ 2 ^ m := by
    have ha : d + 2 ≤ 2 ^ (d + 1) := by
      have := Nat.lt_two_pow_self (n := d + 1)
      omega
    have hb : C.size + d ^ 2 + d + 2 ≤ 2 ^ (C.size + d ^ 2 + d + 1) := by
      have := Nat.lt_two_pow_self (n := C.size + d ^ 2 + d + 1)
      omega
    have hsplit : (d + 2) * (C.size + d ^ 2 + d + 2) ≤ 2 ^ m := by
      calc (d + 2) * (C.size + d ^ 2 + d + 2)
          ≤ 2 ^ (d + 1) * 2 ^ (C.size + d ^ 2 + d + 1) := Nat.mul_le_mul ha hb
        _ = 2 ^ m := by rw [← pow_add, hm]; ring_nf
    have hexp : C.size + d * (m + 1) + 4 ≤ (d + 2) * (C.size + d ^ 2 + d + 2) := by
      rw [hm]
      nlinarith [Nat.zero_le (d * C.size), Nat.zero_le (d ^ 3), Nat.zero_le (d ^ 2)]
    exact hexp.trans hsplit
  calc polyBound C d (k + 2) < 2 ^ (polyBound C d (k + 2)).size :=
        Nat.lt_size_self _
    _ ≤ 2 ^ k := Nat.pow_le_pow_right (by omega) (by omega)

/-- **Binary → unary is not a program.** No `Code .nat .unary` turns a number
into a unary numeral of that value: its output would have size at least twice
the value while its input has size only the value's *bit-length*, and the
blanket bound `Code.cost_size_le_polyBound` forbids that gap. This is the
theorem behind the standing rule that the language has no `range` primitive,
and the reason strong hardness has to be proved against the unary avatar
rather than transported to it. -/
theorem no_binary_to_unary :
    ¬ ∃ c : Code .nat Ty.unary, ∀ n : ℕ, unaryVal (c.eval n) = n := by
  rintro ⟨c, hc⟩
  obtain ⟨C, d, hbound⟩ := Code.cost_size_le_polyBound c
  obtain ⟨k, hk⟩ := exists_two_pow_gt_polyBound C d
  have hsize : (2 : ℕ) ^ k ≤ Ty.size Ty.unary (c.eval (2 ^ k)) := by
    rw [Ty.size_list]
    have hlen : (c.eval (2 ^ k)).length = 2 ^ k := hc (2 ^ k)
    omega
  have hin : Ty.size .nat (2 ^ k) = k + 2 := by
    rw [Ty.size_nat, Nat.size_pow]
  have h := hbound (2 ^ k)
  rw [hin] at h
  omega

/-! ### The unary avatar of BIN PACKING -/

/-- Encode a bundled BIN PACKING instance in unary: sizes, capacity and bin
count all as numerals. -/
def encodeBinPackingUnary (x : BinPackingInstance) : BinPackingUnaryTy.denote :=
  (x.sizes.map encodeUnary, (encodeUnary x.capacity, encodeUnary x.bins))

/-- **The round trip**: decoding the unary encoding returns the very same
instance. As for the number-target type, the reverse composite is idempotent
rather than the identity — decoding reads lengths and forgets entries. -/
theorem decodeBinPackingUnary_encodeBinPackingUnary (x : BinPackingInstance) :
    decodeBinPackingUnary (encodeBinPackingUnary x) = x := by
  unfold decodeBinPackingUnary encodeBinPackingUnary
  rw [List.map_map]
  have h : (unaryVal ∘ encodeUnary) = id := funext fun n ↦ unaryVal_encodeUnary n
  rw [h, List.map_id, unaryVal_encodeUnary, unaryVal_encodeUnary]

/-- BIN PACKING is faithfully represented by its concrete *unary* encoding. -/
def binPackingToConcreteUnary : BIN_PACKING ⟶ᵣ Concrete.BIN_PACKING_UNARY :=
  ⟨encodeBinPackingUnary, fun x ↦ by
    change _ ↔ BIN_PACKING (decodeBinPackingUnary (encodeBinPackingUnary x))
    rw [decodeBinPackingUnary_encodeBinPackingUnary]⟩

/-- Concrete unary BIN PACKING interprets back: definitional. -/
def concreteUnaryToBinPacking : Concrete.BIN_PACKING_UNARY ⟶ᵣ BIN_PACKING :=
  ⟨decodeBinPackingUnary, fun _ ↦ Iff.rfl⟩

/-! ## The loop, closed -/

/-- The abstract SUBSET SUM → PARTITION reduction, recovered from the certified
padding program. -/
example : SUBSET_SUM ⟶ᵣ PARTITION :=
  subsetSumToConcrete.comp
    (subsetSumToPartitionCertified.toReduction.comp concreteToPartition)

/-- The abstract SUBSET SUM → KNAPSACK reduction, recovered from the certified
duplication program. -/
example : SUBSET_SUM ⟶ᵣ KNAPSACK :=
  subsetSumToConcrete.comp
    (ssToKnapsackCertified.toReduction.comp concreteToKnapsack)

/-- The abstract PARTITION → BIN PACKING reduction, recovered from the
certified doubling program. -/
example : PARTITION ⟶ᵣ BIN_PACKING :=
  partitionToConcrete.comp
    (partitionToBinPackingCertified.toReduction.comp concreteToBinPacking)

/-- The abstract 3-DIMENSIONAL MATCHING → BIN PACKING reduction, recovered from
the strong chain: every step is a program, and every number the chain emits is
unary until the last decoding. -/
noncomputable example : MATCHING_3D ⟶ᵣ BIN_PACKING :=
  matching3DToConcrete.comp
    (matching3DToBinPackingCertified.toReduction.comp concreteUnaryToBinPacking)

/-- The abstract 3-DIMENSIONAL MATCHING → 4-PARTITION reduction, recovered
from the certified program that targets the *unary* avatar: the loop closes
across domains, and across encodings of numbers. -/
noncomputable example : MATCHING_3D ⟶ᵣ FOUR_PARTITION :=
  matching3DToConcrete.comp
    (matching3DToFourPartitionUnaryCertified.toReduction.comp
      concreteUnaryToFourPartition)

/-- The abstract 3-DIMENSIONAL MATCHING → 3-PARTITION reduction, recovered
from the certified chain through the unary avatar — the Garey–Johnson
strong-hardness chain, with nothing left on the mathematical side alone. -/
noncomputable example : MATCHING_3D ⟶ᵣ THREE_PARTITION :=
  matching3DToConcrete.comp
    (matching3DToThreePartitionUnaryCertified.toReduction.comp
      concreteUnaryToThreePartition)

end Cert
end Hardness