Transfinite Induction, for the order ω^ω (realized as antilex-ordered (ordinary) lists of naturals)

omegaOmega.v

Require Import Arith.

Open Scope list_scope.

(** Print le
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
    
*)

Lemma strongHInduction (P : nat -> Type)
  (IH : forall k,
    (forall n, n < k -> P n) -> P k ) : (forall k, P k).
Proof.
  intro k.
  revert P IH.
  induction k.
  intros.
    apply IH.
    intros.
    contradict H.
    apply lt_n_0.
  intros.
  refine ( IHk (fun z => P (S z)) _).
  intros.
  apply IH.
  intros l ord.
  destruct l.
   apply IH.
    intros.
    contradict H.
    apply lt_n_0.
    apply X.
    apply lt_S_n.
    auto.
Defined.

Inductive antiLex : list nat -> list nat -> Prop :=
  | longer la lb : (length la > length lb) -> antiLex la lb
  | winner a b la lb : (length la = length lb) -> (a > b) -> antiLex (cons a la) (cons b lb)
  | heritable a la lb : (length la = length lb) -> (antiLex la lb) -> antiLex (cons a la) (cons a lb).

(**
  The antiLex ordering of list nat is a model of the well-order ω^ω (ordinal power)
  Can we prove that it is a well-order?
 *)

Lemma antiLex_nil_a (l : list nat) : ~ antiLex nil l.
Proof.
  intro.
  remember nil as NIL in H.
  destruct H.
  rewrite HeqNIL in H.
  contradict H.
  apply lt_n_0.
  contradict HeqNIL.
    discriminate.
  contradict HeqNIL.
    discriminate.
Defined.

Inductive fiber {A B : Type} (f : A -> B) : B -> Type
  := 
  img (a : A) : fiber f (f a).

Lemma src { A B : Type } { f : A -> B } { b : B } :
  fiber f b -> A.
Proof.
  intros [a].
  auto.
Defined.

Fixpoint snoc {A : Type} (l : list A) (a : A) : list A :=
  match l with
  | nil => (a :: nil)
  | cons b ll => (cons b (snoc ll a)) end.

Fixpoint rdc {A : Type} (x : list A) : list A :=
  match x with
  | nil => nil
  | (x :: z) => match z with 
    | nil => nil
    | _ => cons x (rdc z) end end.

Fixpoint last { A : Type } (x : list A) :
  ( (x = nil) + A )%type.
Proof.
  destruct x.
  left. auto.
  right.
  destruct (last _ x).
   exact a.
   exact a0.
Defined.

Fixpoint rac_rdc {A : Type} (x : list A) :
  (( x = nil ) + { l : list A & { a : A & x = snoc l a } } )%type.
Proof.
  destruct x.
  left.
  auto.
  right.
  destruct (rac_rdc _ x).
  exists nil.
  exists a.
  rewrite e. auto.
  destruct s.
  destruct s.
  exists (cons a x0).
  exists x1.
  rewrite e.
  auto.
Defined.

Lemma length_snoc {A : Type} (x : list A) (a : A) :
  length (snoc x a) = S (length x).
Proof.
  induction x.
  auto.
  simpl.
  f_equal.
  auto.
Defined.

Fixpoint rdc_snoc {A : Type} (x : list A) {struct x} :
   forall (a : A), rdc (snoc x a) = x.
Proof.
  destruct x.
    simpl. auto.
  intros.
  simpl.
  rewrite (rdc_snoc A x a0).
  destruct x; auto.
Defined.

Lemma antilex_snoc_n (la lb : list nat) (n : nat) :
  antiLex la lb -> antiLex (snoc la n) (snoc lb n).
Proof.
  intro.
  induction H.
  apply longer.
  rewrite length_snoc.
  rewrite length_snoc.
  apply le_n_S.
  auto.
  refine (winner _ _ _ _ _ H0).
  rewrite length_snoc. rewrite length_snoc.
  f_equal. auto.
  refine (heritable a _ _ _ _).
  rewrite length_snoc. rewrite length_snoc.
  f_equal. auto.
  auto.
Defined.

Lemma antiLex_length (la lb : list nat) :
  antiLex la lb -> (length la) >= (length lb).
Proof.
  intro.
  destruct H.
  apply lt_le_weak. auto.
  simpl.
  apply le_n_S.  rewrite H.
  auto.
  simpl. apply le_n_S. rewrite H. auto.
Defined.

Lemma antiLex_n_snoc (la lb : list nat) (a b : nat) :
  antiLex (snoc la a) (snoc lb b) ->
    (antiLex la lb) + ( (la = lb) * (a > b)).
