import Beth.Semantics
import Beth.BethTrees
import Logic.Syntax
import Beth.Coverage

/-!
## Trivial Beth Frame from a Kripke Frame

Any Kripke frame gives rise to a trivial Beth frame with coverage given
by all maximal sieves i.e. the discrete topology

-/

namespace Beth

namespace Examples

open Syntax

universe u

instance bethFrameOfKripke (W : Type u) [F : Kripke.Frame W] : BethFrame W where
  coverage := maximalSieveCoverage W
  val      := F.val
  le_val   := F.le_val
  sheaf_condition := by
W : Type u
F : Kripke.Frame W
⊢ ∀ {i : ℕ} {w : W} {S : Sieve w}, covers w S → (∀ q ∈ S, Kripke.Frame.val q i) → Kripke.Frame.val w i
    intro i w
W : Type u
F : Kripke.Frame W
i : ℕ
w : W
⊢ ∀ {S : Sieve w}, covers w S → (∀ q ∈ S, Kripke.Frame.val q i) → Kripke.Frame.val w i S
W : Type u
F : Kripke.Frame W
i : ℕ
w : W
S : Sieve w
⊢ covers w S → (∀ q ∈ S, Kripke.Frame.val q i) → Kripke.Frame.val w i hS
W : Type u
F : Kripke.Frame W
i : ℕ
w : W
S : Sieve w
hS : covers w S
⊢ (∀ q ∈ S, Kripke.Frame.val q i) → Kripke.Frame.val w i hval
W : Type u
F : Kripke.Frame W
i : ℕ
w : W
S : Sieve w
hS : covers w S
hval : ∀ q ∈ S, Kripke.Frame.val q i
⊢ Kripke.Frame.val w i
    apply hval w
W : Type u
F : Kripke.Frame W
i : ℕ
w : W
S : Sieve w
hS : covers w S
hval : ∀ q ∈ S, Kripke.Frame.val q i
⊢ w ∈ S
    show w ∈ S.carrier
W : Type u
F : Kripke.Frame W
i : ℕ
w : W
S : Sieve w
hS : covers w S
hval : ∀ q ∈ S, Kripke.Frame.val q i
⊢ w ∈ S.carrier
    rw [hS]
W : Type u
F : Kripke.Frame W
i : ℕ
w : W
S : Sieve w
hS : covers w S
hval : ∀ q ∈ S, Kripke.Frame.val q i
⊢ w ∈ (maximal_sieve w).carrier; exact le_refl w
  nonempty_covers := by
W : Type u
F : Kripke.Frame W
⊢ ∀ {w : W} {S : Sieve w}, covers w S → Nonempty ↑S.carrier
    intro w S
W : Type u
F : Kripke.Frame W
w : W
S : Sieve w
⊢ covers w S → Nonempty ↑S.carrier hS
W : Type u
F : Kripke.Frame W
w : W
S : Sieve w
hS : covers w S
⊢ Nonempty ↑S.carrier
    exact ⟨⟨w, by
W : Type u
F : Kripke.Frame W
w : W
S : Sieve w
hS : covers w S
⊢ w ∈ S.carrier rw [hS]
W : Type u
F : Kripke.Frame W
w : W
S : Sieve w
hS : covers w S
⊢ w ∈ (maximal_sieve w).carrier; exact le_refl w⟩⟩

namespace BinaryBitsTree

section BinaryBitsTree

open BethTrees

/-!
### Binary Bits Tree as a Beth Frame

Binary tree over `Bool` is the `BethTree` where every node is valid.

We have the following valuation:
- `val xs p = (εₛ :> ff ≤ xs)`    — "p forced along left branch"
- `val xs q = (εₛ :> tt ≤ xs)`    — "q forced along right branch"
- `val l _ = False`               — no other variables forced

We can then use a bar at depth 1 to show that p ∨ q is true at the root.
Note that this is not true in the underlying Kripke frame
-/

def fullBinaryTree : BethTree Bool where
  tree_node _ := True
  root        := trivial
  prefix_closed _ _ _ := trivial
  pruned _l _  := ⟨false, trivial⟩

