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

From Coq Require Import
     Arith
     Basics
     List
     Recdef
     ZArith.
From mathcomp Require Import
     ssrbool
     ssreflect
     ssrnat.
From QuickChick Require Import
     Classes
     GenLow
     GenHigh
     Sets.

Import GenHigh
       GenLow
       ListNotations
       QcDefaultNotation.

Set Bullet Behavior "Strict Subproofs".

(** Basic generator instances *)
Global Instance genBoolSized : GenSized bool :=
  {| arbitrarySized x := choose (false, true) |}.

Instance genNatSized : GenSized nat :=
  {| arbitrarySized x := choose (0,x) |}.

Global Instance genZSized : GenSized Z :=
  {| arbitrarySized x := let z := Z.of_nat x in
                         choose (-z, z)%Z |}.

Global Instance genNSized : GenSized N :=
  {| arbitrarySized x := let n := N.of_nat x in
                         choose (N0, n) |}.

Global Instance genListSized {A : Type} `{GenSized A} : GenSized (list A) :=
  {| arbitrarySized x := vectorOf x (arbitrarySized x) |}.

(* [3] is a lower priority than [Classes.GenOfGenSized],
   avoiding an infinite loop in typeclass resolution. *)

Global Instance genList {A : Type} `{Gen A} : Gen (list A) | 3 :=
  {| arbitrary := listOf arbitrary |}.

