# Inspecting Mathematica object

I'm using ProofObject for my question, but it applies to other objects too. FindEquationalProof returns ProofObject as a result:

proof = FindEquationalProof[a == c, {a == b, b == c}]


This example is taken from Mathematica's Help for FindEquationalProof.

The the Help article goes on with the following line:

proof["ProofDataset"]


When I look inside the proof object by List@@prof or by proof//FullForm I get this:

ProofObject[
"EquationalLogic",
a == c,
a == b && b == c,
{{"Axiom", 1} -> <|"Statement" -> b == a,
"Proof" -> <||>|>, {"Axiom", 2} -> <|"Statement" -> b == c,
"Proof" -> <||>|>, {"Hypothesis", 1} -> <|"Statement" -> a == c,
"Proof" -> <||>|>,
{"SubstitutionLemma", 1} -> <|"Statement" -> a == c,
"Proof" -> <|"Input" -> {"Axiom", 2}, "Position" -> 1,
"Construct" -> {"Axiom", 1}, "Orientation" -> 1,
"Rule" -> b -> a,
"OutputExpression" -> a == c|>|>, {"Conclusion",
1} -> <|"Statement" -> True,
"Proof" -> <|"Input" -> {"Hypothesis", 1}, "Position" -> 1,
"Construct" -> {"SubstitutionLemma", 1}, "Orientation" -> 1,
"Rule" -> a -> c, "OutputExpression" -> True|>|>}]


But there's no "ProofDataset" in this object.

In another question about ColorDataFunction I found the code for getting a list of property names and it worked for ProofObject:

proof["Properties"]


{"Axioms", "Logic", "ProofDataset", "ProofFunction", "ProofGraph", "ProofNotebook", "Theorem"}

And indeed ProofDataset is one of the property names.

I also tried ??ProofObject but it also does not include any definitions for properties.

My question is: what kind of object is ProofObject and which introspection functions can I use to get its contents?

Why is it possible to do proof["Properties"] for this object? What happens under the hood?

• If you want to see the definitions relating to "ProofDataset", you can find them using the tools in this question Dec 5, 2018 at 22:35

"ProofDataset" is a computed property of the ProofObject, it can be computed from the data inside the ProofObject but is not necessarily contained within the object.

Here is a simple toy example to demonstrate how this works:

getMyObject is a constructor, which creates a MyObject

getMyObject[{a_, b_}] := MyObject[<|"a" -> a, "b" -> b|>];
MyObject[assoc_]["ABSum"] := assoc["a"] + assoc["b"]


Now you can create this object and ask for it's "ABSum" property,

mo = getMyObject[{1, 2}]
(* MyObject[<|"a" -> 1, "b" -> 2|>] *)

mo["ABSum"]
(* 3 *)


Even though there are no rules inside of mo corresponding to "ABSum", there are definitions on MyObject on how to compute it:

SubValues@MyObject
(* {HoldPattern[MyObject[assoc_]["ABSum"]] :>
assoc["a"] + assoc["b"]} *)