private lemma nil_prefix {α : Type u} (l : SnocList α) : εₛ ≤ l := by
α : Type u
l : SnocList α
⊢ εₛ ≤ l
  induction l with
  | nil        =>
nil
α : Type u
⊢ εₛ ≤ εₛ exact le_refl _
  | snoc _ _ ih =>
snoc
α : Type u
a✝¹ : SnocList α
a✝ : α
ih : εₛ ≤ a✝¹
⊢ εₛ ≤ (a✝¹ :> a✝) exact Or.inr ih

private lemma not_prefix_false_of_const_true (l : SnocList Bool) (n : ℕ)
    (h : ¬ (SnocList.nil :> false : SnocList Bool) ≤ l) :
    ¬ (SnocList.nil :> false : SnocList Bool) ≤ l ++ initial (fun _ => true) n := by
l : SnocList Bool
n : ℕ
h : ¬(εₛ :> false) ≤ l
⊢ ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
  induction n with
  | zero  =>
zero
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
⊢ ¬(εₛ :> false) ≤ l ++ initial (fun x => true) 0 simpa [initial]
  | succ n ih =>
succ
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
⊢ ¬(εₛ :> false) ≤ l ++ initial (fun x => true) (n + 1)
    simp [initial]
succ
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
⊢ ¬(εₛ :> false) ≤ (l ++ initial (fun x => true) n :> true)
    intro hc
succ
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
hc : (εₛ :> false) ≤ (l ++ initial (fun x => true) n :> true)
⊢ False
    rcases hc with hc | hc
succ.inl
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
hc : (εₛ :> false) = (l ++ initial (fun x => true) n :> true)
⊢ False
succ.inr
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
hc : (εₛ :> false).is_prefix (l ++ initial (fun x => true) n)
⊢ False
    ·
succ.inl
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
hc : (εₛ :> false) = (l ++ initial (fun x => true) n :> true)
⊢ False rw [SnocList.snoc.injEq] at hc
succ.inl
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
hc : εₛ = l ++ initial (fun x => true) n ∧ false = true
⊢ False
      apply absurd hc.2
succ.inl
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
hc : εₛ = l ++ initial (fun x => true) n ∧ false = true
⊢ ¬false = true
      decide
    ·
succ.inr
l : SnocList Bool
h : ¬(εₛ :> false) ≤ l
n : ℕ
ih : ¬(εₛ :> false) ≤ l ++ initial (fun x => true) n
hc : (εₛ :> false).is_prefix (l ++ initial (fun x => true) n)
⊢ False exact ih hc

private lemma not_prefix_true_of_const_false (l : SnocList Bool) (n : ℕ)
    (h : ¬ (SnocList.nil :> true : SnocList Bool) ≤ l) :
    ¬ (SnocList.nil :> true : SnocList Bool) ≤ l ++ initial (fun _ => false) n := by
l : SnocList Bool
n : ℕ
h : ¬(εₛ :> true) ≤ l
⊢ ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
  induction n with
  | zero  =>
zero
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
⊢ ¬(εₛ :> true) ≤ l ++ initial (fun x => false) 0 simpa [initial]
  | succ n ih =>
succ
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
⊢ ¬(εₛ :> true) ≤ l ++ initial (fun x => false) (n + 1)
    simp only [initial]
succ
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
⊢ ¬(εₛ :> true) ≤ l ++ (initial (fun x => false) n :> false)
    intro hc
succ
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
hc : (εₛ :> true) ≤ l ++ (initial (fun x => false) n :> false)
⊢ False
    rcases hc with hc | hc
succ.inl
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
hc : (εₛ :> true) = (l.append (initial (fun x => false) n) :> false)
⊢ False
succ.inr
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
hc : (εₛ :> true).is_prefix (l.append (initial (fun x => false) n))
⊢ False
    ·
succ.inl
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
hc : (εₛ :> true) = (l.append (initial (fun x => false) n) :> false)
⊢ False rw [SnocList.snoc.injEq] at hc
succ.inl
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
hc : εₛ = l.append (initial (fun x => false) n) ∧ true = false
⊢ False
      exact absurd hc.2 (by
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
hc : εₛ = l.append (initial (fun x => false) n) ∧ true = false
⊢ ¬true = false decide)
    ·
