Skip to content

Commit

Permalink
derive: param1 support for is_true and primitive strings
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Feb 25, 2025
1 parent 19cc599 commit 9df4315
Show file tree
Hide file tree
Showing 4 changed files with 152 additions and 73 deletions.
5 changes: 5 additions & 0 deletions apps/derive/tests/test_param1_trivial.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,3 +104,8 @@ Redirect "tmp" Check is_sigma_bool_inhab : full sigma_bool is_sigma_bool.
Redirect "tmp" Check is_ord_inhab : forall p px, full (ord p) (is_ord p px).
Redirect "tmp" Check is_ord2_inhab : forall p px, full (ord2 p) (is_ord2 p px).
Redirect "tmp" Check is_val_inhab : full val is_val.

Redirect "tmp" Record sigma_bool2 := { depn : peano; depeq : lib:elpi.is_true (is_zero depn) }.
Redirect "tmp" Elpi derive.param1 sigma_bool2.
Redirect "tmp" Elpi derive.param1.trivial is_sigma_bool2.
Redirect "tmp" Check is_sigma_bool2_inhab.
17 changes: 16 additions & 1 deletion apps/derive/theories/derive/param1.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,9 @@ Register is_uint63 as elpi.derive.is_uint63.
Inductive is_float64 : PrimFloat.float -> Type := float64 (f : PrimFloat.float ) : is_float64 f.
Register is_float64 as elpi.derive.is_float64.

Inductive is_pstring : lib:elpi.pstring -> Type := pstring (s : lib:elpi.pstring) : is_pstring s.
Register is_pstring as elpi.derive.is_pstring.

