# Program Fixpoint decreasing on measure produces unsolvable goal

I have trouble understanding how to produce more sensible goal in the obligation

Require Import Coq.Program.Wf.
Require Import List.
Import ListNotations.

Inductive I :=
| Ibool : bool -> I
| Inested : list I -> I.

Fixpoint i_measure (i: I) : nat :=
match i with
| Ibool x => 1
| Inested x => 1 + list_sum (map i_measure x)
end.

Program Fixpoint foo (i: I) {measure (i_measure i)} : bool :=
match i with
| Ibool x => x
| Inested x => forallb (fun q => foo q) (rev x)
end.
Next Obligation.
(* x : list I *)
(* foo : forall i : I, i_measure i < i_measure (Inested x) -> bool *)
(* q : I *)
(* ============================ *)
(* i_measure q < i_measure (Inested x) *)



In this example i would like Coq to generate additional hypothesis, smth like

H: In q (rev x)


Are there some standard practices when dealing with problems of this kind?

The gallery of the Equations plugin (the spiritual successors of Program) has quite a few examples of patterns to handle this kind of problems. In your case rose trees contains a similar pattern as what you are looking for, albeit with map rather than forall. Still, we can mimick that:

Require Import Coq.Program.Wf.
Require Import List Lia.
Import ListNotations.

Program Fixpoint forall_In {A : Type} (l : list A) (f : forall (x : A), In x l -> bool) : bool :=
match l with
| nil => true
| cons x xs => (f x _) && (forall_In xs (fun x H => f x _))
end.
Next Obligation.
now constructor.
Qed.
Next Obligation.
now constructor.
Qed.

Lemma forall_In_spec {A : Type} (f : A -> bool) (l : list A) :
forall_In l (fun (x : A) (_ : In x l) => f x) = forallb f l.
Proof.
induction l ; cbn.
1: reflexivity.
now rewrite IHl.
Qed.

Section list_size.
Context {A : Type} (f : A -> nat).

Fixpoint list_size (l : list A) : nat :=
match l with
| nil => 0
| x :: xs => S (f x + list_size xs)
end.

Lemma In_list_size: forall x xs, In x xs -> f x < S (list_size xs).
Proof.
intros.
induction xs ; cbn in *.
1: easy.
destruct H as [->|?%IHxs].
all: lia.
Defined.
End list_size.
Transparent list_size.

Inductive I :=
| Ibool : bool -> I
| Inested : list I -> I.

Fixpoint i_measure (i: I) : nat :=
match i with
| Ibool x => 1
| Inested x => 1 + list_size i_measure x
end.

Program Fixpoint foo (i: I) {measure (i_measure i)} : bool :=
match i with
| Ibool x => x
| Inested x => forall_In (rev x) (fun q H => foo q)
end.
Next Obligation.
now apply In_list_size, in_rev.
Qed.


Alternatively, you can express the equivalent of forall_In in term of map, or define an even more general fold_In.