open import Level
open import Ordinals
module generic-filter {n : Level } (O : Ordinals {n})   where

import filter 
open import zf
open import logic
-- open import partfunc {n} O
import OD 

open import Relation.Nullary 
open import Relation.Binary 
open import Data.Empty 
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
import BAlgbra 

open BAlgbra O

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom
import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O


import ODC

open filter O

open _∧_
open _∨_
open Bool


open HOD

-------
--    the set of finite partial functions from ω to 2
--
--

open import Data.List hiding (filter)
open import Data.Maybe 

import OPair
open OPair O

record CountableOrdinal : Set (suc (suc n)) where
   field
       ctl→ : Nat → Ordinal
       ctl← : Ordinal → Nat
       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x

record CountableHOD : Set (suc (suc n)) where
   field
       mhod : HOD
       mtl→ : Nat → Ordinal
       mtl→∈P : (i : Nat) → odef mhod (mtl→ i)
       mtl← : (x : Ordinal) → odef mhod x → Nat
       mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x 
       mtl-iso← : { x : Nat }  → mtl← (mtl→ x ) (mtl→∈P x) ≡ x
   
       
open CountableOrdinal 
open CountableHOD

----
--   a(n) ∈ M
--   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q    
--
PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
PGHOD i C P p = record { od = record { def = λ x  →
       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
   ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }  

---
--   p(n+1) = if (f n) then qn otherwise p(n)
--
next-p :  (p : Ordinal) → (f : HOD → HOD) → Ordinal
next-p p f with is-o∅  ( & (f (* p)))  
next-p p f | yes y = p
next-p p f | no not = & (ODC.minimal O (f (* p) ) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice

---
--  ascendant search on p(n)
--
find-p :  (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
find-p C P Zero x = x
find-p C P (Suc i) x = find-p C P i ( next-p x (λ p → PGHOD i C P (& p) ))

---
-- G = { r ∈ Power P | ∃ n → r ⊆ p(n) }
--
record PDN  (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where
   field
       gr : Nat
       pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y
       x∈PP  : odef (Power P) x

open PDN

---
-- G as a HOD
--
PDHOD :  (C : CountableOrdinal) → (P : HOD ) → HOD
PDHOD C P = record { od = record { def = λ x →  PDN C P x }
    ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt)  } 

open PDN

----
--  Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set )
--
--  p 0 ≡ ∅
--  p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q  (axiom of choice)
---             else p n

P∅ : {P : HOD} → odef (Power P) o∅
P∅ {P} =  subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅  o∅≡od∅) where
    lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
    lemma x eq = power← P od∅  (λ {x} lt → ⊥-elim (¬x<0 lt ))
x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt

open _⊆_

P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
P-GenericFilter C P = record {
      genf = record { filter = PDHOD C P ; f⊆PL =  f⊆PL ; filter1 = {!!} ; filter2 = {!!} }
    ; generic = λ D → {!!}
   } where
        find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y 
        find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso
            ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
        find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p x (λ p → PGHOD i C P (& p)))   y {!!} {!!}
        f⊆PL :  PDHOD C P ⊆ Power P
        f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
             find-p-⊆P C P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }


open GenericFilter
open Filter

record Incompatible  (P : HOD ) : Set (suc (suc n)) where
   field
      except : HOD → ( HOD ∧ HOD )
      incompatible : { p : HOD } →  Power P ∋ p  →  Power P ∋ proj1 (except p )  →  Power P ∋ proj2 (except p ) 
          → ( p ⊆ proj1 (except p)  ) ∧ ( p ⊆ proj2 (except p)  )
          → ∀ ( r : HOD ) →  Power P ∋ r → ¬ (( proj1 (except p)  ⊆ r ) ∧ ( proj2 (except p)  ⊆ r ))

lemma725 : (M : CountableHOD ) (C : CountableOrdinal) (P : HOD ) →  mhod M ∋ Power P
    →  Incompatible P → ¬ ( mhod M ∋ filter ( genf ( P-GenericFilter C P )))
lemma725 = {!!}

open import PFOD O

-- HODω2 : HOD
-- 
-- ω→2 : HOD
-- ω→2 = Power infinite

lemma725-1 :   Incompatible HODω2
lemma725-1 = {!!}

lemma726 :  (C : CountableOrdinal) (P : HOD ) 
    →  Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2
lemma726 = {!!}

--
--   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
--
--   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }
--