Push inv under exp

math-comp · Jul 18, 2023 · 90979f3 · 90979f3
1 parent 14df4d2
commit 90979f3
Show file tree

Hide file tree

Showing 2 changed files with 45 additions and 57 deletions.
diff --git a/theories/common.elpi b/theories/common.elpi
@@ -522,59 +522,49 @@ irquote Inv rmorphism-Z {{ Z.mul lp:In1 lp:In2 }}
   quote.expr.mul Out1 Out2 Out.
 % (_ ^+ _)%R
 irquote Inv C {{ @GRing.exp lp:R' lp:In1 lp:In2 }}
-       {{ @RExpn lp:R lp:OutM1 lp:OutM2 }} Out' VM :-
-  can-inv Inv,
+       {{ @RExpn lp:R lp:OutM1 lp:OutM2 }} Out VM :-
   rmorphism->sring C R,
   coq.unify-eq R R' ok,
   quote.ncstr In2 OutM2 Out2, !,
-  rquote C In1 OutM1 Out1 VM, !,
-  quote.expr.exp Out1 Out2 Out,
-  quote.expr.cond-inv Inv Out Out'.
+  irquote Inv C In1 OutM1 Out1 VM, !,
+  quote.expr.exp Out1 Out2 Out.
 % (_ ^ _)%R
-irquote Inv C {{ @exprz lp:R' lp:In1 lp:In2 }} OutM Out' VM :-
-  can-inv Inv,
+irquote Inv C {{ @exprz lp:R' lp:In1 lp:In2 }} OutM Out VM :-
   quote.icstr In2 Pos OutM2 Out2,
   rmorphism->uring C R,
   coq.unify-eq R R' ok,
   if (Pos = tt)
      (CONT =
-       (!, rquote C In1 OutM1 Out1 VM, !,
+       (!, irquote Inv C In1 OutM1 Out1 VM, !,
         OutM = {{ @RExpPosz lp:R lp:OutM1 lp:OutM2 }}, !,
         quote.expr.exp Out1 Out2 Out))
      (CONT =
-       (rmorphism->field C F, not quote.expr.inv-only-const, !,
-        rquote C In1 OutM1 Out1 VM, !,
+       (rmorphism->field C F, !,
+        irquote {negb Inv} C In1 OutM1 Out1 VM, !,
         OutM = {{ @RExpNegz lp:F lp:OutM1 lp:OutM2 }}, !,
-        quote.expr.inv { quote.expr.exp Out1 Out2 } Out)),
-  CONT,
-  quote.expr.cond-inv Inv Out Out'.
+        quote.expr.exp Out1 Out2 Out)),
+  CONT.
 % expn
 irquote Inv rmorphism-nat {{ expn lp:In1 lp:In2 }}
-       {{ @RnatExpn lp:OutM1 lp:OutM2 }} Out' VM :-
-  can-inv Inv,
+       {{ @RnatExpn lp:OutM1 lp:OutM2 }} Out VM :-
   quote.ncstr In2 OutM2 Out2, !,
-  rquote rmorphism-nat In1 OutM1 Out1 VM, !,
-  quote.expr.exp Out1 Out2 Out,
-  quote.expr.cond-inv Inv Out Out'.
+  irquote Inv rmorphism-nat In1 OutM1 Out1 VM, !,
+  quote.expr.exp Out1 Out2 Out.
 % N.pow
 irquote Inv rmorphism-N {{ N.pow lp:In1 lp:In2 }}
-       {{ @RNExp lp:OutM1 lp:Out2 }} Out' VM :-
-  can-inv Inv,
+       {{ @RNExp lp:OutM1 lp:Out2 }} Out VM :-
   reduction-N In2 Out2, !,
-  rquote rmorphism-N In1 OutM1 Out1 VM, !,
-  quote.expr.exp Out1 Out2 Out,
-  quote.expr.cond-inv Inv Out Out'.
+  irquote Inv rmorphism-N In1 OutM1 Out1 VM, !,
+  quote.expr.exp Out1 Out2 Out.
 % Z.pow
 irquote Inv rmorphism-Z {{ Z.pow lp:In1 lp:In2 }}
-       {{ @RZExp lp:OutM1 lp:OutM2 }} Out' VM :-
-  reduction-Z In2 OutM2,
-  (can-inv Inv; OutM2 = {{ Zneg _ }}), !,
+       {{ @RZExp lp:OutM1 lp:OutM2 }} Out VM :-
+  reduction-Z In2 OutM2, !,
   ((OutM2 = {{ Z0 }}, !, Out2 = {{ N0 }}; % If [In2] is non-negative
     OutM2 = {{ Zpos lp:P }}, !, Out2 = {{ Npos lp:P }}), !,
-   rquote rmorphism-Z In1 OutM1 Out1 VM, !,
-   quote.expr.exp Out1 Out2 Out,
-   quote.expr.cond-inv Inv Out Out';
-   quote.expr.zero Out'). % If [In2] is negative
+   irquote Inv rmorphism-Z In1 OutM1 Out1 VM, !,
+   quote.expr.exp Out1 Out2 Out;
+   quote.expr.zero Out). % If [In2] is negative
 % _^-1
 irquote Inv C {{ @GRing.inv lp:R lp:In1 }} {{ @RInv lp:F lp:OutM1 }} Out VM :-
   rmorphism->field C F,

diff --git a/theories/common.v b/theories/common.v
@@ -519,13 +519,13 @@ Fixpoint Fnorm invb R (f : R -> F) (e : RExpr R) : F :=
   | RMul _ e1 e2 | RnatMul e1 e2 | RNMul e1 e2 | RZMul e1 e2  =>
       fun f => mul (Fnorm invb f e1) (Fnorm invb f e2)
   | RExpn _ e1 n | RnatExpn e1 n =>
-      fun f => invr (exp (Fnorm false f e1) (N_of_large_nat n))
-  | RExpPosz _ e1 n => fun f => invr (exp (Fnorm false f e1) (N_of_large_nat n))
+      fun f => exp (Fnorm invb f e1) (N_of_large_nat n)
+  | RExpPosz _ e1 n => fun f => exp (Fnorm invb f e1) (N_of_large_nat n)
   | RExpNegz _ e1 n =>
-      fun f => invr (inv (exp (Fnorm false f e1) (N.succ (N_of_large_nat n))))
-  | RNExp e1 n => fun f => invr (exp (Fnorm false f e1) n)
+      fun f => exp (Fnorm (~~ invb) f e1) (N.succ (N_of_large_nat n))
+  | RNExp e1 n => fun f => exp (Fnorm invb f e1) n
   | RZExp e1 (Z.neg _) => fun f => zero
-  | RZExp e1 n => fun f => invr (exp (Fnorm false f e1) (Z.to_N n))
+  | RZExp e1 n => fun f => exp (Fnorm invb f e1) (Z.to_N n)
   | RInv _ e1 => fun f => Fnorm (~~ invb) f e1
   | RnatS p e => fun f => invr (add (F_of_Z false (Zpos p)) (Fnorm false f e))
   | RnatC n => fun => F_of_Z invb (Z_of_large_nat n)
@@ -594,18 +594,12 @@ move: f f' invb m ff'; elim e using (@RExpr_ind' P P0); rewrite {R e}/P {}/P0 //
   by congr mul; [exact: IHe1|exact: IHe2].
 - move=> e1 IHe1 e2 IHe2 f f' invb m ff'.
   by congr mul; [exact: IHe1|exact: IHe2].
-- move=> R e1 IHe1 n f f'.
-  by case=> m ff'; [congr inv|]; (congr exp; exact: IHe1).
-- move=> R e1 IHe1 n f f'.
-  by case=> m ff'; [congr inv|]; (congr exp; exact: IHe1).
-- move=> R e1 IHe1 n f f'.
-  by case=> m ff'; [congr inv|]; (congr inv; congr exp; exact: IHe1).
-- move=> e1 IHe1 n f f'.
-  by case=> m ff'; [congr inv|]; (congr exp; exact: IHe1).
-- move=> e1 IHe1 n f f'.
-  by case=> m ff'; [congr inv|]; (congr exp; exact: IHe1).
-- move=> e1 IHe1 [|p|//] f f';
-    (case=> m ff'; [congr inv|]; congr exp; exact: IHe1).
+- by move=> R e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1.
+- by move=> R e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1.
+- by move=> R e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1.
+- by move=> e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1.
+- by move=> e1 IHe1 n f f' invb m ff'; congr exp; exact: IHe1.
+- by move=> e1 IHe1 [|p|//] f f' invb m ff'; congr exp; exact: IHe1.
 - by move=> R e1 IHe1 f f' invb m ff'; exact: IHe1.
 - move=> p e IHe f f'.
   by case=> m ff'; [congr inv|]; congr add; rewrite ?ff'//; exact: IHe.
@@ -665,18 +659,22 @@ move: invb f; elim e using (@RExpr_ind' P P0); rewrite {R e}/P {}/P0 //=.
   by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb.
 - move=> e1 IHe1 e2 IHe2 invb f; rewrite rmorphM invfM.
   by rewrite (IHe1 true) (IHe2 true) (IHe1 false) (IHe2 false); case: invb.
-- by move=> R e1 IHe1 n invb f; rewrite rmorphXn (IHe1 false) -large_nat_N_nat.
-- by move=> R e1 IHe1 n invb f; rewrite rmorphXn (IHe1 false) -large_nat_N_nat.
-- move=> R e1 IHe1 n invb f.
-  rewrite fmorphV rmorphXn (IHe1 false) -large_nat_N_nat.
-  by case: invb; [congr (_ ^-1)|]; congr (_ ^- _); lia.
-- by move=> e1 IHe1 n invb f; rewrite rmorphXn (IHe1 false) -large_nat_N_nat.
+- move=> R e1 IHe1 n invb f; rewrite rmorphXn -exprVn.
+  by rewrite (IHe1 true) (IHe1 false) -large_nat_N_nat; case: invb.
+- move=> R e1 IHe1 n invb f; rewrite rmorphXn -exprVn.
+  by rewrite (IHe1 true) (IHe1 false) -large_nat_N_nat; case: invb.
+- move=> R e1 IHe1 n invb f; rewrite fmorphV invrK rmorphXn -exprVn.
+  rewrite (IHe1 true) (IHe1 false) -large_nat_N_nat -Nnat.N2Nat.inj_succ.
+  by case: invb.
+- move=> e1 IHe1 n invb f; rewrite rmorphXn -exprVn.
+  by rewrite (IHe1 true) (IHe1 false) -large_nat_N_nat; case: invb.
 - move=> e1 IHe1 n invb f.
   have ->: (Reval e1 ^ n)%num = Reval e1 ^+ N.to_nat n by lia.
-  by rewrite rmorphXn (IHe1 false).
-- move=> e1 IHe1 [|p|p] invb f; rewrite ?(rmorph0, rmorph1, invr0, if_same) //=.
-  by case: invb; rewrite /Fnorm; [congr (_ ^-1)|];
-    rewrite -[X in X ^+ _](IHe1 false) -rmorphXn/=; congr (f _); lia.
+  by rewrite rmorphXn -exprVn (IHe1 true) (IHe1 false); case: invb.
+- move=> e1 IHe1.
+  case=> [|p|p] invb f; rewrite ?(rmorph0, rmorph1, invr0, invr1, if_same) //=.
+  rewrite /Fnorm -[X in X ^+ _](IHe1 invb) (fun_if (fun x => GRing.exp x _)).
+  by rewrite exprVn /= -rmorphXn; case: invb; [congr (_ ^-1)|]; congr (f _); lia.
 - by move=> R e1 IHe1 invb f; rewrite fmorphV invrK -if_neg IHe1.
 - move=> p e1 IHe1 invb f.
   by rewrite add_pos_natE rmorphD (IHe1 false) -[Pos.to_nat p]natn rmorph_nat.