check_with_type_error.v

Set Implicit Arguments.
Unset Strict Implicit.

Definition True_or_Eq (P: Prop)(dec: {P}+{~P}): Prop := if dec then True else 0 = 0.
Definition I_or_0eq0 (P: Prop)(dec: {P}+{~P}): True_or_Eq dec :=
  if dec as dec' return True_or_Eq dec' then I else eq_refl 0.
Definition onlyTrue (H: True): True := H.

Class dec_Type :=
  {
    carrier: Type;
    decider: forall (x y: carrier), {x = y} + {~x = y}
  }.
Coercion carrier: dec_Type >-> Sortclass.

Definition check_eq {X: dec_Type}(x y: X) := I_or_0eq0 (decider x y).
Notation ok x y := (onlyTrue (check_eq x y)).


Require Import Bool.

Instance dec_bool: dec_Type :=
  {
    decider := bool_dec
  }.

Notation "1" := true: bool_scope.
Notation "0" := false: bool_scope.

Open Scope bool_scope.

Definition nand (x y: bool): bool :=
  match x, y with
  | 1,1 => 0
  | _,_ => 1
  end.
Notation "x 'NAND' y" := (nand x y) (at level 50, left associativity).

Check ok (0 NAND 0) 1.
Check ok (1 NAND 0) 1.
Check ok (0 NAND 1) 1.
Check ok (1 NAND 1) 0.


Definition and (x y: bool) := let b := (x NAND y) in b NAND b.
Notation "x 'AND' y" := (and x y) (at level 40, left associativity).
Notation "x * y" := (x AND y) (at level 40, left associativity).

Check ok (0 AND 0) 0.
Check ok (1 AND 0) 0.
Check ok (0 AND 1) 0.
Check ok (1 AND 1) 1.


Definition not (x: bool): bool := x NAND x.
Notation "'NOT' x" := (not x) (at level 35, right associativity): bool_scope.
Notation "! x" := (not x) (at level 35, right associativity): bool_scope.

Check ok (NOT 0) 1.
Check ok (NOT 1) 0.


Definition or (x y: bool) := !(!x * !y).
Notation "x 'OR' y" := (or x y) (at level 50, left associativity): bool_scope.
Notation "x + y" := (x OR y) (at level 50, left associativity): bool_scope.

Check ok (0 OR 0) 0.
Check ok (1 OR 0) 1.
Check ok (0 OR 1) 1.
Check ok (1 OR 1) 1.


Definition xor (x y: bool): bool := (x + y) * (x NAND y).
Notation "x 'XOR' y" := (xor x y) (at level 55, left associativity): bool_scope.

Check ok (0 XOR 0) 0.
Check ok (1 XOR 0) 1.
Check ok (0 XOR 1) 1.
Check ok (1 XOR 1) 0.


Definition mux (x y sel: bool): bool := (!sel * x) + (sel * y).

Check ok (mux 0 0 0) 0.
Check ok (mux 0 0 1) 0.
Check ok (mux 0 1 0) 0.
Check ok (mux 0 1 1) 1.
Check ok (mux 1 0 0) 1.
Check ok (mux 1 0 1) 0.
Check ok (mux 1 1 0) 1.
Check ok (mux 1 1 1) 1.


Definition mux' (x y sel: bool): bool := (!sel * x) + (!sel * y).

Check ok (mux' 0 0 0) 0.
Check ok (mux' 0 0 1) 0.
Fail Check ok (mux' 0 1 0) 0.
(* The command has indeed failed with message: *)
(* => Error: The term "check_eq (mux' 0 1 0) 0" has type *)
(*     "True_or_Eq (decider (mux' 0 1 0) 0)" while it is expected to have type *)
(*     "True". *)


Require Import Arith.
Open Scope nat_scope.

Instance dec_nat: dec_Type :=
  {
    decider := eq_nat_dec
  }.

Fixpoint evenb (n: nat) :=
  match n with
  | O => true
  | S n' => negb (evenb n')
  end.

Definition updown (n: nat): nat :=
  match n with
  | O => S O
  | S n' => if evenb n' then n' else S n
  end.

Check ok (updown 0) 1.
Check ok (updown 1) 0.
Fail Check ok (updown 2) 1.
(* The command has indeed failed with message: *)
(* => Error: The term "check_eq (updown 2) 1" has type *)
(*     "True_or_Eq (decider (updown 2) 1)" while it is expected to have type *)
(*     "True". *)
Check ok (updown 2) 3.
Check ok (updown 3) 2.
Check ok (updown 4) 5.