Module Common

From Coq Require Import FSets.FMapPositive.
From Coq Require Import FSets.FMapFacts.
From Coq Require Import List.
From Coq Require Import Sorting.Permutation.

From Coq Require Import Setoid.
From Coq Require Import Relations RelationPairs.
From Coq Require Import Morphisms.

Import ListNotations.
From Coq Require MSets.MSets.
From Coq Require Export PArith.
From Coq Require Import Classes.EquivDec.

From Velus Require Export Common.CommonTactics.
From Velus Require Export Common.CommonList.
From Velus Require Export Common.CommonStreams.
From Velus Require Export Common.CommonPS.
From Velus Require Export ClockDefs.

Open Scope list.

Properties

Lemma not_or':
  forall A B, ~(A \/ B) <-> ~A /\ ~B.

Lemma flip_impl:
  forall {P Q : Prop},
    (P -> Q) ->
    ~Q ->
    ~P.

Lemma None_eq_dne:
  forall {A} (v : option A),
    ~(v <> None) <-> (v = None).

About identifiers *

Lemma ident_eqb_neq:
  forall x y, ident_eqb x y = false <-> x <> y.

Lemma ident_eqb_eq:
  forall x y, ident_eqb x y = true <-> x = y.

Lemma ident_eqb_refl:
  forall f, ident_eqb f f = true.

Lemma ident_eqb_sym:
  forall x y, ident_eqb x y = ident_eqb y x.
Proof Pos.eqb_sym.

Lemma ident_eq_sym:
  forall (x y: ident), x = y <-> y = x.

Lemma decidable_eq_ident:
  forall (f g: ident),
    Decidable.decidable (f = g).

Lemma equiv_decb_negb:
  forall x, (x ==b negb x) = false.

Definition mem_assoc_ident {A} (x: ident): list (ident * A) -> bool :=
  existsb (fun y => ident_eqb (fst y) x).

Lemma mem_assoc_ident_false:
  forall {A} x xs (t: A),
    mem_assoc_ident x xs = false ->
    ~ In (x, t) xs.

Lemma mem_assoc_ident_true:
  forall {A} x xs,
    mem_assoc_ident x xs = true ->
    exists t: A, In (x, t) xs.

Definition assoc_ident {A} (x: ident) (xs: list (ident * A)): option A :=
  match find (fun y => ident_eqb (fst y) x) xs with
  | Some (_, a) => Some a
  | None => None
  end.

Lemma assoc_ident_true :
  forall {A} (x: ident) (y : A) (xs: list (ident * A)),
    NoDupMembers xs ->
    In (x,y) xs ->
    assoc_ident x xs = Some y.

Lemma assoc_ident_false:
  forall {A} (x: ident) (xs: list (ident * A)),
    ~InMembers x xs ->
    assoc_ident x xs = None.

Module Type IDS.
  Parameter self : ident.
  Parameter out : ident.
  Parameter temp : ident.

  Parameter step : ident.
  Parameter reset : ident.

  Parameter elab : ident.
  Parameter norm1 : ident.
  Parameter norm2 : ident.
  Parameter obc2c : ident.

  Definition gensym_prefs := [elab; norm1; norm2].
  Conjecture gensym_prefs_NoDup : NoDup gensym_prefs.

  Parameter default : ident.

  Conjecture reset_not_step: reset <> step.

  Parameter atom : ident -> Prop.

  Conjecture self_atom : atom self.
  Conjecture out_atom : atom out.
  Conjecture temp_atom : atom temp.

  Conjecture step_atom : atom step.
  Conjecture reset_atom : atom reset.
  Conjecture elab_atom : atom elab.
  Conjecture norm1_atom : atom norm1.
  Conjecture norm2_atom : atom norm2.
  Conjecture obc2c_atom : atom obc2c.

Name generation by prefixing

  Parameter prefix : ident -> ident -> ident.

  Conjecture prefix_not_atom:
    forall pref id,
      ~atom (prefix pref id).

  Conjecture prefix_injective:
    forall pref id pref' id',
      prefix pref id = prefix pref' id' ->
      pref = pref' /\ id = id'.

