Stream: Coq users

Topic: Use `auto` to generate Σ types?


view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Mar 26 2021 at 14:20):

Oh, right! Thanks!

view this post on Zulip 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?

view this post on Zulip Ignat Insarov (Mar 26 2021 at 14:40):

Here f is simply this:

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

view this post on Zulip Ignat Insarov (Mar 26 2021 at 14:42):

This also does not work:

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

view this post on Zulip 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.

view this post on Zulip 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: Feb 08 2023 at 23:03 UTC