Require Import Coq.Program.Tactics.

Inductive A :=
  | init : A
  | ofB : B -> A
  | op : A -> A
with B :=
  | ofA : A -> B
  | liftedOp : B -> B
.

Notation "'liftedOp b" := (ofA (op (ofB b))) (at level 0).

Fixpoint sizeA a :=
  match a with
  | init => 1
  | ofB b => 1 + sizeB b
  | op a' => 1 + sizeA a'
  end
with sizeB b :=
  match b with
  | ofA a => 1 + sizeA a
  | liftedOp b' => (* 1 + sizeB ('liftedOp b) = *) 4 + sizeB b'
  end
.

Lemma sizeOk : forall b, sizeB ('liftedOp b) < sizeB (liftedOp b).
firstorder.
Qed.

(*
Fixpoint fA (a : A) : unit
with fB (b : B) : unit.
- pose (a' := a).
  destruct a.
  + exact tt.
  + exact (fB b).
  + exact (fA a).
- pose (b' := b).
  destruct b.
  + exact (fA a).
  + exact (fB ('liftedOp b)).
(* Error:
Error:
Recursive definition of fB is ill-formed.
In environment
fA : A -> unit
fB : B -> unit
b : B
b0 : B
Recursive call to fB has principal argument equal to "'liftedOp (b0)" instead
of "b0".
Recursive definition is:
"fun b : B =>
 let b' := b in
 match b as b0 return (let b'0 := b0 in unit) with
 | ofA a => let b'0 := ofA a in fA a
 | liftedOp b0 => let b'0 := liftedOp b0 in fB 'liftedOp (b0)
 end".
*)
Defined.
*)



(*
(* Error: Only structural decreasing is supported for a non-Program Fixpoint *)
Fixpoint fA (a : A) {measure (sizeA a)} : unit
with fB (b : B) {measure (sizeB b)} : unit.
- pose (a' := a).
  destruct a.
  + exact tt.
  + exact (fB b).
  + exact (fA a).
- pose (b' := b).
  destruct b.
  + exact (fA a).
  + exact (fB ('liftedOp b)).
Defined.
*)



(*
Program Fixpoint fA (a : A) : unit := _
with fB (b : B) : unit := _.
Obligation 1 of fA.
- pose (a' := a).
  destruct a.
  + exact tt.
  (* Error: The reference fB was not found in the current environment. *)
  + exact (fB b).
  + exact (fA a).
Obligation 1 of fB.
- pose (b' := b).
  destruct b.
  + exact (fA a).
  + exact (fB ('liftedOp b)).
Defined.
*)



(*
(* Error: Well-founded fixpoints not allowed in mutually recursive blocks *)
Program Fixpoint fA (a : A) {measure (sizeA a)} : unit := _
with fB (b : B) {measure (sizeB b)} : unit := _.
Obligation 1 of fA.
- pose (a' := a).
  destruct a.
  + exact tt.
  + exact (fB b).
  + exact (fA a).
Obligation 1 of fB.
- pose (b' := b).
  destruct b.
  + exact (fA a).
  + exact (fB ('liftedOp b)).
Defined.
*)





(* Of course, I can just give the size as an argument and then it works.
But this is already annoying in this case and in the general case,
I'd need the "size" to be a tree (with the same arities as the arities
of my constructors)... *)

Fixpoint fA (a : A) {sa} {Hsa : sa = sizeA a} : unit
with fB (b : B) {sb} {Hsb : sb = sizeB b} : unit.
- pose (a' := a).
  destruct a; destruct sa; try discriminate; simpl in Hsa; injection Hsa as Hsa'.
  + exact tt.
  + exact (fB b sa Hsa').
  + exact (fA a sa Hsa').
- pose (b' := b).
  destruct b; destruct sb; try discriminate; simpl in Hsb; injection Hsb as Hsb'.
  + exact (fA a sb Hsb').
  + exact (fB ('liftedOp b) sb Hsb').
Defined.