## Stream: Coq users

### Topic: error message

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

#### 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…

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

#### 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)

#### sara lee (Nov 17 2021 at 16:11):

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

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

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

#### Pierre Castéran (Nov 18 2021 at 09:45):

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

#### 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])".

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

#### Théo Winterhalter (Nov 18 2021 at 16:01):

Note you can also do `unfold ">=".`

#### sara lee (Nov 18 2021 at 16:38):

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

#### sara lee (Nov 18 2021 at 16:58):

However unfold ">=" works. Thank u.

#### 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?

#### Paolo Giarrusso (Nov 19 2021 at 09:39):

Now `apply H0` should help.

#### sara lee (Nov 19 2021 at 16:56):

still error message " no witness found".

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

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

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

#### 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) k2`and `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: Sep 30 2023 at 05:01 UTC