Fix rocq-prover#4416: - Incorrect "Error: Incorrect number of goals"

In `Ftactic` the number of results could desynchronise with the number
of goals when some goals were solved by side effect in a different
branch of a `DISPATCH`.

See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).

Author: aspiwack

lib/monad.ml

@@ -64,6 +64,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 
@@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct
       | a::b::l -> f a >> f b >> iter f l
 
 
+    let rec map_filter f = function
+      | [] -> return []
+      | a::l ->
+        f a >>= function
+        | None -> map_filter f l
+        | Some b ->
+          map_filter f l >>= fun filtered ->
+          return (b::filtered)
 
     let rec fold_left2 r f x l1 l2 =
       match l1,l2 with

lib/monad.mli

@@ -66,6 +66,9 @@ module type ListS = sig
       its second argument in a tail position. *)
   val iter : ('a -> unit t) -> 'a list -> unit t
 
+  (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*)
+  val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t
+
 
   (** {6 Two-list iterators} *)
 

proofs/proofview.ml

@@ -1016,6 +1016,10 @@ module Goal = struct
     in
     tclUNIT (CList.map_filter map step.comb)
 
+  let unsolved { self=self } =
+    tclEVARMAP >>= fun sigma ->
+    tclUNIT (not (Option.is_empty (advance sigma self)))
+
   (* compatibility *)
   let goal { self=self } = self
 

proofs/proofview.mli

@@ -466,6 +466,10 @@ module Goal : sig
   (** Recover the list of current goals under focus, without evar-normalization *)
   val goals : [ `LZ ] t tactic list tactic
 
+  (** [unsolved g] is [true] if [g] is still unsolved in the current
+      proof state. *)
+  val unsolved : 'a t -> bool tactic
+
   (** Compatibility: avoid if possible *)
   val goal : [ `NF ] t -> Evar.t
 

tactics/ftactic.ml

@@ -29,13 +29,28 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
   | Uniform x ->
     (** We dispatch the uniform result on each goal under focus, as we know
         that the [m] argument was actually dependent. *)
-    Proofview.Goal.goals >>= fun l ->
-    let ans = List.map (fun _ -> x) l in
+    Proofview.Goal.goals >>= fun goals ->
+    let ans = List.map (fun g -> (g,x)) goals in
     Proofview.tclUNIT ans
-  | Depends l -> Proofview.tclUNIT l
+  | Depends l ->
+    Proofview.Goal.goals >>= fun goals ->
+    Proofview.tclUNIT (List.combine goals l)
+  in
+  (* After the tactic has run, some goals which were previously
+     produced may have been solved by side effects. The values
+     attached to such goals must be discarded, otherwise the list of
+     result would not have the same length as the list of focused
+     goals, which is an invariant of the [Ftactic] module. It is the
+     reason why a goal is attached to each result above. *)
+  let filter (g,x) =
+    g >>= fun g ->
+    Proofview.Goal.unsolved g >>= function
+    | true -> Proofview.tclUNIT (Some x)
+    | false -> Proofview.tclUNIT None
   in
   Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
-  Proofview.tclUNIT (Depends (List.concat l))
+  Proofview.Monad.List.map_filter filter (List.concat l) >>= fun filtered ->
+  Proofview.tclUNIT (Depends filtered)
 
 let nf_enter f =
   bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))