Handle rewrite rules with binders as arguments to constructors under literals

[JasonGross]

Currently, we cannot handle rewrite rules such as

forall x, '(S x) = pred '(S (S x))

because we end up generating a pattern like forall x1 x2, x1 =? S x && x2 =? S (S x) -> 'x1 = pred 'x2, and the reification machinery does not know how to invert these equations to eliminate x:

rewriter/src/Rewriter/Rewriter/Reify.v

Lines 657 to 696 in 351f48c

	Ltac2 substitute_beq_with (base_interp_beq : constr) (only_eliminate_in_ctx : (ident * constr (* ty *) * constr (* var *)) list) (full_ctx : ident list) (term : constr) (beq : constr) (x : constr) : constr :=
	Reify.debug_wrap
	"substitute_beq_with" (fun () => fprintf "(%t) =? _ in %t" x term) ()
	Reify.should_debug_fine_grained Reify.should_debug_fine_grained (Some Message.of_constr)
	(fun ()
	=> let only_eliminate_in_ctx := List.map (fun (n, _ty, _v) => n) only_eliminate_in_ctx in
	let is_good (y : constr) :=
	match Constr.Unsafe.kind_nocast y with
	| Constr.Unsafe.Var y
	=> neg (List.mem Ident.equal y full_ctx) && List.mem Ident.equal y only_eliminate_in_ctx
	| _ => false
	end in
	let term'_y := match! term with
	| context term'[?beq' ?x' ?y]
	=> if Constr.equal_nounivs x x'
	&& is_good y
	&& (Constr.equal_nounivs beq' beq
	|| match! beq' with
	| @base.interp_beq ?base ?base_interp ?base_interp_beq ?t
	=> true
	| ?base_interp_beq' ?t
	=> if Constr.equal_nounivs base_interp_beq' base_interp_beq
	then true
	else Control.zero Match_failure
	| ?base_interp_beq' ?t1 ?t2
	=> if Constr.equal_nounivs base_interp_beq' base_interp_beq
	then true
	else Control.zero Match_failure
	end)
	then Some (term', y)
	else Control.zero Match_failure
	| _ => None
	end in
	match term'_y with
	| Some term'_y
	=> let (term', y) := term'_y in
	let term := Pattern.instantiate term' 'true in
	substitute_with term x y
	| None => term
	end).

Presumably we could write some sort of custom inversion machinery to handle these constructors? And/or we could emit better error messages than just

Error:
Uncaught Ltac2 exception:
RewriteRules.Reify.Cannot_eliminate_functional_dependencies
  (message:((fun u2 : Z =>
             existT
               (RewriteRules.Compile.rewrite_ruleTP
                  IdentifiersGENERATED.Compilers.pattern.ident.arg_types_unfolded)
               {|
                 pattern.type_of_anypattern :=
                   type.base
                     (pattern.base.type.type_base Compilers.Z *
                      pattern.base.type.type_base Compilers.Z)%pbtype;
                 pattern.pattern_of_anypattern :=
                   #Compilers.pattern_ident_Z_cast2 @
                   (#(Compilers.pattern_ident_pair
                        (pattern.base.type.type_base Compilers.zrange)
                        (pattern.base.type.type_base Compilers.zrange)) @
                    #(Compilers.pattern_ident_Literal Compilers.zrange) @
                    #(Compilers.pattern_ident_Literal Compilers.zrange)) @
                   (#Compilers.pattern_ident_Z_mul_split @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)) @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)) @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)))
               |}
               {|
                 RewriteRules.Compile.rew_should_do_again := true;
                 RewriteRules.Compile.rew_with_opt := true;
                 RewriteRules.Compile.rew_under_lets := true;
                 RewriteRules.Compile.rew_replacement :=
                   fun (t t0 : ZRange.zrange)
                     (x0 x1
                      x2 : API.expr
                             (type.base (base.type.type_base Compilers.Z)))
                   =>
                   if
                    ((0 <=? 2 ^ bitwidth - 1)%Z && (0 <=? u1)%Z &&
                     (0 <=? u2)%Z &&
                     Definitions.Z.divideb (u1 + 1) (2 ^ bitwidth - 1 + 1) &&
                     Definitions.Z.divideb (u2 + 1) (2 ^ bitwidth - 1 + 1) &&
                     (negb (u1 =? 2 ^ bitwidth - 1)%Z
                      || negb (u2 =? 2 ^ bitwidth - 1)%Z) &&
                     ZRange.zrange_beq t
                       {| ZRange.lower := 0; ZRange.upper := u1 |} &&
                     ZRange.zrange_beq t0
                       {| ZRange.lower := 0; ZRange.upper := u2 |})%bool
                   then
                    Some
                      (RewriteRules.Reify.expr_value_to_rewrite_rule_replacement
                         (@RewriteRules.Compile.reflect_ident_iota
                            Compilers.base
                            IdentifiersBasicGENERATED.Compilers.ident
                            Compilers.base_interp Compilers.baseHasNat
                            Compilers.buildIdent Compilers.buildEagerIdent
                            Compilers.toRestrictedIdent
                            Compilers.toFromRestrictedIdent
                            Compilers.invertIdent Compilers.baseHasNatCorrect
                            Compilers.try_make_base_transport_cps var) true
                         (#Compilers.ident_Z_cast2 @
                          (###{| ZRange.lower := 0; ZRange.upper := u1 |},
                           ###{| ZRange.lower := 0; ZRange.upper := u2 |}) @
                          (#Compilers.ident_Z_cast2 @
                           (###{|
                                 ZRange.lower := 0;
                                 ZRange.upper := 2 ^ bitwidth - 1
                               |},
                            ###{|
                                 ZRange.lower := 0;
                                 ZRange.upper := 2 ^ bitwidth - 1
                               |}) @
                           (#Compilers.ident_Z_mul_split @ $$x0 @ $$x1 @ $$x2))))
                   else None
               |})))