I'm trying to get the hang of HB, so I'm making experiments. I defined a new structure, `CmpSet`

and defined direct instances on `nat`

and `list A`

. Then I defined a pullback which enabled me to use `@length A`

to pull back the nat-CmpSet structure to a new listA-CmpSet, and I would like to prove it's actually the same structure ; but I don't know how to express it neatly, and I'm at loss at how to prove it.

The whole code is here, but perhaps that is enough:

```
(* annoying:
1. I'd like to write it with `cmp` pointing out which structure I want
2. using `(@length A)` instead of just `length` seems a bit awkward as the types looks pretty transparent
*)
Lemma coherent_cmp_on_list (A: Type) (l1 l2: list A) : iff (cmp_pullback (@length A) l1 l2) (cmp_list l1 l2).
Proof.
split.
revert l2. (* seems sensible *)
induction l1.
simpl.
auto.
unfold cmp_pullback.
unfold cmp. (* I want `length (a::l1) <= length l2`, and I don't know how to get it *)
Qed.
```

Notice that since I'm working on my skills, I'm not really interested in a complete proof of my case: I'm looking for hints on what I did wrong or pointers to examples where something similar is done.

I don't have time to play with your script, but the Pullback section seems wrong since the instance "key" is a variable.

Also the statement seems weird, don't you want to show `iff (cmp (length l1) (length l2)) (cmp l1 l2)`

?

@Enrico Tassi Sorry, I had missed your answer ; I don't know what you call " instance "key" ", so probably I did something wrong indeed. As for your suggestion, it means bypassing the pullback by making it explicit, so it's not what I wanted to try.

Last updated: May 28 2023 at 18:29 UTC