(** 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 *) (** this is code that conforms to the description in the article "Permutations in Coinductive Graph Representation" by the authors *) Require Export Arith. Require Import Utf8. Require Import Setoid. Require Import List. Require Import NatSeg. Require Import EqImplIso. 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. (* Introduction of the work done on NatSeg *) (* It will be useful to prove that Fin is injective *) Definition Fin_NatSeg : forall (n: nat) (f: Fin n), NatSeg n. Proof. intros h f. exists (decode_Fin f). apply (decode_Fin_inf_n f). Defined. Program Definition Fin_NatSeg' (n: nat) (f: Fin n): NatSeg n := decode_Fin f. Next Obligation. apply (decode_Fin_inf_n f). Defined. Lemma Fin_NatSeg_eq_Fin_NatSeg' : forall (n : nat)(f: Fin n), natSeg_eq (Fin_NatSeg f) (Fin_NatSeg' f). Proof. reflexivity. Qed. Add Parametric Morphism (n: nat): (Fin_NatSeg (n:= n)) with signature (eq (A:= Fin n)) ==> (natSeg_eq (n:=n)) as Fin_NatSegM. Proof. reflexivity. Qed. Definition NatSeg_Fin (n: nat) (ns: NatSeg n): Fin n := code_Fin1 (proof_lt ns). Add Parametric Morphism (n: nat): (NatSeg_Fin (n := n)) with signature (natSeg_eq (n:=n)) ==> (eq (A:= Fin n)) as NatSeg_FinM. Proof. destruct n as [|n]; intros x y h. no_NatSeg_0 x. destruct h as [h]. apply (code_Fin1_Sn_proofirr2 _ _ h). Qed. Lemma Fin_NatSeg_NatSeg_Fin_Id: forall (n: nat) (ns: NatSeg n), natSeg_eq (Fin_NatSeg (NatSeg_Fin ns)) ns. Proof. intros n ns. apply is_natSeg_eq. apply (decode_code1_Id (proof_lt ns)). Qed. Lemma NatSeg_Fin_Fin_NatSeg_Id: forall (n: nat) (f: Fin n), NatSeg_Fin (Fin_NatSeg f) = f. Proof. intros n f. apply (code1_decode_Id f). Qed. Definition fin_morph (n n': nat) (i: Fin n -> Fin n') := Morphism (eq(A:=Fin n) ==> eq(A:=Fin n')) i. Definition transfo_fun : forall (n n': nat)(i: Fin n -> Fin n'), NatSeg n -> NatSeg n'. Proof. intros n n' i ns. exact (Fin_NatSeg (i (NatSeg_Fin ns))). Defined. Add Parametric Morphism (n n': nat)(i: Fin n -> Fin n'): (transfo_fun (n:= n) (n':= n') i ) with signature (natSeg_eq (n:= n)) ==> (natSeg_eq (n:= n')) as transfo_funM. Proof. intros x y h. unfold transfo_fun. rewrite h. reflexivity. Qed. Lemma transfo_fun_transfo_fun_id: forall (n n': nat) (i: Fin n -> Fin n')(j: Fin n' -> Fin n) (Idji: forall f: Fin n, j (i f) = f) (Idij: forall f': Fin n', i (j f') = f'), (forall ns: NatSeg n, natSeg_eq (transfo_fun j (transfo_fun i ns)) ns). Proof. intros n n' i j Idji Idij ns. unfold transfo_fun. rewrite NatSeg_Fin_Fin_NatSeg_Id. rewrite Idji. apply Fin_NatSeg_NatSeg_Fin_Id. Qed. (* First step of the proof that Fin is injective *) Definition Fin_inj_aux: forall (n n': nat) (i: Fin n -> Fin n')(j: Fin n' -> Fin n), (forall f: Fin n, (j ( i f)) = f) -> (forall f': Fin n', (i ( j f')) = f') -> n = n'. Proof. intros n n' i j Idji Idij. apply (NatSeg_inj (transfo_funM i ) (transfo_funM j) (transfo_fun_transfo_fun_id i j Idji Idij) (transfo_fun_transfo_fun_id j i Idij Idji)). Defined. (* Proof that Fin is injective *) Definition Fin_inj: forall n n': nat, Fin n = Fin n' -> n = n'. Proof. intros n n' H. apply (Fin_inj_aux _ _ (jjii (Fin n) (Fin n') H) (iijj (Fin n) (Fin n') H)). Defined. 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. (* 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. 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.