Validating Mathematical Structures (Coq Workshop 2019)

demo.v

Section from_ssrfun.

Local Set Implicit Arguments.
Local Unset Strict Implicit.
Local Unset Printing Implicit Defensive.

Variables S T R : Type.

Definition left_inverse e inv (op : S -> T -> R) := forall x, op (inv x) x = e.

Definition left_id e (op : S -> T -> T) := forall x, op e x = x.
Definition right_id e (op : S -> T -> S) := forall x, op x e = x.

Definition left_zero z (op : S -> T -> S) := forall x, op z x = z.
Definition right_zero z (op : S -> T -> T) := forall x, op x z = z.

Definition left_distributive (op : S -> T -> S) add :=
  forall x y z, op (add x y) z = add (op x z) (op y z).
Definition right_distributive (op : S -> T -> T) add :=
  forall x y z, op x (add y z) = add (op x y) (op x z).

Definition commutative (op : S -> S -> T) := forall x y, op x y = op y x.
Definition associative (op : S -> S -> S) :=
  forall x y z, op x (op y z) = op (op x y) z.

End from_ssrfun.

Notation id := (fun x => x).

(******************************************************************************)

Module Monoid.

Record mixin_of (A : Type) := Mixin {
  zero : A;
  add : A -> A -> A;
  _ : associative add;
  _ : left_id zero add;
  }.

Record class_of (A : Type) := Class {
  mixin : mixin_of A
  }.

Structure type :=
  Pack { sort : Type; _ : class_of sort }.

Local Definition class (cT : type) : class_of (sort cT) :=
  match cT as cT' return class_of (sort cT') with Pack _ c => c end.

(* In MathComp, we declare an `Exports` module to gather definitions,         *)
(* coercions, and canonical projections which should be accessible by users,  *)
(* to don't make accessible any names of internal definitions with their      *)
(* unqualified names, e.g, `mixin_of`, `Mixin`, `class_of`, `type`, `Pack`,   *)
(* `sort`, and `class`. Here we comment them out for explanation reasons.     *)
(*
Module Exports.

Coercion sort : type >-> Sortclass.

Definition add {A : type} := add _ (mixin _ (class A)).
Definition zero {A : type} := zero _ (mixin _ (class A)).

End Exports.
*)

End Monoid.
(* Export Monoid.Exports. *)

Definition zero {A : Monoid.type} : Monoid.sort A :=
  Monoid.zero _ (Monoid.mixin _ (Monoid.class A)).
Definition add {A : Monoid.type} :
  Monoid.sort A -> Monoid.sort A ->
  Monoid.sort A :=
  Monoid.add _ (Monoid.mixin _ (Monoid.class A)).

Check @add.
Check @zero.

Coercion Monoid.sort : Monoid.type >-> Sortclass.

Check @add.
Check @zero.

(******************************************************************************)

Module Semiring.

Record mixin_of (A : Monoid.type) := Mixin {
  one : A;
  mul : A -> A -> A;
  _ : commutative (@add A);
  _ : associative mul;
  _ : left_id one mul;
  _ : right_id one mul;
  _ : left_distributive mul add;
  _ : right_distributive mul add;
  _ : left_zero zero mul;
  _ : right_zero zero mul;
  }.

Record class_of (A : Type) := Class {
  base : Monoid.class_of A;
  mixin : mixin_of (Monoid.Pack A base)
  }.

Structure type :=
  Pack { sort : Type; _ : class_of sort }.

Section ClassOps.
Variable (cT : type).

Local Definition class :=
  match cT as cT' return class_of (sort cT') with Pack _ c => c end.

Local Definition monoidType : Monoid.type :=
  Monoid.Pack (sort cT) (base _ class).

End ClassOps.

(*
Module Exports.

Coercion sort : type >-> Sortclass.

Definition mul {A : type} : A -> A -> A := mul _ (mixin _ (class A)).
Definition one {A : type} : A := one _ (mixin _ (class A)).

Coercion monoidType : type >-> Monoid.type.
Canonical monoidType.

End Exports.
*)

End Semiring.
(* Export Semiring.Exports. *)

Coercion Semiring.sort : Semiring.type >-> Sortclass.

Definition mul {A : Semiring.type} : A -> A -> A :=
  Semiring.mul _ (Semiring.mixin _ (Semiring.class A)).
Definition one {A : Semiring.type} : A :=
  Semiring.one _ (Semiring.mixin _ (Semiring.class A)).

(******************************************************************************)

Module Group.

Record mixin_of (A : Monoid.type) := Mixin {
  opp : A -> A;
  _ : left_inverse zero opp add;
  }.

Record class_of (A : Type) := Class {
  base : Monoid.class_of A;
  mixin : mixin_of (Monoid.Pack A base)
  }.

