## Stream: Coq users

### Topic: apply command?

#### sara lee (Sep 11 2021 at 06:59):

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)

#### Karl Palmskog (Sep 11 2021 at 07:40):

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.
``````

#### sara lee (Sep 11 2021 at 11:37):

``````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.
``````

#### Gaëtan Gilbert (Sep 11 2021 at 11:39):

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

#### Karl Palmskog (Sep 11 2021 at 12:19):

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.

#### sara lee (Sep 11 2021 at 12:22):

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

#### Karl Palmskog (Sep 11 2021 at 12:24):

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

#### sara lee (Sep 11 2021 at 12:25):

Difference between inversion Hf & contradict Hf.

#### Karl Palmskog (Sep 11 2021 at 12:26):

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

#### sara lee (Sep 11 2021 at 12:29):

Ok , thank you. One more question if Hf : false = false
goal: ~ S n < 1 . How to finish this goal.

#### Karl Palmskog (Sep 11 2021 at 12:30):

for example, `auto with arith`.

#### sara lee (Sep 11 2021 at 12:31):

I have applied but no change occur.

#### Karl Palmskog (Sep 11 2021 at 12:32):

the following works for me at least:

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

#### Karl Palmskog (Sep 11 2021 at 12:36):

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.

#### sara lee (Sep 11 2021 at 12:38):

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

#### Karl Palmskog (Sep 11 2021 at 12:43):

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.
``````

#### sara lee (Sep 11 2021 at 12:45):

yes. it works. Thank you.

#### sara lee (Sep 11 2021 at 12:46):

(deleted)

Last updated: Jun 18 2024 at 21:01 UTC