The Coq mailing list

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

Dear Matthieu,

 

> plus_n_Sm 0 1 : S (0 + 1) = 0 + S 1 to eq_refl : 2 = 2

 

I see what you mean. But since proof irrelevance of equality for nat is provable in Coq, it should be possible to create a vector_rev function, which produces a proof which reduces by computation to eq_refl. Let me see …

 

Best regards,

 

Michael

 

Michael Soegtrop
iCDG (Intel Communications & Devices Group)

PRD PSE SBA SWR (Software Reliability)
Principal Software Reliability

Phone: +49 (0)89 99 8853-60431
Mobile: +49 (0)172 81 62 56 2
michael.soegtrop AT intel.com

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Matthieu Sozeau
Sent: Tuesday, September 06, 2016 6:13 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Getting "computing" proof terms with dependent types / reduction of matches with single pattern

 

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

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