-generalize in match (refl_eq ? (p t));
-generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (Hpt);
+generalize in match (refl_eq ? (p a));
+generalize in match (p a) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (Hpt);
[1: apply H; intros (y Hyl);
apply H1; simplify;
rewrite > Hyl; rewrite > orbC; reflexivity;
|2: simplify; apply (cmpP d2 x s); simplify; intros (E);
[1: apply H; intros (y Hyl);
apply H1; simplify;
rewrite > Hyl; rewrite > orbC; reflexivity;
|2: simplify; apply (cmpP d2 x s); simplify; intros (E);
simplify; rewrite > cmp_refl; reflexivity
|2: apply H; intros; apply H1; simplify; rewrite > H2;
rewrite > orbC; reflexivity]]
simplify; rewrite > cmp_refl; reflexivity
|2: apply H; intros; apply H1; simplify; rewrite > H2;
rewrite > orbC; reflexivity]]
∀d:eqType.∀p:d→bool.∀l:list d.
(∀x:d.mem d x l = true → notb (p x) = true) → count d p l = O.
intros 3 (d p l); elim l; simplify; [1: reflexivity]
∀d:eqType.∀p:d→bool.∀l:list d.
(∀x:d.mem d x l = true → notb (p x) = true) → count d p l = O.
intros 3 (d p l); elim l; simplify; [1: reflexivity]
- apply (cmpP d x t); [2: rewrite > H2;]; intros; reflexivity;
-|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; autobatch]
+ apply (cmpP d x a); [2: rewrite > H2;]; intros; reflexivity;
+|1:intros (H2); lapply (H1 a); [2:simplify; rewrite > cmp_refl; simplify; autobatch]
[ 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 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.
lemma count_O_mem : ∀d:eqType.∀x:d.∀l:list d.ltb O (count d (cmp d x) l) = mem d x l.
rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
qed.
lemma count_O_mem : ∀d:eqType.∀x:d.∀l:list d.ltb O (count d (cmp d x) l) = mem d x l.
reflexivity; qed.
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).
reflexivity; qed.
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).
[1: generalize in match H2; simplify in H2;
lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
cases H3; clear H3; intros;
[1: generalize in match H2; simplify in H2;
lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
cases H3; clear H3; intros;
rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1);
assumption;]
|1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]
intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H2) in H3 ⊢ %;
clear H2; clear x; lapply (uniq_mem ? ? ? H1) as H4;
rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1);
assumption;]
|1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]
intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H2) in H3 ⊢ %;
clear H2; clear x; lapply (uniq_mem ? ? ? H1) as H4;
rewrite > E in H4; rewrite > H4 in Hy; destruct Hy;]
|2: rewrite > uniq_tail in H1;
generalize in match (refl_eq ? (uniq d l1));
generalize in match (uniq d l1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
[1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1;
rewrite > E in H4; rewrite > H4 in Hy; destruct Hy;]
|2: rewrite > uniq_tail in H1;
generalize in match (refl_eq ? (uniq d l1));
generalize in match (uniq d l1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
[1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1;
[1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
destruct A'; rewrite < count_O_mem in H1;
[1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
destruct A'; rewrite < count_O_mem in 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);
|2: simplify; rewrite > cmp_refl; reflexivity;]
|2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
intros (r Mrl1); lapply (A r);
- [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity]
- generalize in match Hletin1; simplify; apply (cmpP d r t);
+ [2: simplify; rewrite > Mrl1; cases (cmp d r a); reflexivity]
+ generalize in match Hletin1; simplify; apply (cmpP d r a);
intros (d p x); cases x (t Ht); clear x;
generalize in match (mem_finType d t);
generalize in match (uniq_fintype_enum d);
intros (d p x); cases x (t Ht); clear x;
generalize in match (mem_finType d t);
generalize in match (uniq_fintype_enum d);
[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 [_ ⇒ ?|_ ⇒ ?] ?);
[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 [_ ⇒ ?|_ ⇒ ?] ?);
[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]
lapply (uniq_mem ? ? ? H1);
generalize in match Ht;
rewrite > Ett1; intros (Ht1'); clear Ht1;
generalize in match Hletin; elim l; [ reflexivity]
[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]
lapply (uniq_mem ? ? ? H1);
generalize in match Ht;
rewrite > Ett1; intros (Ht1'); clear Ht1;
generalize in match Hletin; elim l; [ reflexivity]
[1: generalize in match H5; cases s; simplify; intros; clear H5;
unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; rewrite > H7; simplify in H4;
[1: generalize in match H5; cases s; simplify; intros; clear H5;
unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
simplify; rewrite > H7; simplify in H4;
simplify; intros; [destruct H6] assumption;]
|2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption]
|2:rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
simplify; intros; [destruct H6] assumption;]
|2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption]
|2:rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]