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 divand modulototal 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