Set Warnings "-extraction-opaque-accessed,-extraction".
Set Warnings "-notation-overridden,-parsing".

Require Import ZArith.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrfun ssrbool ssrnat eqtype seq.

From QuickChick Require Import
     GenLow GenLowInterface
     GenHighImpl GenHighInterface
     RandomQC Tactics Sets.

Set Bullet Behavior "Strict Subproofs".

Import GenLow.
Module Import GenHigh := GenHighImpl.Impl GenLow.

Import QcDefaultNotation.

Lemma oneOf_freq {A} (g : G A) (gs : list (G A)) size :
  semGenSize (oneOf (g ;; gs)) size <-->
  semGenSize (freq ((1, g) ;; map (fun x => (1, x)) gs)) size.
Proof.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs))) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  rewrite semOneofSize semFrequencySize /=.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) l) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  elim : gs => [| g' gs IHgs ] /=.
  - rewrite !cons_set_eq !nil_set_eq !setU_set0_neut !bigcup_set1.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    now apply set_eq_refl.
  - rewrite !cons_set_eq.
    rewrite setU_assoc (setU_comm [set g] [set g']) -setU_assoc -cons_set_eq
            bigcup_setU_l IHgs.
    rewrite setU_assoc (setU_comm [set (1, g)] [set (1, g')])
            -setU_assoc -cons_set_eq bigcup_setU_l.
(* Goal: @set_eq S (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) *)
    eapply setU_set_eq_compat.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs))) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    rewrite !bigcup_set1.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    now apply set_eq_refl. now apply set_eq_refl.
Qed.

Lemma semFreq :
  forall {A : Type} (ng : nat * G A) (l : seq (nat * G A)),
    List.Forall (fun x => x.1 > 0) (ng :: l) ->
    semGen (freq ((fst ng, snd ng) ;; l)) <-->
    \bigcup_(x in (ng :: l)) semGen x.2.
Proof.
(* Goal: forall (A : Type) (ng : prod nat (G A)) (l : list (prod nat (G A))) (_ : @List.Forall (prod nat (G A)) (fun x : prod nat (G A) => is_true (ssrnat.leq (S O) (@fst nat (G A) x))) (@cons (prod nat (G A)) ng l)), @set_eq A (@semGen A (@freq_ A (@snd nat (G A) (@pair nat (G A) (@fst nat (G A) ng) (@snd nat (G A) ng))) (@cons (prod nat (G A)) (@pair nat (G A) (@fst nat (G A) ng) (@snd nat (G A) ng)) l))) (@bigcup (prod nat (G A)) A (@seq_In (prod nat (G A)) (@cons (prod nat (G A)) ng l)) (fun x : prod nat (G A) => @semGen A (@snd nat (G A) x))) *)
  intros S ng l Hall.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs))) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  rewrite semFrequency. simpl.
(* Goal: @set_eq S match (if negb (@eq_op nat_eqType (@fst nat (G S) ng) O) then @cons (prod nat (G S)) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng)) (@filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l) else @filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l) with | nil => @semGenSize S (@snd nat (G S) ng) s | cons p l0 => @bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (if negb (@eq_op nat_eqType (@fst nat (G S) ng) O) then @cons (prod nat (G S)) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng)) (@filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l) else @filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l)) (fun x : prod nat (G S) => @semGenSize S (@snd nat (G S) x) s) end (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) ng l)) (fun x : prod nat (G S) => @semGenSize S (@snd nat (G S) x) s)) *)
  inversion Hall as [| x xs H1 H2 Heq1]; subst. clear Hall.
