The Coq mailing list

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

Jan's version seems closer to mine but I'll try both, thanks !

V.

Le mar. 24 sept. 2019 à 18:28, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> a écrit :

Maybe you could use this one ...

Best,

D.

------------------------

Require Import List Extraction.

Unset Elimination Schemes.

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

Set Elimination Schemes.

Section t_rect.

  Let R t t' :=
    match t' with
      | Base     => False
      | Rec l t' => In (Some t) l \/ t = t'
    end.

  Let Fixpoint R_wf t : Acc R t.
  Proof.
    destruct t as [ | l t ]; constructor; simpl; intros x Hx.
    + destruct Hx.
    + destruct Hx as [ Hx | Hx ].
      * induction l as [ | [ y | ] l IHl ].
        - destruct Hx.
        - destruct Hx as [ | Hx ].
          ++ generalize (R_wf y); inversion H; trivial.
          ++ apply IHl, Hx.
        - destruct Hx as [ | Hx ].
          ++ discriminate H.
          ++ apply IHl, Hx.
      * generalize (R_wf t); subst; trivial.
  Qed.
 
  Variables (P : t -> Type)
            (HP0 : P Base)
            (HP1 : forall l t, (forall k, In (Some k) l -> P k) -> P t -> P (Rec l t)).

  Fixpoint t_rect t : P t.
  Proof.
    generalize (R_wf t).
    revert t.
    refine (fix loop x Hx { struct Hx } := _).
    destruct x as [ | l t ].
    + apply HP0.
    + apply HP1.
      2: apply loop, (Acc_inv Hx); simpl; right; trivial.
      intros k Hk; apply loop, (Acc_inv Hx); simpl; left; trivial.
  Qed.

End t_rect.

Recursive Extraction t_rect.

---

De: "Vincent Siles" <vincent.siles AT ens-lyon.org>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mardi 24 Septembre 2019 18:10:46
Objet: Re: [Coq-Club] Need help for manual induction scheme definition

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.