Hello, I'm super new to coq and I'm trying to get my feet wet. I've defined a strictly monotonic nat list and then tried to prove a simple example. But I'm stuck in the proof and I don't know what to do next... I think I have a False hypothesis `i_les_length: S (S i) < 2`

but not sure how to use it.

```
Definition strict_monotonic (l: list nat) : Prop := forall i:nat, i < (length(l)-1) -> nth i l i < nth (i+1) l (i+1).
```

```
Example trivial_sorted: strict_monotonic [1;2;3].
Proof.
unfold strict_monotonic.
intros i.
unfold length.
simpl.
intros i_les_length.
destruct i.
simpl. auto.
destruct i.
simpl. auto.
```

```
1 subgoal
i : nat
i_les_length : S (S i) < 2
______________________________________(1/1)
match i with
| 0 => 3
| 1 => S (S i)
| S (S _) => S (S i)
end <
match S (S i) + 1 with
| 0 => 1
| 1 => 2
| 2 => 3
| 3 => S (S i) + 1
| S (S (S (S _))) => S (S i) + 1
end
```

Any comment is highly appreciated!

Cheers

Using the `Search`

command with patterns such as `(S _ < S _)`

and `(_ < 0)`

you can find lemmas (lt_S_n, Nat.nlt_0_r) to simplify your hypothese (using `apply ... in ..`

) and explicit the proof of False in your context. You can then finish this case with a `destruct`

of the False hypothesis or a `contradiction`

.

At a higher level, you could also change the way you are specifying your property to simplify your proof, for instance using a computable version of the sorted predicate (then the proof would be essentially reflexivity), or by defining an inductive predicate on lists singling out the sorted ones (following the inductive structure will probably help).

a bit off topic, but we generally recommend newbies to work through (at least core exercises from) one of the books on Coq before trying their own examples. See list of books at https://github.com/coq-community/awesome-coq#books, in particular Software Foundations is often recommended.

Last updated: Jun 25 2024 at 15:02 UTC