Structure type :=
  Pack { sort : Type; _ : class_of sort }.

Section ClassOps.
Variable (cT : type).

Local Definition class :=
  match cT as cT' return class_of (sort cT') with Pack _ c => c end.

Local Definition monoidType : Monoid.type :=
  Monoid.Pack (sort cT) (base _ class).

End ClassOps.

(*
Module Exports.

Coercion sort : type >-> Sortclass.

Definition opp {A : type} : A -> A := opp _ (mixin _ (class A)).

Coercion monoidType : type >-> Monoid.type.
Canonical monoidType.

End Exports.
*)

End Group.
(* Export Group.Exports. *)

Coercion Group.sort : Group.type >-> Sortclass.

Definition opp {A : Group.type} : A -> A :=
  Group.opp _ (Group.mixin _ (Group.class A)).

(******************************************************************************)

Module Ring.

Record class_of (A : Type) := Class {
  base : Group.class_of A;
  semiring_mixin :
    Semiring.mixin_of (Monoid.Pack A (Group.base A base));
  }.

Structure type :=
  Pack { sort : Type; _ : class_of sort }.

Section ClassOps.
Variable (cT : type).

Local Definition class :=
  match cT as cT' return class_of (sort cT') with Pack _ c => c end.

Local Definition monoidType : Monoid.type :=
  Monoid.Pack
    (sort cT) (Group.base _ (base _ class)).
Local Definition groupType : Group.type :=
  Group.Pack (sort cT) (base _ class).
Local Definition semiringType : Semiring.type :=
  Semiring.Pack
    (sort cT)
    (Semiring.Class
       _ (Group.base _ (base _ class)) (semiring_mixin _ class)).
Local Definition group_semiringType : Semiring.type :=
  Semiring.Pack
    groupType
    (Semiring.Class
       _ (Group.base _ (base _ class)) (semiring_mixin _ class)).

End ClassOps.

(*
Module Exports.

Coercion sort : type >-> Sortclass.

Coercion monoidType : type >-> Monoid.type.
Canonical monoidType.
Coercion groupType : type >-> Group.type.
Canonical groupType.
Coercion semiringType : type >-> Semiring.type.
Canonical semiringType.
Canonical group_semiringType.

End Exports.
*)

End Ring.
(* Export Ring.Exports. *)

Coercion Ring.sort : Ring.type >-> Sortclass.

(******************************************************************************)

Module Inheritances.

Local Set Printing All.

(* Semiring *)

Fail Check (fun (A : Semiring.type) => @zero A).

Coercion Semiring.monoidType : Semiring.type >-> Monoid.type.

Check (fun (A : Semiring.type) => @zero A).

Fail Check (add zero one).

Canonical Semiring.monoidType. (* Monoid.sort _ = Semiring.sort _ *)

Check (add zero one).

(* Group *)

Fail Check (fun (A : Group.type) => @zero A).

Coercion Group.monoidType : Group.type >-> Monoid.type.

Check (fun (A : Group.type) => @zero A).

Fail Check (opp zero).

Canonical Group.monoidType. (* Monoid.sort _ = Group.sort _ *)

Check (opp zero).

(* Ring *)

Coercion Ring.monoidType : Ring.type >-> Monoid.type.
Canonical Ring.monoidType. (* Monoid.sort _ = Ring.sort _ *)
Coercion Ring.groupType : Ring.type >-> Group.type.
Canonical Ring.groupType. (* Group.sort _ = Ring.sort _ *)
Coercion Ring.semiringType : Ring.type >-> Semiring.type.
Canonical Ring.semiringType. (* Semiring.sort _ = Ring.sort _ *)

Fail Check (opp one).

Canonical Ring.group_semiringType. (* Semiring.sort _ = Group.sort _ *)

Check (opp one).

Print Canonical Projections.

End Inheritances.

(******************************************************************************)

(* `check_join t1 t2 tjoin` assert that the join of `t1` and `t2` is `tjoin`. *)
Tactic Notation "check_join"
       open_constr(t1) open_constr(t2) open_constr(tjoin) :=
  let rec fillargs t :=
    lazymatch type of t with
      | forall _, _ => let t' := open_constr:(t _) in fillargs t'
      | _ => t
    end
  in
  let t1 := fillargs t1 in
  let t2 := fillargs t2 in
  let tjoin := fillargs tjoin in
  let T1 := open_constr:(_ : t1) in
  let T2 := open_constr:(_ : t2) in
  match tt with
    | _ => unify ((id : t1 -> Type) T1) ((id : t2 -> Type) T2)
    | _ => fail "There is no join of" t1 "and" t2
  end;
  let Tjoin :=
    lazymatch T1 with
      _ (_ ?Tjoin) => Tjoin | _ ?Tjoin => Tjoin | ?Tjoin => Tjoin
    end
  in
  match tt with
    | _ => is_evar Tjoin
    | _ =>
      let Tjoin := eval simpl in (Tjoin : Type) in
      fail "The join of" t1 "and" t2 "is a concrete type" Tjoin
           "but is expected to be" tjoin
  end;
  let tjoin' := type of Tjoin in
  lazymatch tjoin' with
    | tjoin => idtac
    | _ => fail "The join of" t1 "and" t2 "is" tjoin'
                "but is expected to be" tjoin
  end.

