made Vector.nth substructural

[mrhaandi]

The documentation of Vector.nth states "Computational behavior of this function should be the same as ocaml function."
However, the current implementation is not structural in the vector, but in the position.
This is different from OCaml: https://github.com/ocaml/ocaml/blob/83762af41d5a302ed793d6fb4bbe18a3447e18b1/stdlib/list.ml#L37.

The present PR makes Vector.nth follow OCaml nth and return a strict subterm of the input vector.
For example, this allows recursion on nth (which otherwise complains about a non-decreasing argument):

Require Vector.

Inductive container : Type :=
  | c_0 : container
  | c_1 : Vector.t container 2 -> container.

Fixpoint test (c : container) : unit :=
  match c with
  | c_0 => tt
  | c_1 v => test (Vector.nth v (Fin.FS Fin.F1))
  end.

Fixes / closes #16738

• Added / updated test-suite.
• Added changelog.

[Janno]

Alternative definition without equalities:

Suggested change

	fix nth_fix {n : nat} (v : t A n) {struct v} : Fin.t n -> A :=
	match v with
	| nil _ => fun p => False_rect A (Fin.case0 _ p)
	| cons _ x m v' => fun p =>
	match p in (Fin.t m') return (m' = S m -> A) with
	| Fin.F1 => fun _ => x
	| Fin.FS p' => fun E => nth_fix v' (eq_rect _ _ p' m (f_equal Nat.pred E))
	end eq_refl
	end.
	fix nth_fix {n : nat} (v : t A n) {struct v} : Fin.t n -> A :=
	match v with
	| nil _ => fun p => False_rect A (Fin.case0 _ p)
	| cons _ x m v' => fun p =>
	match p with
	| Fin.F1 => fun _ => x
	| Fin.FS p => fun go => go p
	end (nth_fix v')
	end.

I suspect it is correct but I haven't actually tested it.

[mrhaandi]

Unfortunately, no. Your proposed version was the first one I wrote. However, the test mentioned in the intro fails with

Recursive definition of test is ill-formed.
In environment
test : container -> unit
c : container
v : t container 2
Recursive call to test has principal argument equal to
"nth v (Fin.FS Fin.F1)" instead of "v".
Recursive definition is:
"fun c : container =>
 match c with
 | container_v v => test (nth v (Fin.FS Fin.F1))
 | container_0 => tt
 end".

It would be interesting to know why this is the case.

[Janno]

Not sure what I am doing wrong but for me both ways of writing nth fail the test case. This is on 8.16.

[Janno]

Never mind, I was using Vector.nth instead of my local nth.

[mrhaandi]

Not sure what I am doing wrong but for me both ways of writing nth fail the test case. This is on 8.16.

Exactly the following works (for me) on 8.16:

Require Vector. 

Definition my_nth {A} :=
  fix nth_fix {n : nat} (v : Vector.t A n) {struct v} : Fin.t n -> A :=
    match v with
    | Vector.nil _ => fun p => False_rect A (Fin.case0 _ p)
    | Vector.cons _ x m v' => fun p =>
        match p in (Fin.t m') return (m' = S m -> A) with
        | Fin.F1 => fun _ => x
        | Fin.FS p' => fun E => nth_fix v' (eq_rect _ _ p' m (f_equal Nat.pred E))
        end eq_refl
    end.

Inductive container : Type :=
| container_v : Vector.t container 2 -> container
| container_0 : container.

Fixpoint test (c : container) : unit :=
match c with
| container_0 => tt
| container_v v => test (my_nth v (Fin.FS Fin.F1))
end.

[DmxLarchey]

@Janno More precisely, the return type in not an inductive type but the result of a match

[DmxLarchey]

However in either case I don't know if extraction will eliminate the commutative cuts, whereas with a cut on equality it should get erased.

The cut gets erased at extraction. I am pretty sure ;-)

[DmxLarchey]

I mean properly extracted with the match p in Fin.t m return Vector.t _ (pred m) -> _ with version.

[SkySkimmer]

Cutting with just th vector extracts fine, but cutting with nth_fix v' extracts to

let rec nth _ v p =
  match v with
  | Nil -> assert false (* absurd case *)
  | Cons (x, m, v') -> let x0 = nth m v' in (match p with
                                             | F1 _ -> x
                                             | FS (_, p') -> x0 p')

which may or may not compile as efficiently

[mrhaandi]

Let us see what the CI has to say about @SkySkimmer's and @DmxLarchey's suggestions

[mrhaandi]

@coqbot run full ci

[mrhaandi]

I added a changelog entry, and a case to the test-suite to check for strict subterms.
The full ci run had errors due to too long compilation time in vst and fiat_crypto (both unrelated to the PR).

[andres-erbsen]

I don't know Vector that well, but the reasoning for this change makes sense to me. @coq/stdlib-maintainers please feel free to weigh in; if nothing is said in a couple of days I intend to merge.

[andres-erbsen]

@coqbot run full ci

because I cannot figure out how to view the previous results

[SkySkimmer]

because I cannot figure out how to view the previous results

It seems the commit that got full CI was 6ae4735 (pipeline https://gitlab.com/coq/coq/-/pipelines/678316994)
Then 575807e was normal pushed, then 334cfab force pushed

[andres-erbsen]

@coqbot merge now

[coqbot-app]

@andres-erbsen: You cannot merge this PR because:

• There is no kind: label.
• No milestone has been set.

[andres-erbsen]

@coqbot merge now