leanified/CoreReader/Engineering/Reflection.lean

返回主张速览 · 声明与证明

哲学 0.2.1 · 已考虑的 Core 0.1.2。阅读视图来自本仓库公开的目标清单、读者稿和 Lean 文件；页面布局不改变其中的判定。

展开 Lean 与逐行解读 · 113 行

Lean逐行解读

L1import CoreReader.Adopted

导入 CoreReader.Adopted，使其声明及传递依赖可用；此行不新增命题。

L3namespace CoreReader.Engineering.Reflection

开启 CoreReader.Engineering.Reflection 命名空间，后续声明归入其中。

L5open CoreReader.Agency CoreReader.Adopted

允许不带完整限定名引用 CoreReader.Agency CoreReader.Adopted 中的声明；不改变其含义。

L7/- A target retains the owner, the actual object and the stage being examined. -/

注释说明 Target 保留所有者、实际对象及受检阶段的用意；这些连接由字段编码。

L8structure Target (Object : Type) where

对任意对象类型，Target 保存所有者、该类型的实际对象和生命周期阶段。

L9  owner : Nat

所有者标识是自然数；该字段不要求全局唯一。

L10  object : Object

此字段保留实际对象，而非仅存名称。

L11  phase : Phase

目标包含当前受检查的阶段。

L13/- A finite assessment contract has actual tests and a scope it claims to cover.

注释介绍包含实际测试与声称范围的有限评估合约。

L14The scope is an application limit, not a universal definition of assessment. -/

注释把此范围表示限于应用，不将其当作评估的普遍定义。

L15structure Contract (W : Type) where

对任意样本类型 W，Contract 包含一个布尔测试和两个有限列表。

L16  test : W → Bool

测试把每个 W 值映射为布尔结果。

L17  tested : List W

此列表记录初始测试案例，允许为空。

L18  claimed : List W

此字段是合约声称覆盖的列表；evaluate 不读取它。

L20/- Inputs carry the contract belonging to the named target, so another object's

注释介绍与目标关联的输入；后续 Model.input 按该目标选择字段。

L21test result cannot silently discharge this target's inquiry. -/

注释说明防止用另一对象测试替代本次检查的目的；原始 Input 本身不强制来源不变量。

L22structure Input (W Object : Type) where

Input 对样本和对象类型均为多态，组合目标及其检查数据。

L23  target : Target Object

保留完整的所有者、对象、阶段目标。

L24  contract : Contract W

保存模型关联到此对象的测试合约。

L25  requested : List W

初始列表通过后，evaluate 检查此请求列表。

L26  reasons : List String

理由以字符串保存；后续检查列表非空，不通过字符串分析证明其真实性或相关性。

L27  basis : Prop

依据可为任意命题；interpret 要求其成立。

L29inductive Verdict | supportedWithinScope | counterexample | noSupportingSample

定义范围内支持、反例、无支持样本三个判定值。

L30  deriving DecidableEq, Repr

自动派生 DecidableEq, Repr：提供这些构造子的可判定相等与可打印表示。

L32inductive Outcome (W : Type)

Outcome 以样本类型 W 为参数，记录生成结果或评估结果。

L33  | generated (tests scope : List W)

生成结果保存两个 W 列表，分别表示测试和范围。

L34  | assessed (verdict : Verdict)

评估结果保存 Verdict，不保存样本列表。

L35  deriving DecidableEq

在具有 [DecidableEq W] 时为 Outcome W 派生可判定相等；生成的实例保留此前提，具体 ReviewCase 模型满足它。

L37/- A successful sample does not license the wider scope: an actual failing

注释说明初始样本成功本身不授权更广请求列表。

L38instance there changes the assessment to counterexample. -/

注释指出初始成功后，实际失败的请求案例会进入反例分支。

L39def evaluate {W Object : Type} (input : Input W Object) : Verdict :=

evaluate 隐含 W、Object 类型参数，输入一个 Input，以两次布尔全称检查计算判定。

L40  if input.contract.tested.all input.contract.test then

先要求全部初始测试通过；空列表的 List.all 为 true。

L41    if input.requested.all input.contract.test then .supportedWithinScope

初始测试与全部请求案例均通过时返回 supportedWithinScope；初始列表为空也可能如此。

L42    else .counterexample

初始测试通过而请求案例中有失败时，返回 counterexample。

L43  else .noSupportingSample

初始案例失败时返回 noSupportingSample；名称不意味着实现检查了空列表。

L45/- Generation proposes an expanded test set. Proposal generation does not prove

注释把生成描述为提议测试，并开始区分提议与验证。

L46that the resulting contract passes those tests or warrants adoption. -/