Proof.
  intro.
  revert lb H.
  induction la.
  intros.
    destruct lb.
    simpl in *.
    right.
    split; try auto.
    remember (a :: nil) as a_nil.
    remember (b :: nil) as b_nil.
    destruct H.
      contradict H.
      rewrite Heqa_nil.
      rewrite Heqb_nil.
      simpl. apply lt_irrefl.
      injection Heqa_nil.
      injection Heqb_nil.
      intros.
      rewrite <- H2. rewrite <- H4.
      auto.
      contradict H0.
      injection Heqa_nil.
      intros.
      rewrite H0.
      apply antiLex_nil_a.
    contradict H.
    simpl.
    intro.
    assert (HL:= antiLex_length _ _ H).
    simpl in HL.
    rewrite length_snoc in HL.
    refine ( lt_n_0 _ (lt_S_n _ _ HL)).
  intros.
  destruct lb.
  left.
    apply longer. simpl. apply lt_0_Sn.
  simpl in H.
  remember ( a0 :: snoc la a ) as a0_la_a.
  remember ( n :: snoc lb b ) as n_lb_b.
  destruct H.
  left.
  apply longer.
    rewrite Heqn_lb_b in H.
    rewrite Heqa0_la_a in H.
    simpl in H.
    simpl.
    rewrite length_snoc in H.
    rewrite length_snoc in H.
    apply lt_S_n. auto.
  left.
  injection Heqn_lb_b.
  intros.
  rewrite H2 in H0.
  injection Heqa0_la_a.
  intros.
  rewrite H4 in H0.
  rewrite H1 in H.
  rewrite H3 in H. rewrite length_snoc in H.
    rewrite length_snoc in H.
  injection H.
  intros.
  refine (winner _ _ _ _ H5 _).
  auto.
  injection Heqa0_la_a.
  intros.
  destruct H2.
  injection Heqn_lb_b.
  intros.
  destruct H3.
  rewrite H1 in H0.
  rewrite H2 in H0.
  destruct ( IHla _ H0 ).
    left.
    apply heritable.
    rewrite H1 in H.
    rewrite H2 in H.
    repeat progress (rewrite length_snoc in H).
    injection H. auto.
    auto.
  right.
  split.
  f_equal. apply p.
  apply p.
Defined.

(** The following proof looks awfully repetetive (we prove P nil
  several times, per e.g.); 
  this is more to do with the need to collect sufficient extra
  hypotheses than intrinsic redundancy.
*)

Lemma antiLex_induction
  (P : list nat -> Type)
  (IH : forall la , ( forall lb, antiLex la lb -> P lb ) -> P la)
  : forall la, P la.
Proof.
  intro.
  change (P (src (img (@length nat) la))).
  generalize (img (@length _) la).
  generalize (length la).
  intro.
  revert n P IH. clear.
  refine (strongHInduction _ _).
  intros.
  destruct f. simpl in *.
  apply IH.
  intros.
  destruct (rac_rdc a).
  rewrite e in H.
    contradict H.
    apply antiLex_nil_a.
  destruct s as [ ll [ b eqn]] .
  rewrite eqn in *.
  clear eqn.
  destruct (rac_rdc lb).
  rewrite e.
  apply IH. intros.
    contradict H0.
    apply antiLex_nil_a.
  destruct s as [ ly [ c eqn ]].
  rewrite eqn in *.
  clear eqn.
  assert (W := fun lz ord => ( X _ ord P IH (img _ lz))).  
  simpl in W.  
  destruct (antiLex_n_snoc _ _ _ _ H).
    clear H.
    revert c.
    rewrite length_snoc in X.
  refine ( X _ (le_lt_n_Sm _ _ (antiLex_length ll ly a0)) (fun lz => forall c, P (snoc lz c))
   _ (img _ ly)
  ).
  intros la Hx.
  refine (strongHInduction _ _).
  intros.
  apply IH.
  intros.
  destruct (rac_rdc lb0).
    rewrite e. apply IH.
    intros.
    contradict H0.
    apply antiLex_nil_a.
   destruct s.
   destruct s.
   rewrite e in *. clear e.
   destruct (antiLex_n_snoc _ _ _ _ H).
   apply Hx.
   auto.
   destruct p.
   rewrite <- e.
   apply X0. auto.
  destruct p.
  rewrite e in *.
  clear e.
  rewrite length_snoc in X.
  refine ( X _ (le_n _) (fun lz => forall c, P (snoc lz c)) _ (img _ ly) _).
  intros.
  revert c0.
  refine (strongHInduction _ _).
  intros.
  apply IH.
  intros.
  destruct (rac_rdc lb0).
  rewrite e. apply IH.
    intros.
    contradict H1.
    apply antiLex_nil_a.
  destruct s.
  destruct s.
  rewrite e in *.
  clear e.
  destruct (antiLex_n_snoc _ _ _ _ H0).
  apply X0. auto.
  destruct p.
  rewrite e in *.
  clear e.
  apply X1.
  auto.
Defined.