Name generation with fresh identifiers

  Parameter gensym : ident -> ident -> ident.

  Conjecture gensym_not_atom:
    forall pref x,
      ~atom (gensym pref x).

  Conjecture gensym_injective:
    forall pref x pref' x',
      gensym pref x = gensym pref' x' ->
      pref = pref' /\ x = x'.

  Definition AtomOrGensym (prefs : PS.t) (id : ident) :=
    atom id \/ PS.Exists (fun pre => exists n, id = gensym pre n) prefs.

End IDS.

Generalizable Variables A.

Lemma equiv_decb_equiv:
  forall `{EqDec A} (x y : A),
    equiv_decb x y = true <-> equiv x y.

Lemma nequiv_decb_false:
  forall {A} `{EqDec A} (x y: A),
    (x <>b y) = false <-> (x ==b y) = true.

Lemma equiv_decb_refl:
  forall `{EqDec A} (x: A),
    equiv_decb x x = true.

Lemma nequiv_decb_refl:
  forall x, (x <>b x) = false.

Lemma not_equiv_decb_equiv:
  forall `{EqDec A} (x y: A),
    equiv_decb x y = false <-> ~(equiv x y).

Lemma nequiv_decb_true:
  forall {A R} `{EqDec A R} (x y : A),
    (x <>b y) = true <-> (x =/= y).

Lemma not_in_filter_nequiv_decb:
  forall y xs,
    ~In y xs ->
    filter (nequiv_decb y) xs = xs.

Lemma forall2b_Forall2_equiv_decb:
  forall {A R} `{EqDec A R} (xs ys : list A),
    forall2b equiv_decb xs ys = true ->
    Forall2 R xs ys.

Definition equiv_decb3 {A R} `{EqDec A R} (x y z : A) : bool :=
  (x ==b y) && (y ==b z).

Lemma equiv_decb3_equiv:
  forall {A R} `{EqDec A R} x y z,
    (equiv_decb3 x y z = true) <-> (x === y /\ y === z).

