In[]:=
coSubstitutionLemmas[f[x_,g[y_]],f[x_,y_]->h[g[x],k[y]]]
Out[]=
{{1},1}f[h[g[x_],k[y_]],g[y_]],{{2,1},1}f[x_,g[h[g[x_],k[y_]]]]
In[]:=
coSubstitutionLemmas[f[x_,x_],f[x_,y_]->g[x,y]]
Out[]=
{{1},1}f[g[x_,y_],f[x_,y_]],{{2},1}f[f[x_,y_],g[x_,y_]]
In[]:=
coSubstitutionLemmas[f[x_,x_],a->b]
Out[]=
{{1},1}f[b,a],{{2},1}f[a,b]
In[]:=
coSubstitutionLemmas[f[x_,x_,x_],a->b]
Out[]=
{{1},1}f[b,a,a],{{2},1}f[a,b,a],{{3},1}f[a,a,b]
Simplest case
Simplest case
Here the rule can be applied anywhere:
In[]:=
coSubstitutionLemmas[f[a,a,a],a->b]
Out[]=
{{1},1}f[b,a,a],{{2},1}f[a,b,a],{{3},1}f[a,a,b]
In this case substitution is the same:
In[]:=
substitutionLemmas[f[a,a,a],a->b]
Out[]=
{{1},1}f[b,a,a],{{2},1}f[a,b,a],{{3},1}f[a,a,b]
In[]:=
substitutionLemmas[f[x_,x_,x_],a->b]
Out[]=
In[]:=
coSubstitutionLemmas[f[x_,x_,x_],a->b]
Out[]=
{{1},1}f[b,a,a],{{2},1}f[a,b,a],{{3},1}f[a,a,b]
Substitution tries to find a subexpression of expr which matches lhs of rule MatchQ[subexpr, lhs]
Cosubstitution tries to find a subpattern of expr for which there is a match in lhs MatchQ[lhs, subexpr]
Then we can make a global match by aligning all the variables in expr
Then we can make a global match by aligning all the variables in expr
In[]:=
coSubstitutionLemmas[f[g[x_,y_],x_],g[a,b]->c]
Out[]=
{{1,1},1}f[g[c,y_],g[a,b]],{{1,2},1}f[g[x_,c],x_],{{1},1}f[c,a],{{2},1}f[g[g[a,b],y_],c]
In[]:=
coSubstitutionLemmas[f[g[x_],x_],g[a]->c]
Out[]=
{{1,1},1}f[g[c],g[a]],{{1},1}f[c,a],{{2},1}f[g[g[a]],c]
The first two of these have g[a] matching the f[g[x_],x_]
Out[]=
fg[x_],
Out[]=
f,x_
f[x_,x_,x_] can stand for any expression e.g. f[a,a,a]
f[g[x_],x_]
In[]:=
KeyMap[MapAt[Framed,f[g[x_],x_],First[#]]&,coSubstitutionLemmas[f[g[x_],x_],g[a]->c]]
Out[]=
fg,x_f[g[c],g[a]],f,x_f[c,a],fg[x_],f[g[g[a]],c]
In[]:=
ExpressionTree[f[g[x],x]]
Out[]=
In[]:=
ExpressionTree[g[a]]
Out[]=
This tree can match in various places....
[[ Show where the matches can go ]]
In[]:=
KeyMap[MapAt[Framed,f[g[x_],x_],First[#]]&,substitutionLemmas[f[g[x_],x_],g[a_]->c]]
Out[]=
f,x_f[c,x_]
In substitution, the “active variables” are inside the lhs of the rule; in cosubstitution they are inside the expression
<< Additional case: “realignment of RHS variables” >>
Critical pairs
Critical pairs
You can apply something in two different places ; the rules are two-way ;
In[]:=
Graph[{a<->b,a<->c},VertexLabels->Automatic]
Out[]=
In[]:=
coSubstitutionLemmas[a<->b,a<->c]
Out[]=
{Right,{1},1}cb
In[]:=
substitutionLemmas[a<->b,a<->c]
Out[]=
{Right,{1},1}cb
[[ Would these be different if there were parameters ? ]]]
If there is a rule where there is x_ on its own on one side, substitution is enough [ ?? ]
If there is a rule where there is x_ on its own on one side, substitution is enough [ ?? ]
Perhaps relevant:
Explanation Flow
Explanation Flow
In[]:=
DisplayReplacement[sub_,expr_,rule_]:=KeyMap[MapAt[Framed,expr,{First[#]}]&,sub[expr,rule]]
In[]:=
DisplayReplacement[substitutionLemmas,f[g[x_],x_],g[a]->c]
Out[]=
In[]:=
DisplayReplacement[substitutionLemmas,f[x_],f[a]->b]
Out[]=
In[]:=
DisplayReplacement[coSubstitutionLemmas,f[x_],f[a]->b]
Out[]=
ff[b],b
In[]:=
DisplayReplacement[coSubstitutionLemmas,f[x_],f[a]->g[b]]
Out[]=
ff[g[b]],g[b]
In[]:=
DisplayReplacement[coSubstitutionLemmas,f[g[x_],x_],g[a]->c]
Out[]=
fg,x_f[g[c],g[a]],f,x_f[c,a],fg[x_],f[g[g[a]],c]
KeyMap[MapAt[Framed,f[g[x_],x_],First[#]]&,coSubstitutionLemmas[f[g[x_],x_],g[a]->c]]
In[]:=
RepDiagram[type_,rule_,expr_,rep_]:=Grid<|"S"->,"C"->Red|>[type],rule,expr,Frame->All->Framed[rep]
In[]:=
coSubstitutionLemmas[f[x_],a->b]
Out[]=
{{1},1}f[b]
In[]:=
substitutionLemmas[f[x_],a->b]
Out[]=
In[]:=
substitutionLemmas[f[x_],f[u_]->g[u]]
Out[]=
{{},1}g[x_]
In[]:=
coSubstitutionLemmas[f[x_],f[u_]->g[u]]
Out[]=
{{1},1}f[g[u_]],{{},1}g[u_]
In[]:=
Table[VertexCount[ResourceFunction["TokenEventGraph"][{If[#[[1]]==1,{u_,v_}:>Union[Values[substitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]],Values[substitutionLemmas[v,u,"Uniquify"->True,"Canonicalize"->True]]],Nothing],If[#[[2]]==1,{u_,v_}:>Union[Values[coSubstitutionLemmas[u,v,"Uniquify"->True,"Canonicalize"->True]],Values[coSubstitutionLemmas[v,u,"Uniquify"->True,"Canonicalize"->True]]],Nothing]},{a_∘b_<->b_},t,"TokenLabeling"->False,"TokenMultiplicity"->Automatic,"EventLabeling"->"Colors",AspectRatio->1/2]],{t,1,2}]&/@{{1,0},{0,1},{1,1}}
Theorem proving
Theorem proving
Restricted Size
Restricted Size