(* Links a term (constant, inductive type, inductive constructor) with
its parametricity translation *)
Elpi Db derive.param1.db lp:{{
Expand All @@ -62,6 +65,7 @@ pred reali-done i:gref.

reali {{ lib:num.int63.type }} {{ lib:elpi.derive.is_uint63 }} :- !.
reali {{ lib:num.float.type }} {{ lib:elpi.derive.is_float64 }} :- !.
reali {{ lib:elpi.pstring }} {{ lib:elpi.derive.is_pstring }} :- !.

:name "reali:fail"
reali X _ :-
Expand All @@ -71,6 +75,7 @@ reali X _ :-

realiR {{ lib:num.int63.type }} {{ lib:elpi.derive.is_uint63 }} :- !.
realiR {{ lib:num.float.type }} {{ lib:elpi.derive.is_float64 }} :- !.
realiR {{ lib:elpi.pstring }} {{ lib:elpi.derive.is_pstring }} :- !.

:name "realiR:fail"
realiR T TR :-
Expand All @@ -93,10 +98,20 @@ Elpi Accumulate lp:{{
}}.

Module Export exports.

Local Notation core_is_true := is_true. (* avoid shadowing by param1 is_true *)

Elpi derive.param1 eq.
Elpi derive.param1 bool.
Elpi derive.param1 core_is_true.

End exports.
Register is_eq as elpi.derive.is_eq.

Register is_eq as elpi.derive.is_eq.
Register is_bool as elpi.derive.is_bool.
Register is_true as elpi.derive.is_true.
Register is_false as elpi.derive.is_false.
Register is_is_true as elpi.derive.is_is_true.

(* hook into derive *)
Elpi Accumulate derive File paramX.
Expand Down
201 changes: 129 additions & 72 deletions apps/derive/theories/derive/param1_trivial.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,58 +16,7 @@ From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive
From elpi Require Import elpi.
From elpi.apps Require Import derive.param1 derive.param1_congr.


Definition is_uint63_inhab x : is_uint63 x. Proof. constructor. Defined.
Register is_uint63_inhab as elpi.derive.is_uint63_inhab.

Definition is_float64_inhab x : is_float64 x. Proof. constructor. Defined.
Register is_float64_inhab as elpi.derive.is_float64_inhab.

Definition is_eq_inhab
A (PA : A -> Type) (HA : trivial A PA) (x : A) (px: PA x) y (py : PA y) (eq_xy : x = y) :
is_eq A PA x px y py eq_xy.
Proof.
revert py.
case eq_xy; clear eq_xy y.
intro py.
rewrite <- (trivial_uniq A PA HA x px); clear px.
rewrite <- (trivial_uniq A PA HA x py); clear py.
apply (is_eq_refl A PA x (trivial_full A PA HA x)).
Defined.
Register is_eq_inhab as elpi.derive.is_eq_inhab.

Definition is_uint63_trivial : trivial PrimInt63.int is_uint63 :=
fun x => contracts _ is_uint63 x (is_uint63_inhab x)
(fun y => match y with uint63 i => eq_refl end).
Register is_uint63_trivial as elpi.derive.is_uint63_trivial.

Definition is_float64_trivial : trivial PrimFloat.float is_float64 :=
fun x => contracts _ is_float64 x (is_float64_inhab x)
(fun y => match y with float64 i => eq_refl end).
Register is_float64_trivial as elpi.derive.is_float64_trivial.

Lemma is_eq_trivial A (PA : A -> Type) (HA : trivial A PA) (x : A) (px: PA x)
y (py : PA y)
: trivial (x = y) (is_eq A PA x px y py).
Proof.
intro p.
apply (contracts (x = y) (is_eq A PA x px y py) p (is_eq_inhab A PA HA x px y py p)).
revert py.
case p; clear p y.
rewrite <- (trivial_uniq _ _ HA x px). clear px.
intros py.
rewrite <- (trivial_uniq _ _ HA x py). clear py.
intro v; case v; clear v.
unfold is_eq_inhab.
unfold trivial_full.
unfold trivial_uniq.
case (HA x); intros it def_it; compute.
case (def_it it).
reflexivity.
Defined.
Register is_eq_trivial as elpi.derive.is_eq_trivial.

Elpi Db derive.param1.trivial.db lp:{{
Elpi Db derive.param1.trivial.db lp:{{

pred param1-trivial-done i:inductive.
type param1-trivial-db term -> term -> prop.
Expand All @@ -82,13 +31,7 @@ Elpi Db derive.param1.trivial.db lp:{{
#[superglobal] Elpi Accumulate derive.param1.trivial.db Db Header derive.param1.db.
#[superglobal] Elpi Accumulate derive.param1.trivial.db lp:{{

pred coq.mk-app i:term, i:list term, o:term.
pred coq.sort? i:term.

param1-inhab-db {{ lib:elpi.derive.is_uint63 }} {{ lib:elpi.derive.is_uint63_inhab }}.
param1-inhab-db {{ lib:elpi.derive.is_float64 }} {{ lib:elpi.derive.is_float64_inhab }}.
param1-inhab-db {{ lib:elpi.derive.is_eq }} {{ lib:elpi.derive.is_eq_inhab }}.

:name "param1:inhab:start"
param1-inhab-db (fun `f` (prod `_` S _\ T) f\
prod `x` S x\ prod `px` (RS x) _)
(fun `f` (prod `_` S _\ T) f\
Expand All @@ -98,11 +41,6 @@ Elpi Db derive.param1.trivial.db lp:{{
reali T R,
param1-inhab-db R PT,
coq.mk-app PT [{coq.mk-app f [x]}] (P f x).

param1-inhab-db
{{ lib:elpi.derive.is_eq lp:A lp:PA lp:X lp:PX lp:Y lp:PY }}
{{ lib:elpi.derive.is_eq_inhab lp:A lp:PA lp:QA lp:X lp:PX lp:Y lp:PY }} :- !,
param1-trivial-db PA QA.

param1-inhab-db (app [Hd|Args]) (app[P|PArgs]) :-
param1-inhab-db Hd P, !,
Expand All @@ -115,9 +53,7 @@ Elpi Db derive.param1.trivial.db lp:{{
(param1-inhab-db P Q, R = [T,P,Q|PArgs], param1-inhab-db-args Args PArgs)
(R = [T,P|PArgs], param1-inhab-db-args Args PArgs).

param1-trivial-db {{ lib:elpi.derive.is_uint63 }} {{ lib:elpi.derive.is_uint63_trivial }}.
param1-trivial-db {{ lib:elpi.derive.is_float64 }} {{ lib:elpi.derive.is_float64_trivial }}.

:name "param1:trivial:start"
param1-trivial-db (fun `f` (prod `_` S _\ T) f\
prod `x` S x\ prod `px` (RS x) _)
(fun `f` (prod `_` S _\ T) f\
Expand All @@ -128,11 +64,6 @@ Elpi Db derive.param1.trivial.db lp:{{
param1-trivial-db R PT,
coq.mk-app PT [{coq.mk-app f [x]}] (P f x).

param1-trivial-db
{{ lib:elpi.derive.is_eq lp:A lp:PA lp:X lp:PX lp:Y lp:PY }}
{{ lib:elpi.derive.is_eq_trivial lp:A lp:PA lp:QA lp:X lp:PX lp:Y lp:PY }} :-
param1-trivial-db PA QA.

param1-trivial-db (app [Hd|Args]) (app[P|PArgs]) :-
param1-trivial-db Hd P, !,
param1-trivial-db-args Args PArgs.
Expand All @@ -146,6 +77,7 @@ Elpi Db derive.param1.trivial.db lp:{{

}}.


(* standalone *)
Elpi Command derive.param1.trivial.
Elpi Accumulate File derive_hook.
Expand Down Expand Up @@ -184,7 +116,132 @@ Elpi Accumulate lp:{{
coq.error "Usage: derive.param1.inhab <inductive type name>".
}}.

(* ad-hoc rules for primitive data, eq and is_true *)

Module Export exports.
Elpi derive.param1.trivial is_bool.
End exports.

Definition is_uint63_inhab x : is_uint63 x. Proof. constructor. Defined.
Register is_uint63_inhab as elpi.derive.is_uint63_inhab.

Definition is_float64_inhab x : is_float64 x. Proof. constructor. Defined.
Register is_float64_inhab as elpi.derive.is_float64_inhab.

Definition is_pstring_inhab s : is_pstring s. Proof. constructor. Defined.
Register is_pstring_inhab as elpi.derive.is_pstring_inhab.

Definition is_eq_inhab
A (PA : A -> Type) (HA : trivial A PA) (x : A) (px: PA x) y (py : PA y) (eq_xy : x = y) :
is_eq A PA x px y py eq_xy.
Proof.
revert py.
case eq_xy; clear eq_xy y.
intro py.
rewrite <- (trivial_uniq A PA HA x px); clear px.
rewrite <- (trivial_uniq A PA HA x py); clear py.
apply (is_eq_refl A PA x (trivial_full A PA HA x)).
Defined.
Register is_eq_inhab as elpi.derive.is_eq_inhab.

Definition is_true_inhab b (H : is_bool b) p : is_is_true b H p :=
is_eq_inhab bool is_bool is_bool_trivial b H true is_true p.
Register is_true_inhab as elpi.derive.is_true_inhab.


Elpi Accumulate derive.param1.trivial.db lp:{{

:before "param1:inhab:start"
param1-inhab-db {{ lib:elpi.derive.is_uint63 }} {{ lib:elpi.derive.is_uint63_inhab }}.
:before "param1:inhab:start"
param1-inhab-db {{ lib:elpi.derive.is_float64 }} {{ lib:elpi.derive.is_float64_inhab }}.
:before "param1:inhab:start"
param1-inhab-db {{ lib:elpi.derive.is_pstring }} {{ lib:elpi.derive.is_pstring_inhab }}.
:before "param1:inhab:start"
param1-inhab-db {{ lib:elpi.derive.is_eq }} {{ lib:elpi.derive.is_eq_inhab }}.
:before "param1:inhab:start"
param1-inhab-db {{ lib:elpi.derive.is_true }} {{ lib:elpi.derive.is_true_inhab }}.


:before "param1:inhab:start"
param1-inhab-db
{{ lib:elpi.derive.is_eq lp:A lp:PA lp:X lp:PX lp:Y lp:PY }}
{{ lib:elpi.derive.is_eq_inhab lp:A lp:PA lp:QA lp:X lp:PX lp:Y lp:PY }} :- !,
param1-trivial-db PA QA.

:before "param1:inhab:start"
param1-inhab-db {{ lib:elpi.derive.is_is_true lp:B lp:PB }} R :- !,
param1-inhab-db {{ lib:elpi.derive.is_eq lib:elpi.bool lib:elpi.derive.is_bool lp:B lp:PB lib:elpi.true lib:elpi.derive.is_true }} R.

}}.


Definition is_uint63_trivial : trivial PrimInt63.int is_uint63 :=
fun x => contracts _ is_uint63 x (is_uint63_inhab x)
(fun y => match y with uint63 i => eq_refl end).
Register is_uint63_trivial as elpi.derive.is_uint63_trivial.

Definition is_float64_trivial : trivial PrimFloat.float is_float64 :=
fun x => contracts _ is_float64 x (is_float64_inhab x)
(fun y => match y with float64 i => eq_refl end).
Register is_float64_trivial as elpi.derive.is_float64_trivial.

Definition is_pstring_trivial : trivial lib:elpi.pstring is_pstring :=
fun x => contracts _ is_pstring x (is_pstring_inhab x)
(fun y => match y with pstring i => eq_refl end).
Register is_pstring_trivial as elpi.derive.is_pstring_trivial.

Lemma is_eq_trivial A (PA : A -> Type) (HA : trivial A PA) (x : A) (px: PA x)
y (py : PA y)
: trivial (x = y) (is_eq A PA x px y py).
Proof.
intro p.
apply (contracts (x = y) (is_eq A PA x px y py) p (is_eq_inhab A PA HA x px y py p)).
revert py.
case p; clear p y.
rewrite <- (trivial_uniq _ _ HA x px). clear px.
intros py.
rewrite <- (trivial_uniq _ _ HA x py). clear py.
intro v; case v; clear v.
unfold is_eq_inhab.
unfold trivial_full.
unfold trivial_uniq.
case (HA x); intros it def_it; compute.
case (def_it it).
reflexivity.
Defined.
Register is_eq_trivial as elpi.derive.is_eq_trivial.

Definition is_true_trivial b (H : is_bool b) : trivial (lib:elpi.is_true b) (is_is_true b H) :=
is_eq_trivial bool is_bool is_bool_trivial b H true is_true.
Register is_true_trivial as elpi.derive.is_true_trivial.


Elpi Accumulate derive.param1.trivial.db lp:{{

:before "param1:trivial:start"
param1-trivial-db {{ lib:elpi.derive.is_uint63 }} {{ lib:elpi.derive.is_uint63_trivial }}.
:before "param1:trivial:start"
param1-trivial-db {{ lib:elpi.derive.is_float64 }} {{ lib:elpi.derive.is_float64_trivial }}.
:before "param1:trivial:start"
param1-trivial-db {{ lib:elpi.derive.is_pstring }} {{ lib:elpi.derive.is_pstring_trivial }}.
:before "param1:trivial:start"
param1-trivial-db {{ lib:elpi.derive.is_eq }} {{ lib:elpi.derive.is_eq_trivial }}.
:before "param1:trivial:start"
param1-trivial-db {{ lib:elpi.derive.is_true }} {{ lib:elpi.derive.is_true_trivial }}.


:before "param1:trivial:start"
param1-trivial-db
{{ lib:elpi.derive.is_eq lp:A lp:PA lp:X lp:PX lp:Y lp:PY }}
{{ lib:elpi.derive.is_eq_trivial lp:A lp:PA lp:QA lp:X lp:PX lp:Y lp:PY }} :-
param1-trivial-db PA QA.

:before "param1:trivial:start"
param1-trivial-db {{ lib:elpi.derive.is_is_true lp:B lp:PB }} R :- !,
param1-trivial-db {{ lib:elpi.derive.is_eq lib:elpi.bool lib:elpi.derive.is_bool lp:B lp:PB lib:elpi.true lib:elpi.derive.is_true }} R.

}}.

(* hook into derive *)
Elpi Accumulate derive Db derive.param1.trivial.db.
Expand Down
2 changes: 2 additions & 0 deletions theories/elpi.v.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,11 @@ Register Coq.Init.Datatypes.false as elpi.false.
#[only="8.20"] Register Coq.Bool.Bool.reflect as elpi.reflect.
#[only="8.20"] Register Coq.Bool.Bool.ReflectF as elpi.ReflectF.
#[only="8.20"] Register Coq.Bool.Bool.ReflectT as elpi.ReflectT.
#[only="8.20"] Register Coq.Init.Datatypes.is_true as elpi.is_true.
#[skip="8.20"] Register Corelib.Init.Datatypes.reflect as elpi.reflect.
#[skip="8.20"] Register Corelib.Init.Datatypes.ReflectF as elpi.ReflectF.
#[skip="8.20"] Register Corelib.Init.Datatypes.ReflectT as elpi.ReflectT.
#[skip="8.20"] Register Corelib.Init.Datatypes.is_true as elpi.is_true.

#[only="8.20"] From Coq Require PrimString.
#[skip="8.20"] From Corelib Require PrimString.
Expand Down

0 comments on commit 9df4315

Please sign in to comment.