(** Fin.v Version 1.1 February 2011 *) (** runs under V8.3, tested with 8.3pl2 *) (** Celia Picard with contributions by Ralph Matthes, I.R.I.T., University of Toulouse and CNRS*) (** provides a definition and various properties and lemmas about the type Fin, among which, the injectivity of Fin *) Require Export Arith. Require Import Utf8. Require Import Setoid. Require Import List. Require Import Morphisms. Require Import Tools. Set Implicit Arguments. (* The idea here is to reuse the definition of Fin given by McBride & McKinna to represent sets of n elements *) Section Fin_def_tools. (* According to McBride & McKinna, "The view from the left" *) Inductive Fin: nat -> Set := first k : Fin (S k) | succ k: Fin k -> Fin (S k). (* The first thing we want to show is n = m <-> Fin n = Fin m. *) (* The following lemma shows the implication from left to rifht *) Definition Fin_n_m: forall n m: nat, n = m -> Fin n = Fin m. Proof. intros n m H. rewrite H. reflexivity. Defined. (* Definition transformFin (n1 n2:nat)(h:n1=n2)(x:Fin n1): Fin n2 := match h in (_=n) return Fin n with refl_equal => x end. Definition transformFin2 (n1 n2:nat)(h:Fin n1=Fin n2)(x:Fin n1): Fin n2 := match h in (_=f) return f with refl_equal => x end. Lemma transformFin_refl_Id : forall (n: nat) (x: Fin n), transformFin (refl_equal n) x = x. Proof. reflexivity. Qed. *) Lemma Fin_S_pred : forall n: nat, n > 0 -> Fin n = Fin (S (pred n)). Proof. intros n h. rewrite <-(S_pred n 0 h). reflexivity. Qed. (* decode_Fin allows to associate an integer to an element of Fin n *) Fixpoint decode_Fin (n: nat)(f: Fin n): nat := match f with first k => 0 | succ k f' => S ( decode_Fin f') end. Definition decode_Fin_inf_n: forall (n: nat)(f: Fin n), decode_Fin f < n. Proof. intros n f. induction f as [ n | n f IHf]. apply gt_Sn_O. apply (gt_n_S _ _ IHf). Defined. Definition decode_Fin_S_gt_O: forall (n: nat)(f: Fin n), decode_Fin (succ f) > 0. Proof. intros n f. apply gt_Sn_O. Defined. Lemma decode_Fin_match : forall (n m: nat)(f: Fin n)(H: n = m), decode_Fin f = decode_Fin (match H in (_ = l) return Fin l with refl_equal => f end). Proof. intros n m f H. destruct f as [ n | n f] ; refine (match H return _ with refl_equal => _ end) ; reflexivity. Qed. (* code_Fin associates an element of Fin n to an integer *) (* As its definition is not immediate, we had to define auxiliary functions. *) (* What's more, we also define various versions of code_Fin and prove their equivalence *) Fixpoint code_Fin1_aux (n: nat)(m: nat): option(Fin (S n)) := match n return option(Fin (S n)) with | 0 => match m with O => Some(first 0) | S m' => None end | S n' => match m return option(Fin (S (S n'))) with O => Some(first (S n')) | S m' => option_map (succ (k:=(S n'))) (code_Fin1_aux n' m') end end. Definition code_fin1_aux_def: forall n m: nat, m <= n -> {f: Fin (S n) | code_Fin1_aux n m = Some f}. Proof. induction n as [ | n IHn]; intros m H ; destruct m as [ | m]; simpl. exists (first 0); reflexivity. destruct (le_Sn_O m H). exists (first (S n)); reflexivity. destruct (IHn m (le_S_n _ _ H)) as [f0 eq]. exists (succ f0). rewrite eq. reflexivity. Defined. Definition code_Fin1_Sn (n m: nat)(h: m<=n): Fin (S n) := projT1 (code_fin1_aux_def h). (* First version of code_Fin *) Definition code_Fin1 (n m: nat)(h: m fun (m : nat) (h : m < 0) => match (lt_n_O m h) return (Fin 0) with end | S n0 => fun (m : nat) (h : m < S n0) => code_Fin1_Sn (lt_n_Sm_le m n0 h) end m h. (* We prove a certain number of properties on code_Fin1 *) Lemma code_Fin1_Sn_0: forall (n:nat)(h:0<=n), code_Fin1_Sn h = first n. Proof. intros n h. destruct n as [ | n]; reflexivity. Qed. Lemma code_Fin1_Sn_S : forall (n m:nat)(h:S m<=S n), code_Fin1_Sn h = succ (code_Fin1_Sn (le_S_n m n h)). Proof. intros n m h. unfold code_Fin1_Sn. simpl projT1. destruct (code_fin1_aux_def (le_S_n m n h)) as [x e]. reflexivity. Qed. Lemma code_Fin1_Sn_proofirr:forall (n m:nat)(h1 h2:m<=n), code_Fin1_Sn h1 = code_Fin1_Sn h2. Proof. intros n m. revert n. induction m as [ | m IHm]; intros n h1 h2. do 2 rewrite code_Fin1_Sn_0. reflexivity. destruct n as [ | n]. inversion h1. do 2 rewrite code_Fin1_Sn_S. f_equal. apply IHm. Qed. Lemma code_Fin1_Sn_proofirr2 : forall (n m1 m2:nat)(h1:m1<=n)(h2:m2<=n)(e: m1=m2), code_Fin1_Sn h1 = code_Fin1_Sn h2. Proof. induction n as [| n IHn]; intros m1 m2 h1 h2 e; destruct m1 as [|m1]; destruct m2 as [|m2]. do 2 rewrite code_Fin1_Sn_0. reflexivity. destruct (O_S m2 e). destruct (O_S m1 (sym_eq e)). inversion h1. do 2 rewrite code_Fin1_Sn_0. reflexivity. destruct (O_S m2 e). destruct (O_S m1 (sym_eq e)). do 2 rewrite code_Fin1_Sn_S. f_equal. apply (IHn _ _ _ _ (eq_add_S m1 m2 e)). Qed. Lemma code_Fin1_0_: forall (n:nat)(h:0 (forall (n m:nat)(h:S m forall (n m:nat)(h:m f1 = f2. Proof. intros n f1 f2 h. rewrite <- (code1_decode_Id f1); rewrite <- (code1_decode_Id f2). destruct n as [|n]. inversion f1. assert (h1 := decode_Fin_inf_n f1). rewrite (code_Fin1_proofirr _ h1). revert h1. rewrite h. intros h1. apply code_Fin1_proofirr. Qed. Lemma decode_Fin_0_first: forall(n: nat) (f: Fin (S n)), decode_Fin f = 0 -> f = first n. Proof. intros n f H. apply decode_Fin_unique. rewrite H. reflexivity. Qed. Definition mkFinn : forall (n: nat), Fin (S n). Proof. intros n ; induction n as [|n IH]. exact (first 0). exact (succ IH). Defined. Lemma decode_Fin_mkFinn_n : forall n, decode_Fin (mkFinn n) = n. Proof. induction n as [|n IH]. reflexivity. simpl. rewrite IH ; reflexivity. Qed. Definition get_cons: forall (n: nat) (f: Fin (S n))(h: decode_Fin f > 0), Fin n. Proof. intros n f h. elim (O_or_S (decode_Fin f)); intro a. destruct a as [x e]. assert (H: x < n). apply lt_S_n. rewrite e. apply (decode_Fin_inf_n f). exact (code_Fin1 H). rewrite a in h. apply False_rec. apply (lt_irrefl _ h). Defined. Lemma get_cons_ok: forall (n: nat)(f: Fin n), get_cons (succ f) (decode_Fin_S_gt_O f) = f. Proof. intros n f. destruct n as [|n]. inversion f. rewrite <- code1_decode_Id. unfold get_cons. simpl. apply code_Fin1_proofirr. Qed. Lemma get_cons_proofirr: forall (n: nat) (f: Fin (S n))(h h': decode_Fin f > 0), get_cons f h = get_cons f h'. Proof. intros n f h h'. apply decode_Fin_unique. unfold get_cons, sumor_rec, sumor_rect. elim (O_or_S (decode_Fin f)) ; intros b. reflexivity. apply False_rec. rewrite <- b in h. inversion h. Qed. Lemma Fin_first_1: forall (f: Fin 1), f = first 0. Proof. intros f. rewrite <- (code1_decode_Id f). assert (h:= decode_Fin_inf_n f) ; rewrite (code_Fin1_proofirr _ h). elim (zerop (decode_Fin f)); intros a. revert h ; rewrite a; intro h. apply code_Fin1_0_. apply False_rec. apply (lt_irrefl _ (lt_le_trans _ _ _ a (lt_n_Sm_le _ _ h))). Qed. Lemma decode_Fin_get_cons: forall (n: nat)(f: Fin (S n))(h: decode_Fin f > 0), decode_Fin f = S (decode_Fin (get_cons f h)). Proof. intros n f h. unfold get_cons. simpl. unfold sumor_rec ; unfold sumor_rect. elim (O_or_S (decode_Fin f)) ; [intros [m h1] | intros a]. rewrite decode_code1_Id. rewrite h1. reflexivity. apply False_rec. rewrite a in h. apply (lt_irrefl _ h). Qed. Lemma get_cons_ok1 (n: nat)(i: Fin (S n))(h: 0 < decode_Fin i) : succ (get_cons _ h) = i. Proof. apply decode_Fin_unique, sym_eq, decode_Fin_get_cons. Qed. Lemma get_cons_ok2 (n: nat)(i: Fin n)(h: 0 < decode_Fin (succ i)) : get_cons (succ i) h = i. Proof. rewrite (get_cons_proofirr _ _ (decode_Fin_S_gt_O i) ). apply get_cons_ok. Qed. (* Definition and lemma to create a list of all the elements of Fin n *) Definition makeListFin : forall (n: nat), list (Fin n). Proof. intros n. induction n as [|n IHn]. exact nil. exact (cons (first n) (map (succ (k:= n)) IHn )). Defined. Fixpoint makeListFin' (n: nat): list (Fin n):= match n with O => nil | S k => (first k) :: (map (succ (k:= k)) (makeListFin' k)) end. Lemma makeListFin_eq_makeListFin': forall n, makeListFin n = makeListFin' n. Proof. reflexivity. Qed. Lemma makeListFin_nb_elem_ok: forall n: nat, (length (makeListFin n)) = n. Proof. intros n. induction n as [|n IHn]. reflexivity. rewrite <- IHn at 3. simpl. rewrite map_length. reflexivity. Qed. Lemma all_Fin_n_in_makeListFin : forall (n: nat), forall f: Fin n, In f (makeListFin n). Proof. intros n f. induction f as [k | k f IHf] ; simpl. left; reflexivity. right. apply in_map. apply IHf. Qed. Lemma nth_makeListFin: forall (n m: nat)(h: m < n), code_Fin1 h = nth m (makeListFin n) (code_Fin1 h). Proof. induction n as [|n IHn]; intros m h. inversion h. destruct m as [|m]. apply code_Fin1_Sn_0. simpl. destruct n as [|n]. apply False_rec. apply (le_Sn_O _ (gt_S_le _ _ h)). rewrite code_Fin1_Sn_S. rewrite map_nth. f_equal. unfold code_Fin1 in IHn. rewrite (code_Fin1_Sn_proofirr _ (lt_n_Sm_le m n (lt_S_n _ _ h))). apply IHn. Qed. Lemma nth_makeListFin_def: forall (n m: nat)(h: m < n)(d: Fin n), code_Fin1 h = nth m (makeListFin n) d. Proof. intros n m h f. rewrite (nth_indep (makeListFin n) f (code_Fin1 h)). apply nth_makeListFin. rewrite makeListFin_nb_elem_ok. assumption. Qed. Lemma makeListFin_S: forall n: nat, makeListFin (S n) = (first n) :: (map (succ (k:= n)) (makeListFin n)). Proof. reflexivity. Qed. Lemma Fin_first_or_succ: forall (n: nat)(f: Fin (S n)), In f ((first n)::(map (succ (k:= n)) (makeListFin n))). Proof. intros n f. rewrite <- makeListFin_S. apply all_Fin_n_in_makeListFin. Qed. End Fin_def_tools. Section rewrite_Fins. Lemma match_sym_eq_eq: forall (n1 n2: nat)(f: Fin n1)(e: n1 = n2), f = match sym_eq e in (_ = l) return (Fin l) with refl_equal => match e in (_ = l) return (Fin l) with refl_equal => f end end. Proof. intros n1 n2 f e. refine (match e return _ with refl_equal => _ end). reflexivity. Qed. Lemma match_eq_sym_eq: forall (n1 n2: nat)(f: Fin n1)(e: n2 = n1), f = match e in (_ = l) return (Fin l) with refl_equal => match sym_eq e in (_ = l) return (Fin l) with refl_equal => f end end. Proof. intros n1 n2 f e. refine ((match e as e' return forall g: Fin _, _ with refl_equal => _ end) f). reflexivity. Qed. (* crucial definition, but nothing more than an abbreviation *) Definition rewriteFins (n1 n2: nat)(H: n1 = n2)(f: Fin n1): Fin n2 := match H in _ = l return Fin l with refl_equal => f end. (* this wraps decode_Fin_match and should be called differently *) Lemma decode_Fin_match' : forall (n m: nat)(f: Fin n)(H: n = m), decode_Fin f = decode_Fin (rewriteFins H f). Proof. apply decode_Fin_match. Qed. Lemma rewriteFins_refl : forall (n: nat)(e: n = n)(f: Fin n), rewriteFins e f = f. Proof. intros n e f. apply decode_Fin_unique, (sym_eq (decode_Fin_match' _ _)). Qed. Lemma rewriteFins_sym: forall (n1 n2: nat)(e: n1 = n2)(f: Fin n2), rewriteFins e (rewriteFins (sym_eq e) f) = f. Proof. intros n1 n2 e f. apply (sym_eq (match_eq_sym_eq f e)). Qed. Lemma rewriteFins_trans :forall (n1 n2 n3: nat) (e1: n1 = n2)(e2: n2 = n3)(f: Fin n1), rewriteFins e2 (rewriteFins e1 f) = rewriteFins (trans_eq e1 e2) f. Proof. intros n1 n2 n3 e1 e2 f. refine ((match e2 return _ with refl_equal => _ end) f). reflexivity. Qed. End rewrite_Fins. Section Fin_injectivity. Lemma succ_first_neq (n n' : nat)(f: Fin (S n) -> Fin (S n')) (g: Fin (S n') -> Fin (S n))(H: Bijective f g): decode_Fin (f (first n)) = 0 -> forall i, decode_Fin (f (succ i)) > 0. Proof. intros a i. apply neq_0_lt. intros H1. rewrite H1 in a. apply decode_Fin_unique, (bij_inj H) in a. inversion a. Qed. Lemma first_succ_neq (n n' : nat)(f: Fin (S n) -> Fin (S n')) (g: Fin (S n') -> Fin (S n))(H: Bijective f g)(i: Fin n): decode_Fin (f (succ i)) = 0 -> decode_Fin (f (first n)) > 0. Proof. intros a. apply neq_0_lt. intros H1. assert (H2 := succ_first_neq H (sym_eq H1) i). rewrite a in H2 ; inversion H2. Qed. Definition FSnFSn'_FnFn' (n n' : nat)(f: Fin (S n) -> Fin (S n')) (g: Fin (S n') -> Fin (S n))(H: Bijective f g): Fin n -> Fin n'. Proof. intros i. elim (zerop (decode_Fin (f (succ i)))) ; intros a. exact (get_cons _ (first_succ_neq H i a)). exact (get_cons _ a). Defined. Lemma FSnFSn'_FnFn'_ok1 (n n' : nat)(f: Fin (S n) -> Fin (S n')) (g: Fin (S n') -> Fin (S n))(H: Bijective f g)(i: Fin n) (H1: decode_Fin (f (succ i)) = 0) : FSnFSn'_FnFn' H i = get_cons _ (first_succ_neq H i H1). Proof. unfold FSnFSn'_FnFn', sumbool_rec, sumbool_rect. elim (zerop (decode_Fin (f (succ i)))) ; intros a. apply get_cons_proofirr. apply False_rec, (lt_0_neq _ a), sym_eq, H1. Qed. Lemma FSnFSn'_FnFn'_ok2 (n n' : nat)(f: Fin (S n) -> Fin (S n')) (g: Fin (S n') -> Fin (S n))(H: Bijective f g)(i: Fin n) (H1: decode_Fin (f (succ i)) > 0) : FSnFSn'_FnFn' H i = get_cons _ H1. Proof. unfold FSnFSn'_FnFn', sumbool_rec, sumbool_rect. elim (zerop (decode_Fin (f (succ i)))) ; intros a. apply False_rec, (lt_0_neq _ H1), sym_eq, a. apply get_cons_proofirr. Qed. Lemma FSnFSn'_FnFn'_proofirr (n n' : nat)(f: Fin (S n) -> Fin (S n')) (g: Fin (S n') -> Fin (S n))(H1 H2: Bijective f g) : forall i, FSnFSn'_FnFn' H1 i = FSnFSn'_FnFn' H2 i. Proof. intros i. elim (zerop (decode_Fin (f (succ i)))) ; intros a. rewrite (FSnFSn'_FnFn'_ok1 H1 _ a), (FSnFSn'_FnFn'_ok1 H2 _ a). apply get_cons_proofirr. rewrite (FSnFSn'_FnFn'_ok2 H1 _ a), (FSnFSn'_FnFn'_ok2 H2 _ a). apply get_cons_proofirr. Qed. Lemma succ_inj (n: nat)(i1 i2 : Fin n) : succ i1 = succ i2 -> i1 = i2. Proof. intros H. apply decode_Fin_unique, eq_add_S. change (decode_Fin (succ i1) = decode_Fin (succ i2)). rewrite H. reflexivity. Qed. Lemma FSnFSn'_FnFn'_aux_bij(n n' : nat)(f: Fin (S n) -> Fin (S n')) (g: Fin (S n') -> Fin (S n))(H1: Bijective f g)(H2 : Bijective g f) : forall i, FSnFSn'_FnFn' H2 (FSnFSn'_FnFn' H1 i) = i. Proof. intros i ; destruct H1 as [H1 H3]. elim (zerop (decode_Fin (f (succ i)))) ; intros a. rewrite (FSnFSn'_FnFn'_ok1 _ _ a). assert (b : decode_Fin (g (succ (get_cons (f (first n)) (first_succ_neq (conj H1 H3) i a)))) = 0). rewrite get_cons_ok1, H1. reflexivity. rewrite (FSnFSn'_FnFn'_ok1 _ _ b). apply succ_inj. rewrite get_cons_ok1, <- (H1 (succ i)). f_equal. apply decode_Fin_unique, sym_eq, a. rewrite (FSnFSn'_FnFn'_ok2 _ _ a). assert (b : decode_Fin (g (succ (get_cons (f (succ i)) a))) > 0). rewrite (get_cons_ok1 _ a), H1. apply lt_0_Sn. rewrite (FSnFSn'_FnFn'_ok2 _ _ b). revert b ; rewrite (get_cons_ok1 _ a), H1 ; intros b. apply get_cons_ok2. Qed. Lemma FSnFSn'_FnFn'_bij(n n' : nat)(f: Fin (S n) -> Fin (S n')) (g: Fin (S n') -> Fin (S n))(H: Bijective f g) : Bijective (FSnFSn'_FnFn' H) (FSnFSn'_FnFn' (Bij_sym H)). Proof. split ; intros i ; apply FSnFSn'_FnFn'_aux_bij. Qed. Definition Fin_inj_aux: forall (n n': nat) (f: Fin n -> Fin n')(g: Fin n' -> Fin n), Bijective f g -> n = n'. Proof. induction n as [|n IH] ; intros [|n'] f g H. reflexivity. assert (i := g (first n')). inversion i. assert (i := f (first n)). inversion i. f_equal. apply (IH _ (FSnFSn'_FnFn' H) (FSnFSn'_FnFn' (Bij_sym H))). apply FSnFSn'_FnFn'_bij. Defined. Definition FnFn' (n n' : nat)(H : Fin n = Fin n')(i : Fin n) := match H in _=l return l with refl_equal => i end. Lemma FnFn'_Fn'Fn (n n' : nat)(H : Fin n = Fin n') : forall i, FnFn' (sym_eq H) (FnFn' H i) = i. Proof. unfold FnFn' ; rewrite H. reflexivity. Qed. Lemma FnFn'_Fn'Fn_inv (n n' : nat)(H : Fin n = Fin n') : forall i, FnFn' H (FnFn' (sym_eq H) i) = i. Proof. unfold FnFn' ; rewrite H. reflexivity. Qed. Definition Fin_inj: forall (n n': nat) , Fin n = Fin n' -> n = n'. Proof. intros n n' H. apply (Fin_inj_aux (conj (FnFn'_Fn'Fn H) (FnFn'_Fn'Fn_inv H))). Defined. End Fin_injectivity.