Stream: Coq users

Topic: apply command?


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

view this post on Zulip sara lee (Sep 11 2021 at 07:00):

(deleted)

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

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

view this post on Zulip Gaƫtan Gilbert (Sep 11 2021 at 11:39):

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

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

view this post on Zulip sara lee (Sep 11 2021 at 12:22):

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

view this post on Zulip Karl Palmskog (Sep 11 2021 at 12:24):

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

view this post on Zulip sara lee (Sep 11 2021 at 12:25):

Difference between inversion Hf & contradict Hf.

view this post on Zulip Karl Palmskog (Sep 11 2021 at 12:26):

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

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

view this post on Zulip Karl Palmskog (Sep 11 2021 at 12:30):

for example, auto with arith.

view this post on Zulip sara lee (Sep 11 2021 at 12:31):

I have applied but no change occur.

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

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

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

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

view this post on Zulip sara lee (Sep 11 2021 at 12:45):

yes. it works. Thank you.

view this post on Zulip sara lee (Sep 11 2021 at 12:46):

(deleted)


Last updated: Feb 08 2023 at 23:03 UTC