## Stream: Coq users

### Topic: Use `auto` to generate Σ types?

#### Ignat Insarov (Mar 26 2021 at 13:42):

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?

#### Ignat Insarov (Mar 26 2021 at 13:49):

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!

#### Ignat Insarov (Mar 26 2021 at 14:01):

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.

#### Ignat Insarov (Mar 26 2021 at 14:05):

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?

#### Guillaume Melquiond (Mar 26 2021 at 14:15):

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

#### Ignat Insarov (Mar 26 2021 at 14:20):

Oh, right! Thanks!

#### Ignat Insarov (Mar 26 2021 at 14:40):

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?

#### Ignat Insarov (Mar 26 2021 at 14:40):

Here `f` is simply this:

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

#### Ignat Insarov (Mar 26 2021 at 14:42):

This also does not work:

``````  assert (ltac:(auto)).
``````

#### Ignat Insarov (Mar 26 2021 at 16:09):

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

#### Ignat Insarov (Mar 26 2021 at 16:13):

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: Sep 28 2023 at 11:01 UTC