From 1a4efa19170a13407df2e1bd16f68c0ed779eb11 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 14 Nov 2022 23:15:29 +0100 Subject: [PATCH] Port to Hierarchy Builder --- examples/zmodule.v | 9 +++++++-- theories/common.elpi | 44 ++++++++++++++++++++++---------------------- theories/ring.v | 13 +++++++++++++ 3 files changed, 42 insertions(+), 24 deletions(-) diff --git a/examples/zmodule.v b/examples/zmodule.v index 86459e0..8bdabf0 100644 --- a/examples/zmodule.v +++ b/examples/zmodule.v @@ -399,6 +399,11 @@ Ltac morph_zmodule_reflection V VarMap ME1 ME2 ZE1 ZE2 := apply: (@AG_correct V VarMap ZE1 ZE2); [vm_compute; reflexivity]. +Module MorphSort. +Import GRing. +Definition Additive U V := @Additive.apply U V (Phant (U -> V)). +End MorphSort. + Elpi Tactic morph_zmodule. Elpi Accumulate lp:{{ @@ -423,8 +428,8 @@ quote V F {{ @subr lp:V' lp:In1 lp:In2 }} coq.unify-eq V V' ok, !, quote V F In1 OutM1 Out1 VarMap, quote V F In2 OutM2 Out2 VarMap. quote V F In {{ @MMorph lp:U lp:V lp:G lp:OutM }} Out VarMap :- - coq.unify-eq {{ @GRing.Additive.apply lp:U lp:V lp:Ph lp:G lp:In1 }} In ok, !, - quote U (x\ F {{ @GRing.Additive.apply lp:U lp:V lp:Ph lp:G lp:x }}) + coq.unify-eq {{ @MorphSort.Additive lp:U lp:V lp:G lp:In1 }} In ok, !, + quote U (x\ F {{ @MorphSort.Additive lp:U lp:V lp:G lp:x }}) In1 OutM Out VarMap. quote V F In {{ @MX lp:V lp:In }} {{ AGX lp:N }} VarMap :- !, mem VarMap (F In) N. diff --git a/theories/common.elpi b/theories/common.elpi index 6371965..b27101b 100644 --- a/theories/common.elpi +++ b/theories/common.elpi @@ -140,7 +140,7 @@ quote.nat _ {{ Nat.of_num_uint lp:In }} {{ NC lp:OutM }} Out _ :- n-constant N OutM, quote.expr.constant { z-constant N } Out. quote.nat R In {{ NX lp:In }} Out VarMap :- !, - Zmodule = {{ GRing.Ring.zmodType lp:R }}, + Zmodule = {{ GRing_Ring__to__GRing_Zmodule lp:R }}, mem VarMap {{ @GRing.natmul lp:Zmodule (@GRing.one lp:R) lp:In }} N, !, quote.expr.variable { positive-constant {calc (N + 1)} } Out. @@ -193,13 +193,13 @@ quote.zmod U R Morph {{ @intmul lp:U' lp:In1 lp:In2 }} quote.zmod U R Morph In1 OutM1 Out1 VarMap, !, quote.ring {{ int_Ring }} none R - (n\ {{ @intmul (GRing.Ring.zmodType lp:R) (@GRing.one lp:R) lp:n }}) + (n\ {{ @intmul (GRing_Ring__to__GRing_Zmodule lp:R) (@GRing.one lp:R) lp:n }}) In2 OutM2 Out2 VarMap, !, quote.expr.mul Out1 Out2 Out. % additive functions quote.zmod U R Morph In {{ @ZMMorph lp:V lp:U lp:NewMorphInst lp:OutM }} Out VarMap :- - NewMorph = (x\ {{ @GRing.Additive.apply lp:V lp:U _ lp:NewMorphInst lp:x }}), + NewMorph = (x\ {{ @MorphSort.Additive lp:V lp:U lp:NewMorphInst lp:x }}), coq.unify-eq In (NewMorph In1) ok, !, % TODO: for concrete additive functions, should we unpack [NewMorph]? @@ -223,26 +223,26 @@ pred quote.ring i:term, i:option term, i:term, i:(term -> term), i:term, o:term, o:term, o:list term. % 0%R quote.ring R _ _ _ {{ @GRing.zero lp:V }} {{ @R0 lp:R }} Out _ :- - coq.unify-eq V {{ GRing.Ring.zmodType lp:R }} ok, !, + coq.unify-eq V {{ GRing_Ring__to__GRing_Zmodule lp:R }} ok, !, quote.expr.zero Out. % -%R quote.ring R F TR Morph {{ @GRing.opp lp:V lp:In1 }} {{ @ROpp lp:R lp:OutM1 }} Out VarMap :- - coq.unify-eq V {{ GRing.Ring.zmodType lp:R }} ok, + coq.unify-eq V {{ GRing_Ring__to__GRing_Zmodule lp:R }} ok, !, quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !, quote.expr.opp Out1 Out. % Z.opp quote.ring R none TR Morph {{ Z.opp lp:In1 }} {{ @RZOpp lp:OutM1 }} Out VarMap :- - coq.unify-eq {{ ZInstances.Z_ringType }} R ok, + coq.unify-eq {{ Z_ringType }} R ok, !, quote.ring R none TR Morph In1 OutM1 Out1 VarMap, !, quote.expr.opp Out1 Out. % +%R quote.ring R F TR Morph {{ @GRing.add lp:V lp:In1 lp:In2 }} {{ @RAdd lp:R lp:OutM1 lp:OutM2 }} Out VarMap :- - coq.unify-eq V {{ GRing.Ring.zmodType lp:R }} ok, + coq.unify-eq V {{ GRing_Ring__to__GRing_Zmodule lp:R }} ok, !, quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !, quote.ring R F TR Morph In2 OutM2 Out2 VarMap, !, @@ -250,7 +250,7 @@ quote.ring R F TR Morph {{ @GRing.add lp:V lp:In1 lp:In2 }} % Z.add quote.ring R none TR Morph {{ Z.add lp:In1 lp:In2 }} {{ @RZAdd lp:OutM1 lp:OutM2 }} Out VarMap :- - coq.unify-eq {{ ZInstances.Z_ringType }} R ok, + coq.unify-eq {{ Z_ringType }} R ok, !, quote.ring R none TR Morph In1 OutM1 Out1 VarMap, !, quote.ring R none TR Morph In2 OutM2 Out2 VarMap, !, @@ -258,7 +258,7 @@ quote.ring R none TR Morph {{ Z.add lp:In1 lp:In2 }} % Z.sub quote.ring R none TR Morph {{ Z.sub lp:In1 lp:In2 }} {{ @RZSub lp:OutM1 lp:OutM2 }} Out VarMap :- - coq.unify-eq {{ ZInstances.Z_ringType }} R ok, + coq.unify-eq {{ Z_ringType }} R ok, !, quote.ring R none TR Morph In1 OutM1 Out1 VarMap, !, quote.ring R none TR Morph In2 OutM2 Out2 VarMap, !, @@ -266,7 +266,7 @@ quote.ring R none TR Morph {{ Z.sub lp:In1 lp:In2 }} % (_ *+ _)%R quote.ring R F TR Morph {{ @GRing.natmul lp:V lp:In1 lp:In2 }} {{ @RMuln lp:R lp:OutM1 lp:OutM2 }} Out VarMap :- - coq.unify-eq V {{ @GRing.Ring.zmodType lp:R }} ok, + coq.unify-eq V {{ @GRing_Ring__to__GRing_Zmodule lp:R }} ok, !, quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !, quote.nat TR In2 OutM2 Out2 VarMap, !, @@ -274,12 +274,12 @@ quote.ring R F TR Morph {{ @GRing.natmul lp:V lp:In1 lp:In2 }} % (_ *~ _)%R quote.ring R F TR Morph {{ @intmul lp:V lp:In1 lp:In2 }} {{ @RMulz lp:R lp:OutM1 lp:OutM2 }} Out VarMap :- - coq.unify-eq V {{ @GRing.Ring.zmodType lp:R }} ok, + coq.unify-eq V {{ @GRing_Ring__to__GRing_Zmodule lp:R }} ok, !, quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !, quote.ring {{ int_Ring }} none TR - (n\ {{ @intmul (GRing.Ring.zmodType lp:TR) (@GRing.one lp:TR) lp:n }}) + (n\ {{ @intmul (GRing_Ring__to__GRing_Zmodule lp:TR) (@GRing.one lp:TR) lp:n }}) In2 OutM2 Out2 VarMap, !, quote.expr.mul Out1 Out2 Out. % 1%R @@ -298,7 +298,7 @@ quote.ring R F TR Morph {{ @GRing.mul lp:R' lp:In1 lp:In2 }} % Z.mul quote.ring R none TR Morph {{ Z.mul lp:In1 lp:In2 }} {{ @RZMul lp:OutM1 lp:OutM2 }} Out VarMap :- - coq.unify-eq {{ ZInstances.Z_ringType }} R ok, + coq.unify-eq {{ Z_ringType }} R ok, !, quote.ring R none TR Morph In1 OutM1 Out1 VarMap, !, quote.ring R none TR Morph In2 OutM2 Out2 VarMap, !, @@ -317,7 +317,7 @@ quote.ring R F TR Morph {{ @exprz lp:R' lp:In1 lp:In2 }} z-constant Exp { coq.reduction.vm.norm {{ Z_of_int lp:In2 }} {{ Z }} }, if (Exp >= 0) (CONT = - (coq.unify-eq {{ GRing.UnitRing.ringType lp:R' }} R ok, !, + (coq.unify-eq {{ GRing_UnitRing__to__GRing_Ring lp:R' }} R ok, !, quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !, n-constant Exp Out2, !, OutM = {{ @RExpPosz lp:R' lp:OutM1 lp:Out2 }}, !, @@ -325,7 +325,7 @@ quote.ring R F TR Morph {{ @exprz lp:R' lp:In1 lp:In2 }} (CONT = (field-mode, F = some F', - coq.unify-eq R' {{ GRing.Field.unitRingType lp:F' }} ok, !, + coq.unify-eq R' {{ GRing_Field__to__GRing_UnitRing lp:F' }} ok, !, quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !, n-constant { calc (~ (Exp + 1)) } Out2, !, OutM = {{ @RExpNegz lp:F' lp:OutM1 lp:Out2 }}, !, @@ -334,7 +334,7 @@ quote.ring R F TR Morph {{ @exprz lp:R' lp:In1 lp:In2 }} % Z.pow quote.ring R none TR Morph {{ Z.pow lp:In1 lp:In2 }} {{ @RZExp lp:OutM1 lp:In2' }} Out VarMap :- - coq.unify-eq {{ ZInstances.Z_ringType }} R ok, + coq.unify-eq {{ Z_ringType }} R ok, coq.reduction.vm.norm In2 {{ Z }} In2', z-constant Exp In2', !, @@ -347,7 +347,7 @@ quote.ring R none TR Morph {{ Z.pow lp:In1 lp:In2 }} quote.ring R (some F) TR Morph {{ @GRing.inv lp:R' lp:In1 }} {{ @RInv lp:F lp:OutM1 }} {{ @FEinv Z lp:Out1 }} VarMap :- field-mode, - coq.unify-eq R' {{ GRing.Field.unitRingType lp:F }} ok, + coq.unify-eq R' {{ GRing_Field__to__GRing_UnitRing lp:F }} ok, !, quote.ring R (some F) TR Morph In1 OutM1 Out1 VarMap. % Posz @@ -363,14 +363,14 @@ quote.ring R _ TR _ {{ Negz lp:In }} {{ @RNegz lp:OutM1 }} Out VarMap :- quote.expr.opp { quote.expr.add { quote.expr.one } Out1 } Out. % Z constants quote.ring R _ _ _ In {{ @RZC lp:In }} Out _ :- - coq.unify-eq {{ ZInstances.Z_ringType }} R ok, + coq.unify-eq {{ int_Ring }} R ok, z-constant _ In, !, quote.expr.constant In Out. % morphisms quote.ring R _ TR Morph In {{ @RMorph lp:Q lp:R lp:NewMorphInst lp:OutM }} Out VarMap :- - NewMorph = (x\ {{ @GRing.RMorphism.apply - lp:Q lp:R _ lp:NewMorphInst lp:x }}), + NewMorph = (x\ {{ @MorphSort.RMorphism + lp:Q lp:R lp:NewMorphInst lp:x }}), coq.unify-eq In (NewMorph In1) ok, !, % TODO: for concrete morphisms, should we unpack [NewMorph]? @@ -379,8 +379,8 @@ quote.ring R _ TR Morph In quote.ring R _ TR Morph In {{ @RMorph' lp:V lp:R lp:NewMorphInst lp:OutM }} Out VarMap :- NewMorph = - (x\ {{ @GRing.Additive.apply - lp:V (GRing.Ring.zmodType lp:R) _ lp:NewMorphInst lp:x }}), + (x\ {{ @MorphSort.Additive + lp:V (GRing_Ring__to__GRing_Zmodule lp:R) lp:NewMorphInst lp:x }}), coq.unify-eq In (NewMorph In1) ok, !, % TODO: for concrete additive functions, should we unpack [NewMorph]? diff --git a/theories/ring.v b/theories/ring.v index cff3d87..6770563 100644 --- a/theories/ring.v +++ b/theories/ring.v @@ -691,6 +691,19 @@ Strategy expand [addn_expand nat_of_pos_rec_expand nat_of_pos_expand nat_of_N_expand int_of_Z_expand Neval Reval Nnorm Rnorm Fnorm PEeval FEeval]. +Definition int_Ring := Eval hnf in [the ringType of int : Type]. +Definition Z_ringType := Eval hnf in [the ringType of Z : Type]. + +Definition GRing_Ring__to__GRing_Zmodule : ringType -> zmodType := id. +Definition GRing_UnitRing__to__GRing_Ring : unitRingType -> ringType := id. +Definition GRing_Field__to__GRing_UnitRing : fieldType -> unitRingType := id. + +Module MorphSort. +Import GRing. +Definition Additive U V := @Additive.apply U V (Phant (U -> V)). +Definition RMorphism U V := @RMorphism.apply U V (Phant (U -> V)). +End MorphSort. + Elpi Tactic ring. Elpi Accumulate File "theories/common.elpi". Elpi Accumulate File "theories/ring.elpi".