Magic number `100%N` used as "fuel" in reflexive normalization (?)

[pi8027]

I should investigate this at some point, but I'm not sure if 100 is large enough:

algebra-tactics/theories/ring.v

Line 654 in 0b8356c

refine (@ring_correct R 100%N VarMap Lpe RE1 RE2 PE1 PE2 LpeProofs

Coq uses 1000 instead:
https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/theories/setoid_ring/Ring_tac.v#L340

I think we should at least give a constant name to this number as in Coq.

[gares]

ring 1000: H?

[pi8027]

@gares I don't think letting the user specify this number for every tactic call is very useful. If I should make it configurable, I would do that through a tactic that returns this number.

@thery What do you think? Is it useful if this number is configurable?

[thery]

Oh my god no 😱 Could you use some binary encoding so to give as fuel something really big.

[thery]

I remember in Buchberger I was using some fuel with a double recursion.

type ’a rp = Stop of ’a | More of ’a
let rec iter_rp n f v = match v with
| More r -> match n with
               | O -> f r
               | S n1 -> iter_rp n1 f (iter_rp n1 f v)
              end
| _ -> v
end

[pi8027]

The actual code that requires this fuel is, I guess, these functions in setoid_ring: https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/theories/setoid_ring/Ring_polynom.v#L467-L499

I'm not going to change them. But, it seems to me that (10*10*10)%nat is an effective technique to reduce the term size, including those obtained during reduction.

[thery]

is this the code that handles the substitution of H1 in ring [H1]? Can you try x^101 = 1 with H1 : x = 1?

[pi8027]

is this the code that handles the substitution of H1 in ring [H1]?

Yes, I think so, and my main problem is that I have no idea how big this fuel should be.

Can you try x^101 = 1 with H1 : x = 1?

It works without any problem:

Goal forall (R : comRingType) (x : R), x = 1 -> x ^+ 101 = 1.
Proof. by move=> R x; ring. Qed.

Goal forall (R : comRingType) (x : R), x = 1 -> x ^+ 10000 = 1.
Proof. by move=> R x; ring. Qed.

[thery]

you don't need to say explicitely to use the assumption?

[pi8027]

If the goal is implication P1 -> ... -> Pn -> Q, my ring tactic uses P1 ... Pn as assumptions.

[thery]

this is dangerous! x = x^2 -> x = x ring will use all the fuel.

[pi8027]

Aha, I thought it was more intelligent. I will try to produce such an example.