Library strict_inc_and_dec
Require Import List.
Require Import ZArith.
Require Import quicksort.
Inductive is_strict_inc : list nat -> Prop :=
is_strict_inc_nil : is_strict_inc nil
| is_strict_inc_sing : forall (n : nat), is_strict_inc (n :: nil)
| is_strict_inc_cons : forall (l : list nat) (x y : nat),
is_strict_inc (y :: l)
-> x < y
-> is_strict_inc (x :: y :: l).
Lemma is_strict_inc_rmsnd :
forall (l : list nat) (x y : nat),
is_strict_inc (x :: y :: l)
-> is_strict_inc (x :: l).
Proof.
induction l;intros;constructor;
inversion H;inversion H2;intuition.
Qed.
Lemma in_strict_sort :
forall (l : list nat) (a x : nat),
is_strict_inc (a :: l)
-> In x l
-> a < x.
Proof.
induction l;intros;inversion H0.
subst;inversion H;assumption.
apply IHl.
eapply is_strict_inc_rmsnd;eassumption.
assumption.
Qed.
Lemma is_strict_inc_tail :
forall (l : list nat) (a : nat),
is_strict_inc (a :: l)
-> is_strict_inc l.
Proof.
intros;inversion H;[constructor | assumption].
Qed.
Lemma strict_inc_add_hd :
forall (l : list nat) (x : nat),
is_strict_inc l
-> (forall (y : nat),
In y l
-> x < y)
-> is_strict_inc (x :: l).
Proof.
induction l;intros;constructor.
apply IHl.
eapply is_strict_inc_tail;eassumption.
intros;eapply in_strict_sort;eassumption.
intuition.
Qed.
Lemma sort_NoDup_strict_inc :
forall (l : list nat),
is_sorted nat le l
-> NoDup l
-> is_strict_inc l.
Proof.
induction 1;intros;constructor.
apply IHis_sorted;inversion H1;assumption.
inversion H1;simpl in H4;intuition.
Qed.
Lemma strict_inc_NoDup :
forall (l : list nat),
is_strict_inc l
-> NoDup l.
Proof.
induction 1;constructor;try intuition;try constructor.
simpl in H1;decompose [or]H1.
intuition.
assert (y < x).
eapply in_strict_sort;eassumption.
intuition.
Qed.
Lemma rev_dec_inc_aux :
forall (l : list nat) (a : nat),
(forall (x : nat),
In x l
-> x < a)
-> is_strict_inc l
-> is_strict_inc (l ++ a :: nil).
Proof.
induction l;simpl;intros.
constructor.
destruct l;simpl.
constructor;[constructor | apply H;intuition].
constructor.
simpl in IHl;apply IHl.
intuition.
inversion H0;subst;intuition.
inversion H0;assumption.
inversion H0;assumption.
Qed.
Inductive is_strict_dec : list nat -> Prop :=
is_strict_dec_nil : is_strict_dec nil
| is_strict_dec_sing : forall (n : nat), is_strict_dec (n :: nil)
| is_strict_dec_cons : forall (l : list nat) (x y : nat),
is_strict_dec (y :: l)
-> y < x
-> is_strict_dec (x :: y :: l).
Lemma is_strict_dec_rmsnd :
forall (l : list nat) (a x : nat),
is_strict_dec (a :: x :: l)
-> is_strict_dec (a :: l).
Proof.
induction l;intros;constructor;
inversion H;inversion H2;intuition.
Qed.
Lemma strict_dec_in :
forall (l : list nat) (a x : nat),
In x l
-> is_strict_dec (a :: l)
-> x < a.
Proof.
induction l;intros;inversion H.
subst;inversion H0;assumption.
apply IHl.
assumption.
eapply is_strict_dec_rmsnd;eassumption.
Qed.
Lemma rev_dec_inc :
forall (l : list nat),
is_strict_dec l
-> is_strict_inc (rev l).
Proof.
induction l;intros;simpl.
constructor.
apply rev_dec_inc_aux.
intros;assert (In x l).
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
assumption.
apply (strict_dec_in l a x);assumption.
apply IHl;inversion H;[constructor | assumption].
Qed.
Lemma rev_inc_dec_aux :
forall (l : list nat) (x : nat),
(forall (y : nat),
In y l
-> x < y)
-> is_strict_dec l
-> is_strict_dec (l ++ x :: nil).
Proof.
induction l;intros;simpl.
constructor.
destruct l;simpl.
constructor;[constructor | apply H;intuition].
constructor.
simpl in IHl;apply IHl.
intros.
decompose [or]H1;subst;apply H;intuition.
inversion H0;assumption.
inversion H0;intuition.
Qed.
Lemma rev_inc_dec :
forall (l : list nat),
is_strict_inc l
-> is_strict_dec (rev l).
Proof.
induction l;intros;simpl.
constructor.
apply rev_inc_dec_aux.
intros;eapply in_strict_sort.
eassumption.
eapply Permutation_in.
apply Permutation_sym;apply Permutation_rev.
assumption.
apply IHl;eapply is_strict_inc_tail;eassumption.
Qed.
Lemma is_strict_dec_tail :
forall (l : list nat) (a : nat),
is_strict_dec (a :: l)
-> is_strict_dec l.
Proof.
intros;inversion H;[constructor | assumption].
Qed.
Lemma strict_dec :
forall (l : list nat) (a : nat),
(forall (x : nat),
In x l
-> x < a)
-> is_strict_dec l
-> is_strict_dec (a :: l).
Proof.
induction l;simpl;intros.
constructor.
constructor.
apply IHl;intuition.
eapply strict_dec_in;eassumption.
eapply is_strict_dec_tail;eassumption.
apply H;intuition.
Qed.
Inductive no_fst_dup : list (nat*nat) -> Prop:=
no_fst_dup_nil : no_fst_dup nil
| no_fst_dup_cons :
forall (l : list (nat*nat)) (x y : nat),
no_fst_dup l
-> (forall (z : nat), ~In (x,z) l)
-> no_fst_dup ((x,y) :: l).
Lemma fst_dup_dup :
forall (l : list (nat*nat)),
no_fst_dup l
-> NoDup l.
Proof.
induction l;intros;[|destruct a].
constructor.
constructor;[|apply IHl];inversion H;[apply (H4 n0)|];assumption.
Qed.
Inductive is_strict_dec_fst : list (nat*nat) -> Prop :=
| is_strict_dec_fst_nil : is_strict_dec_fst nil
| is_strict_dec_fst_sing : forall (n : (nat*nat)),
is_strict_dec_fst (n :: nil)
| is_strict_dec_fst_cons : forall (a b x y : nat) (l : list (nat*nat)),
x < a
-> is_strict_dec_fst ((x,y) :: l)
-> is_strict_dec_fst ((a,b) :: (x,y) :: l).
Lemma strict_dec_fst_rmsnd :
forall (l : list (nat*nat)) (a b x y : nat),
is_strict_dec_fst ((a,b) :: (x,y) :: l)
-> is_strict_dec_fst ((a,b) :: l).
Proof.
induction l;[|destruct a];intros;constructor;
inversion H;inversion H6;intuition.
Qed.
Lemma strict_dec_fst_in :
forall (l : list (nat*nat)) (a b x y : nat),
In (x,y) l
-> is_strict_dec_fst ((a,b) :: l)
-> x < a.
Proof.
induction l;simpl;intros.
intuition.
decompose [or] H.
destruct a.
inversion H0;inversion H1;intuition.
eapply IHl.
eassumption.
destruct a;eapply strict_dec_fst_rmsnd;eassumption.
Qed.
Lemma no_fst_dup_strict_dec_fst :
forall (l : list (nat*nat)),
is_strict_dec_fst l
-> no_fst_dup l.
Proof.
induction 1.
constructor.
destruct n;apply no_fst_dup_cons.
constructor.
intuition.
constructor.
assumption.
unfold not;intros.
simpl in H1;decompose [or] H1.
inversion H2;intuition.
assert (a < x).
eapply strict_dec_fst_in;eassumption.
intuition.
Qed.