Global Instance genOption {A : Type} `{Gen A} : Gen (option A) | 3 :=
  {| arbitrary := freq [ (1, returnGen None)
                       ; (7, liftGen Some arbitrary)] |}.

Global Instance genPairSized {A B : Type} `{GenSized A} `{GenSized B}
: GenSized (A*B) :=
  {| arbitrarySized x :=
       liftGen2 pair (arbitrarySized x)
                     (arbitrarySized x)
  |}.

Global Instance genPair {A B : Type} `{Gen A} `{Gen B} : Gen (A * B) :=
  {| arbitrary := liftGen2 pair arbitrary arbitrary |}.

(** Shrink Instances *)
Global Instance shrinkBool : Shrink bool :=
  {| shrink x :=
       match x with
         | false => nil
         | true  => cons false nil
       end
  |}.

(** Shrinking of nat starts to become annoying *)
Function shrinkNatAux (x : nat) {measure (fun x => x) x} : list nat :=
  match x with
    | O => nil
    | S n =>
      let x' := Nat.div x 2 in
      x' :: shrinkNatAux x'
  end.
Proof.
  move => x n Eq;
  pose proof (Nat.divmod_spec n 1 0 0) as H.
  assert (H' : (0 <= 1)%coq_nat) by omega; apply H in H';
  subst; simpl in *; clear H.
(* Goal: not (@eq nat (S (S O)) O) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.div2 (Pos.to_nat xH))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.pred (Nat.div2 (Pos.to_nat xH)))) *)
  destruct (Nat.divmod n 1 0 0) as [q u];  destruct u; simpl in *; omega.
Defined.

Global Instance shrinkNat : Shrink nat :=
  {| shrink := shrinkNatAux |}.

(** Shrinking of Z is even more so *)
Lemma abs_div2_pos : forall p, Z.abs_nat (Z.div2 (Z.pos p)) = Nat.div2 (Pos.to_nat p).
Proof.
(* Goal: forall p : positive, or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg p)))) (Nat.div2 (Pos.to_nat p))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg p)))) (Nat.pred (Nat.div2 (Pos.to_nat p)))) *)
  intros. destruct p.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
    rewrite /Z.div2 /Pos.div2.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
      rewrite /Z.abs_nat. rewrite Pos2Nat.inj_xI.
(* Goal: @eq nat (Pos.to_nat p) (Nat.div2 (S (Init.Nat.mul (S (S O)) (Pos.to_nat p)))) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg (xO p))))) (Nat.div2 (Pos.to_nat (xO p)))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg (xO p))))) (Nat.pred (Nat.div2 (Pos.to_nat (xO p))))) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.div2 (Pos.to_nat xH))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.pred (Nat.div2 (Pos.to_nat xH)))) *)
      rewrite <- Nat.add_1_r. rewrite mult_comm.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
      rewrite Nat.div2_div. rewrite Nat.div_add_l; simpl; omega.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
    rewrite /Z.div2 /Pos.div2.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
      rewrite /Z.abs_nat. rewrite Pos2Nat.inj_xO.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
      rewrite mult_comm. rewrite Nat.div2_div. rewrite Nat.div_mul. reflexivity. omega.
(* Goal: @set1 (prod A B) (@prod_curry A B (prod A B) (@pair A B) (@pair A B a b)) (@pair A B a b) *)
  reflexivity.
Qed.

Lemma neg_succ : forall p,
  Z.neg (Pos.succ p) = Z.pred (Z.neg p).
Proof.
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
  move => p. rewrite <- Pos.add_1_r.
(* Goal: @eq Z (Zneg (Pos.add p xH)) (Z.pred (Zneg p)) *)
  rewrite <- Pos2Z.add_neg_neg.
(* Goal: @eq Z (Z.add (Zneg p) (Zneg xH)) (Z.pred (Zneg p)) *)
  rewrite <- Z.sub_1_r.
(* Goal: @set1 (prod A B) (@prod_curry A B (prod A B) (@pair A B) (@pair A B a b)) (@pair A B a b) *)
  reflexivity.
Qed.

Lemma neg_pred : forall p, (p > 1)%positive ->
  Z.neg (Pos.pred p) = Z.succ (Z.neg p).
Proof.
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
  move => p Hp. destruct p using Pos.peano_ind. by inversion Hp.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
  rewrite Pos.pred_succ. rewrite neg_succ. rewrite Z.succ_pred.
(* Goal: @set1 (prod A B) (@prod_curry A B (prod A B) (@pair A B) (@pair A B a b)) (@pair A B a b) *)
  reflexivity.
Qed.

Lemma abs_succ_neg : forall p,
  Z.abs_nat (Z.succ (Z.neg p)) = Nat.pred (Pos.to_nat p).
Proof.
(* Goal: @set1 (prod A B) (@prod_curry A B (prod A B) (@pair A B) (@pair A B a b)) (@pair A B a b) *)
  move => p. destruct p using Pos.peano_ind. reflexivity.
(* Goal: @set1 (prod A B) (@prod_curry A B (prod A B) (@pair A B) (@pair A B a b)) (@pair A B a b) *)
  rewrite -neg_pred /Z.abs_nat. rewrite Pos2Nat.inj_pred. reflexivity.
(* Goal: Pos.lt xH (Pos.succ p) *)
(* Goal: Pos.gt (Pos.succ p) xH *)
  apply Pos.lt_1_succ. apply Pos.lt_gt; apply Pos.lt_1_succ.
Qed.

Lemma abs_succ_div2_neg : forall p,
  Z.abs_nat (Z.succ (Z.div2 (Z.neg p))) = Nat.div2 (Pos.to_nat p) \/
  Z.abs_nat (Z.succ (Z.div2 (Z.neg p))) = Nat.pred (Nat.div2 (Pos.to_nat p)).
Proof.
(* Goal: forall p : positive, or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg p)))) (Nat.div2 (Pos.to_nat p))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg p)))) (Nat.pred (Nat.div2 (Pos.to_nat p)))) *)
  intros. destruct p.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
    left. rewrite /Z.div2 /Pos.div2.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
      rewrite neg_succ. rewrite <- Zsucc_pred. rewrite /Z.abs_nat. rewrite Pos2Nat.inj_xI.
(* Goal: @eq nat (Pos.to_nat p) (Nat.div2 (S (Init.Nat.mul (S (S O)) (Pos.to_nat p)))) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg (xO p))))) (Nat.div2 (Pos.to_nat (xO p)))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg (xO p))))) (Nat.pred (Nat.div2 (Pos.to_nat (xO p))))) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.div2 (Pos.to_nat xH))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.pred (Nat.div2 (Pos.to_nat xH)))) *)
      rewrite <- Nat.add_1_r. rewrite mult_comm.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
      rewrite Nat.div2_div. rewrite Nat.div_add_l; simpl; omega.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
    right. rewrite /Z.div2 /Pos.div2.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
      rewrite Pos2Nat.inj_xO. rewrite mult_comm.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
      rewrite Nat.div2_div. rewrite Nat.div_mul. simpl.
(* Goal: not (@eq nat (S (S O)) O) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.div2 (Pos.to_nat xH))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.pred (Nat.div2 (Pos.to_nat xH)))) *)
      apply abs_succ_neg. omega.
(* Goal: @set1 (prod A B) (@prod_curry A B (prod A B) (@pair A B) (@pair A B a b)) (@pair A B a b) *)
  left. simpl. reflexivity.
Qed.

Function shrinkZAux (x : Z) {measure (fun x => Z.abs_nat x) x}: list Z :=
  match x with
    | Z0 => nil
    | Zpos _ => rev (cons (Z.pred x) (cons (Z.div2 x) (shrinkZAux (Z.div2 x))))
    | Zneg _ => rev (cons (Z.succ x) (cons (Z.succ (Z.div2 x)) (shrinkZAux (Z.succ (Z.div2 x)))))
  end.
Proof.
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
  move => ? p ?. subst. rewrite abs_div2_pos. rewrite Zabs2Nat.inj_pos.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
    rewrite Nat.div2_div. apply Nat.div_lt. apply Pos2Nat.is_pos. omega.
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
  move => ? p ?. subst. destruct (abs_succ_div2_neg p) as [H | H].
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
    rewrite {}H /Z.abs_nat. rewrite Nat.div2_div.
(* Goal: not (@eq nat (S (S O)) O) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.div2 (Pos.to_nat xH))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.pred (Nat.div2 (Pos.to_nat xH)))) *)
      apply Nat.div_lt. apply Pos2Nat.is_pos. omega.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
    rewrite {}H /Z.abs_nat. eapply le_lt_trans. apply le_pred_n. rewrite Nat.div2_div.
(* Goal: not (@eq nat (S (S O)) O) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.div2 (Pos.to_nat xH))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.pred (Nat.div2 (Pos.to_nat xH)))) *)
      apply Nat.div_lt. apply Pos2Nat.is_pos. omega.
Qed.

Global Instance shrinkZ : Shrink Z :=
  {| shrink := shrinkZAux |}.

Open Scope program_scope.

Global Instance shrinkN : Shrink N :=
  {| shrink := map Z.to_N ∘ shrink ∘ Z.of_N |}.

Fixpoint shrinkListAux {A : Type} (shr : A -> list A) (l : list A) : list (list A) :=
  match l with
    | nil => nil
    | cons x xs =>
      cons xs (map (fun xs' => cons x xs') (shrinkListAux shr xs))
           ++ (map (fun x'  => cons x' xs) (shr x ))
  end.

Global Instance shrinkList {A : Type} `{Shrink A} : Shrink (list A) :=
  {| shrink := shrinkListAux shrink |}.