注释否认提议生成能证明测试通过或采纳有据。

L47def generate {W Object : Type} (input : Input W Object) : Outcome W :=

generate 隐含样本与对象类型参数，依据输入产生一个提议结果。

L48  .generated input.requested input.requested

把 requested 同时复制到生成测试与范围；此处不验证任一列表。

L50def interpret {W Object : Type} (activity : Activity) (input : Input W Object)

interpret 接收活动与输入，两个类型参数均隐含。

L51    (outcome : Outcome W) : Prop :=

最后一个显式参数是结果；返回值是关于该结果的命题。

L52  input.reasons ≠ [] ∧ input.basis ∧ match activity with

要求理由列表非空、输入依据命题成立，再按活动分支。

L53  | .generation => outcome = generate input

生成活动的含义是结果恰等于该输入的实际生成器输出。

L54  | .assessment => outcome = .assessed (evaluate input)

评估活动的含义是结果恰等于 evaluate 对此输入计算的判定。

L56structure Model (W Object : Type) where

Model 对 W、Object 参数化，提供目标成员、合约、适用性和记录结果。

L57  owner : Nat

模型具有一个自然数所有者标识。

L58  objects : List Object

仅此有限列表中的对象可满足 Model.self。

L59  contracts : Object → Contract W

为每个 Object 值分配合约，包括 objects 列表以外的值。

L60  requested : Object → Phase → List W

请求案例依赖对象与阶段。

L61  reasons : Object → Phase → List String

理由字符串依赖同一对象与阶段。

L62  basis : Object → Phase → Prop

依据命题也依赖该对象与阶段。

L63  generationApplies : Object → Phase → Prop

命题逐对象、逐阶段确定生成适用性。

L64  assessmentApplies : Object → Phase → Prop

另一命题确定评估适用性。

L65  recorded : Activity → Object → Phase → Outcome W

记录结果依赖活动、对象与阶段；此处不假定其正确。

L67def Model.input {W Object : Type} (m : Model W Object) (t : Target Object) : Input W Object :=

Model.input 为任意目标构建检查输入，本身不检查所有者或成员资格。

L68  ⟨t, m.contracts t.object, m.requested t.object t.phase, m.reasons t.object t.phase,

保留目标本身，按其实际对象和阶段选取合约、请求案例及理由。

L69    m.basis t.object t.phase⟩

以同一对象、阶段选出的依据补全输入。

L71def Model.self {W Object : Type} (m : Model W Object) (t : Target Object) : Prop :=

Model.self 是目标的成员与所有权谓词。

L72  t.owner = m.owner ∧ t.object ∈ m.objects

同时要求所有者相等、实际对象属于列表；此处不限制阶段。

L74def Model.rule {W Object : Type} (m : Model W Object) (activity : Activity) :

给定模型与活动，构造对应的反身规则。

L75    ReflexiveRule (Target Object) (Input W Object) (Outcome W) where

规则的目标、输入、输出类型分别固定为 Target Object、Input W Object、Outcome W。

L76  key := ⟨m.owner, match activity with | .generation => 0 | .assessment => 1⟩

键由模型所有者和局部编号组成，生成用 0，评估用 1。

L77  activity := activity

在规则中保留传入的活动。

L78  applicable t := m.self t ∧ match activity with

适用性要求目标属于自身，且满足对应活动的适用条件。

L79    | .generation => m.generationApplies t.object t.phase

生成采用此对象在此阶段的 generationApplies。

L80    | .assessment => m.assessmentApplies t.object t.phase

评估采用此对象在此阶段的 assessmentApplies。

L81  input := m.input

实际规则输入采用模型按目标构造的 input。

L82  meaning := interpret activity

规则含义采用该活动的实际 interpret 函数。

L84def Model.rules {W Object : Type} (m : Model W Object) :=

构建此模型的规则列表，两个泛型类型由推断确定。

L85  [m.rule .generation, m.rule .assessment]

规则列表仅含生成与评估两项，依次排列。

L87/- These are the stated records. The separate follows test compares each stated

注释指出 performed 数据是陈述记录，另由 follows 检查。

L88outcome with the actual input's evaluation, rather than defining success by its name. -/

注释说明要与实际输入评估比较，不能由结果名称推断成功。

L89def Model.performed {W Object : Type} (m : Model W Object)

定义属于此模型的记录执行关系。

L90    (key : PrincipleKey) (t : Target Object) (input : Input W Object) (outcome : Outcome W) : Prop :=

关系显式接收原则键、目标、输入、结果并返回 Prop。

L91  m.self t ∧ input = m.input t ∧

要求目标属于自身，且输入恰等于该目标实际构造的输入。