Lemma forall3b_equiv_decb3:
  forall {A R} `{EqDec A R} xs ys zs,
    forall3b equiv_decb3 xs ys zs = true ->
    Forall2 R xs ys /\ Forall2 R ys zs.

About Coq stdlib

Lemma pos_le_plus1:
  forall x, (x <= x + 1)%positive.

Lemma pos_lt_plus1:
  forall x, (x < x + 1)%positive.

Lemma not_None_is_Some:
  forall A (x : option A), x <> None <-> (exists v, x = Some v).

Corollary not_None_is_Some_Forall:
  forall {A} (xs: list (option A)),
    Forall (fun (v: option A) => ~ v = None) xs ->
    exists ys, xs = map Some ys.

Lemma not_Some_is_None:
  forall A (x : option A), (forall v, x <> Some v) <-> x = None.

Section IsNoneSome.

  Context {A : Type}.

  Fixpoint isNone (o : option A) : bool :=
    match o with None => true | Some _ => false end.

  Fixpoint isSome (o : option A) : bool :=
    match o with None => false | Some _ => true end.

  Lemma isSome_true:
    forall (v : option A), isSome v = true <-> exists v', v = Some v'.

  Lemma isSome_false:
    forall (v : option A), isSome v = false <-> v = None.

End IsNoneSome.


Lemma relation_equivalence_subrelation:
  forall {A} (R1 R2 : relation A),
    relation_equivalence R1 R2 <-> (subrelation R1 R2 /\ subrelation R2 R1).


Section TypesAndClocks.

  Context {type clock : Type}.



  Definition idty : list (ident * (type * clock)) -> list (ident * type) :=
    map (fun xtc => (fst xtc, fst (snd xtc))).

  Definition idck : list (ident * (type * clock)) -> list (ident * clock) :=
    map (fun xtc => (fst xtc, snd (snd xtc))).


  Lemma idty_app:
    forall xs ys,
      idty (xs ++ ys) = idty xs ++ idty ys.

  Lemma InMembers_idty:
    forall x xs,
      InMembers x (idty xs) <-> InMembers x xs.

  Lemma NoDupMembers_idty:
    forall xs,
      NoDupMembers (idty xs) <-> NoDupMembers xs.

  Lemma map_fst_idty:
    forall xs,
      map fst (idty xs) = map fst xs.

  Lemma length_idty:
    forall xs,
      length (idty xs) = length xs.

  Lemma In_idty_exists:
    forall x (ty : type) xs,
      In (x, ty) (idty xs) <-> exists (ck: clock), In (x, (ty, ck)) xs.

  Lemma idty_InMembers:
    forall x ty (xs : list (ident * (type * clock))),
      In (x, ty) (idty xs) ->
      InMembers x xs.

  Global Instance idty_Permutation_Proper:
    Proper (@Permutation (ident * (type * clock))
            ==> @Permutation (ident * type)) idty.


  Lemma idck_app:
    forall xs ys,
      idck (xs ++ ys) = idck xs ++ idck ys.

  Lemma InMembers_idck:
    forall x xs,
      InMembers x (idck xs) <-> InMembers x xs.

  Lemma NoDupMembers_idck:
    forall xs,
      NoDupMembers (idck xs) <-> NoDupMembers xs.

  Lemma map_fst_idck:
    forall xs,
      map fst (idck xs) = map fst xs.

  Lemma length_idck:
    forall xs,
      length (idck xs) = length xs.

  Lemma In_idck_exists:
    forall x (ck : clock) xs,
      In (x, ck) (idck xs) <-> exists (ty: type), In (x, (ty, ck)) xs.

  Global Instance idck_Permutation_Proper:
    Proper (Permutation (A:=(ident * (type * clock)))
            ==> Permutation (A:=(ident * clock))) idck.

  Lemma filter_fst_idck:
    forall (xs: list (ident * (type * clock))) P,
      idck (filter (fun x => P (fst x)) xs) = filter (fun x => P (fst x)) (idck xs).

End TypesAndClocks.

Lemma In_of_list_InMembers:
  forall {A} x (xs : list (ident * A)),
    PS.In x (PSP.of_list (map fst xs)) <-> InMembers x xs.


Section OptionLists.

  Context {A B : Type}.

  Definition omap (f : A -> option B) (xs : list A) : option (list B) :=
    List.fold_right (fun x ys => match f x, ys with
                              | Some y, Some ys => Some (y :: ys)
                              | _, _ => None
                              end) (Some []) xs.

  Definition ofold_right (f : A -> B -> option B) (acc : option B) (xs : list A)
    : option B :=
    fold_right (fun x acc => match acc with
                          | Some acc => f x acc
                          | None => None
                          end) acc xs.

  Lemma ofold_right_none_none:
    forall (f : A -> B -> option B) xs, ofold_right f None xs = None.

End OptionLists.


Section ORel.

  Context {A : Type}
          (R : relation A).

  Inductive orel : relation (option A) :=
  | Oreln : orel None None
  | Orels : forall sx sy, R sx sy -> orel (Some sx) (Some sy).

  Global Instance orel_refl `{RR : Reflexive A R} : Reflexive orel.

  Global Instance orel_trans `{RT : Transitive A R} : Transitive orel.

  Global Instance orel_sym `{RS : Symmetric A R} : Symmetric orel.

  Global Instance orel_equiv `{Equivalence A R} : Equivalence orel.
  Proof (Build_Equivalence orel orel_refl orel_sym orel_trans).

  Global Instance orel_preord `{PreOrder A R} : PreOrder orel.
  Proof (Build_PreOrder orel orel_refl orel_trans).

  Global Instance orel_Some_Proper: Proper (R ==> orel) Some.

  Global Instance orel_Proper `{Symmetric A R} `{Transitive A R} :
    Proper (orel ==> orel ==> iff) orel.

  Lemma orel_inversion:
    forall x y, orel (Some x) (Some y) <-> R x y.

End ORel.

Arguments orel {A}%type R%signature.
Hint Extern 4 (orel _ None None) => now constructor.
Hint Extern 5 (orel _ ?x ?x) => reflexivity.

Lemma orel_eq {A : Type} :
  forall x y, orel (@eq A) x y <-> x = y.

Lemma orel_eq_weaken:
  forall {A} R `{Reflexive A R} (x y : option A),
    x = y -> orel R x y.

Instance orel_option_map_Proper
         {A B} (RA : relation A) (RB : relation B) `{Equivalence B RB}:
  Proper ((RA ==> RB) ==> orel RA ==> orel RB) (@option_map A B).

Instance orel_option_map_pointwise_Proper
         {A B} (RA : relation A) (RB : relation B)
         `{Equivalence B RB}:
  Proper (pointwise_relation A RB ==> eq ==> orel RB) (@option_map A B).

Instance orel_subrelation {A} (R1 R2 : relation A) `{subrelation A R1 R2}:
  subrelation (orel R1) (orel R2).