Global Instance shrinkPair {A B} `{Shrink A} `{Shrink B} : Shrink (A * B) :=
  {|
    shrink := fun (p : A * B) =>
      let (a,b) := p in
      map (fun a' => (a',b)) (shrink a) ++ map (fun b' => (a,b')) (shrink b)
  |}.

Global Instance shrinkOption {A : Type} `{Shrink A} : Shrink (option A) :=
  {| shrink m :=
       match m with
         | None => []
         | Some x => None :: (map Some (shrink x))
       end
  |}.

(** Arbitraries are derived automatically! *)


(** Instance correctness *)

Program Instance arbNatMon : SizeMonotonic (@arbitrary nat _).
Next Obligation.
(* Goal: and (is_true (leq (@length A l) s)) (@set_incl A (@seq_In A l) (@semGenSize A (@arbitrary A G) s)) *)
  rewrite !semSizedSize !semChooseSize // => n /andP [/leP H1 /leP H2].
(* Goal: not (@eq nat (S (S O)) O) *)
(* Goal: or (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.div2 (Pos.to_nat xH))) (@eq nat (Z.abs_nat (Z.succ (Z.div2 (Zneg xH)))) (Nat.pred (Nat.div2 (Pos.to_nat xH)))) *)
  move : H => /leP => Hle. apply/andP. split; apply/leP; omega.
Qed.

(** Correctness proof about built-in generators *)

Instance boolSizeMonotonic : SizeMonotonic (@arbitrary bool _).
Proof.
(* Goal: @set_eq bool (@semGen bool (@arbitrary bool (@GenOfGenSized bool genBoolSized))) (@setT bool) *)
  unfold arbitrary, GenOfGenSized.
(* Goal: @SizeMonotonic bool (@sized bool (@arbitrarySized bool genBoolSized)) *)
  eapply sizedSizeMonotonic; unfold arbitrarySized, genBoolSized.
(* Goal: forall _ : nat, @SizeMonotonic bool (@choose bool RandomQC.ChooseBool (@pair bool bool false true)) *)
(* Goal: @SizedMonotonic bool (fun _ : nat => @choose bool RandomQC.ChooseBool (@pair bool bool false true)) *)
  intros _. eauto with typeclass_instances.
(* Goal: @SizedMonotonic bool (@arbitrarySized bool genBoolSized) *)
  intros n s1 s2 Hs. eapply subset_refl.
Qed.

Instance boolSizedMonotonic : SizedMonotonic (@arbitrarySized bool _).
Proof.
(* Goal: @SizedMonotonic bool (@arbitrarySized bool genBoolSized) *)
  intros n s1 s2 Hs. eapply subset_refl.
Qed.

Instance boolCorrect : Correct bool arbitrary.
Proof.
(* Goal: @set_eq bool (@semGen bool (@arbitrary bool (@GenOfGenSized bool genBoolSized))) (@setT bool) *)
  constructor. unfold arbitrary, GenOfGenSized.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
  rewrite semSized.
(* Goal: @set_eq bool (@bigcup nat bool (@setT nat) (fun s : nat => @semGenSize bool (@arbitrarySized bool genBoolSized s) s)) (@setT bool) *)
  unfold arbitrarySized, genBoolSized.
(* Goal: @set1 (option A) (@None A) (@None A) *)
  intros x. split; intros H; try now constructor.
(* Goal: @set1 (option A) (@None A) (@None A) *)
  exists 0. split. constructor.
(* Goal: @semGenSize bool (@choose bool RandomQC.ChooseBool (@pair bool bool false true)) O x *)
  eapply semChooseSize; eauto.
(* Goal: is_true (andb (@RandomQC.leq bool (@RandomQC.super bool RandomQC.ChooseBool) false x) (@RandomQC.leq bool (@RandomQC.super bool RandomQC.ChooseBool) x true)) *)
  destruct x; eauto.
Qed.

Lemma arbBool_correct:
  semGen arbitrary <--> [set: bool].
Proof.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
rewrite /arbitrary /arbitrarySized /genBoolSized /=.
(* Goal: @semGenSize bool (@choose bool RandomQC.ChooseBool (@pair bool bool false true)) (nat_of_bool n) n *)
rewrite semSized => n; split=> // _.
(* Goal: @bigcup nat bool (@setT nat) (fun s : nat => @semGenSize bool (@choose bool RandomQC.ChooseBool (@pair bool bool false true)) s) n *)
exists n; split=> //.
(* Goal: @semGenSize bool (@choose bool RandomQC.ChooseBool (@pair bool bool false true)) (nat_of_bool n) n *)
apply semChooseSize => //=; case n => //.
Qed.

Lemma arbNat_correct:
  semGen arbitrary <--> [set: nat].
Proof.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
rewrite /arbitrary /=.
(* Goal: @bigcup nat bool (@setT nat) (fun s : nat => @semGenSize bool (@choose bool RandomQC.ChooseBool (@pair bool bool false true)) s) n *)
rewrite semSized => n; split=> // _; exists n; split=> //.
(* Goal: forall _ : @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b), @setX A B (Sa s) (Sb s) (@pair A B a b) *)
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
by rewrite (semChooseSize _ _ _) /RandomQC.leq /=.
Qed.

Instance ArbNatGenCorrect : Correct nat arbitrary.
Proof.
(* Goal: @set1 (option A) (@None A) (@None A) *)
  constructor. now apply arbNat_correct.
Qed.

Lemma arbInt_correct s :
  semGenSize arbitrary s <-->
  [set z | (- Z.of_nat s <= z <= Z.of_nat s)%Z].
Proof.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
rewrite semSizedSize semChooseSize.
(* Goal: forall _ : @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b), @setX A B (Sa s) (Sb s) (@pair A B a b) *)
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
  by move=> n; split=> [/andP|] [? ?]; [|apply/andP]; split; apply/Zle_is_le_bool.
apply/(Zle_bool_trans _ 0%Z); apply/Zle_is_le_bool.
  exact/Z.opp_nonpos_nonneg/Zle_0_nat.
exact/Zle_0_nat.
Qed.

Lemma arbBool_correctSize s :
  semGenSize arbitrary s <--> [set: bool].
Proof.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
rewrite /arbitrary //=.
(* Goal: @set_eq bool (@semGenSize bool (@sized bool (fun _ : nat => @choose bool RandomQC.ChooseBool (@pair bool bool false true))) s) (@setT bool) *)
rewrite semSizedSize semChooseSize //; split=> /RandomQC.leq _ //=; case a=> //=.
Qed.

Lemma arbNat_correctSize s :
  semGenSize arbitrary s <--> [set n : nat | (n <= s)%coq_nat].
Proof.
(* Goal: forall _ : @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b), @setX A B (Sa s) (Sb s) (@pair A B a b) *)
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
by rewrite semSizedSize semChooseSize // => n /=; case: leP.
Qed.

Lemma arbInt_correctSize : semGen arbitrary <--> [set: Z].
Proof.
rewrite /arbitrarySized semSized => n; split=> // _; exists (Z.abs_nat n); split=> //.
(* Goal: @semGenSize (option A) (@snd nat (GenLow.G (option A)) (@pair nat (GenLow.G (option A)) (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S O))))))) (@liftGen A (option A) (@Some A) (@arbitrary A G)))) s (@Some A a) *)
simpl.
(* Goal: iff (@semGenSize (list A) (@arbitrary (list A) (@genList A G)) s l) (and (is_true (leq (@length A l) s)) (forall (x : A) (_ : @In A x l), P s x)) *)
rewrite Nat2Z.inj_abs_nat (semChooseSize _ _ _).
(* Goal: forall _ : @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b), @setX A B (Sa s) (Sb s) (@pair A B a b) *)
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
  by case: n => //= p; rewrite !Z.leb_refl.
apply/(Zle_bool_trans _ 0%Z); apply/Zle_is_le_bool.
  exact/Z.opp_nonpos_nonneg/Z.abs_nonneg.
exact/Z.abs_nonneg.
Qed.

Lemma arbList_correct:
  forall {A} `{H : Arbitrary A} (P : nat -> A -> Prop) s,
    (semGenSize arbitrary s <--> P s) ->
    (semGenSize arbitrary s <-->
     (fun (l : list A) => length l <= s /\ (forall x, List.In x l -> P s x))).
