Solve an `exists` goal in a field with proof search?

Using Coq
1

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.
2

To better explain what I mean, this is how we can semi-automatically find this inverse:

Lemma move_sum: ∀ (x y z: ℝ), x + y = z ↔ x = z + (- y).
Proof with field. split; intros. subst z... subst x... Qed.

Lemma move_product: ∀ (x y z: ℝ), y ≠ 0 → x * y = z ↔ x = z * (/ y).
Proof with field; tauto. split; intros. subst z... subst x... Qed.

Lemma inverse_of_R_1: ∀ c x y, health x ≠ 0 ∧ damage y ≠ 0 → ∃ R_minus, ∀ r, R c x y (R_minus c x y r) = r: ℙ.
Proof.
  intros.
  (* We only care about the last argument of `R`, here called `g`. If we can
    invert `g`, we can invert `R` trivially. *)
  remember (R c x y) as g.
  cut (∃ f, ∀ (r: ℝ), g (f r) = r). intros. destruct H0. exists (fun _ _ _ => x0). assumption.
  (* So, `f` is the inverse of `g`. We know how to compute `f` and we are going
  to explain this to Coq presently. We use `eexists` to access the body of the
  existential clause. *)
  subst g. eexists ?[inverse].
  intros. unfold R. unfold Rminus. unfold Rdiv.
    apply move_sum. rewrite Ropp_involutive. rewrite Rplus_comm.  symmetry.
    apply move_sum. rewrite Rmult_comm. rewrite <- Rmult_assoc.
    apply move_product. apply Rinv_neq_0_compat. tauto.
    apply move_product. tauto.
    apply move_sum.
  (* Goal at this point:
    `?inverse r = (1 + - r) * / / health x * / damage y + - c x y`
    This is where we should like Coq to infer the definition of `?inverse`. But
    how do we explain that to Coq? Instead, we can do it by hand. *)
  instantiate (inverse := fun r => (1 - r) / / health x / damage y - c x y). simpl. reflexivity.
Qed.

So, there are three parts to the task:

  1. Derive the inverse function f.
  2. Instantiate the existential variable provided by eexists with f.
  3. Prove the resulting equality.

How I imagine this to be automated is like this:

  1. A hole ?inverse with the type of f is made. The type should capture that f is the inverse of R.
  2. The hole ?inverse is filled with some auto magic.
  3. The resulting function is made available in the context as f.
  4. f is given to instantiate.
  5. field proves the equality.

Unfortunately, I have no idea how to proceed with this plan.

3

Maybe the right way to go about it is this:

An example:

Definition f (x: ℤ): ℤ := x + 1.
Definition g (x: ℤ): {y | f y = x} := ltac:(eauto using Z.sub_add).
Compute (f (proj1_sig (g 10))).
    = 10
    : ℤ

The question is what options to give to eauto.

4

A first answer is that tactics that need a difficult guess followed by an easy proof are a typical candidates for tactics by reflexion: an unprove code performs the guess and simple tactic prove that the guess is correct. Canonically this guess is programmed in ltac or ocaml if heavy computations are needed. Proof automation generally can be done in ltac. The guess part could even be delegated to some computer algebra system I suppose.