I’m often doing a lot of bookkeeping work, implementing "better" induction schemes for some types, as follows:

```
Inductive expr :=
| e_nat (n : nat)
| e_tuple (l : list expr)
| ….
```

What we want is an induction scheme with cases like `forall (e : expr) (l : list expr), Forall P l -> P e -> P (e_tuple (e :: l))`

, but Coq generates a scheme with a case `forall (l : list expr), P (e_tuple l)`

. In http://adam.chlipala.net/cpdt/html/InductiveTypes.html#lab32, Adam Chlipala writes a bit about this.

There has been some investigation of this problem in a general context (not specific to Coq, but still regarding inductive types) in this paper https://www.cs.appstate.edu/~johannp/20-fossacs.pdf and some work using MetaCoq https://arxiv.org/abs/2006.15135. The first paper proposes a general principle which the authors claim "inducts over all of the structured data present", the second paper was presented at the Coq Workshop 2020 (https://coq-workshop.gitlab.io/2020/).

I wish Coq were extended in some easy-to-use way, with which appropriate induction schemes could be generated automatically. For example `Scheme expr_deep_rect := Deep Induction for expr Sort Type.`

and maybe first importing a plug-in. Are other people interested in something like this? Do some of you know of other work on this topic? I haven’t yet read the papers closely nor looked closely at the plugin given in the second paper I linked. I might work on this, during this summer break.

To be explicit: The automatically generated induction scheme `expr_rect`

has type

```
forall P : expr -> Type,
(forall n : nat, P (e_nat n)) ->
(forall l : list expr, P (e_prod l)) ->
forall e : expr, P e
```

but I’d like it to have type

```
forall P : expr -> Type,
(forall n : nat, P (e_nat n)) ->
(forall l : list expr, Forall P l -> P (e_prod l)) ->
forall e : expr, P e
```

or

```
forall P : expr -> Type,
(forall n : nat, P (e_nat n)) ->
(P (e_prod nil)) ->
(forall (e : expr) (l : list expr),
P e -> P (e_prod l) -> P (e_prod (cons e l))) ->
forall e : expr, P e
```

or somesuch. It’s possible to prove such theorems using the automatically generated induction principle using the following construction:

```
Section expr_rect.
Variable (P : expr -> Prop).
Hypothesis H_nat : forall n, P (e_nat n).
Hypothesis H_prod : forall l, Forall P l -> P (e_prod l).
Fixpoint expr_rect' (e : expr) : P e :=
match e with
| e_nat n => H_nat n
| e_prod l =>
H_prod l ((fix e_prod_fix (l : list expr) : Forall P l :=
match l with
| nil => (Forall_nil P)
| cons hd tl => (Forall_cons hd (expr_rect' hd) (e_prod_fix tl))
end
) l)
end.
End expr_rect.
```

Yes, everybody wants this as soon as they add list foo to their foo :-). The alternative is Inductive foo … with foos := (* a specialized copy of list foo *)

Coq-elpi might be suitable to implement this.

Otherwise the best way I know is this: https://github.com/Blaisorblade/dot-iris/blob/master/theories/Dot/syn/syn.v#L652

I don't think this is very hard to implement, it just needs to be done ©

There are several equivalent ways of phrasing the inductive property, and the one from the linked paper is slightly problematic in the context of induction because we need to invent a predicate

I arrived at a point in my project, where automatic generation of deep induction schemes seems unavoidable. To avoid having to automatically invent predicates, I'll probably only generate "theorems" and leave the filling in to the user. Will probably be incompatible with the 'induction' tactic.

I may be missing something, but aren't you asking for the first half of what's described in this paper? https://drops.dagstuhl.de/opus/volltexte/2019/11084/

I feel immensely stupid. Thank’s for pointing this out. When I first came across the paper I skimmed it and thought "Well, that only concerns itself with equality. Not my use-case."

For the record: derive comes shipped with coq-elpi. Usage example:

```
From elpi.apps Require Import derive.
derive list.
derive
Inductive expr :=
| ...
About expr.induction.
```

Hello @Columbus , are you saying Coq-Elpi's derive works fine in your use case? (I did not get much feedback so far)

CC @Vincent Laporte , is your data type of expressions like this one?

Oh, I see you already reported a few issues/whishes, thanks!

(I've fixed #262 in master, I can make a minor release if it helps)

Hey. At first I was surprised, that I had to `derive list`

and other types from the stdlib. I also couldn't apply the generated `.induction`

schema using the `induction`

tactic, and applying `.is_*_full`

was also necessary (but I don’t know whether this is the intended usage).

But oh my! The induction principle does precisely what I wanted. Automagically. This is just great!

I see:

- I guess I could add a file such that
`From elpi.apps Require Import derive.stdlib`

brings you the principles on most of the data types that come with Coq's stdlib - Yes, the induction principles require an extra argument which is also synthesized. I "specialize" them only when I use them for the equality tests

I make two issues about these, thanks for testing!

Currently I struggle with deriving the induction schema for quite a large predicate (~15 cases, some of them having `Forall2`

as premises), but I'll try to minimize the problem and get back to you.

Enrico Tassi said:

(I've fixed #262 in master, I can make a minor release if it helps)

Thanks. I'll use `opam pin`

for now.

Enrico Tassi said:

is your data type of expressions like this one?

Exactly. Expressions are made of operators applied to arguments: `Inductive expr := App of operator & seq expr.`

There are also commands that sometimes contain basic blocks: `Inductive command := Assign of var & expr | Loop of seq command & expr & seq command.`

Last updated: Jun 24 2024 at 01:01 UTC