IPPJustification.v

(** 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.

Definition FinIndex (n: nat)(e: Fin n): nat :=
  match e with first m => m | @succ m e' => m end.

(* an interactive definition: *)
Definition FinIndex_alt (n: nat)(e: Fin n): nat.
Proof.
  destruct e; exact k.
Defined.

Lemma FinIndex_alt_is_same (n: nat)(e: Fin n): FinIndex e = FinIndex_alt e.
Proof.
  induction e; reflexivity.
Qed.

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 ; cbn.
  - 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.
  - cbn.
    apply le_plus_l.
  - cbn.
    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.
  cbn.
  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.
  cbn.
  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.
  cbn.
  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).
    cbn.
    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).
    cbn.
    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).
    cbn.
    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.
      cbn.
      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]]].
    cbn.
    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.