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
In this specific example, as "x < y" is defined as "x <= S y", one can use
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: Feb 06 2023 at 12:04 UTC