succ.inr
l : SnocList Bool
h : ¬(εₛ :> true) ≤ l
n : ℕ
ih : ¬(εₛ :> true) ≤ l ++ initial (fun x => false) n
hc : (εₛ :> true).is_prefix (l.append (initial (fun x => false) n))
⊢ False exact ih hc

def binaryBranchVal : BethVal fullBinaryTree where
  val l i := match i with
    | 0 => (SnocList.nil :> false) ≤ l
    | 1 => (SnocList.nil :> true) ≤ l
    | _ => False
  mono_val := by
⊢ ∀ {l m : SnocList Bool} {i : ℕ},
  l ≤ m →
    fullBinaryTree.tree_node m →
      (match i with
        | 0 => (εₛ :> false) ≤ l
        | 1 => (εₛ :> true) ≤ l
        | x => False) →
        match i with
        | 0 => (εₛ :> false) ≤ m
        | 1 => (εₛ :> true) ≤ m
        | x => False
    intro l m
l : SnocList Bool
m : SnocList Bool
⊢ ∀ {i : ℕ},
  l ≤ m →
    fullBinaryTree.tree_node m →
      (match i with
        | 0 => (εₛ :> false) ≤ l
        | 1 => (εₛ :> true) ≤ l
        | x => False) →
        match i with
        | 0 => (εₛ :> false) ≤ m
        | 1 => (εₛ :> true) ≤ m
        | x => False i
l : SnocList Bool
m : SnocList Bool
i : ℕ
⊢ l ≤ m →
  fullBinaryTree.tree_node m →
    (match i with
      | 0 => (εₛ :> false) ≤ l
      | 1 => (εₛ :> true) ≤ l
      | x => False) →
      match i with
      | 0 => (εₛ :> false) ≤ m
      | 1 => (εₛ :> true) ≤ m
      | x => False hle
l : SnocList Bool
m : SnocList Bool
i : ℕ
hle : l ≤ m
⊢ fullBinaryTree.tree_node m →
  (match i with
    | 0 => (εₛ :> false) ≤ l
    | 1 => (εₛ :> true) ≤ l
    | x => False) →
    match i with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False _
l : SnocList Bool
m : SnocList Bool
i : ℕ
hle : l ≤ m
a✝ : fullBinaryTree.tree_node m
⊢ (match i with
  | 0 => (εₛ :> false) ≤ l
  | 1 => (εₛ :> true) ≤ l
  | x => False) →
  match i with
  | 0 => (εₛ :> false) ≤ m
  | 1 => (εₛ :> true) ≤ m
  | x => False hval
l : SnocList Bool
m : SnocList Bool
i : ℕ
hle : l ≤ m
a✝ : fullBinaryTree.tree_node m
hval : match i with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
⊢ match i with
| 0 => (εₛ :> false) ≤ m
| 1 => (εₛ :> true) ≤ m
| x => False
    match i with
    | 0 =>
l : SnocList Bool
m : SnocList Bool
i : ℕ
hle : l ≤ m
a✝ : fullBinaryTree.tree_node m
hval : match 0 with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
⊢ match 0 with
| 0 => (εₛ :> false) ≤ m
| 1 => (εₛ :> true) ≤ m
| x => False exact SnocList.is_prefix_trans hval hle
    | 1 =>
l : SnocList Bool
m : SnocList Bool
i : ℕ
hle : l ≤ m
a✝ : fullBinaryTree.tree_node m
hval : match 1 with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
⊢ match 1 with
| 0 => (εₛ :> false) ≤ m
| 1 => (εₛ :> true) ≤ m
| x => False exact SnocList.is_prefix_trans hval hle
    | _ + 2 =>
l : SnocList Bool
m : SnocList Bool
i : ℕ
hle : l ≤ m
a✝ : fullBinaryTree.tree_node m
n✝ : ℕ
hval : match n✝ + 2 with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
⊢ match n✝ + 2 with
| 0 => (εₛ :> false) ≤ m
| 1 => (εₛ :> true) ≤ m
| x => False exact hval.elim
  sheaf_val := by
