leanified/CoreReader/Engineering/Reflection.lean

Back to claims · Declarations and proofs

Philosophy 0.2.1 · considered Core 0.1.2. This view uses the repository’s public target catalog, readers and Lean files. Presentation does not change their judgments.

Expand Lean and line explanations · 113 lines

LeanLine explanation

L1import CoreReader.Adopted

Import CoreReader.Adopted, making its declarations and transitive dependencies available; this line adds no new proposition.

L3namespace CoreReader.Engineering.Reflection

Open namespace CoreReader.Engineering.Reflection for the following declarations.

L5open CoreReader.Agency CoreReader.Adopted

Allow unqualified references to declarations in CoreReader.Agency CoreReader.Adopted; their meaning is unchanged.

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

Comment explains why Target retains owner, actual object and examined stage; these links are encoded by its fields.

L8structure Target (Object : Type) where

For any object type, Target stores an owner, an object of that type, and a lifecycle phase.

L9  owner : Nat

The owner's identifier is a natural number; uniqueness is not a field invariant.

L10  object : Object

This field retains the actual object, rather than just its name.

L11  phase : Phase

The target includes the phase being examined.

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

Comment introduces a finite assessment contract with actual tests and a claimed scope.

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

Comment limits this scope representation to the application; it is not a universal definition of assessment.

L15structure Contract (W : Type) where

For any sample type W, Contract packages one Boolean test and two finite lists.

L16  test : W → Bool

The test maps each W value to a Boolean verdict.

L17  tested : List W

This list records the initial tested cases; it may be empty.

L18  claimed : List W

This is the contract's claimed list; evaluate does not read it.

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

Comment introduces target-associated inputs; Model.input later enforces the field selection from that target.

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

Comment states the purpose of preventing another object's test from replacing this inquiry; raw Input alone does not enforce a provenance invariant.

L22structure Input (W Object : Type) where

Input is polymorphic in sample and object types, packaging the target and the data used for its inquiry.

L23  target : Target Object

Retain the full owner/object/phase target.

L24  contract : Contract W

Store the test contract associated by the model with this object.

L25  requested : List W

This requested list is what evaluate checks after the initial list passes.

L26  reasons : List String

Reasons are strings; nonemptiness will be checked, not their truth or relevance by string analysis.

L27  basis : Prop

The basis is an arbitrary proposition; interpret requires its proof.

L29inductive Verdict | supportedWithinScope | counterexample | noSupportingSample

Define three verdicts: support within scope, counterexample, and no supporting sample.

L30  deriving DecidableEq, Repr

Derive DecidableEq, Repr: decidable equality and printable representations of these constructors.

L32inductive Outcome (W : Type)

Outcome is indexed by sample type W and records either a generation result or an assessment.

L33  | generated (tests scope : List W)

A generated outcome stores separate tests and scope lists, both over W.

L34  | assessed (verdict : Verdict)

An assessed outcome stores a Verdict and no sample list.

L35  deriving DecidableEq

Derive decidable equality for Outcome W when [DecidableEq W] is available; the generated instance retains that typeclass premise, satisfied by the concrete ReviewCase model.

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

Comment warns that success on initial samples does not by itself license a wider requested list.

L38instance there changes the assessment to counterexample. -/

Comment identifies an actually failing requested case as the counterexample branch after initial success.

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

With implicit types W and Object and one input, evaluate computes a verdict from two Boolean all-tests.

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

First require every initially tested case to pass; List.all on an empty list is true.

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

If initial tests pass and every requested case passes, return supportedWithinScope, even when initial tests are empty.

L42    else .counterexample

If initial tests pass but some requested case fails, return counterexample.

L43  else .noSupportingSample

A failing initial case returns noSupportingSample; the name does not mean an explicit empty-list check exists.

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

Comment describes generation as proposing tests and begins the distinction from validating them.

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

Comment denies that proposal generation proves either test success or warranted adoption.

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

With implicit sample/object types, generate produces a proposed Outcome from the input.

L48  .generated input.requested input.requested

Copy requested into both generated tests and generated scope; neither list is validated here.

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

interpret takes an activity and an input, with both types implicit.

L51    (outcome : Outcome W) : Prop :=

The final explicit argument is an outcome; the result is a proposition about that outcome.

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

Require a nonempty reasons list and the input's basis proposition, then branch on the activity.

L53  | .generation => outcome = generate input

Generation means exact equality to this input's actual generator output.

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

Assessment means exact equality to the verdict computed by evaluate on this input.

L56structure Model (W Object : Type) where

A Model over W and Object supplies target membership, contracts, applicability and recorded outcomes.

L57  owner : Nat

The model has one natural-number owner identifier.

L58  objects : List Object

Only objects in this finite list can satisfy Model.self.

L59  contracts : Object → Contract W

Assign a contract to every Object value, including values outside objects.

L60  requested : Object → Phase → List W

