πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.Explorations.Forcing.Orthogonal where

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Termination.Ordering
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.More

Orthogonal forcing

This is work in progress to formalize a counterexample to the conjecture that the cartesian product of streamless sets is streamless.

Good : {X : Set} β†’ (X β†’ X β†’ Set) β†’ (β„• β†’ X) β†’ Set
Good _β‰ˆ_ f = βˆƒ[ i ] βˆƒ[ j ] i β‰’ j Γ— f i β‰ˆ f j 

key-lemma : (f : β„• β†’ β„•) (n : β„•) β†’ Good _≑_ f ⊎ βˆƒ[ i ] βˆƒ[ j ] i β‰’ j Γ— (f i β‰₯ n Γ— f j β‰₯ n)
key-lemma f n = {!!}
-- Proof idea: Inspect the first n + 2 values of f.
-- There are only n numbers smaller than n.
-- So if these values are all distinct, at least two of them are guaranteed to be β‰₯ n.
-- Else we have duplicates.
data Cl {X : Set} (_β‰ˆ_ : X β†’ X β†’ Set) : X β†’ X β†’ Set where
  β‰ˆ-base  : {a b : X} β†’ a β‰ˆ b β†’ Cl _β‰ˆ_ a b
  β‰ˆ-refl  : {a : X} β†’ Cl _β‰ˆ_ a a
  β‰ˆ-symm  : {a b : X} β†’ Cl _β‰ˆ_ a b β†’ Cl _β‰ˆ_ b a
  β‰ˆ-trans : {a b c : X} β†’ Cl _β‰ˆ_ a b β†’ Cl _β‰ˆ_ b c β†’ Cl _β‰ˆ_ a c

Cl' : {X : Set} β†’ List (X Γ— X) β†’ (X β†’ X β†’ Set)
Cl' ps = Cl (Ξ» a b β†’ (a , b) ∈ ps)

_β««_ : {X : Set} β†’ (R S : X β†’ X β†’ Set) β†’ Set
R β«« S = (a b : _) β†’ R a b β†’ S a b β†’ a ≑ b

L : Set
L = List (β„• Γ— β„•) Γ— List (β„• Γ— β„•)

data βˆ‡ (P : L β†’ Set) : L β†’ Set where
  now    : {Οƒ : L} β†’ P Οƒ β†’ βˆ‡ P Οƒ
  laterβ‚— : {R S : List (β„• Γ— β„•)} β†’ (f : β„• β†’ β„•) β†’ ((R' S' : List (β„• Γ— β„•)) β†’ Good (Cl' (R ++ R')) f β†’ βˆ‡ P (R ++ R' , S ++ S')) β†’ βˆ‡ P (R , S)
  laterα΅£ : {R S : List (β„• Γ— β„•)} β†’ (f : β„• β†’ β„•) β†’ ((R' S' : List (β„• Γ— β„•)) β†’ Good (Cl' (S ++ S')) f β†’ βˆ‡ P (R ++ R' , S ++ S')) β†’ βˆ‡ P (R , S)

escape : {P : L β†’ Set} (R S : List (β„• Γ— β„•)) β†’ Cl' R β«« Cl' S β†’ βˆ‡ P (R , S) β†’ βˆƒ[ R' ] βˆƒ[ S' ] (Cl' R' β«« Cl' S') Γ— P (R' , S')
escape = {!!}
theorem : Β¬ βˆ‡ (Ξ» (R , S) β†’ βˆƒ[ i ] βˆƒ[ j ] i β‰’ j Γ— Cl' R i j Γ— Cl' S i j) ([] , [])
theorem = {!!}