Possible lra bug

Using Coq
1

Hello!

It seems that lra can fail if name mangling is enabled:

Require Import Coq.Reals.Reals.
Require Import Psatz.

Open Scope R_scope.

Unset Mangle Names.

Lemma div2mult05_0 : forall r, r / 2 = r * 0.5.
Proof.
  intros r.
  lra.
Qed.

Set Mangle Names.

Lemma div2mult05_1 : forall r, r / 2 = r * 0.5.
Proof.
  intros r.
  lra.

The div2mult05_0 lemma is proven without issue. Turn on name mangling, and the same theorem fails with No applicable tactic..

2

This is a bug. It is reported here. Thanks!!

1 Like
3

@io7m just for your information. A fix has been proposed and merged to master. Hopefully it will be available soon,

4

That was fast. Thanks very much!