Requested cases depend on the object and phase.

L61  reasons : Object → Phase → List String

Reason strings depend on the same object and phase.

L62  basis : Object → Phase → Prop

The basis proposition also depends on that object and phase.

L63  generationApplies : Object → Phase → Prop

A proposition determines generation applicability per object and phase.

L64  assessmentApplies : Object → Phase → Prop

A separate proposition determines assessment applicability.

L65  recorded : Activity → Object → Phase → Outcome W

Recorded outcomes depend on activity, object and phase; correctness is not assumed here.

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

Model.input builds the inquiry for any target; it does not itself check owner or membership.

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

Use the target itself and select contract, requested cases and reasons by its actual object/phase.

L69    m.basis t.object t.phase⟩

Complete the input with the basis selected at the same object and phase.

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

Model.self is the membership/ownership predicate on targets.

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

Both equal owner and membership of the actual object are required; phase is unrestricted here.

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

For a model and activity, construct the corresponding reflexive rule.

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

The rule's target/input/output types are exactly Target Object, Input W Object and Outcome W.

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

Use model owner plus local identifier 0 for generation or 1 for assessment.

L77  activity := activity

Retain the supplied activity in the rule.

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

Applicability requires a self target and the activity-specific applicability condition.

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

Generation uses this object's generationApplies at this phase.

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

Assessment uses this object's assessmentApplies at this phase.

L81  input := m.input

The actual rule input is the model's target-indexed input constructor.

L82  meaning := interpret activity

The rule meaning is the actual interpret function for this activity.

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

Build the list of rules for this model, with both generic types inferred.

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

The rule list contains generation first and assessment second, with no other rules.

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

Comment identifies performed data as stated records, with a separate follows check.

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

Comment specifies comparison with actual input evaluation; success is not inferred from the outcome's name.

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

Define recorded performance as a relation belonging to this model.

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

The relation explicitly takes a principle key, target, input and outcome and returns Prop.

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

Require self membership and exact equality to the input built for that target.

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

Existentially choose an activity whose rule key equals the supplied key.

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

The outcome must be exactly the record for that activity and this same object/phase.

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

Model.follows states that all applicable records satisfy their actual meaning.

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

Universally quantify activity, object and phase, then assume object membership.

L97    (match activity with

The next premise selects applicability by activity.

L98      | .generation => m.generationApplies object phase

For generation, require generationApplies on the quantified object/phase.

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

For assessment, require assessmentApplies before asserting the interpretation.

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

Check recorded outcome against actual input, fixing the target owner to m.owner.

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

Comment emphasizes that the generic implication retains its substantive evaluation premise.

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

Comment requires concrete instances to prove follows for their own actual contracts.

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

For arbitrary types and model, the theorem assumes checked : m.follows; it does not derive this premise.

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

Under that premise, prove rule-key identity and applicable self-performance in reflexivitySpecification.

L106  constructor

Split the specification into identity and performance obligations.

L107  · intro p hp q hq equal

Introduce two listed rules and assume their keys are equal.

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

Expand membership of the two-rule list into generation/assessment alternatives.

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

Substitute each membership alternative, yielding four rule pairs.

L110    · rfl

When both rules are the same activity, their required equality is reflexive.

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

For generation versus assessment, project equal keys to localId and contradict 0 = 1.

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

For assessment versus generation, the same projection contradicts 1 = 0.

L113    · rfl

When both rules are the same activity, their required equality is reflexive.

L114  · intro rule hr target hs ha

Introduce a listed rule, self target and applicability proof for the performance obligation.

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

Reduce the rule's list membership to its two possible activities.

L116    rcases hr with rfl | rfl

Handle generation and assessment separately by substitution.

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

For generation, choose its recorded outcome at this target's object/phase as witness.

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

Prove performed using self membership, exact input, and the generation activity; leave meaning to prove.

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

Apply checked to this generation record, using object membership from hs and applicability from ha.

L120      rcases target with ⟨owner, object, phase⟩

Destructure the target into owner, object and phase to expose the ownership equality.

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

Extract owner = m.owner from the self-target premise.

L122      subst owner

Substitute the model owner so checked and the target refer to identical inputs.

L123      exact actual

The previously obtained actual interpretation now exactly closes the goal.

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

For assessment, choose its recorded verdict at the same target as witness.

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

Construct performed with the assessment activity and exact input/output identities.

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

Use checked for assessment, retaining this target's membership and applicability premises.

L127      rcases target with ⟨owner, object, phase⟩

Destructure the target into owner, object and phase to expose the ownership equality.

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

Extract owner = m.owner from the self-target premise.

L129      subst owner

Substitute the model owner so checked and the target refer to identical inputs.

L130      exact actual

The previously obtained actual interpretation now exactly closes the goal.

L132end CoreReader.Engineering.Reflection

Close namespace CoreReader.Engineering.Reflection; no further mathematical claim is asserted.