Reduction surgery

A tactic fine tuning cbv with a list of allowed unfoldings taken from a module: it mocks up a reduction tactic unfolding only constants from a given module.
From elpi Require Import elpi.
[Loading ML file ppx_deriving.runtime (implicit dependency) ... done]
[Loading ML file re (implicit dependency) ... done]
[Loading ML file re.str (implicit dependency) ... done]
[Loading ML file elpi.util (implicit dependency) ... done]
[Loading ML file elpi.lexer_config (implicit dependency) ... done]
[Loading ML file menhirLib (implicit dependency) ... done]
[Loading ML file stdlib-shims (implicit dependency) ... done]
[Loading ML file elpi.parser (implicit dependency) ... done]
[Loading ML file camlp-streams (implicit dependency) ... done]
[Loading ML file easy-format (implicit dependency) ... done]
[Loading ML file biniou (implicit dependency) ... done]
[Loading ML file yojson (implicit dependency) ... done]
[Loading ML file atdgen-runtime (implicit dependency) ... done]
[Loading ML file elpi.trace.atd (implicit dependency) ... done]
[Loading ML file elpi.trace.runtime (implicit dependency) ... done]
[Loading ML file elpi.runtime (implicit dependency) ... done]
[Loading ML file elpi.compiler (implicit dependency) ... done]
[Loading ML file elpi (implicit dependency) ... done]
[Loading ML file rocq-elpi.elpi ... done]



Elpi Tactic reduce.
Elpi Accumulate lp:{{

pred gref->redflag gref -> coq.redflag.
gref->redflag (const C) (coq.redflags.const C).

solve (goal _ _ Ty _ [str M] as G) GS :-
  coq.locate-module M MP,
  coq.env.module MP GREFS,
  std.map-filter GREFS (x\r\x = gref r, r = (const _)) CONSTANTS,
  std.map CONSTANTS (gr\r\ coq.env.transitive-dependencies gr _ r) DEPS,
  std.fold DEPS {coq.gref.set.empty} coq.gref.set.union ALLDEPS,
  std.append CONSTANTS {coq.gref.set.elements ALLDEPS} All,
  std.map-filter All gref->redflag DELTAFLAGS,
  coq.redflags.add coq.redflags.nored
    [ coq.redflags.beta, coq.redflags.fix, coq.redflags.match | DELTAFLAGS ]
    F,
  (@redflags! F ==> coq.reduction.cbv.norm Ty Ty1),
  refine {{ _ : lp:Ty1 }} G GS. % to leave a vmcast one needs to call ltac1

}}.
Module ToRed.
Interactive Module ToRed started

Definition x := 1.
x is defined

Definition y := 1.
y is defined

Definition alias := plus.
alias is defined

End ToRed.
Module ToRed is defined

Goal ToRed.x + ToRed.y = let z := 1 in S z.
1 goal
  
  ============================
  ToRed.x + ToRed.y = (let z := 1 in S z)

elpi reduce "ToRed".
1 goal
  
  ============================
  2 = (let z := 1 in S z)

match goal with |- 2 = let z := 1 in S z => trivial end.
No more goals.

Show Proof.
(eq_refl : 2 = (let z := 1 in S z))

Abort.