Skip to content

Commit

Permalink
finish eqOK
Browse files Browse the repository at this point in the history
  • Loading branch information
Enrico Tassi committed Oct 17, 2018
1 parent 0049497 commit 92425f0
Show file tree
Hide file tree
Showing 6 changed files with 43 additions and 95 deletions.
2 changes: 1 addition & 1 deletion derive/derive.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ main T M :-
derive.bcongr.main T {calc (Indname ^ "bcongr_")},
derive.eqK.main T {calc (Indname ^ "eq_axiom_")},
derive.eqcorrect.main T {calc (Indname ^ "eq_correct")},
simplify (eqcorrect-db T) {calc (Indname ^ "eq_OK")}
derive.eqOK T {calc (Indname ^ "eq_OK")}
].

}
84 changes: 27 additions & 57 deletions derive/eqOK.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,68 +4,38 @@

namespace derive.eqOK {

strip-last-arg (app [Hd|Args]) X R :-
appendR Prefix [X] Args,
if (Prefix = []) (R = Hd) (R = app[Hd|Prefix]).
pred body i:int, i:term, i:term, i:term, o:term.

body N (prod NA A a\ prod NF (A_eq a) (B a)) E P
(lam NA A a\ lam NF (A_eq a) f\
lam `p` (PA a f) (B1 a f)) :-
N > 0, !, M is N - 1,
@pi-decl NA A a\
@pi-decl NF (A_eq a) f\
(PA a f = {{ forall x : lp:a, @elpi.derive.eqK.eq_axiom lp:a lp:f x }},
@pi-decl `p` (PA a f) p\
body M (B a f) {mk-app E [a,f]}
{mk-app P [a, {{@elpi.derive.eqK.eq_axiom lp:a lp:f}}, p]}
(B1 a f p)).

trivial? T P :-
strip-last-arg T X Pred,
prove Pred Proof, mk-app Proof [X] P.

prove X _ :- coq.say "prove" X, fail.
prove X P :- param1P-db X P.
prove (app[X|Args]) (app[P|PArgs]) :-
param1P-db X P,
prove-args Args PArgs.

prove-args [] [].
prove-args [X,PX|Args] [X,PX,QX|PArgs] :-
prove PX QX,
prove-args Args PArgs.

hyp (prod _ S T) T1 H Args (lam `_` S _\ R) :-
/*safe-dest-app S HD ArgsS, appendR As [_] ArgsS,
constant? HD As, !,
pi x\ hyp (T x) T1 H Args R.*/ trivial? S P, !,
hyp (T P) T1 H Args R.

hyp (prod N S T) (prod N S T1) H Args (lam N S R) :- !,
pi x\ hyp (T x) (T1 x) H [x|Args] (R x).

hyp T T H A R :- mk-app H {rev A} R.

% Looks like a property on the parameter: specialize
body (prod N (sort _ as S) x\
prod _ (prod _ x _\ sort _) px\ T x px) B Args (lam N S R) :- !,
pi x\ sigma A\
A = {{ @elpi.derive.param1.UnitPred lp:x }},
decl x N S =>
body (T x A) B [A,x|Args] (R x).
% done
body 0 (prod N S x\ prod _ _ _) E P (lam N S R) :-
@pi-decl N S x\ mk-app E [x,{mk-app P [x]}] (R x).

% A trivial premise: prove
body (prod _ S T) B Args R :- trivial? S P, !,
body (T P) B [P|Args] R.
main T O [] :-
assert (T = indt GR) "derive.eqOK: not an inductive type",
coq.env.indt GR _ Lno _ _ _ _,

% A regular premise: recursively simplify
body (prod N S T) B Args (lam N TX R) :- !,
@pi-decl N S x\
(hyp S TX x [] (A x), body (T x) B [A x|Args] (R x)).
assert (eqcorrect-db T E) "derive.eqOK: use derive.eqcorrect before",
coq.env.typeof-gr {term->gr E} ETy,

% done
body _ B Args R :- mk-app B {rev Args} R.
assert (reali T IsT) "derive.eqOK: use derive.param1 before",
assert (param1P-db IsT TisT) "derive.eqOK: use derive.param1P before",

log P :- P, !.
log _ :- coq.say "type checking fails", fail.
body Lno ETy E TisT NewBo,
coq.say {coq.term->string NewBo},
coq.typecheck NewBo NewTy,

main T O [] :- do! [
coq.env.typeof-gr {term->gr T} Ty,
body Ty T [] NewBo,
coq.say {coq.term->string NewBo},
log (coq.typecheck NewBo NewTy),
% TODO: also fix eta expansions
(pi F X T\ copy (app [lam _ _ F, X]) T :- !, copy (F X) T) =>
copy NewTy NewTyNice,
coq.env.add-const O NewBo NewTyNice @opaque! _
].
coq.env.add-const O NewBo NewTy @opaque! _.

}
6 changes: 3 additions & 3 deletions theories/derive/eqOK.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,15 @@
license: GNU Lesser General Public License Version 2.1 or later
------------------------------------------------------------------------- *)

