a : nat

H : (0 <? a) = false

______________________________________(1/1)

goal: ~ 0 < a . It should be solve by eauto. But this command is not working. What command I should apply under these conditions.

(deleted)

Coq doesn't conflate booleans (`bool`

with members `true`

and `false`

) and propositions (`Prop`

). See here for a general discussion of this. Here is one lengthy way to prove the goal that should give an idea what is going on (`Nat.ltb_nlt`

from Stdlib already proves it) :

```
Require Import Arith.
Lemma my_ltb_nlt a : (0 <? a) = false -> ~ 0 < a.
Proof.
intro Hf.
unfold Nat.ltb in Hf.
simpl in Hf.
destruct a.
- auto with arith.
- congruence.
Qed.
```

```
Lemma my_ltb_nlt_r a : ~ 0 < a->
(0 <? a) = false .
Proof.
intro Hf.
unfold Nat.ltb .
simpl .
destruct a.
auto with arith.
unfold not in Hf.
```

https://coq.zulipchat.com/help/format-your-message-using-markdown#code

there's typically not any reason to unfold `not`

. For example, replacing the `unfold`

with `contradict Hf. auto with arith.`

is one way to finish the proof.

When apply - inversion Hf. I get "The type of Hf is not inductive."

yes, you can see I corrected to `contradict Hf. auto with arith.`

.

Difference between inversion Hf & contradict Hf.

https://coq.inria.fr/refman/proof-engine/tactics.html

Ok , thank you. One more question if Hf : false = false

goal: ~ S n < 1 . How to finish this goal.

for example, `auto with arith`

.

I have applied but no change occur.

the following works for me at least:

```
Goal forall n, ~ S n < 1.
intros n.
auto with arith.
Qed.
```

generally, we recommend users to follow a tutorial or book to memorize a basic set of tactics, since there are so many. See here for a list of books. Software Foundations vol 1 is a common recommendation.

what could be the reason that i cannot close goal .Although I have copied above goal .( auto with arith. is not working).

I might have had loaded some more machinery. The following should work in any context:

```
Require Import Arith.
Goal forall n, ~ S n < 1.
intros n.
apply Nat.nlt_succ_r.
auto with arith.
Qed.
```

yes. it works. Thank you.

(deleted)

Last updated: Jun 18 2024 at 21:01 UTC