1
$\begingroup$

Say that I have a list structure and a lemma:

my_list :  BoolSet U -> Type

Lemma union_comm (A B : BoolSet U) :
  Union A B = Union B A
Proof.
...
Qed.

Lemma my_list_eq_union (A B : BoolSet U) :
  my_list (Union A B) = my_list (Union B A).
Proof.
  rewrite union_comm; reflexivity.
Qed.

This lemma states that the two types are equal. In a function expecting a type my_list (Union A B) I would like to be able to pass a my_list (Union B A). I am able to do this by using the lemma above to create a mapping map {A B : BoolSet U} (m : my_list (Union A B)) : my_list (Union B A). from one type to the other. However, this means that my term is wrapped in this function mapping it to the correct type. This makes it hard to work with in proofs when I want to unfold it. I tried defining a coercion, but this is simply an automatic application of the mapping.

Is there a better way to use one type instead of the other when you can show their equality?

$\endgroup$
1
  • $\begingroup$ What specifically is my_list and Union? It is plausible that you should replace equality of types with equivalence of types, in which case, and then also replace equality of functions with pointwise equality. More context would help, and especially actual working code. $\endgroup$ Apr 27, 2023 at 20:43

1 Answer 1

1
$\begingroup$

Without more context, I would say that you are doing things in the only possible way: the only way to use propositional equality is transport, which in your case corresponds to the function map.

If you want to avoid this problem, you will have to alter code in other places, typically find a way to have the function(s) to which you pass map m take m instead.

$\endgroup$
2
  • $\begingroup$ Thank you, at least I know I'm not missing something obvious! The context I am working in is that I have sets of these my_lists defined as: Definition my_b (E : BoolSet U) := my_list E -> Prop. If I have a 'b1 : my_b E1` and a b2 : my_b E2, I can compose these comp b1 b2 into a my_b Union E1 E2, but I can also compose them as comp b2 b1 into a my_b Union E2 E1. I want to show this composition operator is commutative, so that comp b1 b2= comp b2 b1, but then I run into this issue. I think I will work with the mapping for now. $\endgroup$ Apr 27, 2023 at 9:52
  • $\begingroup$ So the baseline of the issue is that your BoolSet should represent (multi)sets, and you want associativity of union to be definitional rather than propositional? In this case, indeed there is no easy solution: Coq does not provide the possibility to define a datatype of such "strict" sets. $\endgroup$ May 3, 2023 at 10:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.