Require Import Arith. Require Import InductiveFiniteSets. Require Import FiniteTypes. Require Import Substitution. Require Import JMeq. Set Implicit Arguments. (*****************************************************************************) (* finj - the positions for the flatten containr *) (*****************************************************************************) Section FinSumm_defs. Definition sum_n (n : nat) : (Fin n -> nat) -> nat. induction n. intros; exact 0. intro f; exact (f (fz n) + (IHn (fun i => f (fs i)))). Defined. Lemma f_emb : forall (n : nat) (f : Fin (S n) -> nat) , f (tp n) + sum_n (fun i : Fin n => f (emb (rv i))) = sum_n (fun i : Fin n => f (fs (rv i))) + f (fz n) . Proof. induction n; simpl; auto. intro f; rewrite (IHn (fun i : Fin (S n) => f (emb i)) ). rewrite (plus_assoc_reverse (f (fs (tp n))) (sum_n (fun i : Fin n => f (fs (emb (rv i))))) (f (fz (S n))) ); reflexivity. Qed. Lemma sum_n_rv (n : nat) (f : Fin n -> nat) : sum_n (fun i : Fin n => f (rv i)) = sum_n f. Proof. induction n; simpl; trivial. intro f; rewrite <- (IHn (fun x : Fin n => f (fs x)) ). rewrite (plus_comm (f (fz n)) (sum_n (fun i : Fin n => f (fs (rv i))))). apply (f_emb f). Qed. Lemma sum_nm (n m : nat) (f : Fin n -> nat) (g : Fin m -> nat) : sum_n (fun i : Fin (n + m) => match FinCase n m i with | inl z => f z | inr z => g z end) = sum_n f + sum_n g. Proof. intros n m f0 g0; induction n. simpl. rewrite (extensionality (fun i : Fin m => g0 i) g0 (fun i : Fin m => refl_equal (g0 i))); reflexivity. simpl. rewrite <- (extensionality (fun i : Fin (n + m) => match FinCase n m i with | inl z => f0 (fs z) | inr z => g0 z end) (fun i : Fin (n + m) => match FinCase (S n) m (fs i) with | inl z => f0 z | inr z => g0 z end) (fincaseS f0 g0) ). rewrite (IHn (fun i : Fin n => f0 (fs i)) ). rewrite <- plus_assoc; trivial. Qed. Lemma sumLastLem (n : nat) (F : Fin (S n) -> nat) : sum_n F = sum_n (fun i => F (emb i)) + F (tp n). Proof. intros n F; induction n; simpl. apply (sym_equal (plus_n_O (F (fz 0)))). rewrite (plus_assoc_reverse (F (fz (S n))) (sum_n (fun i : Fin n => F (fs (emb i)))) (F (fs (tp n)))). rewrite <- (IHn (fun i => F (fs i))); trivial. Qed. Lemma sumLem (n : nat) (F : Fin (S n) -> nat) : sum_n F = F (tp n) + sum_n (fun i0 : Fin n => F (emb (rv i0))). Proof. induction n; simpl; trivial. intro F. generalize (IHn (fun i => F (emb i))). intro H; simpl in H. rewrite <- H. rewrite (plus_permute (F (fs (tp n))) (F (fz (S n))) (sum_n (fun i : Fin n => F (fs (emb i)))) ). set (R := sumLastLem (fun i => F (fs i))); simpl in R; rewrite (trans_equal R (plus_comm (sum_n (fun i => F (fs (emb i)))) (F (fs (tp n))))); trivial. Qed. Definition finj (n : nat) (f : Fin n -> nat) (i : Fin n) : Fin (f i) -> Fin (sum_n f). intros n f i k; induction i. exact (fin_inl (f (fz n)) (sum_n (fun z : Fin n => f (fs z))) k). exact (fin_inr (f (fz n)) (sum_n (fun z => f (fs z))) (IHi (fun z => f (fs z)) k)). Defined. Inductive FinSumm (n : nat) (f : Fin n -> nat) : Fin (sum_n f) -> Set := finPair : forall (i: Fin n) (k : Fin (f i)), FinSumm f (finj f i k). Definition finSumm (n:nat) (f: Fin n -> nat) (x : Fin (sum_n f)) : FinSumm f x. intros n f x; induction n. inversion x. destruct (finsplit (f (fz n)) (sum_n (fun i : Fin n => f (fs i))) x) as [| i _ ]. exact (finPair f (fz n) i). destruct (IHn (fun a => f (fs a)) i) as [x fx ]. exact (finPair f (fs x) fx). Defined. Lemma finjF (n : nat) (i : Fin n) (f : Fin n -> nat) (f1 f2 : Fin (f i)) : finj f i f1 = finj f i f2 -> f1 = f2. Proof. intros n i f0 ff1 f2 H; induction i; simpl in H. apply (fin_inl_inject (sum_n (fun z : Fin n => f0 (fs z))) ff1 f2 H). apply (IHi (fun a : Fin n => f0 (fs a)) ff1 f2 (fin_inr_inject (f0 (fz n)) (finj (fun z : Fin n => f0 (fs z)) i ff1) (finj (fun z : Fin n => f0 (fs z)) i f2) H)). Qed. Lemma finj_inj (n : nat) (i j: Fin n) (f : Fin n -> nat) (fi : Fin (f i)) (fj : Fin (f j)) : finj f i fi = finj f j fj -> i = j /\ JMeq fi fj . Proof. intros n i j f0 f0i f0j H; induction i. destruct j using FinSn_rect. case (fin_inl_inr f0i (finj (fun z : Fin n => f0 (fs z)) j f0j) H). rewrite (finjF (fz n) f0 f0i f0j H); auto. destruct j using FinSn_rect. destruct (IHi j (fun a : Fin n => f0 (fs a)) f0i f0j (fin_inr_inject (f0 (fz n)) (finj (fun z : Fin n => f0 (fs z)) i f0i) (finj (fun z : Fin n => f0 (fs z)) j f0j) H)). split; congruence. case (fin_inl_inr f0j (finj (fun z : Fin n =>f0 (fs z)) i f0i) (sym_equal H)). Qed. Lemma finSumm_uniq (n : nat) (f : Fin n -> nat) (i : Fin n) (k : Fin (f i)) (fx :FinSumm f (finj f i k)) : fx = finSumm f (finj f i k) . Proof. intros n f i k fx; destruct fx. induction i0; simpl. rewrite (finsplit_inl (sum_n (fun i0 : Fin n => f (fs i0))) k0); trivial. rewrite (finsplit_inr (f (fz n)) (finj (fun z: Fin n => f (fs z)) i0 k0)). rewrite <- (IHi0 (fun a : Fin n => f (fs a)) i0 k0); trivial. Qed. Lemma finjFmLem (n : nat ) (F : Fin (S n) -> nat) (j : Fin (F (tp n))) : JMeq (finj F (tp n) j) (fin_inr (sum_n (fun i => F (emb i))) (F (tp n)) j). Proof. intros; induction n; simpl. exact (fin_inl_O j). apply (dp_rwt Fin (fun (a : nat) (fn : Fin a) => JMeq (fin_inr (F (fz (S n))) a fn) (fin_inr (F (fz (S n)) + sum_n (fun i => F (fs (emb i)))) (F (fs (tp n))) j)) (sym_equal (sumLastLem (fun x => F (fs x)))) (sym_JMeq (IHn (fun i => F (fs i)) j)) ). apply (fin_inr_inr (F (fz (S n))) (sum_n (fun i => F (fs (emb i)))) j). Qed. Lemma finjFmLem2 (n : nat ) (F : Fin (S n) -> nat) (i : Fin n) (j : Fin (F (emb i))) (jt : Fin (F (tp n))) : JMeq (finj F (emb i) j) (fin_inr (sum_n (fun i => F (emb (rv i)))) (F (tp n)) jt) -> False . Proof. intros n F i j jt; induction i; simpl in *. set (R := f_emb (fun i => F (emb i))) ; simpl in R; rewrite R; clear R. set (R := sumLem (fun i => F (fs i)) ); simpl in R. intro H; rewrite (plus_comm (sum_n (fun i : Fin n => F (fs (emb (rv i))))) (F (fz (S n))))in H . case (fin_inl_inrN (F (fs (fz n))) (sum_n (fun i : Fin n => F (fs (fs i)))) (sum_n (fun i : Fin n => F (fs (emb (rv i))))) (trans_equal R (plus_comm (F (fs (tp n))) (sum_n (fun i => F (fs (emb (rv i))))))) j jt H). set (R := sumLem (fun i => F (emb i))); simpl in R; rewrite <- R; clear R . set (R := sumLastLem (fun i => F (fs i))); simpl in R. set (R' := sum_n_rv (fun i => F (fs i))); simpl in R'. rewrite <- ( plus_reg_l (sum_n (fun i : Fin n => F (fs (emb (rv i))))) (sum_n (fun i : Fin n => F (fs (emb i)))) (F (fs (tp n))) (trans_equal (sym_equal (trans_equal (sym_equal R) (sym_equal R'))) (plus_comm (sum_n (fun i : Fin n => F (fs (emb i)))) (F (fs (tp n)))))) . apply (fun H => fin_inr_inrPlus (F (fz (S n))) (F (fs (fz n))) (sum_n (fun i : Fin n => F (fs (fs i)))) (sum_n (fun i0 : Fin n => F (fs (emb (rv i0))))) (trans_equal (sym_equal R') (plus_comm (F (fs (tp n))) (sum_n (fun i : Fin n => F (fs (emb (rv i))))))) jt (IHi (fun i => F (fs i)) j jt) H). Qed. Lemma finjFmLem3 (n : nat ) (F : Fin (S n) -> nat) (i : Fin n) (j : Fin (F (emb i))): JMeq (finj F (emb i) j) (fin_inl (sum_n (fun i => F (emb i))) (F (tp n)) (finj (fun i => F (emb i)) i j )). Proof. intros n F i j. induction i; simpl. set ( R := sumLastLem (fun i => F (fs i)) ); simpl in R; rewrite R. apply (finl_inl_inlx (sum_n (fun i : Fin n => F (fs (emb i)))) (F (fs (tp n))) j). set ( R := sumLastLem (fun i => F (fs i)) ); simpl in R. set (X := IHi (fun i => F (fs i)) j); simpl in X. apply (dp_rwt Fin (fun (x : nat) (fx : Fin x) => JMeq (fin_inr (F (fz (S n))) x fx) (fin_inl (F (fz (S n)) + sum_n (fun i0 : Fin n => F (fs (emb i0)))) (F (fs (tp n))) (fin_inr (F (fz (S n))) (sum_n (fun z : Fin n => F (fs (emb z)))) (finj (fun z : Fin n => F (fs (emb z))) i j)))) (sym_equal R) (sym_JMeq X) ). set (x := F (fz (S n))); induction x; simpl; trivial. apply ( fin_fs (plus_assoc_reverse x (sum_n (fun i : Fin n => F (fs (emb i)))) (F (fs (tp n)))) IHx ). Qed. Lemma finjLem (n : nat) (F : Fin n -> nat) (i : Fin n) (fi : Fin (F i)) (j : Fin n) (rj : Fin (F (rv j))) : JMeq (finj F i fi) (rv (finj (fun z => F (rv z)) j rj)) -> i = (rv j) /\ JMeq fi (rv rj) . Proof. intros n F i fi j rj H. induction j. destruct (finEmtp i). split; trivial. simpl in *. generalize (trans_JMeq H (rvFin_inl (sum_n (fun z => F (emb (rv z)))) rj)). clear H; intro H; generalize (trans_JMeq (sym_JMeq (finjFmLem F fi)) H); clear H. intro H; rewrite (sum_n_rv (fun i => F (emb i))) in H. case (fin_inr_inject (sum_n (fun i => F (emb i))) fi (rv rj) (JMeq_eq H)); trivial. generalize (trans_JMeq H (rvFin_inl (sum_n (fun z => F (emb (rv z)))) rj)). clear H; intro H; simpl in *. case (finjFmLem2 F i fi (rv rj) H ). destruct (finEmtp i); simpl in *. generalize (trans_JMeq H (rvFin_inr (F (tp n)) (finj (fun z : Fin n => F (emb (rv z))) j rj))); clear H; intro H. set (P := trans_JMeq (sym_JMeq (finjFmLem F fi)) H). set (R := sumLastLem F); simpl in R. set (R' := sum_n_rv F ); simpl in R'. rewrite <- ( plus_reg_l (sum_n (fun i : Fin n => F (emb (rv i)))) (sum_n (fun i : Fin n => F (emb i))) (F (tp n)) (trans_equal (sym_equal (trans_equal (sym_equal R) (sym_equal R'))) (plus_comm (sum_n (fun i : Fin n => F (emb i))) (F (tp n))))) in P . case (finsplit_inl_inr (rv (finj (fun z : Fin n => F (emb (rv z))) j rj)) fi (sym_equal (JMeq_eq P))). generalize (trans_JMeq H (rvFin_inr (F (tp n)) (finj (fun z : Fin n => F (emb (rv z))) j rj))); clear H. intro H; generalize (trans_JMeq (sym_JMeq H) (finjFmLem3 F i fi)); clear H; intro H. set (R := sumLastLem F); simpl in R. set (R' := sum_n_rv F ); simpl in R'. destruct ((IHj (fun i => F (emb i)) i fi rj) (sym_JMeq (fin_inl_JM (F (tp n)) ( plus_reg_l (sum_n (fun i : Fin n => F (emb (rv i)))) (sum_n (fun i : Fin n => F (emb i))) (F (tp n)) (trans_equal (sym_equal (trans_equal (sym_equal R) (sym_equal R'))) (plus_comm (sum_n (fun i : Fin n => F (emb i))) (F (tp n))))) (rv (finj (fun z : Fin n => F (emb (rv z))) j rj)) (finj (fun i : Fin n => F (emb i)) i fi) H ))); split; auto. rewrite <- H0; trivial. Qed. Axiom jm_ext : forall ( X A B: Set) (f : A -> X) (g : B -> X) , (forall (a: A) (b : B), JMeq a b -> f a = g b) -> JMeq f g. Lemma Fnm (n m : nat)(i : Fin n) (F : Fin (S n) -> nat) (G : Fin m -> nat) (FG : Fin (S n + m) -> nat) (H : FG = fun x : Fin (S n + m) => match FinCase (S n) m (fin_inl (S n) m (fs i)) with | inl z => F z | inr z => G z end) : (forall (x : Fin n) (b : Fin (S n)), b = fs x) -> JMeq FG F . intros. apply jm_ext. rewrite H. intros. rewrite (FinCase_inl m (fs i)). case (H0 i b); trivial. Qed. Lemma finjInl_fz (n m : nat) (F :Fin (S n) -> nat)(G : Fin m -> nat) (j : Fin (F(fz n))) : JMeq (fin_inl (F (fz n)) (sum_n (fun z : Fin(n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)) j) (fin_inl (F (fz n) + sum_n (fun i : Fin n => F (fs i))) (sum_n G) (fin_inl (F (fz n)) (sum_n (fun z : Fin n => F (fs z))) j)). Proof. intros. induction j; simpl. set (R := sum_nm (fun z : Fin n => F (fs z)) G ); simpl in R. apply (eq_subs (fun x : nat => JMeq (fz( n0 + (sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)))) (fz x) ) (plus_assoc n0 (sum_n (fun i : Fin n => F (fs i))) (sum_n G)) ). rewrite (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) in R; rewrite R; trivial. set (R := sum_nm F G ); simpl in R. rewrite <- (plus_assoc ( F (fz n)) (sum_n (fun i : Fin n => F (fs i))) (sum_n G)) in R. apply (fin_fs (sym_equal (trans_equal (f_equal (plus n0) ( plus_reg_l ( sum_n (fun i : Fin (n + m) => match FinCase (S n) m (fs i) with | inl z => F z | inr z => G z end)) (sum_n (fun i : Fin n => F (fs i)) + sum_n G) (F (fz n)) R )) (plus_assoc n0 (sum_n (fun i : Fin n => F (fs i))) (sum_n G)) ) ) IHj). Qed. Lemma finj_f (n : nat) (F G : Fin n -> nat) (H : F = G) (i : Fin n) (fi : Fin (F i)) (gi : Fin (G i)) : JMeq fi gi -> JMeq (finj F i fi) (finj G i gi). Proof. intros n F G H; case H. intros i fi gi H1; case (JMeq_eq H1); trivial. Qed. Definition finJmeq (n m : nat) (H : n = m) (i: Fin n) : JMeq i (eq_subs (fun x : nat => Fin x) H i). intros n m H; case H. intro i; auto. Qed. Lemma finjInl_Inl (n m : nat) (F : Fin n -> nat) (G : Fin m -> nat) (i : Fin n) (Fj : Fin (F i)) (k : Fin match FinCase n m (fin_inl n m i) with | inl z => F z | inr z => G z end ) : JMeq Fj k -> JMeq (finj (fun a : Fin (n + m) => match FinCase n m a with | inl z => F z | inr z => G z end) (fin_inl n m i) k) (fin_inl (sum_n F) (sum_n G) (finj F i Fj)). Proof. intros n m F G i Fj k H . induction i; simpl in *. case (JMeq_eq H). apply (finjInl_fz F G Fj). simpl in *. set (R := sum_nm F G); simpl in R. rewrite <- (plus_assoc ( F (fz n)) (sum_n (fun i : Fin n => F (fs i))) (sum_n G)) in R. set (R1 := eq_subs (fun FF : Fin (n +m) -> nat => sum_n FF = sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) ) (sym_equal (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) ) (refl_equal(sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)))); simpl in R1. apply (dp_rwt Fin (fun (x : nat ) (fx : Fin x) => JMeq (fin_inr (F (fz n)) x fx) (fin_inl (F (fz n) + sum_n (fun i0 : Fin n => F (fs i0))) (sum_n G) (fin_inr (F (fz n)) (sum_n (fun z : Fin n => F (fs z))) (finj (fun z : Fin n => F (fs z)) i Fj)))) R1 (sym_JMeq (finj_f (sym_equal (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) ) (fin_inl n m i) (finJmeq (sym_equal (fincaseS F G (fin_inl n m i))) k))) ). rewrite <- R1 in R. apply (dp_rwt Fin (fun (x : nat) (fx : Fin x) => JMeq (fin_inr (F (fz n)) x fx) (fin_inl (F (fz n) + sum_n (fun i0 : Fin n => F (fs i0))) (sum_n G) (fin_inr (F (fz n)) (sum_n (fun z : Fin n => F (fs z))) (finj (fun z : Fin n => F (fs z)) i Fj)))) (sym_equal ( plus_reg_l ( sum_n (fun i : Fin (n + m) => match FinCase n m i with | inl z => F (fs z) | inr z => G z end)) (sum_n (fun i : Fin n => F (fs i)) + sum_n G) (F (fz n)) R )) (sym_JMeq (IHi (fun i : Fin n => F (fs i)) Fj (eq_subs (fun x : nat => Fin x) (sym_equal (fincaseS F G (fin_inl n m i))) k ) (trans_JMeq H (finJmeq (sym_equal (fincaseS F G (fin_inl n m i))) k )) )) ). clear H ; clear R; clear R1. set (Y := F (fz n)). induction Y; simpl; trivial. apply (fin_fs (sym_equal (plus_assoc Y (sum_n (fun i : Fin n => F (fs i))) (sum_n G))) IHY). Qed. Lemma fincF (n m : nat) (F : Fin n -> nat) (G : Fin m -> nat) (i : Fin n) : (match FinCase n m (fin_inl n m i ) with | inl z => F z | inr z => G z end) = (F i). Proof. intros n m F G i. rewrite (FinCase_inl m i); trivial. Qed. Lemma finjInlr_false (n m : nat) (F : Fin (S n) -> nat) (G : Fin m -> nat) (j : Fin n ) (Fj : Fin (F (fz n))) ( k : Fin match FinCase (S n) m (fin_inl (S n) m (fs j)) with | inl z => F z | inr z => G z end ): JMeq (finj (fun a : Fin (S n + m) => match FinCase (S n) m a with | inl z => F z | inr z => G z end) (fin_inl (S n) m (fs j)) k) (fin_inl (sum_n F) (sum_n G) (finj F (fz n) Fj)) -> False. Proof. intros n m F G j Fj k . destruct j; simpl. intro H. set (H1 := trans_JMeq (sym_JMeq H) (fin_inr_inlJm (F (fz (S n))) (sum_n (fun i : Fin (n + m) => match FinCase (S (S n)) m (fs (fs i)) with | inl z => F z | inr z => G z end)) k)). rewrite (extensionality (fun i : Fin (n + m) => match FinCase (S (S n)) m (fs (fs i)) with | inl z => F z | inr z => G z end) (fun i : Fin (n + m) => match FinCase n m i with | inl z => F (fs (fs z)) | inr z => G z end) ) in H1. rewrite (sum_nm (fun i : Fin n => F (fs (fs i))) G) in H1. case (fin_inl_inl_inr1 (sum_n (fun i : Fin n => F (fs (fs i)))) (sum_n G) (fincF F G (fs (fz n)) ) Fj k H1 ). intro a. destruct (finsplit n m a). set (R := FinCase_inl m (fs (fs i))); simpl in R; rewrite R. rewrite (FinCase_inl m i); trivial. set (R := FinCase_inr (S (S n)) j); simpl in R; rewrite R. rewrite (FinCase_inr n j); trivial. intro H. set (R := sum_nm (fun i => (F (fs (fs i)))) G); simpl in R. rewrite <- (extensionality (fun i : Fin (n + m) => match FinCase (S (S n)) m (fs (fs i)) with | inl z => F z | inr z => G z end) (fun i : Fin (n + m) => match FinCase n m i with | inl z => F (fs (fs z)) | inr z => G z end) ) in R. case (fin_inl_inr_lr (F (fs (fz n))) (sum_n (fun i : Fin n => F (fs (fs i)))) (sum_n G) R (finj (fun z : Fin (n + m) => match FinCase (S (S n)) m (fs (fs z)) with | inl z0 => F z0 | inr z0 => G z0 end) (fin_inl n m j) k) Fj H). intro a. destruct (finsplit n m a). set (R1 := FinCase_inl m (fs (fs i))); simpl in R1; rewrite R1. rewrite (FinCase_inl m i); trivial. set (R1 := FinCase_inr (S (S n)) j0); simpl in R1; rewrite R1. rewrite (FinCase_inr n j0); trivial. Qed. Lemma finjInl_false (n m : nat) (F : Fin (S n) -> nat) (G : Fin m -> nat) (i : Fin n) (Fi : Fin (F (fs i))) (j : Fin (F (fz n))) : JMeq (fin_inl (F (fz n)) (sum_n (fun a : Fin (n + m) => match FinCase(S n) m (fs a) with | inl z => F z | inr z => G z end)) j) (fin_inl (F (fz n) + sum_n (fun i : Fin n => F (fs i)))(sum_n G) (fin_inr (F (fz n)) (sum_n (fun z : Fin n => F (fs z))) (finj (fun z : Fin n => F (fs z)) i Fi))) -> False. Proof. intros n m F G i Fi j. induction j; simpl . set (R := sum_nm F G); simpl in R. rewrite <- (plus_assoc ( F (fz n)) (sum_n (fun i : Fin n => F (fs i))) (sum_n G)) in R. rewrite <- (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) . set (R1 := eq_subs (fun FF : Fin (n +m) -> nat => sum_n FF = sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) ) (sym_equal (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) ) (refl_equal(sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)))) ; simpl in R1. rewrite <- R1 in R. rewrite ( plus_reg_l ( sum_n (fun i : Fin (n + m) => match FinCase n m i with | inl z => F (fs z) | inr z => G z end)) (sum_n (fun i : Fin n => F (fs i)) + sum_n G) (F (fz n)) R) . apply ( eq_subs (fun x : nat => JMeq (fz x) (fs (fin_inl (n0 + sum_n (fun z : Fin n => F (fs z))) (sum_n G) (fin_inr n0 (sum_n (fun z : Fin n => F (fs z))) (finj (fun z : Fin n => F (fs z)) i Fi)))) -> False ) (sym_equal (plus_assoc n0 (sum_n (fun i : Fin n => F (fs i))) (sum_n G))) ). intro H; set (H1 := JMeq_eq H); discriminate H1. set (R1 := eq_subs (fun FF : Fin (n +m) -> nat => sum_n FF = sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) ) (sym_equal (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) ) (refl_equal(sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)))) ; simpl in R1. rewrite <- R1 in IHj. rewrite <- R1 . rewrite (sum_nm (fun i : Fin n => F (fs i)) G). rewrite (sum_nm (fun i : Fin n => F (fs i)) G) in IHj. apply (fun i => IHj (Jmeq_fsInject (plus_assoc n0 (sum_n (fun i : Fin n => F (fs i))) (sum_n G)) i ) ). Qed. Lemma finj_feq_inj (n : nat) (F F1 : Fin n -> nat) (H : F = F1) (i j : Fin n) (Fi :Fin (F i)) (F1j : Fin (F1 j)) : JMeq (finj F i Fi) (finj F1 j F1j ) -> i = j /\ JMeq Fi F1j. Proof. intros n F F1 H; case H; clear H. intros i j Fi F1j H. apply (finj_inj i j F Fi F1j (JMeq_eq H) ). Qed. Lemma Jmeq_fin_inr1 (x z y A: nat) (H : A = z + y) (j : Fin A) (i : Fin y) : JMeq (fin_inr x A j) (fin_inr (x + z) y i) -> JMeq j (fin_inr z y i). Proof. intros x z y A H; rewrite H. clear H. intros . induction x; simpl in *; auto. apply (IHx (Jmeq_fsInject (plus_assoc x z y) H)). Qed. Lemma finjInr_inj (n m : nat) (F : Fin n -> nat) (G : Fin m -> nat) (i j : Fin m) (Gj : Fin (G j)) (k : Fin match FinCase n m (fin_inr n m i) with | inl z => F z | inr z => G z end ) : JMeq (finj (fun a : Fin (n + m) => match FinCase n m a with | inl z => F z | inr z => G z end) (fin_inr n m i) k) (fin_inr (sum_n F) (sum_n G) (finj G j Gj)) -> i = j /\ JMeq Gj k. Proof. intros n m F G i j Gj k. induction n; simpl in *. intro H. destruct (finj_feq_inj (extensionality (fun a : Fin m => G a) G (fun x : Fin m => (refl_equal (G x)))) i j k Gj H); split; trivial. apply (sym_JMeq H1). intro H. set (R := sum_nm (fun z : Fin n => F (fs z)) G); simpl in R. rewrite (extensionality (fun i : Fin (n + m) => match FinCase n m i with | inl z0 => F (fs z0) | inr z0 => G z0 end) (fun i : Fin (n + m) => match FinCase (S n) m (fs i) with | inl z0 => F z0 | inr z0 => G z0 end) (fun i : Fin (n + m) => fincaseS F G i)) in R. destruct (IHn (fun z => F (fs z)) (eq_subs (fun z : nat => Fin z)(sym_equal (fincaseS F G (fin_inr n m i)))k ) (trans_JMeq (finj_f (extensionality (fun z : Fin (n + m) => match FinCase n m z with | inl z0 => F (fs z0) | inr z0 => G z0 end) (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)(fun a : Fin (n + m) => fincaseS F G a))(fin_inr n m i) (sym_JMeq ( finJmeq (sym_equal (fincaseS F G (fin_inr n m i))) k))) (Jmeq_fin_inr1 (F (fz n)) (sum_n (fun i : Fin n => F (fs i))) R (finj (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fin_inr n m i) k) (finj G j Gj) H))). split; trivial. apply (trans_JMeq H1 (sym_JMeq (finJmeq (sym_equal (fincaseS F G (fin_inr n m i))) k))). Qed. (* finjInl_inj proof starts here! *) Lemma finjInl_inj (n m : nat) (F : Fin n -> nat) (G : Fin m -> nat) (i j : Fin n) (Fj : Fin (F i)) (k : Fin match FinCase n m (fin_inl n m j) with | inl z => F z | inr z => G z end ) : JMeq (finj (fun a : Fin (n + m) => match FinCase n m a with | inl z => F z | inr z => G z end) (fin_inl n m j) k) (fin_inl (sum_n F) (sum_n G) (finj F i Fj)) -> i = j /\ JMeq Fj k. Proof. intros n m F G i j Fj k. induction j. destruct i using FinSn_rect; simpl in *. intro H; case (finjInl_false F G i Fj k H). trivial. set (R1 := eq_subs (fun FF : Fin (n +m) -> nat => sum_n FF = sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) ) (sym_equal (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) ) (refl_equal(sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)))) ; simpl in R1. intro H; set (H1 := eq_subs (fun x : nat => JMeq (fin_inl (F (fz n)) x k) (fin_inl (F (fz n) + sum_n (fun i : Fin n => F (fs i))) (sum_n G) (fin_inl (F (fz n)) (sum_n (fun z : Fin n => F (fs z))) Fj))) (sym_equal R1) H ); simpl in H1. rewrite (sum_nm (fun x : Fin n => F (fs x)) G) in H1. case (fin_inl_inject (sum_n (fun x : Fin n => F (fs x)) + sum_n G) k Fj (JMeq_eq (trans_JMeq H1 (sym_JMeq (finl_inl_inlx (sum_n (fun x : Fin n => F (fs x))) (sum_n G) Fj))))); split; trivial. destruct i using FinSn_rect. simpl. set (R := sum_nm F G); simpl in R. set (R1 := eq_subs (fun FF : Fin (n +m) -> nat => sum_n FF = sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) ) (sym_equal (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) ) (refl_equal(sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)))) ; simpl in R1. apply (dp_rwt Fin (fun (x : nat) (fx : Fin x) => JMeq (fin_inr (F (fz n)) x fx ) (fin_inl (F (fz n) + sum_n (fun i : Fin n => F (fs i))) (sum_n G) (fin_inr (F (fz n)) (sum_n (fun z : Fin n => F (fs z))) (finj (fun z : Fin n => F (fs z)) i Fj))) -> fs i = fs j /\ JMeq Fj k ) R1 (sym_JMeq (finj_f (sym_equal (extensionality (fun a : Fin ( n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G))) (fin_inl n m j) (finJmeq (sym_equal (fincaseS F G (fin_inl n m j))) k))) ). intro h. set (X := trans_JMeq h (fin_inl_inrJm (F (fz n)) (sum_n G) (finj (fun z : Fin n => F (fs z)) i Fj))). rewrite <- (plus_assoc ( F (fz n)) (sum_n (fun i : Fin n => F (fs i))) (sum_n G)) in R. rewrite <- R1 in R. destruct (IHj (fun x : Fin n => F (fs x)) i Fj (eq_subs (fun x : nat => Fin x) (sym_equal (fincaseS F G (fin_inl n m j))) k) (fin_inrJm (F (fz n)) ( plus_reg_l ( sum_n (fun i : Fin (n + m) => match FinCase n m i with | inl z => F (fs z) | inr z => G z end)) (sum_n (fun i : Fin n => F (fs i)) + sum_n G) (F (fz n)) R) (finj (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end) (fin_inl n m j) (eq_subs (fun x : nat => Fin x) (sym_equal (fincaseS F G (fin_inl n m j))) k)) (fin_inl (sum_n (fun z : Fin n => F (fs z))) (sum_n G) (finj (fun z : Fin n => F (fs z)) i Fj)) X) ). apply (eq_subs (fun x : Fin n => fs x = fs j /\ JMeq Fj k) (sym_equal H) ). split; trivial. apply (trans_JMeq H0 (sym_JMeq (finJmeq (sym_equal (fincaseS F G (fin_inl n m j))) k))). intro H. case (finjInlr_false F G j Fj k H). Qed. Lemma finjInr_Inr (n m : nat) (F : Fin n -> nat) (G : Fin m -> nat) (j : Fin m) (Gj : Fin (G j)) (k : Fin match FinCase n m (fin_inr n m j) with | inl z => F z | inr z => G z end ) : JMeq Gj k -> JMeq (finj (fun a : Fin (n + m) => match FinCase n m a with | inl z => F z | inr z => G z end) (fin_inr n m j) k) (fin_inr (sum_n F) (sum_n G) (finj G j Gj)). Proof. intros. induction n; simpl. apply (sym_JMeq (finj_f (extensionality G (fun a : Fin m => G a) (fun a :Fin m => refl_equal (G a))) j H)). simpl in *. set (R := sum_nm F G); simpl in R; rewrite <- (plus_assoc ( F (fz n)) (sum_n (fun i : Fin n => F (fs i))) (sum_n G)) in R. set (R1 := eq_subs (fun FF : Fin (n +m) -> nat => sum_n FF = sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) ) (sym_equal (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) ) (refl_equal(sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)))); simpl in R1. rewrite <- R1 in R. apply (dp_rwt Fin (fun (x : nat ) (fx : Fin x) => JMeq (fin_inr (F (fz n)) x fx) (fin_inr (F (fz n) + sum_n (fun i : Fin n => F (fs i))) (sum_n G) (finj G j Gj))) R1 (sym_JMeq (finj_f (sym_equal (extensionality (fun a : Fin (n + m) => match FinCase n m a with | inl z => F (fs z) | inr z => G z end ) (fun a : Fin (n + m) => match FinCase (S n) m (fs a) with | inl z => F z | inr z => G z end) (fincaseS F G)) ) (fin_inr n m j) (finJmeq (sym_equal (fincaseS F G (fin_inr n m j))) k)))). clear R1. apply (dp_rwt Fin (fun (x : nat) (fx : Fin x) => JMeq (fin_inr (F (fz n)) x fx) (fin_inr (F (fz n) + sum_n (fun i : Fin n => F (fs i))) (sum_n G) (finj G j Gj))) (sym_equal ( plus_reg_l ( sum_n (fun i : Fin (n + m) => match FinCase n m i with | inl z => F (fs z) | inr z => G z end)) (sum_n (fun i : Fin n => F (fs i)) + sum_n G) (F (fz n)) R )) (sym_JMeq (IHn (fun i : Fin n => F (fs i)) (eq_subs (fun x : nat => Fin x) (sym_equal (fincaseS F G (fin_inr n m j))) k) (trans_JMeq H (finJmeq (sym_equal (fincaseS F G (fin_inr n m j))) k)) )) ). clear H; clear R. set (X := F (fz n)). induction X; simpl; trivial. apply (fin_fs (sym_equal (plus_assoc X (sum_n (fun i : Fin n => F (fs i))) (sum_n G))) IHX). Qed. Lemma finjInr_Inl_false (n m : nat) (F : Fin n -> nat) (G : Fin m -> nat)(i : Fin n) (j : Fin m) (Fi : Fin (F i)) (k : Fin match FinCase n m (fin_inr n m j) with | inl z => F z | inr z => G z end ) : JMeq (finj (fun a : Fin (n + m) => match FinCase n m a with | inl z => F z | inr z => G z end) (fin_inr n m j) k) (fin_inl (sum_n F) (sum_n G) (finj F i Fi)) -> False. Proof. intros. induction i; simpl in *. case (Jmeq_fin_inl_inr3 (sum_n (fun i : Fin n => F (fs i))) (sum_n G) (trans_equal (sym_equal (eq_subs (fun Q : Fin (n + m) -> nat => sum_n Q = (sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end))) (sym_equal (extensionality (fun z : Fin (n + m) => match FinCase n m z with | inl z0 => F (fs z0) | inr z0 => G z0 end) (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fincaseS F G))) (refl_equal (sum_n (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end))))) (sum_nm (fun i => F (fs i)) G)) (finj (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fin_inr n m j) k) Fi H ). set (H1:= trans_JMeq H (sym_JMeq (fin_inr_inlJm (F (fz n)) (sum_n G) (finj (fun z : Fin n => F (fs z)) i Fi)))). set (R := sum_nm (fun z => F (fs z)) G); simpl in R. rewrite (extensionality (fun z : Fin (n + m) => match FinCase n m z with | inl z0 => F (fs z0) | inr z0 => G z0 end) (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fincaseS F G)) in R. apply (IHi (fun z => F (fs z)) Fi (eq_subs (fun x : nat => Fin x) (sym_equal (fincaseS F G (fin_inr n m j))) k) (sym_JMeq (trans_JMeq (Jmeq_fin_inr (F (fz n)) (sym_equal R) (finj (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fin_inr n m j) k) (fin_inl (sum_n (fun z : Fin n => F (fs z))) (sum_n G) (finj (fun z : Fin n => F (fs z)) i Fi)) H1) (sym_JMeq (finj_f (extensionality (fun z : Fin (n + m) => match FinCase n m z with | inl z0 => F (fs z0) | inr z0 => G z0 end) (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fincaseS F G)) (fin_inr n m j) (sym_JMeq (finJmeq (sym_equal (fincaseS F G (fin_inr n m j))) k))))))). Qed. Lemma finjInl_Inr_false (n m : nat) (F : Fin n -> nat) (G : Fin m -> nat)(i : Fin n) (j : Fin m) (Gj : Fin (G j)) (k : Fin match FinCase n m (fin_inl n m i) with | inl z => F z | inr z => G z end ) : JMeq (finj (fun a : Fin (n + m) => match FinCase n m a with | inl z => F z | inr z => G z end) (fin_inl n m i) k) (fin_inr (sum_n F) (sum_n G) (finj G j Gj)) -> False. Proof. intros. induction i; simpl in *. set (R := sum_nm (fun z => F (fs z)) G); simpl in R. rewrite (extensionality (fun z : Fin (n + m) => match FinCase n m z with | inl z0 => F (fs z0) | inr z0 => G z0 end) (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fun i : Fin (n + m) => fincaseS F G i)) in R. case (fin_inl_inrZ1 (sum_n (fun i : Fin n => F (fs i))) R k (finj G j Gj) H ). set (R := sum_nm (fun z => F (fs z)) G); simpl in R. rewrite (extensionality (fun z : Fin (n + m) => match FinCase n m z with | inl z0 => F (fs z0) | inr z0 => G z0 end) (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fun i : Fin (n + m) => fincaseS F G i)) in R. apply (IHi (fun x => F (fs x)) (eq_subs (fun z => Fin z) (sym_equal (fincaseS F G (fin_inl n m i))) k) (trans_JMeq (finj_f (extensionality (fun z : Fin (n + m) => match FinCase n m z with | inl z0 => F (fs z0) | inr z0 => G z0 end) (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end)(fun a : Fin (n + m) => fincaseS F G a))(fin_inl n m i) (sym_JMeq ( finJmeq (sym_equal (fincaseS F G (fin_inl n m i))) k))) (Jmeq_fin_inr1 (F (fz n)) (sum_n (fun i : Fin n => F (fs i))) R (finj (fun z : Fin (n + m) => match FinCase (S n) m (fs z) with | inl z0 => F z0 | inr z0 => G z0 end) (fin_inl n m i) k) (finj G j Gj) H)) ). Qed. End FinSumm_defs .