Convert 2nd part of rewriting chapter to prodn

[jfehrle]

Fixes: #13803

[Zimmi48]

The introduction should probably refer to the Eval @red_expr in command (and possibly also the Eval @red_expr in construct in Definition and the eval @red_expr in Ltac-construct) as other ways of applying these reduction strategies.

[Zimmi48]

In addition to my previous comments about moving the section "Controlling the reduction strategies and the conversion algorithm" here and referring to the various constructs that use the red_expr syntax in the introduction, I also think that the "Conversion rules" section of the "Core language" chapter should get some reference to this section in its introduction.

[jfehrle]

It would be nice to have a bit of text in the introduction describing the differences between the various conversion tactics and when to use them. Or we could add a sentence covering that to each tactic.

[jfehrle]

What do you think about pulling these sections into this chapter since they relate to equalities?

https://coq.inria.fr/distrib/V8.12.2/refman/proof-engine/tactics.html#equality
https://coq.inria.fr/distrib/V8.12.2/refman/proof-engine/tactics.html#equality-and-inductive-sets

[jfehrle]

Updated.

[jfehrle]

What about forall {* @binder }, T then?

Is the forall optional?

[Zimmi48]

Is the forall optional?

Yes. And it's the same thing for the argument to rewrite.

What do you think about pulling these sections into this chapter since they relate to equalities?

https://coq.inria.fr/distrib/V8.12.2/refman/proof-engine/tactics.html#equality
https://coq.inria.fr/distrib/V8.12.2/refman/proof-engine/tactics.html#equality-and-inductive-sets

With the new chapter title, this would make sense. But then we should rename the file to equality.rst. (Note: if we do the renaming, then we should introduce an HTML redirection. See #12330 for examples.)

It would be nice to have a bit of text in the introduction describing the differences between the various conversion tactics and when to use them.

Yes, you can maybe mention that simpl and cbn are "clever" tactics to get readable results, lazy and cbv can be used to perform precise reduction steps, and that vm_compute and native_compute are performance-oriented.

[JasonGross]

Not just the goal, but also the context, if so specified by @occurences.

[Zimmi48]

Goal can sometimes designate the goal + its context: https://coq.gitlab.io/-/coq/-/jobs/1062149393/artifacts/_install_ci/share/doc/coq/sphinx/html/proofs/writing-proofs/proof-mode.html#term-goal

Up to @jfehrle to decide whether this one should stay as is or be reworded.

[jfehrle]

Updated.

[jfehrle]

Updated. The "constant" and "body" changes are in a separate commit. I eyeballed them and removed some silly ones, e.g. uses of :term: in section titles and error messages, but I didn't try to understand the meaning of each use--I think you're better situated to do that. Please those that should be reversed.

[Zimmi48]

It's taking me a huge time reviewing the glossary term usages and it's not even for a huge gain, as this could be done incrementally too. So I'll stop there. I suggest you take my suggestions into account for the files I have reviewed (the ones in language/, practical-tools/ and addendum/) and drop the changes to the rest. Also, the rest of the PR is basically ready, so you may squash the review commits.

[Zimmi48]

Why did you change the order? I preferred the previous one.

[jfehrle]

I made it match the order of the text below. The : case is the most common/basic case, right? While <: and <:: are specialized. And we lack an explanation for :>.

WDYT?

[JasonGross]

I've never seen :> used, and while it parses, it does not seem to leave evidence in the term (at least not any printed evidence). Is it a no-op? I suspect it should be removed....

[Zimmi48]

Oh right, actually I prefer the new order. I just wanted the undocumented :> to be last.

[Zimmi48]

:> is CastCoerce. It looks like it was introduced in 2007 by @mattam82. The only example use I found is:

(** Coerces objects before comparing them *)
Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).

introduced at that time in a contrib.

I don't have an example of what it does.

[jfehrle]

Updated. Just a couple things left to tweak, see above.

[Zimmi48]

I didn't re-review anything, just trusting that the last round of suggestion has been correctly implemented. The only remaining question is if we can document :> (CastCoerce) and if we put it at the end of the cast list. But I'm actually tempted to just merge this right now as this can always be left-over for future improvement.

Suggestions taken into account.

[jfehrle]

To merge, or not to merge, that is the question:
Whether 'tis nobler in the mind to suffer
The slings and arrows of outrageous fortune,
Or to take arms against a sea of troubles
And by opposing end them.

More seriously, putting CastCoerce at the end of the list makes sense; it appears to be the least important of the 4 alternatives. Seems to me the following comment could be adapted to give a bit of explanation. But not eager to wait long on this. Let me know what you'd like me to do (if anything).

| CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)

[Zimmi48]

Unfortunately, I don't know enough about coercions to come up with a working example from this explanation. But I guess you can still put this as a description. And with or without description, it makes sense for :> to be the last one in the list. I'll let you do at least this last change since you seemed to agree.

[JasonGross]

Unfortunately, I don't know enough about coercions to come up with a working example from this explanation. But I guess you can still put this as a description. And with or without description, it makes sense for :> to be the last one in the list. I'll let you do at least this last change since you seemed to agree.

By inspecting the source code, I've discovered that :> has an effect only in program mode, where it invokes

coq/pretyping/coercion.mli

Lines 39 to 43 in c738d65

	(** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
	inserts a coercion into [j], if needed, in such a way it gets as
	type its base type (the notion depends on the coercion system) *)
	val inh_coerce_to_base : ?loc:Loc.t -> program_mode:bool ->
	env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment

coq/pretyping/coercion.ml

Lines 502 to 508 in c738d65

	let inh_coerce_to_base ?loc ~program_mode env sigma j =
	if program_mode then
	let sigma, (ct, typ', _trace) = mu env sigma j.uj_type in
	let sigma, uj_val = app_coercion env sigma ct j.uj_val in
	let res = { uj_val; uj_type = typ' } in
	sigma, res
	else (sigma, j)

Here is an example:

Require Import Coq.Program.Program.
Program Definition foo (x : { n : nat | n = 0 }) := x.
Program Definition bar (x : { n : nat | n = 0 }) := x :>.
Print foo.
(* foo = fun x : {n : nat | n = 0} => x
     : {n : nat | n = 0} -> {n : nat | n = 0}
 *)
Print bar.
(* bar = fun x : {n : nat | n = 0} => ` x
     : {n : nat | n = 0} -> nat
 *)
Unset Printing Notations.
Print bar.
(* bar = fun x : sig (fun n : nat => eq n O) => proj1_sig x
     : forall _ : sig (fun n : nat => eq n O), nat
*)

---

Following code, it seems like this only applies for whatever is registered in coqlib as core.sig.type, and literally nothing else:

coq/pretyping/coercion.ml

Lines 426 to 442 in c738d65

	let mu env sigma t =
	let rec aux v =
	let v' = hnf env sigma v in
	match disc_subset sigma v' with
	| Some (u, p) ->
	let sigma, (f, ct, trace) = aux u in
	let p = hnf_nodelta env sigma p in
	let p1 = delayed_force sig_proj1 in
	let sigma, p1 = Evarutil.new_global sigma p1 in
	sigma,
	(Some (fun sigma x ->
	app_opt env sigma
	f (mkApp (p1, [| u; p; x |]))),
	ct,
	Coe {head=p1; args=[u;p]; previous=trace})
	| None -> sigma, (None, v, IdCoe)
	in aux t

coq/pretyping/coercion.ml

Lines 115 to 128 in c738d65

	let disc_subset sigma x =
	match EConstr.kind sigma x with
	| App (c, l) ->
	(match EConstr.kind sigma c with
	Ind (i,_) ->
	let len = Array.length l in
	let sigty = delayed_force sig_typ in
	if Int.equal len 2 && Ind.CanOrd.equal i (Globnames.destIndRef sigty)
	then
	let (a, b) = pair_of_array l in
	Some (a, b)
	else None
	| _ -> None)
	| _ -> None

coq/pretyping/program.ml

Line 20 in c738d65

let sig_typ () = Coqlib.lib_ref "core.sig.type"

[JasonGross]

So x :> means proj1_sig x in Program mode when x is of type sig _ (i.e., x : { n : _ | _ }) (technically, of a type that is unifiable with whatever is registered as core.sig.type), and in all other cases x :> is just x.

[JasonGross]

Unlike the other cast nodes, it seems that :> does not persist past pretyping, i.e., does not show up as a cast node in the term the kernel sees. (It in fact seems a bit unfortunate for the rest of the code to have to deal with CastCoerce when it seems like in fact there's no reason for it to be valid in the syntax layers post-pretyping.) (I might be missing something, though.)

[Zimmi48]

OK then it looks like a feature that is too intricate and of limited use, that we could propose for removal instead of documenting it. Thanks for figuring this out!

[jfehrle]

Updated, put the :> cast last and added a terse description.

[Zimmi48]

Thanks to your PR #13911, I've discovered that this feature is documented in the refman in this section: https://coq.inria.fr/refman/addendum/program.html#syntactic-control-over-equalities

Instead of this approximate description, I suggest that you just add a link to this section for the documentation of :>.

[jfehrle]

Updated. I made it

:n:`@term10 :> @type` specifies casting to a base type (for example, an
underlying inductive type).  See :ref:`syntactic_control`.

[Zimmi48]

This is still unsatisfying. The most problematic thing is this @type after :> (it doesn't correspond to the grammar). The second issue is that Jason pointed out that this is a Program-specific feature but this description doesn't make this clear at all. I'd suggest something much simpler like:

:n:`@term10 :>` casts to the support type in Program-mode. See :ref:`syntactic_control`.

It's a bit annoying though that we are losing so much time over documenting a feature that we might very well decide to remove very soon.

[jfehrle]

Updated.

[jfehrle]

Hooray! It's been a long time coming. Thanks for your help and patience.

And thanks to @JasonGross for your help.

[Zimmi48]

@coqbot merge now

[jfehrle]

Should we try to put this in 8.13.2? OTOH I don't remember if we've included any post-8.13 material.

[Zimmi48]

My main issue with this is whether the move of an entire section + some additional commands from the Commands chapter to the Equality chapter is appropriate for a patch-level release (as it will break documentation links).