This file defines theorems related to the inputs of TPE.

theorem Cedar.Thm.decide_eq_implies_eq {α : Sort u_1} [DecidableEq α] {y : α} (x : α) : decide (x = y) = true → x = y

inductive Cedar.Thm.PartialIsValid {α : Type u_1} : (α → Prop) → Option α → Prop

• some {α : Type u_1} (p : α → Prop) (x : α) (h : p x) : PartialIsValid p (Option.some x)
• none {α : Type u_1} {p : α → Prop} : PartialIsValid p Option.none

theorem Cedar.Thm.partial_is_valid_rfl {α : Type u_1} (f : α → Bool) (p : α → Prop) (o : Option α) : (∀ (x : α), f x = true → p x) → TPE.partialIsValid o f = true → PartialIsValid p o

def Cedar.Thm.RequestRefines (req : Spec.Request) (preq : TPE.PartialRequest) : Prop

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.EntitiesRefine (es : Spec.Entities) (pes : TPE.PartialEntities) : Prop

Equations

• One or more equations did not get rendered due to their size.

def Cedar.Thm.RequestAndEntitiesRefine (req : Spec.Request) (es : Spec.Entities) (preq : TPE.PartialRequest) (pes : TPE.PartialEntities) : Prop

Concrete request req and entities es refine their partial counterparts peq and pes.

Equations

• Cedar.Thm.RequestAndEntitiesRefine req es preq pes = (Cedar.Thm.RequestRefines req preq ∧ Cedar.Thm.EntitiesRefine es pes)

theorem Cedar.Thm.consistent_checks_ensure_refinement {schema : Validation.Schema} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} : TPE.isValidAndConsistent schema req es preq pes = Except.ok () → RequestAndEntitiesRefine req es preq pes

Requests and entities that pass isValidAndConsistent satisfy RequestAndEntitiesRefine.