derive should generate functoriality properties for param1 translation of non-inductive predicates

[adelaett]

ocaml version: 4.14.0 Coq version : 8.16.1 coq-elpi version: 1.15.6 I'm trying to synthesize induction principles for terms builds using Autosubst using coq-elpi's derive. Here is a minimal example with the same issues:

From elpi.apps Require Import derive.
Set Uniform Inductive Parameters.

Elpi derive bool.

Definition annotation (T: Type) := T.
Inductive term :=
| Dummy (x: bool)
| Lam (t: annotation term).

Here is the induction principle that Coq generates

term_ind : forall P : term -> Prop,
       (forall x : bool, P (Dummy x)) ->
       (forall t : annotation term, P t -> P (Lam t)) -> forall t : term, P t

However, elpi's derive fails because of the annotation. Here is what I've tried:

Fail Elpi derive annotation.

Elpi derive.isK term.
Elpi derive.map term.
Elpi derive.projK term.
Fail Elpi derive.param1 term.

Is there is a way to either:

• support user input for what elpi.derive cannot synthesize
• support reduction when building the induction principle

Trace for Elpi derive annotation:

The elpi tactic/command derive failed without giving a specific error
message. Please report this inconvenience to the authors of the
program.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Vernacextend.vtdefault.(fun) in file "vernac/vernacextend.ml", line 136, characters 29-33
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 205, characters 24-69
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml", line 255, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 253, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2177, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 964, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2319, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2420, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.finish in file "stm/stm.ml", line 2431, characters 12-50
Called from Stm.process_transaction in file "stm/stm.ml", line 2691, characters 22-45
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.add in file "stm/stm.ml", line 2790, characters 8-50
Called from Dune__exe__Idetop.add in file "ide/coqide/idetop.ml", line 89, characters 25-60
Called from Dune__exe__Idetop.eval_call.interruptible in file "ide/coqide/idetop.ml", line 496, characters 12-15
Called from Xmlprotocol.abstract_eval_call in file "ide/coqide/protocol/xmlprotocol.ml", line 788, characters 29-44

Trace for Elpi derive.param1 term.

derive.param1: No unary parametricity translation for annotation
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Elpi__Runtime_trace_off.FFI.wrap_type_err in file "src/runtime_trace_off.ml", line 2071, characters 6-9
Called from Elpi__Runtime_trace_off.FFI.call.aux in file "src/runtime_trace_off.ml", line 2159, characters 25-87
Called from Elpi__Runtime_trace_off.FFI.call in file "src/runtime_trace_off.ml", line 2240, characters 21-70
Called from Elpi__Runtime_trace_off.Constraints.exect_builtin_predicate in file "src/runtime_trace_off.ml", line 3185, characters 20-77
Called from Elpi__Runtime_trace_off.Mainloop.make_runtime.run in file "src/runtime_trace_off.ml", line 3591, characters 19-84
Called from Elpi_util__Util.Fork.fork.ensure_runtime in file "src/utils/util.ml", line 466, characters 16-19
Re-raised at Elpi_util__Util.Fork.fork.ensure_runtime in file "src/utils/util.ml", line 475, characters 7-14
Called from Elpi__Runtime_trace_off.mk_outcome in file "src/runtime_trace_off.ml", line 3842, characters 14-23
Called from Elpi__Runtime_trace_off.execute_once in file "src/runtime_trace_off.ml", line 3859, characters 20-211
Re-raised at Elpi__Runtime_trace_off.execute_once in file "src/runtime_trace_off.ml", line 3864, characters 2-9
Called from Elpi__API.Execute.once in file "src/API.ml" (inlined), line 186, characters 4-55
Called from Coq_elpi_vernacular.run in file "src/coq_elpi_vernacular.ml", line 584, characters 11-53
Called from Coq_elpi_vernacular.run_and_print in file "src/coq_elpi_vernacular.ml", line 604, characters 8-47
Called from Vernacextend.vtdefault.(fun) in file "vernac/vernacextend.ml", line 136, characters 29-33
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 205, characters 24-69
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml", line 255, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 253, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2177, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 964, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2319, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2420, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.finish in file "stm/stm.ml", line 2431, characters 12-50
Called from Stm.process_transaction in file "stm/stm.ml", line 2691, characters 22-45
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.add in file "stm/stm.ml", line 2790, characters 8-50
Called from Dune__exe__Idetop.add in file "ide/coqide/idetop.ml", line 89, characters 25-60
Called from Dune__exe__Idetop.eval_call.interruptible in file "ide/coqide/idetop.ml", line 496, characters 12-15
Called from Xmlprotocol.abstract_eval_call in file "ide/coqide/protocol/xmlprotocol.ml", line 788, characters 29-44

