import HardnessReductions.Core
import HardnessReductions.Ordering.Defs

/-!
# BETWEENNESS

Given a finite set and a collection of ordered triples of its elements, is
there an arrangement of the set in a line — a one-to-one map onto the positions
`{1, …, |A|}` — under which the middle element of every prescribed triple lies
strictly between the two others, in one direction or the other?
Garey–Johnson's [MS1].

The question is *reversal-symmetric*: reversing an arrangement sends solutions
to solutions, because the condition on a triple is a disjunction over the two
directions. Every gadget reducing into the problem inherits that symmetry, so
nothing an arrangement decides is absolute — only relative to a distinguished
element, which is why the construction that lands here reads its truth values
as *sides* of one global element.

## Building the arrangement in a convenient order

A reduction does not build a map into `Fin |A|` directly: the positions are
determined by the whole instance, while a gadget knows only where each element
should sit *relative* to the others. `exists_btw_of_key` is the unbundling
lemma that closes the gap — any injection into any linearly ordered type is
enough, and the arrangement is recovered by counting predecessors. A gadget
that wants a block layout with room reserved inside the blocks takes the key
type to be a lexicographic product (`Betweenness/FromNae3Sat.lean`), where no
gap arithmetic is needed at all.

Hardness proof (in `Betweenness/`): from NAE3SAT (`FromNae3Sat.lean`, Opatrný's
gadget — one global element whose two sides are the truth values, and one fresh
element per clause forced to the side opposite the clause's first literal and
between the other two; certified in `FromNae3Sat/Code.lean` and
`FromNae3Sat/Adequacy.lean`).
-/

namespace Hardness

/-- BETWEENNESS: is there a one-to-one arrangement of the elements under which
every prescribed triple's middle element lies strictly between its other two? -/
def BETWEENNESS : Problem TripleSystemInstance := fun x ↦
  ∃ f : x.A → Fin (Fintype.card x.A), Function.Injective f ∧ ∀ t ∈ x.triples, Btw f t

/-! ### From a key to an arrangement -/

/-- **The unbundling lemma**: an arrangement may be specified by an injection
into *any* linearly ordered type. The positions are recovered by counting
predecessors, which is strictly monotone, so the betweenness conditions
transfer one by one. -/
theorem exists_btw_of_key {A K : Type*} [Fintype A] [LinearOrder K]
    (T : List (A × A × A)) (k : A → K) (hk : Function.Injective k)
    (h : ∀ t ∈ T, Btw k t) :
    ∃ f : A → Fin (Fintype.card A), Function.Injective f ∧ ∀ t ∈ T, Btw f t := by
  classical
  set r : A → ℕ := fun a ↦ (Finset.univ.filter fun b ↦ k b < k a).card with hrdef
  have hmono : ∀ a b : A, k a < k b → r a < r b := by
    intro a b hab
    refine Finset.card_lt_card ((Finset.ssubset_iff_of_subset ?_).mpr ⟨a, ?_, ?_⟩)
    · exact fun c hc ↦ Finset.mem_filter.mpr
        ⟨Finset.mem_univ c, lt_trans (Finset.mem_filter.mp hc).2 hab⟩
    · exact Finset.mem_filter.mpr ⟨Finset.mem_univ a, hab⟩
    · simp
  have hlt : ∀ a, r a < Fintype.card A := by
    intro a
    have hss : (Finset.univ.filter fun b ↦ k b < k a) ⊂ (Finset.univ : Finset A) :=
      (Finset.ssubset_iff_of_subset (Finset.subset_univ _)).mpr
        ⟨a, Finset.mem_univ a, by simp⟩
    simpa using Finset.card_lt_card hss
  refine ⟨fun a ↦ ⟨r a, hlt a⟩, fun a b hab ↦ ?_, fun t ht ↦ ?_⟩
  · have hr : r a = r b := congrArg Fin.val hab
    rcases lt_trichotomy (k a) (k b) with hk' | hk' | hk'
    · exact absurd hr (Nat.ne_of_lt (hmono a b hk'))
    · exact hk hk'
    · exact absurd hr.symm (Nat.ne_of_lt (hmono b a hk'))
  · exact (h t ht).imp
      (fun hc ↦ ⟨Fin.mk_lt_mk.mpr (hmono _ _ hc.1), Fin.mk_lt_mk.mpr (hmono _ _ hc.2)⟩)
      fun hc ↦ ⟨Fin.mk_lt_mk.mpr (hmono _ _ hc.1), Fin.mk_lt_mk.mpr (hmono _ _ hc.2)⟩

/-! ### Renaming invariance -/

/-- One direction of the invariance, which the two uses instantiate at `e` and
at `e.symm`. -/
private theorem exists_btw_transport {A B : Type*} [Fintype A] [Fintype B]
    {S : List (A × A × A)} {T : List (B × B × B)} (e : A ≃ B)
    (h : ∀ t : A × A × A, (e t.1, e t.2.1, e t.2.2) ∈ T → t ∈ S)
    (hf : ∃ f : A → Fin (Fintype.card A), Function.Injective f ∧ ∀ t ∈ S, Btw f t) :
    ∃ g : B → Fin (Fintype.card B), Function.Injective g ∧ ∀ t ∈ T, Btw g t := by
  obtain ⟨f, hinj, hbtw⟩ := hf
  have hcard : Fintype.card A = Fintype.card B := Fintype.card_congr e
  have hstrict : StrictMono (finCongr hcard) := fun a b hab ↦ by
    rw [Fin.lt_def, finCongr_apply, finCongr_apply, Fin.val_cast, Fin.val_cast]
    exact hab
  refine ⟨fun b ↦ finCongr hcard (f (e.symm b)), fun a b hab ↦ ?_, fun t ht ↦ ?_⟩
  · exact e.symm.injective (hinj ((finCongr hcard).injective hab))
  · have hmem : (e (e.symm t.1), e (e.symm t.2.1), e (e.symm t.2.2)) ∈ T := by
      simpa using ht
    exact Btw.comp_strictMono hstrict
      (hbtw (e.symm t.1, e.symm t.2.1, e.symm t.2.2) (h _ hmem))

/-- **Renaming invariance**, in the shape the certificates produce and the
representation pair consumes: a bijection of the elements matching the two
triple collections carries arrangements both ways. The witness is indexed by
the *positions*, so the transport composes with `finCongr` on the counts, which
is strictly monotone and therefore preserves betweenness. -/
theorem exists_btw_iff_of_equiv {A B : Type*} [Fintype A] [Fintype B]
    {S : List (A × A × A)} {T : List (B × B × B)} (e : A ≃ B)
    (hmem : ∀ t : A × A × A, t ∈ S ↔ (e t.1, e t.2.1, e t.2.2) ∈ T) :
    (∃ f : A → Fin (Fintype.card A), Function.Injective f ∧ ∀ t ∈ S, Btw f t) ↔
      ∃ g : B → Fin (Fintype.card B), Function.Injective g ∧ ∀ t ∈ T, Btw g t := by
  constructor
  · exact exists_btw_transport e fun t ht ↦ (hmem t).mpr ht
  · refine exists_btw_transport e.symm fun t ht ↦ ?_
    have := (hmem (e.symm t.1, e.symm t.2.1, e.symm t.2.2)).mp ht
    simpa using this

end Hardness