(** IPPJustification.v Version 1.0 February 2012 *) (** runs under V8.3, tested with 8.3pl3 *) (** Ralph Matthes and Celia Picard, I.R.I.T., University of Toulouse and CNRS*) (** justification of the infinite pigeonhole principle used in Graphs.v in the proof of Lemma TeqPerm_GeqPerm from the law of excluded middle *) Require Import Fin. Require Import Ilist. Require Import GPerm. Require Import IlistPerm. Require Import Tools. Require Import List. Require Import Le. Require Import Plus. Require Import Logic.ClassicalFacts. (* this does not assume classical axioms but only studies them *) Require Import Logic.ChoiceFacts. (* this does not assume choice axioms but only studies them *) Set Implicit Arguments. Fixpoint FinIndex (n: nat)(e: Fin n): nat := match e with first m => m | succ m e' => m end. Lemma FinIndexOk (n: nat)(e: Fin n): n = S (FinIndex e). Proof. induction e; reflexivity. Defined. Lemma FinIndexOkCor (n: nat)(e: Fin n): n-1 = FinIndex e. Proof. destruct n. inversion e. apply eq_add_S. rewrite <- FinIndexOk. destruct n; reflexivity. Defined. Lemma SkAux (k: nat): S k - 1 = k. Proof. induction k; reflexivity. Defined. Lemma FinIndexOkCor2 (n: nat)(e: Fin (S n)): n = FinIndex e. Proof. rewrite <- FinIndexOkCor. apply (sym_eq (SkAux n)). Defined. (* a useless decomposition lemma: *) Lemma FinDestruct (n: nat)(e: Fin n): e = rewriteFins (sym_eq(FinIndexOk e)) (first (FinIndex e)) \/ exists e':(Fin(FinIndex e)), e = rewriteFins (sym_eq(FinIndexOk e))(succ e'). Proof. induction e. left. reflexivity. right. exists e. reflexivity. Qed. Definition FinCasesAux (A: Type)(a: A)(n: nat)(f: Fin (n-1) -> A): Fin n -> A. Proof. intro e. refine ((match e in Fin k return (Fin (k-1) -> A) -> A with first _ => fun _ => a | succ _ e' => _ end) f). intro f'. rewrite SkAux in f'. exact (f' e'). Defined. Definition FinCases (A: Type)(a: A)(n: nat)(f: Fin n -> A): Fin (S n) -> A. Proof. intro e. revert f. rewrite <- (SkAux n). intro f. exact (FinCasesAux a f e). Defined. (* just an easier alternative through decode_Fin *) Definition FinCases' (A: Type)(a: A)(n: nat)(f: Fin n -> A): Fin (S n) -> A. Proof. intros i. elim (zerop (decode_Fin i)) ; intros H. exact a. exact (f (get_cons _ H)). Defined. Lemma FinCasesOK1 (A: Type)(a: A)(n: nat)(f: Fin n -> A): FinCases a f (first n) = a. Proof. destruct n; reflexivity. Qed. Lemma FinCasesOK2 (A: Type)(a: A)(n: nat)(f: Fin n -> A)(e: Fin n): FinCases a f (succ e) = f e. Proof. destruct n; reflexivity. Qed. Lemma FinCasesElim (A: Type)(a: A)(n: nat)(f: Fin n -> A)(R: Fin (S n) -> A -> Prop): R (first n) a -> (forall (e: Fin n), R (succ e) (f e)) -> forall (e: Fin (S n)), R e (FinCases a f e). Proof. intros Hyp1 Hyp2 e. elim (zerop (decode_Fin e)) ; intros H. rewrite (decode_Fin_0_first _ H). rewrite FinCasesOK1. assumption. rewrite (decode_Fin_unique _ _ (decode_Fin_get_cons _ H : decode_Fin e = decode_Fin (succ _))). rewrite FinCasesOK2. apply Hyp2. Qed. (* very bad situation where the support for Fin in Coq does not help *) Lemma FinCases_FinCases'(A: Type)(a: A)(n: nat)(f: Fin n -> A) : forall i, FinCases a f i = FinCases' a f i. Proof. intros i ; unfold FinCases' ; elim (zerop (decode_Fin i)) ; intros H ; simpl. rewrite (decode_Fin_0_first _ H). apply FinCasesOK1. rewrite (decode_Fin_unique _ _ (decode_Fin_get_cons _ H : _ = decode_Fin (succ _))) at 1. apply FinCasesOK2. Qed. (* FinCases' will no longer be used *) Lemma FunctionalChoiceFin (m: nat): FunctionalChoice_on (Fin m) nat. Proof. red. induction m ; intros R H. exists (fun _ => 0). intro x; inversion x. set (R' := fun e => R (succ e)). destruct (IHm R') as [f Hyp]; clear IHm. intro x. apply (H (succ x)). destruct (H (first m)) as [y0 Hyp0]. clear H. exists (FinCases y0 f). apply FinCasesElim; assumption. Qed. Definition IP3ClCases (n: nat)(f: IlistPerm3Cert_list n -> nat): IlistPerm3Cert_list (S n) -> nat. Proof. intros [[i1 i2] s]. exact (decode_Fin i1 * (S n) * (S n) + decode_Fin i2 * (S n) + (f s)). Defined. (* we need to study some classical facts - without ever taking them as axioms *) Definition DNE: Prop := forall P: Prop, ~~P -> P. Lemma ExclMiddleImpDNE: excluded_middle -> DNE. Proof. intros EM P H. destruct (EM P) as [H1|H1]. assumption. apply False_rec. contradiction H. Qed. Lemma DeMorganExists: DNE -> forall (A: Type)(P: A -> Prop), ~ (forall a: A, ~ P a) -> exists a: A, P a. Proof. intros DNE A P Hyp. apply DNE. intro H. apply Hyp. intro a. intro H1. apply H. exists a. assumption. Qed. Fixpoint MaxFin (m: nat): (Fin m -> nat) -> nat := match m return (Fin m -> nat) -> nat with | 0 => fun _ => 0 | S m' => fun f => f (first m') + MaxFin (fun e: Fin m' => f (succ e)) end. Lemma MaxFinOk (m: nat)(f: Fin m -> nat)(e: Fin m): MaxFin f >= f e. Proof. revert f; induction e; intros. simpl. apply le_plus_l. simpl. eapply le_trans. eapply (IHe (fun e: Fin k => f (succ e))). apply le_plus_r. Qed. Definition MaxFin' (m: nat) (f: Fin m -> nat) : nat := max_list_nat (map f (makeListFin m)). Lemma MaxFin'Ok (m: nat)(f: Fin m -> nat)(e: Fin m): MaxFin' f >= f e. Proof. apply max_list_max. apply in_map. apply all_Fin_n_in_makeListFin. Qed. Definition IPPFin: Prop := forall (m: nat)(P: nat -> Fin m -> Prop), (forall n: nat, exists f: Fin m, P n f) -> exists f0: Fin m, forall n: nat, exists n': nat, n' >= n /\ P n' f0. Lemma DNEImpIPPFin: DNE -> IPPFin. Proof. intro DNE. red. intros m P HH. apply (DeMorganExists DNE). intro H. assert (H0: forall f0 : Fin m, exists k: nat, forall n: nat, P n f0 -> ~ n >= k). intro. assert (H1 := H f0). clear H. apply (DeMorganExists DNE). intro H2. apply H1. intro k. apply (DeMorganExists DNE). intro H4. assert (H3 := H2 k). clear H2. apply H3. intros n Hyp1 Hyp2. apply (H4 n). split; assumption. clear H. apply FunctionalChoiceFin in H0. destruct H0 as [k' Hyp]. assert (H: forall (n:nat), ~ n >= MaxFin' k'). intro n. destruct (HH n) as [f fgood]. intros H. apply (Hyp _ _ fgood). apply (le_trans _ (MaxFin' k')). apply MaxFin'Ok. assumption. apply (H (S (MaxFin' k'))). apply le_n_Sn. Qed. (* Thus, DNE (or excluded_middle) suffices to justify IPPFin, but we need to justify IPPIlistPerm3Cert. The only difference is that the latter uses IlistPerm3Cert_list m instead of Fin m. The following is the tedious proof that this is inessential. *) Definition IPPGen (A: Set): Prop := forall (P: nat -> A -> Prop), (forall n: nat, exists f: A, P n f) -> exists f0: A, forall n: nat, exists n': nat, n' >= n /\ P n' f0. Lemma IPPGen_gen: (forall m: nat, IPPGen (Fin m)) = IPPFin. Proof. reflexivity. Qed. Lemma IPPGen_bij (A B: Set)(f: A -> B)(g: B -> A)(HypB: Bijective f g): IPPGen A -> IPPGen B. Proof. intro Hyp. red. intros. destruct HypB as [Hyp1 Hyp2]. assert (H': forall n : nat, exists a : A, P n (f a)). intro n. destruct (H n) as [b bgood]. exists (g b). rewrite Hyp2. assumption. destruct (Hyp _ H') as [a0 a0good]. exists (f a0). assumption. Qed. Lemma FmFnFmn_aux(m n p : nat): p < m*n -> p + n < (S m) * n. Proof. rewrite plus_comm. apply plus_lt_compat_l. Qed. Definition FmFnFmn (m n: nat) : Fin m * Fin n -> Fin (m * n). Proof. revert n ; induction m as [|m IH]; intros n [i1 i2]. inversion i1. elim (zerop (decode_Fin i1)) ; intros H1. apply (@code_Fin1 _ (decode_Fin i2)), lt_plus_trans, decode_Fin_inf_n. apply (@code_Fin1 _ (decode_Fin (IH _ ((get_cons _ H1), i2)) + n)). apply FmFnFmn_aux, decode_Fin_inf_n. Defined. Lemma FmnFmFn_aux(m n p : nat): p < S m * n -> n <= p -> p - n < m * n. Proof. intros h1 h2. apply (plus_lt_reg_l _ _ n). rewrite <- (le_plus_minus _ _ h2). apply h1. Qed. Definition FmnFmFn (m n: nat) : Fin (m * n) -> Fin m * Fin n. Proof. revert n ; induction m as [|m IH]; intros n i. inversion i. elim (le_lt_dec n (decode_Fin i)) ; intros a. assert (H1 := FmnFmFn_aux _ (decode_Fin_inf_n i) a). exact (succ (fst (IH _ (code_Fin1 H1))), snd (IH _ (code_Fin1 H1))). exact (first m, code_Fin1 a). Defined. Lemma FmnFmFn_ok1 (m n :nat) (i: Fin ((S m)*n))(h1 : decode_Fin i < n): FmnFmFn _ _ i = (first m, code_Fin1 h1). Proof. simpl. unfold sumbool_rec, sumbool_rect. set (x := le_lt_dec n (decode_Fin i)). change (le_lt_dec n (decode_Fin i)) with x. elim x ; intros a. apply False_rec, (lt_irrefl n), (le_lt_trans _ _ _ a h1). f_equal. treatFinPure. Qed. Lemma FmnFmFn_ok2 (m n :nat) (i: Fin ((S m)*n))(h1 : n <= decode_Fin i): FmnFmFn _ _ i = (succ (fst (FmnFmFn _ _ (code_Fin1 (FmnFmFn_aux _ (decode_Fin_inf_n i) h1)))), (snd (FmnFmFn _ _ (code_Fin1 (FmnFmFn_aux _ (decode_Fin_inf_n i) h1))))). Proof. simpl. unfold sumbool_rec, sumbool_rect. set (x := le_lt_dec n (decode_Fin i)). change (le_lt_dec n (decode_Fin i)) with x. elim x ; intros a. do 3 f_equal ; try treatFinPure. f_equal ; treatFinPure. apply False_rec, (lt_irrefl n), (le_lt_trans _ _ _ h1 a). Qed. Lemma FmFnFmn_ok1 (m n :nat) (i1: Fin (S m)) (i2 : Fin n)(h1 : decode_Fin i1 = 0): FmFnFmn (i1, i2) = code_Fin1 (lt_plus_trans _ _ (m*n) (decode_Fin_inf_n i2)). Proof. simpl. unfold sumbool_rec, sumbool_rect. elim (zerop (decode_Fin i1)) ; intros a. treatFinPure. apply False_rec, (lt_irrefl 0). rewrite h1 in a. assumption. Qed. Lemma FmFnFmn_ok2 (m n :nat) (i1: Fin (S m)) (i2 : Fin n)(h1 : 0 < decode_Fin i1): FmFnFmn (i1, i2) = code_Fin1 (FmFnFmn_aux _ _ (decode_Fin_inf_n (FmFnFmn (get_cons _ h1, i2)))). Proof. simpl. unfold sumbool_rec, sumbool_rect. elim (zerop (decode_Fin i1)) ; intros a. apply False_rec, (lt_irrefl 0). rewrite a in h1. assumption. assert (h2 : get_cons i1 a = get_cons i1 h1) by treatFinPure. rewrite h2. reflexivity. Qed. Lemma decode_FmFnFmn(m n: nat)(i1 : Fin m)(i2 : Fin n) : decode_Fin (FmFnFmn (i1, i2)) = decode_Fin i1 * n + decode_Fin i2. Proof. induction m as [|m]. inversion i1. elim (zerop (decode_Fin i1)) ; intros H1. rewrite FmFnFmn_ok1 ; try assumption. rewrite decode_code1_Id, H1. rewrite mult_0_l. rewrite plus_O_n; reflexivity. rewrite (FmFnFmn_ok2 _ _ H1). rewrite decode_code1_Id. rewrite IHm. rewrite (decode_Fin_get_cons _ H1). simpl. rewrite plus_comm. apply plus_assoc. Qed. Lemma decode_FmnFmFn(m n: nat)(i : Fin (m*n)) : decode_Fin (fst (FmnFmFn _ _ i)) * n + decode_Fin (snd (FmnFmFn _ _ i))= decode_Fin i. Proof. revert i ; induction m as [|m] ; intros i. inversion i. elim (le_lt_dec n (decode_Fin i)) ; intros a. rewrite (FmnFmFn_ok2 _ _ a). simpl. set (i' := code_Fin1 (FmnFmFn_aux m (decode_Fin_inf_n i) a)). change (n + decode_Fin (fst (FmnFmFn m n i')) * n + decode_Fin (snd (FmnFmFn m n i')) = decode_Fin i). rewrite <- plus_assoc. rewrite IHm. unfold i'. rewrite decode_code1_Id. apply le_plus_minus_r, a. rewrite (FmnFmFn_ok1 _ _ a). simpl. apply decode_code1_Id. Qed. Require Import Euclid. Lemma le_exists (n m : nat) : 0 < m -> m <= n -> exists x, exists y, y < m /\ n = x * m + y. Proof. intros H1 H2. destruct (quotient _ H1 n) as [x [y [H3 H4]]]. exists x, y. split ; assumption. Qed. Lemma Fin_bij_mult (m n: nat): Bijective (@FmFnFmn m n) (@FmnFmFn m n). Proof. revert n ; induction m as [|m IH] ; intros n ; split ; try intros [i1 i2] ; try intros i. inversion i1. inversion i. destruct (IH n) as [IH' _]. elim (zerop (decode_Fin i1)); intros a. rewrite (FmFnFmn_ok1 _ _ a). assert (H1 : decode_Fin (code_Fin1 (lt_plus_trans (decode_Fin i2) n (m * n) (decode_Fin_inf_n i2))) < n). rewrite decode_code1_Id. apply decode_Fin_inf_n. rewrite (FmnFmFn_ok1 _ _ H1). rewrite (decode_Fin_0_first _ a). f_equal. treatFinPure. rewrite (FmFnFmn_ok2 _ _ a). assert (H1 : n <= decode_Fin (code_Fin1 (FmFnFmn_aux m n (decode_Fin_inf_n (FmFnFmn (get_cons i1 a, i2)))))). rewrite decode_code1_Id. apply le_plus_r. rewrite (FmnFmFn_ok2 _ _ H1). revert H1. set (x := code_Fin1 (FmFnFmn_aux m n (decode_Fin_inf_n (FmFnFmn (get_cons i1 a, i2))))). intros H1. assert (H2 : FmnFmFn m n (code_Fin1 (FmnFmFn_aux m (decode_Fin_inf_n x) H1)) = (get_cons _ a, i2)). rewrite <- IH'. f_equal. apply decode_Fin_unique. unfold x. repeat rewrite decode_code1_Id. rewrite plus_comm. apply minus_plus. rewrite H2. simpl. rewrite <- (decode_Fin_unique _ _ (decode_Fin_get_cons _ a :_ = decode_Fin (succ _))). reflexivity. apply decode_Fin_unique. rewrite (surjective_pairing (FmnFmFn (S m) n i)). rewrite decode_FmFnFmn. apply decode_FmnFmFn. Qed. Lemma IlistPerm3Cert_list_bij_Fin (n: nat): exists m: nat, exists f: IlistPerm3Cert_list n -> Fin m, exists g: Fin m -> IlistPerm3Cert_list n, Bijective f g. Proof. induction n. exists 1. exists (fun c: IlistPerm3Cert_list 0 => first 0), (fun f: Fin 1 => tt). split; intro. destruct t. reflexivity. apply sym_eq, Fin_first_1. destruct IHn as [m0 [f0 [g0 HypB0]]]. simpl. exists ((S n) * (S n) * m0). rewrite <- mult_assoc. exists (fun x => FmFnFmn ((fst (fst x)) , (FmFnFmn (snd (fst x), (f0 (snd x)))))), (fun i => (fst (FmnFmFn _ _ i), fst (FmnFmFn _ _ (snd (FmnFmFn _ _ i))), g0 (snd (FmnFmFn _ _ (snd (FmnFmFn _ _ i)))))). destruct (Fin_bij_mult (S n) (S n * m0)) as [Fb1 Fb2]. destruct (Fin_bij_mult (S n) m0) as [Fb1' Fb2']. split. intros [[i1 i2] s]. rewrite Fb1. change ((i1, fst (FmnFmFn (S n) m0 (FmFnFmn (i2, f0 s))), g0 (snd (FmnFmFn (S n) m0 (FmFnFmn (i2, f0 s))))) = (i1, i2, s)). rewrite Fb1'. repeat f_equal. apply HypB0. intros i. change (FmFnFmn (fst (FmnFmFn (S n) (S n * m0) i), FmFnFmn (fst (FmnFmFn (S n) m0 (snd (FmnFmFn (S n) (S n * m0) i))), f0 (g0 (snd (FmnFmFn (S n) m0 (snd (FmnFmFn (S n) (S n * m0) i))))))) = i). destruct HypB0 as [Hyp1 Hyp2]. rewrite Hyp2. rewrite <- surjective_pairing. rewrite Fb2'. rewrite <- surjective_pairing. apply Fb2. Qed. Theorem IPPJustification: DNE -> IPPIlistPerm3Cert. Proof. intros DNE m'. change (IPPGen (IlistPerm3Cert_list m')). destruct (IlistPerm3Cert_list_bij_Fin m') as [m [f [g H]]]. apply Bij_sym in H. apply (IPPGen_bij H). unfold IPPGen. apply DNEImpIPPFin, DNE. Qed. (* for emphasis: *) Corollary IPPJustification': (forall P: Prop, P \/ ~P) -> IPPIlistPerm3Cert. Proof. intro Hyp. apply IPPJustification. apply ExclMiddleImpDNE. assumption. Qed.