Hi!
I’ve been doing a lot of reading about tactics (and I cannot stress enough how much of a beginner I am at this), and I’m not sure how best to prove the following:
Program Fixpoint transp (l: list (list A)){measure (length l)}:list(list A) :=
match l with
| nil => nil
| nil :: t => transp t
| (a :: r) :: t => (a :: maphd t)::transp(r::maptl t)
end.
Next Obligation.
Admitted.
Next Obligation.
Admitted.
Theorem transptransp: forall a: list(list A),
a=transp (transp a).
Proof.
intros a.
unfold transp.
unfold maphd.
unfold maptl.
induction a as [| a' IHa'].
- (* a = 0 *)
simpl.
auto.
Is what I currently have (I can supply the maphd and maptl functions if necessary). I simply want to prove my transpose function by saying that transpose(transpose x) =x. Reflexivity doesn’t work; I clearly need to unpick my proof a bit more but I don’t know how!
Is it a problem that I cheated and used measure to convince the compiler that my recursion is well-founded?
Hello,
It would be easier to help you if you provide a fully compiling code indeed, please give us the definitiosn of maphd and maptl notably.
With respect to using a measure, it is not cheating per se, but it usually makes proofs about the function harder compared to an hypothetic structural alternative.
Best,
Yannick
I am answering this part of your question:
It is problematic, because you can’t evaluate the function, because the computation gets stuck. It gets stuck, because the function can’t be defined by measure (length l). Actually, the length is the same in each recursive call! What you want is measure (size l), where size l returns the number of elements in the matrix:
From Coq Require Import List.
Import ListNotations.
From Coq Require Import Program.Wf.
From Coq Require Import Lia.
Set Implicit Arguments.
Section Mat.
Variable A : Type.
Fixpoint maphd (l: list (list A)) : (list A):=
match l with
| nil => nil
| nil :: t => maphd t
| (a :: r) :: t => a :: (maphd t)
end.
Fixpoint maptl (l: list (list A)) : (list (list A)):=
match l with
| nil => nil
| r :: t => tl r :: (maptl t)
end.
Definition size (l : list (list A)) : nat := fold_right (fun b a => S (length b + a)) 0 l.
Lemma size_cons (x : list A) (l : list (list A)) :
size (x :: l) = S (length x + size l).
Proof. reflexivity. Qed.
(* This lemma belongs into the stdlib! *)
Lemma length_tl (X : Type) (l : list X) :
length (tl l) = pred (length l).
Proof. now destruct l. Qed.
Lemma size_maptl_le (l : list (list A)) :
size (maptl l) <= size l.
Proof.
induction l.
- reflexivity.
- cbn [maptl]. rewrite !size_cons, length_tl. lia.
Qed.
Program Fixpoint transp (l: list (list A)) { measure (size l)} : list(list A) :=
match l with
| nil => nil
| nil :: t => transp t
| (a :: r) :: t => (a :: maphd t) :: transp (maptl (r :: t))
end.
Next Obligation.
rewrite size_cons; cbn.
pose proof size_maptl_le t.
rewrite length_tl. lia.
Qed.
End Mat.
(I took the maphd function from here).
For the verification: You should test your definition first! Now that we have given the right measure, you can compute the function using Eval cbv in (or equivalently Compute):
Section Test.
Let test := [[1;2;3]; [4;5;6]].
Eval cbv in transp test.
(* = [[1; 4]; [3; 5]; [6]] *)
Eval cbv in transp (transp test).
(* = [[1; 3; 6]; [5]] *)
End Test.
That looks like there is a mistake in your definition. Or maybe I did something wrong in the definition of maptl. 
PS: It is sometimes a good idea to first implement a prototype of your algorithm in a functional PL like ocaml or Standard ML. This sometimes makes testing easier, in particular when you’re working with discrete data types. However, I often find it useful to ‘debug’ a function while proving it correct. 
Thank you both very much! I did not yet know about the ability to Test, that looks very useful, thanks!
I now know that my maphd and maptl work as expected, but my transpose function does not. Here is my entire code:
Require Extraction.
Extraction Language Haskell.
Require Coq.Program.Tactics.
Require Setoid.
Require Coq.Program.Wf.
Set Nested Proofs Allowed.
Set Implicit Arguments.
Notation "x :: l" := (cons x l)
(at level 60, right associativity).
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Section MapArray.
Fixpoint maptl (l: list (list nat)) : list(list nat):=
match l with
| nil => nil
| nil :: t => maptl t
| (a :: r) :: t => r :: (maptl t)
end.
Fixpoint maphd (l: list (list nat)) : (list nat):=
match l with
| nil => nil
| nil :: t => maphd t
| (a :: r) :: t => a :: (maphd t)
end.
End MapArray.
Program Fixpoint transp (l: list (list nat)){measure (length l)}:list(list nat) :=
match l with
| nil => nil
| nil :: t => transp t
| (a :: r) :: t => (a :: maphd t)::transp(r::maptl t)
end.
Next Obligation.
Admitted.
Next Obligation.
Admitted.
Section Test.
Let test := [[1;1;1]; [2;2;2];[3;3;3]].
Eval cbv in transp test.
Eval cbv in transp (transp test).
End Test.
I should say, I now have:
Require Extraction.
Extraction Language Haskell.
Require Coq.Program.Tactics.
Require Setoid.
Require Coq.Program.Wf.
From Coq Require Import List.
Import ListNotations.
From Coq Require Import Program.Wf.
From Coq Require Import Lia.
Set Nested Proofs Allowed.
Set Implicit Arguments.
Notation "x :: l" := (cons x l)
(at level 60, right associativity).
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Section MapArray.
Fixpoint maptl (l: list (list nat)) : list(list nat):=
match l with
| nil => nil
| nil :: t => maptl t
| (a :: r) :: t => r :: (maptl t)
end.
Fixpoint maphd (l: list (list nat)) : (list nat):=
match l with
| nil => nil
| nil :: t => maphd t
| (a :: r) :: t => a :: (maphd t)
end.
End MapArray.
Definition size (l : list (list nat)) : nat := fold_right (fun b a => S (length b + a)) 0 l.
Program Fixpoint transp (l: list (list nat)) { measure (size l)} : list(list nat) :=
match l with
| nil => nil
| nil :: t => transp t
| (a :: r) :: t => (a :: maphd t) :: transp (r :: maptl t)
end.
Next Obligation.
Admitted.
Section Test.
Let test := [[1;1;1]; [2;2;2];[3;3;3]].
Eval cbv in transp test.
Eval cbv in transp (transp test).
End Test.
Theorem transptransp: forall a: list(list nat),
a=transp (transp a).
Proof.
simpl.
induction a.
-intuition.
-intuition.
Qed.
Transp now works as expected, but I’m still stuck on the proof and I don’t know how to get rid of my measure.
I’ve just tried this for the proof:
Proof.
intros a.
unfold transp.
unfold maphd.
unfold maptl.
induction a as [| a' IHa'].
- (* a = 0 *)
simpl.
auto.
- simpl.
auto.
The first subgoal is fine, but the second needs work!
It would definitely be easier if I could refactor the transpose function but I don’t know how.
The case of non-rectangle matrices is still problematic I think:
Let test := [[1;1]; [2;2;2];[3;3;3]].
Eval cbv in transp (transp test).
Maybe you should consider replacing list (list nat) by something like Vector.t (Vector.t nat m) n.
I’d use the Equations plugin; that will generate unfolding lemmas for your function, that otherwise would be tricky to to prove by hand.
Here is one implementation using Vector.t (Vector.t nat m) n. I use a ‘tabulation function’ together with ‘nth’ to compute the transpose. You can also do the same with lists, but you don’t get ‘bound checks’ for free of course.
From Coq Require Import Vector Fin.
Set Implicit Arguments.
(* Lemmas to make working with `Vector.t` and `Fin.t` easier. *)
Section Vector_Basic.
Variable (X:Type).
Lemma vector_inv_0 (v : Vector.t X 0) :
v = Vector.nil _.
Proof.
refine (match v with
| Vector.nil _ => _
end).
reflexivity.
Qed.
Lemma vector_inv_S (n : nat) (v : Vector.t X (S n)) :
{x & {v' | v = Vector.cons _ x _ v'}}.
Proof.
refine (match v with
| Vector.cons _ x _ v' => _
end).
eauto.
Qed.
Lemma fin_inv_0 (i : Fin.t 0) : False.
Proof. refine (match i with end). Defined.
Lemma fin_inv_S (n : nat) (i : Fin.t (S n)) :
(i = Fin.F1) + { i' | i = Fin.FS i' }.
Proof.
refine (match i with
| Fin.F1 => _
| Fin.FS _ => _
end); eauto.
Qed.
End Vector_Basic.
Section Tabulate.
Variable X : Type.
Fixpoint vec_tab (m : nat) { struct m } : (Fin.t m -> X) -> Vector.t X m :=
match m with
| 0 => fun _ : t 0 -> X => Vector.nil X
| S m => fun (f : t (S m) -> X) => Vector.cons X (f Fin.F1) m (vec_tab (fun x : t m => f (Fin.FS x)))
end.
Lemma vec_tab_nth (m : nat) (f : Fin.t m -> X) (i : Fin.t m) :
Vector.nth (vec_tab f) i = f i.
Proof.
induction m.
- exfalso. now apply fin_inv_0.
- pose proof fin_inv_S i as [-> | (i'&->)].
+ reflexivity.
+ cbn. now rewrite IHm.
Qed.
End Tabulate.
Section Matrix.
Variable A : Type.
Definition mat (m n : nat) := Vector.t (Vector.t nat m) n.
Definition transpose (m n : nat) (M : mat m n) : mat n m :=
vec_tab (fun i : Fin.t m => vec_tab (fun j : Fin.t n => nth (nth M j) i)).
Theorem transpose_inv (m n : nat) (M : mat m n) :
transpose (transpose M) = M.
Proof.
unfold transpose.
eapply eq_nth_iff. intros ? i ->.
rewrite vec_tab_nth.
eapply eq_nth_iff. intros ? j ->.
now rewrite !vec_tab_nth.
Qed.
End Matrix.
1 Like
Thank you so much for this! I admit it will take me a little while to parse what you’ve done, but thanks very much! 
It’s very strange, but when I import the Equations plugin, it breaks the code I already have. I don’t suppose you’d know why that is?
Specifically, it breaks the definition of transpose so that it doesn’t compute the transpose any longer. (You need to add another
Next Obligation.
Admitted.
after the first one, and then the transpose function doesn’t actually do anything).
My proposal was to replace the Program-based definition with an Equations-based definition, but your question is still a good one.
In general, Coq has various global flags that can be affected by loading modules, which can cause such problems.
I haven’t confirmed this, but here is my suspicion:
Loading Equations changes the “obligation tactic”, the tactic used to solve obligations automatically; and sometimes some obligations must be actually defined for definitions to compute. Loading Program instead sets the obligation tactic to program_simpl (not to be confused with program_simplify).
To fix this, I’d try finding which obligation is the new one (probably one asking for a proof that your measure is well_founded), and solving it with
Next Obligation. program_simpl. Defined.
I also expect that using Qed for Defined will prevent reduction.
If that is correct, I expect that in general, if a Program definition/fixpoint/… breaks after loading Equations, it seems you can fix that by Solve All Obligations with program_simpl, if Set Transparent Obligations. is left to its default value “on”.
For debugging, you can also set Obligation Tactic := idtac. after your imports and before your definition, so that you can see all the generated obligations in both cases; if those are different, then maybe more settings are affected.
It is the best solution I have met. I have stuck the matrix or vector problem based on Coq for several weeks. Thank you very much 