2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ If you want to see the definitions relating to "ProofDataset", you can find them using the tools in this question $\endgroup$ – Jason B. Dec 5 '18 at 22:35
2
$\begingroup$

"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"]} *)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.