You can see a complete example code at the bottom of the post.

Many usual computer algebra systems, for example Sage Math, have a feature of solving an equation over a field for a variable. That is to say, they can invert functions. But they do not give you any proof. Also, Sage Math in particular seems to have a less powerful language in comparison to Coq, The example I have seems to be out of reach for its symbolic algebra engine because it uses a record type — even though this type is immediately projected into real numbers.

So, the question is whether Coq can find these inverses automatically. I know and use some automation tactics like `tauto`

and `field`

, but they do not seem to be useful when a whole new formula is needed — even if any college student can derive this formula in 5 minutes. I understand that finding inverses to arbitrary functions is a hard problem, but in this case it is merely a formula in a field over some variables.

Are there some more powerful automation tactics that can help me here? Maybe I need to configure `auto`

with a strong hint data base? I tried to give it more axioms and increase depth, but it does not seem to work.

In this example, `R_inverse`

is the function I would like to find automatically.

```
From Coq Require Import Unicode.Utf8.
From Coq Require Import Logic.Decidable.
From Coq Require Import Reals.
Definition ℕ := nat.
Definition ℙ := Prop.
Definition 𝔹 := bool.
Notation ℝ := R.
Record Unit: Set :=
makeUnit
{ health: ℝ
; damage: ℝ
}.
Open Scope R_scope.
Definition R (c: Unit → Unit → ℝ) (x: Unit) (y: Unit) (t: ℝ): ℝ := 1 - (damage y / health x) * (t + c x y).
Definition R_inverse (c: Unit → Unit → ℝ) (x: Unit) (y: Unit) (r: ℝ): ℝ := (health x * (1 - r)) / damage y - c x y.
Lemma inverse_of_R: ∀ c x y, health x ≠ 0 ∧ damage y ≠ 0 → ∃ R_inverse, ∀ r, R c x y (R_inverse c x y r) = r.
Proof.
intros.
exists R_inverse.
intros.
unfold R, R_inverse.
field. tauto.
Qed.
```