NFI

Non Forgetful Inheritance is a very nasty problem which can arise if a hierarchy is badly designed and is very hard to pinpoint. HB is capable of detecting the problem and, unless the #[non_forgetful_inheritance] attribute is passed, it refuses to declare instances which break the invariant. In some rare cases it may make sense to break the invariant locally, hence the reason of existance for the attribute.

This problem was studied in this paper in the context of functional analysis, here we describe it in a simpler, but more artificial, setting.

From HB Require Import structures.
Require Import ssreflect ssrfun ssrbool.

Module BadInheritance.

HB.mixin Record HasMul T := {
  mul : T -> T -> T;
}.
HB.structure Definition Mul := { T of HasMul T }.

HB.mixin Record HasSq T := {
  sq : T -> T;
}.
HB.structure Definition Sq := { T of HasSq T }.

(* We need a functorial construction (a container)
   which preserves both structures. The simplest one is the option type. *)
Definition option_mul {T : Mul.type} (o1 o2 : option T) : option T :=
  match o1, o2 with
  | Some n, Some m => Some (mul n m)
  | _, _ => None
  end.
HB.instance Definition _ (T : Mul.type) := HasMul.Build (option T) option_mul.

Definition option_square {T : Sq.type} (o : option T) : option T :=
  match o with
  | Some n => Some (sq n)
  | None => None
  end.
HB.instance Definition _ (T : Sq.type) := HasSq.Build (option T) option_square.

(* Now we mix the two unrelated structures by building Sq out of Mul.

               *** This breaks Non Forgetful Inheritance ***

*)
#[non_forgetful_inheritance]
HB.instance Definition _ (T : Mul.type) := HasSq.Build T (fun x => mul x x).

(* As we expect we can proved this (by reflexivity) *)
Lemma sq_mul (V : Mul.type) (v : V) : sq v = mul v v.
Proof. by reflexivity. Qed.

