The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Indeed, the issue is that those proofs were ended with Qed rather than Defined.  You can control the automation of Program via [Obligation Tactic := ... ].  I believe the default is [program_simpl].

On the theory behind it, note that proofs of equality are *freely generated* by the single pattern.  With univalence, you can get other proofs of equality, and without UIP or axiom K, you cannot prove that they don't exist in general.

On Tue, Sep 6, 2016, 9:01 AM 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?

 

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