(* Goal: @set_eq S (let l' := @filter (prod (Equality.sort nat_eqType) (G S)) (fun x : prod (Equality.sort nat_eqType) (G S) => negb (@eq_op nat_eqType (@fst (Equality.sort nat_eqType) (G S) x) O)) (@cons (prod nat (G S)) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng)) l) in match l' with | nil => @semGenSize S (@snd nat (G S) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng))) s | cons p l => @bigcup (prod (Equality.sort nat_eqType) (G S)) S (@seq_In (prod (Equality.sort nat_eqType) (G S)) l') (fun x : prod (Equality.sort nat_eqType) (G S) => @semGenSize S (@snd (Equality.sort nat_eqType) (G S) x) s) end) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) ng l)) (fun x : prod nat (G S) => @semGenSize S (@snd nat (G S) x) s)) *)
  destruct ng as [n g]; simpl.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (if negb (@eq_op nat_eqType (@fst nat (G S) (@pair nat (G S) xn xg)) O) then @cons (prod nat (G S)) (@pair nat (G S) xn xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs) else (fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) xn xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  case : n H1 => [| n ] //= H1.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs))) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  rewrite !cons_set_eq !bigcup_setU_l.
(* Goal: @set_eq S (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) *)
  eapply setU_set_eq_compat.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  now apply set_eq_refl.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) l) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  elim : l H2 => [| x xs IHxs] H2.
  - rewrite !nil_set_eq //=.
  - unfold filter. inv H2.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs) else (fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) x xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    destruct x as [xn xg].
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (if negb (@eq_op nat_eqType (@fst nat (G S) (@pair nat (G S) xn xg)) O) then @cons (prod nat (G S)) (@pair nat (G S) xn xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs) else (fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) xn xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    case : xn H2 H3 => [| xn] //= H2 H3.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs))) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    rewrite !cons_set_eq !bigcup_setU_l.
(* Goal: @set_eq S (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) *)
    eapply setU_set_eq_compat.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    now apply set_eq_refl.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    eapply IHxs. eassumption.
Qed.

Lemma semFreqSize :
  forall {A : Type} (ng : nat * G A) (l : seq (nat * G A)) (size : nat),
    List.Forall (fun x => x.1 > 0) (ng :: l) ->
    semGenSize (freq ((fst ng, snd ng) ;; l)) size <-->
    \bigcup_(x in (ng :: l)) semGenSize x.2 size.
Proof.
(* Goal: forall (A : Type) (ng : prod nat (G A)) (l : list (prod nat (G A))) (size : nat) (_ : @List.Forall (prod nat (G A)) (fun x : prod nat (G A) => is_true (ssrnat.leq (S O) (@fst nat (G A) x))) (@cons (prod nat (G A)) ng l)), @set_eq A (@semGenSize A (@freq_ A (@snd nat (G A) (@pair nat (G A) (@fst nat (G A) ng) (@snd nat (G A) ng))) (@cons (prod nat (G A)) (@pair nat (G A) (@fst nat (G A) ng) (@snd nat (G A) ng)) l)) size) (@bigcup (prod nat (G A)) A (@seq_In (prod nat (G A)) (@cons (prod nat (G A)) ng l)) (fun x : prod nat (G A) => @semGenSize A (@snd nat (G A) x) size)) *)
  intros S ng l s Hall.
(* Goal: @set_eq S (let l' := @filter (prod (Equality.sort nat_eqType) (G S)) (fun x : prod (Equality.sort nat_eqType) (G S) => negb (@eq_op nat_eqType (@fst (Equality.sort nat_eqType) (G S) x) O)) (@cons (prod nat (G S)) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng)) l) in match l' with | nil => @semGenSize S (@snd nat (G S) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng))) s | cons p l => @bigcup (prod (Equality.sort nat_eqType) (G S)) S (@seq_In (prod (Equality.sort nat_eqType) (G S)) l') (fun x : prod (Equality.sort nat_eqType) (G S) => @semGenSize S (@snd (Equality.sort nat_eqType) (G S) x) s) end) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) ng l)) (fun x : prod nat (G S) => @semGenSize S (@snd nat (G S) x) s)) *)
  rewrite semFrequencySize. simpl.
(* Goal: @set_eq S match (if negb (@eq_op nat_eqType (@fst nat (G S) ng) O) then @cons (prod nat (G S)) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng)) (@filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l) else @filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l) with | nil => @semGenSize S (@snd nat (G S) ng) s | cons p l0 => @bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (if negb (@eq_op nat_eqType (@fst nat (G S) ng) O) then @cons (prod nat (G S)) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng)) (@filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l) else @filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l)) (fun x : prod nat (G S) => @semGenSize S (@snd nat (G S) x) s) end (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) ng l)) (fun x : prod nat (G S) => @semGenSize S (@snd nat (G S) x) s)) *)
  inversion Hall as [| x xs H1 H2 Heq1]; subst. clear Hall.
