(** 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 *) (** this is code that conforms to the description in the article "Permutations in Coinductive Graph Representation" by the authors *) Require Import Fin. Require Import Ilist. Require Import GPerm. Require Import IlistPerm. 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. exists (fun _ => 0). intro x; inversion x. intros. set (R' := fun e => R (succ e)). destruct (IHm R') as [f Hyp]; clear IHm. intro x. destruct (H (succ x)) as [y Hyp]. exists y; assumption. destruct (H (first m)) as [y0 Hyp0]. clear H. exists (FinCases y0 f). apply FinCasesElim; assumption. Qed. (* 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. red. intro EM. intros. destruct (EM P). assumption. contradict H. assumption. 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 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. assert (H3 := H2 k). clear H2. apply (DeMorganExists DNE). intro H4. apply H3. intros n Hyp1 Hyp2. apply (H4 n). split; assumption. clear H. apply FunctionalChoiceFin in H0. change (exists k' : Fin m -> nat, forall (f0: Fin m)(n : nat), P n f0 -> ~ n >= k' f0) in H0. destruct H0 as [k' Hyp]. set (kmax := MaxFin k'). assert (H0: forall (f0: Fin m)(n : nat), P n f0 -> ~ n >= kmax). intros f0 n HP Hgeq. apply (Hyp f0 n HP). eapply le_trans. eapply MaxFinOk. assumption. clear Hyp. assert (H: forall (n:nat), ~ n >= kmax). intro n. destruct (HH n) as [f fgood]. apply (H0 _ _ fgood). clear H0. apply (H (S kmax)). 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]. set (P' := fun n a => P n (f a)). assert (H': forall n : nat, exists a : A, P' n a). intro n. destruct (H n) as [b bgood]. exists (g b). red. rewrite Hyp2. assumption. apply (Hyp P') in H'. destruct H' as [a0 a0good]. exists (f a0). intro n. destruct (a0good n) as [n' n'good]. destruct n'good as [n'good1 n'good2]. exists n'. split; assumption. Qed. Lemma lt_rew (x y n m : nat) : x < m -> y < n -> x * n + y < m * n. Proof. intros h1 h2. destruct m as [|m]. inversion h1. destruct n as [|n]. inversion h2. apply lt_n_Sm_le in h1. apply lt_n_Sm_le in h2. apply (le_lt_trans _ (n + m * S n)). rewrite plus_comm. apply plus_le_compat ; try assumption. apply mult_le_compat_r, h1. apply lt_n_Sn. Qed. Definition FmFnFmn' (m n: nat) : Fin m * Fin n -> Fin (m * n). Proof. intros [i1 i2]. exact (code_Fin1 (lt_rew (decode_Fin_inf_n i1) (decode_Fin_inf_n i2))). Defined. 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 FmFnFmn_FmFnFmn'(m n : nat) : forall (i: Fin m * Fin n), FmFnFmn i = FmFnFmn' i. Proof. revert n ; induction m as [|m IH] ; intros n [i1 i2]. inversion i1. simpl. unfold sumbool_rec, sumbool_rect. elim (zerop (decode_Fin i1)) ; intros H1. apply decode_Fin_unique. do 2 rewrite decode_code1_Id. rewrite H1. reflexivity. apply decode_Fin_unique. do 2 rewrite decode_code1_Id. rewrite IH. simpl. rewrite decode_code1_Id. rewrite (decode_Fin_get_cons _ H1). simpl. rewrite (plus_comm n _). rewrite <- plus_assoc. rewrite (plus_comm (decode_Fin i2) n). apply plus_assoc. Qed. 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 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. destruct (IH n) as [_ IH']. elim (le_lt_dec n (decode_Fin i)) ; intros a. rewrite (FmnFmFn_ok2 _ _ a). assert (H1 : 0 < decode_Fin (succ (fst (FmnFmFn m n (code_Fin1 (FmnFmFn_aux m (decode_Fin_inf_n i) a)))))). simpl. apply lt_0_Sn. rewrite (FmFnFmn_ok2 _ _ H1). assert (H2 : FmFnFmn (get_cons _ H1, snd (FmnFmFn m n (code_Fin1 (FmnFmFn_aux m (decode_Fin_inf_n i) a)))) = code_Fin1 (FmnFmFn_aux _ (decode_Fin_inf_n i) a )). rewrite <- IH'. f_equal. rewrite (get_cons_proofirr _ _ (decode_Fin_S_gt_O (fst (FmnFmFn m n (code_Fin1 (FmnFmFn_aux m (decode_Fin_inf_n i) a)))))). rewrite get_cons_ok. symmetry. apply surjective_pairing. rewrite H2. set (H3 := FmFnFmn_aux m n (decode_Fin_inf_n (code_Fin1 (FmnFmFn_aux m (decode_Fin_inf_n i) a)))). generalize H3 ; clear H3. rewrite decode_code1_Id. rewrite plus_comm, <- le_plus_minus ; try assumption. intros H3. treatFinPure. rewrite (FmnFmFn_ok1 _ _ a). rewrite FmFnFmn_ok1 ; try reflexivity. treatFinPure. 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. set (f := fun c: IlistPerm3Cert_list 0 => first 0). set (g := fun f: Fin 1 => tt). exists f; exists g. split; intro. induction t. reflexivity. apply decode_Fin_unique. simpl. assert (H:= decode_Fin_inf_n u). inversion H. symmetry. assumption. inversion H1. 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)))))). exists (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. rewrite Fb2. reflexivity. Qed. Theorem IPPJustification: DNE -> IPPIlistPerm3Cert. Proof. intro DNE. intro 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. assumption. Qed. (* for emphasis: *) Corollary IPPJustification': (forall P: Prop, P \/ ~P) -> IPPIlistPerm3Cert. Proof. intro Hyp. apply IPPJustification. apply ExclMiddleImpDNE. assumption. Qed.