(** CardFin.v Version 1.0 May 2012 *) (** runs under V8.3, tested with 8.3pl2 *) (** Celia Picard, I.R.I.T., University of Toulouse, based on a development by Yves Bertot (INRIA Sophia-Antipolis), communicated privately *) (** provides a proof of a calculation of the cardinal of Fin, without using Ssreflect (hence with no card operation really) and an alternative proof of the injectivity of Fin *) Require Import List Arith. Require Import Fin. Set Implicit Arguments. Definition eq_dec (T: Type) : Type := forall (x y : T), {x = y}+{x <> y}. Section EnumFinType. Variable T : Type. Variable T_eq_dec : eq_dec T. Fixpoint count (tst : eq_dec T) x l := match l with nil => 0 | a::tl => if tst x a then 1 + count tst x tl else count tst x tl end. Lemma count_irrel : forall tst1 tst2 x l, count tst1 x l = count tst2 x l. Proof. intros tst1 tst2 x l. induction l as [ | a tl Ht]. reflexivity. simpl; case (tst1 x a);[intros xa | intros xna]; (case (tst2 x a);[intros xa' | intros xna']). rewrite Ht ; reflexivity. case xna'; assumption. case xna; assumption. apply Ht. Qed. (* An enumeration is a list that contains exactly once all the elements of T *) Definition is_enum l := forall x, count T_eq_dec x l = 1. Lemma count_app (l1 l2 : list T)(t: T) : count T_eq_dec t (l1++l2) = count T_eq_dec t l1 + count T_eq_dec t l2. Proof. induction l1 as [|t1 l1 IH]. reflexivity. simpl. elim (T_eq_dec t t1) ; intros a. rewrite IH. reflexivity. apply IH. Qed. Fixpoint rem1 x l := match l with nil => nil | a::tl => if T_eq_dec x a then tl else a::rem1 x tl end. Lemma count_rem1_eq : forall x l, count T_eq_dec x l <> 0 -> count T_eq_dec x l = 1 + count T_eq_dec x (rem1 x l). Proof. intros x; induction l as [ | a tl Ht]. intros abs; case abs; reflexivity. simpl; case_eq (T_eq_dec x a); simpl. intros _ _ _; reflexivity. intros n tst cn0; rewrite tst. apply Ht; assumption. Qed. Lemma count_rem1_eq_length : forall x l, count T_eq_dec x l <> 0 -> length l = S (length (rem1 x l)). Proof. intros x ; induction l as [|t l IH]. intros H1. apply False_rec, H1, eq_refl. simpl. elim (T_eq_dec x t) ; intros H1 H2 ; f_equal. apply (IH H2). Qed. Lemma count_rem1_diff : forall x y l, x <> y -> count T_eq_dec y l = count T_eq_dec y (rem1 x l). Proof. intros x y l xny; induction l as [ | a tl Ht]. reflexivity. simpl; case_eq (T_eq_dec y a); intros ya tya. case (T_eq_dec x a). intros xa; case xny; rewrite ya; assumption. simpl; rewrite tya, Ht; reflexivity. case (T_eq_dec x a); [reflexivity | simpl; rewrite Ht, tya; reflexivity]. Qed. Lemma count_rem1_diff_length : forall x l, count T_eq_dec x l = 0 -> length l = length (rem1 x l). Proof. intros x l H; induction l as [ | t l IH]. reflexivity. revert H ; simpl; elim (T_eq_dec x t) ; intros H1 H. inversion H. simpl ; f_equal. apply IH, H. Qed. Lemma rem1_cons_eq : forall x l, rem1 x (x::l) = l. Proof. intros x l. simpl. elim (T_eq_dec x x) ; intros H. reflexivity. apply False_rec, H, eq_refl. Qed. Lemma rem1_cons_diff : forall x y l, x <> y -> rem1 x (y :: l) = y :: rem1 x l. Proof. intros x y l H1. simpl. elim (T_eq_dec x y) ; intros H2. contradiction H1. reflexivity. Qed. Lemma count_cons_eq : forall x l, count T_eq_dec x (x :: l) = S (count T_eq_dec x l). Proof. intros x l. simpl. elim (T_eq_dec x x) ; intros H1. reflexivity. apply False_rec, H1, eq_refl. Qed. Lemma count_cons_diff : forall x y l, x <> y -> count T_eq_dec x (y :: l) = count T_eq_dec x l. Proof. intros x y l H1. simpl. elim (T_eq_dec x y) ; intros H2. contradiction H1. reflexivity. Qed. Lemma rem1_count_inf : forall x y l, count T_eq_dec x (rem1 y l) <= count T_eq_dec x l. Proof. intros x y ; induction l as [|t l IH]. apply le_refl. simpl. elim (T_eq_dec y t) ; simpl ; elim (T_eq_dec x t) ; intros H1 H2. apply le_n_Sn. apply le_refl. apply le_n_S, IH. apply IH. Qed. Lemma rem1_count_0 : forall x y l, count T_eq_dec x l = 0 -> count T_eq_dec x (rem1 y l) = 0. Proof. intros x y l H1. apply sym_eq, le_n_0_eq. rewrite <- H1. apply rem1_count_inf. Qed. Lemma is_enum_eq (x: T)(l1 l2 : list T) : is_enum (l1 ++ x :: l2) -> count T_eq_dec x l1 = 0 /\ count T_eq_dec x l2 = 0. Proof. intros H. assert (H1 := H x). rewrite count_app, count_cons_eq, <- plus_n_Sm in H1. apply eq_add_S in H1. apply plus_is_O, H1. Qed. Lemma is_enum_eq_cor1 (x: T)(l1 l2 : list T) : is_enum (l1 ++ x :: l2) -> count T_eq_dec x l1 = 0. Proof. intros H. destruct (is_enum_eq _ _ _ H) as [H1 _]. assumption. Qed. Lemma is_enum_eq_cor2 (x: T)(l1 l2 : list T) : is_enum (l1 ++ x :: l2) -> count T_eq_dec x l2 = 0. Proof. intros H. destruct (is_enum_eq _ _ _ H) as [_ H1]. assumption. Qed. Lemma indep_enum: forall l1 l2, is_enum l1 -> is_enum l2 -> length l1 = length l2. Proof. assert (aux : forall l1 l2 l3, is_enum (l3++l1) -> is_enum (l3++l2) -> length l1 = length l2). induction l1 as [|t1 l1 IH1] ; intros [|t2 l2] l3 H1 H2. reflexivity. rewrite app_nil_r in H1. assert (H3 := is_enum_eq_cor1 _ _ _ H2). rewrite (H1 t2) in H3. inversion H3. rewrite app_nil_r in H2. assert (H3 := is_enum_eq_cor1 _ _ _ H1). rewrite (H2 t1) in H3. inversion H3. assert (H3 : length (t2 :: l2) = length (t1::rem1 t1 (t2::l2))). simpl. elim (T_eq_dec t1 t2) ; intros a. reflexivity. simpl. f_equal. rewrite <- count_rem1_eq_length. reflexivity. intros H. assert (H2' := H2 t1). rewrite count_app, count_cons_diff, H, (is_enum_eq_cor1 _ _ _ H1) in H2' ; try apply a. inversion H2'. rewrite H3. change (S (length l1) = S (length (rem1 t1 (t2 :: l2)))). f_equal. elim (T_eq_dec t1 t2) ; intros a. rewrite a. rewrite rem1_cons_eq. rewrite <- a in H2. apply (IH1 _ (l3 ++ t1 :: nil)) ; rewrite <- app_assoc, <- app_comm_cons, app_nil_l ; assumption. rewrite rem1_cons_diff; try apply a. apply (IH1 (t2 :: rem1 t1 l2) (l3 ++ t1 :: nil)). rewrite <- app_assoc, <- app_comm_cons, app_nil_l ; assumption. rewrite <- app_assoc, <- app_comm_cons, app_nil_l. intros x. generalize (H2 x). do 2 rewrite count_app. simpl. elim (T_eq_dec x t2) ; elim (T_eq_dec x t1) ; intros H4 H5 H6 ; try (rewrite <- H4 in *|-* ; clear H4) ; try (rewrite <- H5 in *|-* ; clear H5). apply False_rec, a, eq_refl. rewrite <- H6 ; do 2 f_equal. rewrite (is_enum_eq_cor2 _ _ _ H2). apply rem1_count_0, (is_enum_eq_cor2 _ _ _ H2). rewrite <- H6 ; f_equal. rewrite (count_rem1_eq x l2). reflexivity. intros H7. rewrite (is_enum_eq_cor1 _ _ _ H1), H7 in H6. inversion H6. rewrite <- H6 ; f_equal. rewrite <- count_rem1_diff. reflexivity. apply not_eq_sym, H4. intros l1 l2 H1 H2. apply (aux _ _ nil) ; rewrite app_nil_l ; assumption. Qed. End EnumFinType. Section CardFin. Lemma eq_dec_Fin (n: nat) : eq_dec (Fin n). Proof. intros i1 i2. elim (eq_nat_dec (decode_Fin i1) (decode_Fin i2)) ; intros a. left. apply decode_Fin_unique, a. right. intros b. apply a ; rewrite b ; reflexivity. Qed. Lemma first_succ_count_0 (n: nat)(l: list (Fin n)): count (@eq_dec_Fin _) (first n) (map (@succ _) l) = 0. Proof. induction l as [|t l IH]. trivial. simpl. elim (eq_dec_Fin (first n) (succ t)) ; intros a. inversion a. apply IH. Qed. Definition injective (T U : Set)(f: T -> U) : Prop := forall t1 t2, f t1 = f t2 -> t1 = t2. Lemma count_map (T U : Set)(tstT : eq_dec T) (tstU : eq_dec U)(f: T -> U)(h: injective f)(l: list T): forall t, count tstT t l = count tstU (f t) (map f l). Proof. induction l as [|tt l IH] ; intros t. reflexivity. simpl. rewrite IH. elim (tstT t tt) ; intros a. rewrite a. elim (tstU (f tt) (f tt)) ; intros b. reflexivity. apply False_rec, b ; reflexivity. elim (tstU (f t) (f tt)) ; intros b. apply h in b. contradiction a. reflexivity. Qed. Lemma succ_inj (n: nat) : injective (@succ n). Proof. intros i1 i2 H. (* The injection tactic does not help here *) assert (H1 := decode_Fin_S_gt_O i1). rewrite <- (get_cons_ok2 H1), <- (get_cons_ok i2). revert H1 ; rewrite H ; intros H1. apply get_cons_proofirr. Qed. Lemma enum_makeListFin : forall n, is_enum (@eq_dec_Fin _) (makeListFin n). Proof. induction n as [|n IH] ; intros i. inversion i. simpl. elim (eq_dec_Fin i (first n)) ; intros a. rewrite a. rewrite first_succ_count_0. reflexivity. elim (zerop (decode_Fin i)) ; intros b. contradiction a. apply (decode_Fin_0_first _ b). rewrite <- (get_cons_ok1 _ b), <- (count_map (@eq_dec_Fin _) _ (@succ_inj _)). apply IH. Qed. Lemma Fin_inj_alt (n m: nat) : Fin n = Fin m -> n = m. Proof. intros H1. generalize (@eq_dec_Fin n), (makeListFin n), (makeListFin_nb_elem_ok n), (@enum_makeListFin n). rewrite H1. intros Heq l H2 H3. rewrite <- H2, <- makeListFin_nb_elem_ok. apply (indep_enum H3). intros x. rewrite (count_irrel Heq (@eq_dec_Fin _)). apply enum_makeListFin. Qed. End CardFin.