Stream: Coq users

Topic: Deep Induction Schemes

Stéphane Desarzens (Jun 16 2021 at 16:06):

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.

Paolo Giarrusso (Jun 16 2021 at 23:59):

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 *)

Paolo Giarrusso (Jun 16 2021 at 23:59):

Coq-elpi might be suitable to implement this.

Paolo Giarrusso (Jun 17 2021 at 00:02):

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

Pierre-Marie Pédrot (Jun 17 2021 at 12:03):

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

Pierre-Marie Pédrot (Jun 17 2021 at 12:04):

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

Stéphane Desarzens (Jul 10 2021 at 21:02):

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.

Christian Doczkal (Jul 10 2021 at 21:16):

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/

Stéphane Desarzens (Jul 11 2021 at 08:28):

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.

Enrico Tassi (Jul 11 2021 at 12:48):

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

Enrico Tassi (Jul 11 2021 at 12:51):

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

Enrico Tassi (Jul 11 2021 at 12:53):

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

Enrico Tassi (Jul 11 2021 at 13:16):

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

Stéphane Desarzens (Jul 11 2021 at 13:25):

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!

Enrico Tassi (Jul 11 2021 at 13:31):

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!

Stéphane Desarzens (Jul 11 2021 at 13:50):

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.

Stéphane Desarzens (Jul 11 2021 at 13:54):

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.

Vincent Laporte (Jul 13 2021 at 13:36):

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: Oct 13 2024 at 01:02 UTC