The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

I can't say what exactly is wrong with your approach. While trying to 
fix it, I got confused by the way it was written. Below is a working 
implementation written in a way that I vaguely understand. The first 
match return type annotation is optional. Coq is smart enough to figure 
that one out. The other annotations are not optional, AFAICT.


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.
    Definition Ret x := match x with Some e => P e | None => True end.
    Parameter HRec: forall l x,
        All
          (option t)
          Ret
          l ->
        P x ->
        P (Rec l x).

    Fixpoint induc (e : t) { struct e } : P e :=
        match e as e return P e with
        | Base => HBase
        | Rec l x =>
          let induc_rec :=
              fix induc_rec l : All (option t) Ret l :=
                match l with
                | nil => I
                | hd :: tl =>
                  conj
                  (match hd as hd return Ret hd with
                   | Some e => induc e
                   | None => I
                   end)
                  (induc_rec tl)
                end
          in
          HRec l x (induc_rec l) (induc x)
        end.
End Induc.


On 9/24/19 6:10 PM, Vincent Siles wrote:
> 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 
> <mailto: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
>  
> <mailto: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.