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
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: Dec 07 2023 at 09:01 UTC