The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

 

I have a question regarding reduction of proof terms with dependent types, especially reduction of matches with single patterns. A simple example is this:

 

Require Import Vector.

 

Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n2+n1) :=

  match v1 in Vector.t _ n1' return Vector.t A (n2 + n1') with

  | nil _               => v2

  | cons _ e n1' sv     => vector_rev sv (cons A e n2 v2)

  end.

 

Definition Example2_01 :=

  cons bool false 1 (

  cons bool true  0 (

  nil bool

  )).

 

Eval compute in vector_rev Example2_01 (nil bool).

 

This results in:

 

     = match plus_n_Sm 0 1 in (_ = y) return (t bool y) with

       | eq_refl =>

           match plus_n_Sm 1 0 in (_ = y) return (t bool y) with

           | eq_refl =>

               match plus_n_O 2 in (_ = y) return (t bool y) with

               | eq_refl => cons bool true 1 (cons bool false 0 (nil bool))

               end

           end

       end

     : t bool (0 + 2)

 

I wonder why Coq can’t reduce this to “cons bool true 1 (cons bool false 0 (nil bool))”. All the matches have just one pattern, so it should be obvious which one it is. I guess this is required to show that “t bool (0 + 2)” is the same as “t bool 2” but isn’t there a simpler way which computes?

 

If a match is just there to transform types, can’t Coq reduce the match if the types would unify without the match?

 

Would it help if plus_n_Sm would not be opaque? Which brings me to the question how I can control automation of Program proof obligations.

 

Best regards,

 

Michael

 

P.S.: If I use Vector.t A (n1+n2) it also works, but the proof terms get larger.

 

P.P.S.P I sent this message already yesterday but apparently there was a server issue. My apologizes if someone got it twice.

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928