## Stream: Coq users

### Topic: Equal to 1

#### sara lee (Dec 19 2021 at 17:19):

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

#### Karl Palmskog (Dec 19 2021 at 17:20):

This will work:

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

#### sara lee (Dec 21 2021 at 15:18):

auto with arith will solve it ?

#### Gleb (Dec 22 2021 at 06:59):

sara lee said:

auto with arith will solve it ?

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

#### Pierre Castéran (Dec 22 2021 at 09:05):

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.

#### Guillaume Melquiond (Dec 22 2021 at 10:08):

Actually, `4 mod 0` evaluates to `4` nowadays, so that the definitional equality of `div` and `mod` always holds, even for a zero divisor.

#### Pierre Castéran (Dec 22 2021 at 10:21):

Ah Ok ! I was using 8.13 !
https://github.com/coq/coq/pull/14086

#### sara lee (Dec 22 2021 at 12:55):

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

#### Gleb (Dec 22 2021 at 18:16):

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.

#### sara lee (Dec 22 2021 at 18:42):

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: Sep 28 2023 at 11:01 UTC