The Coq mailing list

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

I tried to prove it using tactics and check the proof term and that's what is happening, but I can't managed to replicate it, now I get:

In environment
induc : forall u : t, P u
u : t
l : list (option t)
x : t
induc_rec :
forall l : list (option t),
All (option t)
  (fun x : option t => match x with
                       | Some x0 => P x0
                       | None => True
                       end) l
l0 : list (option t)
hd : option t
tl : list (option t)
The term
 "match hd as o return match o with
                       | Some x0 => P x0
                       | None => True
                       end with
  | Some e => induc e
  | None => I
  end" has type "match hd with
                 | Some x0 => P x0
                 | None => True
                 end" while it is expected to have type
"?A@{l0:=l; l:=l0}" (unable to find a well-typed instantiation for
"?A": cannot ensure that "Type" is a subtype of "Prop").

I guess I'll go with the tactic solution, it's a bit more readable anyway :D

PS: sorry for the dup, first answer got sent with the wrong address...

Le mar. 24 sept. 2019 à 17:50, Matthieu Sozeau <matthieu.sozeau AT inria.fr> a écrit :

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.