Library UniMath.Combinatorics.WellFoundedRelations

From Peter Lumsdaine, Aug 29, 2018:
Prompted by a question of Dan Grayson:
If you assume a relation is a well-order in the sense of having induction into families of propositions, does it then have induction into arbitrary type families?
Answer: yes. See the theorem below.
The result is also Proposition 1.4 of this article:
Intuitionistic Sets and Ordinals, by Paul Taylor The Journal of Symbolic Logic, Vol. 61, No. 3 (Sep., 1996), pp. 705-744

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Local Arguments funextsec {_ _ _ _} _.

Definition hereditary {X} (lt : X X Type) (P : X Type) : Type
  := x, ( y, lt y x P y) P x.

Definition strongly_well_founded {X} (lt : X X Type)
  := (P : X Type) (H : hereditary lt P),
      (f : x, P x), x, f x = H x (λ y _, f y).

Definition weakly_well_founded {X} (lt : X X Type)
  := P : X hProp, hereditary lt P x, P x.

Section Attempts.

  Context {X} (lt : X X Type).

  Notation "x < y" := (lt x y).

  Definition chain (n : nat) : (x y:X), Type.
    induction n as [|n H].
    - intros x y. exact (x = y).
    - intros x y. exact ( s t, H x s × s<t × t=y).

  Definition le (x y : X) : Type := n, chain n x y.

  Notation "x ≤ y" := (le x y) (at level 70).

  Definition nil {x} : xx := (0,,idpath x).

  Definition cons' {x x' y z} (p : z y) (l : y < x') (e : x' = x) : z x.
    induction p as [n c].
    exact (S n,,y,,x',,c,,l,,e).

  Definition cons1 {n y z z'} : (x : X) (e : z = z') (l : z' < y) (c : chain n y x), chain (S n) z x.
    induction n as [|n H].
    - intros x e l c. exact (z',,y,,e,,l,,c).
    - intros x e l c. induction c as [s [t [c' [l' e']]]].
      exact (s,,t,,H s e l c',,l',,e').

  Definition cons {x y z z'} (e : z = z') (l : z' < y) (p : y x) : z x.
    induction p as [n c]. (S n). exact (cons1 x e l c).

  Goal w w' x y z' z (e : w=w') (l : w'<x) (p : xy) (m : y<z') (f : z'=z),
    cons e l (cons' p m f) = cons' (cons e l p) m f.

  Context (P : X Type) (H : hereditary lt P).

  Definition guided_by x (f : y, y x P y) H
    := y pyx, f y pyx = H y (λ z l, f z (cons (idpath z) l pyx)).

  Definition attempt x := f, guided_by x f H.

  Definition attempt_fun {x} : attempt x ( y _, P y) := pr1.
  Coercion attempt_fun : attempt >-> Funclass.

  Definition attempt_comp {x} : (f : attempt x), _ := pr2.

  Definition disassemble_attempt {x} : attempt x ( y w, y<w w=x attempt y).
    intros f y' y l e. (λ t p, f t (cons' p l e)).
    intros z p. use attempt_comp.

  Definition assemble_attempt {x}
    : ( y y', y<y' y'=x attempt y) attempt x.
    intros fs. use tpair.
    - intros y [[|n] c].
      + apply H. intros z lzy. exact (fs z y lzy c z nil).
      + induction c as [s [t [c' [l' e']]]]. exact (fs s t l' e' y (n,,c')).
    - intros y [[|n] c].
      + reflexivity.
      + use attempt_comp.

  Definition attempt_lemma {x} (f g : attempt x)
             (T : ( y (pyx : y x), f y pyx = g y pyx) Type) :
    ( (e : attempt_fun f = attempt_fun g), T (λ y pyx, eqtohomot (eqtohomot e y) pyx))
     e, T e.
    intros HT e.
    simple refine (transportf _ _ (HT _)).
    { apply funextsec; intros y; apply funextsec; intros pyx.
      eapply pathscomp0.
      { refine (eqtohomot _ _). apply maponpaths.
        refine (eqtohomot _ _). apply toforallpaths_funextsec. }
      refine (eqtohomot _ _). apply toforallpaths_funextsec. }

  Definition attempt_paths {x} (f g : attempt x) :
       (e_fun : y pyx, f y pyx = g y pyx),
      ( y pyx,
          attempt_comp f y pyx
           @ maponpaths (H y) (funextsec (λ z, funextsec (λ lzy, e_fun z (cons (idpath z) lzy pyx))))
          = e_fun y pyx @ attempt_comp g y pyx)
     f = g.
    use attempt_lemma.
    intros e. induction f as [f0 f1], g as [g0 g1]. cbn in e. induction e.
    intros e_comp. apply maponpaths.
    apply funextsec; intros y; apply funextsec; intros pyx.
    refine (!_ @ e_comp _ _).
    refine (maponpaths _ _ @ pathscomp0rid _).
    refine (@maponpaths _ _ _ _ (idpath _) _).
    refine (maponpaths funextsec _ @ funextsec_toforallpaths _).
    apply funextsec; intros z.
    apply (funextsec_toforallpaths (idpath _)).

  Definition assemble_disassemble {x} (f : attempt x)
    : assemble_attempt (disassemble_attempt f) = f.
    use attempt_paths.
    - intros y [[|n] pyx].
      + apply pathsinv0. use attempt_comp.
      + reflexivity.
    - intros y [[|n] pyx].
      + cbn.
        refine (@maponpaths _ _ _ _ (idpath _) _ @ ! pathsinv0l _).
        refine (maponpaths _ _ @ funextsec_toforallpaths _).
        apply funextsec; intros z.
        apply (funextsec_toforallpaths (idpath _)).
      + refine (maponpaths _ _ @ pathscomp0rid _).
        refine (@maponpaths _ _ _ _ (idpath _) _).
        refine (maponpaths funextsec _ @ funextsec_toforallpaths _).
        apply funextsec; intros w.
        apply (funextsec_toforallpaths (idpath _)).

  Context (wwf_lt : weakly_well_founded lt).

  Definition iscontr_attempt : x, iscontr (attempt x).
    apply (wwf_lt (λ x, iscontr_hProp (attempt x))).
    intros x IH.
    apply (iscontrretract _ _ assemble_disassemble).
    apply impred_iscontr; intro z; apply impred_iscontr; intro z';
      apply impred_iscontr; intro l; apply impred_iscontr; intro e.
    induction e.
    exact (IH z l).

  Local Definition the_attempt x : attempt x
    := iscontrpr1 (iscontr_attempt x).

  Local Definition the_value x : P x
    := the_attempt x x nil.

  Local Definition the_comp x : the_value x = H x (λ y l, the_value y).
    assert (e : the_attempt x = assemble_attempt (λ y _ _ _, the_attempt y)).
    { apply pathsinv0, iscontr_uniqueness. }
    exact (eqtohomot (eqtohomot (maponpaths attempt_fun e) x) nil).

End Attempts.

Arguments le {_ _} _ _.

Theorem strongly_from_weakly_well_founded {X} {lt : X X Type}
  : weakly_well_founded lt strongly_well_founded lt.
  intros wwf_lt P H_P.
   (the_value lt P H_P wwf_lt).
  exact (the_comp lt P H_P wwf_lt).

Section OrderedSets.

  Context {X:UU} (lt : X X Type).

  Context (wwf_lt : weakly_well_founded lt).

  Notation "x < y" := (lt x y).

  Lemma irrefl z : ¬ (z < z).
This proof is provided by Marc Bezem.
We use the strong version of well foundedness, so we can avoid needing funextemptyAxiom to prove that ¬ (z=t) is a proposition.
    intro l.
    simple refine (pr1 (strongly_from_weakly_well_founded wwf_lt
                        (λ t, ¬ (z=t)) _) z (idpath z)).
    intros x h e. induction e.
    exact (h z l (idpath z)).

  Lemma notboth {r s} : (r<s) ¬ (s<r).
This proof is modeled after Marc's proof above.
    intros l m.
    simple refine (pr1 (strongly_from_weakly_well_founded wwf_lt
                        (λ t, ¬ ((r=t) ⨿ (s=t))) _) r (ii1 (idpath r))).
    intros x h c. induction c as [e|e].
    + induction e. exact (h s m (ii2 (idpath s))).
    + induction e. exact (h r l (ii1 (idpath r))).

  Lemma diagRecursion
        (f : nat nat Type)
        (init : n, f 0 n)
        (ind : m n, f m (S n) f (S m) n):
     m n, f m n.
    intros m.
    induction m as [|m H].
    - exact init.
    - intros n. apply ind. apply H.

  Lemma chaintrans {x y z m n} : chain lt m x y chain lt n y z chain lt (m+n) x z.
    revert m n y.
    apply (diagRecursion (λ m n, y, chain lt m x y chain lt n y z chain lt (m + n) x z)).
    - intros k y c. induction c. exact (idfun _).
    - intros r s p y c d.
      induction c as [u [t [b [k e]]]].
      change ((S r) + s) with (S (r+s)).
      rewrite plus_n_Sm.
      apply (p u b); clear p b x r.
      induction e.
      exact (cons1 lt z (idpath u) k d).

End OrderedSets.