(* Goal: @set_eq S (let l' := @filter (prod (Equality.sort nat_eqType) (G S)) (fun x : prod (Equality.sort nat_eqType) (G S) => negb (@eq_op nat_eqType (@fst (Equality.sort nat_eqType) (G S) x) O)) (@cons (prod nat (G S)) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng)) l) in match l' with | nil => @semGenSize S (@snd nat (G S) (@pair nat (G S) (@fst nat (G S) ng) (@snd nat (G S) ng))) s | cons p l => @bigcup (prod (Equality.sort nat_eqType) (G S)) S (@seq_In (prod (Equality.sort nat_eqType) (G S)) l') (fun x : prod (Equality.sort nat_eqType) (G S) => @semGenSize S (@snd (Equality.sort nat_eqType) (G S) x) s) end) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) ng l)) (fun x : prod nat (G S) => @semGenSize S (@snd nat (G S) x) s)) *)
  destruct ng as [n g]; simpl.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (if negb (@eq_op nat_eqType (@fst nat (G S) (@pair nat (G S) xn xg)) O) then @cons (prod nat (G S)) (@pair nat (G S) xn xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs) else (fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) xn xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  case : n H1 => [| n ] //= H1.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs))) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  rewrite !cons_set_eq !bigcup_setU_l.
(* Goal: @set_eq S (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) *)
  eapply setU_set_eq_compat.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  now apply set_eq_refl.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@filter (prod nat (G S)) (fun x : prod nat (G S) => negb (@eq_op nat_eqType (@fst nat (G S) x) O)) l)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) l) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
  elim : l H2 => [| x xs IHxs] H2.
  - rewrite !nil_set_eq //=.
  - unfold filter. inv H2.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs) else (fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) x xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    destruct x as [xn xg].
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (if negb (@eq_op nat_eqType (@fst nat (G S) (@pair nat (G S) xn xg)) O) then @cons (prod nat (G S)) (@pair nat (G S) xn xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs) else (fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) xn xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    case : xn H2 H3 => [| xn] //= H2 H3.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs))) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) (@cons (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    rewrite !cons_set_eq !bigcup_setU_l.
(* Goal: @set_eq S (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) (@setU S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s))) *)
    eapply setU_set_eq_compat.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@set1 (prod nat (G S)) (@pair nat (G S) (Datatypes.S xn) xg)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    now apply set_eq_refl.
