The Coq mailing list

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

Dear Coq Users,

 

I am experimenting with the matrix definition of Coquelicot. I wanted to implement some purely structural operations like transpose trying to avoid the requirement for a zero element, which is used inside Coquelicot as error element for matrix element access functions. Not that it would be terribly bad to require a zero element for e.g. transpose, but I am sometimes a bit stubborn and think it should work without it.

 

A simple example for a structural operation is a function which returns the first column of a matrix as m x 1 matrix. I managed to define a first_col function using Program Fixpoint. Although the Program Fixpoint “proof” is trivial, containing just 1 induction and 2 exact tactics, I am struggling to write a corresponding Fixpoint definition using match:

 

 

Require Import Coquelicot.Coquelicot.

Require Import Program.

 

Program Fixpoint first_col_PF {T : Type} {m n : nat} (M : @matrix T m (S n)) : @matrix T m 1 := _.

Next Obligation.

  induction m.

  - exact ().

  - exact ( (fst (fst M), ()), IHm (snd M) ).

Defined.

 

(* ... which is equivalent to ... *)

 

Definition first_col_NR {T : Type} {m n : nat} (M : @matrix T m (S n)) : @matrix T m 1 :=

  nat_rect

    (fun m' : nat => matrix m' (S n) -> matrix m' 1)

    (fun _ : matrix 0 (S n) => ())

    (fun m' IHm M' => ( (fst (fst M'), ()), IHm (snd M') )  )

    m M.

 

(* ... which in turn should be equivalent to ... *)

 

Fixpoint first_col {T : Type} {m n : nat} (M : @matrix T m (S n)) : @matrix T m 1 :=

  match m return @matrix T m 1 with

  | 0    => ()

  | S m' => ( (fst (fst M), ()), first_col (snd M))

  end.

 

 

Coq does not see that since m=S m', M has at least one row in “fst M”. I guess I need a more fancy in/as/return annotation for the match or some explicit type annotations here and there, but I can’t figure it out. Btw.: the return as given is required – without it Coq doesn’t accept the 0 case term.

 

I guess this would be much easier with the Equations plugin. I guess it is due time to look into it, but I also find it worthwhile to understand how it would work in basic Coq.

Best regards,

 

Michael

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, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928