Recursion.v

(* Nope, not structurally decreasing *)
Fail Fixpoint f (x y : nat) :=
  match x with
  | O => O
  | S x' => f y x'
  end.

(* But looking at f, we can define its domain inductively.
   This is literally "the set of x and y for which f is defined",
   where each subterm of an [f_dom] term represents the arguments
   of recursive calls (which should therefore be in the domain).
 *)
Inductive f_dom : nat -> nat -> Type :=
| f_O y : f_dom O y
| f_S x' y : f_dom y x' -> f_dom (S x') y
.

(* For every x and y in its domain, f is defined. *)
Fixpoint f_aux (x y : nat) (h : f_dom x y) :=
  match h with
  | f_O y          (* (x, y) = (O, y)  *)
                => O
  | f_S x' y h'    (* x, y = (S x', y),
                      and (y, x') is in the domain of f *)
                => f_aux y x' h'
  end.

(* Every x and y is in the domain of f *)
Theorem f_dom_all : forall x y, f_dom x y.
Proof.
  (* By induction on (x + y) or something. *)
Admitted.

(* So f is defined everywhere. *)
Definition f (x y : nat) := f_aux x y (f_dom_all x y).