generalize in match Hn; generalize in match Hn; clear Hn;
unfold segment_enum;
generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
- intros 1 (m); elim m (Hm Hn p IH Hm Hn); [ destruct Hm ]
+ intros 1 (m); elim m (Hm Hn p IH Hm Hn); [ simplify in Hm; destruct Hm ]
simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
- [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?);
- unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
+ [1:unfold segment in ⊢ (? ? match ? % ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
+ unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify;
[2:rewrite > IH; [1,3: autobatch]
rewrite < ltb_n_Sm in Hm; rewrite > Enp in Hm;
lemma uniqP : ∀d:eqType.∀l:list d.
reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l).
-intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H]
+intros (d l); apply prove_reflect; elim l; [1: simplify in H1; destruct H1 | 3: simplify in H; destruct H]
[1: generalize in match H2; simplify in H2;
lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
cases H3; clear H3; intros;
[1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1;
unfold Not; intros (A); lapply (A t) as A';
[1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
- destruct A'; clear A'; rewrite < count_O_mem in H1;
- rewrite > Hcut in H1; destruct H1;
+ destruct A'; rewrite < count_O_mem in H1;
+ rewrite > Hcut in H1; simplify in H1; destruct H1;
|2: simplify; rewrite > cmp_refl; reflexivity;]
|2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
intros (r Mrl1); lapply (A r);
generalize in match Hletin1; simplify; apply (cmpP d r t);
simplify; intros (E Hc); [2: assumption]
destruct Hc; rewrite < count_O_mem in Mrl1;
- rewrite > Hcut in Mrl1; destruct Mrl1;]]
+ rewrite > Hcut in Mrl1; simplify in Mrl1; destruct Mrl1;]]
qed.
lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true.
intros (d p x); cases x (t Ht); clear x;
generalize in match (mem_finType d t);
generalize in match (uniq_fintype_enum d);
-elim (enum d); [destruct H1] simplify;
+elim (enum d); [simplify in H1; destruct H1] simplify;
cases (in_sub_eq d p t1); simplify;
[1:generalize in match H3; clear H3; cases s (r Hr); clear s;
simplify; intros (Ert1); generalize in match Hr; clear Hr;
rewrite > Ert1; clear Ert1; clear r; intros (Ht1);
- unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
+ unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; apply (cmpP ? t t1); simplify; intros (Ett1);
[1: cut (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht})
(filter d (sigma d p) (if_p d p) l) = O); [1:rewrite > Hcut; reflexivity]
generalize in match Hletin; elim l; [ reflexivity]
simplify; cases (in_sub_eq d p t2); simplify;
[1: generalize in match H5; cases s; simplify; intros; clear H5;
- unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
+ unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; rewrite > H7; simplify in H4;
generalize in match H4; clear H4; apply (cmpP ? t1 t2);
simplify; intros; [destruct H5] apply H3; assumption;