(** * Bar induction *)

Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core.
Require Import Spaces.Nat.Core.
Require Import Spaces.NatSeq.Core.
Require Import Spaces.List.Core Spaces.List.Theory.
Require Import BoundedSearch.

Local Open Scope nat_scope.
Local Open Scope type_scope.
Local Open Scope list_scope.

(** ** The basic definitions *)

(** A family [B] on a type of lists is a bar if every infinite sequence restricts to a finite sequence satisfying [B]. *)
Definition IsBar {A : Type} (B : list A -> Type)
  := forall (s : nat -> A), {n : nat & B (list_restrict s n)}.

(** A family [B] is a uniform bar if it is a bar such that there is an upper bound for the lengths of the restrictions needed to satisfy the bar condition. *)
Definition IsUniformBar {A : Type} (B : list A -> Type)
  := {M : nat & forall (s : nat -> A),
                  {n : nat & (n <= M) * B (list_restrict s n)}}.

(** A family [B] on a type of finite sequences is inductive if, for every list [l], if the concatenation of [l] with any term satisfies [B], then the list satisfies [B]. *)
Definition IsInductive {A : Type} (B : list A -> Type)
  := forall (l : list A), (forall (a : A), B (l ++ [a])) -> B l.

(** A family [B] on a type of finite sequences is monotone if for every list satisfying [B], the concatenation with any other list still satisfies [B]. Equivalently, we can just check the concatenations with lists of length one. *)
Definition IsMonotone {A : Type} (B : list A -> Type)
  := forall (l1 l2 : list A), B l1 -> B (l1 ++ l2).

Definition IsMonotoneSingleton {A : Type} (B : list A -> Type)
  := forall (l : list A) (a : A), B l -> B (l ++ [a]).

Definition ismonotone_ismonotonesingleton {A : Type} (B : list A -> Type)
  (mon : IsMonotoneSingleton B)
  : IsMonotone B.
A: Type
B: list A -> Type
mon: IsMonotoneSingleton B
IsMonotone B
Proof.
A: Type
B: list A -> Type
mon: IsMonotoneSingleton B
IsMonotone B
  intros l1 l2; induction l2 as [|a l2 IHl2] in l1 |- *.
A: Type
B: list A -> Type
mon: IsMonotoneSingleton B
l1: list A
B l1 -> B (l1 ++ nil)
A: Type
B: list A -> Type
mon: IsMonotoneSingleton B
l1: list A
a: A
l2: list A
IHl2: forall l1 : list A, B l1 -> B (l1 ++ l2)
B l1 -> B (l1 ++ a :: l2)
  -
A: Type
B: list A -> Type
mon: IsMonotoneSingleton B
l1: list A
B l1 -> B (l1 ++ nil) by rewrite app_nil.
  -
A: Type
B: list A -> Type
mon: IsMonotoneSingleton B
l1: list A
a: A
l2: list A
IHl2: forall l1 : list A, B l1 -> B (l1 ++ l2)
B l1 -> B (l1 ++ a :: l2) intro h.
A: Type
B: list A -> Type
mon: IsMonotoneSingleton B
l1: list A
a: A
l2: list A
IHl2: forall l1 : list A, B l1 -> B (l1 ++ l2)
h: B l1
B (l1 ++ a :: l2)
    rewrite (app_assoc l1 [a] l2).
A: Type
B: list A -> Type
mon: IsMonotoneSingleton B
l1: list A
a: A
l2: list A
IHl2: forall l1 : list A, B l1 -> B (l1 ++ l2)
h: B l1
B ((l1 ++ [a]) ++ l2)
    apply IHl2, mon, h.
Defined.

(** We state three forms of bar induction: (full) bar induction, monotone bar induction and decidable bar induction. *)

Definition DecidableBarInduction (A : Type) :=
  forall (B : list A -> Type)
  (dec : forall (l : list A), Decidable (B l))
  (ind : IsInductive B)
  (bar : IsBar B),
  B nil.

Definition MonotoneBarInduction (A : Type) :=
  forall (B : list A -> Type)
  (mon : IsMonotone B)
  (ind : IsInductive B)
  (bar : IsBar B),
  B nil.

Definition BarInduction (A : Type) :=
  forall (B : list A -> Type)
  (ind : IsInductive B)
  (bar : IsBar B),
  B nil.

