Silly question: Is there any hope of getting a variant of this to work?

```
Require Import Lia.
Goal forall n, n < 5 -> exists X, n + 3 < X /\ X = X.
intros.
eexists; split.
- lia.
- auto.
```

Obviously the goal is to get `lia`

or a similar tactic to synthesize the `X`

.

In this specific example, as "x < y" is defined as "x <= S y", one can use `unfold "<";reflexivity`

.

But I think you mean in a more general setting, you want a tactic that solves existential quantified goals over nat, like `Goal forall n, n < 5 -> exists X, n + X = 5 /\ X =X.`

? I do not know of such a tactic and I'm working on stuff where I would like something like this as well, as I'm heavily using evars to synthesise run-time functions for doing complexity theory on an programming language.

Last updated: Sep 25 2023 at 12:01 UTC