Hello!

I’m trying to write a specification for a binary file format. The format can be expressed fairly tidily using an expression language, but the inductive expression definition contains a couple of lists and so needs a special induction principle. There’s a well-known tree example in the Coq codebase, and I used that as a guide. Unfortunately, the resulting Fixpoint is apparently ill-formed, but the suggested change would actually make the function ill-typed…

```
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import Coq.Init.Byte.
Require Import Coq.Unicode.Utf8_core.
Import ListNotations.
Section binaryExpressions.
Local Unset Elimination Schemes.
Inductive binaryExp : Set :=
| BiU32 : nat → binaryExp
| BiU64 : nat → binaryExp
| BiBytes : list byte → binaryExp
| BiUTF8 : list byte → binaryExp
| BiArray : list binaryExp → binaryExp
| BiUnspecified : nat → binaryExp
| BiRecord : list (string * binaryExp) → binaryExp.
Parameter P : binaryExp → Prop.
Parameter P_BiU32 : ∀ c, P (BiU32 c).
Parameter P_BiU64 : ∀ c, P (BiU64 c).
Parameter P_BiBytes : ∀ bs, P (BiBytes bs).
Parameter P_BiUTF8 : ∀ bs, P (BiUTF8 bs).
Parameter P_BiArray : ∀ es, Forall P es → P (BiArray es).
Parameter P_BiUnspecified : ∀ c, P (BiUnspecified c).
Parameter P_BiRecord : ∀ es, Forall P (map snd es) → P (BiRecord es).
Fixpoint binaryExp_ind (b : binaryExp) : P b :=
let
fix expForAll (e : list binaryExp) : Forall P e :=
match e as ex return (Forall P ex) with
| [] => @Forall_nil binaryExp P
| (x :: xs) => @Forall_cons binaryExp P x xs (binaryExp_ind x) (expForAll xs)
end
in
match b as bx return (P bx) with
| BiU32 c => P_BiU32 c
| BiU64 c => P_BiU64 c
| BiBytes bs => P_BiBytes bs
| BiUTF8 bs => P_BiUTF8 bs
| BiArray es => P_BiArray es (expForAll es)
| BiUnspecified c => P_BiUnspecified c
| BiRecord fs => P_BiRecord fs (expForAll (map snd fs))
end.
End binaryExpressions.
```

The error message is:

```
Recursive definition of binaryExp_ind is ill-formed.
In environment
binaryExp_ind : ∀ b : binaryExp, P b
b : binaryExp
fs : list (string * binaryExp)
expForAll : ∀ e : list binaryExp, Forall P e
e : list binaryExp
x : binaryExp
xs : list binaryExp
Recursive call to binaryExp_ind has principal argument equal to "x" instead of "fs".
Recursive definition is:
"λ b : binaryExp,
let
fix expForAll (e : list binaryExp) : Forall P e :=
match e as ex return (Forall P ex) with
| [] => Forall_nil P
| x :: xs => Forall_cons x (binaryExp_ind x) (expForAll xs)
end in
match b as bx return (P bx) with
| BiU32 c => P_BiU32 c
| BiU64 c => P_BiU64 c
| BiBytes bs => P_BiBytes bs
| BiUTF8 bs => P_BiUTF8 bs
| BiArray es => P_BiArray es (expForAll es)
| BiUnspecified c => P_BiUnspecified c
| BiRecord fs => P_BiRecord fs (expForAll (map snd fs))
end".
```

Note that `binaryExp_ind : ∀ b : binaryExp, P b`

, but the error message suggests passing a value `fs : list (string * binaryExp)`

to it…

Is there something I can do about this?