- intros 1 (m); elim m (Hm Hn p IH Hm Hn);
- [ destruct Hm;
- | simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
- (* XXX simplify che spacca troppo *)
- fold simplify (filter nat_eqType (sigma nat_eqType (λx.ltb x bound))
- (if_p nat_eqType (λx.ltb x bound)) (iota O p));
- [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?);
- unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
- simplify in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
- generalize in match (refl_eq ? (eqb n p));
- generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b);
- cases b; simplify;
- [2:intros (Enp); rewrite > IH; [1,3: auto]
- rewrite < ltb_n_Sm in Hm; rewrite > Enp in Hm;
- generalize in match Hm; cases (ltb n p); intros; [1:reflexivity]
- simplify in H1; destruct H1;
- |1:clear IH; intros (Enp);
- fold simplify (count fsort (cmp fsort {n, Hn})
- (filter ? (sigma nat_eqType (λx.ltb x bound))
- (if_p nat_eqType (λx.ltb x bound)) (iota O p)));
- rewrite > (count_O fsort); [1: reflexivity]
- intros 1 (x);
- rewrite < (b2pT ? ? (eqP ? n ?) Enp);
- cases x (y Hy); intros (ABS); clear x;
- unfold segment; unfold notb; simplify;
- generalize in match (refl_eq ? (cmp ? n y));
- generalize in match (cmp ? n y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
- intros (Eny); simplify; [2: auto]
- rewrite < ABS; symmetry; clear ABS;
- generalize in match Hy; clear Hy; rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny);
- simplify; intros (Hn); fold simplify (iota O n);
- apply (mem_filter nat_eqType fsort);
- intros (w Hw);
- fold simplify (sort nat_eqType);
- 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;
- 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]
- |2:rewrite > IH; [1:reflexivity|3:assumption]
- rewrite < ltb_n_Sm in Hm;
- cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption]
- rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn;
- rewrite > Hn in H; cases (H ?); reflexivity;
- ]]]
+ 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 [_ ⇒ ?|_ ⇒ ?] ?);
+ 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;
+ rewrite > orbC in Hm; assumption;
+ |1:clear IH; rewrite > (count_O fsort); [reflexivity]
+ intros 1 (x); rewrite < Enp; cases x (y Hy);
+ intros (ABS); clear x; unfold segment; unfold notb; simplify;
+ apply (cmpP ? n y); intros (Eny); simplify; [2:reflexivity]
+ rewrite < ABS; symmetry; clear ABS;
+ generalize in match Hy; clear Hy;rewrite < Eny;
+ simplify; intros (Hn); apply (mem_filter nat_eqType fsort); intros (w Hw);
+ 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;
+ 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]
+ |2:rewrite > IH; [1:reflexivity|3:assumption]
+ rewrite < ltb_n_Sm in Hm;
+ cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption]
+ rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn;
+ rewrite > Hn in H; cases (H ?); reflexivity]]