⊢ ∀ {l : SnocList Bool} {i : ℕ},
  fullBinaryTree.tree_node l →
    IsBar fullBinaryTree l
        {m |
          match i with
          | 0 => (εₛ :> false) ≤ m
          | 1 => (εₛ :> true) ≤ m
          | x => False} →
      match i with
      | 0 => (εₛ :> false) ≤ l
      | 1 => (εₛ :> true) ≤ l
      | x => False
    intro l i
l : SnocList Bool
i : ℕ
⊢ fullBinaryTree.tree_node l →
  IsBar fullBinaryTree l
      {m |
        match i with
        | 0 => (εₛ :> false) ≤ m
        | 1 => (εₛ :> true) ≤ m
        | x => False} →
    match i with
    | 0 => (εₛ :> false) ≤ l
    | 1 => (εₛ :> true) ≤ l
    | x => False _
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
⊢ IsBar fullBinaryTree l
    {m |
      match i with
      | 0 => (εₛ :> false) ≤ m
      | 1 => (εₛ :> true) ≤ m
      | x => False} →
  match i with
  | 0 => (εₛ :> false) ≤ l
  | 1 => (εₛ :> true) ≤ l
  | x => False hbar
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l
  {m |
    match i with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False}
⊢ match i with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
    match i with
    | 0 =>
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l
  {m |
    match 0 with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False}
⊢ match 0 with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
      by_contra h
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l
  {m |
    match 0 with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False}
h : ¬match 0 with
  | 0 => (εₛ :> false) ≤ l
  | 1 => (εₛ :> true) ≤ l
  | x => False
⊢ False
      simp at h
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l
  {m |
    match 0 with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False}
h : ¬(εₛ :> false) ≤ l
⊢ False
      simp at hbar
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l {m | (εₛ :> false) ≤ m}
h : ¬(εₛ :> false) ≤ l
⊢ False
      -- If ¬ εₛ :> ff ≤ l, then the l ++ initial (fun _ => tt) is not barred
      obtain ⟨n, hn⟩ := hbar (fun _ => true) trivial (fun _ => trivial)
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l {m | (εₛ :> false) ≤ m}
h : ¬(εₛ :> false) ≤ l
n : ℕ
hn : {m | (εₛ :> false) ≤ m} (l ++ initial (fun x => true) n)
⊢ False
      apply not_prefix_false_of_const_true l n h hn

    | 1 =>
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l
  {m |
    match 1 with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False}
⊢ match 1 with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
      by_contra h
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l
  {m |
    match 1 with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False}
h : ¬match 1 with
  | 0 => (εₛ :> false) ≤ l
  | 1 => (εₛ :> true) ≤ l
  | x => False
⊢ False
      simp at h
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l
  {m |
    match 1 with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False}
h : ¬(εₛ :> true) ≤ l
⊢ False
      simp at hbar
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l {m | (εₛ :> true) ≤ m}
h : ¬(εₛ :> true) ≤ l
⊢ False
      -- If ¬ εₛ :> tt ≤ l, then the l ++ initial (fun _ => ff) is not barred
      obtain ⟨n, hn⟩ := hbar (fun _ => false) trivial (fun _ => trivial)
l : SnocList Bool
i : ℕ
a✝ : fullBinaryTree.tree_node l
hbar : IsBar fullBinaryTree l {m | (εₛ :> true) ≤ m}
h : ¬(εₛ :> true) ≤ l
n : ℕ
hn : {m | (εₛ :> true) ≤ m} (l ++ initial (fun x => false) n)
⊢ False
      exact not_prefix_true_of_const_false l n h hn
    | i + 2 =>
l : SnocList Bool
i✝ : ℕ
a✝ : fullBinaryTree.tree_node l
i : ℕ
hbar : IsBar fullBinaryTree l
  {m |
    match i + 2 with
    | 0 => (εₛ :> false) ≤ m
    | 1 => (εₛ :> true) ≤ m
    | x => False}
⊢ match i + 2 with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
      simp at hbar
l : SnocList Bool
i✝ : ℕ
a✝ : fullBinaryTree.tree_node l
i : ℕ
hbar : IsBar fullBinaryTree l ∅
⊢ match i + 2 with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
      obtain ⟨_, hm, _⟩ := IsBar.nonempty fullBinaryTree hbar trivial
