There is a way to generate the identity function:

```
Definition g1 (x: ℝ): ℝ := ltac:(auto).
```

I can write a constant function by hand:

```
Definition g2 (x: ℝ): {y: ℝ | y = 3} := ltac:(exact (exist _ 3 eq_refl)).
```

How can I use `auto`

to generate such constant functions for me?

If I put `auto`

there, I shall receive an error:

```
Definition g2 (x: ℝ): {y: ℝ | y = 3} := ltac:(auto).
Error:
The following term contains unresolved implicit arguments:
(λ x : ℝ, ?Goal)
More precisely:
- ?Goal: Cannot infer an existential variable of type "{y : ℝ | y = 3}" in
environment:
x : ℝ
```

But if I put `eauto`

there instead, it will successfully generate the constant for me! Awesome!

What I really want to do is make Coq generate inverse functions for me, as I asked about elsewhere recently. For example, see:

```
Definition g4 (x: ℝ): {y | f y = x}.
Proof. unfold f. refine (exist _ (x - 1) _). field. Qed.
Example example_1: (f (proj1_sig (g4 13))) = 13.
Proof. pose proof (proj2_sig (g4 13)). simpl in H. assumption.
```

Seems to work.

Unfortunately, I have no idea how to actually compute anything with this Σ thing.

```
Compute (proj1_sig (g4 13)).
= let (x, _) := g4 (R1 + (R1 + R1) * ((R1 + R1) * (R1 + (R1 + R1)))) in x
: ℝ
```

How is this the expected number 13?

Your definition `g4`

is opaque (due to `Qed`

). If you want to compute with it, you have to make it transparent by terminating it with `Defined`

.

Oh, right! Thanks!

So, I can define functions that return values with associated proofs. But how can I automate this? This is where I am:

```
Definition g6 (x: ℤ): {y | f y = x}.
Proof.
unfold f. refine (exist _ _ _).
(* x : ℤ *)
(* ============================ *)
(* ?Goal + 1 = x *)
assert (x - 1 + 1 = x). ring. exact H.
Qed.
```

I would like to use `auto`

on the `?Goal`

existential variable. For some reason, `instantiate`

does not work:

```
instantiate (Goal := x - 1).
Error: Unknown existential variable.
```

How do I do this?

Here `f`

is simply this:

```
Definition f (x: ℤ): ℤ := x + 1.
```

This also does not work:

```
assert (ltac:(auto)).
Error: The reference auto was not found in the current environment.
```

I should use `eauto`

whenever there are some suspicious interdependent goals in sight. I am not sure how this works, but for example:

```
Definition g6 (x: ℤ): {y | f y = x}.
Proof. unfold f. eexists. eauto using Z.sub_add. Qed.
```

Or even:

```
Definition g6 (x: ℤ): {y | f y = x} := ltac:(eauto using Z.sub_add).
```

So, the issue is to provide the right set of theorems to `eauto`

.

Last updated: Jun 18 2024 at 09:02 UTC