title: Decreasing argument (and what is a Program Fixpoint)
body: <p>Consider the following fixpoint:</p>
  
  <pre><code>Require Import Coq.Lists.List.
  Import ListNotations.
  
  Inductive my_type: Type:=
  | Left: my_type
  | Right: my_type
  .
  
  Fixpoint decrease (which: my_type) (left right: list my_type) : list my_type :=
  match which with
  | Left =&gt;
    match left with
    | [] =&gt; []
    | a::tl =&gt; decrease a tl right
    end
  | Right =&gt;
    match right with
    | [] =&gt; []
    | a::tl =&gt; decrease a left tl
    end
  end.
  </code></pre>
  
  <p>Coq rejects the following fixpoint because it can not guess the decreasing fixpoint (sometimes the <code>left</code> list looses its head, sometimes it is the <code>right</code> one).</p>
  
  <p>This <a href="https://stackoverflow.com/questions/33302526/well-founded-recursion-in-coq">answer</a> shows that one can solve this by using a <code>Program Fixpoint</code> and specifying a <code>{measure ((length left)+(length right))}</code>.</p>
  
  <p>My questions are: </p>
  
  <ul>
  <li>What is the difference between a regular <code>Fixpoint</code> and a <code>Program Fixpoint</code> ?</li>
  <li>Is it possible to explicit the decreasing argument in a regular <code>Fixpoint</code> ?</li>
  <li>What is the <code>Next Obligation</code> goal ?</li>
  </ul>