# Bifurcations and KeYmaera X  -- The 1D Saddle-node Birfurcation

--
Author: Nathan Fulton
Category: Automated Reasoning
Date Published: 07-25-2017
--

This note describes how to leverage bifurcation results in the KeYmaera X theorem prover.
The [Saddle-node bifurcation](https://en.wikipedia.org/wiki/Saddle-node_bifurcation) is 
a canonical bifurcation in a continuous dynamical system.
The simplest example of a Saddle-node bifurcation is a one dimensional system with one parameter `r`;
as this parameter varies, the system's equilibrium point changes.

This note will describe how to write a computer-checked proof (using the KeYmaera X prover) 
that the system `x' = r + x^2` has at least one equilibrium point for every non-positive choice of `r`.
Explore the full proof in our web UI for KeYmaera X on [web.keymaerax.org](https://web.keymaerax.org/show/bifurcations/saddle-nodes/1D/combined.kya),
or download the source code from [KeYmaera X projects repository](https://github.com/LS-Lab/KeYmaeraX-projects/tree/master/bifurcations/saddle-nodes/1D).
If you're unfamiliar with KeYmaera X, you may want to work through the Learner's Mode tutorial by creating a new account on [web.keymaerax.org](https://web.keymaerax.org)
before continuing.

### The System

In KeYmaera X, we can express the one dimensional saddle node as a simple reachability property:

    r <= 0 -> \exists f (x=f -> [{x' = r + x^2}]x=f)

This property states that for every `r <= 0`, there is a fixed point of the system `x' = r + x^2`.
I.e., for every non-positive choice of `r`, there an initial value `x_0 = f` such that
along **every** flow of the ODE `x' = r + x^2`, `x=f` is always true.
More concisely, for every non-positive choice of the parameter `r` there exists an equilibrium point `f` of `x' = r + x^2`.

As we vary the parameter `r`, the equilibrium point of this system will change.

  * At `r<0`, there is an equilibrium point at `f = -\sqrt(-r)`.
  * At `r=0`, there is an equilibrium point at `f = 0`.


### The Proof

We cannot prove this property for a single choice of `r`; the value of `f` will be different when `r<0` than when `r=0`.
Therefore, any proof that begins by instantiating the existential `\exists f` will fail!
Instead, the proof needs to split into two cases at the bifurcation point.

I do this by introducing a lemma `r<0 | r=0` and then splitting the proof along this disjunction.
First, we cut in the disjunction lemma and prove it follows from our existing assumption that `r <= 0`.

            *
    QE --------------------       ---------------------------------------------------------
       r<=0 |- ..., r<0|r=0       r<=0, r<0|r=0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)
    --------------------------------------------------------------------------------------- cut({`r<0 | r=0`})
                              r <= 0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)

On the right branch, the proof now decomposes along the bifurcation point by splitting the disjunction:

    r<0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)     r<0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)
    ----------------------------------------------------------------------------------------------- orL(-1)
                  r<0|r=0       |- \exists f (x=f -> [{x' = r + x^2}]x=f)
    ----------------------------------------------------------------------------------------------- hideL(-1)
                  r<=0, r<0|r=0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)

We choose the appropriate instantiation of `f` for each value of `r`.

The right subgoal is easiest:

         *
    --------------------------------------------- implyR(1); ODE
    r<0 |- x=0 -> [{x' = r + x^2}]x=0
    --------------------------------------------- existsR({`0`}, 1)
    r<0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)

Proving that `x=0` is an equilibrium point when `r<0` is a job for differential ghosts; fortunately,
the ODE tactic already automates this proof. If you're curious about how to do this proof by hand,
see my [note on differential ghosts](http://nfulton.org/2017/01/14/Ghosts/).

For the `r<0` case we have to do a bit more work in order to express the quantity `-\sqrt(-r)` in KeYmaera X.
Introduce a value `s = \sqrt(-r)` via an **arithmetic ghost** and then phrase the equilibrium point in terms of
this new value `s`.

                          *
    --------------------------------------------------------------- implyR(1); ODE
    r<0, r=-s*s           |- x=-s -> [{x' = r + x^2}]x=-s
    --------------------------------------------------------------- existsR({`-s`}, 1)
    r<0, r=-s*s           |- \exists f (x=f -> [{x' = r + x^2}]x=f)
    --------------------------------------------------------------- existsL(-2)
    r<0, \exists s r=-s*s |- \exists f (x=f -> [{x' = r + x^2}]x=f)
    --------------------------------------------------------------- cut({`\exists s r=-s*s`})
    r<0                   |- \exists f (x=f -> [{x' = r + x^2}]x=f)

The "cut show" branch just involves hiding everything except the valid cut `\exists s r=-s*s`.

The by-hand proof for this equilibrium point is slightly more difficult than those covered in
my [note on differential ghosts](http://nfulton.org/2017/01/14/Ghosts/). Here's the answer,
which you can verify using the process outlined in my note on ghosts:

    dG({`{y'=(-(x-s))*y}`}, {`y*(x+s)=0&y>0`}, 1); 
    existsR({`1`}, 1); 
    boxAnd(1) ; andR(1) <(
      dI(1)
      ,
      dG({`{z'=(x-s)/2*z}`}, {`z^2*y=1`}, 1);
      existsR({`1`}, 1); 
      dI(1)
    )

### Conclusion

Most bifurcation results are very simple to leverage in KeYmaera X:

 * Cut in a disjunction that describes the bifurcation; each "side" of the
   bifurcation should be a separate term in the disjunction.
 * Split the proof into sub-cases by splitting the disjunction.
 * Prove each sub-case separately. This step is the most difficult, but we're
   working on providing more and more ODE prover automation.

<hr/>

### Appendix: The whole proof

I've avoided using `ODE` tactic in this proof to demonstrate how the entire differential ghost argument works:

    /* Move r <= 0 to the antecedent */
    implyR(1); 
    /* Introduce and prove r=0|r<0; hide assumption that r<=0 */
    cut({`r=0|r < 0`}) <(hideL(-1), hideR(1) ; QE); 
    /* Split the proof. */
    orL(-1) <(
     
      /* CASE 1: r=0 */
      existsR({`0`}, 1);                    /* choose f=0 */
      implyR(1); 
      dG({`{y'=-x*y}`}, {`y*x=0&y>0`}, 1);  /* x=0 <-> \exists y (y*x=0&y>0) */
      existsR({`1`}, 1);                    /* choose arbitrarily y != 0; e.g. y=1 */
      /* Consider y*x=0 and y>0 differential invariants separately */
      boxAnd(1); andR(1) <(
        /* y*x=0 is differentially inductive because:
           (yx)'=0 <-> y'x + x'y = 0 <-> -x*y^2 + r + x^2 = 0
           (recall: r=0)
        */
        dI(1)
        ,
        /* y>0 case needs an extra cut. See note on differential ghosts. */
        dG({`{z'=x/2*z}`}, {`z^2*y=1`}, 1); 
        existsR({`1`}, 1); 
        dI(1)
      )

      ,

      /* CASE 2: r<0 */
      /* introduce new variable s = sqrt(-r) and prove s exists. */
      cut({`\exists s r=-s*s`}) <(nil, hideR(1) ; QE);
      /* Some cleanup work about s */
      existsL(-2) ; existsR({`-s`}, 1) ; implyR(1) ; 
      /* See not on differential ghosts. */
      dG({`{y'=(-(x-s))*y}`}, {`y*(x+s)=0&y>0`}, 1) ; existsR({`1`}, 1) ; 
      boxAnd(1) ; andR(1) <(
        dI(1),
        dG({`{z'=(x-s)/2*z}`}, {`z^2*y=1`}, 1) ; existsR({`1`}, 1) ; dI(1)
      )
    )