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

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrbool ssrnat eqtype.
Require Import Show Sets GenLow GenHigh RoseTrees Checker Classes.

Import GenLow GenHigh QcNotation.

Definition resultSuccessful (r : Result) : bool :=
  match r with
    | MkResult (Some res) expected _ _ _ _ _ =>
      res == expected
    | _ => true
  end.

Definition successful qp :=
  match qp with
    | MkProp (MkRose res _) => resultSuccessful res
  end.

(* Maps a Checker to a Prop *)

(* begin semCheckerSize *)
Definition semCheckerSize (c : Checker) (s : nat): Prop :=
  successful @: semGenSize c s \subset [set true].
(* end semCheckerSize *)

(* ZP: Do we want to define semChecker in terms of semCheckerSize? *)

(* begin semChecker *)
Definition semChecker (c : Checker) : Prop := forall s, semCheckerSize c s.
(* end semChecker *)

(* Maps a Checkable to a Prop i.e. gives an equivalent proposition to the
   property under test *)

(* begin semCheckableSize *)
Definition semCheckableSize {A} `{Checkable A} (a : A) (s : nat) : Prop :=
  semCheckerSize (checker a) s.
(* end semCheckableSize *)

(* begin semCheckable *)
Definition semCheckable {A} `{Checkable A} (a : A) : Prop := semChecker (checker a).
(* end semCheckable *)

