Meta results regarding sorry and pseudo attributions

i. Overview

The purpose of this module is to collect all results which depend on the sorryAx axiom and the Lean.ofReduceBool axiom, and check that these results are correctly attributed sorryful and pseudo respectively.

ii. Key results

• sorryfulPseudoTest : A test that all results attributed sorryful depend on the sorryAx axiom and vice versa, and all results attributed pseudo depend on the Lean.ofReduceBool axiom and vice versa.

iii. Table of contents

• A. Collectings results depending on sorryAx and Lean.ofReduceBool
  • A.1. The state information to be collected
  • A.2. The monad for collecting names
  • A.3. The collection function
  • A.4. Given an array updating the state with all names depending on axioms
  • A.5. Given an array getting all names depending on axioms
  • A.6. Getting all names depending on axioms from all user defined constants
• B. Collecting all names attributed sorryful and pseudo
• C. Testing the sorryful and pseudo attributions are correctly applied

iv. References

Some of the code here is adapted from from the file: Lean.Util.CollectAxioms copyright (c) 2020 Microsoft Corporation. Authored by Leonardo de Moura.

A. Collectings results depending on sorryAx and Lean.ofReduceBool

A.1. The state information to be collected

structure PhysLean.CollectSorry.State : Type

A structure used for collecting names of results dependent on the sorryAx axiom and the Lean.ofReduceBool axiom.

• visited : Lean.NameSet

  The names which have already been visited as part of the state.

• containsSorry : Lean.NameSet

  The names which depend on the sorryAx axiom.

• containsOfReduceBool : Lean.NameSet

  The names which depend on the Lean.ofReduceBool axiom.

A.2. The monad for collecting names

@[reducible, inline]

abbrev PhysLean.CollectSorry.M (α : Type) : Type

A monad used for collecting names of results dependent on the sorryAx axiom and the Lean.ofReduceBool axiom.

Equations

• PhysLean.CollectSorry.M = ReaderT Lean.Environment (StateM PhysLean.CollectSorry.State)

A.3. The collection function

partial def PhysLean.CollectSorry.collect (c : Lean.Name) (parents : Lean.NameSet) : M Unit

Given a c : Name updating the monad M based on which results which c uses depend on the sorryAx axiom and the Lean.ofReduceBool axiom.

A.4. Given an array updating the state with all names depending on axioms

def PhysLean.CollectSorry.allSorryPseudo (c : Array Lean.Name) : M Unit

Given a c : Array Name updating the monad M based on which results depend on the sorryAx axiom and the Lean.ofReduceBool axiom.

Equations

• PhysLean.CollectSorry.allSorryPseudo c = Array.forM (fun (x : Lean.Name) => PhysLean.CollectSorry.collect x ∅) c

A.5. Given an array getting all names depending on axioms

def PhysLean.collectSorryPseudo (c : Array Lean.Name) : Lean.CoreM (Array Lean.Name × Array Lean.Name)

Given a c : Array Name the names of all results used to defined the results in c with the sorryAx axiom and the Lean.ofReduceBool axiom.

Equations

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

A.6. Getting all names depending on axioms from all user defined constants

def PhysLean.allWithSorryPseudo : Lean.CoreM (Array Lean.Name × Array Lean.Name)

The axioms of a constant.

Equations

• PhysLean.allWithSorryPseudo = do let __do_lift ← PhysLean.allUserConsts let x ← PhysLean.collectSorryPseudo (Array.map (fun (c : Lean.ConstantInfo) => c.name) __do_lift) pure x

B. Collecting all names attributed sorryful and pseudo

unsafe def PhysLean.allSorryfulAttributed : Lean.CoreM (Array Lean.Name)

All names which are attributed sorryful.

Equations

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

unsafe def PhysLean.allPseudoAttributed : Lean.CoreM (Array Lean.Name)

All names which are attributed pseudo.

Equations

• PhysLean.allPseudoAttributed = do let env ← Lean.getEnv let pseudoInfos : Array PseudoInfo := pseudoExtension.getState env pure (Array.map (fun (info : PseudoInfo) => info.name) pseudoInfos)

C. Testing the sorryful and pseudo attributions are correctly applied

unsafe def PhysLean.sorryfulPseudoTest : Lean.MetaM Unit

Checks whether all results attributed sorryful depend on the ```sorryAx` axiom and vice versa.

Equations

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