diff options
| author | Hugo Herbelin | 2020-05-06 23:03:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-06 23:03:27 +0200 |
| commit | 325a644b3f5a5f8c1a86191004576e7c763ae9f3 (patch) | |
| tree | 1207f1774e239abe7cfd4213a7d866018929cc75 | |
| parent | 2dd59422a4f2ba1d6e75e710b88129751379aa79 (diff) | |
| parent | 245b58ac8b6dda26005ae998e5d2cf61a069711c (diff) | |
Merge PR #12171: [stdlib] [list] Symmetry in conclusions of map_eq_cons and map_eq_app
Reviewed-by: anton-trunov
Reviewed-by: herbelin
| -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 21d04da877..31d9f7f0ed 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. |