derive eqbOK does not work with is_true

[eponier]

This works

From elpi.apps Require Import derive.std.

Inductive t (n:nat) := C : Nat.leb n 0 = true -> t.

#[only(param1)] derive Nat.leb.
#[only(eqbOK)] derive t.

but this does not

From elpi.apps Require Import derive.std.

Inductive t (n:nat) := C : Datatypes.is_true (Nat.leb n 0) -> t.

#[only(param1)] derive Nat.leb.
#[only(param1)] derive Datatypes.is_true.
#[only(eqbOK)] derive t.

(*
derive.param1_inhab: cannot prove inhabitation: param1-inhab-db
 (app
   [global (const «is_is_true»), 
    app [global (const «Nat.leb»), c0, global (indc «O»)], 
    app
     [global (const «is_leb»), c0, c1, global (indc «O»), 
      global (indc «is_O»)]]) X0^4
*)

[gares]

The problem is that I have a special case for eq here

coq-elpi/apps/derive/theories/derive/param1_trivial.v

Line 26 in 2560ad0

Definition is_eq_inhab

I think it should not be hard to understand is_true there as well

[eponier]

is_true is common enough to deserve a special case indeed, I think. But could it also be possible to unfold it and discover the equality inside? Maybe this is not the spirit of the param1 commands.

[gares]

Yes, I was imagining an ad-hoc unfold rule

param1-inhab-db {{ lib:elpi.derive.is_true lp:B }} R :- param1-inhab-db {{ lib:elpi.eq bool lp:B true }} R.
% also for inhab

(there is not Register for is_true today)