Lef Ioannidis (Jul 05 2021 at 17:35): Lef Ioannidis (Jul 05 2021 at 17:35):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.)
Lef Ioannidis (Jul 05 2021 at 19:12):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.
Christian Doczkal (Jul 05 2021 at 19:21):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?
Meven Lennon-Bertrand (Jul 06 2021 at 09:18):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
Yannick Forster (Jul 06 2021 at 10:51):But the trick of using m*n is definitely the right way to go
Yannick Forster (Jul 06 2021 at 10:52):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.
Théo Winterhalter (Jul 06 2021 at 11:07):Is the definition of vectors using refinement types not possible? It would be the better solution wouldn't it?
Lef Ioannidis (Jul 06 2021 at 15:21):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!
Paolo Giarrusso (Jul 06 2021 at 15:37):@Théo Winterhalter I agree refinement types are much nicer, especially combined with Equations
Last updated: Apr 19 2024 at 19:02 UTC