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 ZArith.BinInt.

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 Coq Require Export PeanoNat.
From Coq Require Export Lia.

Open Scope list.

Common definitions

Finite sets and finite maps

Definition ident := positive.

Module PS := Coq.MSets.MSetPositive.PositiveSet.
Module PSP := MSetProperties.WPropertiesOn Pos PS.
Module PSF := MSetFacts.Facts PS.
Module PSE := MSetEqProperties.WEqPropertiesOn Pos PS.
Module PSdec := Coq.MSets.MSetDecide.WDecide PS.

Definition ident_eq_dec := Pos.eq_dec.
Definition ident_eqb := Pos.eqb.

Global Instance: EqDec ident eq := { equiv_dec := ident_eq_dec }.

Implicit Type i j: ident.

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_ident (x : ident): list ident -> bool :=
  existsb (fun y => ident_eqb y x).

Lemma mem_ident_spec : forall x xs,
    mem_ident x xs = true <-> In x xs.

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.

Corollary mem_assoc_ident_false_iff:
  forall {A} x (xs: list (ident * A)),
    mem_assoc_ident x xs = false <->
    ~ InMembers x 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.

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

Module Type IDS.
  Parameter bool_id : ident.
  Parameter true_id : ident.
  Parameter false_id : ident.

  Parameter self : ident.
  Parameter out : ident.
  Parameter temp : ident.

  Parameter step : ident.
  Parameter reset : ident.

  Parameter elab : ident.
  Parameter last : ident.
  Parameter auto : ident.
  Parameter switch : ident.
  Parameter local : ident.
  Parameter norm1 : ident.
  Parameter norm2 : ident.
  Parameter obc2c : ident.

  Definition elab_prefs := PS.singleton elab.
  Definition last_prefs := PS.add last elab_prefs.
  Definition auto_prefs := PS.add auto last_prefs.
  Definition switch_prefs := PS.add switch auto_prefs.
  Definition local_prefs := PS.add local switch_prefs.
  Definition norm1_prefs := PS.add norm1 local_prefs.
  Definition norm2_prefs := PS.add norm2 norm1_prefs.

  Definition gensym_prefs := [elab; last; auto; switch; local; 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 auto_atom : atom auto.
  Conjecture last_atom : atom last.
  Conjecture switch_atom : atom switch.
  Conjecture local_atom : atom local.
  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 -> (option ident) -> ident -> ident.

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

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

  Definition AtomOrGensym (prefs : PS.t) (id : ident) :=
    atom id \/ PS.Exists (fun pre => exists n hint, id = gensym pre hint 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.

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

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.

Lemma Nat2Z_inj_pow:
  forall m n,
    Z.of_nat (n ^ m) = Zpower.Zpower_nat (Z.of_nat n) m.

Section IsNoneSome.
  Context {A : Type}.

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

  Definition 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.

Global Hint Unfold idty idck : list.

Lemma In_of_list : forall xs x,
    PS.In x (PSP.of_list xs) <-> In x xs.

Corollary 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) : list A -> option (list B) :=
    fold_right (fun x ys => match f x, ys with
                            | Some y, Some ys => Some (y :: ys)
                            | _, _ => None
                            end) (Some []).

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

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

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

End OptionLists.


Definition or_default {A} (d: A) (o: option A) : A :=
  match o with Some a => a | None => d end.

Definition or_default_with {A B} (d: B) (f: A -> B) (o: option A) : B :=
  match o with Some a => f a | None => d end.


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.

  Global Instance orel_preord `{PreOrder A R} : PreOrder orel.

  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.
Global Hint Constructors orel : datatypes.
Global Hint Extern 5 (orel _ ?x ?x) => reflexivity : datatypes.

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.

Global 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).

Global 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).

Global 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)).

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

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

Global Program 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 }.


Section ORelB.
  Context {A : Type}
          (f : A -> A -> bool).

  Definition orelb (x y : option A) :=
    match x, y with
    | None, None => true
    | Some x, Some y => f x y
    | _, _ => false
    end.

  Lemma orelb_orel : forall R x y,
      (forall x y, f x y = true <-> R x y) ->
      orelb x y = true <-> orel R x y.

End ORelB.


Section ORel2.

  Context {A B : Type}
          (R : A -> B -> Prop).

  Inductive orel2 : option A -> option B -> Prop :=
  | Orel2n : orel2 None None
  | Orel2s : forall sx sy,
      R sx sy ->
      orel2 (Some sx) (Some sy).

  Lemma orel2_inversion:
    forall x y, orel2 (Some x) (Some y) <-> R x y.

End ORel2.



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.

Declare Scope option_monad_scope.

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.