Case valuations

A derivation that values the case of nominals step by step keeps, for each nominal, the value its case has received so far, none while it is unvalued: a valuation of the nominals. Every step of the formalized case theories, the dependent-case rules of [Mar91], Agree ([Cho00]) and the licensing of [Kal18], keeps the nominals and the values already assigned and assigns new values only from what its rules provide: it extends the valuation by those values (Extends). What such steps have in common, that a derivation is total, that a value once assigned persists, and that every new value comes from the rules, is proved once here for Extends and inherited by each theory through a single lemma per step.

The steps are not monotone: a more valued input can yield an output that does not extend the output of a less valued one, as when lexical case on a lower nominal bleeds the dependent case of a higher one. They are only inflationary, so no order-theoretic closure applies. A second relation, ValuedLE, compares two derivations by which nominals they value at all, for accounts in which adding an assigner may change what values a nominal but never leaves one unvalued.

Main definitions

• Case.Valuation: nominals, from the highest down, each with the value of its case.
• Case.Valuation.initial, Case.Valuation.fill, Case.Valuation.unvalued: the valuation with given values, the simultaneous valuation of the unvalued nominals, and the positions of the unvalued ones.
• Case.Valuation.valueOf: the value of a nominal, the nominals being identified by their own type rather than by a label.
• Case.Valuation.Extends: one valuation extends another by values satisfying a predicate.
• Case.Valuation.ValuedLE: one valuation values every nominal another does.

Main results

• Case.Valuation.Extends.getElem?_of_some, Case.Valuation.Extends.of_getElem?: values persist, and every new value satisfies the predicate.
• Case.Valuation.Extends.foldl: a sequence of extending steps extends.
• Case.Valuation.extends_fill: filling the unvalued nominals extends the valuation.

Implementation notes

The operations are structurally recursive on the list, rather than defined through List.mapIdx or List.lookmap, whose accumulators decide cannot evaluate.

References

• [Mar91]
• [Cho00]
• [Kal18]

@[reducible, inline]

abbrev Case.Valuation (α : Type u_1) (β : Type u_2) : Type (max u_2 u_1)

Nominals, from the highest down, each with the value of its case, none while unvalued.

Equations

• Case.Valuation α β = List (α × Option β)

Operations

def Case.Valuation.initial {α : Type u_1} {β : Type u_2} (v : α → Option β) (xs : List α) : Valuation α β

The valuation giving each nominal the value v gives it.

Equations

• Case.Valuation.initial v xs = List.map (fun (x : α) => (x, v x)) xs

def Case.Valuation.fillFrom {α : Type u_1} {β : Type u_2} (f : ℕ → α → Option β) : ℕ → Valuation α β → Valuation α β

fill, with positions counted from i.

Equations

• Case.Valuation.fillFrom f x✝ [] = []
• Case.Valuation.fillFrom f x✝ ((x_2, none) :: s) = (x_2, f x✝ x_2) :: Case.Valuation.fillFrom f (x✝ + 1) s
• Case.Valuation.fillFrom f x✝ ((x_2, some v) :: s) = (x_2, some v) :: Case.Valuation.fillFrom f (x✝ + 1) s

def Case.Valuation.fill {α : Type u_1} {β : Type u_2} (f : ℕ → α → Option β) (s : Valuation α β) : Valuation α β

Value every unvalued nominal with what f proposes for its position, simultaneously.

Equations

• Case.Valuation.fill f s = Case.Valuation.fillFrom f 0 s

def Case.Valuation.valueOf {α : Type u_1} {β : Type u_2} [DecidableEq α] (a : α) (s : Valuation α β) : Option β

The value of nominal a, if it has one.

Equations

• Case.Valuation.valueOf a s = (List.lookup a s).join

def Case.Valuation.unvalued {α : Type u_1} {β : Type u_2} (P : α → Bool) (s : Valuation α β) : List ℕ

The positions of the unvalued nominals P selects, highest first.

Equations

• Case.Valuation.unvalued P s = List.map (fun (x : (α × Option β) × ℕ) => x.snd) (List.filter (fun (p : (α × Option β) × ℕ) => p.fst.snd.isNone && P p.fst.fst) (List.zipIdx s))

@[simp]

theorem Case.Valuation.length_initial {α : Type u_1} {β : Type u_2} (v : α → Option β) (xs : List α) : List.length (initial v xs) = xs.length

theorem Case.Valuation.initial_getElem? {α : Type u_1} {β : Type u_2} (v : α → Option β) (xs : List α) (i : ℕ) : (initial v xs)[i]? = Option.map (fun (x : α) => (x, v x)) xs[i]?

theorem Case.Valuation.fillFrom_getElem? {α : Type u_1} {β : Type u_2} (f : ℕ → α → Option β) (i j : ℕ) (s : Valuation α β) : (fillFrom f i s)[j]? = Option.map (fun (p : α × Option β) => if p.snd.isNone = true then (p.fst, f (i + j) p.fst) else p) s[j]?

theorem Case.Valuation.fill_getElem? {α : Type u_1} {β : Type u_2} (f : ℕ → α → Option β) (s : Valuation α β) (i : ℕ) : (fill f s)[i]? = Option.map (fun (p : α × Option β) => if p.snd.isNone = true then (p.fst, f i p.fst) else p) s[i]?

theorem Case.Valuation.fill_getElem?_of_none {α : Type u_1} {β : Type u_2} {f : ℕ → α → Option β} {s : Valuation α β} {i : ℕ} {x : α} (h : s[i]? = some (x, none)) : (fill f s)[i]? = some (x, f i x)

