Stream: Coq users

Topic: error message

view this post on Zulip sara lee (Nov 17 2021 at 10:53):

I have a function f whose input arguments are two nat and list nat l. Output of this function is list nat. To close the goal,I am applying command "rewrite H0" but have error message.I don't know why this happen(only change in nat values and I have that value in hypothesis).

H0:     length l > 0 ->
          list_max l <> 0 ->
          nth 0 l 0 > nth k2 l 0 ->
          nth 0 l 0 > nth (S k2) l 0 ->
  count_occ Nat.eq_dec (f 0 2 l) 0 >= count_occ Nat.eq_dec (f 0 2 l) (S k2)->
S (count_occ Nat.eq_dec (f 1 2 l) 0) >=  (count_occ Nat.eq_dec (f 1 2 l) (S k2)).
 H1:      length l > 0 ->
          list_max l <> 0 ->
          nth 0 l 0 > nth (S k2) l 0 ->
          nth 0 l 0 > nth  (S(S k2)) l 0 ->
  count_occ Nat.eq_dec (f 0 2 l) 0 >= count_occ Nat.eq_dec (f 0 2 l) (S(S k2)).


Goal: S (count_occ Nat.eq_dec (f 1 2 l) 0) >= (count_occ Nat.eq_dec (f 1 2 l) (S(S k2)).

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 11:32):

rewrite usually takes equalities not inequalities. “apply H0” makes more sense, but it will tell you that the conclusion of H0 does not match…

view this post on Zulip Paolo Giarrusso (Nov 17 2021 at 11:34):

The only obvious step I see is “etransitivity. apply H0.”; that should succeed. Whether it helps your proof, dunno.

view this post on Zulip sara lee (Nov 17 2021 at 11:49):

Tactic failure: The relation ge is not a declared transitive relation. Maybe you need to require the Coq.Classes.RelationClasses library.(I have CoqIDE 8.8.0)

view this post on Zulip sara lee (Nov 17 2021 at 16:11):

I have installed 8.14.0. But still I get above error message .

view this post on Zulip Théo Winterhalter (Nov 17 2021 at 16:13):

It might work if you used <= rather than >=, but it's surprising that >= is not declared transitive.
This probably suggests that you should use <=.

view this post on Zulip sara lee (Nov 17 2021 at 18:11):

I am applying " etransitivity. apply H0." as a result I get above error message. Now how and where I should use <= relation instead of >= relation? Secondly I have >= relation between two terms. This is the right way to solve or have any other .

view this post on Zulip Pierre Castéran (Nov 18 2021 at 09:45):

The Arithlibrary contains much more lemmas on le than ge. Just compare the answers to Search lewith Search ge.
But ge is defined simply in terms of le. With red [in ...]or unfold ge [in ...], you can convert your x >= yinto y <= x, then call etransitivity

view this post on Zulip sara lee (Nov 18 2021 at 15:30):

unfold ge [in ...] means unfold ge [in f] or unfold ge [in count_occ]. I have tried both unfold ge [in ...] but get error message "Syntax error: [unfold_occ] expected after 'unfold' (in [simple_tactic])".

view this post on Zulip Théo Winterhalter (Nov 18 2021 at 16:01):

I think he meant square brackets to mean optional. Either unfold ge. or unfold ge in count_occ..

view this post on Zulip Théo Winterhalter (Nov 18 2021 at 16:01):

Note you can also do unfold ">=".

view this post on Zulip sara lee (Nov 18 2021 at 16:38):

When apply "unfold ge in count_occ ". Error message " No such hypothesis: count_occ"

view this post on Zulip sara lee (Nov 18 2021 at 16:58):

However unfold ">=" works. Thank u.

view this post on Zulip sara lee (Nov 18 2021 at 17:16):

Goal: S (count_occ Nat.eq_dec (f 1 2 l) 0) >= (count_occ Nat.eq_dec (f 1 2 l) (S(S k2)) after applying unfold >= & etransitivity , I get these two sub gols.
(count_occ Nat.eq_dec (f 1 2 l) (S(S k2)) <=? y
?y <= S (count_occ Nat.eq_dec (f 1 2 l) 0). However closing goal with the help of H0 and H1 is still not possible.How I can close goal with the help of hypothesis?

view this post on Zulip Paolo Giarrusso (Nov 19 2021 at 09:39):

Now apply H0 should help.

view this post on Zulip sara lee (Nov 19 2021 at 16:56):

still error message " no witness found".

view this post on Zulip Michael Soegtrop (Nov 19 2021 at 17:27):

This goal is not provable from what you show us. You want to prove something about (count_occ Nat.eq_dec (f 1 2 l) (S(S k2))but your hypothesis are about count_occ Nat.eq_dec (f 0 2 l) (S(S k2)) or (count_occ Nat.eq_dec (f 1 2 l) (S k2)) so either the first or second argument of count_occ is different.

Assuming you have hypothesis from which the goal follows by the rules of linear arithmetic and inequalities, you can use the lia tactic to prove it. There is rarely a need to handle things like transitivity of nat or Z directly.

view this post on Zulip sara lee (Nov 19 2021 at 17:52):

Simplify the statement like below still not provable? 

H1: nth k1 (a :: l) 0 >  nth (S k2) (a :: l) 0

IHs2 : nth k1 (a :: l) 0 > nth k2 (a :: l) 0 ->
count_occ Nat.eq_dec (f 0 2 l) k1  >=  count_occ Nat.eq_dec (f 0 2 l) k2.

goal: count_occ Nat.eq_dec (f 0 2 l) k1 >=count_occ Nat.eq_dec (f 0 2 l) (S k2).

error: Unable to unify
 "count_occ Nat.eq_dec (f 0 2 (a::l)) k2 <=
  count_occ Nat.eq_dec (f 0 2 (a::l)) k1"   with
"count_occ Nat.eq_dec (f 0 2 (a::l) (S k2) <= ?y".

view this post on Zulip Théo Winterhalter (Nov 19 2021 at 18:02):

In general, you should be able to do the proof on paper before attempting it in Coq if you are struggling with the tool.

view this post on Zulip Michael Soegtrop (Nov 20 2021 at 09:12):

From what you show us, this is not provable because with the information available count_occ Nat.eq_dec (f 0 2 l) k2and count_occ Nat.eq_dec (f 0 2 l) (S k2) are unrelated. You try to derive the occurrence count of S k2 in the list (f 0 2 l) from the occurrence count of k2 in the same list. These two numbers are totally unrelated und you can prove nothing about them unless you know something about (f 0 2 l) you are not telling us.

This has nothing to do with Coq, but with logic in general - as Théo said: you should first be able to have a proof concept before you try to prove something with a formal tool.

Last updated: Apr 20 2024 at 10:02 UTC