Skip to content

Instantly share code, notes, and snippets.

@kana-sama
Last active April 8, 2021 23:08
Show Gist options
  • Save kana-sama/11acc3e66d72f5203faddf403fbbaa4d to your computer and use it in GitHub Desktop.
Save kana-sama/11acc3e66d72f5203faddf403fbbaa4d to your computer and use it in GitHub Desktop.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment