Stream: Coq users

Topic: Finding expression bounds


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

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC