SetoidRewrite: various cleanups and simplifications

[jdchristensen]

I'm starting to experiment with SetoidRewrite, and while reading through the file I made some simplifications and cleanups.

I removed the comments about requiring the standard library, since that's no longer the case.

I do get dune warnings saying

Warning: in file SetoidRewrite.v, library Init.Tactics is required
         from root Stdlib and has not been found in the loadpath!
         [module-not-found,filesystem,default]
Warning: in file SetoidRewrite.v, library Setoids.Setoid is required
         from root Stdlib and has not been found in the loadpath!
         [module-not-found,filesystem,default]

but the build is still successful. @Alizter , any idea what's up with these?

I don't know anything about the setoid rewriting stuff, but I was surprised that we have to provide lots of proofs that are just composites of transitivity and symmetry. Can't we just declare that these relations are transitive and symmetric?

@patrick-nicodemus Can you review this?

[Alizter]

Those warnings are not from dune but from Coqc. If you pass --always-display-command-line to dune it will output an shell-approximation of what it ran to get that output. That should allow you to see exactly which rocq command and flags were passed.

_build/log also contains similar information. The issue here is likely that dune is passing -boot everywhere, and that causes endless confusion for Coq. IIRC this was fixed in 9.1, but I definitely haven't checked.

[jdchristensen]

@Alizter Ah, the warnings are from coqdep, not coqc. I'm using Rocq Prover, version 9.1.0, without the standard library, and I get those warnings with the existing version of SetoidRewrite.v as well. So whatever is causing this has nothing to do with this PR. For the record, here's what is in _build/log:

$ (cd _build/default/contrib && /home/jdc/scratchy/.opam/9.1-4.14.2/bin/coqdep -boot 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/btauto 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/cc 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/cc_core 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/derive 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/extraction 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/firstorder 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/firstorder_core 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/funind 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/ltac 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/ltac2 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/ltac2_ltac1 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/micromega 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/micromega_core 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/nsatz 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/nsatz_core 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/number_string_notation 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/ring 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/rtauto 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/ssreflect 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/ssrmatching 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/tauto 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/tutorial/p0 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/tutorial/p1 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/tutorial/p2 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/tutorial/p3 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/tutorial/p4 
-I /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/../rocq-runtime/plugins/zify 
-R /home/jdc/scratchy/.opam/9.1-4.14.2/lib/coq/theories Coq 
-Q ../theories HoTT 
-R . HoTT.Contrib 
-dyndep opt -vos SetoidRewrite.v HoTTBookExercises.v HoTTBook.v) > _build/default/contrib/.HoTT.theory.d
> Warning: in file SetoidRewrite.v, library Init.Tactics is required
>          from root Stdlib and has not been found in the loadpath!
>          [module-not-found,filesystem,default]
> Warning: in file SetoidRewrite.v, library Setoids.Setoid is required
>          from root Stdlib and has not been found in the loadpath!
>          [module-not-found,filesystem,default]

[jdchristensen]

@patrick-nicodemus I think the changes I made here are pretty straightforward, so if you can give it a quick skim, that would be great. Thanks!

[patrick-nicodemus]

Okay, I will review it

[jdchristensen]

@patrick-nicodemus I just added a few more clarifications.

[patrick-nicodemus]

Ok. I will review this this morning.

[patrick-nicodemus]

Okay. Thanks for your patience.

I only noticed one thing, the string CoqDoc appears in a comment on line 361 in file Cubical/PathSquare.v
(* Dependent path product definition of [PathSquare] CoqDoc *)
That seems like a mistake.

Looks okay other than that.

[jdchristensen]

I only noticed one thing, the string CoqDoc appears in a comment on line 361 in file Cubical/PathSquare.v

This PR only changed one file, SetoidRewrite.v, so I'm not sure why you are commenting on PathSquare.v. Were you looking at the correct PR when reviewing? (Also, that typo was just fixed in #2328.)

[patrick-nicodemus]

I only noticed one thing, the string CoqDoc appears in a comment on line 361 in file Cubical/PathSquare.v

This PR only changed one file, SetoidRewrite.v, so I'm not sure why you are commenting on PathSquare.v. Were you looking at the correct PR when reviewing? (Also, that typo was just fixed in #2328.)

I ran git diff master instead of git diff $(git merge-base master setoid-rewrite) setoid-rewrite when reading the changes, my mistake. Okay. Everything looks good then.

[jdchristensen]

Ah, for future reference, you can just look at the "Files Changed" tab on this github page. Thanks for the review!