Program Fixpoint decreasing on measure produces unsolvable goal

Question

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?

Answer 1

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.