Cache the domain information for a formula. This is called by processDomains to apply it to the entire document.

The same routine as reverseEquation, but doesn't reverse the equation. This differs from eq.copy() in that it doesn't copy attributes

Expression Diff

Given two Application LC's which differ only at one node, return the address of that node (or undefined if no such node exists). This is useful in transitive chains for determining when a substitution occurs within a compound expression.

For example, in (x+1)+(x^2+x)=(x+1)+(x⋅x+x) we want to know that the LHS can be obtained from the RHS by substituting x^2=x⋅x.

If they differ at more than one location, return the array of all of the addresses where they differ. If the optional argument 'intersect' is true return the highest address containing all of the diffs. For example,

  diff( f(g(a,b) , f(g(c,d)) ) returns [[1,1],[1,2]]

but

  diff( f(g(a,b) , f(g(c,d)) , true ) returns [[1]]

so in the latter case we know that the second expression can be obtained from the first via the single substitution g(a,b)=g(c,d), whereas the former would require two substitutions, a=c and b=d.

Check if an expression is forbidden as a Weeny Currently we don't try to match user expressions to a pattern that is a single metavariable or EFA that is not partially instantiated because they match everything. This causes some rules, like or- or substitution, to require another validation tool like BIH, Cases, or Equations.

Note that for EFA's it is ok if the expression is partially instantiated, so that it's not enough just for it to be an EFA. For example, in the substitution rule, both the premise and conclusion is of the form @P(x) where bot P and x are metaviarables. But if the premise that is the equation is instantiated first to create a partial instantiation of the rule, then the x will be replaced by an expression not containing any metavariables which is MUCH more efficient for matching. For example, in an expression like (-(z*y)+z*x)+z*y = z*y+(-(z*y)+z*x) (an actual example) trying to match that expression to @P(x) where x and P are metavars produces a whopping 191 matches. But trying to match it to e.g. @P(z*y), only produces 16 matches... much more manageable.

The LurchOptions.avoidLoneMetavars and LurchOptions.avoidLoneEFAs options can be used to change the behavior of this function in the corresponding manner. They are both true by default.

Find all of the Rules that have a conclusion that is a single metavariable, and only appears in the Rule as a single metavariable outermost expression (i.e., not contained in any other expression). This is called a caselike rule.

Get all of the user proposition in the document, but don't include any duplicates, i.e., no two expressions should have the same prop form. This should be run BEFORE instantiating so the expressions in instantiations aren't counted as a user expression.

Many of the tools that work with $n$-compact validation (including the $n$-compact tool itself) require creating and inserting instantiations and marking them in various ways. This utility makes that process more coherent. It also allows us to check for 'bad' instantiations that e.g. instantiate a metavariable that is inside (declared by) a declaration with a constant, or instantiate both $x$ and $y$ with the same thing in an declaration like [ x y ].

If we want to give users symmetry of = for free, it is more efficient to just manually instantiate the symmetry rule for all equations than to insert the rule and let matching do it.

This is the meat of the algorithm for $n$-compact validation. It takes a document as an argument.

1. Get the set of propositions, E, in the user's document.
2. Get the set, F, of all unfinished formulas with any max weenies.
3. For each f in F, a. Match each maximally weeny p in f to each e in E. b. Every time a match is found. i. Insert the relevant instantiation, and store e in its .creators js attribute (it can have more than one) along with other info. ii. Cache its domain and update its weenies.
4. Mark f as .finished. It cannot be instantiated again on future passes because while the number of available formulas can go up on each pass, the set of user expressions E cannot.
5. Iterate until every instantiation attempt has been exhausted.

Transitivity Instantiations

Go through and fetch all of the user's equations (i.e., only equations that are conclusions) which have more than two arguments and create and insert them after the EquationsRule rule. For example, a=b=c=d=e would produce and insert the instantiation :{ :a=b :b=c :c=d :d=e a=e }

This is a helper utility called by processEquations().

Check a proposed instantiation for bad declarations.

• If it declares a constant, it's bad.
• If it declares more than one symbol that are instantiated with the same thing, it's bad.

Match Givens.

Since Matching won't match an environment to a formula that has a different given status, check if LCs a and b are both givens or both claims and if not, toggle the given status of a. Return true if it was toggled and false it it wasn't. This is just a utility used by processBIHs.

Matching Propositions.

Since we consider Lets and ForSomes to be proposition, we want to be able to try to match any proposition to any other proposition. The Problem class currently can't handle this, so we add a utility here to make it possible.

This routine returns an array of solutions.

Process BIHs

Go through and create the appropriate instantiations from the Blatant Hints in document L, mark each as BIH-valid or not, and insert the relevant instantiation when they are BIH-valid. Note that we are keeping track of the distinction between being propositionally valid, and being BIH-valid. Namely, a particular environment, marked as a BIH, could be propositionally valid in the user's document, but not a BIH. e.g. { :P (⇒ P P)} << would be propositionally valid in a document that depends on Prop lib but not an instatiation of the ⇒+ rule.

Process the Proof by Cases tool.

Find the first Rule in the document flagged with .label='cases'. If found, instantiate its last child using each user conclusion that has .by='cases', insert the (usually partial) instantiations after the Rule, leaving the Rule available for further instantation by the global Prop tool (i.e. don't mark it .finished).

Then check of LurchOptions.autoCases is true. If it is find every rule that has

a) its last conclusion is a metavariable

b) every occurrence of that metavariable in the rule is an outermost expression.

Create the instantiation of every such rule by matching the metavariable conclusion to every one of the user's conclusions.

Cache all Domains

For efficiency, mark all of the expressions in formulas with their domains (the set of metavariable text names) for easy lookup. This assumes that the metavariables have been marked during interpretation. We also mark the formula with its maximally Weenyexpressions, and its domain size while we are caching stuff for easy access later.

This routine applies cacheFormulaDomainInfo to all formulas in the document.

Check if the doc contains the Rule :{ :EquationsRule }. If not, just split the equation chains.

Otherwise after splitting get the diffs of all equations, and add the instantiation :{ :x=y f(x)=f(y) } after the above Rule. For an arbitrary equation A=B the values of x,y are computed with diff(A,B). Note that this assumes = is reflexive, because the normal way to say this would be to say that A=A by reflexive and then :{ :x=y :A=A A=B } by substitution.

For each equation a=b=c=d that is split, also include the instantiation :{ :a=b :b=c :c=d a=d } after the above rule. This assumes transitivity of equality.

Finally, to assume symmetry we allow both x=y and y=x versions of the above rules. So including the Transitive Chain Rule is assuming reflexive, symmetric, transitive, and substitution properties for equality.

Given an equation x=y, return the equation y=x using copies of x and y. It does not copy the LC attributes of the original equation.

Go through and fetch all of the user's equations (i.e., only equations that are conclusions). If they have more than two arguments split them into binary pairs and insert them in the document.

Rename ProperNames from declarations with body to something easier to read by changing, e.g. c#(= (+ (+ m n) p) (+ m (+ n p)) to c#13 by putting them all in a list and using the list number instead of the body name. This isn't necessary for the algorithm to work, but it's easier to debug and read.

Validate!

This is the main routine! It requires that doc is an LC environment that has already been interpreted, so if it has not, then it runs interpret() first. It then runs all available validation tools that are compatible with n-compact global validation. Finally, it runs global validation algorithm itself, and returns the modified document with feedback stored in the various locations.

The optional second argument specifies which inference in the document should be validated, and defaults to checking the entire document. The optional third argument determines if it should additionally check for preemies and defaults to true. It defaults to the entire document.

This function can be called with various different options set. But rather than trying to pass the options object along the chain of computation as an optional argument, we just set a global LurchOptions object. This allows

The current validation tools available are the BIH tool, the Equations tool, the Cases tool, and Scoping tool. These can be toggled or customized via the settings object. In general, this routine provides the hook for installing new n-compact global validation compatible tools in the future. Validation tools can add validation feedback and add additional complete instantiations to the document, and can be run before or after instantiation, but should not add new Rules.