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 /theories/Sorting | |
| parent | 010ef152611977770fa137ed5980205d412febe5 (diff) | |
Symmetry in conclusions of List.map_eq_*
allow simplified iterated applications
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/CPermutation.v | 5 | ||||
| -rw-r--r-- | theories/Sorting/Permutation.v | 1 |
2 files changed, 2 insertions, 4 deletions
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. |