Redefine mkRestrPainting to have better computation rule for q := 0 case

[olympichek]

The problem

Here is the current definition of mkRestrPainting:

Fixpoint mkRestrPainting `(extraDepsCohs: DepsCohsExtension p k depsCohs):
  mkRestrPaintingType (mkExtraDeps extraDepsCohs).
Proof.
  red; intros * (l, c); destruct q.
  - now exact (l ε).
  - destruct extraDepsCohs.
    + exfalso; now apply leR_O_contra in Hq.
    + unshelve esplit.
      * now exact (mkRestrLayer depsCohs.(_restrPaintings) depsCohs.(_cohs)
        q (⇓ Hq) ε d l).
      * now exact (mkRestrPainting p.+1 k depsCohs extraDepsCohs
        q (⇓ Hq) ε (d; l) c).
Defined.

In the recursive case of this definition, both direction variable q and extraDepsCohs are decreasing, so Rocq is free to choose either of them as a structurally smaller value that makes the recursion well-founded. In practice, for this definition, Rocq chooses extraDepsCohs. However, at the q := 0 case the definition of mkRestrPainting actually doesn't depend on extraDepsCohs. Thus, we might expect mkRestrPainting to evaluate at q := 0 irregardless of extraDepsCohs, but with the current definition this is not the case:

Lemma mkRestrPainting_q0 `(extraDepsCohs: DepsCohsExtension p k depsCohs) ε
    (d: mkFrame mkDepsRestr.(1))
    (l: mkLayer mkDepsRestr .(_restrFrames) d)
    (c: mkPainting (mkExtraDeps extraDepsCohs) (d; l)):
  mkRestrPainting extraDepsCohs 0 leR_O ε d (l; c) = (l ε).
Proof.
  Fail reflexivity.
  now destruct extraDepsCohs.
Defined.

This makes the proofs of coherence equations for paintings more complicated than they should be, i.e. makes it necessary to rely on dependent pattern matching, which doesn't always behave in obvious way:

destruct extraDepsCohs2, depsCohs2.
Fail destruct _extraDepsCohs0.
(* Abstracting over the terms n, _depsCohs0 and _extraDepsCohs0 leads to a term which is ill-typed! *)
generalize dependent _extraDepsCohs0. intro.
now refine (match _extraDepsCohs0 with TopCohDep E => _ end).

Possible solutions

Implement mkRestrPainting in such a way to regain this definitional equality at q := 0. The issue here is that we can't directly instruct Rocq to consider q the structurally smaller value for the recursion, as q is hidden beyond mkRestrPaintingType definition. We can consider inlining mkRestrPaintingType and making recursion over q explicit:

Fixpoint mkRestrPainting `(extraDepsCohs: DepsCohsExtension p k depsCohs)
  q {struct q}:
  forall (Hq: q <= k) ε (d: mkFrame mkDepsRestr.(1)),
    (mkPaintings (mkDepsRestr; mkExtraDeps extraDepsCohs)).2 d ->
    mkDepsRestr.(_paintings).2 (mkDepsRestr.(_restrFrames).2 q Hq ε d) :=
  match q with
  | 0 => fun _ ε _ '(l; _) => l ε
  | q.+1 =>
    match extraDepsCohs with
    | TopCohDep E => fun Hq _ _ _ => match leR_O_contra Hq with end
    | AddCohDep depsCohs extraDepsCohs => fun Hq ε d '(l; c) =>
      (mkRestrLayer depsCohs.(_restrPaintings) depsCohs.(_cohs) q (⇓ Hq) ε d l;
       mkRestrPainting extraDepsCohs q (⇓ Hq) ε (d; l) c)
    end
  end.

Note that this term-level definition with explicit recursion over q turns to be cleaner and less verbose than the one proposed in pull request #9. This is the one implemented in this pull request.

Alternatively, we can continue using tactics, but explicitly use induction q:

Definition mkRestrPainting `(extraDepsCohs: DepsCohsExtension p k depsCohs):
  mkRestrPaintingType (mkExtraDeps extraDepsCohs).
Proof.
  intros q.
  generalize dependent k.
  generalize dependent p.
  induction q as [| q mkRestrPainting]; intros * (l, c).
  - now exact (l ε).
  - destruct extraDepsCohs.
    + exfalso; now apply leR_O_contra in Hq.
    + unshelve esplit.
      * now exact (mkRestrLayer depsCohs.(_restrPaintings) depsCohs.(_cohs)
        q (⇓ Hq) ε d l).
      * now exact (mkRestrPainting p.+1 k depsCohs extraDepsCohs
        (⇓ Hq) ε (d; l) c).
Defined.

With both of the definitions above we get mkRestrPainting extraDepsCohs 0 leR_O ε d (l; c) = (l ε) provable by reflexivity without the need to destruct extraDepsCohs, which allows to avoid refine (match ...) trick in coherence equations for paintings. This is especially beneficial in a more complicated coherence proofs that I am working on, for degeneracies in all directions.

[artagnon]

Thanks for clearly explaining the issue! I just have one question before we can land this.