Theory /Cortex /Wire /AdmissionArtifact /Check

Cortex.Wire.AdmissionArtifact.Check

proofs

On this page

Overview
Decidable Propositions
List Quantifiers
Standard Row Properties
Gated Pair Checks

Imports

import Mathlib.Data.List.Perm.Basic

Overview

Reusable boolean checker combinators for decoded Wire admission artifacts.

Each helper is intentionally small: a checker returns Bool, and its paired soundness theorem converts check = true into the proof-facing predicate. These are Lean-side soundness combinators, not standalone proofs that the Haskell validator uses the same algorithm. Artifact-specific modules keep the semantic predicates and any Haskell-correspondence obligations.

              namespace Cortex.Wirenamespace AdmissionArtifactnamespace Check

Decidable Propositions

Boolean form of a decidable proposition.

def propCheck (predicate : Prop) [Decidable predicate] : Bool :=
  decide predicate

Successful proposition checking returns the proposition.

theorem propCheck_sound
    {predicate : Prop}
    [Decidable predicate]
    (hCheck : propCheck predicate = true) :
    predicate :=
  of_decide_eq_true hCheck

List Quantifiers

Boolean universal quantification over a decoded finite row list.

def allDecide {α : Type}
    (items : List α)
    (predicate : α → Prop)
    [DecidablePred predicate] :
    Bool :=
  items.all fun item => decide (predicate item)

A successful finite boolean universal check supplies the corresponding predicate.

theorem allDecide_sound
    {α : Type}
    {items : List α}
    {predicate : α → Prop}
    [DecidablePred predicate]
    (hCheck : allDecide items predicate = true) :
    ∀ item, item ∈ items → predicate item := byα:Typeitems:List αpredicate:α → Propinst✝:DecidablePred predicatehCheck:allDecide items predicate = true⊢ ∀ (item : α), item ∈ items → predicate item
  intro item hItemα:Typeitems:List αpredicate:α → Propinst✝:DecidablePred predicatehCheck:allDecide items predicate = trueitem:αhItem:item ∈ items⊢ predicate item
  have hItemCheck :
      decide (predicate item) = true :=
    (List.all_eq_true.mp hCheck) item hItemα:Typeitems:List αpredicate:α → Propinst✝:DecidablePred predicatehCheck:allDecide items predicate = trueitem:αhItem:item ∈ itemshItemCheck:decide (predicate item) = true⊢ predicate item
  exact of_decide_eq_true hItemCheckAll goals completed! 🐙

Boolean universal quantification for row checkers that already return Bool.

def allBool {α : Type} (items : List α) (check : α → Bool) : Bool :=
  items.all check

A successful finite boolean universal check transports through local soundness.

theorem allBool_sound
    {α : Type}
    {items : List α}
    {check : α → Bool}
    {predicate : α → Prop}
    (hCheck : allBool items check = true)
    (hSound :
      ∀ item, item ∈ items → check item = true → predicate item) :
    ∀ item, item ∈ items → predicate item := byα:Typeitems:List αcheck:α → Boolpredicate:α → ProphCheck:allBool items check = truehSound:∀ (item : α), item ∈ items → check item = true → predicate item⊢ ∀ (item : α), item ∈ items → predicate item
  intro item hItemα:Typeitems:List αcheck:α → Boolpredicate:α → ProphCheck:allBool items check = truehSound:∀ (item : α), item ∈ items → check item = true → predicate itemitem:αhItem:item ∈ items⊢ predicate item
  exact hSound item hItem ((List.all_eq_true.mp hCheck) item hItem)All goals completed! 🐙

Boolean existential search over a decoded finite row list.

def anyDecide {α : Type}
    (items : List α)
    (predicate : α → Prop)
    [DecidablePred predicate] :
    Bool :=
  items.any fun item => decide (predicate item)

A successful finite boolean existential check supplies a matching row.

theorem anyDecide_sound
    {α : Type}
    {items : List α}
    {predicate : α → Prop}
    [DecidablePred predicate]
    (hCheck : anyDecide items predicate = true) :
    ∃ item, item ∈ items ∧ predicate item := byα:Typeitems:List αpredicate:α → Propinst✝:DecidablePred predicatehCheck:anyDecide items predicate = true⊢ ∃ item, item ∈ items ∧ predicate item
  rcases List.any_eq_true.mp hCheck with ⟨item, hItem, hPredicate⟩α:Typeitems:List αpredicate:α → Propinst✝:DecidablePred predicatehCheck:anyDecide items predicate = trueitem:αhItem:item ∈ itemshPredicate:decide (predicate item) = true⊢ ∃ item, item ∈ items ∧ predicate item
  exact ⟨item, hItem, of_decide_eq_true hPredicate⟩All goals completed! 🐙

Standard Row Properties

Boolean duplicate-freedom check for a decoded list.