(* The assertions generated by our tool: *)
Goal False.
check_join Group.type Group.type Group.type.
Fail check_join Group.type Monoid.type Group.type.
Fail check_join Group.type Ring.type Ring.type.
Fail check_join Group.type Semiring.type Ring.type.
Fail check_join Monoid.type Group.type Group.type.
check_join Monoid.type Monoid.type Monoid.type.
Fail check_join Monoid.type Ring.type Ring.type.
Fail check_join Monoid.type Semiring.type Semiring.type.
Fail check_join Ring.type Group.type Ring.type.
Fail check_join Ring.type Monoid.type Ring.type.
check_join Ring.type Ring.type Ring.type.
Fail check_join Ring.type Semiring.type Ring.type.
Fail check_join Semiring.type Group.type Ring.type.
Fail check_join Semiring.type Monoid.type Semiring.type.
Fail check_join Semiring.type Ring.type Ring.type.
check_join Semiring.type Semiring.type Semiring.type.
Abort.

Import Inheritances.

Goal False.
check_join Group.type Group.type Group.type.
check_join Group.type Monoid.type Group.type.
check_join Group.type Ring.type Ring.type.
check_join Group.type Semiring.type Ring.type.
check_join Monoid.type Group.type Group.type.
check_join Monoid.type Monoid.type Monoid.type.
check_join Monoid.type Ring.type Ring.type.
check_join Monoid.type Semiring.type Semiring.type.
check_join Ring.type Group.type Ring.type.
check_join Ring.type Monoid.type Ring.type.
check_join Ring.type Ring.type Ring.type.
check_join Ring.type Semiring.type Ring.type.
check_join Semiring.type Group.type Ring.type.
check_join Semiring.type Monoid.type Semiring.type.
check_join Semiring.type Ring.type Ring.type.
check_join Semiring.type Semiring.type Semiring.type.
Abort.

(******************************************************************************)

(* Z ring instance *)

Require Import ZArith.

Definition Z_monoid := Monoid.Mixin _ 0%Z Z.add Z.add_assoc Z.add_0_l.

Canonical Z_monoidType := Monoid.Pack Z (Monoid.Class _ Z_monoid).

Definition Z_semiring :=
  Semiring.Mixin
    _ 1%Z Z.mul Z.add_comm Z.mul_assoc Z.mul_1_l Z.mul_1_r
    Z.mul_add_distr_r Z.mul_add_distr_l Z.mul_0_l Z.mul_0_r.

Module wrong.

Local Set Printing All.

Goal False.
check_join Monoid.type Semiring.type Semiring.type.
check_join Semiring.type Monoid.type Semiring.type.
Abort.

(* A bad example of unification hint. *)
Local Canonical Z_semiringType :=
  Semiring.Pack Z_monoidType (Semiring.Class _ _ Z_semiring).
             (* ^^^^^^^^^^^^ This must be literally Z. *)

Print Canonical Projections.
(* Monoid.sort <- Semiring.sort ( Z_semiringType ) *)

Goal False.

(* Our unification hints solve `Monoid.sort _ = Semiring.sort _` correctly.   *)
check_join Monoid.type Semiring.type Semiring.type.

let t1 := open_constr:(_ : Monoid.type) in
let t2 := open_constr:(_ : Semiring.type) in
unify ((id : _ -> Type) t1) ((id : _ -> Type) t2);
idtac t1;
idtac t2.

(* But they don't behave the same for `Semiring.sort _ = Monoid.sort _`.      *)
Fail check_join Semiring.type Monoid.type Semiring.type.

let t1 := open_constr:(_ : Semiring.type) in
let t2 := open_constr:(_ : Monoid.type) in
unify ((id : _ -> Type) t1) ((id : _ -> Type) t2);
idtac t1;
idtac t2.

Abort.

End wrong.

Canonical Z_semiringType :=
  Semiring.Pack Z (Semiring.Class _ _ Z_semiring).

Definition Z_group := Group.Mixin _ Z.opp Z.add_opp_diag_l.

Canonical Z_groupType :=
  Group.Pack Z (Group.Class _ _ Z_group).

Canonical Z_ringType :=
  Ring.Pack Z (Ring.Class _ (Group.Class _ _ Z_group) Z_semiring).