The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Vincent,

  You should write a return clause `match e as e’ return match e’ with None 
=> True | Some t => P t end with ...` for the match on the option value, I 
guess. Coq cannot infer its type automatically. The error message is sadly 
misleading.

Best,
-- Matthieu

> Le 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.