I am writing and proving lemma,

```
Lemma rt_state: forall l,
0 = 1 mod (length l)->
length l =1.
```

But error message is " Cannot infer the implicit parameter A of

length whose type is "Type"."

This will work:

```
Lemma rt_state: forall (A : Type) (l : list A),
0 = 1 mod (length l)->
length l =1.
```

auto with arith will solve it ?

sara lee said:

auto with arith will solve it ?

IMO it's not provable – try the lemma statement with an empty `l`

.

In Coq, `4/0`

and `4 mod 0`

evaluate to 0, but this is a convention, in order to make `div`

and `modulo`

total functions.

Perhaps it would be better to add an hypothesis (l <> nil) to your statement.

Actually, `4 mod 0`

evaluates to `4`

nowadays, so that the definitional equality of `div`

and `mod`

always holds, even for a zero divisor.

Ah Ok ! I was using 8.13 !

https://github.com/coq/coq/pull/14086

Ok ,If I add hypothesis that l <> nil then it is provable ? Now

```
Lemma rt_state: forall (A : Type) (l : list A),
l <> nil ->
0 = 1 mod (length l)->
length l =1.
```

sara lee said:

Ok ,If I add hypothesis that l <> nil then it is provable ? Now

`Lemma rt_state: forall (A : Type) (l : list A), l <> nil -> 0 = 1 mod (length l)-> length l =1.`

My bad: it seems provable with or *without* that extra hypothesis on Coq *8.14.0* where `1 mod 0`

is `1`

.

I mentioned it not provable before since I had in mind the 8.12.0 version of `modulo`

where `1 mod 0`

is `0`

. Sorry for that.

Right. In maths , 1 mod 1 or n mod n=0 . If I compare this with above then only reason for answer to be zero is the natural number (length l)=1.

Last updated: Jun 18 2024 at 00:02 UTC