(** The three bar induction principles can be more generally stated for two families. It's clear that the two-family versions imply the one-family versions. We show the reverse implications for full bar induction and monotone bar induction. We do not know if the definitions are equivalent in the decidable case yet. *)

Definition DecidableBarInduction' (A : Type) :=
  forall (B C : list A -> Type)
  (sub : forall l : list A, C l -> B l)
  (dC : forall (l : list A), Decidable (C l))
  (ind : IsInductive B)
  (bar : IsBar C),
  B nil.

Definition MonotoneBarInduction' (A : Type) :=
  forall (B C : list A -> Type)
  (sub : forall l : list A, C l -> B l)
  (monC : IsMonotone C)
  (indB : IsInductive B)
  (barC : IsBar C),
  B nil.

Definition BarInduction' (A : Type) :=
  forall (B C : list A -> Type)
  (sub : forall l : list A, C l -> B l)
  (indB : IsInductive B)
  (barC : IsBar C),
  B nil.

Definition barinduction'_barinduction (A : Type) (BI : BarInduction A)
  : BarInduction' A
  := fun B C sub indB barC => BI B indB (fun s => ((barC s).1; sub _ (barC s).2)).

Definition monotonebarinduction'_monotonebarinduction (A : Type)
  (MBI : MonotoneBarInduction A)
  : MonotoneBarInduction' A.
A: Type
MBI: MonotoneBarInduction A
MonotoneBarInduction' A
Proof.
A: Type
MBI: MonotoneBarInduction A
MonotoneBarInduction' A
  intros B C sub monC indB barC.
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
B nil
  pose (P := fun v => forall w, B (v ++ w)).
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
B nil
  apply (MBI P).
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
IsMonotone P
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
IsInductive P
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
IsBar P
  -
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
IsMonotone P intros u v H w.
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
u, v: list A
H: P u
w: list A
B ((u ++ v) ++ w)
    by rewrite <- app_assoc.
  -
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
IsInductive P intros l1 H [|a l2].
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
l1: list A
H: forall a : A, P (l1 ++ [a])
B (l1 ++ nil)
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
l1: list A
H: forall a : A, P (l1 ++ [a])
a: A
l2: list A
B (l1 ++ a :: l2)
    +
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
l1: list A
H: forall a : A, P (l1 ++ [a])
B (l1 ++ nil) apply indB.
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
l1: list A
H: forall a : A, P (l1 ++ [a])
forall a : A, B ((l1 ++ nil) ++ [a])
      intro a.
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
l1: list A
H: forall a : A, P (l1 ++ [a])
a: A
B ((l1 ++ nil) ++ [a])
      specialize (H a nil).
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
l1: list A
a: A
H: B ((l1 ++ [a]) ++ nil)
B ((l1 ++ nil) ++ [a])
      by rewrite app_nil in *.
    +
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
l1: list A
H: forall a : A, P (l1 ++ [a])
a: A
l2: list A
B (l1 ++ a :: l2) specialize (H a l2).
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
l1: list A
a: A
l2: list A
H: B ((l1 ++ [a]) ++ l2)
B (l1 ++ a :: l2)
      by rewrite <- app_assoc in H.
  -
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
IsBar P intro s.
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
s: nat -> A
{n : nat & P (list_restrict s n)}
    exists (barC s).1.
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
s: nat -> A
P (list_restrict s (barC s).1)
    intro w.
A: Type
MBI: MonotoneBarInduction A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
monC: IsMonotone C
indB: IsInductive B
barC: IsBar C
P:= fun v : list A => forall w : list A, B (v ++ w): list A -> Type
s: nat -> A
w: list A
B (list_restrict s (barC s).1 ++ w)
    apply sub, monC, barC.
Defined.

(** Since decidable bar induction uses decidable predicates, we can state a logically equivalent form based on families of decidable propositions. This form has the advantage of being a proposition. *)

Definition HPropDecidableBarInduction (A : Type) :=
  forall (B : list A -> Type)
  (prop : forall (l : list A), IsHProp (B l))
  (dec : forall (l : list A), Decidable (B l))
  (ind : IsInductive B)
  (bar : IsBar B),
  B nil.

Definition ishprop_hpropdecidablebarinduction `{Funext} (A : Type)
  : IsHProp (HPropDecidableBarInduction A)
  := _.

Definition decidablebarinduction_hpropdecidablebarinduction (A : Type)
  (pDBI : HPropDecidableBarInduction A)
  : DecidableBarInduction A.
A: Type
pDBI: HPropDecidableBarInduction A
DecidableBarInduction A
Proof.
A: Type
pDBI: HPropDecidableBarInduction A
DecidableBarInduction A
  intros P dP iP bP.
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
P nil
  apply merely_inhabited_iff_inhabited_stable.
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
Tr (-1) (P nil)
  rapply (pDBI (Tr (-1) o P)).
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
IsInductive (fun x : list A => Tr (-1) (P x))
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
IsBar (fun x : list A => Tr (-1) (P x))
  -
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
IsInductive (fun x : list A => Tr (-1) (P x)) intros l q.
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
l: list A
q: forall a : A, Tr (-1) (P (l ++ [a]))
Tr (-1) (P l)
    refine (tr (iP _ _)).
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
l: list A
q: forall a : A, Tr (-1) (P (l ++ [a]))
forall a : A, P (l ++ [a])
    intro a; apply merely_inhabited_iff_inhabited_stable, (q a).
  -
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
IsBar (fun x : list A => Tr (-1) (P x)) intros s.
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
s: nat -> A
{n : nat & Tr (-1) (P (list_restrict s n))}
    exists (bP s).1.
A: Type
pDBI: HPropDecidableBarInduction A
P: list A -> Type
dP: forall l : list A, Decidable (P l)
iP: IsInductive P
bP: IsBar P
s: nat -> A
Tr (-1) (P (list_restrict s (bP s).1))
    exact (tr (bP s).2).
Defined.

(** ** Relations between the three forms of bar induction *)

(** Full bar induction clearly implies the other two. We now show that monotone bar induction implies decidable bar induction, by passing through the two-family versions. *)

Definition decidablebarinduction'_monotone_bar_induction' (A : Type)
  (MBI : MonotoneBarInduction' A)
  : DecidableBarInduction' A.
A: Type
MBI: MonotoneBarInduction' A
DecidableBarInduction' A
Proof.
A: Type
MBI: MonotoneBarInduction' A
DecidableBarInduction' A
  intros B C sub dC indB barC.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
B nil
  (* The [n <= length l] part is redundant, but makes it clear that [P l] is decidable, which is used below. *)
  pose (P l := {n : nat & (n <= length l) * C (take n l)}).
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
B nil
  pose (Q l := B l + P l).
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
B nil
  (* First we show that it is enough to prove [Q nil] (two cases), and then we prove [Q nil]. *)
  enough (Q nil) as [b0 | [n [hn hc]]].
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
b0: B nil
B nil
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
n: nat
hn: n <= length nil
hc: C (take n nil)
B nil
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
Q nil
  1: exact b0.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
n: nat
hn: n <= length nil
hc: C (take n nil)
B nil
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
Q nil
  1: exact (sub _ (take_nil _ # hc)).
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
Q nil
  apply (MBI Q P (fun l pl => inr pl)).
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
IsMonotone P
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
IsInductive Q
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
IsBar P
  -
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
IsMonotone P intros l1 l2 [n (cn1, cn2)].
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l1, l2: list A
n: nat
cn1: n <= length l1
cn2: C (take n l1)
P (l1 ++ l2)
    exists n; split.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l1, l2: list A
n: nat
cn1: n <= length l1
cn2: C (take n l1)
n <= length (l1 ++ l2)
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l1, l2: list A
n: nat
cn1: n <= length l1
cn2: C (take n l1)
C (take n (l1 ++ l2))
    +
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l1, l2: list A
n: nat
cn1: n <= length l1
cn2: C (take n l1)
n <= length (l1 ++ l2) rewrite length_app; exact _.
    +
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l1, l2: list A
n: nat
cn1: n <= length l1
cn2: C (take n l1)
C (take n (l1 ++ l2)) exact (take_app l1 l2 cn1 # cn2).
  -
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
IsInductive Q intros l hl.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
Q l
    assert (dP : Decidable (P l)) by rapply decidable_search.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
dP: Decidable (P l)
Q l
    destruct dP as [t|f].
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
t: P l
Q l
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
Q l
    1: exact (inr t).
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
Q l
    left.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
B l apply indB.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
forall a : A, B (l ++ [a])
    intro a; destruct (hl a) as [b | [n [hn hc]]].
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
b: B (l ++ [a])
B (l ++ [a])
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hn: n <= length (l ++ [a])
hc: C (take n (l ++ [a]))
B (l ++ [a])
    1: exact b.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hn: n <= length (l ++ [a])
hc: C (take n (l ++ [a]))
B (l ++ [a])
    destruct (equiv_leq_lt_or_eq hn) as [hn1 | hn2]; clear hn.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
B (l ++ [a])
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn2: n = length (l ++ [a])
B (l ++ [a])
    +
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
B (l ++ [a]) contradiction f.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
P l
      assert (hln : n <= length l).
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
n <= length l
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
hln: n <= length l
P l
      {
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
n <= length l rewrite length_app, nat_add_comm in hn1.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length [a] + length l
n <= length l cbn in hn1; unfold "<" in hn1.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n.+1 <= (length l).+1
n <= length l
        exact (leq_pred' hn1). }
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
hln: n <= length l
P l
      exists n; constructor.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
hln: n <= length l
n <= length l
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
hln: n <= length l
C (take n l)
      *
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
hln: n <= length l
n <= length l exact hln.
      *
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn1: n < length (l ++ [a])
hln: n <= length l
C (take n l) exact ((take_app l [a] hln)^ # hc).
    +
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn2: n = length (l ++ [a])
B (l ++ [a]) refine (sub _ ((take_length_leq _ _ _) # hc)).
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
l: list A
hl: forall a : A, Q (l ++ [a])
f: ~ P l
a: A
n: nat
hc: C (take n (l ++ [a]))
hn2: n = length (l ++ [a])
length (l ++ [a]) <= n
      by destruct hn2^.
  -
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
IsBar P intro s.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
{n : nat & P (list_restrict s n)}
    pose (n := (barC s).1).
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
{n : nat & P (list_restrict s n)}
    exists n; exists n.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
(n <= length (list_restrict s n)) *
C (take n (list_restrict s n))
    split.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
n <= length (list_restrict s n)
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
C (take n (list_restrict s n))
    +
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
n <= length (list_restrict s n) by rewrite length_list_restrict.
    +
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
C (take n (list_restrict s n)) rewrite take_length_leq.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
C (list_restrict s n)
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
length (list_restrict s n) <= n
      1: exact (barC s).2.
A: Type
MBI: MonotoneBarInduction' A
B, C: list A -> Type
sub: forall l : list A, C l -> B l
dC: forall l : list A, Decidable (C l)
indB: IsInductive B
barC: IsBar C
P:= fun l : list A =>
{n : nat & (n <= length l) * C (take n l)}: list A -> Type
Q:= fun l : list A => B l + P l: list A -> Type
s: nat -> A
n:= (barC s).1: nat
length (list_restrict s n) <= n
      by rewrite length_list_restrict.
Defined.

Definition decidable_bar_induction_monotone_bar_induction (A : Type)
  (MBI : MonotoneBarInduction A)
  : DecidableBarInduction A
  := fun B dec ind bar =>
      (decidablebarinduction'_monotone_bar_induction' A
        (monotonebarinduction'_monotonebarinduction A MBI))
      B B (fun _ => idmap) dec ind bar.

(** ** Examples of types that satisfy forms of bar induction *)

(** The empty type and all contractible types satisfy full bar induction. *)

Definition barinduction_empty : BarInduction Empty.
BarInduction Empty
Proof.
BarInduction Empty
  intros B iB _.
B: list Empty -> Type
iB: IsInductive B
B nil
  rapply iB.
B: list Empty -> Type
iB: IsInductive B
forall a : Empty, B (nil ++ [a])
  intro a; contradiction a.
Defined.

Definition barinduction_contr (A : Type) `{Contr A} : BarInduction A.
A: Type
Contr0: Contr A
BarInduction A
Proof.
A: Type
Contr0: Contr A
BarInduction A
  intros B iB bB.
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
bB: IsBar B
B nil
  pose (c := fun (n : nat) => center A).
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
bB: IsBar B
c:= fun _ : nat => center A: nat -> A
B nil
  specialize (bB c) as [n hn]; induction n.
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
c:= fun _ : nat => center A: nat -> A
hn: B (list_restrict c 0)
B nil
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
c:= fun _ : nat => center A: nat -> A
n: nat
hn: B (list_restrict c n.+1)
IHn: B (list_restrict c n) -> B nil
B nil
  1: exact hn.
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
c:= fun _ : nat => center A: nat -> A
n: nat
hn: B (list_restrict c n.+1)
IHn: B (list_restrict c n) -> B nil
B nil
  apply IHn, iB.
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
c:= fun _ : nat => center A: nat -> A
n: nat
hn: B (list_restrict c n.+1)
IHn: B (list_restrict c n) -> B nil
forall a : A, B (list_restrict c n ++ [a])
  intro x.
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
c:= fun _ : nat => center A: nat -> A
n: nat
hn: B (list_restrict c n.+1)
IHn: B (list_restrict c n) -> B nil
x: A
B (list_restrict c n ++ [x])
  nrefine (_ # hn).
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
c:= fun _ : nat => center A: nat -> A
n: nat
hn: B (list_restrict c n.+1)
IHn: B (list_restrict c n) -> B nil
x: A
list_restrict c n.+1 = list_restrict c n ++ [x]
  rewrite (path_contr x (center A)).
A: Type
Contr0: Contr A
B: list A -> Type
iB: IsInductive B
c:= fun _ : nat => center A: nat -> A
n: nat
hn: B (list_restrict c n.+1)
IHn: B (list_restrict c n) -> B nil
x: A
list_restrict c n.+1 = list_restrict c n ++ [center A]
  napply list_restrict_succ.
Defined.

(** If a type satisfies decidable bar induction assuming that it is pointed, then it satisfies decidable bar induction. *)
Definition decidablebarinduction_pointed_decidablebarinduction
  (A : Type) (p : A -> DecidableBarInduction A)
  : DecidableBarInduction A.
A: Type
p: A -> DecidableBarInduction A
DecidableBarInduction A
Proof.
A: Type
p: A -> DecidableBarInduction A
DecidableBarInduction A
  intros B dB iB bB.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
B nil
  destruct (dec (B nil)) as [b | n].
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
b: B nil
B nil
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
B nil
  1: exact b.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
B nil
  apply iB.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
forall a : A, B (nil ++ [a])
  intro a; cbn.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B [a]
  pose (B' l := B (a :: l)).
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
B [a]
  apply (p a B' _).
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
IsInductive B'
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
IsBar B'
  -
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
IsInductive B' intros l; unfold B'.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
l: list A
(forall a0 : A, B (a :: l ++ [a0])) -> B (a :: l)
    exact (iB (a :: l)).
  -
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
IsBar B' intro s; unfold B'.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
{n : nat & B (a :: list_restrict s n)}
    destruct (bB (seq_cons a s)) as [m r].
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m)
{n : nat & B (a :: list_restrict s n)}
    destruct m.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
r: B (list_restrict (seq_cons a s) 0)
{n : nat & B (a :: list_restrict s n)}
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
{n : nat & B (a :: list_restrict s n)}
    +
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
r: B (list_restrict (seq_cons a s) 0)
{n : nat & B (a :: list_restrict s n)} contradiction (n r).
    +
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
{n : nat & B (a :: list_restrict s n)} exists m.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
B (a :: list_restrict s m)
      nrefine (_ # r).
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
list_restrict (seq_cons a s) m.+1 =
a :: list_restrict s m
      snapply path_list_nth'.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
length (list_restrict (seq_cons a s) m.+1) =
length (a :: list_restrict s m)
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
forall (n0 : nat)
(H : n0 < length (list_restrict (seq_cons a s) m.+1)),
nth' (list_restrict (seq_cons a s) m.+1) n0 H =
nth' (a :: list_restrict s m) n0
  (transport (lt n0) ?p H)
      1: cbn; by rewrite !length_list_restrict.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
forall (n : nat)
(H : n < length (list_restrict (seq_cons a s) m.+1)),
nth' (list_restrict (seq_cons a s) m.+1) n H =
nth' (a :: list_restrict s m) n
  (transport (lt n)
     (internal_paths_rew_r
        (fun n0 : nat =>
         length
           (list_map
              (fun pat : {i : nat & i < m.+1} =>
               seq_cons a s pat.1)
              (reverse_acc [(m; leq_refl m.+1)]
                 (list_map
                    (functor_sigma idmap
                       (fun (k : nat) (H0 : k < m) =>
                        leq_succ_r H0))
                    (nat_rec
                       (fun n1 : nat =>
                        list {k : nat & k < n1}) nil
                       (fun (n1 : nat)
                          (IHn : list
                                   {k : nat & k < n1})
                        =>
                        (n1; leq_refl n1.+1)
                        :: list_map
                             (functor_sigma idmap
                                (...)) IHn) m)))) =
         n0.+1)
        (internal_paths_rew_r
           (fun n0 : nat => n0 = m.+1) 1
           (length_list_restrict (seq_cons a s) m.+1))
        (length_list_restrict s m)
      :
      length (list_restrict (seq_cons a s) m.+1) =
      length (a :: list_restrict s m)) H)
      intros k hk; destruct k.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
hk: 0 < length (list_restrict (seq_cons a s) m.+1)
nth' (list_restrict (seq_cons a s) m.+1) 0 hk =
nth' (a :: list_restrict s m) 0
  (transport (lt 0)
     (internal_paths_rew_r
        (fun n : nat =>
         length
           (list_map
              (fun pat : {i : nat & i < m.+1} =>
               seq_cons a s pat.1)
              (reverse_acc [(m; leq_refl m.+1)]
                 (list_map
                    (functor_sigma idmap
                       (fun (k : nat) (H : k < m) =>
                        leq_succ_r H))
                    (nat_rec
                       (fun n0 : nat =>
                        list {k : nat & k < n0}) nil
                       (fun (n0 : nat)
                          (IHn : list
                                   {k : nat & k < n0})
                        =>
                        (n0; leq_refl n0.+1)
                        :: list_map
                             (functor_sigma idmap
                                (fun ... ... =>
                                 leq_succ_r H)) IHn) m)))) =
         n.+1)
        (internal_paths_rew_r
           (fun n : nat => n = m.+1) 1
           (length_list_restrict (seq_cons a s) m.+1))
        (length_list_restrict s m)) hk)
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
k: nat
hk: k.+1 < length (list_restrict (seq_cons a s) m.+1)
nth' (list_restrict (seq_cons a s) m.+1) k.+1 hk =
nth' (a :: list_restrict s m) k.+1
  (transport (lt k.+1)
     (internal_paths_rew_r
        (fun n : nat =>
         length
           (list_map
              (fun pat : {i : nat & i < m.+1} =>
               seq_cons a s pat.1)
              (reverse_acc [(m; leq_refl m.+1)]
                 (list_map
                    (functor_sigma idmap
                       (fun (k : nat) (H : k < m) =>
                        leq_succ_r H))
                    (nat_rec
                       (fun n0 : nat =>
                        list {k : nat & k < n0}) nil
                       (fun (n0 : nat)
                          (IHn : list
                                   {k : nat & k < n0})
                        =>
                        (n0; leq_refl n0.+1)
                        :: list_map
                             (functor_sigma idmap
                                (fun ... ... =>
                                 leq_succ_r H)) IHn) m)))) =
         n.+1)
        (internal_paths_rew_r
           (fun n : nat => n = m.+1) 1
           (length_list_restrict (seq_cons a s) m.+1))
        (length_list_restrict s m)) hk)
      1: cbn; by rewrite nth'_list_restrict.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
k: nat
hk: k.+1 < length (list_restrict (seq_cons a s) m.+1)
nth' (list_restrict (seq_cons a s) m.+1) k.+1 hk =
nth' (a :: list_restrict s m) k.+1
  (transport (lt k.+1)
     (internal_paths_rew_r
        (fun n : nat =>
         length
           (list_map
              (fun pat : {i : nat & i < m.+1} =>
               seq_cons a s pat.1)
              (reverse_acc [(m; leq_refl m.+1)]
                 (list_map
                    (functor_sigma idmap
                       (fun (k : nat) (H : k < m) =>
                        leq_succ_r H))
                    (nat_rec
                       (fun n0 : nat =>
                        list {k : nat & k < n0}) nil
                       (fun (n0 : nat)
                          (IHn : list
                                   {k : nat & k < n0})
                        =>
                        (n0; leq_refl n0.+1)
                        :: list_map
                             (functor_sigma idmap
                                (fun ... ... =>
                                 leq_succ_r H)) IHn) m)))) =
         n.+1)
        (internal_paths_rew_r
           (fun n : nat => n = m.+1) 1
           (length_list_restrict (seq_cons a s) m.+1))
        (length_list_restrict s m)) hk)
      assert (hk' : k < length (list_restrict s m)).
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
k: nat
hk: k.+1 < length (list_restrict (seq_cons a s) m.+1)
k < length (list_restrict s m)
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
k: nat
hk: k.+1 < length (list_restrict (seq_cons a s) m.+1)
hk': k < length (list_restrict s m)
nth' (list_restrict (seq_cons a s) m.+1) k.+1 hk =
nth' (a :: list_restrict s m) k.+1
  (transport (lt k.+1)
     (internal_paths_rew_r
        (fun n : nat =>
         length
           (list_map
              (fun pat : {i : nat & i < m.+1} =>
               seq_cons a s pat.1)
              (reverse_acc [(m; leq_refl m.+1)]
                 (list_map
                    (functor_sigma idmap
                       (fun (k : nat) (H : k < m) =>
                        leq_succ_r H))
                    (nat_rec
                       (fun n0 : nat =>
                        list {k : nat & k < n0}) nil
                       (fun (n0 : nat)
                          (IHn : list
                                   {k : nat & k < n0})
                        =>
                        (n0; leq_refl n0.+1)
                        :: list_map
                             (functor_sigma idmap
                                (fun ... ... =>
                                 leq_succ_r H)) IHn) m)))) =
         n.+1)
        (internal_paths_rew_r
           (fun n : nat => n = m.+1) 1
           (length_list_restrict (seq_cons a s) m.+1))
        (length_list_restrict s m)) hk)
      {
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
k: nat
hk: k.+1 < length (list_restrict (seq_cons a s) m.+1)
k < length (list_restrict s m) rewrite length_list_restrict in *.
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
k: nat
hk: k.+1 < m.+1
k < m
        exact _. }
A: Type
p: A -> DecidableBarInduction A
B: list A -> Type
dB: forall l : list A, Decidable (B l)
iB: IsInductive B
bB: IsBar B
n: ~ B nil
a: A
B':= fun l : list A => B (a :: l): list A -> Type
s: nat -> A
m: nat
r: B (list_restrict (seq_cons a s) m.+1)
k: nat
hk: k.+1 < length (list_restrict (seq_cons a s) m.+1)
hk': k < length (list_restrict s m)
nth' (list_restrict (seq_cons a s) m.+1) k.+1 hk =
nth' (a :: list_restrict s m) k.+1
  (transport (lt k.+1)
     (internal_paths_rew_r
        (fun n : nat =>
         length
           (list_map
              (fun pat : {i : nat & i < m.+1} =>
               seq_cons a s pat.1)
              (reverse_acc [(m; leq_refl m.+1)]
                 (list_map
                    (functor_sigma idmap
                       (fun (k : nat) (H : k < m) =>
                        leq_succ_r H))
                    (nat_rec
                       (fun n0 : nat =>
                        list {k : nat & k < n0}) nil
                       (fun (n0 : nat)
                          (IHn : list
                                   {k : nat & k < n0})
                        =>
                        (n0; leq_refl n0.+1)
                        :: list_map
                             (functor_sigma idmap
                                (fun ... ... =>
                                 leq_succ_r H)) IHn) m)))) =
         n.+1)
        (internal_paths_rew_r
           (fun n : nat => n = m.+1) 1
           (length_list_restrict (seq_cons a s) m.+1))
        (length_list_restrict s m)) hk)
      by rewrite (nth'_cons _ _ _ hk'), !nth'_list_restrict.
Defined.

(** The same is true for monotone bar induction. *)
Definition monotonebarinduction_pointed_monotonebarinduction
  (A : Type) (p : A -> MonotoneBarInduction A)
  : MonotoneBarInduction A.
A: Type
p: A -> MonotoneBarInduction A
MonotoneBarInduction A
Proof.
A: Type
p: A -> MonotoneBarInduction A
MonotoneBarInduction A
  intros B mB iB bB.
A: Type
p: A -> MonotoneBarInduction A
B: list A -> Type
mB: IsMonotone B
iB: IsInductive B
bB: IsBar B
B nil
  apply iB.
A: Type
p: A -> MonotoneBarInduction A
B: list A -> Type
mB: IsMonotone B
iB: IsInductive B
bB: IsBar B
forall a : A, B (nil ++ [a])
  intro a; cbn.
A: Type
p: A -> MonotoneBarInduction A
B: list A -> Type
mB: IsMonotone B
iB: IsInductive B
bB: IsBar B
a: A
B [a]
  by apply (mB nil), (p a).
Defined.

(** Combining [monotonebarinduction_pointed_monotonebarinduction] and [barinduction_contr], we prove that any proposition satisfies monotone bar induction. *)
Definition monotonebarinduction_hprop (A : Type) `{IsHProp A}
  : MonotoneBarInduction A.
A: Type
IsHProp0: IsHProp A
MonotoneBarInduction A
Proof.
A: Type
IsHProp0: IsHProp A
MonotoneBarInduction A
  apply monotonebarinduction_pointed_monotonebarinduction.
A: Type
IsHProp0: IsHProp A
A -> MonotoneBarInduction A
  intro a.
A: Type
IsHProp0: IsHProp A
a: A
MonotoneBarInduction A
  enough (BarInduction A) as BI.
A: Type
IsHProp0: IsHProp A
a: A
BI: BarInduction A
MonotoneBarInduction A
A: Type
IsHProp0: IsHProp A
a: A
BarInduction A
  1: exact (fun B _ iB bB => BI B iB bB).
A: Type
IsHProp0: IsHProp A
a: A
BarInduction A
  apply barinduction_contr, (contr_inhabited_hprop A a).
Defined.

(** Note that [monotone_bar_induction_pointed_monotone_bar_induction] does not have an analogue for full bar induction. We prove below that every type satisfying full bar induction is Sigma-compact and therefore decidable. Then, as in [monotone_bar_induction_hprop], we would be able to prove that any proposition satisfies bar induction and therefore that every proposition is decidable. *)

(** ** Implications of bar induction *)

(** Full bar induction for a type [A] implies that it is Sigma-compact, in the sense that any decidable family over [A] has a decidable Sigma-type. To prove this, we begin by defining a type family [P] on [list A] so that [P nil] is our goal. *)

Definition BI_sig_family {A : Type} (P : A -> Type) (l : list A) : Type
  := match l with
      | nil => Decidable {a : A & P a}
      | a :: l' => ~(P a)
     end.

Definition is_bar_BI_sig_family {A : Type} {P : A -> Type}
  (dec : forall n : A, Decidable (P n))
  : IsBar (BI_sig_family P).
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
IsBar (BI_sig_family P)
Proof.
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
IsBar (BI_sig_family P)
  intro s.
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
s: nat -> A
{n : nat & BI_sig_family P (list_restrict s n)}
  destruct (dec (s 0)) as [p|p'].
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
s: nat -> A
p: P (s 0)
{n : nat & BI_sig_family P (list_restrict s n)}
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
s: nat -> A
p': ~ P (s 0)
{n : nat & BI_sig_family P (list_restrict s n)}
  -
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
s: nat -> A
p: P (s 0)
{n : nat & BI_sig_family P (list_restrict s n)} exists 0.
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
s: nat -> A
p: P (s 0)
BI_sig_family P (list_restrict s 0)
    simpl.
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
s: nat -> A
p: P (s 0)
Decidable {a : A & P a}
    exact (inl (s 0; p)).
  -
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
s: nat -> A
p': ~ P (s 0)
{n : nat & BI_sig_family P (list_restrict s n)} exists 1.
A: Type
P: A -> Type
dec: forall n : A, Decidable (P n)
s: nat -> A
p': ~ P (s 0)
BI_sig_family P (list_restrict s 1)
    exact p'.
Defined.

Definition isinductive_BI_sig_family {A : Type} (P : A -> Type)
  : IsInductive (BI_sig_family P).
A: Type
P: A -> Type
IsInductive (BI_sig_family P)
Proof.
A: Type
P: A -> Type
IsInductive (BI_sig_family P)
  intros [|a l] h.
A: Type
P: A -> Type
h: forall a : A, BI_sig_family P (nil ++ [a])
BI_sig_family P nil
A: Type
P: A -> Type
a: A
l: list A
h: forall a0 : A, BI_sig_family P ((a :: l) ++ [a0])
BI_sig_family P (a :: l)
  -
A: Type
P: A -> Type
h: forall a : A, BI_sig_family P (nil ++ [a])
BI_sig_family P nil right.
A: Type
P: A -> Type
h: forall a : A, BI_sig_family P (nil ++ [a])
~ {a : A & P a} exact (fun pa => h pa.1 pa.2).
  -
A: Type
P: A -> Type
a: A
l: list A
h: forall a0 : A, BI_sig_family P ((a :: l) ++ [a0])
BI_sig_family P (a :: l) exact (h a).
Defined.

Definition issigcompact_barinduction {A : Type} (BI : BarInduction A)
  (P : A -> Type) (dec : forall n : A, Decidable (P n))
  : Decidable {a : A & P a}
  := BI (BI_sig_family P)
          (isinductive_BI_sig_family P) (is_bar_BI_sig_family dec).

(** Full bar induction for [nat] implies the limited principle of omniscience, i.e., for every sequence of natural numbers we can decide whether every term is zero or there exists a non-zero term. *)

Definition LPO_barinduction {BI : BarInduction nat} (s : nat -> nat)
  : (forall n : nat, s n = 0) + {n : nat & s n <> 0}.
BI: BarInduction nat
s: nat -> nat
(forall n : nat, s n = 0) + {n : nat & s n <> 0}
Proof.
BI: BarInduction nat
s: nat -> nat
(forall n : nat, s n = 0) + {n : nat & s n <> 0}
  destruct (issigcompact_barinduction BI (fun n => s n <> 0) _) as [l|r].
BI: BarInduction nat
s: nat -> nat
l: {a : nat & s a <> 0}
(forall n : nat, s n = 0) + {n : nat & s n <> 0}
BI: BarInduction nat
s: nat -> nat
r: ~ {a : nat & s a <> 0}
(forall n : nat, s n = 0) + {n : nat & s n <> 0}
  -
BI: BarInduction nat
s: nat -> nat
l: {a : nat & s a <> 0}
(forall n : nat, s n = 0) + {n : nat & s n <> 0} right; exact l.
  -
BI: BarInduction nat
s: nat -> nat
r: ~ {a : nat & s a <> 0}
(forall n : nat, s n = 0) + {n : nat & s n <> 0} left; exact (fun n => stable (fun z : s n <> 0 => r (n; z))).
Defined.