Generated proof term does not unify with goal if goal contains not fully reduced fractions
The following example:
Require Import Reals.
Require Import Flocq.Core.Core.
Require Import Gappa.Gappa_tactic.
Open Scope R_scope.
Definition fix32_rnd_dn := (rounding_fixed rndDN (-32)).
Definition fix32_fmt := generic_format radix2 (FIX_exp (-32)).
Lemma Test: forall x:R, fix32_fmt x -> 0 <= x <= powerRZ 2 (-9) ->
0 <= x <= powerRZ 2 (-9) ->
Rabs
(round radix2 (FIX_exp (-32)) Zfloor
(3037000500 * powerRZ 2 (-32) + powerRZ 2 (-33) -
(x * (1518501474 * powerRZ 2 (-32)) +
(powerRZ 2 (-33) + fix32_rnd_dn x * x) * (377954992 * powerRZ 2 (-32)))) -
(3037000500 * powerRZ 2 (-32) + 0 -
(x * (1518501474 * powerRZ 2 (-32)) + (0 + x * x) * (377954992 * powerRZ 2 (-32))))) <=
powerRZ 2 (-32).
Proof.
unfold fix32_fmt.
unfold fix32_rnd_dn.
intros x Fx.
Fail gappa.
Abort.
fails with an error that the proof term and proof goal types don't match. If one simplifies both types, one sees that the reason is that gappa reduces reducible fractions and creates a proof term for the reduced fractions. This cannot be unified with the original goal.
Simplified type of generated proof term:
forall _x : R,
{| Fnum := 0; Fexp := 0 |} <= _x <= {| Fnum := 1; Fexp := -9 |} /\
_x = Generic_fmt.round radix2 (FIX.FIX_exp (-32)) rndNE _x /\
({| Fnum := 0; Fexp := 0 |} <=
Rabs
(Generic_fmt.round radix2 (FIX.FIX_exp (-32)) Raux.Zfloor
({| Fnum := 759250125; Fexp := -30 |} + {| Fnum := 1; Fexp := -33 |} -
(_x * {| Fnum := 759250737; Fexp := -31 |} +
({| Fnum := 1; Fexp := -33 |} +
Generic_fmt.round radix2 (FIX.FIX_exp (-32)) Raux.Zfloor _x * _x) *
{| Fnum := 23622187; Fexp := -28 |})) -
({| Fnum := 759250125; Fexp := -30 |} + Float1 0 -
(_x * {| Fnum := 759250737; Fexp := -31 |} +
(Float1 0 + _x * _x) * {| Fnum := 23622187; Fexp := -28 |}))) <= {| Fnum := 5; Fexp := -3 |} ->
False) -> False
Simplified type of the goal (after preparation):
forall x0 : R,
{| Fnum := 0; Fexp := 0 |} <= x0 <= {| Fnum := 1; Fexp := -9 |} /\
x0 = round radix2 (FIX_exp (-32)) rndNE x0 /\
({| Fnum := 0; Fexp := 0 |} <=
Rabs
(round radix2 (FIX_exp (-32)) Zfloor
({| Fnum := 3037000500; Fexp := -32 |} + {| Fnum := 1; Fexp := -33 |} -
(x0 * {| Fnum := 1518501474; Fexp := -32 |} +
({| Fnum := 1; Fexp := -33 |} + round radix2 (FIX_exp (-32)) Zfloor x0 * x0) *
{| Fnum := 377954992; Fexp := -32 |})) -
({| Fnum := 3037000500; Fexp := -32 |} + 0 -
(x0 * {| Fnum := 1518501474; Fexp := -32 |} +
(0 + x0 * x0) * {| Fnum := 377954992; Fexp := -32 |}))) <= {| Fnum := 5; Fexp := -3 |} ->
False) -> False : Prop
The terms match except for the reduction of numbers.
If the goal is changed such that the numbers are fully reduced, it does work.
I see if I can fix it by reducing numbers in the goal in the gappa_prepare tactic.