136 lines
3.5 KiB
Coq
136 lines
3.5 KiB
Coq
From HB Require Import structures.
|
||
From mathcomp Require Import all_ssreflect.
|
||
|
||
Reserved Notation "⊥" (at level 20).
|
||
Reserved Notation "⊤" (at level 20).
|
||
Reserved Notation "⊓" (at level 50).
|
||
Reserved Notation "⊔" (at level 50).
|
||
(*𝟘 𝟙 𝟎 𝟏*)
|
||
|
||
HB.mixin Record IsLattice A := {
|
||
meet: A -> A -> A;
|
||
join: A -> A -> A;
|
||
|
||
joinC: commutative join;
|
||
meetC: commutative meet;
|
||
joinA: associative join;
|
||
meetA: associative meet;
|
||
|
||
(* Absorption laws *)
|
||
abs_jm: forall a b: A,
|
||
join a (meet a b) = a;
|
||
abs_mj: forall a b: A,
|
||
meet a (join a b) = a;
|
||
}.
|
||
HB.structure Definition Lattice := { A of IsLattice A }.
|
||
|
||
Section LatticeLemmas.
|
||
Infix "⊓" := meet (at level 50).
|
||
Infix "⊔" := join (at level 50).
|
||
|
||
Variable L: Lattice.type.
|
||
|
||
Lemma joinb: idempotent (@join L).
|
||
Proof.
|
||
rewrite /idempotent => x.
|
||
rewrite -{2}(abs_mj x x).
|
||
by rewrite abs_jm.
|
||
Qed.
|
||
|
||
Lemma meetb: idempotent (@meet L).
|
||
Proof.
|
||
rewrite /idempotent => x.
|
||
rewrite -{2}(abs_jm x x).
|
||
by rewrite abs_mj.
|
||
Qed.
|
||
End LatticeLemmas.
|
||
|
||
Print right_id.
|
||
|
||
HB.mixin Record IsBoundedLattice A of IsLattice A := {
|
||
bot: A;
|
||
top: A;
|
||
top_meet: right_id top meet;
|
||
bot_join: right_id bot join;
|
||
}.
|
||
HB.structure Definition BoundedLattice := { A of IsBoundedLattice A }.
|
||
|
||
Section BoundedLatticeLemmas.
|
||
Notation "⊥" := bot.
|
||
Notation "⊤" := top.
|
||
|
||
Variable L: BoundedLattice.type.
|
||
End BoundedLatticeLemmas.
|
||
|
||
Module b3Lattice.
|
||
Definition t: Type := option bool.
|
||
Definition top: t := Some true.
|
||
Definition bot: t := Some false.
|
||
|
||
Definition meet (a b: t): t :=
|
||
match a, b with
|
||
| Some false, _ => Some false
|
||
| _, Some false => Some false
|
||
| None, _ => None
|
||
| Some true, Some true => Some true
|
||
| Some true, None => None
|
||
end.
|
||
|
||
Definition join (a b: t): t :=
|
||
match a, b with
|
||
| Some true, _ => Some true
|
||
| _, Some true => Some true
|
||
| None, None => None
|
||
| Some false, _ => b
|
||
| _, Some false => a
|
||
end.
|
||
|
||
Lemma joinC: commutative join.
|
||
Proof. by do !case. Qed.
|
||
Lemma joinA: associative join.
|
||
Proof. by do !case. Qed.
|
||
Lemma meetC: commutative meet.
|
||
Proof. by do !case. Qed.
|
||
Lemma meetA: associative meet.
|
||
Proof. by do !case. Qed.
|
||
|
||
Lemma abs_jm: forall a b: t,
|
||
join a (meet a b) = a.
|
||
Proof. by do !case. Qed.
|
||
Lemma abs_mj: forall a b: t,
|
||
meet a (join a b) = a.
|
||
Proof. by do !case. Qed.
|
||
|
||
Lemma top_meet: right_id top meet.
|
||
Proof. by do !case. Qed.
|
||
Lemma bot_join: right_id bot join.
|
||
Proof. by do !case. Qed.
|
||
End b3Lattice.
|
||
|
||
HB.instance Definition ob_Lat := IsLattice.Build _
|
||
b3Lattice.meet b3Lattice.join
|
||
b3Lattice.joinC b3Lattice.meetC
|
||
b3Lattice.joinA b3Lattice.meetA
|
||
b3Lattice.abs_jm b3Lattice.abs_mj.
|
||
|
||
HB.instance Definition ob_BLat := IsBoundedLattice.Build _
|
||
b3Lattice.bot b3Lattice.top
|
||
b3Lattice.top_meet b3Lattice.bot_join.
|
||
(*
|
||
ob_BLat is defined
|
||
|
||
non forgetful inheritance detected.
|
||
You have two solutions:
|
||
1. (Best practice) Reorganize your hierarchy to make init_IsBoundedLattice
|
||
depend on init_Lattice. See the paper "Competing inheritance paths in
|
||
dependent type theory" (https://hal.inria.fr/hal-02463336) for more
|
||
explanations
|
||
2. Use the attribute #[non_forgetful_inheritance] to disable this check.
|
||
We strongly advise you encapsulate this instance inside a module,
|
||
in order to isolate it from the rest of the code, and to be able
|
||
to import it on demand. See the above paper and the file
|
||
https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v
|
||
to witness devastating effects.
|
||
[HB.non-forgetful-inheritance,HB]
|
||
*)
|