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!
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
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: Sep 30 2023 at 07:01 UTC