Stream: math-comp users

Topic: how to prove symmetry of [pred x | p1 x == p2 x]?


view this post on Zulip Andrey Klaus (Nov 29 2021 at 06:00):

  T : eqType
  p1, p2 : pred T
  ============================
  [pred x | p1 x == p2 x] = [pred x | p2 x == p1 x]

I think about some kind of rewrite under but what kind the under equation do I need?

view this post on Zulip Enrico Tassi (Nov 29 2021 at 06:08):

If you state it with =1 then it is provable without axioms. A pred is just a function to bool, your goal is very strong in type theory.

view this post on Zulip Andrey Klaus (Nov 29 2021 at 10:28):

@Enrico Tassi , thank you very much.


Last updated: Mar 29 2024 at 15:02 UTC