def nodupCheck {α : Type} [DecidableEq α] (items : List α) : Bool :=
  propCheck items.Nodup

Successful duplicate-freedom checking proves List.Nodup.

theorem nodupCheck_sound
    {α : Type}
    [DecidableEq α]
    {items : List α}
    (hCheck : nodupCheck items = true) :
    items.Nodup :=
  propCheck_sound hCheck

Boolean duplicate-freedom check for a projected key list.

def nodupMapCheck {α β : Type}
    [DecidableEq β]
    (items : List α)
    (key : α → β) :
    Bool :=
  nodupCheck (items.map key)

Successful projected duplicate-freedom checking proves List.Nodup for the keys.

theorem nodupMapCheck_sound
    {α β : Type}
    [DecidableEq β]
    {items : List α}
    {key : α → β}
    (hCheck : nodupMapCheck items key = true) :
    (items.map key).Nodup :=
  nodupCheck_sound hCheck

Boolean permutation check for two decoded lists.

def permCheck {α : Type} [DecidableEq α] (left right : List α) : Bool :=
  propCheck (left.Perm right)

Successful permutation checking proves List.Perm.

theorem permCheck_sound
    {α : Type}
    [DecidableEq α]
    {left right : List α}
    (hCheck : permCheck left right = true) :
    left.Perm right :=
  propCheck_sound hCheck

Boolean membership check for a decoded finite list.

def memCheck {α : Type} [DecidableEq α] (item : α) (items : List α) : Bool :=
  propCheck (item ∈ items)

Successful membership checking proves list membership.

theorem memCheck_sound
    {α : Type}
    [DecidableEq α]
    {item : α}
    {items : List α}
    (hCheck : memCheck item items = true) :
    item ∈ items :=
  propCheck_sound hCheck

Boolean set-style equality for lists, ignoring multiplicity and order.

def sameMembersCheck {α : Type} [DecidableEq α] (left right : List α) : Bool :=
  allDecide left (fun item => item ∈ right) &&
    allDecide right (fun item => item ∈ left)

Successful set-style equality checking proves membership equivalence.

theorem sameMembersCheck_sound
    {α : Type}
    [DecidableEq α]
    {left right : List α}
    (hCheck : sameMembersCheck left right = true) :
    ∀ item, item ∈ left ↔ item ∈ right := byα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:sameMembersCheck left right = true⊢ ∀ (item : α), item ∈ left ↔ item ∈ right
  unfold sameMembersCheck at hCheckα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:((allDecide left fun item => item ∈ right) && allDecide right fun item => item ∈ left) = true⊢ ∀ (item : α), item ∈ left ↔ item ∈ right
  rw [Bool.and_eq_true] at hCheckα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:(allDecide left fun item => item ∈ right) = true ∧ (allDecide right fun item => item ∈ left) = true⊢ ∀ (item : α), item ∈ left ↔ item ∈ right
  intro itemα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:(allDecide left fun item => item ∈ right) = true ∧ (allDecide right fun item => item ∈ left) = trueitem:α⊢ item ∈ left ↔ item ∈ right
  constructormpα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:(allDecide left fun item => item ∈ right) = true ∧ (allDecide right fun item => item ∈ left) = trueitem:α⊢ item ∈ left → item ∈ rightmprα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:(allDecide left fun item => item ∈ right) = true ∧ (allDecide right fun item => item ∈ left) = trueitem:α⊢ item ∈ right → item ∈ left
  ·mpα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:(allDecide left fun item => item ∈ right) = true ∧ (allDecide right fun item => item ∈ left) = trueitem:α⊢ item ∈ left → item ∈ right intro hItemmpα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:(allDecide left fun item => item ∈ right) = true ∧ (allDecide right fun item => item ∈ left) = trueitem:αhItem:item ∈ left⊢ item ∈ right
    exact allDecide_sound hCheck.left item hItemAll goals completed! 🐙
  ·mprα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:(allDecide left fun item => item ∈ right) = true ∧ (allDecide right fun item => item ∈ left) = trueitem:α⊢ item ∈ right → item ∈ left intro hItemmprα:Typeinst✝:DecidableEq αleft:List αright:List αhCheck:(allDecide left fun item => item ∈ right) = true ∧ (allDecide right fun item => item ∈ left) = trueitem:αhItem:item ∈ right⊢ item ∈ left
    exact allDecide_sound hCheck.right item hItemAll goals completed! 🐙

Gated Pair Checks

Check all pairs that satisfy a decidable gate. Ungated pairs are ignored.

def allPairsWhenCheck
    {α β : Type}
    (left : List α)
    (right : List β)
    (condition : α → β → Prop)
    [DecidableRel condition]
    (check : α → β → Bool) :
    Bool :=
  left.all fun leftItem =>
    right.all fun rightItem =>
      if condition leftItem rightItem then
        check leftItem rightItem
      else
        true

