Stream: Coq users

Topic: solving exists statements with coq-hammer

view this post on Zulip Ben Siraphob (Apr 15 2022 at 02:03):

For some reason, coq-hammer can't solve the following simple goal with exists (I have all supported ATPs installed).

From Hammer Require Import Hammer.
From Hammer Require Import Tactics.
Require Import ZArith.
Open Scope Z_scope.
Goal exists (n : Z), n + 50 > 100.
hammer.

What is the reason for this and how can I solve such goals automatically? I know that Z3 can easily find n = 51 for instance.

Last updated: Sep 23 2023 at 13:01 UTC