l : SnocList Bool
i✝ : ℕ
a✝ : fullBinaryTree.tree_node l
i : ℕ
hbar : IsBar fullBinaryTree l ∅
w✝ : SnocList Bool
hm : ∅ w✝
right✝ : l ≤ w✝
⊢ match i + 2 with
| 0 => (εₛ :> false) ≤ l
| 1 => (εₛ :> true) ≤ l
| x => False
      exact hm.elim

instance fullBinaryBethFrame : BethFrame {l : SnocList Bool // fullBinaryTree.tree_node l} :=
  BethTreeFrame fullBinaryTree binaryBranchVal

abbrev root :  {l : SnocList Bool // fullBinaryTree.tree_node l} := ⟨.nil, trivial⟩

example : at_world root (Tm.or (Tm.var 0) (Tm.var 1)) := by
⊢ at_world root (Tm.var 0 ∨ Tm.var 1)
  simp only [at_world]
⊢ ∃ S, covers root S ∧ ∀ w' ∈ S, BethFrame.val w' 0 ∨ BethFrame.val w' 1

  let S : Sieve root := {
    carrier      := {w | (εₛ :> false : SnocList Bool) ≤ w.1 ∨
                         (εₛ :> true  : SnocList Bool) ≤ w.1},
    bounded      := fun _ => nil_prefix _,
    upward_closed := by
⊢ ∀ {q r : { l // fullBinaryTree.tree_node l }},
  r ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w} → r ≤ q → q ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}
      intro q r
q : { l // fullBinaryTree.tree_node l }
r : { l // fullBinaryTree.tree_node l }
⊢ r ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w} → r ≤ q → q ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w} hmem
q : { l // fullBinaryTree.tree_node l }
r : { l // fullBinaryTree.tree_node l }
hmem : r ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}
⊢ r ≤ q → q ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w} r_le_q
q : { l // fullBinaryTree.tree_node l }
r : { l // fullBinaryTree.tree_node l }
hmem : r ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}
r_le_q : r ≤ q
⊢ q ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}
      simp at hmem
q : { l // fullBinaryTree.tree_node l }
r : { l // fullBinaryTree.tree_node l }
hmem : (εₛ :> false) ≤ ↑r ∨ (εₛ :> true) ≤ ↑r
r_le_q : r ≤ q
⊢ q ∈ {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}
      apply hmem.imp
f
q : { l // fullBinaryTree.tree_node l }
r : { l // fullBinaryTree.tree_node l }
hmem : (εₛ :> false) ≤ ↑r ∨ (εₛ :> true) ≤ ↑r
r_le_q : r ≤ q
⊢ (εₛ :> false) ≤ ↑r → (εₛ :> false) ≤ ↑q
g
q : { l // fullBinaryTree.tree_node l }
r : { l // fullBinaryTree.tree_node l }
hmem : (εₛ :> false) ≤ ↑r ∨ (εₛ :> true) ≤ ↑r
r_le_q : r ≤ q
⊢ (εₛ :> true) ≤ ↑r → (εₛ :> true) ≤ ↑q
      ·
f
q : { l // fullBinaryTree.tree_node l }
r : { l // fullBinaryTree.tree_node l }
hmem : (εₛ :> false) ≤ ↑r ∨ (εₛ :> true) ≤ ↑r
r_le_q : r ≤ q
⊢ (εₛ :> false) ≤ ↑r → (εₛ :> false) ≤ ↑q exact (fun h => SnocList.is_prefix_trans h r_le_q)
      ·
g
q : { l // fullBinaryTree.tree_node l }
r : { l // fullBinaryTree.tree_node l }
hmem : (εₛ :> false) ≤ ↑r ∨ (εₛ :> true) ≤ ↑r
r_le_q : r ≤ q
⊢ (εₛ :> true) ≤ ↑r → (εₛ :> true) ≤ ↑q exact (fun h => SnocList.is_prefix_trans h r_le_q)
    }
  refine ⟨S, ?_, ?_⟩
refine_1
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
⊢ covers root S
refine_2
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
⊢ ∀ w' ∈ S, BethFrame.val w' 0 ∨ BethFrame.val w' 1
  ·
refine_1
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
⊢ covers root S -- The sieve is a bar at nil: at depth 1, f 0 is false or true.
    intro f _
refine_1
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
f : ℕ → Bool
a✝ : fullBinaryTree.tree_node ↑root
⊢ (∀ (n : ℕ), fullBinaryTree.tree_node (↑root ++ initial f n)) → ∃ n, nodeBar S (↑root ++ initial f n) _
refine_1
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
f : ℕ → Bool
a✝¹ : fullBinaryTree.tree_node ↑root
a✝ : ∀ (n : ℕ), fullBinaryTree.tree_node (↑root ++ initial f n)
⊢ ∃ n, nodeBar S (↑root ++ initial f n)
    refine ⟨1, trivial, ?_⟩
refine_1
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
f : ℕ → Bool
a✝¹ : fullBinaryTree.tree_node ↑root
a✝ : ∀ (n : ℕ), fullBinaryTree.tree_node (↑root ++ initial f n)
⊢ ⟨↑root ++ initial f 1, trivial⟩ ∈ S.carrier
    -- Reduce nil ++ initial f 1 = nil :> f 0 and unfold set membership
    simp only [initial, SnocList.append_snoc, SnocList.append_nil]
refine_1
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
f : ℕ → Bool
a✝¹ : fullBinaryTree.tree_node ↑root
a✝ : ∀ (n : ℕ), fullBinaryTree.tree_node (↑root ++ initial f n)
⊢ ⟨εₛ :> f 0, ⋯⟩ ∈ S.carrier
    -- Goal: nil :> false ≤ nil :> f 0 ∨ nil :> true ≤ nil :> f 0
    simp [S]
refine_1
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
f : ℕ → Bool
a✝¹ : fullBinaryTree.tree_node ↑root
a✝ : ∀ (n : ℕ), fullBinaryTree.tree_node (↑root ++ initial f n)
⊢ (εₛ :> false) ≤ (εₛ :> f 0) ∨ (εₛ :> true) ≤ (εₛ :> f 0)
    exact Bool.casesOn (f 0) (Or.inl (Or.inl rfl)) (Or.inr (Or.inl rfl))
  ·
refine_2
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
⊢ ∀ w' ∈ S, BethFrame.val w' 0 ∨ BethFrame.val w' 1 -- Every element of the sieve forces var 0 or var 1.
    intro ⟨m, _⟩ hm
refine_2
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
m : SnocList Bool
property✝ : fullBinaryTree.tree_node m
hm : ⟨m, property✝⟩ ∈ S
⊢ BethFrame.val ⟨m, property✝⟩ 0 ∨ BethFrame.val ⟨m, property✝⟩ 1
    rcases hm with h | h
refine_2.inl
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
m : SnocList Bool
property✝ : fullBinaryTree.tree_node m
h : (εₛ :> false) ≤ ↑⟨m, property✝⟩
⊢ BethFrame.val ⟨m, property✝⟩ 0 ∨ BethFrame.val ⟨m, property✝⟩ 1
refine_2.inr
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
m : SnocList Bool
property✝ : fullBinaryTree.tree_node m
h : (εₛ :> true) ≤ ↑⟨m, property✝⟩
⊢ BethFrame.val ⟨m, property✝⟩ 0 ∨ BethFrame.val ⟨m, property✝⟩ 1
    ·
refine_2.inl
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
m : SnocList Bool
property✝ : fullBinaryTree.tree_node m
h : (εₛ :> false) ≤ ↑⟨m, property✝⟩
⊢ BethFrame.val ⟨m, property✝⟩ 0 ∨ BethFrame.val ⟨m, property✝⟩ 1 exact Or.inl h
    ·
refine_2.inr
S : Sieve root := { carrier := {w | (εₛ :> false) ≤ ↑w ∨ (εₛ :> true) ≤ ↑w}, bounded := ⋯, upward_closed := ⋯ }
m : SnocList Bool
property✝ : fullBinaryTree.tree_node m
h : (εₛ :> true) ≤ ↑⟨m, property✝⟩
⊢ BethFrame.val ⟨m, property✝⟩ 0 ∨ BethFrame.val ⟨m, property✝⟩ 1 exact Or.inr h