diff options
| author | Olivier Laurent | 2020-04-24 17:07:09 +0200 |
|---|---|---|
| committer | Olivier Laurent | 2020-04-30 13:54:34 +0200 |
| commit | 245b58ac8b6dda26005ae998e5d2cf61a069711c (patch) | |
| tree | efdc605e279706c207ce29848248e602cf4e8440 | |
| parent | 010ef152611977770fa137ed5980205d412febe5 (diff) | |
Symmetry in conclusions of List.map_eq_*
allow simplified iterated applications
| -rw-r--r-- | theories/Lists/List.v | 4 | ||||
| -rw-r--r-- | theories/Sorting/CPermutation.v | 5 | ||||
| -rw-r--r-- | theories/Sorting/Permutation.v | 1 |
3 files changed, 4 insertions, 6 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 5d5f74db44..638e8e8308 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1141,7 +1141,7 @@ Section Map. Qed. Lemma map_eq_cons : forall l l' b, - map l = b :: l' -> exists a tl, l = a :: tl /\ b = f a /\ l' = map tl. + map l = b :: l' -> exists a tl, l = a :: tl /\ f a = b /\ map tl = l'. Proof. intros l l' b Heq. destruct l; inversion_clear Heq. @@ -1149,7 +1149,7 @@ Section Map. Qed. Lemma map_eq_app : forall l l1 l2, - map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ l1 = map l1' /\ l2 = map l2'. + map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ map l1' = l1 /\ map l2' = l2. Proof. induction l; simpl; intros l1 l2 Heq. - symmetry in Heq; apply app_eq_nil in Heq; destruct Heq; subst. diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v index fac9cd1d6d..ddc835891c 100644 --- a/theories/Sorting/CPermutation.v +++ b/theories/Sorting/CPermutation.v @@ -235,9 +235,8 @@ induction m as [| b m]; intros l HC. apply CPermutation_nil in HC; inversion HC. - symmetry in HC. destruct (CPermutation_vs_cons_inv HC) as [m1 [m2 [-> Heq]]]. - apply map_eq_app in Heq as [l1 [l1' [-> [-> Heq]]]]. - symmetry in Heq. - apply map_eq_cons in Heq as [a [l1'' [-> [-> ->]]]]. + apply map_eq_app in Heq as [l1 [l1' [-> [<- Heq]]]]. + apply map_eq_cons in Heq as [a [l1'' [-> [<- <-]]]]. exists (a :: l1'' ++ l1); split. + now simpl; rewrite map_app. + now rewrite app_comm_cons. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index ffef8a216d..1dd9285412 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -552,7 +552,6 @@ Proof. - symmetry in HP. destruct (Permutation_vs_cons_inv HP) as [l3 [l4 Heq]]. destruct (map_eq_app _ _ _ _ Heq) as [l1' [l2' [Heq1 [Heq2 Heq3]]]]; subst. - symmetry in Heq3. destruct (map_eq_cons _ _ Heq3) as [b [l1'' [Heq1' [Heq2' Heq3']]]]; subst. rewrite map_app in HP; simpl in HP. symmetry in HP. |