Bool.v

(* -*- mode: coq; mode: visual-line -*- *)
(** * Theorems about the booleans *)

Require Import HoTT.Basics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Equiv.

Local Open Scope path_scope.

(* coq calls it "bool", we call it "Bool" *)
Local Unset Elimination Schemes.
Inductive Bool : Type0 :=
  | true : Bool
  | false : Bool.
Scheme Bool_ind := Induction for Bool Sort Type.
Scheme Bool_rec := Minimality for Bool Sort Type.
(* For compatibility with Coq's [induction] *)
Definition Bool_rect := Bool_ind.

Add Printing If Bool.

Declare Scope bool_scope.

Delimit Scope bool_scope with Bool.

Bind Scope bool_scope with Bool.

Definition andb (b1 b2 : Bool) : Bool := if b1 then b2 else false.

Definition orb (b1 b2 : Bool) : Bool := if b1 then true else b2.

Definition negb (b : Bool) := if b then false else true.

Definition implb (b1 b2 : Bool) : Bool := if b1 then b2 else true.

Infix "||" := orb : bool_scope.
Infix "&&" := andb : bool_scope.
Infix "->" := implb : bool_scope.

Definition implb_true {b} : implb b true = true
  := if b as b return implb b true = true then idpath else idpath.

Definition implb_impl {a b} : (a -> b)%Bool = true <-> (a = true -> b = true).a, b: Bool
(a -> b)%Bool = true <-> (a = true -> b = true)
Proof.a, b: Bool
(a -> b)%Bool = true <-> (a = true -> b = true)
  destruct a; simpl; split; trivial using idpath with nocore;
  destruct b; simpl; auto using idpath with nocore.
Defined.

Global Instance trunc_if n A B `{IsTrunc n A, IsTrunc n B} (b : Bool)
: IsTrunc n (if b then A else B) | 100
  := if b as b return (IsTrunc n (if b then A else B)) then _ else _.

(** ** Decidability *)

Section BoolDecidable.
  Definition false_ne_true : ~ (false = true)
    := fun H => match H in (_ = y) return (if y return Set then Empty else Bool) with
                  | 1%path => true
                end.

  Definition true_ne_false : ~ (true = false)
    := fun H => false_ne_true (symmetry _ _ H).

  Global Instance decidable_paths_bool : DecidablePaths Bool
    := fun x y => match x as x, y as y return ((x = y) + ~(x = y)) with
                    | true, true => inl idpath
                    | false, false => inl idpath
                    | true, false => inr true_ne_false
                    | false, true => inr false_ne_true
                  end.

  Corollary hset_bool : IsHSet Bool.IsHSet Bool
  Proof.IsHSet Bool
    exact _.
  Defined.
End BoolDecidable.

(** In particular, [negb] has no fixed points *)
Definition not_fixed_negb (b : Bool) : negb b <> b
  := match b return negb b <> b with
       | true => false_ne_true
       | false => true_ne_false
     end.

(** And conversely, if two elements of [Bool] are unequal, they must be related by [negb]. *)
Definition negb_ne {b1 b2 : Bool}
: (b1 <> b2) -> (b1 = negb b2).b1, b2: Bool
b1 <> b2 -> b1 = negb b2
Proof.b1, b2: Bool
b1 <> b2 -> b1 = negb b2
  destruct b1, b2.true <> true -> true = negb true
true <> false -> true = negb false
false <> true -> false = negb true
false <> false -> false = negb false
  -true <> true -> true = negb true intros oops; case (oops idpath).
  -true <> false -> true = negb false reflexivity.
  -false <> true -> false = negb true reflexivity.
  -false <> false -> false = negb false intros oops; case (oops idpath).
Defined.

(** This version of [negb_ne] is more convenient to [destruct] against. *)
Definition negb_ne' {b1 b2 : Bool}
  : (b1 <> b2) -> (negb b1 = b2).b1, b2: Bool
b1 <> b2 -> negb b1 = b2
Proof.b1, b2: Bool
b1 <> b2 -> negb b1 = b2
  intros oops.b1, b2: Bool
oops: b1 <> b2
negb b1 = b2
  symmetry.b1, b2: Bool
oops: b1 <> b2
b2 = negb b1
  apply negb_ne.b1, b2: Bool
oops: b1 <> b2
b2 <> b1
  exact (symmetric_neq oops).
Defined.

(** ** Products as [forall] over [Bool] *)

Section BoolForall.
  Variable P : Bool -> Type.

  Let f (s : forall b, P b) := (s false, s true).

  Let g (u : P false * P true) (b : Bool) : P b :=
    match b with
      | false => fst u
      | true => snd u
    end.

  Definition equiv_bool_forall_prod `{Funext} :
    (forall b, P b) <~> P false * P true.P: Bool -> Type
f:= fun s : forall b : Bool, P b => (s false, s true): (forall b : Bool, P b) -> P false * P true
g:= fun (u : P false * P true) (b : Bool) =>
if b as b0 return (P b0) then snd u else fst u: P false * P true -> forall b : Bool, P b
H: Funext
(forall b : Bool, P b) <~> P false * P true
  Proof.P: Bool -> Type
f:= fun s : forall b : Bool, P b => (s false, s true): (forall b : Bool, P b) -> P false * P true
g:= fun (u : P false * P true) (b : Bool) =>
if b as b0 return (P b0) then snd u else fst u: P false * P true -> forall b : Bool, P b
H: Funext
(forall b : Bool, P b) <~> P false * P true
    apply (equiv_adjointify f g);
    repeat (reflexivity
              || intros []
              || intro
              || apply path_forall).

  Defined.
End BoolForall.

Definition equiv_bool_rec_uncurried `{Funext} (P : Type) : P * P <~> (Bool -> P)
  := (equiv_bool_forall_prod (fun _ => P))^-1%equiv.

(** ** The type [Bool <~> Bool] is equivalent to [Bool]. *)

(** The nonidentity equivalence is negation (the flip). *)
Global Instance isequiv_negb : IsEquiv negb.IsEquiv negb
Proof.IsEquiv negb
  refine (@Build_IsEquiv
            _ _
            negb negb
            (fun b => if b as b return negb (negb b) = b then idpath else idpath)
            (fun b => if b as b return negb (negb b) = b then idpath else idpath)
            _).forall x : Bool,
(if negb x as b return (negb (negb b) = b)
 then 1
 else 1) =
ap negb
  (if x as b return (negb (negb b) = b) then 1 else 1)
  intros []; simpl; exact idpath.
Defined.

Definition equiv_negb : Bool <~> Bool
  := Build_Equiv Bool Bool negb _.

(** Any equivalence [Bool <~> Bool] sends [true] and [false] to different things. *)
Lemma eval_bool_isequiv (f : Bool -> Bool) `{IsEquiv Bool Bool f}
: f false = negb (f true).f: Bool -> Bool
H: IsEquiv f
f false = negb (f true)
Proof.f: Bool -> Bool
H: IsEquiv f
f false = negb (f true)
  pose proof (eissect f true).f: Bool -> Bool
H: IsEquiv f
X: (f^-1 o f) true = idmap true
f false = negb (f true)
  pose proof (eissect f false).f: Bool -> Bool
H: IsEquiv f
X: (f^-1 o f) true = idmap true
X0: (f^-1 o f) false = idmap false
f false = negb (f true)
  simpl in *.f: Bool -> Bool
H: IsEquiv f
X: f^-1 (f true) = true
X0: f^-1 (f false) = false
f false = negb (f true)
  destruct (f true), (f false).f: Bool -> Bool
H: IsEquiv f
X: f^-1 true = true
X0: f^-1 true = false
true = negb true
f: Bool -> Bool
H: IsEquiv f
X: f^-1 true = true
X0: f^-1 false = false
false = negb true
f: Bool -> Bool
H: IsEquiv f
X: f^-1 false = true
X0: f^-1 true = false
true = negb false
f: Bool -> Bool
H: IsEquiv f
X: f^-1 false = true
X0: f^-1 false = false
false = negb false
  -f: Bool -> Bool
H: IsEquiv f
X: f^-1 true = true
X0: f^-1 true = false
true = negb true etransitivity; try (eassumption || (symmetry; eassumption)).
  -f: Bool -> Bool
H: IsEquiv f
X: f^-1 true = true
X0: f^-1 false = false
false = negb true simpl.f: Bool -> Bool
H: IsEquiv f
X: f^-1 true = true
X0: f^-1 false = false
false = false reflexivity.
  -f: Bool -> Bool
H: IsEquiv f
X: f^-1 false = true
X0: f^-1 true = false
true = negb false simpl.f: Bool -> Bool
H: IsEquiv f
X: f^-1 false = true
X0: f^-1 true = false
true = true reflexivity.
  -f: Bool -> Bool
H: IsEquiv f
X: f^-1 false = true
X0: f^-1 false = false
false = negb false etransitivity; try (eassumption || (symmetry; eassumption)).
Defined.

Section EquivBoolEquiv.

  (** We will identify the constant equivalence with [true] and the flip equivalence with [false], and do this by evaluating the equivalence function on [true]. *)
  Let f : (Bool <~> Bool) -> Bool := fun e => e true.
  Let g : Bool -> (Bool <~> Bool) := fun b => if b
                                              then (equiv_idmap Bool)
                                              else equiv_negb.

  Definition aut_bool_canonical (e : Bool <~> Bool)
  : e == g (f e).f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e: Bool <~> Bool
e == g (f e)
  Proof.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e: Bool <~> Bool
e == g (f e)
    unfold f, g; clear f g; intros []; simpl.e: Bool <~> Bool
e true = (if e true then 1%equiv else equiv_negb) true
e: Bool <~> Bool
e false =
(if e true then 1%equiv else equiv_negb) false
    -e: Bool <~> Bool
e true = (if e true then 1%equiv else equiv_negb) true destruct (e true); reflexivity.
    -e: Bool <~> Bool
e false =
(if e true then 1%equiv else equiv_negb) false refine (eval_bool_isequiv e @ _).e: Bool <~> Bool
negb (e true) =
(if e true then 1%equiv else equiv_negb) false
      destruct (e true); reflexivity.
  Defined.

  Lemma equiv_bool_aut_bool `{Funext} : Bool <~> (Bool <~> Bool).f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
Bool <~> (Bool <~> Bool)
  Proof.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
Bool <~> (Bool <~> Bool)
    refine (equiv_adjointify g f _ _).f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
(fun x : Bool <~> Bool => g (f x)) == idmap
f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
(fun x : Bool => f (g x)) == idmap
    -f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
(fun x : Bool <~> Bool => g (f x)) == idmap intro e.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
e: Bool <~> Bool
g (f e) = e
      apply path_equiv, path_forall.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
e: Bool <~> Bool
g (f e) == e
      intros b; symmetry; apply aut_bool_canonical.
    -f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
(fun x : Bool => f (g x)) == idmap intros []; reflexivity.
  Defined.

  (** It follows that every automorphism of [Bool] is either [idmap] or [negb]. *)
  Definition aut_bool_idmap_or_negb `{Funext} (e : Bool <~> Bool)
  : (e = equiv_idmap Bool) + (e = equiv_negb).f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
e: Bool <~> Bool
(e = 1%equiv) + (e = equiv_negb)
  Proof.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
e: Bool <~> Bool
(e = 1%equiv) + (e = equiv_negb)
    revert e.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
forall e : Bool <~> Bool,
(e = 1%equiv) + (e = equiv_negb) equiv_intro equiv_bool_aut_bool e.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
e: Bool
(equiv_bool_aut_bool e = 1%equiv) +
(equiv_bool_aut_bool e = equiv_negb)
    destruct e; simpl.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
(1%equiv = 1%equiv) + (1%equiv = equiv_negb)
f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
(equiv_negb = 1%equiv) + (equiv_negb = equiv_negb)
    -f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
(1%equiv = 1%equiv) + (1%equiv = equiv_negb) exact (inl idpath).
    -f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
H: Funext
(equiv_negb = 1%equiv) + (equiv_negb = equiv_negb) exact (inr idpath).
  Defined.

  (** But, obviously, not both. *)
  Definition idmap_bool_ne_negb : equiv_idmap Bool <> equiv_negb.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
1%equiv <> equiv_negb
  Proof.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
1%equiv <> equiv_negb
    intros oops.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
oops: 1%equiv = equiv_negb
Empty
    exact (true_ne_false (ap10_equiv oops true)).
  Defined.

  (** In particular, every pair of automorphisms of [Bool] commute with each other. *)
  Definition abelian_aut_bool (e1 e2 : Bool <~> Bool)
  : e1 o e2 == e2 o e1.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e1, e2: Bool <~> Bool
e1 o e2 == e2 o e1
  Proof.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e1, e2: Bool <~> Bool
e1 o e2 == e2 o e1
    intro b.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e1, e2: Bool <~> Bool
b: Bool
e1 (e2 b) = e2 (e1 b)
    refine (ap e1 (aut_bool_canonical e2 b) @ _).f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e1, e2: Bool <~> Bool
b: Bool
e1 (g (f e2) b) = e2 (e1 b)
    refine (aut_bool_canonical e1 _ @ _).f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e1, e2: Bool <~> Bool
b: Bool
g (f e1) (g (f e2) b) = e2 (e1 b)
    refine (_ @ ap e2 (aut_bool_canonical e1 b)^).f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e1, e2: Bool <~> Bool
b: Bool
g (f e1) (g (f e2) b) = e2 (g (f e1) b)
    refine (_ @ (aut_bool_canonical e2 _)^).f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e1, e2: Bool <~> Bool
b: Bool
g (f e1) (g (f e2) b) = g (f e2) (g (f e1) b)
    unfold f, g.f:= fun e : Bool <~> Bool => e true: Bool <~> Bool -> Bool
g:= fun b : Bool => if b then 1%equiv else equiv_negb: Bool -> Bool <~> Bool
e1, e2: Bool <~> Bool
b: Bool
(if e1 true then 1%equiv else equiv_negb)
  ((if e2 true then 1%equiv else equiv_negb) b) =
(if e2 true then 1%equiv else equiv_negb)
  ((if e1 true then 1%equiv else equiv_negb) b)
    destruct (e1 true), (e2 true), b; reflexivity.
  Defined.

End EquivBoolEquiv.