Stream: Hierarchy Builder devs & users

Topic: Comparing two structures of the same type

view this post on Zulip Julien Puydt (Sep 27 2022 at 07:26):

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).
revert l2. (* seems sensible *)
induction l1.
unfold cmp_pullback.
unfold cmp. (* I want `length (a::l1) <= length l2`, and I don't know how to get it *)

view this post on Zulip Julien Puydt (Sep 27 2022 at 07:34):

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.

view this post on Zulip Enrico Tassi (Sep 27 2022 at 08:16):

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)?

view this post on Zulip Julien Puydt (Oct 11 2022 at 15:30):

@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: Jul 24 2024 at 12:02 UTC