make subset types compatible for function application

Link:: https://stackoverflow.com/q/49620573

Display all goals and responses

Question

I'm trying to get familiar with subset types in Coq and I've come across a kind of use case where I don't know how to proceed. Consider a function that expects a natural number greater than 2, and another function that expects a natural number greater than 2 and less than 10. Inside the latter function I'd like to call the former, which should be possible, but it seems I have to do something to make its type suitable for function application. This is what I'm trying to do:

Definition add_one_if_gt_2 (i : {i1 : nat | i1 > 2}) := (proj1_sig i) + 1.
Definition add_one_if_gt_2_and_lt_10 (i : {i1 : nat | i1 > 2 /\ i1 < 10}) :=
  add_one_if_gt_2 i.In environment
i : {i1 : nat | i1 > 2 /\ i1 < 10}
The term "i" has type "{i1 : nat | i1 > 2 /\ i1 < 10}"
while it is expected to have type
 "{i1 : nat | i1 > 2}".

What's missing in add_one_if_gt_2_and_lt_10 to make it typecheck? In general, for more complicated subset types that might be compatible, what's the usual way to proceed?

Also, I'm using i1 in the subset type specification just in case, but it seems it also works if I use i, although I don't know if there's any potential issue there since the parameter name is also i. Would using i for both variables be problematic?

Answer (Daniel Schepler)

One possibility would be to use the Program functionality:

Require Import Program.

Program Definition add_one_if_gt_2 (i : {i1 : nat | i1 > 2}) :=
  i + 1.
Program Definition add_one_if_gt_2_and_lt_10
  (i : {i1 : nat | i1 > 2 /\ i1 < 10}) :=
  add_one_if_gt_2 i.

If you step through this code, you'll notice that the system is generating messages about "obligations" - but in this example, all the obligations were simple enough that the system could automatically resolve them on its own, and the definitions immediately completed. (In this case, the obligation generated by the second definition is that i > 2 /\ i < 10 implies i > 2.)

In other situations where it cannot solve the obligations so easily, you might get pending obligations. In this case, you can use Gallina directives such as Next Obligation. to enter proof mode and prove them yourself. (For more information, see the appropriate chapter of the Coq documentation.)

Answer (Anton Trunov)

You do this manually because it's not hard to destruct a term of type {i1 : nat | i1 > 2 /\ i1 < 10} which is basically a triple of a nat (i1) and two proofs: i1 > 2 and i2 < 10. What we are going to do is to destruct this triple, throw away the third component and repack it into a term of type {i1 : nat | i1 > 2}, which is a pair:

Definition add_one_if_gt_2 (i : {i1 : nat | i1 > 2}) :=
  S (proj1_sig i).

Definition add_one_if_gt_2_and_lt_10 (i : {i1 : nat | i1 > 2 /\ i1 < 10}) :=
  let '(exist _ i1 (conj i1_gt2 _)) := i in
  add_one_if_gt_2 (exist _ i1 i1_gt2).

We can do it with projections as well:

Definition add_one_if_gt_2_and_lt_10' (i : {i1 : nat | i1 > 2 /\ i1 < 10}) :=
  add_one_if_gt_2 (exist _ (proj1_sig i)
                         (proj1 (proj2_sig i))).

Another approach is to use sig2 type for your special case:

Definition add_one_if_gt_2_and_lt_10_sig2 (i : {i1 : nat | i1 > 2 & i1 < 10}) :=
  add_one_if_gt_2 (sig_of_sig2 i).

And using the coercion mechanism you can simplify the above definition into:

Coercion sig_of_sig2 : sig2 >-> sig.

Definition add_one_if_gt_2_and_lt_10_sig2'
           (i : {i1 : nat | i1 > 2 & i1 < 10}) :=
  add_one_if_gt_2 i.

Which is exactly the solution you were trying to apply!

In case you are not familiar with coercions: this mechanism inserts sig_of_sig2 (or some other suitable coercion) automatically if it encounters a type error which can be mended.