Proof.
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
  move => A G S H P s Hgen l. rewrite !/arbitrary //=.
(* Goal: iff (@imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b)) (@setX A B (Sa s) (Sb s) (@pair A B a b)) *)
  split.
  - move => /semListOfSize [Hl Hsize]. split => // x HIn //=. apply Hgen. auto.
  - move => [Hl HP]. apply semListOfSize. split => // x HIn.
(* Goal: @semGenSize A (@arbitrary A G) s x *)
    apply Hgen. auto.
Qed.

Lemma arbOpt_correct:
  forall {A} `{H : Arbitrary A} (P : nat -> A -> Prop) s,
    (semGenSize arbitrary s <--> P s) ->
    (semGenSize arbitrary s <-->
     (fun (m : option A) =>
        match m with
          | None => true
          | Some x => P s x
        end)).
Proof.
(* Goal: iff (@imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b)) (@setX A B (Sa s) (Sb s) (@pair A B a b)) *)
  move => A G S Arb P s Hgen m. rewrite !/arbitrary //=; split.
  - move => /semFrequencySize [[w g] H2]; simpl in *.
    move: H2 => [[H2 | [H2 | H2]] H3];
    destruct m => //=; apply Hgen => //=;
(* Goal: P s x *)
    inversion H2; subst; auto.
    + apply semReturnSize in H3; inversion H3.
    + apply semLiftGenSize in H3; inversion H3 as [x [H0 H1]].
(* Goal: P s x *)
      inversion H1; subst; auto.
  - destruct m eqn:Hm; simpl in *; move => HP; subst.
(* Goal: @semGenSize (option A) (@snd nat (GenLow.G (option A)) (@pair nat (GenLow.G (option A)) (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S O))))))) (@liftGen A (option A) (@Some A) (@arbitrary A G)))) s (@Some A a) *)
    + apply semFrequencySize; simpl.
(* Goal: P s x *)
      exists (7, liftGen Some arbitrary); split; auto.
(* Goal: P s x *)
      * right; left; auto.
(* Goal: @semGenSize (option A) (@snd nat (GenLow.G (option A)) (@pair nat (GenLow.G (option A)) (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S O))))))) (@liftGen A (option A) (@Some A) (@arbitrary A G)))) s (@Some A a) *)
      * simpl. apply semLiftGenSize; simpl.
(* Goal: P s x *)
        apply imset_in; apply Hgen; auto.
(* Goal: @semGenSize (option A) (@snd nat (GenLow.G (option A)) (@pair nat (GenLow.G (option A)) (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S O))))))) (@liftGen A (option A) (@Some A) (@arbitrary A G)))) s (@Some A a) *)
    + apply semFrequencySize; simpl.
(* Goal: P s x *)
      exists (1, returnGen None); split; auto.
(* Goal: P s x *)
      * left; auto.
(* Goal: @set1 (option A) (@None A) (@None A) *)
      * simpl; apply semReturnSize. constructor.
Qed.

Lemma arbPair_correctSize
      {A B} `{Arbitrary A} `{Arbitrary B} (Sa : nat -> set A)
      (Sb : nat -> set B) s:
    (semGenSize arbitrary s <--> Sa s) ->
    (semGenSize arbitrary s <--> Sb s) ->
    (semGenSize arbitrary s <--> setX (Sa s) (Sb s)).
Proof.
(* Goal: forall _ : @setX A B (Sa s) (Sb s) (@pair A B a b), @imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b) *)
  move => Hyp1 Hyp2 . rewrite semLiftGen2Size; move => [a b].
(* Goal: iff (@imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b)) (@setX A B (Sa s) (Sb s) (@pair A B a b)) *)
  split.
(* Goal: iff (@imset2 A B (prod A B) (@pair A B) (@semGenSize A (@arbitrary A H) s) (@semGenSize B (@arbitrary B H2) s) (@pair A B a b)) (@setX A B (Sa s) (Sb s) (@pair A B a b)) *)
  by move => [[a' b'] [[/= /Hyp1 Ha /Hyp2 Hb] [Heq1 Heq2]]]; subst; split.
(* Goal: P s x *)
  move => [/Hyp1 Ha /Hyp2 Hb]. eexists; split; first by split; eauto.
(* Goal: @set1 (prod A B) (@prod_curry A B (prod A B) (@pair A B) (@pair A B a b)) (@pair A B a b) *)
  reflexivity.
Qed.