Lemma problem (W : Mul.type) (w : option W) : sq w = mul w w.
Proof.
Fail reflexivity. (* What? It used to work! *)
Fail rewrite sq_mul. (* Lemmas don't cross the container either! *)
(* Let's investigate *)
rewrite /mul/= /sq/=.
(* As we expect, we are on the option type. In the LHS it is the Sq built using
   the NFI instance
 
     option_square w = option_mul w w
*)
rewrite /option_mul/=.
rewrite /option_square/sq/=.
congr (match w with Some n => _ | None => None end).
(* The branches for Some differ, since w is a variable,
   they don't compare as equal

      (fun n : W => Some (mul n n)) =
      (fun n : W => match w with
                    | Some m => Some (mul n m)
                    | None => None
                    end)
*)
Abort.

End BadInheritance.

Since the structures Mul and Sq are somewhat related, since the operations of the two are expected to validate a common law, we should put them in the same hierarchy.

From HB Require Import structures.
Require Import ssreflect ssrfun ssrbool.

Module GoodInheritance.

HB.mixin Record HasMul T := {
  mul : T -> T -> T;
}.
HB.structure Definition Mul := { T of HasMul T }.

HB.mixin Record HasSq T of Mul T := {
  sq : T -> T;
  sq_mul : forall x, sq x = mul x x;
}.
HB.structure Definition Sq := { T of HasSq T & Mul T }.

Definition option_mul {T : Mul.type} (o1 o2 : option T) : option T :=
  match o1, o2 with
  | Some n, Some m => Some (mul n m)
  | _, _ => None
  end.
HB.instance Definition _ (T : Mul.type) := HasMul.Build (option T) option_mul.

Definition option_square {T : Sq.type} (o : option T) : option T :=
  match o with
  | Some n => Some (sq n)
  | None => None
  end.
Lemma option_sq_mul {T : Sq.type} (o : option T) : option_square o = mul o o.
Proof. by rewrite /option_square; case: o => [x|//]; rewrite sq_mul. Qed.
HB.instance Definition _ (T : Sq.type) := HasSq.Build (option T) option_square option_sq_mul.

Lemma problem (W : Sq.type) (w : option W) : sq w = mul w w.
Proof. by rewrite sq_mul. Qed.

End GoodInheritance.

Example in Dioid

We practically encountered the issue when developing the Dioid library

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice order.

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

Declare Scope dioid_scope.
Delimit Scope dioid_scope with D.
Local Open Scope dioid_scope.

Import Order.Theory.

HB.mixin Record IsSemiRing R := {
  zero : R;
  one : R;
  add : R -> R -> R;
  mul : R -> R -> R;
  adddA : associative add;
  adddC : commutative add;
  add0d : left_id zero add;
  muldA : associative mul;
  mul1d : left_id one mul;
  muld1 : right_id one mul;
  muldDl : left_distributive mul add;
  muldDr : right_distributive mul add;
  mul0d : left_zero zero mul;
  muld0 : right_zero zero mul;
}.

HB.structure Definition SemiRing := { R of Choice R & IsSemiRing R }.

Bind Scope dioid_scope with SemiRing.sort.
Notation "0" := zero : dioid_scope.
Infix "+" := (@add _) : dioid_scope.

(* A dioid is an idempotent semiring. *)
HB.mixin Record SemiRing_IsDioid D of SemiRing D := {
  adddd : @idempotent D add;
}.

HB.structure Definition Dioid := { D of SemiRing_IsDioid D & SemiRing D }.

(* It is equipped with a canonical (partial) order : a <= b when a + b = b *)
Section DioidPOrder.

Variable D : Dioid.type.

Implicit Type a b : D.

Definition le_dioid a b := a + b == b.

Definition lt_dioid a b := (b != a) && le_dioid a b.

Lemma lt_def_dioid a b : lt_dioid a b = (b != a) && le_dioid a b.
Proof. by []. Qed.
Lemma le_refl_dioid : reflexive le_dioid.
Proof. by move=> a; rewrite /le_dioid adddd. Qed.

Lemma le_anti_dioid : antisymmetric le_dioid.
Proof.
by move=> a b /andP[]; rewrite /le => /eqP ? /eqP; rewrite adddC => <-.
Qed.

Lemma le_trans_dioid : transitive le_dioid.
Proof.
move=> a b c; rewrite /le_dioid => /eqP H /eqP <-.
by rewrite -[in X in _ == X]H adddA.
Qed.

Fact dioid_display : unit. Proof. by []. Qed.

#[non_forgetful_inheritance]
HB.instance Definition _ := Order.IsPOrdered.Build dioid_display D
  lt_def_dioid le_refl_dioid le_anti_dioid le_trans_dioid.

End DioidPOrder.

However, in the common case where the base type of a dioid has already an order, the above is creating a new one, often equal but not convertible. To fix the issue, we include the POrder structure in the Dioid structure.

(* same code down to the SemiRing structure *)

Fact dioid_display : unit. Proof. by []. Qed.

HB.mixin Record SemiRing_IsDioid D
         of SemiRing D & Order.POrder dioid_display D := {
  adddd : @idempotent D add;
  le_def : forall (a b : D), (a <= b)%O = (a + b == b)
}.

HB.structure Definition Dioid :=
  { D of SemiRing_IsDioid D & SemiRing D & Order.POrder dioid_display D }.

(* In case D has no predefined order, we can use a factory to build                                                                                                                       
   the order and the dioid structures all at once. *)
HB.factory Record Choice_IsDioid D of Choice D := {
  zero : D;
  one : D;
  add : D -> D -> D;
  mul : D -> D -> D;
  adddA : associative add;
  adddC : commutative add;
  add0d : left_id zero add;
  adddd : idempotent add;
  muldA : associative mul;
  mul1d : left_id one mul;
  muld1 : right_id one mul;
  muldDl : left_distributive mul add;
  muldDr : right_distributive mul add;
  mul0d : left_zero zero mul;
  muld0 : right_zero zero mul;
}.

HB.builders Context D of Choice_IsDioid D.

  HB.instance Definition _ := IsSemiRing.Build D
    adddA adddC add0d muldA mul1d muld1 muldDl muldDr mul0d muld0.

  Definition le_dioid a b := add a b == b :> [the Choice.type of D].

  Definition lt_dioid a b := (b != a :> [the Choice.type of D]) && le_dioid a b.

  Lemma lt_def_dioid a b : lt_dioid a b = (b != a) && le_dioid a b.
  Proof. by []. Qed.

  Lemma le_refl_dioid : reflexive le_dioid.
  Proof. by move=> a; rewrite /le_dioid adddd. Qed.

  Lemma le_anti_dioid : antisymmetric le_dioid.
  Proof.
  by move=> a b /andP[]; rewrite /le => /eqP ? /eqP; rewrite adddC => <-.
  Qed.

  Lemma le_trans_dioid : transitive le_dioid.
  Proof.
  move=> a b c; rewrite /le_dioid => /eqP H /eqP <-.
  by rewrite -[in X in _ == X]H adddA.
  Qed.

  HB.instance Definition _ := Order.IsPOrdered.Build dioid_display D
    lt_def_dioid le_refl_dioid le_anti_dioid le_trans_dioid.

  Lemma le_def (a b : D) : (a <= b)%O = (add a b == b).
  Proof. by []. Qed.

  HB.instance Definition _ := SemiRing_IsDioid.Build D adddd le_def.

HB.end.