## Stream: Coq users

### Topic: Is wrong statement?

#### pianke (Jun 28 2022 at 05:07):

``````H1 : length (x :: l) > 0
n : (x <? S (list_max (x :: l) + m)) = true
H2 : list_max (x :: l) <= x
``````

Is above contra statement? We can prove it false ? (l= list nat , x m are nat)

#### Pierre Castéran (Jun 28 2022 at 05:21):

No, your context is not contradictory. Take for instance `x=3` and `l=[3]`. Note that `H1`and `n` aren't truly hypotheses (because they are provable for any `x`and `l` ).

#### pianke (Jun 29 2022 at 13:37):

You have given example in which one element present in the list. If I add H3 then it become contra statement?
H3 : nth 0 (a :: l) 0 > nth (S k2) (a :: l) 0

#### James Wood (Jun 29 2022 at 13:55):

`H3` is `x > nth k2 l 0` (assuming you meant `x` rather than `a`), so `x=3; l=[2]; k2=0` should be an example. `H2` says that `x` is the maximal element of `x :: l` (because it's as big as anything in the list, and also itself in the list), so saying that `x` is bigger than some other element in the list doesn't tell you that much.

#### James Wood (Jun 29 2022 at 14:02):

You could also have `k2` be out of bounds, in which case the type of `H3` simplifies to `x > 0`, which again doesn't tell you that much. That suggests that a hypothesis of the form `_ > nth k2 l 0` should come with another hypothesis that `k2 < length l`.

#### pianke (Jun 29 2022 at 17:49):

I have k2< length l. Now x is at zero index then k2=0 is not possible.Because two indexes can not be same.Should i add hypothesis that two indexes are not same Or by default it consider that two indexed are not same. What more information i required to prove above is wrong?

#### pianke (Jun 30 2022 at 18:08):

Proof of above is possible?

#### James Wood (Jun 30 2022 at 20:25):

It's hard to know what's reasonable in your setting, but I guess the following would be contradictory:

``````list_max l <= x
nth i l 0 > x
``````

(And it happens that you don't have to worry about `i` being out of bounds for this one, because `0` is not strictly greater than anything.)

You should eventually establish the standard characterisation of `list_max`, namely that `list_max l` is greater than or equal to everything in `l`, and that for any `x` greater than or equal to everything in `l`, `x >= list_max l` too. This probably goes a long way towards proving whatever you want to prove about `list_max`.

Last updated: Jun 15 2024 at 05:01 UTC