Looking forward to use your library

[gares]

Hello, thanks for reporting the bug. On the last release

From elpi.apps Require Import derive.std.
Set Uniform Inductive Parameters.

Definition annotation (T: Type) := T.
Inductive term :=
| Dummy (x: bool)
| Lam (t: annotation term).

#[verbose,recursive,only(induction)] derive term.

shows

Error: derive.induction generates illtyped term: Illegal application: 
The term "His_Lam" of type
 "forall t : annotation term, is_annotation term P t -> P (Lam t)"
cannot be applied to the terms
 "t" : "annotation term"
 "Pt" : "is_annotation term is_term t"
The 2nd term has type "is_annotation term is_term t"
which should be coercible to "is_annotation term P t".

showing that induction generates a bad term, namely

fun (P : term -> Type) (His_Dummy : forall x : bool, is_bool x -> P (Dummy x))
  (His_Lam : forall t : annotation term, is_annotation term P t -> P (Lam t))
=>
fix IH (s1 : term) (x : is_term s1) {struct x} : P s1 :=
  match x in (is_term s2) return (P s2) with
  | is_Dummy x0 Px => His_Dummy x0 Px
  | is_Lam t Pt => His_Lam t Pt
  end

which lacks a call to IH in His_Lam t (IH t Pt) I guess.

I'll need a few more days to find the time to tackle this one.

[eponier]

@gares ping :smile:

[gares]

For some reason, we don't generate the functoriality property of definitions. If I amend that manually:

From elpi.apps Require Import derive.std.
Set Uniform Inductive Parameters.

Definition annotation (T: Type) := T.

#[verbose] derive annotation.

Definition is_annotation_functor T P Q :
  (forall x:T, P x -> Q x) ->
  forall x, is_annotation T P x -> is_annotation T Q x. trivial. Defined.

Elpi Accumulate derive lp:{{

param1-functor-db {{ is_annotation lp:T lp:P }} {{ is_annotation lp:T lp:Q }}
                  {{ is_annotation_functor lp:T lp:P lp:Q lp:H }} :-
                  param1-functor-db P Q H.

}}.

Inductive term :=
| Dummy (x: bool)
| Lam (t: annotation term).

#[verbose,recursive,only(induction)] derive term.

Print term_induction.

gives:

term_induction =
fun (P : term -> Type)
  (His_Dummy : forall x : bool, is_bool x -> P (Dummy x))
  (His_Lam : forall t : annotation term, is_annotation term P t -> P (Lam t))
=>
fix IH (s1 : term) (x : is_term s1) {struct x} : P s1 :=
  match x in (is_term s2) return (P s2) with
  | is_Dummy x0 Px => His_Dummy x0 Px
  | is_Lam t Pt => His_Lam t (is_annotation_functor term is_term P IH t Pt)
  end
     : forall P : term -> Type,
       (forall x : bool, is_bool x -> P (Dummy x)) ->
       (forall t : annotation term, is_annotation term P t -> P (Lam t)) ->
       forall s1 : term, is_term s1 -> P s1

[gares]

The question is when this property holds and how to prove it systematically. CC @CohenCyril

[CohenCyril]

~I think the answer is always on ground terms without axioms and I think I know how to implement it.~

Actually that's not true, I suspect not all param1 are going to be functorial. Take foo T := T -> T for example. We have is_foo T P := fun f : T -> T => forall x, P x -> P (f x) and unless I'm mistaken we don't have that (forall x, P x -> Q x) -> forall f, is_foo T P f -> is_foo T Q f but only (forall x, P x <-> Q x) -> forall f, is_foo T P f -> is_foo T Q f

So it's functorial but for a different source category... :confused: but it looks too strong for your use case...

[gares]

Yes, had the impressions that the position in which the parameter occurs makes it provable or not. For "containers" the property is true as long as the parameter is positive (I mean at the left of -> as in cons : A -> list A -> list A, or used as another parameter). I don't know how this concept transports to definitions.

[CohenCyril]

Actually we studied that with Enzo and Assia. In our upcoming paper we show how the shape of the term you have influences how strong hypotheses must be. CC @ecranceMERCE @amahboubi

[gares]

OK, then I'll assign you the bug ;-)

[CohenCyril]

And indeed it is essentially tied to positivity.