[ apply (mk_finType fsort enum Hcut)
| intros (x); cases x (n Hn); simplify in Hn; clear x;
generalize in match Hn; generalize in match Hn; clear Hn;
[ apply (mk_finType fsort enum Hcut)
| intros (x); cases x (n Hn); simplify in Hn; clear x;
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); [ simplify in Hm; destruct Hm ]
simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
unfold segment_enum;
generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
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;
unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify;
[2:rewrite > IH; [1,3: autobatch]
unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify;
[2:rewrite > IH; [1,3: autobatch]
fold simplify (sort nat_eqType); (* CANONICAL?! *)
cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
simplify; [2: reflexivity]
fold simplify (sort nat_eqType); (* CANONICAL?! *)
cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
simplify; [2: reflexivity]
- generalize in match H1; clear H1; cases s; clear s; intros (H1);
- unfold segment; simplify; simplify in H1; rewrite > H1;
+ generalize in match H1; clear H1; cases s (r Pr); clear s; intros (H1);
+ unfold fsort; unfold segment; simplify; simplify in H1; rewrite > H1;
rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?));
unfold Not; intros (Enw); rewrite > Enw in Hw;
rewrite > ltb_refl in Hw; destruct Hw]
rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?));
unfold Not; intros (Enw); rewrite > Enw in Hw;
rewrite > ltb_refl in Hw; destruct Hw]
lemma uniq_tail :
∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l).
intros (d x l); elim l; simplify; [reflexivity]
lemma uniq_tail :
∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l).
intros (d x l); elim l; simplify; [reflexivity]
rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
qed.
rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
qed.
[2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x t);
intros (H5); simplify;
[1: rewrite > count_O; [reflexivity]
[2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x t);
intros (H5); simplify;
[1: rewrite > count_O; [reflexivity]
rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1);
assumption;]
|1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]
rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1);
assumption;]
|1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]