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

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`

).

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

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

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`

.

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?

Proof of above is possible?

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