# 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.
Intuitionistic Sets and Ordinals, by Paul Taylor The Journal of Symbolic Logic, Vol. 61, No. 3 (Sep., 1996), pp. 705-744 https://www.jstor.org/stable/pdf/2275781.pdf

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.
Proof.
induction n as [|n H].
- intros x y. exact (x = y).
- intros x y. exact ( s t, H x s × s<t × t=y).
Defined.

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.
Proof.
induction p as [n c].
exact (S n,,y,,x',,c,,l,,e).
Defined.

Definition cons1 {n y z z'} : (x : X) (e : z = z') (l : z' < y) (c : chain n y x), chain (S n) z x.
Proof.
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').
Defined.

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

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.
Proof.
reflexivity.
Defined.

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).
Proof.
intros f y' y l e. (λ t p, f t (cons' p l e)).
intros z p. use attempt_comp.
Defined.

Definition assemble_attempt {x}
: ( y y', y<y' y'=x attempt y) attempt x.
Proof.
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.
Defined.

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.
Proof.
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. }
Defined.

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.
Proof.
use attempt_lemma.
intros e. induction f as [f0 f1], g as [g0 g1]. cbn in e. induction e.
cbn.
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 _)).
Defined.

Definition assemble_disassemble {x} (f : attempt x)
: assemble_attempt (disassemble_attempt f) = f.
Proof.
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 _)).
Defined.

Context (wwf_lt : weakly_well_founded lt).

Definition iscontr_attempt : x, iscontr (attempt x).
Proof.
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).
Defined.

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).
Proof.
assert (e : the_attempt x = assemble_attempt (λ y _ _ _, the_attempt y)).
{ apply pathsinv0, iscontr_uniqueness. }
exact (eqtohomot (eqtohomot (maponpaths attempt_fun e) x) nil).
Defined.

End Attempts.

Arguments le {_ _} _ _.

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

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).
Proof.
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)).
Defined.

Lemma notboth {r s} : (r<s) ¬ (s<r).
Proof.
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))).
Defined.

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.
Proof.
intros m.
induction m as [|m H].
- exact init.
- intros n. apply ind. apply H.
Defined.

Lemma chaintrans {x y z m n} : chain lt m x y chain lt n y z chain lt (m+n) x z.
Proof.
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).
Defined.

End OrderedSets.