coq - Coq：绕过统一继承条件

Question

标签： coqcoercionsubtype

Answer 1

I've trouble understanding the (point of the) gauntlet one has to pass to bypass the uniform inheritance condition (UIC).

Intuitively, the uniform inheritance condition says (roughly) "it's syntactically possible to determine every argument to the coercion function just from the type of the source argument".

The developer that added coercions found it easier (I presume) to write the code implementing coercions if the uniform inheritance condition is assumed. I'm sure that a pull request relaxing this constraint and correctly implementing more general coercions would be welcomed!

That said, note that there is a warning message (not an error message) when you declare a coercion that violates the UIC. It will still add it to the table of coercions. Depending on your version of Coq, the coercion might never trigger, or you might get an error message at type inference time when the code applying the coercion builds an ill-typed term because it tries to apply the coercion assuming the UIC holds when it actually doesn't, or (in older versions of Coq) you can get anomalies (see, e.g., bug reports #4114, #4507, #4635, #3373, and #2828).

That said, here is an example where Identity Coercions are useful:

Require Import Coq.PArith.PArith. (* positive *)
Require Import Coq.FSets.FMapPositive.

Definition lookup {A} (map : PositiveMap.t A) (idx : positive) : option A
  := PositiveMap.find idx map.

(* allows us to apply maps as if they were functions *)
Coercion lookup : PositiveMap.t >-> Funclass.

Definition nat_tree := PositiveMap.t nat.
Axiom mymap1 : PositiveMap.t nat.
Axiom mymap2 : nat_tree.

Local Open Scope positive_scope. (* let 1 mean 1:positive *)

Check mymap1 1. (* mymap1 1 : option nat *)
Fail Check mymap2 1.
(* The command has indeed failed with message:
Illegal application (Non-functional construction):
The expression "mymap2" of type "nat_tree"
cannot be applied to the term
 "1" : "positive" *)
Identity Coercion Id_nat_tree : nat_tree >-> PositiveMap.t.
Check mymap2 1. (* mymap2 1 : option nat *)

Basically, in the extremely limited case where you have an identifier which would be recognized as the source of an existing coercion if you unfolded its type a bit, you can use Identity Coercion to do that. (You can also do it by defining a copy of your existing coercion with a different type signature, and declaring that a coercion too. But then if you have some lemmas that mention one coercion, and some lemmas that mention the other, rewrite will have issues.)

There is one other use case for Identity Coercions, which is that, when your source is not an inductive type, you can use them for folding and not just unfolding identifiers, by playing tricks with Modules and Module Types; see this comment on #3115 for an example.

In general, though, there isn't a way that I know of to bypass the uniform inheritance condition.