(* Goal: @set_eq S (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) ((fix filter (s : list (prod nat (G S))) : list (prod nat (G S)) := match s with | nil => @nil (prod nat (G S)) | cons x s' => if negb (@eq_op nat_eqType (@fst nat (G S) x) O) then @cons (prod nat (G S)) x (filter s') else filter s' end) xs)) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) (@bigcup (prod nat (G S)) S (@seq_In (prod nat (G S)) xs) (fun i : prod nat (G S) => @semGenSize S (@snd nat (G S) i) s)) *)
    eapply IHxs. eassumption.
Qed.


Lemma bigcup_cons_setI_subset_compat_backtrack_weak
      {A} (n : nat) (g g' : G (option A)) (l l' : seq (nat * G (option A))) :
  (forall s, isSome :&: semGenSize g s  \subset isSome :&: semGenSize g' s) ->
  (forall s, \bigcup_(x in (l :&: (fun x => x.1 <> 0))) (isSome :&: semGenSize x.2 s) \subset
        \bigcup_(x in (l' :&: (fun x => x.1 <> 0))) (isSome :&: semGenSize x.2 s)) ->
  (forall s, \bigcup_(x in (((n, g) :: l) :&: (fun x => x.1 <> 0))) (isSome :&: semGenSize x.2 s) \subset
        \bigcup_(x in (((n, g') :: l') :&: (fun x => x.1 <> 0))) (isSome :&: semGenSize x.2 s)).
Proof.
(* Goal: forall (_ : forall s : nat, @set_incl (option A) (@bigcup (prod nat (G (option A))) (option A) (@setI (prod nat (G (option A))) (@seq_In (prod nat (G (option A))) l) (fun x : prod nat (G (option A)) => not (@eq nat (@fst nat (G (option A)) x) O))) (fun x : prod nat (G (option A)) => @setI (option A) (fun u : option A => is_true (@isSome A u)) (@semGenSize (option A) (@snd nat (G (option A)) x) s))) (@bigcup (prod nat (G (option A))) (option A) (@setI (prod nat (G (option A))) (@seq_In (prod nat (G (option A))) l') (fun x : prod nat (G (option A)) => not (@eq nat (@fst nat (G (option A)) x) O))) (fun x : prod nat (G (option A)) => @setI (option A) (fun u : option A => is_true (@isSome A u)) (@semGenSize (option A) (@snd nat (G (option A)) x) s)))) (s : nat), @set_incl (option A) (@bigcup (prod nat (G (option A))) (option A) (@setI (prod nat (G (option A))) (@seq_In (prod nat (G (option A))) l) (fun x : prod nat (G (option A)) => not (@eq nat (@fst nat (G (option A)) x) O))) (fun x : prod nat (G (option A)) => @setI (option A) (fun u : option A => is_true (@isSome A u)) (@semGenSize (option A) (@snd nat (G (option A)) x) s))) (@bigcup (prod nat (G (option A))) (option A) (@setI (prod nat (G (option A))) (@seq_In (prod nat (G (option A))) (@cons (prod nat (G (option A))) (@pair nat (G (option A)) n g) l')) (fun x : prod nat (G (option A)) => not (@eq nat (@fst nat (G (option A)) x) O))) (fun x : prod nat (G (option A)) => @setI (option A) (fun u : option A => is_true (@isSome A u)) (@semGenSize (option A) (@snd nat (G (option A)) x) s))) *)
  intros. eapply bigcup_cons_setI_subset_compat_backtrack; eauto.
Qed.

Lemma bigcup_cons_setI_subset_pres_backtrack_weak
      {A} (n : nat) (g : G (option A)) (l l' : seq (nat * G (option A))) :
  (forall s, \bigcup_(x in (l :&: (fun x => x.1 <> 0))) (isSome :&: semGenSize x.2 s) \subset
        \bigcup_(x in (l' :&: (fun x => x.1 <> 0))) (isSome :&: semGenSize x.2 s)) ->
  (forall s, \bigcup_(x in (l :&: (fun x => x.1 <> 0))) (isSome :&: semGenSize x.2 s) \subset
         \bigcup_(x in ((n, g) :: l') :&: (fun x => x.1 <> 0)) (isSome :&: semGenSize x.2 s)).
Proof.
(* Goal: forall (_ : forall s : nat, @set_incl (option A) (@bigcup (prod nat (G (option A))) (option A) (@setI (prod nat (G (option A))) (@seq_In (prod nat (G (option A))) l) (fun x : prod nat (G (option A)) => not (@eq nat (@fst nat (G (option A)) x) O))) (fun x : prod nat (G (option A)) => @setI (option A) (fun u : option A => is_true (@isSome A u)) (@semGenSize (option A) (@snd nat (G (option A)) x) s))) (@bigcup (prod nat (G (option A))) (option A) (@setI (prod nat (G (option A))) (@seq_In (prod nat (G (option A))) l') (fun x : prod nat (G (option A)) => not (@eq nat (@fst nat (G (option A)) x) O))) (fun x : prod nat (G (option A)) => @setI (option A) (fun u : option A => is_true (@isSome A u)) (@semGenSize (option A) (@snd nat (G (option A)) x) s)))) (s : nat), @set_incl (option A) (@bigcup (prod nat (G (option A))) (option A) (@setI (prod nat (G (option A))) (@seq_In (prod nat (G (option A))) l) (fun x : prod nat (G (option A)) => not (@eq nat (@fst nat (G (option A)) x) O))) (fun x : prod nat (G (option A)) => @setI (option A) (fun u : option A => is_true (@isSome A u)) (@semGenSize (option A) (@snd nat (G (option A)) x) s))) (@bigcup (prod nat (G (option A))) (option A) (@setI (prod nat (G (option A))) (@seq_In (prod nat (G (option A))) (@cons (prod nat (G (option A))) (@pair nat (G (option A)) n g) l')) (fun x : prod nat (G (option A)) => not (@eq nat (@fst nat (G (option A)) x) O))) (fun x : prod nat (G (option A)) => @setI (option A) (fun u : option A => is_true (@isSome A u)) (@semGenSize (option A) (@snd nat (G (option A)) x) s))) *)
  intros. eapply bigcup_cons_setI_subset_pres_backtrack; eauto.
Qed.
