Ivan Postolski (Jul 17 2020 at 21:17): Ivan Postolski (Jul 17 2020 at 21:17):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
Kenji Maillard (Jul 17 2020 at 21:39):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.
Kenji Maillard (Jul 17 2020 at 21:44):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).
Karl Palmskog (Jul 17 2020 at 21:46):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: Sep 30 2023 at 07:01 UTC