I'm trying to learn HB by trying to apply it to toy situations ; I do manage to get along, but I'm not 100% satisfied with what I get, so perhaps I can get some hints to improve matters:

```
Require Import List Reals ZArith.
From HB Require Import structures.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* experiments learning HB, first round *)
(* first experiment: a naive structure with a set endowed with an involution, with
some trivial instances and a stupid theorem *)
HB.mixin Record Involutive_Type M := {
inv: M -> M;
self_inv: forall m, inv (inv m) = m;
}.
HB.structure Definition Involutive := { M of Involutive_Type M }.
HB.instance Definition Z_involutive := Involutive_Type.Build Z Z.opp_involutive.
HB.instance Definition R_involutive := Involutive_Type.Build R Ropp_involutive.
Lemma thrice_once (M: Involutive.type): forall (m: M), inv (inv (inv m)) = inv m.
Proof.
intro m.
apply self_inv.
Qed.
(* second experiment: a set with a reflexive&transitive relation, trivial instances and
a less trivial one *)
HB.mixin Record is_CmpSet M := {
cmp: M -> M -> Prop;
cmp_reflexive: forall m, cmp m m;
cmp_transitive: forall m n p, cmp m n -> cmp n p -> cmp m p;
}.
HB.structure Definition CmpSet := { M of is_CmpSet M}.
HB.instance Definition nat_cmp := is_CmpSet.Build nat le_refl le_trans.
HB.instance Definition N_cmp := is_CmpSet.Build N N.le_refl N.le_trans.
HB.instance Definition Z_cmp := is_CmpSet.Build Z Z.le_refl Z.le_trans.
Fixpoint cmp_list {A} (l1 l2: list A) := (* it's just a length comparison *)
match l1 with
| nil => True
| h1 :: t1 => match l2 with | nil => False | h2 :: t2 => cmp_list t1 t2 end
end.
Lemma cmp_list_reflexive {A}: forall (l: list A), cmp_list l l.
Proof.
intro l.
induction l.
unfold cmp_list.
auto.
unfold cmp_list.
auto.
Qed.
Lemma cmp_list_transitive {A}: forall (l1 l2 l3: list A), cmp_list l1 l2 -> cmp_list l2 l3 -> cmp_list l1 l3.
Proof.
intros l1.
induction l1.
auto.
induction l2.
unfold cmp_list at 1 2.
intro l3.
apply (False_ind (True -> cmp_list (a::l1) l3)). (* FIXME: why so complex? *)
induction l3.
simpl.
auto.
simpl.
apply IHl1.
Qed.
HB.instance Definition list_cmp {A} := is_CmpSet.Build (list A) cmp_list_reflexive cmp_list_transitive.
(* third experiment: push the previous one further, trying to play the "structure transfert" game
with a pullback trick *)
Section Pullback.
Variable Source: Type.
Variable Destination: CmpSet.type.
Variable f: Source -> Destination.
Definition cmp_pullback (s1 s2: Source) := cmp (f s1) (f s2).
Lemma cmp_pullback_reflexive: forall s, cmp_pullback s s.
Proof.
intro s.
unfold cmp_pullback.
apply cmp_reflexive.
Qed.
Lemma cmp_pullback_transitive: forall s1 s2 s3, cmp_pullback s1 s2 -> cmp_pullback s2 s3 -> cmp_pullback s1 s3.
Proof.
intros s1 s2 s3.
unfold cmp_pullback.
apply cmp_transitive.
Qed.
HB.instance Definition pullback_cmp :=
is_CmpSet.Build Source cmp_pullback_reflexive cmp_pullback_transitive.
End Pullback.
Check (pullback_cmp (@length _)).
(* fourth experiment: can I express that pulling back `length` from the
integers to the lists will give me the same comparison? and then:
can I prove it? *)
(* FIXME:
1. I'd like to write it with `cmp` pointing out which structure I want, not by using
explicit `cmp_list` and `cmp_pullback`
2. Using `(@length A)` instead of just `length` seems a bit awkward ; indeed length seems generic,
but since I declared the list types, the fact that it's *this* length seems pretty explicit!
3. The proof I wrote is pretty long... the fact I wanted to use bare Coq and not SSR might not have
helped, but I wonder if I didn't miss something nice.
*)
Lemma coherent_cmp_on_list (A: Type) (l1 l2: list A):
iff (cmp_pullback (@length A) l1 l2) (cmp_list l1 l2).
Proof.
split.
(* first implication *)
revert l2.
induction l1.
simpl.
auto.
induction l2.
unfold cmp_pullback.
unfold cmp.
simpl.
apply Nat.nle_succ_0.
unfold cmp_pullback.
unfold cmp.
simpl.
intro lel1l2.
apply le_S_n in lel1l2.
apply IHl1.
unfold cmp_pullback.
unfold cmp.
auto.
(* second implication *)
revert l2.
induction l1.
unfold cmp_pullback.
unfold cmp.
simpl.
intros l2 T.
apply Nat.le_0_l.
induction l2.
unfold cmp_pullback.
unfold cmp.
simpl.
apply False_ind.
unfold cmp_pullback.
unfold cmp.
simpl.
intro cmpl1l2.
apply le_n_S.
apply IHl1.
exact cmpl1l2.
Qed.
```

Last updated: Jan 29 2023 at 16:02 UTC