Skip to content

Instantly share code, notes, and snippets.

@davidad
Created August 30, 2018 03:34
Show Gist options
  • Save davidad/15b18046d16ff265c59837b95437de93 to your computer and use it in GitHub Desktop.
Save davidad/15b18046d16ff265c59837b95437de93 to your computer and use it in GitHub Desktop.
Require Import Coq.Lists.List Coq.Relations.Relations Coq.Sorting.Sorted.
Require Import Coq.Program.Equality Psatz.
Lemma Sorted_iff_by_explicit_indices {A} {R: relation A} (l: list A):
Sorted R l <-> forall n, (S n) < length l -> exists d,
R (nth n l d) (nth (S n) l d).
Proof with (cbn in *; firstorder).
split; induction l; intros.
- unshelve esplit; contradict H0...
- unshelve esplit; intuition; inversion H.
induction n.
+ destruct H4...
+ intros...
assert (S n < length l) by intuition.
destruct (H5 n H6).
do 2 rewrite (nth_indep l a x) by intuition.
trivial.
- intuition.
- apply Sorted_cons.
+ apply IHl; intros.
apply (H (S n))...
+ induction l...
apply HdRel_cons.
pose proof (H 0 ltac:(cbn;intuition))...
Qed.
Theorem rev_asc_desc {A} {R: relation A} (l: list A):
(Sorted R l) -> (Sorted (transp _ R) (rev l)).
Proof.
repeat rewrite Sorted_iff_by_explicit_indices.
intros; destruct l.
- contradict H0; firstorder.
- rewrite rev_length in H0.
set (L := length (a :: l)) in *.
pose (m := L - S (S n)).
assert ((S m) < L) by (unfold m; intuition).
destruct (H m H1); exists x.
do 2 rewrite rev_nth by intuition; fold L m.
replace (L - S n) with (S m); unfold m; intuition.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment