The Coq mailing list

[Lars Rasmusson <Lars.Rasmusson AT sics.se>]

I came up with one less ugly way to do the type coercion. I used refine, and inserted an

underscore before the return value, as a place holder for a function that converts the type

to the right type, and then proves how to convert the types afterwards.

Is there some other way to make the type inference more powerful (in this case, to use ring to

see that two types are actually convertible)?

My development:

Definition TestERR (n pad:nat) (v:Vector.t nat n) : Vector.t nat ((S pad)*n).

  refine (

  match n as m return n=m -> Vector.t nat ((S pad)*n) with

    | 0   => fun _ => _ (Vector.nil nat)

    | S p => fun _ => _ (append (const 0 (S pad)) (const 0 ((S pad)*p)))

  end

    (eq_refl n));

  intros; subst.

  replace (S pad * 0) with 0; auto.

  replace (S pad * S p) with  (S pad + S pad * p); auto; ring.

Qed.

On Wed, May 6, 2015 at 2:37 PM, Lars Rasmusson <Lars.Rasmusson AT sics.se> wrote:

As the others have said, it seems to be a problem with "Program".

I tried to rewrite TestERR without using Program.

I use the "Convoy Pattern" idea to not lose the info that n=0 in the first case and n=S n' in the second case.

I had to convince the type checker that 

* when n=0 then t nat 0  actually is equal  t nat ((S pad)*n, and

* when n=S n; then  t nat (S pad + (S pad * n')) -> t nat ((S pad)*n)

To do that, I defined two functions, f1 and f2 that took a term of the first type and returned the second type.

My question is:  is there a more elegant way to do this, without having to introduce the "dummy type coersion functions"?

Here is my development:

Definition f1 (pad n:nat) : n = 0 -> t nat 0 -> t nat ((S pad)*n).

  intros. subst. rewrite mult_0_r. auto. Qed.

Definition f2 (pad n n':nat) : n = S n' -> t nat (S pad + (S pad * n')) -> t nat ((S pad)*n).

  intros H H0. replace (S pad + S pad * n') with (S pad * S n') in H0 by ring.

  subst; auto.

Qed.

Definition TestERR (n pad:nat) (v:Vector.t nat n) : Vector.t nat ((S pad)*n) :=

  match n as m return n=m -> Vector.t nat ((S pad)*n) with

    | 0 => fun H => f1 _ _ H (Vector.nil nat)

    | S p => fun H => f2 _ _ _ H (append (const 0 (S pad)) (const 0 ((S pad)*p)))

  end

    (eq_refl n).