I'm having some difficulty in the base case of the induction in the `group_ungroup_opp`

lemma below, specifically I can't seem to rewrite with `mult_n_O`

in either the hypothesis or the goal, as that would be changing the type of l, but then how can I make claims about l without simplifying its type? Any help is much appreciated!

```
From Coq Require Import Vectors.VectorDef.
From Coq Require Import micromega.Lia.
From Coq Require Import Program.Basics.
Require Import JMeq.
Import VectorNotations.
Open Scope program_scope.
Set Transparent Obligations.
Definition vec := t.
Program Fixpoint group{a: Type}{n m: nat}(v: vec a (n*m)): vec (vec a n) m :=
match m with
| 0 => []
| S _ => let (h, ts) := splitat n v in
h :: group ts
end.
Next Obligation. lia. Defined.
(* concat *)
Program Fixpoint ungroup{a: Type}{n m: nat}(v: vec (vec a n) m): vec a (n*m) :=
match v with
| [] => []
| h::ts => h ++ ungroup ts
end.
Next Obligation. lia. Defined.
Lemma group_ungroup_opp: forall {a: Type} {m n} (l: vec a (n*m)),
ungroup (group l) = l.
Proof.
induction m; intros.
- simpl.
Admitted.
```

Welcome to dependent types hell. I think you cornered yourself pretty badly here. Normally, the way one reasons about indexed types is to generalize the hypothesis in whose type one wants to do a rewrite. That is, if the conclusion is something like `forall v : vec (n * 0), ...`

one can usually rewrite this to `forall v : vec (0), ...`

, and then make use of the fact that there is only one such vector. However, if one generalizes the vecor in your example, one still cannot perform the rewrite, because group requires that its argument has type `vec (a * b)`

for some `a`

and `b`

, so one cannot generalize over the multiplication in order to perform the rewrite. (On coq 8.13 I had to import JMeq to make coq accept ungroup.)

Thank you @Christian Doczkal indeed dependent types hell :)

I added JMeq to the imports. Agree the type of group is pretty restrictive on what lemmas I can use on `vec a (n*m)`

without breaking the types, but I am also not quite sure this is unprovable either.

The bottom line is that these properties you mention are downright trivial if not for the dependent types. Do you actually need the dependently typed functions?

Here is a working solution. The main point of difference with yours is to subtly replace `n*m`

with `m*n`

. This makes a big difference because `*`

computes by induction on its left argument, so that `(S m)*n`

is definitionally equal to `n + m*n`

(and `0*n`

to `0`

) rather than only propositionally. That way you can get rid of JMEq (which should be avoided as much as possible), and with a bit of sweat you get what you want.

```
From Coq Require Import Vectors.VectorDef.
From Coq Require Import micromega.Lia.
From Coq Require Import Program.Basics Program.Equality.
Import VectorNotations.
Open Scope program_scope.
Set Transparent Obligations.
Definition vec := t.
Program Fixpoint group{a: Type}{n m: nat}(v: vec a (m*n)): vec (vec a n) m :=
match m with
| 0 => []
| S _ => let (h, ts) := splitat n v in
h :: group ts
end.
(* concat *)
Program Fixpoint ungroup{a: Type}{n m: nat}(v: vec (vec a n) m): vec a (m*n) :=
match v with
| [] => []
| h::ts => h ++ ungroup ts
end.
Lemma group_ungroup_opp: forall {a: Type} {m n} (l: vec a (m*n)),
ungroup (group l) = l.
Proof.
induction m; intros ; cbn in *.
- now dependent destruction l.
- destruct (splitat n l) as [h ts] eqn:e.
eapply Vector.append_splitat in e as ->.
cbn.
now rewrite IHm.
Qed.
```

For me your `dependent desctruction`

call introduces `JMeq_eq`

as axiom @Meven Lennon-Bertrand. If you replace it by `revert l. eapply case0. reflexivity.`

the axiom is not needed

But the trick of using `m*n`

is definitely the right way to go

If you really can't @Lef Ioannidis , here's a solution which works without the trick:

```
From Coq Require Import Vectors.VectorDef.
From Coq Require Import micromega.Lia.
From Coq Require Import Program.Basics.
Require Import JMeq.
Import VectorNotations.
Open Scope program_scope.
Set Transparent Obligations.
Definition vec := t.
Program Fixpoint group{a: Type}{n m: nat}(v: vec a (n*m)): vec (vec a n) m :=
match m with
| 0 => []
| S _ => let (h, ts) := splitat n v in
h :: group ts
end.
Next Obligation. lia. Defined.
(* concat *)
Program Fixpoint ungroup{a: Type}{n m: nat}(v: vec (vec a n) m): vec a (n*m) :=
match v with
| [] => []
| h::ts => h ++ ungroup ts
end.
Next Obligation. lia. Defined.
Lemma group_ungroup_opp: forall {a: Type} {m n} (l: vec a (n*m)),
ungroup (group l) = l.
Proof.
induction m; intros.
- cbn. destruct (mult_n_O n). cbn. revert l. now eapply case0.
- cbn.
match goal with [ |- context [eq_rect _ _ _ _ ?P] ] => generalize P end.
intros e. destruct splitat eqn:E.
cbn. match goal with [ |- context [eq_rect _ _ _ _ ?P] ] => generalize P end.
intros e0. destruct e0. cbn. rewrite IHm.
rewrite <- Eqdep_dec.eq_rect_eq_dec in E.
+ erewrite <- Vector.append_splitat; eauto.
+ eapply PeanoNat.Nat.eq_dec.
Qed.
```

Note how it's a lot uglier than Meven's solution. The trick here is to generalize over the proof in `eq_rect`

repeatedly, destruct it and then go on.

Is the definition of vectors using refinement types not possible? It would be the better solution wouldn't it?

Thank you @Meven Lennon-Bertrand for the quick solution! I tried induction on both n, m but you had to also switch them in the definitions of group/ungroup like you did to make progress. Also thank you @Yannick Forster for the `case0`

tip and also your proof, it showed me how to deal with `eq_rect`

when they do show, very useful!

@Théo Winterhalter I agree refinement types are much nicer, especially combined with `Equations`

Last updated: Jun 25 2024 at 19:01 UTC