@[simp]

theorem Case.Valuation.fill_none {α : Type u_1} {β : Type u_2} (s : Valuation α β) : fill (fun (x : ℕ) (x_1 : α) => none) s = s

Filling with no proposals changes nothing.

theorem Case.Valuation.mem_unvalued_iff {α : Type u_1} {β : Type u_2} {P : α → Bool} {s : Valuation α β} {i : ℕ} : i ∈ unvalued P s ↔ ∃ (x : α), s[i]? = some (x, none) ∧ P x = true

Extension

@[reducible, inline]

abbrev Case.Valuation.Extends {α : Type u_1} {β : Type u_2} (p : β → Prop) (s t : Valuation α β) : Prop

t extends s by values satisfying p: it has the same nominals, keeps every value s assigns, and values a nominal s leaves unvalued only with a value satisfying p.

Equations

• Case.Valuation.Extends p s t = List.Forall₂ (fun (a b : α × Option β) => a.fst = b.fst ∧ (a.snd = b.snd ∨ a.snd = none ∧ ∀ (v : β), v ∈ b.snd → p v)) s t

theorem Case.Valuation.Extends.refl {α : Type u_1} {β : Type u_2} {p : β → Prop} (s : Valuation α β) : Extends p s s

theorem Case.Valuation.Extends.mono {α : Type u_1} {β : Type u_2} {p q : β → Prop} {s t : Valuation α β} (hpq : ∀ (v : β), p v → q v) (h : Extends p s t) : Extends q s t

theorem Case.Valuation.Extends.trans {α : Type u_1} {β : Type u_2} {p : β → Prop} {s t u : Valuation α β} (h₁ : Extends p s t) (h₂ : Extends p t u) : Extends p s u

theorem Case.Valuation.Extends.length_eq {α : Type u_1} {β : Type u_2} {p : β → Prop} {s t : Valuation α β} (h : Extends p s t) : List.length s = List.length t

theorem Case.Valuation.Extends.getElem?_of_some {α : Type u_1} {β : Type u_2} {p : β → Prop} {s t : Valuation α β} (h : Extends p s t) {i : ℕ} {x : α} {v : β} (hs : s[i]? = some (x, some v)) : t[i]? = some (x, some v)

A value, once assigned, persists.

theorem Case.Valuation.Extends.of_getElem? {α : Type u_1} {β : Type u_2} {p : β → Prop} {s t : Valuation α β} (h : Extends p s t) {i : ℕ} {x : α} {v : β} (ht : t[i]? = some (x, some v)) : s[i]? = some (x, some v) ∨ p v

A value of the extending valuation was already assigned or satisfies p.

theorem Case.Valuation.Extends.of_mem {α : Type u_1} {β : Type u_2} {p : β → Prop} {s t : Valuation α β} (h : Extends p s t) {x : α} {v : β} (ht : (x, some v) ∈ t) : (x, some v) ∈ s ∨ p v

theorem Case.Valuation.Extends.map {α : Type u_1} {β : Type u_2} {p : β → Prop} {s t : Valuation α β} {γ : Type u_3} (f : α → γ) (h : Extends p s t) : Extends p (List.map (Prod.map f id) s) (List.map (Prod.map f id) t)

theorem Case.Valuation.Extends.foldl {α : Type u_1} {β : Type u_2} {p : β → Prop} {γ : Type u_3} {F : γ → Valuation α β → Valuation α β} (l : List γ) : (∀ (c : γ), c ∈ l → ∀ (s : Valuation α β), Extends p s (F c s)) → ∀ (s : Valuation α β), Extends p s (List.foldl (fun (s : Valuation α β) (c : γ) => F c s) s l)

A sequence of steps each extending by p extends by p.

theorem Case.Valuation.extends_fillFrom {α : Type u_1} {β : Type u_2} {p : β → Prop} {f : ℕ → α → Option β} (hf : ∀ (i : ℕ) (x : α) (v : β), f i x = some v → p v) (i : ℕ) (s : Valuation α β) : Extends p s (fillFrom f i s)

theorem Case.Valuation.extends_fill {α : Type u_1} {β : Type u_2} {p : β → Prop} {f : ℕ → α → Option β} (hf : ∀ (i : ℕ) (x : α) (v : β), f i x = some v → p v) (s : Valuation α β) : Extends p s (fill f s)

Filling the unvalued nominals extends the valuation by the values proposed.

Comparing derivations

@[reducible, inline]

abbrev Case.Valuation.ValuedLE {α : Type u_1} {β : Type u_2} (s t : Valuation α β) : Prop

t has the nominals of s and values every nominal s values.

Equations

• s.ValuedLE t = List.Forall₂ (fun (a b : α × Option β) => a.fst = b.fst ∧ (a.snd.isSome = true → b.snd.isSome = true)) s t

theorem Case.Valuation.ValuedLE.refl {α : Type u_1} {β : Type u_2} (s : Valuation α β) : s.ValuedLE s

theorem Case.Valuation.ValuedLE.trans {α : Type u_1} {β : Type u_2} {s t u : Valuation α β} : s.ValuedLE t → t.ValuedLE u → s.ValuedLE u

theorem Case.Valuation.Extends.valuedLE {α : Type u_1} {β : Type u_2} {p : β → Prop} {s t : Valuation α β} (h : Extends p s t) : s.ValuedLE t

A valuation values every nominal the valuation it extends values.