The Coq mailing list

[Jerome Hugues <jhugues AT andrew.cmu.edu>]

Thanks Jason,

 

You pointed to the right direction. Obviously the type checker was confused and I now understand how to interpret it.

 

For the record, here is the final working solution

 

(*************)

 

From Coq Require Import List.

 

Set Implicit Arguments.

Set Asymmetric Patterns.

 

Inductive componentInstance :=

    | component_instance : nat -> list subcomponentInstance -> componentInstance

with subcomponentInstance :=

    | subcomponent_instance : nat -> componentInstance -> subcomponentInstance.

 

Section All.

 

    Variable T : Set.

    Variable P : T -> Prop.

 

    Fixpoint All (ls : list T) : Prop :=

      match ls with

        | nil => True

        | h :: t => P h /\ All t

      end.

 

  End All.

 

Section componentInstance_ind'.

 

  Variable Pc : componentInstance -> Prop.

 

  Definition Ps (s : subcomponentInstance) : Prop :=

    match s with

    | subcomponent_instance _ c => Pc c

    end.

 

  Variable Pls : list subcomponentInstance -> Prop.

 

  Hypothesis component_case : forall (n : nat) (ls : list subcomponentInstance),

    All Ps ls -> Pc (component_instance n ls).

 

Fixpoint componentInstance_ind' (c : componentInstance) : Pc c :=

  match c return Pc c with

  | component_instance n ls =>

    component_case n ls

    ((fix subcomponentInstance_ind (ls : list subcomponentInstance) : All (Ps) (ls) :=

      match ls return All _ ls  with

      | nil => I

      | subcomponent_instance _ c' :: ls' =>

          conj (componentInstance_ind' c')

               (subcomponentInstance_ind ls')

      end)

    ls)

end.

 

End componentInstance_ind'.

 

From: <coq-club-request AT inria.fr> on behalf of Jason Gross <jasongross9 AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Friday, January 29, 2021 at 7:57 PM
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Type error for user-defined induction principle for inductive type

 

Have not tried running the code, but try `match ls return All _ ls with` instead of `match ls with`.  The error message that you got is saying "I don't know how to figure out what to apply "All" to to get "True"".  Another way of phrasing this issue is that when you write "match ls with ..." it doesn't know whether you want the type of the branches to be in terms of `ls`, or to be in terms of the branch of the match.

Best,

Jason

 

 

On Fri, Jan 29, 2021 at 5:22 PM Jerome Hugues <jhugues AT andrew.cmu.edu> wrote:

Thanks for the suggestion

I tried this, but this still produces the same error on nil => I (see rewrite below)
The error changed to

The term "I" has type "True" while it is expected to have type
"All Ps ?l@{ls:=ls0; l0:=nil}".

which is a similar error message with different variable names due to the renaming

Fixpoint componentInstance_ind' (c : componentInstance) : Pc c :=
  match c with
  | component_instance n ls =>
    component_case n ls
    ((fix subcomponentInstance_ind (ls : list subcomponentInstance) : All (Ps) (ls) :=
      match ls with
      | nil => I (* True *) (* All Ps nil *)
      | subcomponent_instance _ c' :: ls' => (componentInstance_ind' c') /\
          (subcomponentInstance_ind ls')
      end)
    ls)
end.

On 1/29/21, 5:14 PM, "coq-club-request AT inria.fr on behalf of Gaëtan Gilbert" <coq-club-request AT inria.fr on behalf of gaetan.gilbert AT skyskimmer.net> wrote:

    Didn't check but I think

         ((fix subcomponentInstance_ind (lsi : list subcomponentInstance) : All (Ps) (ls) :=

    should be ... : All Ps lsi, not ... : All Ps ls

    Then I would just shadow ls to reduce typo possibilities

    Gaëtan Gilbert

    On 29/01/2021 22:58, Jerome Hugues wrote:
    >      ((fix subcomponentInstance_ind (lsi : list subcomponentInstance) : All (Ps) (ls) :=
    >