Lemma orel_pair:
  forall {A B} (RA: relation A) (RB: relation B)
    a1 a2 b1 b2,
    RA a1 a2 ->
    RB b1 b2 ->
    orel (RelationPairs.RelProd RA RB) (Some (a1, b1)) (Some (a2, b2)).

Instance orel_subrelation_Proper {A}:
  Proper (@subrelation A ==> eq ==> eq ==> Basics.impl) orel.

Instance orel_equivalence_Proper {A}:
  Proper (@relation_equivalence A ==> eq ==> eq ==> iff) orel.

Instance orel_EqDec {A R} `{EqDec A R} : EqDec (option A) (orel R) :=
  { equiv_dec := fun xo yo =>
                   match xo, yo with
                   | None, None => left _
                   | Some x, Some y => match x == y with
                                      | left _ => left _
                                      | right _ => right _
                                      end
                   | _, _ => right _
                   end }.



Definition obind {A B: Type} (f: option A) (g: A -> option B) : option B :=
  match f with
  | Some x => g x
  | None => None
  end.

Definition obind2 {A B C: Type} (f: option (A * B)) (g: A -> B -> option C) : option C :=
  match f with
  | Some (x, y) => g x y
  | None => None
  end.

Notation "'do' X <- A ; B" := (obind A (fun X => B))
                                (at level 200, X ident, A at level 100, B at level 200)
                              : option_monad_scope.

Notation "'do' ( X , Y ) <- A ; B" := (obind2 A (fun X Y => B))
                                        (at level 200, X ident, Y ident, A at level 100, B at level 200)
                                      : option_monad_scope.

Remark obind_inversion:
  forall (A B: Type) (f: option A) (g: A -> option B) (y: B),
    obind f g = Some y ->
    exists x, f = Some x /\ g x = Some y.

Remark obind2_inversion:
  forall {A B C: Type} (f: option (A*B)) (g: A -> B -> option C) (z: C),
    obind2 f g = Some z ->
    exists x, exists y, f = Some (x, y) /\ g x y = Some z.

Local Open Scope option_monad_scope.

Remark omap_inversion:
  forall (A B: Type) (f: A -> option B) (l: list A) (l': list B),
    omap f l = Some l' ->
    Forall2 (fun x y => f x = Some y) l l'.


Ltac omonadInv1 H :=
  match type of H with
  | (Some _ = Some _) =>
    inversion H; clear H; try subst
  | (None = Some _) =>
    discriminate
  | (obind ?F ?G = Some ?X) =>
    let x := fresh "x" in (
      let EQ1 := fresh "EQ" in (
        let EQ2 := fresh "EQ" in (
          destruct (obind_inversion F G H) as (x & EQ1 & EQ2);
          clear H; try (omonadInv1 EQ2))))
  | (obind2 ?F ?G = Some ?X) =>
    let x1 := fresh "x" in (
      let x2 := fresh "x" in (
        let EQ1 := fresh "EQ" in (
          let EQ2 := fresh "EQ" in (
            destruct (obind2_inversion F G H) as (x1 & x2 & EQ1 & EQ2);
            clear H; try (omonadInv1 EQ2)))))
  | (match ?X with left _ => _ | right _ => None end = Some _) =>
    destruct X; [try (omonadInv1 H) | discriminate]
  | (match (negb ?X) with true => _ | false => None end = Some _) =>
    destruct X as [] eqn:?; [discriminate | try (omonadInv1 H)]
  | (match ?X with true => _ | false => None end = Some _) =>
    destruct X as [] eqn:?; [try (omonadInv1 H) | discriminate]
  | (omap ?F ?L = Some ?M) =>
    generalize (omap_inversion F L H); intro
  end.

Ltac omonadInv H :=
  omonadInv1 H ||
             match type of H with
             | (?F _ _ _ _ _ _ _ _ = Some _) =>
               ((progress simpl in H) || unfold F in H); omonadInv1 H
             | (?F _ _ _ _ _ _ _ = Some _) =>
               ((progress simpl in H) || unfold F in H); omonadInv1 H
             | (?F _ _ _ _ _ _ = Some _) =>
               ((progress simpl in H) || unfold F in H); omonadInv1 H
             | (?F _ _ _ _ _ = Some _) =>
               ((progress simpl in H) || unfold F in H); omonadInv1 H
             | (?F _ _ _ _ = Some _) =>
               ((progress simpl in H) || unfold F in H); omonadInv1 H
             | (?F _ _ _ = Some _) =>
               ((progress simpl in H) || unfold F in H); omonadInv1 H
             | (?F _ _ = Some _) =>
               ((progress simpl in H) || unfold F in H); omonadInv1 H
             | (?F _ = Some _) =>
               ((progress simpl in H) || unfold F in H); omonadInv1 H
             end.


Section OptionReasoning.

  Context {A B C : Type}.

  Global Add Parametric Morphism
         {RA : relation A} {RB : relation (option B)} `{Reflexive _ RB} : obind
      with signature (orel RA ==> (RA ==> RB) ==> RB)
        as obind_orel_ho.

  Global Add Parametric Morphism (RB : relation (option B)) `{Reflexive _ RB} : obind
      with signature (@eq (option A) ==> (pointwise_relation A RB) ==> RB)
        as obind_pointwise.

  Global Add Parametric Morphism
         (RA : relation A) (RB : relation B) (RC : relation (option C))
         `{Reflexive _ RC} : obind2
      with signature (orel (RA * RB) ==> (RA ==> RB ==> RC) ==> RC)
        as obind2_orel_ho.

  Lemma orel_obind_intro:
    forall (RA: relation A) {RB: relation B}
      {oa1 oa2 : option A} {f1 f2 : A -> option B},
      orel RA oa1 oa2 ->
      (forall a1 a2, oa1 = Some a1 ->
                oa2 = Some a2 ->
                RA a1 a2 ->
                orel RB (f1 a1) (f2 a2)) ->
      orel RB (obind oa1 f1) (obind oa2 f2).

  Lemma orel_obind_intro_eq:
    forall {RB: relation B} {oa1 oa2 : option A} {f1 f2 : A -> option B},
      oa1 = oa2 ->
      (forall a, oa1 = Some a ->
            oa2 = Some a ->
            orel RB (f1 a) (f2 a)) ->
      orel RB (obind oa1 f1) (obind oa2 f2).

  Lemma orel_obind_intro_same:
    forall {RB: relation B} {oa : option A} {f1 f2 : A -> option B},
      (forall a, oa = Some a ->
            orel RB (f1 a) (f2 a)) ->
      orel RB (obind oa f1) (obind oa f2).

  Lemma orel_obind_inversion
        (RA : relation A) `{Reflexive A RA}
        {RB : relation B} `{Equivalence B RB}
        {g} `{Proper _ (RA ==> orel RB) g} :
    forall f q,
      orel RB (obind f g) (Some q)
      <-> (exists p, orel RA f (Some p) /\ orel RB (g p) (Some q)).
  Global Arguments orel_obind_inversion RA%signature {_} {RB}%signature {_ _ _}.

  Lemma ofold_right_altdef:
    forall (f : A -> B -> option B) xs acc,
      ofold_right f acc xs = fold_right (fun x acc => obind acc (f x)) acc xs.

  Lemma ofold_right_cons:
    forall (f : A -> B -> option B) x xs acc,
      ofold_right f acc (x::xs) = obind (ofold_right f acc xs) (f x).

  Global Instance ofold_right_Proper (RA: relation A) (RB: relation B):
    Proper ((RA ==> RB ==> orel RB)
              ==> orel RB ==> SetoidList.eqlistA RA ==> orel RB) ofold_right.

  Global Instance omap_Proper (RA: relation A):
    Proper ((RA ==> orel RA) ==> SetoidList.eqlistA RA
                           ==> orel (SetoidList.eqlistA RA)) omap.

  Global Instance omap_Proper_pointwise (RA: relation A):
    Proper (pointwise_relation A (orel RA) ==> eq
                               ==> orel (SetoidList.eqlistA RA)) omap.

  Lemma orel_omap:
    forall (f g : A -> option B) xs,
      (forall x, orel eq (f x) (g x)) ->
      orel eq (omap f xs) (omap g xs).

  Lemma orel_omap_eqlistA (RB : relation B) :
    forall f g (xs : list A),
      (forall x, orel RB (f x) (g x)) ->
      orel (SetoidList.eqlistA RB) (omap f xs) (omap g xs).

  Lemma orel_option_map (RB :relation B):
    forall (f g : A -> B) x,
      (forall x, RB (f x) (g x)) ->
      orel RB (option_map f x) (option_map g x).

  Lemma orel_obind_head
        {RA : relation A} {RB : relation B} `{Equivalence _ RB} {f f'}:
    orel RA f f' ->
    forall g, Proper (RA ==> orel RB) g ->
         forall h, orel RB (obind f g) h <-> orel RB (obind f' g) h.

  Lemma orel_obind2_head
        {RA : relation A} {RB : relation B} {RC : relation C}
        `{Equivalence _ RC} {f f'}:
    orel (RA * RB) f f' ->
    forall g, Proper (RA ==> RB ==> orel RC) g ->
         forall h, orel RC (obind2 f g) h <-> orel RC (obind2 f' g) h.

  Fixpoint oconcat (xs : list (option (list A))) : option (list A) :=
    match xs with
    | [] => Some ([])
    | None::_ => None
    | Some x :: xs =>
      do xs' <- oconcat xs;
        Some (x ++ xs')
    end.

  Lemma option_map_inv_Some : forall (f : A -> B) oa b,
      option_map f oa = Some b ->
      exists a, oa = Some a /\ f a = b.

  Lemma option_map_inv_None : forall (f : A -> B) oa,
      option_map f oa = None ->
      oa = None.
End OptionReasoning.

Definition orel_obind_intro_endo {A} {R: relation A}
  := @orel_obind_intro A A R R.

Lemma orel_obind2_intro:
  forall {A B C} (RA: relation A) (RB: relation B) {RC: relation C}
    {oab1 oab2 : option (A * B)} {f1 f2 : A -> B -> option C},
    orel (RA * RB) oab1 oab2 ->
    (forall a1 b1 a2 b2, oab1 = Some (a1, b1) ->
                    oab2 = Some (a2, b2) ->
                    RA a1 a2 ->
                    RB b1 b2 ->
                    orel RC (f1 a1 b1) (f2 a2 b2)) ->
    orel RC (obind2 oab1 f1) (obind2 oab2 f2).

Ltac split_orel_obinds :=
  repeat intro;
  repeat progress
         (subst*; match goal with
                  | |- orel ?RB (match ?e with _ => _ end) (match ?e with _ => _ end) =>
                    destruct e; split_orel_obinds
                  | H: ?equive ?e1 ?e2
                    |- orel ?RA (match ?e1 with _ => _ end)
                           (match ?e2 with _ => _ end) =>
                    setoid_rewrite H
                  | |- orel ?RB (obind ?oa ?f1) (obind ?oa ?f2) =>
                    eapply orel_obind_intro_same; split_orel_obinds
                  | |- orel ?RB (obind ?oa1 ?f1) (obind ?oa2 ?f2) =>
                    eapply orel_obind_intro; split_orel_obinds
                  | |- orel ?RB (obind2 ?oa1 ?f1) (obind2 ?oa2 ?f2) =>
                    eapply orel_obind2_intro; split_orel_obinds
                  | |- orel ?RB (Some _) (Some _) =>
                    eapply orel_inversion
                  | |- RelProd _ _ _ _ =>
                    eapply pair_compat; split_orel_obinds
                  end; (reflexivity || eassumption || idtac)).

Ltac rewrite_orel_obinds :=
  repeat progress
         (subst; match goal with
                 | [ H:?equiv ?L ?R |- context [ ?L ] ] => setoid_rewrite H
                 end; try reflexivity).

Ltac solve_orel_obinds := split_orel_obinds; repeat rewrite_orel_obinds.

Section check_nodup.

  Definition check_nodup (l : list positive) :=
    Nat.eqb (PS.cardinal (ps_from_list l)) (List.length l).

  Lemma check_nodup_correct : forall l,
      check_nodup l = true ->
      NoDup l.

End check_nodup.

Section sig2.
  Context {A : Type} {P Q : A -> Prop}.

  Lemma sig2_of_sig:
    forall (s : { s : A | P s }),
      Q (proj1_sig s) ->
      { s | P s & Q s }.
  Extraction Inline sig2_of_sig.

  Lemma sig2_weaken2:
    forall {Q' : A -> Prop},
      (forall s, Q s -> Q' s) ->
      { s : A | P s & Q s } ->
      { s | P s & Q' s }.
  Extraction Inline sig2_weaken2.
End sig2.