bool_by_j_pred.v

Definition sig_fst {A B} {p q : {x : A & B x}} (H : p = q)
  : projT1 p = projT1 q :=
  eq_rect _ (fun z => projT1 p = projT1 z) eq_refl _ H.

Definition sig_snd {A B} {p q : {x : A & B x}} (H : p = q)
  : eq_rect _ B (projT2 p) _ (sig_fst H) = projT2 q :=
  match H with
  | eq_refl => eq_refl
  end.

Lemma sig_ext {A B} (p q : {x : A & B x})
  (H1 : projT1 p = projT1 q)
  (H2 : eq_rect _ B (projT2 p) _ H1 = projT2 q)
  : p = q.
  destruct p, q; simpl in *.
  destruct H1, H2; simpl in *.
  reflexivity.
Defined.

Definition C_Bool : Type := forall A, A -> A -> A.
Definition c_true : C_Bool := fun A t f => t.
Definition c_false : C_Bool := fun A t f => f.

Definition I_Bool (c_b : C_Bool) : Type :=
  forall P, P c_true -> P c_false -> P c_b.
Definition i_true : I_Bool c_true := fun P t f => t.
Definition i_false : I_Bool c_false := fun P t f => f.

Definition W_Bool : Type := {c_b : C_Bool & I_Bool c_b}.
Definition w_true : W_Bool := existT _ c_true i_true.
Definition w_false : W_Bool := existT _ c_false i_false.

Definition Bool : Type := {w_b : W_Bool &
  projT1 w_b _ (w_true = w_b) (w_false = w_b)}.
Definition true : Bool := existT _ w_true eq_refl.
Definition false : Bool := existT _ w_false eq_refl.

Lemma contr_true w : true = existT _ w_true w.
  simpl in w; unfold c_true in w.
  apply (sig_ext true (existT _ _ _) w).
  unfold eq_rect; simpl.
  exact (
    match w in (_ = existT _ c_b i_b) return
      i_b
        (fun c_b => forall i_b,
          w_true = existT _ c_b i_b ->
          w_true = existT _ c_b i_b)
        (fun i_b w =>
          match w in (_ = w_b) return
            (projT1 w_b _ (w_true = w_b) (w_false = w_b))
          with
          | eq_refl => eq_refl
          end)
        (fun i_b w => w)
        i_b
        w =
        w with
    | eq_refl => eq_refl
    end
  ).
Defined.

Lemma contr_c_true i_b w : true = existT _ (existT _ c_true i_b) w.
  unfold c_true in *; simpl in *; fold c_true in *.
  refine (
    match w in (_ = w_b) return
      forall w,
      true = existT _ w_b w with
    | eq_refl => _
    end w
  ).
  clear; intros w.
  apply contr_true.
Defined.

Lemma contr_false w : false = existT _ w_false w.
  simpl in w; unfold c_false in w.
  apply (sig_ext false (existT _ _ _) w).
  unfold eq_rect; simpl.
  exact (
    match w in (_ = existT _ c_b i_b) return
      i_b
        (fun c_b => forall i_b,
          w_false = existT _ c_b i_b ->
          w_false = existT _ c_b i_b)
        (fun i_b w => w)
        (fun i_b w =>
          match w in (_ = w_b) return
            (projT1 w_b _ (w_true = w_b) (w_false = w_b))
          with
          | eq_refl => eq_refl
          end)
        i_b
        w =
        w with
    | eq_refl => eq_refl
    end
  ).
Defined.

Lemma contr_c_false i_b w : false = existT _ (existT _ c_false i_b) w.
  unfold c_false in *; simpl in *; fold c_false in *.
  refine (
    match w in (_ = w_b) return
      forall w,
      false = existT _ w_b w with
    | eq_refl => _
    end w
  ).
  clear; intros w.
  apply contr_false.
Defined.

Definition case (b : Bool) : C_Bool := projT1 (projT1 b).

Lemma ind b : forall P : Bool -> Type, P true -> P false -> P b.
  destruct b as [[c_b i_b] w]; simpl in *.
  intros P t f.
  (* TODO: this is really ugly *)
  assert (c_b Type (P true) (P false) = P (existT _ (existT _ c_b i_b) w)).
  refine (
    i_b (fun i_c_b => i_c_b = c_b ->
      i_c_b _ (P true) (P false) = P (existT _ (existT _ c_b i_b) w)
     ) _ _ eq_refl
  ); intros H; destruct H.
  rewrite (contr_c_true i_b w); reflexivity.
  rewrite (contr_c_false i_b w); reflexivity.
  epose (i_b (fun c_b => c_b _ (P true) (P false)) t f); simpl in *.
  rewrite H in p; exact p.
Defined.