Ill-formed recursive definition using `let fix`

Using Coq
1

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?

2

I guess the subterm property doesn’t go through map snd.
If you do a separate let fix for it it works:


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
  let
    fix expForAllSnd (e : list (string * binaryExp)) : Forall P (map snd e) :=
      match e as ex return (Forall P (map snd ex)) with
      | []        => @Forall_nil binaryExp P
      | ((_,x) :: xs) => @Forall_cons binaryExp P x (map snd xs) (binaryExp_ind x) (expForAllSnd 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 (expForAllSnd fs)
     end.
3

Ah, thank you! Bit of an odd one. :slightly_smiling_face: