Optimizing the propagation of the guard condition under a match on a type with indices by discarding only the type information from the indices

[herbelin]

Kind: enhancement

The type-based filtering of decreasing arguments passed across a match was not taking into account that the return predicate had a specific instance in each branch. We take this instance into account and this allows to recognize more useful fixpoints as guarded (e.g. map3 on vectors when mechanically generated with small inversion).

We observe that the protection against the inconsistency of propositional extensionality obtained by not using at all the indices of the type of the term to match in propagating the subterm status through a match (see 9b272a8 and further commits) is finally overly restrictive: only the type information present in the indices needs to be ignored (see comment below for a proof sketch).

This allows to:

• fix Guard checking regression #17062,
• support complex forms of small inversion,
• (virtually) provide definitional UIP on the subset of rewriting not involving types without breaking normalization.

Here is a typical example of small inversion exploiting the PR:

Inductive vector (A : Type) : nat -> Set :=                                                                         
    Cons : forall n : nat, vector A n -> vector A (S n).                                                            

Fixpoint degenerated_map3
  (A : Type) (n : nat) (v0 v1 v2 : vector A n) {struct v2} : vector A n :=
match v0 in vector _ n0 return vector A n0 -> vector A n0 -> vector A n0 with
| Cons _ n0 tl0 =>
  fun (v1 : vector A (S n0)) (v2 : vector A (S n0)) =>
  match
    v1 in vector _ n1
    return match n1 with  
    | 0 => IDProp
    | S n1 => vector A n1 -> vector A (S n1) -> vector A (S n1)
    end
  with
  | Cons _ n1 tl1 =>  
    fun (tl0 : vector A n1) (v2 : vector A (S n1)) =>
    match
      v2 in (vector _ n2)
      (* This return type was not recognized as casting tl0 with a
         "vector" type because n2 was left as an uninstantiated variable,
         blocking the reduction of the "match", while it could have been
         instantiated with its value in the branch, i.e. (S n1), allowing the 
         match on n2 to reduce *)
      return match n2 with
      | 0 => IDProp
      | S p => vector A p -> vector A p -> vector A (S p)
      end
    with  
    | Cons _ n2 tl2 =>
      fun (tl0 tl1 : vector A n2) =>  
      Cons A n2 (degenerated_map3 A n2 tl0 tl1 tl2)
    end tl0 tl1
  end tl0 v2
end v1 v2.

• Added / updated test-suite
• Entry added in the changelog

TODO: apply it to restrict_spec too.

[herbelin]

It looks like I was redoing #798 and re-introducing the propositional extensionality issue.

I made a new proposal which instantiates the predicate only with the constructed part of its indices.

It fills non-constructor terms with a dummy (generally ill-typed) Prop which is a bit ugly. A possible alternative would be to add an argument x : forall A, A to the signature and, to compute the type T of the return and to use x T. Is it worth the detour.

[SkySkimmer]

Removing the milestone as there has been no change since 8.14.

[ppedrot]

Since this PR is incorrect and there are upcoming changes in the guard condition anyways, I'm closing it.

[herbelin]

What about doing a lazy substitution of the indices:

• for match and fix we head-reduce according to the indices, keeping the substitution explicit
• once we meet an application, a forall, a sort, an inductive type, we drop the substitution

That would solve both the map3 example above and #17062.

Ideally, I suspect that we could go one step further and continue to propagate the substitution of object in a small type, since the problem with extensionality arrives when dealing with equality of types.

[herbelin]

As a restricted form of univalence, the statement of propositional extensionality says that A = B :> Prop is equivalent to A <-> B, that is to the pair of a map f from A to B and a map g from B to A. The computational contents of A = B -> P A -> P B, as found e.g. in cubical type theory, is then to apply the functor P covariantly on f and contravariantly on g. In this interpretation, it is thus expected when e.g. P X := X, that eliminating e : A = B to get B from A introduces a coercion, and, if this coercion necessarily includes a constructor, this directly breaks the size of the type. This seems to be the root cause of the proof of inconsistency of propositional extensionality in the presence of a guard criterion which assumes that traversing an elimination of some e : A = B does not change the size of the return type.

This limitation seems specific to equality of types. For instance, traversing an elimination on e : p = q : nat to produce P q from P p cannot lead to change the size of P p: by inspection of the form of P (seeing inductive types as built from μ, ν, Empty_set, unit, sig, sum, Prop-truncation, equality), the elimination of e can only go to non-type arguments of P (or to arguments of match/fix if the type is built by case analysis).

Traversing an elimination e : t = u : V when V is an inductive type containing type arguments or a function type ending in a sort would pose problems though since the type information in u could be extracted by match or application respectively and P could be built from it (either directly if P is X, or indirectly if P is say Box X for X binding to the corresponding extracted type information). This type information, say U, is related up to an isomorphism to the corresponding type information in t, say T, and if U has size information, it would be virtually affected by the isomorphism.

Here is a strategy to ensure that no isomorphism hidden behind an equality of types can modify the size of the return type when eliminating in a type with indices (and in particular when eliminating an equality proof):

Normalize all indices u1, ..., un of the term and replace all occurrences of an inductive type eventually returned in the type by some "undefined" type Ω that inhibits any possible contribution to the size of the premisses or conclusions of the return type.

I just pushed a version which is almost this new "optimal" algorithm.

I'm saying almost optimal because, ideally, I would have needed access to the indices of the term being matched, but they don't seem to be available (except sometimes in the CaseInvert case). Typing is not available either. So, I implemented an a priori more costly and less optimal algorithm that propagates size information branch per branch based on the type-inhibited indices in the branches (this is more costly because done for the each branch rather than once for all; this is a priori less optimal because, iianm, it can reject a recursive call on a commutative-cut argument on a "match"-like return predicate in a branch choosing a branch of the return predicate missing enough products to absorb the argument and which would have not been used for size if we had used the indices of the term to match).

[herbelin]

By the way, the restriction on the return clause done in this PR could be applied to definitional UIP to prevent the breakage of normalization with impredicativity... and thus to always activate definitional UIP (or, at worst, to make optional only the subcase of definitional UIP involving rewriting of types).

[SkySkimmer]

By the way, the restriction on the return clause done in this PR could be applied to definitional UIP

Can you explain more? The issue with definitional UIP does not involve any fixpoints so the guard condition is unrelated.
For reference the example:
https://coq.github.io/doc/master/refman/addendum/sprop.html#non-termination-with-uip

[herbelin]

Can you explain more?

I mean that in:

Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q.
Definition transport (P Q:Prop) (x:P) (y:Q) : Q := match all_eq P Q x y with srefl _ => x end.

the criterion above detects that the match used in transport may not respect the size. This is actually expected: P and Q have no reasons to have the same size (what is exploited to get non-termination).

On the other side, still from the reference manual, in:

Axiom e : seq 0 0.
Definition hidden_arrow := match e return Set with srefl _ => nat -> nat end.

the match used in hidden_arrow is recognized as letting the inside and outside type of the match having the same size (because it does not rewrite types).

[SkySkimmer]

But how is the size used?
How would your change lead to the example not looping?

[herbelin]

But how is the size used?

I'm sorry, when talking about the Prop non-termination, I was using the word "size" in an informal Prop-like sense, not in the sense of the size of an inductive, as in the case of the guard of a fixpoint. I mean, informally, that the expression (fun x : top => x (top -> top) (fun x => x) x) used in the non-termination is similar to calling a recursive constructor and thus changing the size.

How would your change lead to the example not looping?

The PR itself does not modify definitional UIP. What I'm saying is that if we restricted definitional UIP to those match for which the return predicate and indices satisfy the size-preservation condition implemented in this PR, then, the match used in the looping example would not be any more a valid definitional UIP and thus would be blocked.

So, in some sense, this suggests a notion of "guarded definitional UIP" which reduces all UIP-like match except those that involve type rewriting, where forbidding type rewriting is sufficient to preserve the "size".

Added note: For fixpoints, it is enough to mask inductive types. For "guarded definitional UIP" one would a priori need to mask all applied/projected variables, inductive types and pi-types in impredicative sorts.

[coqbot-app]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[SkySkimmer]

AFAICT there is currently not much interest in weakening the guard condition without some strong theoretical argumentation (eg a formalized proof or at least a published paper instead of some github postings)