unit_neq_bool.v

From mathcomp Require Import all_ssreflect.

(* Simple solution via is_prop *)
Definition is_prop (A : Type) : Prop :=
  forall x y : A, x = y.

Definition unit_is_prop : is_prop unit :=
  fun 'tt 'tt => erefl.

Definition bool_isn't_prop : ~ is_prop bool :=
  fun bool_is_prop => 
    let true_neq_false : true <> false := fun 'erefl => I in
    let true_eq_false : true = false := bool_is_prop true false in
    true_neq_false true_eq_false.

Definition unit_neq_bool_on_prop : unit <> bool :=
  fun unit_eq_bool =>
    let bool_is_prop : is_prop bool :=
      match unit_eq_bool in _ = U return is_prop U
       with erefl => unit_is_prop end
     in bool_isn't_prop bool_is_prop.


(* Simple solution via is_contr *)
Definition is_contr (A : Type) : Prop :=
  exists x : A, forall y : A, x = y.

Definition unit_is_contr : is_contr unit :=
  ex_intro _ tt (fun 'tt => erefl).

Definition bool_isn't_contr : ~ is_contr bool :=
  fun '(ex_intro a a_eq_) => 
    let a_neq_na : a <> ~~ a := match a with true | false => fun 'erefl => I end in
    let a_eq_na : a = ~~ a := a_eq_ (~~a) in
    a_neq_na a_eq_na.

Definition unit_neq_bool_on_contr : unit <> bool :=
  fun unit_eq_bool =>
    let bool_is_contr : is_contr bool :=
      match unit_eq_bool in _ = U return is_contr U
       with erefl => unit_is_contr end
     in bool_isn't_contr bool_is_contr.


(* General solution *)
Definition neq_by {A : Type} {x y : A} (P : A -> Prop) : P x -> ~ P y -> x <> y :=
  fun px npy xy => npy (let 'erefl := xy in px).

  
(* Example 1, unit <> bool *)
Definition gen_unit_neq_bool_1 : unit <> bool :> Type :=
  neq_by is_prop unit_is_prop bool_isn't_prop.

Definition gen_unit_neq_bool_2 : unit <> bool :> Type :=
  neq_by is_contr unit_is_contr bool_isn't_contr.


(* Example 2 *)
Definition one_neq_two : 1 <> 2 :=
  let one_eq_one : 1 = 1 := erefl in
  (* heh, useless for terms *)
  let one_neq_two : 1 <> 2 := fun 'erefl => I in
  neq_by _ one_eq_one one_neq_two.


(* Example 3, True <> False *)
Inductive is_inhabited (A : Type) : Prop := mkInhabited (value : A).
Definition True_is_inhabited : is_inhabited True := mkInhabited _ I.
Definition False_isn't_inhabited : ~ is_inhabited False := fun '(mkInhabited f) => f.

Definition gen_true_neq_false : True <> False :=
  neq_by (fun x : Prop => is_inhabited x) True_is_inhabited False_isn't_inhabited.

Definition gen_true_neq_false_2 : True <> False :=
  neq_by id I id.