L92    ∃ activity, key = (m.rule activity).key ∧

存在一个活动，其规则键等于传入的键。

L93      outcome = m.recorded activity t.object t.phase

结果必须恰等于该活动与同一对象、阶段的记录。

L95def Model.follows {W Object : Type} (m : Model W Object) : Prop :=

Model.follows 表述所有适用记录均满足其实际含义。

L96  ∀ activity object phase, object ∈ m.objects →

全称量化活动、对象、阶段，再假设对象属于列表。

L97    (match activity with

下一前提按活动选取适用性。

L98      | .generation => m.generationApplies object phase

对生成，要求所量化对象、阶段的 generationApplies。

L99      | .assessment => m.assessmentApplies object phase) →

对评估，要求 assessmentApplies，再断言解释成立。

L100    interpret activity (m.input ⟨m.owner, object, phase⟩) (m.recorded activity object phase)

将记录结果与实际输入核对，目标所有者固定为 m.owner。

L102/- This generic implication retains the actual evaluation premise. Concrete

注释强调通用蕴涵保留实质评估前提。

L103engineering instances must discharge follows separately for their own contracts. -/

注释要求具体实例为各自实际合约证明 follows。

L104theorem recordedReflexivity {W Object : Type} (m : Model W Object) (checked : m.follows) :

对任意类型和模型，此定理假设 checked : m.follows，并不证明此前提。

L105    reflexivitySpecification m.rules m.self m.performed := by

在此前提下，证明 reflexivitySpecification 中的规则键身份与适用的自执行要求。

L106  constructor

将规范拆为身份与执行两个证明义务。

L107  · intro p hp q hq equal

引入列表内的两个规则，并假设其键相等。

L108    simp only [Model.rules, List.mem_cons, List.not_mem_nil, or_false] at hp hq

将两项规则列表的成员资格展开为生成或评估两种可能。

L109    rcases hp with rfl | rfl <;> rcases hq with rfl | rfl

替换两个成员的可能值，形成四种规则配对。

L110    · rfl

两个规则属于同一活动时，所需相等由反身性成立。

L111    · have bad := congrArg PrincipleKey.localId equal; contradiction

对生成与评估的配对，把键相等投影到 localId，得到 0 = 1 的矛盾。

L112    · have bad := congrArg PrincipleKey.localId equal; contradiction

对评估与生成的配对，相同投影得到 1 = 0 的矛盾。

L113    · rfl

两个规则属于同一活动时，所需相等由反身性成立。

L114  · intro rule hr target hs ha

为执行义务引入列表规则、自身目标及适用性证明。

L115    simp only [Model.rules, List.mem_cons, List.not_mem_nil, or_false] at hr

将规则成员资格化为两个活动的可能值。

L116    rcases hr with rfl | rfl

通过替换，分别处理生成与评估。

L117    · refine ⟨m.recorded .generation target.object target.phase,

在生成分支，选择此目标对象、阶段的生成记录作为存在见证。

L118        ⟨hs, rfl, .generation, rfl, rfl⟩, ?_⟩

利用自身成员资格、精确输入与生成活动证明 performed，留下含义义务。

L119      have actual := checked .generation target.object target.phase hs.2 ha.2

以 hs 的对象成员资格与 ha 的适用性，将 checked 用于该生成记录。

L120      rcases target with ⟨owner, object, phase⟩

把目标拆为所有者、对象、阶段，显露所有者相等关系。

L121      have ownerEqual : owner = m.owner := hs.1

从自身目标前提提取 owner = m.owner。

L122      subst owner

代入模型所有者，使 checked 与目标指向相同输入。

L123      exact actual

先前取得的实际解释此时恰好关闭目标。

L124    · refine ⟨m.recorded .assessment target.object target.phase,

在评估分支，选择同一目标的评估记录作为见证。

L125        ⟨hs, rfl, .assessment, rfl, rfl⟩, ?_⟩

以评估活动和精确输入、输出身份构造 performed。

L126      have actual := checked .assessment target.object target.phase hs.2 ha.2

将 checked 用于评估，保留此目标的成员及适用性前提。

L127      rcases target with ⟨owner, object, phase⟩

把目标拆为所有者、对象、阶段，显露所有者相等关系。

L128      have ownerEqual : owner = m.owner := hs.1

从自身目标前提提取 owner = m.owner。

L129      subst owner

代入模型所有者，使 checked 与目标指向相同输入。

L130      exact actual

先前取得的实际解释此时恰好关闭目标。

L132end CoreReader.Engineering.Reflection

关闭 CoreReader.Engineering.Reflection 命名空间；不另行断言数学主张。