The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Oh, for the record I'm using Coq 8.9.1 installed from opam.

Le mar. 24 sept. 2019 à 17:41, Vincent Siles <vincent.siles AT ens-lyon.org> a écrit :

Hi !

I'm facing an somehow complex inductive type, for which I have to write the induction scheme by hand. Here is a stripped down example of what I'm doing:

Require Import List.

Inductive t : Set :=
| Base : t
| Rec : list (option t) -> t -> t
.

Section All.
    Variables (T: Set) (P: T -> Prop).

    Fixpoint All (l : list T) : Prop :=
        match l with
        | nil => True
        | hd :: tl => P hd /\ All tl
        end.
End All.

Section Induc.
    Parameter P: t -> Prop.
    Parameter HBase : P Base.
    Parameter HRec: forall l x,
        All
          (option t)
          (fun x => match x with Some e => P e | None => True end)
          l ->
        P x ->
        P (Rec l x).

    Fixpoint induc (e : t) { struct e } : P e :=
        match e with
        | Base => HBase
        | Rec l x => HRec l x
                ((fix induc_rec l := match l with
                   | nil => I
                   | hd :: tl =>
                           conj (match hd with
                                 | Some e => induc e  (* error here *)
                                 | None => I
                                 end) (induc_rec tl)
                end) l) (induc x)
        end.
End Induc.

Coq complains that:

In environment
induc : forall e : t, P e
e : t
l : list (option t)
x : t
induc_rec : list (option t) -> True
l0 : list (option t)
hd : option t
tl : list (option t)
e0 : t
The term "induc e0" has type "P e0" while it is expected to have type
 "?P@{l0:=l; l:=l0; h0:=Some e0}" (cannot instantiate
"?P" because "e" is not in its scope: available arguments are
"induc" "e" "l" "x" "induc_rec" "l" "hd" "tl" "Some e").

I'm still investigating, but I think I need some external help on that one :D

Best regards,

V.