Sorting histories can destroy eventual generation

def GenLimit.FiniteWitness.Sorting.language : Set ℕ

The positive natural numbers used for the sorting counterexample.

Equations

• GenLimit.FiniteWitness.Sorting.language = {n : ℕ | 0 < n}

def GenLimit.FiniteWitness.Sorting.output (xs : List ℕ) : ℕ

Output zero on a sorted sample with a gap, and otherwise output one above its maximum.

Equations

• GenLimit.FiniteWitness.Sorting.output xs = if List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) xs ∧ xs.toFinset ≠ Finset.Icc 1 (xs.toFinset.sup id) then 0 else xs.toFinset.sup id + 1

def GenLimit.FiniteWitness.Sorting.generator : Generic.Generator ℕ

The ordered-history generator implementing the sorting counterexample.

Equations

• GenLimit.FiniteWitness.Sorting.generator x✝ xs = GenLimit.FiniteWitness.Sorting.output (List.ofFn xs)

@[simp]

theorem GenLimit.FiniteWitness.Sorting.generator_output (stream : ℕ → ℕ) (t : ℕ) : Generic.output generator stream t = output (textPrefix stream t)

theorem GenLimit.FiniteWitness.Sorting.next_max_good (S : Finset ℕ) : S.sup id + 1 ∈ language ∧ S.sup id + 1 ∉ S

theorem GenLimit.FiniteWitness.Sorting.strictMono_of_all_prefixes {stream : ℕ → ℕ} (h : ∀ (t : ℕ), List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (textPrefix stream t)) : StrictMono stream

theorem GenLimit.FiniteWitness.Sorting.increasing_presented_sample {stream : ℕ → ℕ} (hp : Generic.Presents stream language) (hm : StrictMono stream) (t : ℕ) : Generic.sample stream t = Finset.Icc 1 ((Generic.sample stream t).sup id)

theorem GenLimit.FiniteWitness.Sorting.generator_success : Generic.IsLimitGenerator generator {language}

def GenLimit.FiniteWitness.Sorting.badStream (n : ℕ) : ℕ

The presentation starting with 1 and then interleaving 3, 2, 5, 4, and so on.

Equations

• GenLimit.FiniteWitness.Sorting.badStream n = if n = 0 then 1 else if n % 2 = 1 then n + 2 else n

theorem GenLimit.FiniteWitness.Sorting.badStream_presents : Generic.Presents badStream language

theorem GenLimit.FiniteWitness.Sorting.bad_sample_gap {k : ℕ} : 1 ≤ k → 2 * k ∉ Generic.sample badStream (2 * k)

theorem GenLimit.FiniteWitness.Sorting.bad_sample_large {k : ℕ} (hk : 1 ≤ k) : 2 * k + 1 ∈ Generic.sample badStream (2 * k)

def GenLimit.FiniteWitness.Sorting.sortedOutput (S : Finset ℕ) : ℕ

Evaluate the counterexample output after sorting the observed sample.

Equations

• GenLimit.FiniteWitness.Sorting.sortedOutput S = GenLimit.FiniteWitness.Sorting.output (S.sort fun (x1 x2 : ℕ) => x1 ≤ x2)

theorem GenLimit.FiniteWitness.Sorting.sorted_output_zero {k : ℕ} (hk : 1 ≤ k) : sortedOutput (Generic.sample badStream (2 * k)) = 0

theorem GenLimit.FiniteWitness.Sorting.sorted_generator_fails : ¬Generic.IsLimitGenerator (ofSet sortedOutput) {language}

theorem GenLimit.FiniteWitness.Sorting.sorting_counterexample : Generic.IsLimitGenerator generator {language} ∧ ¬Generic.IsLimitGenerator (ofSet sortedOutput) {language}