Skip to content

Instantly share code, notes, and snippets.

@kana-sama

kana-sama/unit_neq_bool.v Secret

Last active April 8, 2021 23:08
Download ZIP

Revisions

  1. kana revised this gist Apr 8, 2021. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -29,9 +29,9 @@ 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 eq_a) =>
    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 := eq_a (~~ a) 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 :=
  2. kana revised this gist Apr 8, 2021. 1 changed file with 6 additions and 4 deletions.
    10 changes: 6 additions & 4 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -46,22 +46,24 @@ Definition unit_neq_bool_on_contr : unit <> bool :=
    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 *)

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

    (* Example 2 *)
    Definition gen_unit_neq_bool_2 : unit <> bool :> Type :=
    neq_by is_contr unit_is_contr bool_isn't_contr.

    (* Example 3 *)

    (* 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 4 *)

    (* 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.
  3. kana revised this gist Apr 8, 2021. 1 changed file with 2 additions and 0 deletions.
    2 changes: 2 additions & 0 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -69,3 +69,5 @@ Definition False_isn't_inhabited : ~ is_inhabited False := fun '(mkInhabited 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.
  4. kana revised this gist Apr 8, 2021. 1 changed file with 5 additions and 5 deletions.
    10 changes: 5 additions & 5 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -43,29 +43,29 @@ Definition unit_neq_bool_on_contr : unit <> bool :=


    (* General solution *)
    Definition neq_by_prop (A : Type) {x y : A} {P : A -> Prop} : P x -> ~ P y -> x <> y :=
    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 *)
    Definition gen_unit_neq_bool_1 : unit <> bool :> Type :=
    neq_by_prop Type unit_is_prop bool_isn't_prop.
    neq_by is_prop unit_is_prop bool_isn't_prop.

    (* Example 2 *)
    Definition gen_unit_neq_bool_2 : unit <> bool :> Type :=
    neq_by_prop Type unit_is_contr bool_isn't_contr.
    neq_by is_contr unit_is_contr bool_isn't_contr.

    (* Example 3 *)
    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_prop nat one_eq_one one_neq_two.
    neq_by _ one_eq_one one_neq_two.

    (* Example 4 *)
    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_prop Prop _ _ is_inhabited True_is_inhabited False_isn't_inhabited.
    neq_by (fun x : Prop => is_inhabited x) True_is_inhabited False_isn't_inhabited.

  5. kana revised this gist Apr 8, 2021. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -57,7 +57,7 @@ Definition gen_unit_neq_bool_2 : unit <> bool :> Type :=
    (* Example 3 *)
    Definition one_neq_two : 1 <> 2 :=
    let one_eq_one : 1 = 1 := erefl in
    (* heh, useless *)
    (* heh, useless for terms *)
    let one_neq_two : 1 <> 2 := fun 'erefl => I in
    neq_by_prop nat one_eq_one one_neq_two.

  6. kana revised this gist Apr 8, 2021. 1 changed file with 1 addition and 0 deletions.
    1 change: 1 addition & 0 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -57,6 +57,7 @@ Definition gen_unit_neq_bool_2 : unit <> bool :> Type :=
    (* Example 3 *)
    Definition one_neq_two : 1 <> 2 :=
    let one_eq_one : 1 = 1 := erefl in
    (* heh, useless *)
    let one_neq_two : 1 <> 2 := fun 'erefl => I in
    neq_by_prop nat one_eq_one one_neq_two.

  7. kana revised this gist Apr 8, 2021. 1 changed file with 2 additions and 1 deletion.
    3 changes: 2 additions & 1 deletion unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -56,8 +56,9 @@ Definition gen_unit_neq_bool_2 : unit <> bool :> Type :=

    (* Example 3 *)
    Definition one_neq_two : 1 <> 2 :=
    let one_eq_one : 1 = 1 := erefl in
    let one_neq_two : 1 <> 2 := fun 'erefl => I in
    neq_by_prop nat erefl one_neq_two.
    neq_by_prop nat one_eq_one one_neq_two.

    (* Example 4 *)
    Inductive is_inhabited (A : Type) : Prop := mkInhabited (value : A).
  8. kana revised this gist Apr 8, 2021. 1 changed file with 2 additions and 4 deletions.
    6 changes: 2 additions & 4 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -56,10 +56,8 @@ Definition gen_unit_neq_bool_2 : unit <> bool :> Type :=

    (* Example 3 *)
    Definition one_neq_two : 1 <> 2 :=
    let eq_one := fun x => x = 1 in
    let one_eq_one : eq_one 1 := erefl in
    let two_neq_one : ~ eq_one 2 := fun 'erefl => I in
    neq_by_prop nat one_eq_one two_neq_one.
    let one_neq_two : 1 <> 2 := fun 'erefl => I in
    neq_by_prop nat erefl one_neq_two.

    (* Example 4 *)
    Inductive is_inhabited (A : Type) : Prop := mkInhabited (value : A).
  9. kana revised this gist Apr 8, 2021. 1 changed file with 1 addition and 3 deletions.
    4 changes: 1 addition & 3 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -44,9 +44,7 @@ Definition unit_neq_bool_on_contr : unit <> bool :=

    (* General solution *)
    Definition neq_by_prop (A : Type) {x y : A} {P : A -> Prop} : P x -> ~ P y -> x <> y :=
    fun px npy xy =>
    let py : P y := match xy in _ = z return P z with erefl => px end in
    npy py.
    fun px npy xy => npy (let 'erefl := xy in px).

    (* Example 1 *)
    Definition gen_unit_neq_bool_1 : unit <> bool :> Type :=
  10. kana revised this gist Apr 8, 2021. 1 changed file with 2 additions and 1 deletion.
    3 changes: 2 additions & 1 deletion unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -45,7 +45,8 @@ Definition unit_neq_bool_on_contr : unit <> bool :=
    (* General solution *)
    Definition neq_by_prop (A : Type) {x y : A} {P : A -> Prop} : P x -> ~ P y -> x <> y :=
    fun px npy xy =>
    npy (match xy in _ = z return P z with erefl => px end : P y).
    let py : P y := match xy in _ = z return P z with erefl => px end in
    npy py.

    (* Example 1 *)
    Definition gen_unit_neq_bool_1 : unit <> bool :> Type :=
  11. kana revised this gist Apr 8, 2021. 1 changed file with 5 additions and 3 deletions.
    8 changes: 5 additions & 3 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -1,3 +1,5 @@
    From mathcomp Require Import all_ssreflect.

    (* Simple solution via is_prop *)
    Definition is_prop (A : Type) : Prop :=
    forall x y : A, x = y.
    @@ -41,9 +43,9 @@ Definition unit_neq_bool_on_contr : unit <> bool :=


    (* General solution *)
    Definition neq_by_prop (U : Type) {A B : U} {P : U -> Prop} : P A -> ~ P B -> A <> B :=
    fun PA not_PB A_eq_B =>
    not_PB (match A_eq_B in _ = X return P X with erefl => PA end : P B).
    Definition neq_by_prop (A : Type) {x y : A} {P : A -> Prop} : P x -> ~ P y -> x <> y :=
    fun px npy xy =>
    npy (match xy in _ = z return P z with erefl => px end : P y).

    (* Example 1 *)
    Definition gen_unit_neq_bool_1 : unit <> bool :> Type :=
  12. kana revised this gist Apr 8, 2021. 1 changed file with 16 additions and 6 deletions.
    22 changes: 16 additions & 6 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -1,3 +1,4 @@
    (* Simple solution via is_prop *)
    Definition is_prop (A : Type) : Prop :=
    forall x y : A, x = y.

    @@ -18,7 +19,7 @@ Definition unit_neq_bool_on_prop : unit <> bool :=
    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.

    @@ -39,22 +40,31 @@ Definition unit_neq_bool_on_contr : unit <> bool :=
    in bool_isn't_contr bool_is_contr.


    Definition type_inequality (U : Type) {A B : U} {P : U -> Prop} : P A -> ~ P B -> A <> B :=
    (* General solution *)
    Definition neq_by_prop (U : Type) {A B : U} {P : U -> Prop} : P A -> ~ P B -> A <> B :=
    fun PA not_PB A_eq_B =>
    not_PB (match A_eq_B in _ = X return P X with erefl => PA end : P B).

    (* Example 1 *)
    Definition gen_unit_neq_bool_1 : unit <> bool :> Type :=
    type_inequality Type unit_is_prop bool_isn't_prop.
    neq_by_prop Type unit_is_prop bool_isn't_prop.

    (* Example 2 *)
    Definition gen_unit_neq_bool_2 : unit <> bool :> Type :=
    type_inequality Type unit_is_contr bool_isn't_contr.

    neq_by_prop Type unit_is_contr bool_isn't_contr.

    (* Example 3 *)
    Definition one_neq_two : 1 <> 2 :=
    let eq_one := fun x => x = 1 in
    let one_eq_one : eq_one 1 := erefl in
    let two_neq_one : ~ eq_one 2 := fun 'erefl => I in
    neq_by_prop nat one_eq_one two_neq_one.

    (* Example 4 *)
    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 :=
    @type_inequality Prop _ _ is_inhabited True_is_inhabited False_isn't_inhabited.
    @neq_by_prop Prop _ _ is_inhabited True_is_inhabited False_isn't_inhabited.

  13. kana created this gist Apr 8, 2021.
    60 changes: 60 additions & 0 deletions unit_neq_bool.v
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,60 @@
    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.



    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 eq_a) =>
    let a_neq_na : a <> ~~ a := match a with true | false => fun 'erefl => I end in
    let a_eq_na : a = ~~ a := eq_a (~~ 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.


    Definition type_inequality (U : Type) {A B : U} {P : U -> Prop} : P A -> ~ P B -> A <> B :=
    fun PA not_PB A_eq_B =>
    not_PB (match A_eq_B in _ = X return P X with erefl => PA end : P B).

    Definition gen_unit_neq_bool_1 : unit <> bool :> Type :=
    type_inequality Type unit_is_prop bool_isn't_prop.

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



    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 :=
    @type_inequality Prop _ _ is_inhabited True_is_inhabited False_isn't_inhabited.