coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Type error for user-defined induction principle for inductive type

From: Jerome Hugues <jjhugues AT sei.cmu.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Type error for user-defined induction principle for inductive type
Date: Fri, 29 Jan 2021 22:21:21 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jjhugues AT sei.cmu.edu; spf=Pass smtp.mailfrom=jjhugues AT sei.cmu.edu; spf=None smtp.helo=postmaster AT taper.sei.cmu.edu
Dkim-filter: OpenDKIM Filter v2.11.0 taper.sei.cmu.edu 10TMLQBK010668
Ironport-phdr: 9a23:jI2kAx3/r2iO+geYsmDT+DRfVm0co7zxezQtwd8ZseMWKPad9pjvdHbS+e9qxAeQG9mCurQf0aGP6fqoGTRZp8rY7zZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq80bjZFsJ6ovxRfFv2VEd/pLzm9sOV6fggzw68it8JNh6Shcp+4t+8tdWqjmYqo0SqBVAi47OG4v/s3rshfDTQqL5nQCV2gdjwRFDQvY4hzkR5n9qiT1uPZz1ymcJs32UKs7WS++4KdxSR/nkzkIOjgk+2zKkMNwjaZboBW8pxxjxoPffY+YOOZicq7bYNgXQ3dKUMRMWCxbGo6yb5UBAfcdPehWrIf9qVkBrRqiCgejC+zi0SNIiWTz3aEmz+gtDQPL0Qo9FNwOqnTUq9D1Ob8WX++r1qnIyjDDYO1L0jn/9YjIfQ0hru+XXbltdsfRy0svFwPYjlWftIzqISiV2/8Ws2eF7upsT/6gi2s6qw1rvDeg29osh5DPi4kIxV/K6T93z5wpJd2kVkF7e9ikHYNRuiyGKYd7Rt4vTm9ntSs7zrALu4C2cSsWxJg5yRPSav6KfouW7hzjW+ufLjZ1in1ldr6hiBi88Uaux/DhWse01ltBsylLksHUu3wQ2BHe6NKLR/lj8ku7xzqC1x7f5vtZLU01jabXNoItzqQxm5ccq0jPADP6lUvsgKOLa0ko4vWk5uvlb7n8pJKQKZV4hh/+P6gwgMCyDuU1Pw4TVGaB4+u8zqfs/UjhTbVKkPI2lq7ZvYjGJcsBvq62HRVV3pw46xmhDjeqysgXnXwaLF5fZh2IkpXpN0nPIPD+E/i/n0yhnCpkyv3EJLHsAIvBImLdnLrhY7px8VNQxQsrwdBa/Z1UC7UBIPzpWk/2sdzVFh05Mw60w+b6B9V9y50RWXmUD6+CLqzSsEWE6f4qI+mRfoMapivyK+U96/70kXA5gUMdfbWu3ZYPdH+4Ge1mL1yFbnron9cOCnwHvhE+TezvkF2NSyRfZ3e0X6Im5zE0EpiqDYnZRtPlvLvUliy8B9hdYn1MIlGKC3bhMYueEb9YYyWLZ8RljzYsVL67SoZn2wv45yHgzL8yDOfO/SgV/bL+28V4/KWHlxMy6DNpAt+1yGyMCWpxgyUFSyJgj/M3mlB01lrWifswuPdfD9EGv6oYADd/DobVyqlBM/63XwvAetmTT1P/GYe9DDB3RdcshdICfhQkQonwvlX4xyOvRoQtufmTHpVtqfDH0nm3LMNgjXvKyft51gR0co50LWSjw5VH2U3TCorOyhTLi6+yeL5axyPMsmyG0CyDsFwKCAM=

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) :=
>

Re: [Coq-Club] Type error for user-defined induction principle for inductive type, Jerome Hugues, 01/29/2021