(* another characterization of semChecker *)
Lemma semChecker_def2 c :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semChecker c <-> (forall qp, semGen c qp -> successful qp = true).
Proof.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite /semChecker /semCheckerSize /semGen. split; intro H.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - intros. destruct H0 as [s [H0 Ho']]. symmetry; eapply (H s). eexists. 
    split; eauto.  reflexivity.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - intros n b [qp [H1 H2]]. symmetry in H2. 
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
    rewrite H2. symmetry. apply H.  
    eexists; eauto. split; eauto. reflexivity.
Qed.

(* CH: This is the definition of Checker I would like to use *)
(* ZP : For now semCheckerSize has a similar definition and 
        semChecker is defined in terms of semCheckerSize *)
Lemma semChecker_def3 c :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semChecker c <-> (successful @: semGen c \subset [set true]).
Proof.
(* Goal: iff (forall (qp : QProp) (_ : @semGen QProp c qp), @eq bool (successful qp) true) (@set_incl bool (@imset QProp bool successful (@semGen QProp c)) (@set1 bool true)) *)
  rewrite semChecker_def2. split; intro H.
(*  CH: why can't I rewrite with semFmap directly? See tentative instances below *)
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - intros b H'. unfold imset, bigcup in H'.
(* Goal: @set1 bool true b *)
(* Goal: forall (qp : QProp) (_ : @semGen QProp c qp), @eq bool (successful qp) true *)
    destruct H' as [qp [H1 H2]]. apply H in H1. by rewrite H1 in H2.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - intros. specialize (H (successful qp)).
(* Goal: @eq bool (successful qp) true *)
    unfold set1 in H. symmetry. apply: H.
(* Goal: semP s (a nat) *)
    by eapply imset_in. 
Qed.

Definition genChecker c := fmap successful c.

Class UnsizedChecker (c : Checker) :=
  {
    unsizedChecker : 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
      forall s1 s2 : nat, semGenSize (genChecker c) s1 <--> semGenSize (genChecker c) s2
  }.

Class SizeMonotonicChecker (c : Checker) :=
  {
    monotonicChecker : 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
      forall s1 s2, s1 <= s2 -> 
                    semGenSize (genChecker c) s1 \subset semGenSize (genChecker c) s2
                                           
  }.

Lemma unsizedChecker_alt_def (c : Checker) `{UnsizedChecker c} :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  forall s1 s2, semCheckerSize c s1 <-> semCheckerSize c s2.
Proof.
  rewrite /semCheckerSize => s1 s2; split;
  move : H => [/(_ s1 s2) H];
  rewrite /genChecker in H; setoid_rewrite semFmapSize in H;
(* Goal: semP s (a nat) *)
  by rewrite H.
Qed.

Lemma monotonicChecker_alt_def (c : Checker) `{SizeMonotonicChecker c} :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  forall s1 s2, s1 <= s2 -> semCheckerSize c s2 -> semCheckerSize c s1.
Proof.
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
  rewrite /semCheckerSize => s1 s2 Hle.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move : H => [/(_ s1 s2 Hle) /= H]. 
(* Goal: forall _ : @set_incl bool (@imset QProp bool successful (@semGenSize QProp c s2)) (@set1 bool true), @set_incl bool (@imset QProp bool successful (@semGenSize QProp c s1)) (@set1 bool true) *)
  rewrite /genChecker in H; setoid_rewrite semFmapSize in H.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move => H1 b H2. apply H1. eauto.
Qed.

Program Instance unsizedMonotonicChecker (c : Checker) `{UnsizedChecker c} : 
  SizeMonotonicChecker c.
Next Obligation. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    rewrite unsizedChecker. move => b Hb. by eauto. 
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma mapTotalResult_idSize {C} `{Checkable C} (f : Result -> Result) (c : C) s :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (forall res, resultSuccessful res = resultSuccessful (f res)) ->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (semCheckerSize (mapTotalResult f c) s <-> semCheckableSize c s).
Proof.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move=> eq_res. 
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite /mapTotalResult /mapRoseResult /mapProp/semCheckableSize /semCheckerSize. 
  split; rewrite semFmapSize. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H1 b [[[res l]] /= [H2 H3]].
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    rewrite -H3 eq_res. apply H1.
    repeat (eexists; split; eauto).
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => /= H1 b [[[res l]] /= [[[[res' l'] [/= H2 [H3 H4]]] H5]]]; subst.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    rewrite <- H5, <- eq_res in *.  apply H1.
    eexists. split; eauto. reflexivity.
Qed.


(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma mapTotalResult_id {C} `{Checkable C} (f : Result -> Result) (c : C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (forall res, resultSuccessful res = resultSuccessful (f res)) ->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (semChecker (mapTotalResult f c) <-> semCheckable c).
Proof.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  move=> eq_res; split => H' s; eapply mapTotalResult_idSize; eauto.
(* Goal: semP s (a nat) *)
  by apply H'.
Qed.


Lemma semCallback_idSize {C} `{Checkable C} (cb : Callback) (c : C) (s : nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (callback cb c) s <-> semCheckableSize c s.
Proof.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite /callback.
(* Goal: iff (semChecker (@forAllShrink A C H1 H2 gen sh f)) (forall (a : A) (_ : @semGen A gen a), @semCheckable C H1 (f a)) *)
  split; move => H'.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - apply mapTotalResult_idSize in H' => //;
(* Goal: semP s (a nat) *)
    by move => [? ? ? ? ? ?].
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - apply mapTotalResult_idSize => //;
(* Goal: semP s (a nat) *)
    by move => [? ? ? ? ? ?].
Qed.

Lemma semCallback_id {C} `{Checkable C} (cb : Callback) (c : C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semChecker (callback cb c) <-> semCheckable c.
Proof.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  split => H' s; eapply semCallback_idSize; eauto.
(* Goal: semP s (a nat) *)
  by apply H'.
Qed.

Lemma semWhenFail_idSize {C} `{Checkable C} (str : String.string) (c : C) s :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (whenFail str c) s <-> semCheckableSize c s.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /whenFail semCallback_idSize.
Qed.

Lemma semWhenFail_id {C} `{Checkable C} (str : String.string) (c : C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semChecker (whenFail str c) <-> semCheckable c.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /whenFail semCallback_id.
Qed.

Lemma semPrintTestCase_idSize {C} `{Checkable C} (str : String.string) (c : C) s :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (printTestCase str c) s <-> semCheckableSize c s.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /printTestCase semCallback_idSize.
Qed.

Lemma semPrintTestCase_id {C} `{Checkable C} (str : String.string) (c : C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semChecker (printTestCase str c) <-> semCheckable c.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /printTestCase semCallback_id.
Qed.

Lemma semShrinking_idSize {C A} {HCheck : Checkable C}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         (sh : A -> list A) (x : A) (pf : A -> C) (s : nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (shrinking sh x pf) s <->
    semCheckableSize (pf x) s.
Proof.
  unfold semCheckableSize, shrinking, semCheckerSize, semGenSize, props.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  have [n <-] : exists n, S n  = 1000 by eexists; reflexivity.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H b [[[res [l]]] [/= [seed Hgen] H']]; subst.
(* Goal: semCheckerSize (@checker C H1 (f a)) s' *)
(* Goal: semCheckerSize (@forAllShrink A C H1 H2 gen sh f) a *)
    + suff :
        successful
          (run
             (fmap
                (fun x0 => {| unProp := joinRose (fmapRose unProp x0) |})
                (promote (@props' _ _ HCheck (S n) pf sh x))) s seed).
      setoid_rewrite runFmap. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
      rewrite runPromote. simpl. rewrite Hgen -H' /=. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
      move => -> //. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
      rewrite <- H => //. eexists. split; try by reflexivity.
      eexists. reflexivity.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H b [[[r [l]]] /= [[seed H1] <-]]. apply H. 
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
    rewrite runFmap runPromote /= in H1.
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
    destruct ((run (checker (pf x)) s seed)) as [[res [l']]] eqn:Heq=> //=.
    simpl in *. move : H1 => [H1 H2]; subst.
    eexists. eexists. exists seed. reflexivity. rewrite Heq. reflexivity.
Qed.

Lemma semShrinking_id {C A} {HCheck : Checkable C}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         (sh : A -> list A) (x : A) (pf : A -> C)  :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semChecker (shrinking sh x pf) <->
    semCheckable (pf x).
Proof.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  split; move => H s; eapply semShrinking_idSize; first by eauto.
(* Goal: @set1 bool true (successful qp) *)
(* Goal: forall _ : forall (a : A) (_ : @semGenSize A gen s a), @set_incl bool (@imset QProp bool successful (@semGenSize QProp (f a) s)) (@set1 bool true), @set_incl bool (@imset QProp bool successful (@semGenSize QProp (@bindGen A QProp gen f) s)) (@set1 bool true) *)
  by apply H.
Qed.

(* Program Instance shrinkingUnsized {C A} `{Checkable C} *)
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
(*         (sh : A -> list A) (x : A) (pf : A -> C)  *)
(*         `{UnsizedChecker (checker (pf x))} : UnsizedChecker (shrinking sh x pf). *)
(* Next Obligation.  *)
(* Abort. *)

Lemma semCover_idSize {C} `{Checkable C} (b: bool) (n: nat)
      (str : String.string) (c : C) (s : nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semCheckerSize (cover b n str c) s <-> semCheckableSize c s.
Proof.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - rewrite /cover. case: b => //.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    move => H1. apply mapTotalResult_idSize in H1 => //.
(* Goal: semP s (a nat) *)
      by move => [? ? ? ? ? ?].
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H1. rewrite /cover. case: b => //.
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
    apply mapTotalResult_idSize => //.
(* Goal: semP s (a nat) *)
      by move => [? ? ? ? ? ?].
Qed.

Lemma semCover_id {C} `{Checkable C} (b: bool) (n: nat)
      (str : String.string) (c : C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semChecker (cover b n str c) <-> semCheckable c.
Proof.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  split; move => H' s; eapply semCover_idSize; first by eauto.
(* Goal: semP s (a nat) *)
  by apply H'.
Qed.

Lemma semClassify_idSize {C} `{Checkable C} (b: bool) (str : String.string)
          (c : C) (s : nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (classify b str c) s <-> semCheckableSize c s.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /classify semCover_idSize.
Qed.

Lemma semClassify_id {C} `{Checkable C} (b: bool) (str : String.string) (c : C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semChecker (classify b str c) <-> semCheckable c.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /classify semCover_id.
Qed.

Lemma semLabel_idSize {C} `{Checkable C} (str : String.string) (c : C) (s : nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (label str c) s <-> semCheckableSize c s.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /label semClassify_idSize.
Qed.

Lemma semLabel_id {C} `{Checkable C} (str : String.string) (c : C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semChecker (label str c) <-> semCheckable c.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /label semClassify_id.
Qed.

Lemma semCollect_idSize {C} `{Checkable C} (str : String.string) (c : C) (s : nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (collect str c) s <-> semCheckableSize c s.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /collect semLabel_idSize.
Qed.

Lemma semCollect_id {C} `{Checkable C} (str : String.string) (c : C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semChecker (collect str c) <-> semCheckable c.
Proof.
(* Goal: semP s (a nat) *)
  by rewrite /collect semLabel_id.
Qed.

Open Scope Checker_scope.

Lemma semImplicationSize {C} `{Checkable C} (c : C) (b : bool) s :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semCheckerSize (b ==> c) s <-> (b -> semCheckableSize c s).
Proof.
(* Goal: semCheckerSize (@checker C H (f a)) s *)
(* Goal: semChecker (@forAllShrink A C H H0 gen shrinker f) *)
  case: b; split=> //=; first by move/(_ refl_equal).
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  by move => _ b [x [/semReturnSize <- <-]].
Qed.

(* begin semImplication *)
Lemma semImplication {C} `{Checkable C} (c : C) (b : bool) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semChecker (b ==> c) <-> (b -> semCheckable c).
(* end semImplication *)
Proof.
  split; [move => H1 b' s' | move => H1 s b'];
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  eapply semImplicationSize; try by eauto.
(* Goal: @set1 bool true b *)
  move => b''. by apply H1.
Qed.

Program Instance implicationUnsized
        {C} `{Checkable C} b (c : C) `{UnsizedChecker (checker c)} : 
  UnsizedChecker (b ==> c).
Next Obligation.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move : H0 => [/(_ s1 s2) H0].
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  rewrite /genChecker in H0 *. rewrite -> !semFmapSize in H0. 
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite !semFmapSize.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  rewrite /implication. case : b; eauto.
(* Goal: @set_eq QProp (@set1 QProp qp) (@set1 QProp qp) *)
  apply imset_eq. rewrite !semReturnSize. reflexivity.
Qed.

Program Instance implicationMonotonic
        {C} `{Checkable C} b (c : C) `{SizeMonotonicChecker (checker c)} : 
  SizeMonotonicChecker (b ==> c).
Next Obligation.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move : H0 => [/(_ s1 s2 H1) H0].
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  rewrite /genChecker in H0 *. rewrite -> !semFmapSize in H0. 
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite !semFmapSize.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  rewrite /implication. case : b; eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  apply imset_incl. rewrite !semReturnSize. by move => ? ?; eauto.
Qed.
  
(* equivalences for other combinators *)

Lemma semReturnGenSize (qp : QProp) (s: nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (returnGen qp) s <-> semCheckableSize qp s.
Proof.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite /semCheckerSize. split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move =>  H qp' [x [H1 H2]]. apply H. eexists; split; eauto. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H b [x [H1 H2]] //. apply H => //=. eexists; split; eauto.
Qed.

Lemma semReturnGen (qp : QProp) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semChecker (returnGen qp) <-> semCheckable qp.
Proof. 
(* Goal: iff (semChecker (@forAllShrink A C H1 H2 gen sh f)) (forall (a : A) (_ : @semGen A gen a), @semCheckable C H1 (f a)) *)
  split; move => H s.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - by move /(_ s) /semReturnGenSize : H => //. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - apply semReturnGenSize; eauto. by apply H.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semBindGenSize {A} (gen : G A) (f : A -> Checker) (s: nat):
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (bindGen gen f) s <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    forall a, semGenSize gen s a -> semCheckerSize (f a) s.
Proof.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  unfold semCheckerSize. split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H a Hsize b [qp [H1 <-]]. apply H.
    exists qp; split => //=. apply semBindSize. eexists; split; eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H b [qp [/semBindSize [a [H1 H2]] <-]]. eapply H; try eassumption.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eexists; split => //; eauto.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semBindGenUsinzed1 {A} (gen : G A) (f : A -> Checker) `{Unsized _ gen} :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (semChecker (bindGen gen f) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
     forall a, semGen gen a -> semChecker (f a)).
Proof.
(* Goal: iff (semChecker (@forAllShrink A C H1 H2 gen sh f)) (forall (a : A) (_ : @semGen A gen a), @semCheckable C H1 (f a)) *)
  split; move => Hgen a.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => [s [_ H']] s'. eapply unsized in H'.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    by eapply semBindGenSize in Hgen; eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - by eapply semBindGenSize; intros; apply Hgen; eexists; split => //; eauto.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semBindGenUsinzed2 {A} (gen : G A) (f : A -> Checker) 
      `{forall a, UnsizedChecker (f a)} :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (semChecker (bindGen gen f) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
     forall a, semGen gen a -> semChecker (f a)).
Proof.
(* Goal: iff (semChecker (@forAllShrink A C H1 H2 gen sh f)) (forall (a : A) (_ : @semGen A gen a), @semCheckable C H1 (f a)) *)
  split; move => Hgen a.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => [s [_ H']] s'.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply semBindGenSize in Hgen; last by eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply unsizedChecker_alt_def; eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - by eapply semBindGenSize; intros; apply Hgen; eexists; split => //; eauto.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semBindGenSizeMonotonic {A} (gen : G A) (f : A -> Checker)
  `{SizeMonotonic _ gen}  
  `{forall a, SizeMonotonicChecker (f a)} :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (semChecker (bindGen gen f) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
   forall a, semGen gen a -> semChecker (f a)).
Proof.
(* Goal: iff (semChecker (@forAllShrink A C H1 H2 gen sh f)) (forall (a : A) (_ : @semGen A gen a), @semCheckable C H1 (f a)) *)
  split; move => Hgen a.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => [s [_ H']] s'. case_eq (s <= s') => [Hleq |  
                                                 /leP/Compare_dec.not_le/ltP/ltnW Hleq].
(* Goal: semCheckerSize (@checker C H1 (f a)) s' *)
(* Goal: semCheckerSize (@forAllShrink A C H1 H2 gen sh f) a *)
    + specialize (Hgen s').
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
      eapply semBindGenSize in Hgen; eauto. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
      eapply monotonic; eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    + specialize (Hgen s). eapply semBindGenSize in Hgen; eauto. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
      eapply monotonicChecker_alt_def; eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - by eapply semBindGenSize; intros; apply Hgen; eexists; split => //; eauto.
Qed.

Lemma semPredQPropSize (c : Checker) (s : nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckableSize c s <-> (semCheckerSize c s).
Proof.
  rewrite /semCheckableSize /checker
          /testChecker /checker /testProp /semCheckerSize.
(* Goal: iff (@set_incl bool (@imset QProp bool successful (@semGenSize QProp c s)) (@set1 bool true)) (@set_incl bool (@imset QProp bool successful (@semGenSize QProp c s)) (@set1 bool true)) *)
  split; move => Hqp qp Hsize; auto.
Qed.

Lemma semPredQProp (c : Checker) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckable c <-> semChecker c.
Proof.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  split => H s; eapply semPredQPropSize; eauto.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Instance forAllMonotonic {A C} {_ : Checkable C} `{Show A} (g : G A) (f : A -> C)
        `{SizeMonotonic _ g} `{forall x, SizeMonotonicChecker (checker (f x))} :
  SizeMonotonicChecker (forAll g f).
Admitted.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semForAllSize {A C} `{Show A, Checkable C} (g : G A) (f : A -> C) (s:nat) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semCheckerSize (forAll g f) s <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  forall (a : A), a \in semGenSize g s -> semCheckableSize (f a) s.
Proof.
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
  split=> H'.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - rewrite /forAll in H'. move/semBindGenSize : H' => H' a /H' Hgen.
(* Goal: semP s (a nat) *)
      by apply semPrintTestCase_idSize in Hgen.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - rewrite /forAll in H' *. apply semBindGenSize => g' Hgen.
(* Goal: semP s (a nat) *)
    rewrite semPrintTestCase_idSize. by apply H'.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semForAllUnsized1 {A C} `{Show A, Checkable C} (g : G A) (f : A -> C)
      `{Unsized _ g} :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (semChecker (forAll g f) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
   forall (a : A), a \in semGen g -> semCheckable (f a)).
Proof.
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
  split=> H'.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => a [s' [_ Hgen]] s. specialize (H' s).
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply semForAllSize in H'; first by eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply unsized; eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => s; eapply semForAllSize; move => a Hgen.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    apply H'; eexists; split => //; eauto. 
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semForAllUnsized2 {A C} `{Show A, Checkable C} (g : G A) (f : A -> C)
      `{forall a, UnsizedChecker (checker (f a))} :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (semChecker (forAll g f) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
   forall (a : A), a \in semGen g -> semCheckable (f a)).
Proof.
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
  split=> H'.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => a [s' [_ Hgen]] s. specialize (H' s').
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply semForAllSize in H'; last by eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    by eapply unsizedChecker_alt_def; eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => s; eapply semForAllSize; move => a Hgen. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    apply H'; eexists; split => //; eauto. 
Qed.

(* begin semForAllSizeMonotonic *)
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semForAllSizeMonotonic {A C} `{Show A, Checkable C} (g : G A) (f : A -> C)
    `{SizeMonotonic _ g} `{forall a, SizeMonotonicChecker (checker (f a))} :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (semChecker (forAll g f) <-> forall (a:A), a \in semGen g -> semCheckable (f a)).
(* end semForAllSizeMonotonic *)
Proof.
(* Goal: iff (semChecker (@forAllShrink A C H1 H2 gen sh f)) (forall (a : A) (_ : @semGen A gen a), @semCheckable C H1 (f a)) *)
  split; move => Hcheck a.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => [s [_ H']] s'. case_eq (s <= s') => [Hleq |  
                                                 /leP/Compare_dec.not_le/ltP/ltnW Hleq].
(* Goal: semCheckerSize (@checker C H1 (f a)) s' *)
(* Goal: semCheckerSize (@forAllShrink A C H1 H2 gen sh f) a *)
    + specialize (Hcheck s').
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
      rewrite -> semForAllSize in Hcheck. apply Hcheck. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
      eapply monotonic; eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    + specialize (Hcheck s). eapply semForAllSize in Hcheck; eauto. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
      by eapply monotonicChecker_alt_def; eauto. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - by eapply semForAllSize; intros; apply Hcheck; eexists; split => //; eauto.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma unsized_printTestCase {A C} `{Checkable C} `{Show A} (c : A -> C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (forall a, Unsized (checker (c a))) ->
  (forall a, Unsized (printTestCase (String.append (Show.show a) newline) (c a))).
Proof.
(*   rewrite /UnsizedChecker /unsized. setoid_rewrite semFmapSize. *)
(*   move => H' a s1 s2. specialize (H' a s1 s2). *)
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
(*   by do 2 rewrite semPrintTestCase_idSize. *)
(* Qed. *)
Abort.


(* alternative definitions
Definition unsizedChecker (c : Checker) : Prop :=
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  forall s1 s2, semCheckerSize c s1 <-> semCheckerSize c s2.

(* another characterization of unsizedChecker *)
Lemma unsizedChecker_def2 {A : Type} : forall (c : Checker),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  unsizedChecker c ->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  forall s, semCheckerSize c s <-> semChecker c.
Proof.
(* Goal: forall b : bool, @eq bool (resultSuccessful (liftBool b)) b *)
  intros. split; intro H'.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - intro s'. rewrite H. eassumption.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - by apply H'.
Qed.
*)

(* CH: We could create a super class UCheckable that includes the
       unsized assumption. And we could use sections to hide all the
       type class stuff from the paper. *)
(* CH: This will be affected by upcoming refactoring;
       proving it like this only because it appears in ITP submission *)



Require Import FunctionalExtensionality.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma curry_uncurry {A B C : Type} (f : A -> B -> C) :
  curry (uncurry f) = f.
(* Goal: @set_eq QProp (@set1 QProp qp) (@set1 QProp qp) *)
Proof. apply functional_extensionality => x. reflexivity. Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma uncurry_curry {A B C : Type} (f : A * B -> C) :
  uncurry (curry f) = f.
Proof. apply functional_extensionality. by intros [a b]. Qed.


Lemma mergeBinds' :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  forall A B C (ga : G A) (gb : G B) (f : A * B -> G C),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semGen (bindGen ga (fun x => bindGen gb ((curry f) x))) <-->
    semGen (bindGen (genPair ga gb) f).
Proof. setoid_rewrite mergeBinds. by setoid_rewrite uncurry_curry. Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma eq_to_impl : forall (a b : Prop), a = b -> a -> b.
Proof. move => a b H. by rewrite H. Qed.

(* CH: could we get rid of this in the RBTree example if we used
   semBindSizeMonotonic instead of semBindUnsized2?  *)
(* CH: The problem with proving this is the silly print in the middle of things.
   There are also some technical problems with setoid_rewriting taking ages,
   and requiring an useless split beforehand. 
   ZP: Got rid of setoid_rewrite. The proof goes through instantly now.   
*)
Lemma mergeForAlls {A B C : Type} `{Checkable C} `{Show A} `{Show B}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         (ga : G A) (gb : G B) (f : A -> B -> C) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
     semChecker (forAll ga (fun a => forAll gb (f a))) <->
     semChecker (forAll (genPair ga gb) (uncurry f)).
Proof.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (* ZP : I know that this proof lacks nice point-free reasoning, but it is 
          significantly smaller and typechecks much faster that the previous one *)
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  split. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => HforAll s. apply semForAllSize; 
    move  => [a b] /= /semLiftGen2Size [[a' b'] [[/= Hg1 Hg2] [Heq1 Heq2]]]; subst.
    specialize (HforAll s). eapply semForAllSize in HforAll.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    by eapply semForAllSize in HforAll; eauto. by eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => HforAll s. apply semForAllSize => a Hgena. 
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
    apply semForAllSize => b Hgenb.
    specialize (HforAll s). 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    move /semForAllSize/(_ (a, b)) : HforAll => /= HforAll. apply HforAll.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    apply semLiftGen2Size. exists (a, b); split => //; eauto.
Qed.

Lemma semForAllShrinkSize:
  forall {A C} `{Checkable C} `{Show A}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         (gen : G A) (f : A -> C) shrinker (size: nat),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckerSize (forAllShrink gen shrinker f) size <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    forall a : A, semGenSize gen size a -> semCheckableSize (f a) size.
Proof.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  move => A C H show gen pf shrink. split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - rewrite /forAllShrink semBindGenSize.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    move=> H' a /H' Hgen. setoid_rewrite semShrinking_idSize in Hgen.
(* Goal: @semCheckableSize C H (pf a) size *)
(* Goal: forall _ : forall (a : A) (_ : @semGenSize A gen size a), @semCheckableSize C H (pf a) size, semCheckerSize (@forAllShrink A C H show gen shrink pf) size *)
    setoid_rewrite semPredQPropSize in Hgen.
(* Goal: semP s (a nat) *)
    by apply semPrintTestCase_idSize in Hgen.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move=> H'. rewrite /forAllShrink semBindGenSize. move => a g.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
    rewrite semShrinking_idSize. apply semPredQPropSize.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
    rewrite semPrintTestCase_idSize. by auto.
Qed.

Lemma semForAllShrinkUnsized1 :
  forall {A C} `{Checkable C} `{Show A}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         (gen : G A) (f : A -> C) shrinker `{Unsized _ gen},
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (semChecker (forAllShrink gen shrinker f) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
     forall a : A, semGen gen a -> semCheckable (f a)).
Proof.
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
  split=> H'.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => a [s' [_ Hgen]] s. specialize (H' s).
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply semForAllShrinkSize in H'; first by eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply H1; eauto. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
 - move => s; eapply semForAllShrinkSize; move => a Hgen. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    apply H'; eexists; split => //; eauto. 
Qed.

Lemma semForAllShrinkUnsized2 :
  forall {A C} `{Checkable C} `{Show A}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         (gen : G A) (f : A -> C) shrinker
  `{forall a, UnsizedChecker (checker (f a))},
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (semChecker (forAllShrink gen shrinker f) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
     forall a : A, semGen gen a -> semCheckable (f a)).
Proof.
(* Goal: @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s *)
(* Goal: forall (_ : @semCheckableSize (forall _ : A, C) (@testProd A (fun _ : A => C) H2 H H0 H1 (fun _ : A => H3)) a s) (a0 : A) (_ : @semGenSize A (@arbitrary A H) s a0), semP s (a a0) *)
  split=> H'.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => a [s' [_ Hgen]] s. specialize (H' s').
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply semForAllShrinkSize in H'; last by eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    eapply unsizedChecker_alt_def; eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => s; eapply semForAllShrinkSize; move => a Hgen. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    apply H'; eexists; split => //; eauto. 
Qed.

Lemma semForAllShrinkMonotonic :
  forall {A C} `{Checkable C} `{Show A}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         (gen : G A) (f : A -> C) shrinker `{SizeMonotonic _ gen}, 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (forall a, SizeMonotonicChecker (checker (f a))) ->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (semChecker (forAllShrink gen shrinker f) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
     forall a : A, semGen gen a -> semCheckable (f a)).
Proof.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move => A C H1 H2 gen f sh Hmon1 Hmon2.
(* Goal: iff (semChecker (@forAllShrink A C H1 H2 gen sh f)) (forall (a : A) (_ : @semGen A gen a), @semCheckable C H1 (f a)) *)
  split; move => Hcheck a.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => [s [_ H']] s'. case_eq (s <= s') => [Hleq |  
                                                 /leP/Compare_dec.not_le/ltP/ltnW Hleq].
(* Goal: semCheckerSize (@checker C H1 (f a)) s' *)
(* Goal: semCheckerSize (@forAllShrink A C H1 H2 gen sh f) a *)
    + specialize (Hcheck s').
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
      rewrite -> semForAllShrinkSize in Hcheck. apply Hcheck. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
      by eapply Hmon1; eauto.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
    + specialize (Hcheck s). eapply semForAllShrinkSize in Hcheck; eauto. 
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
      by eapply monotonicChecker_alt_def; eauto. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - by eapply semForAllShrinkSize; intros; apply Hcheck; eexists; split => //; eauto.
Qed.

Lemma bool_successful :  
  forall b, resultSuccessful (liftBool b) = b.
Proof.
(* Goal: forall b : bool, @eq bool (resultSuccessful (liftBool b)) b *)
  intros. destruct b; auto.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semCheckableBoolSize (b : bool) size : semCheckableSize b size <-> b.
Proof.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite /semCheckableSize /semCheckerSize /checker /testBool.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => /(_ b) H. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    suff : [set true] b by move => <- //.
(* Goal: @set1 bool true (successful qp) *)
(* Goal: forall _ : forall (a : A) (_ : @semGenSize A gen s a), @set_incl bool (@imset QProp bool successful (@semGenSize QProp (f a) s)) (@set1 bool true), @set_incl bool (@imset QProp bool successful (@semGenSize QProp (@bindGen A QProp gen f) s)) (@set1 bool true) *)
    eapply H. eexists (MkProp (MkRose (liftBool b) (lazy nil))).
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    split => //=. by rewrite -> (semReturnSize _ _ _). by eapply bool_successful.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => Hb b' [qp [/semReturnSize <- <-]] /=.
(* Goal: semP s (a nat) *)
    by rewrite bool_successful. 
Qed.

(* begin semCheckableBool *)
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semCheckableBool (b : bool) : semCheckable b <-> b.
(* end semCheckableBool *)
Proof. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  (* CH: brute-force, please fix 
     ZP : better now? We do case analysis on b bun in a lemma; 
          I don't think we can avoid it *)
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  split; [move => /(_ 0) H | move => H s]; eapply semCheckableBoolSize; eauto.
Qed.
 
Program Instance boolUnsized (b : bool) : UnsizedChecker (checker b).
Next Obligation.
(* Goal: @set_eq QProp (@set1 QProp qp) (@set1 QProp qp) *)
  rewrite !semFmapSize !semReturnSize. apply imset_eq. reflexivity.
Qed.

Lemma semCheckableResultSize:
  forall (res: Result) (size: nat),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckableSize res size <-> resultSuccessful res.
Proof.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite /semCheckableSize /checker /testResult /=.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  move => res size. split. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => /(_ (resultSuccessful res)) H. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    suff : [set true] (resultSuccessful res) by move <-.
    apply H. eexists. split; first by apply semReturnSize. 
(* Goal: @set_eq QProp (@set1 QProp qp) (@set1 QProp qp) *)
    reflexivity. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H b [qp' [/semReturnSize <- <-]] //=.
Qed.

Lemma semCheckableResult :
  forall (res: Result),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckable res  <-> resultSuccessful res.
Proof.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  split; [move => /(_ 0) H | move => H s]; eapply semCheckableResultSize; eauto.
Qed.

Program Instance resultUnsized (r : Result) : UnsizedChecker (checker r).
Next Obligation.
(* Goal: @set_eq QProp (@set1 QProp qp) (@set1 QProp qp) *)
  rewrite !semFmapSize !semReturnSize. apply imset_eq. reflexivity.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semCheckableUnitSize (t : unit) size : semCheckableSize t size <-> True.
Proof.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  split => // _ qp [qp' [/semReturnSize <- <-]] //.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Lemma semCheckableUnit (t : unit) : semCheckable t <-> True.
Proof.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  split; [move => /(_ 0) H | move => H s]; eapply semCheckableUnitSize; eauto.
Qed.

Program Instance unitUnsized : UnsizedChecker (checker tt).
Next Obligation.
(* Goal: @set_eq QProp (@set1 QProp qp) (@set1 QProp qp) *)
  rewrite !semFmapSize !semReturnSize. apply imset_eq. reflexivity.
Qed.

Lemma semCheckableQPropSize (qp : QProp) size :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semCheckableSize qp size <-> successful qp.
Proof.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite /semCheckableSize /checker /testProp.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  split. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => /(_ (successful qp)) H. 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    suff : ([set true] (successful qp)) by move => <-.
    apply H. eexists. split ; last by reflexivity.
(* Goal: semP s (a nat) *)
    by apply semReturnSize.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H b [qp' [/semReturnSize <- <-]] //=.
Qed.

Lemma semCheckableQProp (qp : QProp) :
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  semCheckable qp  <-> successful qp.
Proof.
(* Goal: @imset QProp bool successful (@semGenSize QProp c s2) b *)
  split; [move => /(_ 0) H | move => H s]; eapply semCheckableQPropSize; eauto.
Qed.

Program Instance qpUnsized (qp : QProp) : UnsizedChecker (checker qp).
Next Obligation.
(* Goal: @set_eq QProp (@set1 QProp qp) (@set1 QProp qp) *)
  rewrite !semFmapSize !semReturnSize. apply imset_eq. reflexivity.
Qed.

Lemma semCheckableGenSize:
  forall (P : Type) {H : Checkable P} (gen: G P) (size : nat),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (semCheckableSize gen size) <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (forall p, semGenSize gen size p -> semCheckableSize p size).
Proof.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  move=> P H gen s. rewrite /semCheckableSize /checker /testGenProp. split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => /semBindGenSize Hcheck p Hgen //=; eauto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => Hcheck. apply semBindGenSize => a Hgen; eauto.
Qed.


Lemma semCheckableFunSize:
  forall {A C} {H1 : Show A} `{H2 : Arbitrary A} {H3 : Checkable C}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         (f : A -> C) (size: nat),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    semCheckableSize f size <->
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    forall (a : A), semGenSize arbitrary size a -> semCheckableSize (f a) size.
Proof.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move=> A C H1 H2 H3 f.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  rewrite /semCheckable /checker /testFun.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => /semForAllShrinkSize H' a' /H' Gen. by auto.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H'. apply semForAllShrinkSize => a' /H' Hgen. by auto.
Qed.

Lemma semCheckablePolyFunSize:
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  forall {C : Type -> Type} {H : Checkable (C nat)} (f : forall T, C T)
         (size : nat),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (semCheckableSize f size) <-> (semCheckableSize (f nat) size).
Proof.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move => C H f s. rewrite /semCheckableSize {2}/checker /testPolyFun.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  by rewrite semPrintTestCase_idSize.
Qed.

Lemma semCheckablePolyFunSetSize:
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  forall {C : Set -> Type} {H : Checkable (C nat)} (f : forall T, C T) (size: nat),
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    (semCheckableSize f size) <->  (semCheckableSize (f nat) size).
Proof.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  move => C H f s. rewrite /semCheckableSize {2}/checker /testPolyFun.
(* Goal: iff (@proposition (C nat) H (Build_Provable (C nat) H semP proof) s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  by rewrite semPrintTestCase_idSize.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Program Instance uncurryUsized {A B} (f : A -> B -> Checker) p
        `{UnsizedChecker (f (fst p) (snd p))} : UnsizedChecker (uncurry f p).
Next Obligation. by apply unsizedChecker. Qed.

(* A typeclass so we can automate the application of the previous theorems
   and get a readable Prop *)

Class Provable (A : Type) {H: Checkable A} : Type :=
 {
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    proposition : nat -> A -> Prop;
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    proposition_equiv : forall a s, proposition s a <-> semCheckableSize a s
  }.

Program Instance proveResult : Provable Result :=
  {|
    proposition s r := resultSuccessful r
  |}.
Next Obligation.
(* Goal: semP s (a nat) *)
  by rewrite semCheckableResultSize.
Qed.

Program Instance proveUnit : Provable unit :=
  {|
    proposition := fun _ _ => True
  |}.
Next Obligation.
(* Goal: semP s (a nat) *)
  by rewrite semCheckableUnitSize.
Qed.

Program Instance proveQProp : Provable QProp :=
  {|
    proposition s qp := successful qp = true
  |}.
Next Obligation.
(* Goal: semP s (a nat) *)
  by rewrite semCheckableQPropSize.
Qed.

Program Instance proveBool : Provable bool :=
  {|
    proposition s b :=  b = true
  |}.
Next Obligation.
(* Goal: semP s (a nat) *)
  by rewrite semCheckableBoolSize.
Qed.

Program Instance proveGenProp {C} `{Provable C} :
  Provable (G C) :=
  {|
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    proposition s g := (forall p, semGenSize g s p -> proposition s p)
  |}.
Next Obligation.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  destruct H0 as [semP proof]. rewrite /proposition. split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => H'. apply semCheckableGenSize => p Hgen. apply proof. eapply H'. eassumption.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move => /semCheckableGenSize H' p Hgen. eapply proof. apply H'. by auto.
Qed.

Program Instance proveChecker : Provable Checker :=
  {|
    proposition s g := semCheckerSize g s
  |}.
Next Obligation.
(* Goal: @semCheckableSize Checker testChecker (@printTestCase C H (String.append (@Show.show A show a) newline) (pf a)) size *)
  split; intros H; by apply semPredQPropSize.
Qed.

Program Instance proveFun {A C: Type} `{Arbitrary A} `{Show A}
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
        `{Provable C}: Provable (A -> C) :=
  {|
    proposition s p :=
      (forall a,
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
         semGenSize arbitrary s a ->
         proposition s (p a))
  |}.
Next Obligation.
  match goal with 
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
    | [ Hyp : Provable _ |- _ ] => destruct Hyp as [semP proof]
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  end. rewrite /proposition. split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move=> H'. apply semCheckableFunSize => a' /H' Hgen.
(* Goal: semP s (a a') *)
    by apply proof.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move=> H' a' Hgen. apply proof. by apply semCheckableFunSize.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Program Instance provePolyFun {C : Type -> Type} `{Provable (C nat)} :
  Provable (forall T, C T) :=
  {
    proposition s f := proposition s (f nat)
  }.
Next Obligation.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  destruct H0 as [semP proof]. rewrite /proposition. split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move=> /proof H'. by apply semCheckablePolyFunSize.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move=> /semCheckablePolyFunSize H'. by apply proof.
Qed.

(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
Program Instance provePolyFunSet {C : Set -> Type} `{Provable (C nat)} :
  Provable (forall T, C T) :=
  {
    proposition s f := proposition s (f nat)
  }.
Next Obligation.
(* Goal: iff (semP s (a nat)) (@semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s) *)
  destruct H0 as [semP proof]. rewrite /proposition. split.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move=> /proof H'. by apply semCheckablePolyFunSetSize.
(* Goal: forall _ : @semCheckableSize (forall T : Set, C T) (@testPolyFunSet C H) a s, semP s (a nat) *)
  - move=> /semCheckablePolyFunSetSize H'. by apply proof.
Qed.
