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: Oct 13 2024 at 01:02 UTC