I'm using KeYmaera X 5.0.2 on a remote Linux server (Ubuntu 22.04.3 LTS, amd64 architecture) accessed from a local Mac M1. The IJCAR22 implicit function examples do not appear, only the Textbook and Beginner's Tutorial Examples. (https://keymaerax.org/keymaeraXfunc/ indicates "To begin, click on the Import button for IJCAR22 Implicit Definitions Examples to load pre-defined example models.")
I copied the Arctan Identity example from implicitdefinitions.kyx. Apparently built-in functions like sin, cos, are known to my instance of KeYmaera X:
There are no errors or other warnings, but upon clicking "New proof", an error about undefined symbols cos,sin appears:
(NB: Implicit definitions work; e.g., I can define my own versions of sin,cos: implicit Real sine(Real t), cosine(Real t) = {{sine:=0; cosine:=1; t:=0;}; {sine'=cosine, cosine'=-sine, t'=1}};. However, this isn't very robust due to limitations on using custom functions. For example, t=0 & sine(0)=0 & cosine(0)=1 & x=1-> [{x'=-(sine(t)),t'=1} triggers a Core error:
In contrast, t=0 & x=0 & xdot=1 -> [{x'=xdot, xdot'=-x, t'=1}]x<=1 proves automatically. In my limited experience with implicit definitions, automation seems to perform worse in general, even when no errors are thrown. For instance t=0 & sine(0)=0 & cosine(0)=1 -> [{t'=1}@invariant((sine(t))^2 + (cosine(t))^2=1)]sine(t)<=1 requires the invariant for Auto to succeed.)
Probably extraneous detail: While running, the GUI shows "KeYmaera X 5.0.2 (no network)." at the bottom left.
I'm using KeYmaera X 5.0.2 on a remote Linux server (Ubuntu 22.04.3 LTS, amd64 architecture) accessed from a local Mac M1. The IJCAR22 implicit function examples do not appear, only the Textbook and Beginner's Tutorial Examples. (https://keymaerax.org/keymaeraXfunc/ indicates "To begin, click on the Import button for IJCAR22 Implicit Definitions Examples to load pre-defined example models.")
I copied the Arctan Identity example from implicitdefinitions.kyx. Apparently built-in functions like sin, cos, are known to my instance of KeYmaera X:
There are no errors or other warnings, but upon clicking "New proof", an error about undefined symbols cos,sin appears:
(NB: Implicit definitions work; e.g., I can define my own versions of sin,cos:
implicit Real sine(Real t), cosine(Real t) = {{sine:=0; cosine:=1; t:=0;}; {sine'=cosine, cosine'=-sine, t'=1}};. However, this isn't very robust due to limitations on using custom functions. For example,t=0 & sine(0)=0 & cosine(0)=1 & x=1-> [{x'=-(sine(t)),t'=1}triggers a Core error:In contrast,
t=0 & x=0 & xdot=1 -> [{x'=xdot, xdot'=-x, t'=1}]x<=1proves automatically. In my limited experience with implicit definitions, automation seems to perform worse in general, even when no errors are thrown. For instancet=0 & sine(0)=0 & cosine(0)=1 -> [{t'=1}@invariant((sine(t))^2 + (cosine(t))^2=1)]sine(t)<=1requires the invariant forAutoto succeed.)Probably extraneous detail: While running, the GUI shows "KeYmaera X 5.0.2 (no network)." at the bottom left.