def List.all_pairs {α : Type} (l : List α) : List (α × α)

Equations

• [].all_pairs = []
• (h :: t).all_pairs = List.map (fun (x : α) => (h, x)) t ++ t.all_pairs

def List.mem_of_mem_all_pairs {α : Type} {l : List α} {p : α × α} (h : p ∈ l.all_pairs) : p.1 ∈ l ∧ p.2 ∈ l

Equations

• ⋯ = ⋯

theorem List.all_pairs_sorted_of_sorted {α : Type} {l : List α} {R : α → α → Prop} (h : Sorted R l) (p : α × α) : p ∈ l.all_pairs → R p.1 p.2

theorem List.all_pairs_neq_of_nodup {α : Type} {l : List α} (lnodup : l.Nodup) (p : α × α) : p ∈ l.all_pairs → p.1 ≠ p.2

theorem List.mem_all_pairs_iff_of_irrefl_of_antisymm_of_sorted {α : Type} {l : List α} {R : α → α → Prop} [Rirrefl : IsIrrefl α R] [Ranti : IsAntisymm α R] (lsorted : Sorted R l) (p : α × α) : p ∈ l.all_pairs ↔ R p.1 p.2 ∧ p.1 ∈ l ∧ p.2 ∈ l

theorem List.Sorted.antisymm_is_le_sorted_of_nodup_of_sorted {α : Type} {l : List α} {R : α → α → Prop} [Ranti : IsAntisymm α R] (hnodup : l.Nodup) (hsorted : Sorted R l) {a b : Fin l.length} (hab : R l[a] l[b]) : a ≤ b

theorem List.Sublist.sorted {α : Type} {l l' : List α} {R : α → α → Prop} (sub : l'.Sublist l) : Sorted R l → Sorted R l'

theorem triangular_monotone : Monotone fun (N : ℕ) => N * (N - 1) / 2

theorem triangular_next (n : ℕ) : n * (n - 1) / 2 + n = (n + 1) * n / 2

structure EdgeVar (N : ℕ) : Type

• i : Fin N
• j : Fin N
• ijord : self.i > self.j

def decoder {N : ℕ} (idx : Fin (N * (N - 1) / 2)) : EdgeVar N

Equations

• One or more equations did not get rendered due to their size.
• decoder idx_2 = idx_2.elim0

instance instIndexTypeEdgeVar (N : ℕ) : Trestle.IndexType (EdgeVar N)

Equations

• instIndexTypeEdgeVar N = { card := N * (N - 1) / 2, toFin := fun (v : EdgeVar N) => ⟨↑v.i * (↑v.i - 1) / 2 + ↑v.j, ⋯⟩, fromFin := decoder }

instance instLawfulIndexTypeEdgeVar (N : ℕ) : Trestle.LawfulIndexType (EdgeVar N)

def assignment_to_graph {N : ℕ} (τ : Trestle.Model.PropAssignment (EdgeVar N)) (polarity : Bool) : SimpleGraph (Fin N)

Equations

• One or more equations did not get rendered due to their size.

theorem assignment_to_graph_compl {N : ℕ} (τ : Trestle.Model.PropAssignment (EdgeVar N)) (p : Bool) : assignment_to_graph τ p = (assignment_to_graph τ !p)ᶜ

def CliqueFreeEncoding (N x : ℕ) (polarity : Bool) : Trestle.Encode.VEncCNF (EdgeVar N.succ) Unit fun (τ : Trestle.Model.PropAssignment (EdgeVar N.succ)) => (assignment_to_graph τ polarity).CliqueFree x

Equations

• One or more equations did not get rendered due to their size.

def RamseyEncoding (N x y : ℕ) : Trestle.Encode.VEncCNF (EdgeVar N.succ) Unit fun (τ : Trestle.Model.PropAssignment (EdgeVar N.succ)) => (assignment_to_graph τ true).cliqueNum < x ∧ (assignment_to_graph τ true).indepNum < y

Equations

• RamseyEncoding N x y = Trestle.Encode.VEncCNF.mapProp ⋯ ((CliqueFreeEncoding N x true).seq ((CliqueFreeEncoding N y false).seq (Trestle.Encode.VEncCNF.pure ())))

def main (argv : List String) : IO UInt32

Equations

• main argv = do Trestle.Solver.Dimacs.printICnf IO.print (↑(RamseyEncoding argv[0]!.toNat! argv[1]!.toNat! argv[2]!.toNat!)).toICnf pure 0