proposition: Lemma card_pset (s: nat) t: (forall p, StateSetSet.In p t -> setbelow p (state_of_nat s)) -> (StateSetSet.cardinal t <= power s)%nat.
proof: Proof. revert t. induction s; intros t H; simpl. destruct (StateSetSetProps.Props.cardinal_0 t) as (l&Hl&Hlt&->). setoid_rewrite Hlt in H. clear Hlt. revert H Hl. destruct l as [|x [| y q]]; intros H Hl; simpl; auto with arith. exfalso. inversion_clear Hl. apply H0. left. clear H0 H1. rewrite (@below0_empty x), (@below0_empty y). reflexivity. apply H. right. left. reflexivity. apply H. left. reflexivity. pose (t0 := StateSetSet.filter (fun p => StateSet.mem (state_of_nat s) p) t). pose (t1 := StateSetSet.filter (fun p => negb (StateSet.mem (state_of_nat s) p)) t). pose (t0' := statesetset_map (StateSet.remove (state_of_nat s)) t0). setoid_replace t with (StateSetSet.union t0 t1). rewrite StateSetSetProps.Props.union_cardinal. replace (StateSetSet.cardinal t0) with (StateSetSet.cardinal t0'). assert (IH1 := IHs t1). apply apply in IH1. assert (IH0 := IHs t0'). apply apply in IH0. lia. subst t0' t0. clear t1 IH1 IH0. intros p Hp. destruct (statesetset_map_in Hp) as [q Hq Hq']. revert Hq. rewrite StateSetSetProps.mem_iff. rewrite StateSetSetProps.EqProps.filter_mem by solve_p1. case_eq (StateSetSet.mem q t). 2:(intros; discriminate). simpl. intros Hq Hq''. intros x Hx. destruct (eq_num_dec x s). rewrite e, <- Hq' in Hx. exfalso. revert Hx. clear. StateSetProps.setdec. rewrite <- StateSetSetProps.mem_iff in Hq. rewrite <- StateSetProps.mem_iff in Hq''. specialize (H q Hq x). apply apply in H. clear - H n. num_lia. StateSetProps.setdec. subst t1. clear t0 t0' IH1. intro p. rewrite StateSetSetProps.mem_iff. rewrite StateSetSetProps.EqProps.filter_mem by solve_p1. case_eq (StateSetSet.mem p t). 2:(intros; discriminate). simpl. intros Hp Hp'. intros x Hx. destruct (eq_num_dec x s). subst. apply StateSet.mem_1 in Hx. rewrite Hx in Hp'. discriminate. apply StateSetSet.mem_2 in Hp. pose (H' := H p Hp x Hx). num_lia. subst t0' t0. clear t1. apply statesetset_map_cardinal. intros p q. setoid_rewrite StateSetSetProps.mem_iff. do 2 rewrite StateSetSetProps.EqProps.filter_mem by solve_p1. case (StateSetSet.mem p t). 2: (intros; discriminate). case (StateSetSet.mem q t). 2: (intros; discriminate). simpl. setoid_rewrite <- StateSetProps.mem_iff. try StateSetProps.setdec. split; intro Hpq. clear - H0 H1 Hpq. intro x. generalize (Hpq x). clear Hpq. StateSetProps.set_iff. destruct (eq_num_dec s x). subst. firstorder. firstorder. rewrite Hpq. reflexivity. subst t0 t1. clear t0'. intro x. setoid_rewrite StateSetSetProps.mem_iff. do 2 rewrite StateSetSetProps.EqProps.filter_mem by solve_p1. StateSetProps.mem_analyse; StateSetSetProps.mem_analyse; simpl; firstorder congruence. subst t0 t1. clear t0'. intro x. rewrite StateSetSetProps.EqProps.union_filter by trivial. setoid_rewrite StateSetSetProps.mem_iff. rewrite StateSetSetProps.EqProps.filter_mem by solve_p1. rewrite andb_comm. StateSetProps.mem_analyse; reflexivity. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)