diff options
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/Permutation.v | 26 | ||||
| -rw-r--r-- | theories/Sorting/Sorted.v | 11 |
2 files changed, 33 insertions, 4 deletions
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 45fb48ad5d..2bf54baef3 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -535,6 +535,32 @@ Proof. now apply Permutation_cons_inv with x. Qed. +Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + +Lemma Permutation_count_occ l1 l2 : + Permutation l1 l2 <-> forall x, count_occ eq_dec l1 x = count_occ eq_dec l2 x. +Proof. + split. + - induction 1 as [ | y l1 l2 HP IHP | y z l | l1 l2 l3 HP1 IHP1 HP2 IHP2 ]; + cbn; intros a; auto. + + now rewrite IHP. + + destruct (eq_dec y a); destruct (eq_dec z a); auto. + + now rewrite IHP1, IHP2. + - revert l2; induction l1 as [|y l1 IHl1]; cbn; intros l2 Hocc. + + replace l2 with (@nil A); auto. + symmetry; apply (count_occ_inv_nil eq_dec); intuition. + + assert (exists l2' l2'', l2 = l2' ++ y :: l2'') as [l2' [l2'' ->]]. + { specialize (Hocc y). + destruct (eq_dec y y); intuition. + apply in_split, (count_occ_In eq_dec). + rewrite <- Hocc; apply Nat.lt_0_succ. } + apply Permutation_cons_app, IHl1. + intros z; specialize (Hocc z); destruct (eq_dec y z) as [Heq | Hneq]. + * rewrite (count_occ_elt_eq _ _ _ Heq) in Hocc. + now injection Hocc. + * now rewrite (count_occ_elt_neq _ _ _ Hneq) in Hocc. + Qed. + End Permutation_properties. Section Permutation_map. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 206eb606d2..422316d879 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -71,6 +71,7 @@ Section defs. (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> forall l:list A, Sorted l -> P l. Proof. + intros P ? ? l. induction l. firstorder using Sorted_inv. firstorder using Sorted_inv. Qed. @@ -78,7 +79,8 @@ Section defs. Proof. split; [induction 1 as [|a l [|]]| induction 1]; auto using Sorted, LocallySorted, HdRel. - inversion H1; subst; auto using LocallySorted. + match goal with H1 : HdRel a (_ :: _) |- _ => inversion H1 end. + subst; auto using LocallySorted. Qed. (** Strongly sorted: elements of the list are pairwise ordered *) @@ -90,7 +92,7 @@ Section defs. Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) -> StronglySorted l /\ Forall (R a) l. Proof. - intros; inversion H; auto. + intros a l H; inversion H; auto. Defined. Lemma StronglySorted_rect : @@ -99,7 +101,7 @@ Section defs. (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> forall l, StronglySorted l -> P l. Proof. - induction l; firstorder using StronglySorted_inv. + intros P ? ? l; induction l; firstorder using StronglySorted_inv. Defined. Lemma StronglySorted_rec : @@ -120,7 +122,8 @@ Section defs. Lemma Sorted_extends : Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l. Proof. - intros. change match a :: l with [] => True | a :: l => Forall (R a) l end. + intros H a l H0. + change match a :: l with [] => True | a :: l => Forall (R a) l end. induction H0 as [|? ? ? ? H1]; [trivial|]. destruct H1; constructor; trivial. eapply Forall_impl; [|eassumption]. |