import Pretty.Defs.Basic
import Pretty.Supports.MergeBasic

/-!
### Various measure set operations (Figure 12)
-/

/--
- lift;
-/
def MeasureSet.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
MeasureSet.lift (f: Meas → Meas
f : @Meas: {α : Type} → Type
Meas α: ?m.4
α → @Meas: {α : Type} → Type
Meas α: ?m.4
α) : @MeasureSet: {α : Type} → Type
MeasureSet α: ?m.4
α → @MeasureSet: {α : Type} → Type
MeasureSet α: ?m.4
α
  | MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m: Meas
m => MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted (f: Meas → Meas
f m: Meas
m)
  | MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms: List Meas
ms h: ms ≠ []
h => MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set (ms: List Meas
ms.map: {α : Type ?u.58} → {β : Type ?u.57} → (α → β) → List α → List β
map f: Meas → Meas
f) (by
Goals accomplished! 🐙 α: Type

f: Meas → Meas

ms: List Meas

h: ms ≠ []

List.map f ms ≠ []simp [h: ms ≠ []
h]
Goals accomplished! 🐙)

/--
- taint; and
-/
def MeasureSet.taint: {α : Type} → MeasureSet → MeasureSet
MeasureSet.taint : @MeasureSet: {α : Type} → Type
MeasureSet α: ?m.558
α → @MeasureSet: {α : Type} → Type
MeasureSet α: ?m.558
α
  | MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m: Meas
m => MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m: Meas
m
  | MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms: List Meas
ms h: ms ≠ []
h => MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted (ms: List Meas
ms.head: {α : Type ?u.606} → (as : List α) → as ≠ [] → α
head h: ms ≠ []
h)

/--
- union (⊎)
-/
def MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union (F: Factory α
F : Factory: Type → Type
Factory α: ?m.795
α) : @MeasureSet: {α : Type} → Type
MeasureSet α: ?m.795
α → @MeasureSet: {α : Type} → Type
MeasureSet α: ?m.795
α → @MeasureSet: {α : Type} → Type
MeasureSet α: ?m.795
α
  | s: MeasureSet
s, MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted _ => s: MeasureSet
s
  | MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted _, MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms: List Meas
ms h: ms ≠ []
h => MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms: List Meas
ms h: ms ≠ []
h
  | MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms₁: List Meas
ms₁ h₁: ms₁ ≠ []
h₁, MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set ms₂: List Meas
ms₂ _ => 
    MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set (merge: {α : Type} → Factory α → List Meas × List Meas → List Meas
merge F: Factory α
F ⟨ms₁: List Meas
ms₁, ms₂: List Meas
ms₂⟩) (by
Goals accomplished! 🐙 α: Type

F: Factory α

ms₁: List Meas

h₁: ms₁ ≠ []

ms₂: List Meas

h✝: ms₂ ≠ []

merge F (ms₁, ms₂) ≠ []{α: Type

F: Factory α

ms₁: List Meas

h₁: ms₁ ≠ []

ms₂: List Meas

h✝: ms₂ ≠ []

merge F (ms₁, ms₂) ≠ []
      α: Type

F: Factory α

ms₁: List Meas

h₁: ms₁ ≠ []

ms₂: List Meas

h✝: ms₂ ≠ []

merge F (ms₁, ms₂) ≠ []apply merge_not_empty: ∀ {α : Type} {ms₁ ms₂ : List Meas} {F : Factory α}, ms₁ ≠ [] ∨ ms₂ ≠ [] → merge F (ms₁, ms₂) ≠ []
merge_not_emptyα: Type

F: Factory α

ms₁: List Meas

h₁: ms₁ ≠ []

ms₂: List Meas

h✝: ms₂ ≠ []

hms₁ ≠ [] ∨ ms₂ ≠ [] 
      α: Type

F: Factory α

ms₁: List Meas

h₁: ms₁ ≠ []

ms₂: List Meas

h✝: ms₂ ≠ []

merge F (ms₁, ms₂) ≠ []simp [h₁: ms₁ ≠ []
h₁]
Goals accomplished! 🐙
    }
Goals accomplished! 🐙)