From elpi Require Import elpi derive.param1 derive.param1P.
From elpi Require Import elpi derive.param1 derive.param1P derive.eqK derive.eqcorrect.

Elpi Command derive.eqOK.

Elpi Accumulate File "coq-lib-extra.elpi".
Elpi Accumulate File "derive/param1.elpi".
Elpi Accumulate Db derive.param1.db.

Elpi Accumulate Db derive.param1P.db.
Elpi Accumulate Db derive.eqcorrect.db.

Elpi Accumulate File "derive/eqOK.elpi".
Elpi Accumulate "
Expand All @@ -22,7 +22,7 @@ Elpi Accumulate "
main _ :- usage.

usage :-
coq.error ""Usage: derive.eqOK <term name> [<output name>]"".
coq.error ""Usage: derive.eqOK <inductive name> [<output name>]"".
".
Elpi Typecheck.

2 changes: 1 addition & 1 deletion theories/derive/param1P.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ Elpi Accumulate "
coq.locate I T,
coq.gr->id {term->gr T} Tname,
Name is Tname ^ ""_"",
derive.param1P.main T Name _.
derive.param1P.main T {rex_replace ""^is_"" """" Name} _.
main _ :- usage.

usage :-
Expand Down
38 changes: 8 additions & 30 deletions theories/derive/tests/test_eqOK.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,7 @@ Elpi derive.eq nat.
Elpi derive.eqK nat.
Elpi derive.eqcorrect nat.

Elpi derive.eqOK nat_induction nat_ind.
Check nat_ind : forall P, P 0 -> (forall x, P x -> P (S x)) -> forall n, P n.

Elpi derive.eqOK nat_eq_correct nat_eqOK.
Elpi derive.eqOK nat nat_eqOK.
Check nat_eqOK : forall n, eq_axiom nat nat_eq n.

Elpi derive.param1 list.
Expand All @@ -28,16 +25,11 @@ Elpi derive.eq list.
Elpi derive.eqK list.
Elpi derive.eqcorrect list.


Elpi derive.eqOK list_induction list_ind.
Check list_ind :
forall (A : Type) (P : list A -> Type),
P nil ->
(forall H : A, forall H0 : list A, P H0 -> P (H :: H0)%list) -> forall x : list A, P x.

Elpi derive.eqOK list_eq_correct list_eqOK.
Elpi derive.eqOK list list_eqOK.
Check list_eqOK :
forall (A : Type) (F : A -> A -> bool) x, is_list A (eq_axiom A F) x -> eq_axiom (list A) (list_eq A F) x.
forall (A : Type) (F : A -> A -> bool)
(H : forall l, eq_axiom A F l) x,
eq_axiom (list A) (list_eq A F) x.

Inductive dlist A := dnil | dcons (a : A * nat) (l : dlist A).

Expand All @@ -63,23 +55,9 @@ Elpi derive.eq dlist.
Elpi derive.eqK dlist.
Elpi derive.eqcorrect dlist.

Elpi derive.eqOK dlist_induction dlist_ind2.

Check dlist_induction :
forall (A : Type) (PA : A -> Type) (P : dlist A -> Type),
P (dnil A) ->
(forall a : A * nat,
is_prod A PA nat is_nat a ->
forall l : dlist A, P l -> P (dcons A a l)) -> forall x : dlist A, is_dlist A PA x -> P x.

Check dlist_ind2 :
forall (A : Type) (P : dlist A -> Type),
P (dnil A) ->
(forall a : A * nat, forall l : dlist A, P l -> P (dcons A a l)) ->
forall x : dlist A, P x.

Elpi derive.eqOK dlist_eq_correct dlist_eqOK.
Elpi derive.eqOK dlist dlist_eqOK.

Check dlist_eqOK :
forall A f l, is_dlist A (eq_axiom A f) l -> eq_axiom (dlist A) (dlist_eq A f) l.
forall A f (h : forall l, eq_axiom A f l) l,
eq_axiom (dlist A) (dlist_eq A f) l.

6 changes: 3 additions & 3 deletions theories/derive/tests/test_param1P.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,13 @@ From elpi Require Import derive.param1 derive.param1P.
Elpi derive.param1 list.
Elpi derive.param1P is_list.

Check is_list_is_list :
Check list_is_list :
forall A P, (forall x : A, P x) -> forall l, is_list A P l.

Elpi derive.param1 prod.
Elpi derive.param1P is_prod.

Check is_prod_is_prod :
Check prod_is_prod :
forall A P, (forall x : A, P x) ->
forall B Q, (forall x : B, Q x) ->
forall p, is_prod A P B Q p.
Expand All @@ -20,4 +20,4 @@ Elpi derive.param1 xx.
Elpi derive.param1P is_xx.

Check is_xx : xx -> Type.
Check is_xx_is_xx : forall x : xx, is_xx x.
Check xx_is_xx : forall x : xx, is_xx x.

0 comments on commit 92425f0

Please sign in to comment.