diff options
| -rw-r--r-- | theories/Lists/List.v | 147 | ||||
| -rw-r--r-- | theories/Lists/ListDec.v | 103 | ||||
| -rw-r--r-- | theories/Lists/vo.itarget | 1 | ||||
| -rw-r--r-- | theories/Logic/FinFun.v | 400 | ||||
| -rw-r--r-- | theories/Logic/vo.itarget | 1 | ||||
| -rw-r--r-- | theories/Sorting/Permutation.v | 211 | ||||
| -rw-r--r-- | theories/Vectors/Fin.v | 36 |
7 files changed, 736 insertions, 163 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index d5d58efc7..d282fe8c3 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -522,7 +522,6 @@ Section Elts. simpl in *. apply IHn. auto with arith. Qed. - (*****************) (** ** Remove *) (*****************) @@ -1178,6 +1177,21 @@ End Fold_Right_Recursor. | x :: tl => if f x then Some x else find tl end. + Lemma find_some l x : find l = Some x -> In x l /\ f x = true. + Proof. + induction l as [|a l IH]; simpl; [easy| ]. + case_eq (f a); intros Ha Eq. + * injection Eq as ->; auto. + * destruct (IH Eq); auto. + Qed. + + Lemma find_none l : find l = None -> forall x, In x l -> f x = false. + Proof. + induction l as [|a l IH]; simpl; [easy|]. + case_eq (f a); intros Ha Eq x IN; [easy|]. + destruct IN as [<-|IN]; auto. + Qed. + (** [partition] *) Fixpoint partition (l:list A) : list A * list A := @@ -1582,6 +1596,61 @@ Section Cutting. End Cutting. +(**********************************************************************) +(** ** Predicate for List addition/removal (no need for decidability) *) +(**********************************************************************) + +Section Add. + + Variable A : Type. + + (* [Add a l l'] means that [l'] is exactly [l], with [a] added + once somewhere *) + Inductive Add (a:A) : list A -> list A -> Prop := + | Add_head l : Add a l (a::l) + | Add_cons x l l' : Add a l l' -> Add a (x::l) (x::l'). + + Lemma Add_app a l1 l2 : Add a (l1++l2) (l1++a::l2). + Proof. + induction l1; simpl; now constructor. + Qed. + + Lemma Add_split a l l' : + Add a l l' -> exists l1 l2, l = l1++l2 /\ l' = l1++a::l2. + Proof. + induction 1. + - exists nil; exists l; split; trivial. + - destruct IHAdd as (l1 & l2 & Hl & Hl'). + exists (x::l1); exists l2; split; simpl; f_equal; trivial. + Qed. + + Lemma Add_in a l l' : Add a l l' -> + forall x, In x l' <-> In x (a::l). + Proof. + induction 1; intros; simpl in *; rewrite ?IHAdd; tauto. + Qed. + + Lemma Add_length a l l' : Add a l l' -> length l' = S (length l). + Proof. + induction 1; simpl; auto with arith. + Qed. + + Lemma Add_inv a l : In a l -> exists l', Add a l' l. + Proof. + intro Ha. destruct (in_split _ _ Ha) as (l1 & l2 & ->). + exists (l1 ++ l2). apply Add_app. + Qed. + + Lemma incl_Add_inv a l u v : + ~In a l -> incl (a::l) v -> Add a u v -> incl l u. + Proof. + intros Ha H AD y Hy. + assert (Hy' : In y (a::u)). + { rewrite <- (Add_in AD). apply H; simpl; auto. } + destruct Hy'; [ subst; now elim Ha | trivial ]. + Qed. + +End Add. (********************************) (** ** Lists without redundancy *) @@ -1595,27 +1664,32 @@ Section ReDun. | NoDup_nil : NoDup nil | NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x::l). - Lemma NoDup_remove_1 : forall l l' a, NoDup (l++a::l') -> NoDup (l++l'). + Lemma NoDup_Add a l l' : Add a l l' -> (NoDup l' <-> NoDup l /\ ~In a l). + Proof. + induction 1 as [l|x l l' AD IH]. + - split; [ inversion_clear 1; now split | now constructor ]. + - split. + + inversion_clear 1. rewrite IH in *. rewrite (Add_in AD) in *. + simpl in *; split; try constructor; intuition. + + intros (N,IN). inversion_clear N. constructor. + * rewrite (Add_in AD); simpl in *; intuition. + * apply IH. split; trivial. simpl in *; intuition. + Qed. + + Lemma NoDup_remove l l' a : + NoDup (l++a::l') -> NoDup (l++l') /\ ~In a (l++l'). + Proof. + apply NoDup_Add. apply Add_app. + Qed. + + Lemma NoDup_remove_1 l l' a : NoDup (l++a::l') -> NoDup (l++l'). Proof. - induction l; simpl. - inversion_clear 1; auto. - inversion_clear 1. - constructor. - contradict H0. - apply in_or_app; destruct (in_app_or _ _ _ H0); simpl; tauto. - apply IHl with a0; auto. + intros. now apply NoDup_remove with a. Qed. - Lemma NoDup_remove_2 : forall l l' a, NoDup (l++a::l') -> ~In a (l++l'). + Lemma NoDup_remove_2 l l' a : NoDup (l++a::l') -> ~In a (l++l'). Proof. - induction l; simpl. - inversion_clear 1; auto. - inversion_clear 1. - contradict H0. - destruct H0. - subst a0. - apply in_or_app; right; red; auto. - destruct (IHl _ _ H1); auto. + intros. now apply NoDup_remove. Qed. (** Alternative characterisations of being without duplicates, @@ -1659,8 +1733,45 @@ Section ReDun. intros i j Hi Hj E. apply eq_add_S, H; simpl; auto with arith. } Qed. + (** Having [NoDup] hypotheses bring more precise facts about [incl]. *) + + Lemma NoDup_incl_length l l' : + NoDup l -> incl l l' -> length l <= length l'. + Proof. + intros N. revert l'. induction N as [|a l Hal N IH]; simpl. + - auto with arith. + - intros l' H. + destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } + rewrite (Add_length AD). apply le_n_S. apply IH. + now apply incl_Add_inv with a l'. + Qed. + + Lemma NoDup_length_incl l l' : + NoDup l -> length l' <= length l -> incl l l' -> incl l' l. + Proof. + intros N. revert l'. induction N as [|a l Hal N IH]. + - destruct l'; easy. + - intros l' E H x Hx. + destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } + rewrite (Add_in AD) in Hx. simpl in Hx. + destruct Hx as [Hx|Hx]; [left; trivial|right]. + revert x Hx. apply (IH l''); trivial. + * apply le_S_n. now rewrite <- (Add_length AD). + * now apply incl_Add_inv with a l'. + Qed. + End ReDun. +(** NoDup and map *) + +(** NB: the reciprocal result holds only for injective functions, + see FinFun.v *) + +Lemma NoDup_map_inv A B (f:A->B) l : NoDup (map f l) -> NoDup l. +Proof. + induction l; simpl; inversion_clear 1; subst; constructor; auto. + intro H. now apply (in_map f) in H. +Qed. (***********************************) (** ** Sequence of natural numbers *) diff --git a/theories/Lists/ListDec.v b/theories/Lists/ListDec.v new file mode 100644 index 000000000..48070cbfb --- /dev/null +++ b/theories/Lists/ListDec.v @@ -0,0 +1,103 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Decidability results about lists *) + +Require Import List Decidable. +Set Implicit Arguments. + +Definition decidable_eq A := forall x y:A, decidable (x=y). + +Section Dec_in_Prop. +Variables (A:Type)(dec:decidable_eq A). + +Lemma In_decidable x (l:list A) : decidable (In x l). +Proof using A dec. + induction l as [|a l IH]. + - now right. + - destruct (dec a x). + + left. now left. + + destruct IH; simpl; [left|right]; tauto. +Qed. + +Lemma incl_decidable (l l':list A) : decidable (incl l l'). +Proof using A dec. + induction l as [|a l IH]. + - left. inversion 1. + - destruct (In_decidable a l') as [IN|IN]. + + destruct IH as [IC|IC]. + * left. destruct 1; subst; auto. + * right. contradict IC. intros x H. apply IC; now right. + + right. contradict IN. apply IN; now left. +Qed. + +Lemma NoDup_decidable (l:list A) : decidable (NoDup l). +Proof using A dec. + induction l as [|a l IH]. + - left; now constructor. + - destruct (In_decidable a l). + + right. inversion_clear 1. tauto. + + destruct IH. + * left. now constructor. + * right. inversion_clear 1. tauto. +Qed. + +End Dec_in_Prop. + +Section Dec_in_Type. +Variables (A:Type)(dec : forall x y:A, {x=y}+{x<>y}). + +Definition In_dec := List.In_dec dec. (* Already in List.v *) + +Lemma incl_dec (l l':list A) : {incl l l'}+{~incl l l'}. +Proof using A dec. + induction l as [|a l IH]. + - left. inversion 1. + - destruct (In_dec a l') as [IN|IN]. + + destruct IH as [IC|IC]. + * left. destruct 1; subst; auto. + * right. contradict IC. intros x H. apply IC; now right. + + right. contradict IN. apply IN; now left. +Qed. + +Lemma NoDup_dec (l:list A) : {NoDup l}+{~NoDup l}. +Proof using A dec. + induction l as [|a l IH]. + - left; now constructor. + - destruct (In_dec a l). + + right. inversion_clear 1. tauto. + + destruct IH. + * left. now constructor. + * right. inversion_clear 1. tauto. +Qed. + +End Dec_in_Type. + +(** An extra result: thanks to decidability, a list can be purged + from redundancies. *) + +Lemma uniquify_map A B (d:decidable_eq B)(f:A->B)(l:list A) : + exists l', NoDup (map f l') /\ incl (map f l) (map f l'). +Proof. + induction l. + - exists nil. simpl. split; [now constructor | red; trivial]. + - destruct IHl as (l' & N & I). + destruct (In_decidable d (f a) (map f l')). + + exists l'; simpl; split; trivial. + intros x [Hx|Hx]. now subst. now apply I. + + exists (a::l'); simpl; split. + * now constructor. + * intros x [Hx|Hx]. subst; now left. right; now apply I. +Qed. + +Lemma uniquify A (d:decidable_eq A)(l:list A) : + exists l', NoDup l' /\ incl l l'. +Proof. + destruct (uniquify_map d id l) as (l',H). + exists l'. now rewrite !map_id in H. +Qed. diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget index 04994f593..82dd1be82 100644 --- a/theories/Lists/vo.itarget +++ b/theories/Lists/vo.itarget @@ -1,6 +1,7 @@ ListSet.vo ListTactics.vo List.vo +ListDec.vo SetoidList.vo SetoidPermutation.vo StreamMemo.vo diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v new file mode 100644 index 000000000..f070a6889 --- /dev/null +++ b/theories/Logic/FinFun.v @@ -0,0 +1,400 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Functions on finite domains *) + +(** Main result : for functions [f:A->A] with finite [A], + f injective <-> f bijective <-> f surjective. *) + +Require Import List Compare_dec EqNat Decidable ListDec. Require Fin. +Set Implicit Arguments. + +(** General definitions *) + +Definition Injective {A B} (f : A->B) := + forall x y, f x = f y -> x = y. + +Definition Surjective {A B} (f : A->B) := + forall y, exists x, f x = y. + +Definition Bijective {A B} (f : A->B) := + exists g:B->A, (forall x, g (f x) = x) /\ (forall y, f (g y) = y). + +(** Finiteness is defined here via exhaustive list enumeration *) + +Definition Full {A:Type} (l:list A) := forall a:A, In a l. +Definition Finite (A:Type) := exists (l:list A), Full l. + +(** In many following proofs, it will be convenient to have + list enumerations without duplicates. As soon as we have + decidability of equality (in Prop), this is equivalent + to the previous notion. *) + +Definition Listing {A:Type} (l:list A) := NoDup l /\ Full l. +Definition Finite' (A:Type) := exists (l:list A), Listing l. + +Lemma Finite_alt A (d:decidable_eq A) : Finite A <-> Finite' A. +Proof. + split. + - intros (l,F). destruct (uniquify d l) as (l' & N & I). + exists l'. split; trivial. + intros x. apply I, F. + - intros (l & _ & F). now exists l. +Qed. + +(** Injections characterized in term of lists *) + +Lemma Injective_map_NoDup A B (f:A->B) (l:list A) : + Injective f -> NoDup l -> NoDup (map f l). +Proof. + intros Ij. induction 1 as [|x l X N IH]; simpl; constructor; trivial. + rewrite in_map_iff. intros (y & E & Y). apply Ij in E. now subst. +Qed. + +Lemma Injective_list_carac A B (d:decidable_eq A)(f:A->B) : + Injective f <-> (forall l, NoDup l -> NoDup (map f l)). +Proof. + split. + - intros. now apply Injective_map_NoDup. + - intros H x y E. + destruct (d x y); trivial. + assert (N : NoDup (x::y::nil)). + { repeat constructor; simpl; intuition. } + specialize (H _ N). simpl in H. rewrite E in H. + inversion_clear H; simpl in *; intuition. +Qed. + +Lemma Injective_carac A B (l:list A) : Listing l -> + forall (f:A->B), Injective f <-> NoDup (map f l). +Proof. + intros L f. split. + - intros Ij. apply Injective_map_NoDup; trivial. apply L. + - intros N x y E. + assert (X : In x l) by apply L. + assert (Y : In y l) by apply L. + apply In_nth_error in X. destruct X as (i,X). + apply In_nth_error in Y. destruct Y as (j,Y). + assert (X' := map_nth_error f _ _ X). + assert (Y' := map_nth_error f _ _ Y). + assert (i = j). + { rewrite NoDup_nth_error in N. apply N. + - rewrite <- nth_error_Some. now rewrite X'. + - rewrite X', Y'. now f_equal. } + subst j. rewrite Y in X. now injection X. +Qed. + +(** Surjection characterized in term of lists *) + +Lemma Surjective_list_carac A B (f:A->B): + Surjective f <-> (forall lB, exists lA, incl lB (map f lA)). +Proof. + split. + - intros Su. + induction lB as [|b lB IH]. + + now exists nil. + + destruct (Su b) as (a,E). + destruct IH as (lA,IC). + exists (a::lA). simpl. rewrite E. + intros x [X|X]; simpl; intuition. + - intros H y. + destruct (H (y::nil)) as (lA,IC). + assert (IN : In y (map f lA)) by (apply (IC y); now left). + rewrite in_map_iff in IN. destruct IN as (x & E & _). + now exists x. +Qed. + +Lemma Surjective_carac A B : Finite B -> decidable_eq B -> + forall f:A->B, Surjective f <-> (exists lA, Listing (map f lA)). +Proof. + intros (lB,FB) d. split. + - rewrite Surjective_list_carac. + intros Su. destruct (Su lB) as (lA,IC). + destruct (uniquify_map d f lA) as (lA' & N & IC'). + exists lA'. split; trivial. + intro x. apply IC', IC, FB. + - intros (lA & N & FA) y. + generalize (FA y). rewrite in_map_iff. intros (x & E & _). + now exists x. +Qed. + +(** Main result : *) + +Lemma Endo_Injective_Surjective : + forall A, Finite A -> decidable_eq A -> + forall f:A->A, Injective f <-> Surjective f. +Proof. + intros A F d f. rewrite (Surjective_carac F d). split. + - apply (Finite_alt d) in F. destruct F as (l,L). + rewrite (Injective_carac L); intros. + exists l; split; trivial. + destruct L as (N,F). + assert (I : incl l (map f l)). + { apply NoDup_length_incl; trivial. + - now rewrite map_length. + - intros x _. apply F. } + intros x. apply I, F. + - clear F d. intros (l,L). + assert (N : NoDup l). { apply (NoDup_map_inv f), L. } + assert (I : incl (map f l) l). + { apply NoDup_length_incl; trivial. + - now rewrite map_length. + - intros x _. apply L. } + assert (L' : Listing l). + { split; trivial. + intro x. apply I, L. } + apply (Injective_carac L'), L. +Qed. + +(** An injective and surjective function is bijective. + We need here stronger hypothesis : decidability of equality in Type. *) + +Definition EqDec (A:Type) := forall x y:A, {x=y}+{x<>y}. + +(** First, we show that a surjective f has an inverse function g such that + f.g = id. *) + +(* NB: instead of (Finite A), we could ask for (RecEnum A) with: +Definition RecEnum A := exists h:nat->A, surjective h. +*) + +Lemma Finite_Empty_or_not A : + Finite A -> (A->False) \/ exists a:A,True. +Proof. + intros (l,F). + destruct l. + - left; exact F. + - right; now exists a. +Qed. + +Lemma Surjective_inverse : + forall A B, Finite A -> EqDec B -> + forall f:A->B, Surjective f -> + exists g:B->A, forall x, f (g x) = x. +Proof. + intros A B F d f Su. + destruct (Finite_Empty_or_not F) as [noA | (a,_)]. + - (* A is empty : g is obtained via False_rect *) + assert (noB : B -> False). { intros y. now destruct (Su y). } + exists (fun y => False_rect _ (noB y)). + intro y. destruct (noB y). + - (* A is inhabited by a : we use it in Option.get *) + destruct F as (l,F). + set (h := fun x k => if d (f k) x then true else false). + set (get := fun o => match o with Some y => y | None => a end). + exists (fun x => get (List.find (h x) l)). + intros x. + case_eq (find (h x) l); simpl; clear get; [intros y H|intros H]. + * apply find_some in H. destruct H as (_,H). unfold h in H. + now destruct (d (f y) x) in H. + * exfalso. + destruct (Su x) as (y & Y). + generalize (find_none _ l H y (F y)). + unfold h. now destruct (d (f y) x). +Qed. + +(** Same, with more knowledge on the inverse function: g.f = f.g = id *) + +Lemma Injective_Surjective_Bijective : + forall A B, Finite A -> EqDec B -> + forall f:A->B, Injective f -> Surjective f -> Bijective f. +Proof. + intros A B F d f Ij Su. + destruct (Surjective_inverse F d Su) as (g, E). + exists g. split; trivial. + intros y. apply Ij. now rewrite E. +Qed. + + +(** An example of finite type : [Fin.t] *) + +Lemma Fin_Finite n : Finite (Fin.t n). +Proof. + induction n. + - exists nil. + inversion a. + - destruct IHn as (l,Hl). + exists (Fin.F1 :: map Fin.FS l). + intros a. revert n a l Hl. + refine (@Fin.caseS _ _ _); intros. + + now left. + + right. now apply in_map. +Qed. + +(** Instead of working on a finite subset of nat, another + solution is to use restricted [nat->nat] functions, and + to consider them only below a certain bound [n]. *) + +Definition bFun n (f:nat->nat) := forall x, x < n -> f x < n. + +Definition bInjective n (f:nat->nat) := + forall x y, x < n -> y < n -> f x = f y -> x = y. + +Definition bSurjective n (f:nat->nat) := + forall y, y < n -> exists x, x < n /\ f x = y. + +(** We show that this is equivalent to the use of [Fin.t n]. *) + +Module Fin2Restrict. + +Notation n2f := Fin.of_nat_lt. +Definition f2n {n} (x:Fin.t n) := proj1_sig (Fin.to_nat x). +Definition f2n_ok n (x:Fin.t n) : f2n x < n := proj2_sig (Fin.to_nat x). +Definition n2f_f2n : forall n x, n2f (f2n_ok x) = x := @Fin.of_nat_to_nat_inv. +Definition f2n_n2f : forall x n h, f2n (n2f h) = x := @Fin.to_nat_of_nat. +Definition n2f_ext : forall x n h h', n2f h = n2f h' := @Fin.of_nat_ext. +Definition f2n_inj : forall n x y, f2n x = f2n y -> x = y := @Fin.to_nat_inj. + +Definition extend n (f:Fin.t n -> Fin.t n) : (nat->nat) := + fun x => + match le_lt_dec n x with + | left _ => 0 + | right h => f2n (f (n2f h)) + end. + +Definition restrict n (f:nat->nat)(hf : bFun n f) : (Fin.t n -> Fin.t n) := + fun x => let (x',h) := Fin.to_nat x in n2f (hf _ h). + +Ltac break_dec H := + let H' := fresh "H" in + destruct le_lt_dec as [H'|H']; + [elim (Lt.le_not_lt _ _ H' H) + |try rewrite (n2f_ext H' H) in *; try clear H']. + +Lemma extend_ok n f : bFun n (@extend n f). +Proof. + intros x h. unfold extend. break_dec h. apply f2n_ok. +Qed. + +Lemma extend_f2n n f (x:Fin.t n) : extend f (f2n x) = f2n (f x). +Proof. + generalize (n2f_f2n x). unfold extend, f2n, f2n_ok. + destruct (Fin.to_nat x) as (x',h); simpl. + break_dec h. + now intros ->. +Qed. + +Lemma extend_n2f n f x (h:x<n) : n2f (extend_ok f h) = f (n2f h). +Proof. + generalize (extend_ok f h). unfold extend in *. break_dec h. intros h'. + rewrite <- n2f_f2n. now apply n2f_ext. +Qed. + +Lemma restrict_f2n n f hf (x:Fin.t n) : + f2n (@restrict n f hf x) = f (f2n x). +Proof. + unfold restrict, f2n. destruct (Fin.to_nat x) as (x',h); simpl. + apply f2n_n2f. +Qed. + +Lemma restrict_n2f n f hf x (h:x<n) : + @restrict n f hf (n2f h) = n2f (hf _ h). +Proof. + unfold restrict. generalize (f2n_n2f h). unfold f2n. + destruct (Fin.to_nat (n2f h)) as (x',h'); simpl. intros ->. + now apply n2f_ext. +Qed. + +Lemma extend_surjective n f : + bSurjective n (@extend n f) <-> Surjective f. +Proof. + split. + - intros hf y. + destruct (hf _ (f2n_ok y)) as (x & h & Eq). + exists (n2f h). + apply f2n_inj. now rewrite <- Eq, <- extend_f2n, f2n_n2f. + - intros hf y hy. + destruct (hf (n2f hy)) as (x,Eq). + exists (f2n x). + split. + + apply f2n_ok. + + rewrite extend_f2n, Eq. apply f2n_n2f. +Qed. + +Lemma extend_injective n f : + bInjective n (@extend n f) <-> Injective f. +Proof. + split. + - intros hf x y Eq. + apply f2n_inj. apply hf; try apply f2n_ok. + now rewrite 2 extend_f2n, Eq. + - intros hf x y hx hy Eq. + rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal. + apply hf. + rewrite <- 2 extend_n2f. + generalize (extend_ok f hx) (extend_ok f hy). + rewrite Eq. apply n2f_ext. +Qed. + +Lemma restrict_surjective n f h : + Surjective (@restrict n f h) <-> bSurjective n f. +Proof. + split. + - intros hf y hy. + destruct (hf (n2f hy)) as (x,Eq). + exists (f2n x). + split. + + apply f2n_ok. + + rewrite <- (restrict_f2n h), Eq. apply f2n_n2f. + - intros hf y. + destruct (hf _ (f2n_ok y)) as (x & hx & Eq). + exists (n2f hx). + apply f2n_inj. now rewrite restrict_f2n, f2n_n2f. +Qed. + +Lemma restrict_injective n f h : + Injective (@restrict n f h) <-> bInjective n f. +Proof. + split. + - intros hf x y hx hy Eq. + rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal. + apply hf. + rewrite 2 restrict_n2f. + generalize (h x hx) (h y hy). + rewrite Eq. apply n2f_ext. + - intros hf x y Eq. + apply f2n_inj. apply hf; try apply f2n_ok. + now rewrite <- 2 (restrict_f2n h), Eq. +Qed. + +End Fin2Restrict. +Import Fin2Restrict. + +(** We can now use Proof via the equivalence ... *) + +Lemma bInjective_bSurjective n (f:nat->nat) : + bFun n f -> (bInjective n f <-> bSurjective n f). +Proof. + intros h. + rewrite <- (restrict_injective h), <- (restrict_surjective h). + apply Endo_Injective_Surjective. + - apply Fin_Finite. + - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial. +Qed. + +Lemma bSurjective_bBijective n (f:nat->nat) : + bFun n f -> bSurjective n f -> + exists g, bFun n g /\ forall x, x < n -> g (f x) = x /\ f (g x) = x. +Proof. + intro hf. + rewrite <- (restrict_surjective hf). intros Su. + assert (Ij : Injective (restrict hf)). + { apply Endo_Injective_Surjective; trivial. + - apply Fin_Finite. + - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial. } + assert (Bi : Bijective (restrict hf)). + { apply Injective_Surjective_Bijective; trivial. + - apply Fin_Finite. + - exact Fin.eq_dec. } + destruct Bi as (g & Hg & Hg'). + exists (extend g). + split. + - apply extend_ok. + - intros x Hx. split. + + now rewrite <- (f2n_n2f Hx), <- (restrict_f2n hf), extend_f2n, Hg. + + now rewrite <- (f2n_n2f Hx), extend_f2n, <- (restrict_f2n hf), Hg'. +Qed. diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget index ababd75e0..e703f2828 100644 --- a/theories/Logic/vo.itarget +++ b/theories/Logic/vo.itarget @@ -27,3 +27,4 @@ ProofIrrelevanceFacts.vo ProofIrrelevance.vo RelationalChoice.vo SetIsType.vo +FinFun.vo
\ No newline at end of file diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index cf9f8ee42..acad98e5f 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -13,7 +13,7 @@ (* Adapted in May 2006 by Jean-Marc Notin from initial contents by Laurent Théry (Huffmann contribution, October 2003) *) -Require Import List Setoid Compare_dec Morphisms. +Require Import List Setoid Compare_dec Morphisms FinFun. Import ListNotations. (* For notations [] and [a;b;c] *) Set Implicit Arguments. @@ -174,6 +174,12 @@ Proof. Qed. Local Hint Resolve Permutation_cons_app. +Lemma Permutation_Add a l l' : Add a l l' -> Permutation (a::l) l'. +Proof. + induction 1; simpl; trivial. + rewrite perm_swap. now apply perm_skip. +Qed. + Theorem Permutation_middle : forall (l1 l2:list A) a, Permutation (a :: l1 ++ l2) (l1 ++ a :: l2). Proof. @@ -223,10 +229,6 @@ Proof. eauto. Qed. -Ltac break_list l x l' H := - destruct l as [|x l']; simpl in *; - injection H; intros; subst; clear H. - Theorem Permutation_nil_app_cons : forall (l l' : list A) (x : A), ~ Permutation nil (l++x::l'). Proof. @@ -234,61 +236,51 @@ Proof. apply Permutation_nil in HF. destruct l; discriminate. Qed. -Theorem Permutation_app_inv : forall (l1 l2 l3 l4:list A) a, +Ltac InvAdd := repeat (match goal with + | H: Add ?x _ (_ :: _) |- _ => inversion H; clear H; subst + end). + +Ltac finish_basic_perms H := + try constructor; try rewrite perm_swap; try constructor; trivial; + (rewrite <- H; now apply Permutation_Add) || + (rewrite H; symmetry; now apply Permutation_Add). + +Theorem Permutation_Add_inv a l1 l2 : + Permutation l1 l2 -> forall l1' l2', Add a l1' l1 -> Add a l2' l2 -> + Permutation l1' l2'. +Proof. + revert l1 l2. refine (Permutation_ind_bis _ _ _ _ _). + - (* nil *) + inversion_clear 1. + - (* skip *) + intros x l1 l2 PE IH. intros. InvAdd; try finish_basic_perms PE. + constructor. now apply IH. + - (* swap *) + intros x y l1 l2 PE IH. intros. InvAdd; try finish_basic_perms PE. + rewrite perm_swap; do 2 constructor. now apply IH. + - (* trans *) + intros l1 l l2 PE IH PE' IH' l1' l2' AD1 AD2. + assert (Ha : In a l). { rewrite <- PE. rewrite (Add_in AD1). simpl; auto. } + destruct (Add_inv _ _ Ha) as (l',AD). + transitivity l'; auto. +Qed. + +Theorem Permutation_app_inv (l1 l2 l3 l4:list A) a : Permutation (l1++a::l2) (l3++a::l4) -> Permutation (l1++l2) (l3 ++ l4). Proof. - intros l1 l2 l3 l4 a; revert l1 l2 l3 l4. - set (P l l' := - forall l1 l2 l3 l4, l=l1++a::l2 -> l'=l3++a::l4 -> - Permutation (l1++l2) (l3++l4)). - cut (forall l l', Permutation l l' -> P l l'). - intros H; intros; eapply H; eauto. - apply (Permutation_ind_bis P); unfold P; clear P. - - (* nil *) - intros; now destruct l1. - - (* skip *) - intros x l l' H IH; intros. - break_list l1 b l1' H0; break_list l3 c l3' H1. - auto. - now rewrite H. - now rewrite <- H. - now rewrite (IH _ _ _ _ eq_refl eq_refl). - - (* swap *) - intros x y l l' Hp IH; intros. - break_list l1 b l1' H; break_list l3 c l3' H0. - auto. - break_list l3' b l3'' H. - auto. - constructor. now rewrite Permutation_middle. - break_list l1' c l1'' H1. - auto. - constructor. now rewrite Permutation_middle. - break_list l3' d l3'' H; break_list l1' e l1'' H1. - auto. - rewrite perm_swap. constructor. now rewrite Permutation_middle. - rewrite perm_swap. constructor. now rewrite Permutation_middle. - now rewrite perm_swap, (IH _ _ _ _ eq_refl eq_refl). - - (*trans*) - intros. - destruct (In_split a l') as (l'1,(l'2,H6)). - rewrite <- H. - subst l. - apply in_or_app; right; red; auto. - apply perm_trans with (l'1++l'2). - apply (H0 _ _ _ _ H3 H6). - apply (H2 _ _ _ _ H6 H4). + intros. eapply Permutation_Add_inv; eauto using Add_app. Qed. Theorem Permutation_cons_inv l l' a : Permutation (a::l) (a::l') -> Permutation l l'. Proof. - intro H; exact (Permutation_app_inv [] l [] l' a H). + intro. eapply Permutation_Add_inv; eauto using Add_head. Qed. Theorem Permutation_cons_app_inv l l1 l2 a : Permutation (a :: l) (l1 ++ a :: l2) -> Permutation l (l1 ++ l2). Proof. - intro H; exact (Permutation_app_inv [] l l1 l2 a H). + intro. eapply Permutation_Add_inv; eauto using Add_head, Add_app. Qed. Theorem Permutation_app_inv_l : forall l l1 l2, @@ -300,14 +292,10 @@ Proof. apply Permutation_cons_inv with a; auto. Qed. -Theorem Permutation_app_inv_r : forall l l1 l2, +Theorem Permutation_app_inv_r l l1 l2 : Permutation (l1 ++ l) (l2 ++ l) -> Permutation l1 l2. Proof. - induction l. - intros l1 l2; do 2 rewrite app_nil_r; auto. - intros. - apply IHl. - apply Permutation_app_inv with a; auto. + rewrite 2 (Permutation_app_comm _ l). apply Permutation_app_inv_l. Qed. Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a]. @@ -344,31 +332,6 @@ Proof. apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto. Qed. -Let in_middle l l1 l2 (a:A) : l = l1 ++ a :: l2 -> - forall x, In x l <-> a = x \/ In x (l1++l2). -Proof. - intros; subst; rewrite !in_app_iff; simpl. tauto. -Qed. - -Lemma NoDup_cardinal_incl (l l' : list A) : NoDup l -> NoDup l' -> - length l = length l' -> incl l l' -> incl l' l. -Proof. - intros N. revert l'. induction N as [|a l Hal Hl IH]. - - destruct l'; now auto. - - intros l' Hl' E H x Hx. - assert (Ha : In a l') by (apply H; simpl; auto). - destruct (in_split _ _ Ha) as (l1 & l2 & H12). clear Ha. - rewrite in_middle in Hx; eauto. - destruct Hx as [Hx|Hx]; [left|right]; auto. - apply (IH (l1++l2)); auto. - * apply NoDup_remove_1 with a; rewrite <- H12; auto. - * apply eq_add_S. - simpl in E; rewrite E, H12, !app_length; simpl; auto with arith. - * intros y Hy. assert (Hy' : In y l') by (apply H; simpl; auto). - rewrite in_middle in Hy'; eauto. - destruct Hy'; auto. subst y; intuition. -Qed. - Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' -> (forall x:A, In x l <-> In x l') -> Permutation l l'. Proof. @@ -377,25 +340,25 @@ Proof. intros Hl' H. exfalso. rewrite (H a); auto. - intros l' Hl' H. assert (Ha : In a l') by (apply H; simpl; auto). - destruct (In_split _ _ Ha) as (l1 & l2 & H12). - rewrite H12. - apply Permutation_cons_app. - apply IH; auto. - * apply NoDup_remove_1 with a; rewrite <- H12; auto. - * intro x. split; intros Hx. - + assert (Hx' : In x l') by (apply H; simpl; auto). - rewrite in_middle in Hx'; eauto. - destruct Hx'; auto. subst; intuition. - + assert (Hx' : In x l') by (rewrite (in_middle l1 l2 a); eauto). - rewrite <- H in Hx'. destruct Hx'; auto. - subst. destruct (NoDup_remove_2 _ _ _ Hl' Hx). + destruct (Add_inv _ _ Ha) as (l'' & AD). + rewrite <- (Permutation_Add AD). + apply perm_skip. + apply IH; clear IH. + * now apply (NoDup_Add AD). + * split. + + apply incl_Add_inv with a l'; trivial. intro. apply H. + + intro Hx. + assert (Hx' : In x (a::l)). + { apply H. rewrite (Add_in AD). now right. } + destruct Hx'; simpl; trivial. subst. + rewrite (NoDup_Add AD) in Hl'. tauto. Qed. Lemma NoDup_Permutation_bis l l' : NoDup l -> NoDup l' -> - length l = length l' -> incl l l' -> Permutation l l'. + length l' <= length l -> incl l l' -> Permutation l l'. Proof. intros. apply NoDup_Permutation; auto. - split; auto. apply NoDup_cardinal_incl; auto. + split; auto. apply NoDup_length_incl; trivial. Qed. Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'. @@ -433,55 +396,19 @@ Qed. End Permutation_map. -Section Injection. - -Definition injective {A B} (f : A->B) := - forall x y, f x = f y -> x = y. - -Lemma injective_map_NoDup {A B} (f:A->B) (l:list A) : - injective f -> NoDup l -> NoDup (map f l). -Proof. - intros Hf. induction 1 as [|x l Hx Hl IH]; simpl; constructor; trivial. - rewrite in_map_iff. intros (y & Hy & Hy'). apply Hf in Hy. now subst. -Qed. - -Lemma injective_bounded_surjective n f : - injective f -> - (forall x, x < n -> f x < n) -> - (forall y, y < n -> exists x, x < n /\ f x = y). -Proof. - intros Hf H. - set (l := seq 0 n). - assert (P : incl (map f l) l). - { intros x. rewrite in_map_iff. intros (y & <- & Hy'). - unfold l in *. rewrite in_seq in *. simpl in *. - destruct Hy' as (_,Hy'). auto with arith. } - assert (P' : incl l (map f l)). - { unfold l. - apply NoDup_cardinal_incl; auto using injective_map_NoDup, seq_NoDup. - now rewrite map_length. } - intros x Hx. - assert (Hx' : In x l) by (unfold l; rewrite in_seq; auto with arith). - apply P' in Hx'. - rewrite in_map_iff in Hx'. destruct Hx' as (y & Hy & Hy'). - exists y; split; auto. unfold l in *; rewrite in_seq in Hy'. - destruct Hy'; auto with arith. -Qed. - Lemma nat_bijection_Permutation n f : - injective f -> (forall x, x < n -> f x < n) -> + bFun n f -> + Injective f -> let l := seq 0 n in Permutation (map f l) l. Proof. intros Hf BD. - apply NoDup_Permutation_bis; auto using injective_map_NoDup, seq_NoDup. + apply NoDup_Permutation_bis; auto using Injective_map_NoDup, seq_NoDup. * now rewrite map_length. * intros x. rewrite in_map_iff. intros (y & <- & Hy'). rewrite in_seq in *. simpl in *. destruct Hy' as (_,Hy'). auto with arith. Qed. -End Injection. - Section Permutation_alt. Variable A:Type. Implicit Type a : A. @@ -493,7 +420,7 @@ Implicit Type l : list A. Let adapt f n := let m := f (S n) in if le_lt_dec m (f 0) then m else pred m. -Let adapt_injective f : injective f -> injective (adapt f). +Let adapt_injective f : Injective f -> Injective (adapt f). Proof. unfold adapt. intros Hf x y EQ. destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT']. @@ -512,7 +439,7 @@ Proof. now rewrite (Lt.S_pred _ _ LT), (Lt.S_pred _ _ LT'), EQ. Qed. -Let adapt_ok a l1 l2 f : injective f -> length l1 = f 0 -> +Let adapt_ok a l1 l2 f : Injective f -> length l1 = f 0 -> forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n). Proof. unfold adapt. intros Hf E n. @@ -531,7 +458,7 @@ Lemma Permutation_nth_error l l' : Permutation l l' <-> (length l = length l' /\ exists f:nat->nat, - injective f /\ forall n, nth_error l' n = nth_error l (f n)). + Injective f /\ forall n, nth_error l' n = nth_error l (f n)). Proof. split. { intros P. @@ -573,8 +500,8 @@ Qed. Lemma Permutation_nth_error_bis l l' : Permutation l l' <-> exists f:nat->nat, - injective f /\ - (forall n, n < length l -> f n < length l) /\ + Injective f /\ + bFun (length l) f /\ (forall n, nth_error l' n = nth_error l (f n)). Proof. rewrite Permutation_nth_error; split. @@ -591,7 +518,10 @@ Proof. [|apply Hf2 in LT; elim (Lt.lt_not_le _ _ LT H)]. apply Lt.le_lt_or_eq in LE. destruct LE as [LT|EQ]; trivial. rewrite <- nth_error_Some, Hf3, nth_error_Some in LT. - destruct (injective_bounded_surjective Hf Hf2 LT) as (y & Hy & Hy'). + assert (Hf' : bInjective (length l) f). + { intros x y _ _ E. now apply Hf. } + rewrite (bInjective_bSurjective Hf2) in Hf'. + destruct (Hf' _ LT) as (y & Hy & Hy'). apply Hf in Hy'. subst y. elim (Lt.lt_irrefl _ Hy). Qed. @@ -600,8 +530,8 @@ Lemma Permutation_nth l l' d : (let n := length l in length l' = n /\ exists f:nat->nat, - (forall x, x < n -> f x < n) /\ - (forall x y, x < n -> y < n -> f x = f y -> x = y) /\ + bFun n f /\ + bInjective n f /\ (forall x, x < n -> nth x l' d = nth (f x) l d)). Proof. split. @@ -611,6 +541,7 @@ Proof. apply Permutation_nth_error_bis in H. destruct H as (f & Hf & Hf2 & Hf3). exists f. split; [|split]; auto. + intros x y _ _ Hxy. now apply Hf. intros n Hn. rewrite <- 2 nth_default_eq. unfold nth_default. now rewrite Hf3. - intros (E & f & Hf1 & Hf2 & Hf3). diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index b6ec6307c..a1e6b14d6 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -8,10 +8,10 @@ Require Arith_base. -(** [fin n] is a convinient way to represent \[1 .. n\] +(** [fin n] is a convenient way to represent \[1 .. n\] [fin n] can be seen as a n-uplet of unit where [F1] is the first element of -the n-uplet and [FS] set (n-1)-uplet of all the element but the first. +the n-uplet and [FS] set (n-1)-uplet of all the elements but the first. Author: Pierre Boutillier Institution: PPS, INRIA 12/2010-01/2012-07/2012 @@ -103,13 +103,39 @@ Fixpoint of_nat_lt {p n : nat} : p < n -> t n := end end. +Lemma of_nat_ext {p}{n} (h h' : p < n) : of_nat_lt h = of_nat_lt h'. +Proof. + now rewrite (Peano_dec.le_unique _ _ h h'). +Qed. + Lemma of_nat_to_nat_inv {m} (p : t m) : of_nat_lt (proj2_sig (to_nat p)) = p. Proof. -induction p. - reflexivity. - simpl; destruct (to_nat p). simpl. subst p; repeat f_equal. apply Peano_dec.le_unique. +induction p; simpl. +- reflexivity. +- destruct (to_nat p); simpl in *. f_equal. subst p. apply of_nat_ext. Qed. +Lemma to_nat_of_nat {p}{n} (h : p < n) : proj1_sig (to_nat (of_nat_lt h)) = p. +Proof. + revert n h. + induction p; intros; destruct n; simpl; trivial. + - inversion h. + - inversion h. + - set (h' := Lt.lt_S_n p n h). clearbody h'. + specialize (IHp n h'). + destruct (to_nat (of_nat_lt h')); simpl in *. now f_equal. +Qed. + +Lemma to_nat_inj {n} (p q : t n) : + proj1_sig (to_nat p) = proj1_sig (to_nat q) -> p = q. +Proof. + intro H. + rewrite <- (of_nat_to_nat_inv p), <- (of_nat_to_nat_inv q). + destruct (to_nat p) as (np,hp), (to_nat q) as (nq,hq); simpl in *. + revert hp hq. rewrite H. apply of_nat_ext. +Qed. + + (** [weak p f] answers a function witch is the identity for the p{^ th} first element of [fin (p + m)] and [FS (FS .. (FS (f k)))] for [FS (FS .. (FS k))] with p FSs *) |