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.

sara lee (Sep 11 2021 at 07:00):

(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: Apr 19 2024 at 18:01 UTC