search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.26k stars 192 forks source link

better looking terms in presentation test #2031

Closed Alizter closed 3 months ago

Alizter commented 4 months ago

Previously these were harder to read. They are still not so easy, but at least a bit clearer.

Check ⟨ x | x * x * x , -x ⟩.

Build_Finite_GroupPresentation 1 2
  (fscons
  ((fun x : FreeGroup (Fin 1) => x * x * x : FreeGroup (Fin 1))
  ((freegroup_in o fin_nat) 0%nat))
  (fscons
  ((fun x : FreeGroup (Fin 1) => - x : FreeGroup (Fin 1)) ((freegroup_in o fin_nat) 0%nat))
  fsnil))
     : GroupPresentation
Check ⟨ x , y | x * y ,  x * y * x , x * (-y) * x * x * x⟩.

Build_Finite_GroupPresentation 2 3
  (fscons
  ((fun x y : FreeGroup (Fin 2) => x * y : FreeGroup (Fin 2))
  ((freegroup_in o fin_nat) 0%nat) ((freegroup_in o fin_nat) 1%nat))
  (fscons
  ((fun x y : FreeGroup (Fin 2) => x * y * x : FreeGroup (Fin 2))
  ((freegroup_in o fin_nat) 0%nat) ((freegroup_in o fin_nat) 1%nat))
  (fscons
  ((fun x y : FreeGroup (Fin 2) => x * - y * x * x * x : FreeGroup (Fin 2))
  ((freegroup_in o fin_nat) 0%nat) ((freegroup_in o fin_nat) 1%nat))
  fsnil)))
     : GroupPresentation
Check ⟨ x , y , z | x * y * z , x * -z , x * y⟩.

Build_Finite_GroupPresentation 3 3
  (fscons
  ((fun x y z : FreeGroup (Fin 3) => x * y * z : FreeGroup (Fin 3))
  ((freegroup_in o fin_nat) 0%nat) ((freegroup_in o fin_nat) 1%nat)
  ((freegroup_in o fin_nat) 2%nat))
  (fscons
  ((fun x _ z : FreeGroup (Fin 3) => x * - z : FreeGroup (Fin 3))
  ((freegroup_in o fin_nat) 0%nat) ((freegroup_in o fin_nat) 1%nat)
  ((freegroup_in o fin_nat) 2%nat))
  (fscons
  ((fun x y _ : FreeGroup (Fin 3) => x * y : FreeGroup (Fin 3))
  ((freegroup_in o fin_nat) 0%nat) ((freegroup_in o fin_nat) 1%nat)
  ((freegroup_in o fin_nat) 2%nat))
  fsnil)))
     : GroupPresentation
jdchristensen commented 3 months ago

Can you explain a bit more? Is the only change the Require line? Does this enable some notation or something like that? How did the terms look before the change? Can they be beta reduced? They look pretty complicated now.

Alizter commented 3 months ago

@jdchristensen The only change is the imports so that the terms a bit easier to read. Before they were much longer.

Alizter commented 3 months ago

Anyway not an important change.

jdchristensen commented 3 months ago

Ok, I now understand. All that is happening is that the names are no longer qualified, but that's a good thing. So I think we should go ahead with this, and should also change the other require line to include FreeGroup. (In my tests, I get FreeGroup.FreeGroup, while your example output only shows FreeGroup.)

Alizter commented 3 months ago

@jdchristensen I had some issues with the require when I first pushed this since I was lazy and didn't fully qualify some names, which meant coqdep was getting confused about the test vs theories names and causing dependency cycles. I fixed that issue, but it looks like a dropped FreeGroup as you spotted. Now I've added that back in and this is good to go.