You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Elpi's derive improves on Keller-Lasson's paramcoq by iota-expanding the body of fixpoints so that there is no need, as in paramcoq, to manually proving that (fix f x := t) x is observationally equal to t[f:=fix f x := t].
I tried to understand better the scope of the iota-expansion trick and found two situations where it does not apply directly:
fixpoints over terms in inductive types with non-trivial indices as e.g. for Vector.rectS
fixpoints which require to return a variable rather than a constructor so that the guard condition scales, as in Nat.sub where n in the right-hand side should not be expanded so that sub can be used in other fixpoints (e.g., indirectly, in Nat.gcd)
I don't know if these questions have already been investigated in the context of Elpi.
For 1., generalizing first may help, as in the following example:
Inductive A : bool -> Type :=
| Z b : A b
| C : A false -> A false.
Fixpoint f (a : A false) : bool :=
match a with
| Z b => true
| C a => f a
end.
From elpi.apps Require derive.std.
Elpi derive.param1 bool.
Elpi derive.param1 A.
Fail Elpi derive.param1 f.
Fixpoint f_gen b (a : A b) : bool :=
match a with
| Z b => true
| C a => f_gen false a
end.
Elpi derive.param1 f_gen. (* works *)
Definition is_f := is_f_gen false is_false. (* bypassing the limitation *)
It seems that integrating small inversion can also help in some cases as in this alternative definition of parametricity for f:
Fixpoint is_f (a : A false) (Pa : is_A false is_false a) {struct Pa} : is_bool (f a) :=
match Pa in (is_A b P_ s1)
return (if b return A b -> _ then fun _ => unit else fun s1 : A false => is_bool (f s1)) s1
with
| is_Z b _ =>
if b return (if b return A b -> _ then fun _ => unit else fun s1 : A false => is_bool (f s1)) (Z b)
then tt
else is_true
| is_C x P_ =>
is_f x P_
end.
For 2., I suspect that inserting rewriting may work but I see also a possible solution Coq side. The idea would be to slightly change the expressiveness of the match construct in Coq, adding to:
match t as x in I y return P y x with
| C z => u
end
an explicit access to the instance of the term being matched:
match t as x in I y return P y x with
| C z as w => u
end
so that is_sub, that is currently generated (up to reduction) as:
Fixpoint is_sub (n : nat) (Pn : is_nat n) {struct Pn} :
forall m : nat, is_nat m -> is_nat (Nat.sub n m) :=
match
Pn in (is_nat s1)
return (forall m : nat, is_nat m -> is_nat (Nat.sub s1 m))
with
| is_O => fun (m : nat) (_ : is_nat m) => is_O
| is_S x P_ => fun (m : nat) (Pm : is_nat m) =>
match
Pm in (is_nat m0)
return (is_nat match m0 with 0 => S x | S l => Nat.sub x l end)
with
| is_O => is_S x P_
| is_S l Pl => is_sub x P_ l Pl
end
end.
would instead be generated as:
Fixpoint is_sub (n : nat) (Pn : is_nat n) {struct Pn} :
forall m : nat, is_nat m -> is_nat (Nat.sub n m) :=
match
Pn in (is_nat s1)
return (forall m : nat, is_nat m -> is_nat (Nat.sub s1 m))
with
| is_O as x => fun (m : nat) (_ : is_nat m) => x
| is_S x P_ as x => fun (m : nat) (Pm : is_nat m) =>
match
Pm in (is_nat m0)
return (is_nat match m0 with 0 => S x | S l => Nat.sub x l end)
with
| is_O => x
| is_S l Pl => is_sub x P_ l Pl
end
end.
and the subterm property on x is preserved. [Added: see coq/rfcs#73 for a proposal]
Do you think it would eventually be possible in Elpi to support one way or the others the two examples above? (And more generally, is it possible to imagine one day Coq's generation of _rect schemes to be provided by Elpi?)
The text was updated successfully, but these errors were encountered:
About returning the original value I think it should be doable, and even desirable. I have no time now to work it out, but I may give it a try eventually
Elpi's
derive
improves on Keller-Lasson's paramcoq by iota-expanding the body of fixpoints so that there is no need, as in paramcoq, to manually proving that(fix f x := t) x
is observationally equal tot[f:=fix f x := t]
.I tried to understand better the scope of the iota-expansion trick and found two situations where it does not apply directly:
Vector.rectS
Nat.sub
wheren
in the right-hand side should not be expanded so thatsub
can be used in other fixpoints (e.g., indirectly, inNat.gcd
)I don't know if these questions have already been investigated in the context of Elpi.
For 1., generalizing first may help, as in the following example:
It seems that integrating small inversion can also help in some cases as in this alternative definition of parametricity for
f
:For 2., I suspect that inserting rewriting may work but I see also a possible solution Coq side. The idea would be to slightly change the expressiveness of the
match
construct in Coq, adding to:an explicit access to the instance of the term being matched:
so that
is_sub
, that is currently generated (up to reduction) as:would instead be generated as:
and the subterm property on
x
is preserved. [Added: see coq/rfcs#73 for a proposal]Do you think it would eventually be possible in Elpi to support one way or the others the two examples above? (And more generally, is it possible to imagine one day Coq's generation of
_rect
schemes to be provided by Elpi?)The text was updated successfully, but these errors were encountered: