Ignat Insarov (Mar 26 2021 at 13:42): 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.
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: Sep 28 2023 at 11:01 UTC