diff options
| author | affeldt-aist | 2020-05-28 16:24:38 +0200 |
|---|---|---|
| committer | GitHub | 2020-05-28 16:24:38 +0200 |
| commit | 5c67ea2530ba6aaa0dbffaa41e037cfdc9345d00 (patch) | |
| tree | bb22445744384365f6766578a01fae1d5240a81e /mathcomp/ssreflect/fintype.v | |
| parent | 14291b88255b7a1a110c21dec5a3754f25ec8881 (diff) | |
| parent | 37a49513f22a3f792a1ac3241962a7d17455f7e5 (diff) | |
Merge pull request #504 from pi8027/selectors
Revise proofs in ssreflect/*.v
Diffstat (limited to 'mathcomp/ssreflect/fintype.v')
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index 432c30f..67f88a6 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -737,9 +737,7 @@ Proof. by []. Qed. Lemma properP A B : reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B). -Proof. -by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn]. -Qed. +Proof. by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn]. Qed. Lemma proper_sub A B : A \proper B -> A \subset B. Proof. by case/andP. Qed. @@ -1440,7 +1438,7 @@ Definition option_finMixin := Eval hnf in FinMixin option_enumP. Canonical option_finType := Eval hnf in FinType (option T) option_finMixin. Lemma card_option : #|{: option T}| = #|T|.+1. -Proof. by rewrite !cardT !enumT {1}unlock /= !size_map. Qed. +Proof. by rewrite !cardT !enumT [in LHS]unlock /= !size_map. Qed. End OptionFinType. @@ -1714,7 +1712,7 @@ Proof. by apply: val_inj; apply: nth_enum_ord. Qed. Lemma index_enum_ord (i : 'I_n) : index i (enum 'I_n) = i. Proof. -by rewrite -{1}(nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord). +by rewrite -[in LHS](nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord). Qed. End OrdinalEnum. @@ -2158,7 +2156,7 @@ Canonical tag_finType := Eval hnf in FinType {i : I & T_ i} tag_finMixin. Lemma card_tagged : #|{: {i : I & T_ i}}| = sumn (map (fun i => #|T_ i|) (enum I)). Proof. -rewrite cardE !enumT {1}unlock size_flatten /shape -map_comp. +rewrite cardE !enumT [in LHS]unlock size_flatten /shape -map_comp. by congr (sumn _); apply: eq_map => i; rewrite /= size_map -enumT -cardE. Qed. @@ -2184,7 +2182,6 @@ Definition sum_finMixin := Eval hnf in UniqFinMixin sum_enum_uniq mem_sum_enum. Canonical sum_finType := Eval hnf in FinType (T1 + T2) sum_finMixin. Lemma card_sum : #|{: T1 + T2}| = #|T1| + #|T2|. -Proof. by rewrite !cardT !enumT {1}unlock size_cat !size_map. Qed. - +Proof. by rewrite !cardT !enumT [in LHS]unlock size_cat !size_map. Qed. End SumFinType. |