Stream: Coq users

Topic: Strange error (with unshelve and ssreflect)


view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 10:29):

Why would I get

The command has indeed failed with message:
Incorrect number of goals (expected 9 tactics, was given 11).

from Fail (unshelve apply: map_Forall_dec); refine _.?
Using unshelve eapply map_Forall_dec; try apply _. works fine.

A bit more context on a variant:

From stdpp Require Import fin_maps gmap strings.
Require Import ssreflect.
(* ...
Declare
*)
Axiom GlobDecl : Type.
Definition type_table : Type := gmap string GlobDecl.
Axiom complete_decl : type_table  GlobDecl  Prop.
Definition complete_type_table (te : type_table) :=
  map_Forall (fun _key d => complete_decl te d) te.

#[global] Instance complete_type_table_dec te : Decision (complete_type_table te).
Proof.
(* Uh ? *)
Fail (unshelve apply: map_Forall_dec); refine _. (* Incorrect number of goals (expected 1 tactic, was given 2). *)
unshelve eapply map_Forall_dec; try apply _.

About map_Forall_dec.
(*
map_Forall_dec :
∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 :
                                             ∀ A : Type,
                                               Lookup K A (M A))
  (H1 : ∀ A : Type, Empty (M A)) (H2 : ∀ A : Type, PartialAlter K A (M A))
  (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A))
  (EqDecision0 : EqDecision K),
  FinMap K M
  → ∀ (A : Type) (P : K → A → Prop),
      (∀ (i : K) (x : A), Decision (P i x))
      → ∀ m : M A, Decision (map_Forall P m)
*)

view this post on Zulip Gaëtan Gilbert (Sep 21 2021 at 10:48):

does Set Debug "backtrace" make it print an interesting backtrace? (-bt on the command line for older Coq)
can you minimize to remove the stdpp requires?


Last updated: Feb 06 2023 at 13:03 UTC