Cody Roux (Nov 25 2020 at 22:30): Cody Roux (Nov 25 2020 at 22:30):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.
Fabian Kunze (Nov 26 2020 at 07:58):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