Chris Hughes (Aug 05 2018 at 12:13):
What's the easiest way to define a partial function on a quotient type, where the proof that it is well defined depends on the predicate? I tried
quotient.hrec_on but whilst I can define the function, it's hard to prove things about it due to
motive is not type correct errors. For context, I'm experimenting with defining the signature of a permutation as being derived from this.
def sign_aux2 : list α → perm α → units ℤ |  f := 1 | (x::l) f := if f x = x then sign_aux2 l f else -sign_aux2 l (swap x (f x) * f)
I plan to use the list underneath
finset.univ, and prove it doesn't depend on the order of the list.
Chris Hughes (Aug 05 2018 at 12:13):
The problem is that the list has to contain everything of the type in order to prove the
Reid Barton (Aug 05 2018 at 12:24):
pfun can be helpful
Reid Barton (Aug 05 2018 at 12:25):
though maybe I don't quite understand what you're doing yet
Reid Barton (Aug 05 2018 at 12:28):
I guess it's okay. The strategy is to define a (total) function to
roption (units \Z), which sends all "bad" elements to
Reid Barton (Aug 05 2018 at 12:33):
You can also define a dependent function which takes the needed hypothesis as an argument using
quotient.rec, but I found that approach to be really difficult when I had to do something like this.
Chris Hughes (Aug 05 2018 at 12:38):
Good plan. Thanks.
Kevin Buzzard (Aug 05 2018 at 12:51):
Speaking as someone whose job it is to teach students what the signature of a permutation is, I'm pleased about how it's going this year. On the other hand speaking as someone who is well aware that these notions have been around for ages, I can't help but feeling that the issues my students are running into are ones which will already have been solved. Are there already 23 different implementations of signature of a permutation in Coq, for example? I kind-of suspect that the questions we've been running into since we started thinking about this are ones which will have been seen many times before...
Chris Hughes (Aug 05 2018 at 17:35):
I think looking at coq is good for general questions like which proof should I use, but not so good for questions like this.
Reid Barton (Aug 05 2018 at 17:43):
By the way, I was wondering whether it would be possible to define the sign of a permutation as the determinant of the corresponding linear transformation on (say) Q^n, and define the latter in terms of the nth exterior power.
But, in order to show the nth exterior power is not zero, I think you end up needing the fact that a composition of an odd number of transpositions cannot be the identity anyways. Unless there is an even fancier approach which I missed?
Kenny Lau (Aug 05 2018 at 17:44):
Chris (and I independently) defined sign of permutation using number of inversions
Chris Hughes (Aug 05 2018 at 17:52):
I changed it to basically what I posted above
Reid Barton (Aug 05 2018 at 17:52):
Right, but if you were given the fact that was one-dimensional, then you could get signs of permutations (including that it is a group homomorphism) for free.
Reid Barton (Aug 05 2018 at 17:53):
Or there are other facts you could start from, like (or ) having two components
Kevin Buzzard (Aug 05 2018 at 18:40):
To prove that the n'th exterior power is not zero I guess you have to explicitly construct some alternating form? If you could come up with some definition of det which had the property that switching two rows changed the sign etc then you might be in good shape, but the only way I know how to do this is to come up with the definition of det, and the definition of det I know involves signatures. I half-suspect that there were some comments about this in my UG notes, in my office, I'll try and remember to dig them up when I get back to London.
Last updated: May 10 2021 at 23:11 UTC