In the development below, I arrive at the goal, and I don't know how to proceed.
A: Type
a: list (list A)
b: list A
i,j: nat
Hi: i < length a
Hj: j < length (nth i a [])
--------------------------------------------
nth_error (nth i a []) j =
Some
(match nth2 i j as e return (nth2 i j = e -> A) with
| Some a0 => fun _ : nth2 i j = Some a0 => a0
| None =>
fun H : nth2 i j = None =>
False_rect A (nth2_not_None Hi Hj H)
end
eq_refl)
Here is a collcoq link (interactive coq in the browser) https://x80.org/collacoq/ejavedelid.coq
I can't rewrite the nth2 i j term to Some x (although it's provably not None)
My question is how to proceed when I'm using the convoy pattern (a=b -> A) as return type, like I'm doing here.
My question is not how to use another definition of nth2 that doesn't have this problem.
Big thanks to anyone taking the time to look at this.
Require Import List.
Import ListNotations.
Require Import Fin.
Section Example.
Variable (A:Type).
Variable (a:list (list A)) (b: list A).
Definition indices :=
{ '(i, j):(nat * nat) | i < length a /\ j < length (nth i a [])}.
Definition lookup_spec (f:indices -> A) :=
forall ij, let '(i,j) := proj1_sig ij in
nth_error (nth i a []) j = Some (f ij).
Definition nth2 i j : option A :=
match nth_error a i with Some ai => nth_error ai j | None => None end.
Lemma nth2_not_None {i j} (Hi: i < length a) (Hj: j < length (nth i a [])):
nth2 i j <> None.
unfold nth2.
enough (exists (d:A), True) as [d _] by
now rewrite (nth_error_nth' _ [] Hi), (nth_error_nth' _ d Hj).
destruct (nth i a []) as [| x l]. now exfalso. now exists x.
Defined.
Definition lookup (ij : indices): A :=
let '(exist _ (i, j) (conj Hi Hj)) := ij in
match nth2 i j as e return nth2 i j = e -> A with
| Some a => fun _ => a
| None => fun H => False_rect _ (nth2_not_None Hi Hj H)
end eq_refl.
Lemma lookup_ok: lookup_spec lookup.
intros [[i j] [Hi Hj]].
unfold proj1_sig, lookup.
The answer is to do a somewhat tricky generalization:
Lemma lookup_ok: lookup_spec lookup.
Proof.
intros [[i j] [Hi Hj]].
unfold proj1_sig, lookup.
generalize (@eq_refl _ (nth2 i j)) as Heq.
generalize (nth2 i j) at 2 3.
intros [a0|] Heq.
2: { exfalso. eapply nth2_not_None; eassumption. }
unfold nth2 in Heq. destruct (nth_error a i) as [a1|] eqn:Heq2.
2: { congruence. }
erewrite nth_error_nth. 2: eassumption.
easy.
Qed.
Ideally, one would want to destruct (nth2 i j) as [a0|] eqn:Heq, and use the Heq in place of the eq_refl. Unfortunately, Rocq does not support expressing this with tactics, so you have to use generalize properly (or manually copy-paste the goal and change it such that it works). Then you can destruct nth2 i j and reason based on that outcome.
Edit: I found out that this generalize .. at 2 3 trick is not new. For example, it is also discussed in this Rocq Discourse thread.