The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Michael,

On Tue, Sep 6, 2016 at 6:01 PM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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? 

In effect, this would be what the definitional version of uniqueness of identity proofs (aka the K rule/axiom) would give you, i.e. it would use type information to convert plus_n_Sm 0 1 : S (0 + 1) = 0 + S 1 to eq_refl : 2 = 2. This rule is not part of Coq's type theory (and neither from standard Martin-Löf Type Theory).

 

Would it help if plus_n_Sm would not be opaque?

Indeed, if plus_n_Sm were transparent, the proof would compute by itself to eq_refl (as it is a closed value of type S (0 + 1) = 0 + S 1 and there is only one of those), and you would get the expected result. Many of the arithmetic lemmas are Qed'ed though, so you'll have to make your own library for this purpose.

Which brings me to the question how I can control automation of Program proof obligations? 

Apparently your obligations are transparent as you see the lemmas plus_n_Sm and so on that are used inside them. You can control Opacity/Transparency of Program Obligations using the Set Transparent Obligations option.

Best,

-- Matthieu