Searching an expression in mmj2

[Benoit]

Since mmj2 can parse expressions, there might be a way to look for expressions which contain instances of a given expression ?

For example, how do I search all assertions which contain as a subexpression an instance of "ph -> ( E. x ( ph /\ ps ) ->" ?

Thanks,

Benoît

[Glauco]

Reading the help (see below the relevant part) it should be (but it doesn't work, for me):

InWhat: $ap

Part: Formulas

Format: ParseStmt

Oper: <=    (this if you want "contained" instances, as you wrote above)

ForWath: ( ph -> ( E. x ( ph /\ ps ) -> ch ) )      (it wants a "parsable" stmt, otherwise it returns an error)

From the help:

<snip>

The other two Formats, 'ParseExpr' and 'ParseStmt' operate on syntactic
parse trees (and so are restricted to formula objects...) When using these
Formats the contents of the ForWhat field are parsed into syntax trees for
use in the searching process.

<snip>

* ParseStmt : a ParseStmt search term is parsed to construct a parse tree for
  the statement (in set.mm it must be a wff). The statement's parse tree is
  then used in a unification-like process to search for a match with a formula
  parse tree. The precise match requirement is given by the Oper field --
  please refer to the Oper help text for details. Note: ParseExpr search terms
  must not begin with a statement code constant (i.e. "|-") and must not
  contain Work Variables. Example: "( ph -> ps )".

(there's a copypaste mistake: "Note: ParseExpr" should be Note: ParseStmt )

[Benoit]

Thanks Glauco.  I tried several variations but none work for me either...

[Steven Nguyen]

I think you could use "$?" to match any character, and by default it matches any subexpression so there's no need to use "$*", so the command would be like:

search * "$?$? -> ( E. $? ( $?$? /\ $?$? ) ->"

But when I try that, there's no results. Nevertheless there are results for
search * "( E. $? ( $?$? /\ $?$? ) ->"

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f7ea3431-e5d8-4cc6-92a5-b99ccdaed7bbn%40googlegroups.com.

[Benoit]

Thanks "icecream", but my question is about mmj2, not metamath.exe.  Metamath.exe does not parse math expressions, so there is no way to search for instances of a given expression. (In the sense of a substitution instance, e.g., "x e. y -> x e. z" is an instance of "ph -> ps").

Benoît

[David A. Wheeler]

> On Sunday, August 7, 2022 at 5:05:30 AM UTC+2 icecream...@gmail.com wrote:

> I think you could use "$?" to match any character, and by default it matches any subexpression so there's no need to use "$*", so the command would be like: ...

>
> On Aug 7, 2022, at 8:48 AM, Benoit <benoit...@gmail.com> wrote:
> Thanks "icecream", but my question is about mmj2, not metamath.exe. Metamath.exe does not parse math expressions, so there is no way to search for instances of a given expression. (In the sense of a substitution instance, e.g., "x e. y -> x e. z" is an instance of "ph -> ps").
> Benoît

I realize you asked about mmj2, not metamath.exe, but there's a trick I've used with metamath.exe
that *might* be helpful if you're looking for *instances* of a given expression.
You can have metamath.exe display the math expressions for each step,
then search *that* output for the patterns you want to find (e.g., using grep).

You can see an example In the set.mm repo script `scripts/find-repeats`, viewable here:
https://github.com/metamath/set.mm/blob/develop/scripts/find-repeats
That script sorts instances by how common they are, but the approach seems
useful for your case as well. Note: MacOS's grep is really bad & often crashes;
the easy solution is to install GNU grep instead.

The matches can occasionally match "things I didn't want"... but as a way
to quickly search for information, this approach can be quite helpful.

--- David A. Wheeler