Successful gated-pair checking proves the target predicate for every gated pair.

theorem allPairsWhenCheck_sound
    {α β : Type}
    {left : List α}
    {right : List β}
    {condition : α → β → Prop}
    [DecidableRel condition]
    {check : α → β → Bool}
    {predicate : α → β → Prop}
    (hCheck : allPairsWhenCheck left right condition check = true)
    (hSound :
      ∀ leftItem, leftItem ∈ left →
        ∀ rightItem, rightItem ∈ right →
          check leftItem rightItem = true → predicate leftItem rightItem) :
    ∀ leftItem, leftItem ∈ left →
      ∀ rightItem, rightItem ∈ right →
        condition leftItem rightItem → predicate leftItem rightItem := byα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:allPairsWhenCheck left right condition check = truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItem⊢ ∀ (leftItem : α),
  leftItem ∈ left → ∀ (rightItem : β), rightItem ∈ right → condition leftItem rightItem → predicate leftItem rightItem
  intro leftItem hLeftα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:allPairsWhenCheck left right condition check = truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ left⊢ ∀ (rightItem : β), rightItem ∈ right → condition leftItem rightItem → predicate leftItem rightItem rightItemα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:allPairsWhenCheck left right condition check = truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:β⊢ rightItem ∈ right → condition leftItem rightItem → predicate leftItem rightItem hRightα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:allPairsWhenCheck left right condition check = truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ right⊢ condition leftItem rightItem → predicate leftItem rightItem hConditionα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:allPairsWhenCheck left right condition check = truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItem⊢ predicate leftItem rightItem
  unfold allPairsWhenCheck at hCheckα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:(left.all fun leftItem =>
    right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) =
  truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItem⊢ predicate leftItem rightItem
  have hLeftCheck :=
    (List.all_eq_true.mp hCheck) leftItem hLeftα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:(left.all fun leftItem =>
    right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) =
  truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItemhLeftCheck:(right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) = true⊢ predicate leftItem rightItem
  have hRightCheck :=
    (List.all_eq_true.mp hLeftCheck) rightItem hRightα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:(left.all fun leftItem =>
    right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) =
  truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItemhLeftCheck:(right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) = truehRightCheck:(if condition leftItem rightItem then check leftItem rightItem else true) = true⊢ predicate leftItem rightItem
  by_cases hConditionCheck : condition leftItem rightItemposα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:(left.all fun leftItem =>
    right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) =
  truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItemhLeftCheck:(right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) = truehRightCheck:(if condition leftItem rightItem then check leftItem rightItem else true) = truehConditionCheck:condition leftItem rightItem⊢ predicate leftItem rightItemnegα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:(left.all fun leftItem =>
    right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) =
  truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItemhLeftCheck:(right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) = truehRightCheck:(if condition leftItem rightItem then check leftItem rightItem else true) = truehConditionCheck:¬condition leftItem rightItem⊢ predicate leftItem rightItem
  ·posα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:(left.all fun leftItem =>
    right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) =
  truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItemhLeftCheck:(right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) = truehRightCheck:(if condition leftItem rightItem then check leftItem rightItem else true) = truehConditionCheck:condition leftItem rightItem⊢ predicate leftItem rightItem simp [hConditionCheck] at hRightCheckposα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:(left.all fun leftItem =>
    right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) =
  truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItemhLeftCheck:(right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) = truehConditionCheck:condition leftItem rightItemhRightCheck:check leftItem rightItem = true⊢ predicate leftItem rightItem
    exact hSound leftItem hLeft rightItem hRight hRightCheckAll goals completed! 🐙
  ·negα:Typeβ:Typeleft:List αright:List βcondition:α → β → Propinst✝:DecidableRel conditioncheck:α → β → Boolpredicate:α → β → ProphCheck:(left.all fun leftItem =>
    right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) =
  truehSound:∀ (leftItem : α),
  leftItem ∈ left →
    ∀ (rightItem : β), rightItem ∈ right → check leftItem rightItem = true → predicate leftItem rightItemleftItem:αhLeft:leftItem ∈ leftrightItem:βhRight:rightItem ∈ righthCondition:condition leftItem rightItemhLeftCheck:(right.all fun rightItem => if condition leftItem rightItem then check leftItem rightItem else true) = truehRightCheck:(if condition leftItem rightItem then check leftItem rightItem else true) = truehConditionCheck:¬condition leftItem rightItem⊢ predicate leftItem rightItem exact False.elim (hConditionCheck hCondition)All goals completed! 🐙

end Checkend AdmissionArtifactend Cortex.Wire

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Wire.AdmissionArtifact.Boundary Next →Cortex.Wire.AdmissionArtifact.Generated