Inductive type bool from Coq's Init.Datatypes

[benediktahrens]

We are using the booleans of Coq.Init.Datatypes, which are defined as an inductive type:

Inductive bool : Set :=
  | true : bool
  | false : bool.

Should we try replacing it by unit \coprod unit? Is the alternative definition of bool as coproduct already given somewhere?

[DanGrayson]

Before we do that, I'd like to try replacing coprod by total2 over stn 2. Since many analogous theorems are proved for both coprod and total2, we'd be able to shorten many proofs. An example: a coproduct of sets is a set, and a total space of a family of sets indexed by a set is a set.

Then it would make sense to replace bool by stn 2.

[arnoudvanderleer]

@DanGrayson I think it would be unwise to define coprod via total2, because then we can no longer use the induction tactic for elements of coprod A B for case distinction. And of course, we still could prove an induction principle lemma, but personally, I prefer being able to use the induction tactic.

[arnoudvanderleer]

Come to think of it, we have the same problem with coprod unit unit, because then induction x will give two cases: inl x' and inr x'. These are not definitionally equal to true and false, not everything in unit is definitionally equal to tt. So we would have to do induction x as [x' | x']; induction x'. or something like that. And that feels cumbersome when one neesd to to it very often. For example, the proof of andb_is_commutative would get slightly longer:

Definition bool := unit ⨿ unit.

Definition andb : bool -> bool -> bool.
Proof.
  intros b1 b2; induction b1; [exact b2|exact (inr tt)].
Defined.

Lemma andb_is_commutative :
  ∏ b1 b2 : bool, andb b1 b2 = andb b2 b1.
Proof.
  intros; induction b1; induction b2.
Qed.

So is this a thing we still want?

[arnoudvanderleer]

On the other hand, it may be possible to write a tactic that has knowledge about a couple of "types that are equivalent to inductive types". Something like

Tactic old_induction = induction.

Tactic induction [some parameter x] :=
  match typeof x with
    coprod => refine (coprod_ind _ _)
    bool => refine (bool_ind _ _)
    _ => induction x
  end.

[arnoudvanderleer]

Oh, I just realized that we can provide our own induction principles to coq with induction ... using some_bool_rect, so it is slightly more of a hassle, but still doable.

Definition bool := unit ⨿ unit.

Notation "'true'" := (inl tt).
Notation "'false'" := (inr tt).

Definition bool_rect
    (P : bool → Type)
    (HT : P true)
    (HF : P false)
    (c : bool)
    : P c.
Proof.
  now induction c as [t | t];
  induction t.
Defined.

Definition andb : bool -> bool -> bool.
Proof.
  intros b1 b2;
  induction b1 using bool_rect;
  [exact b2 | exact false].
Defined.

Lemma andb_is_commutative :
  ∏ b1 b2 : bool, andb b1 b2 = andb b2 b1.
Proof.
  now intros;
  induction b1 using bool_rect;
  induction b2 using bool_rect.
Qed.

works like a charm.

Regardless, @benediktahrens , how does this tie into the freeze of Foundations?

[arnoudvanderleer]

Closing this as no longer relevant. Feel free to reopen if there is still interest in having/doing this.