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

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

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

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)

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

It might work if you used `<=`

rather than `>=`

, but it's surprising that `>=`

is not declared transitive.

This probably suggests that you should use `<=`

.

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 .

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`

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

I think he meant square brackets to mean optional. Either `unfold ge.`

or `unfold ge in count_occ.`

.

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

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

However unfold ">=" works. Thank u.

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?

Now `apply H0`

should help.

still error message " no witness found".

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.

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

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

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