PartialBijection.v

From Tealeaves Require Import
  Functors.Option.

#[local] Generalizable Variables A B f g.

(** * Partial Bijections *)
(**********************************************************************)
Class PartialBijection {A B: Type}
  (f: A -> option B)
  (g: B -> option A) :=
  { pb_fwd: forall (a: A) (b: B),
      f a = Some b -> g b = Some a;
    pb_bwd: forall (b: B) (a: A),
      g b = Some a -> f a = Some b;

  }.

Lemma pb_iff `{PartialBijection A B f g}:
  forall (a: A) (b: B),
    f a = Some b <-> g b = Some a.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
forall (a : A) (b : B), f a = Some b <-> g b = Some a
Proof.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
forall (a : A) (b : B), f a = Some b <-> g b = Some a
  intros.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
f a = Some b <-> g b = Some a split.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
f a = Some b -> g b = Some a
A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
g b = Some a -> f a = Some b
  apply pb_fwd.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
g b = Some a -> f a = Some b
  apply pb_bwd.
Qed.

Lemma pb_fwd_None `{PartialBijection A B f g}:
  forall (a: A),
    f a = None -> forall b, g b = Some a -> False.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
forall a : A,
f a = None -> forall b : B, g b = Some a -> False
Proof.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
forall a : A,
f a = None -> forall b : B, g b = Some a -> False
  introv H1 H2.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
H1: f a = None
b: B
H2: g b = Some a
False
  apply pb_bwd in H2.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
H1: f a = None
b: B
H2: f a = Some b
False
  congruence.
Qed.


Lemma pb_bwd_None `{PartialBijection A B f g}:
  forall (b: B),
    g b = None -> forall a, f a = Some b -> False.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
forall b : B,
g b = None -> forall a : A, f a = Some b -> False
Proof.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
forall b : B,
g b = None -> forall a : A, f a = Some b -> False
  introv H1 H2.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
b: B
H1: g b = None
a: A
H2: f a = Some b
False
  apply pb_fwd in H2.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
b: B
H1: g b = None
a: A
H2: g b = Some a
False
  congruence.
Qed.


Lemma pb_iff_None `{PartialBijection A B f g}:
  forall (a: A),
    f a = None <-> forall (b: B), ~ (g b = Some a).A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
forall a : A,
f a = None <-> (forall b : B, g b <> Some a)
Proof.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
forall a : A,
f a = None <-> (forall b : B, g b <> Some a)
  intros.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
f a = None <-> (forall b : B, g b <> Some a) remember (f a) as fa.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
fa: option B
Heqfa: fa = f a
fa = None <-> (forall b : B, g b <> Some a)
  symmetry in Heqfa.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
fa: option B
Heqfa: f a = fa
fa = None <-> (forall b : B, g b <> Some a)
  destruct fa.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
Heqfa: f a = Some b
Some b = None <-> (forall b : B, g b <> Some a)
A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
Heqfa: f a = None
None = None <-> (forall b : B, g b <> Some a)
  -A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
Heqfa: f a = Some b
Some b = None <-> (forall b : B, g b <> Some a) apply pb_fwd in Heqfa.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
Heqfa: g b = Some a
Some b = None <-> (forall b : B, g b <> Some a)
    split.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
Heqfa: g b = Some a
Some b = None -> forall b : B, g b <> Some a
A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
Heqfa: g b = Some a
(forall b : B, g b <> Some a) -> Some b = None
    inversion 1.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
Heqfa: g b = Some a
(forall b : B, g b <> Some a) -> Some b = None
    intros contra.A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
Heqfa: g b = Some a
contra: forall b : B, g b <> Some a
Some b = None
    specialize (contra b Heqfa).A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
b: B
Heqfa: g b = Some a
contra: False
Some b = None
    contradiction.
  -A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
Heqfa: f a = None
None = None <-> (forall b : B, g b <> Some a) specialize (pb_fwd_None a Heqfa).A, B: Type
f: A -> option B
g: B -> option A
H: PartialBijection f g
a: A
Heqfa: f a = None
(forall b : B, g b = Some a -> False) ->
None = None <-> (forall b : B, g b <> Some a)
    split; auto.
Qed.


(** ** Characterizing Partial Bijections *)
(**********************************************************************)
Theorem partial_bijection_spec1:
  forall (A B: Type) (f: A -> option B) (g: B -> option A),
    (forall (a: A), f a = None \/ map g (f a) = Some (Some a)) ->
    (forall (b: B), g b = None \/ map f (g b) = Some (Some b)) ->
    (forall (a: A) (b: B), f a = Some b <-> g b = Some a).forall (A B : Type) (f : A -> option B)
  (g : B -> option A),
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a)) ->
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) ->
forall (a : A) (b : B), f a = Some b <-> g b = Some a
Proof.forall (A B : Type) (f : A -> option B)
  (g : B -> option A),
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a)) ->
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) ->
forall (a : A) (b : B), f a = Some b <-> g b = Some a
  introv HA HB.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
forall (a : A) (b : B), f a = Some b <-> g b = Some a
  intros a b.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
a: A
b: B
f a = Some b <-> g b = Some a
  split.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
a: A
b: B
f a = Some b -> g b = Some a
A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
a: A
b: B
g b = Some a -> f a = Some b
  -A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
a: A
b: B
f a = Some b -> g b = Some a intros Hf.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
a: A
b: B
Hf: f a = Some b
g b = Some a
    specialize (HA a).A, B: Type
f: A -> option B
g: B -> option A
a: A
HA: f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
b: B
Hf: f a = Some b
g b = Some a
    rewrite Hf in HA.A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
HA: Some b = None \/ map g (Some b) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
Hf: f a = Some b
g b = Some a
    cbn in HA.A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
HA: Some b = None \/ Some (g b) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
Hf: f a = Some b
g b = Some a
    inversion HA.A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
HA: Some b = None \/ Some (g b) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
Hf: f a = Some b
H: Some b = None
g b = Some a
A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
HA: Some b = None \/ Some (g b) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
Hf: f a = Some b
H: Some (g b) = Some (Some a)
g b = Some a
    +A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
HA: Some b = None \/ Some (g b) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
Hf: f a = Some b
H: Some b = None
g b = Some a inversion H.
    +A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
HA: Some b = None \/ Some (g b) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
Hf: f a = Some b
H: Some (g b) = Some (Some a)
g b = Some a inversion H.A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
HA: Some b = None \/ Some (g b) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
Hf: f a = Some b
H: Some (g b) = Some (Some a)
H1: g b = Some a
g b = g b
      reflexivity.
  -A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
a: A
b: B
g b = Some a -> f a = Some b intros Hg.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
HB: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
a: A
b: B
Hg: g b = Some a
f a = Some b
    specialize (HB b).A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
b: B
HB: g b = None \/ map f (g b) = Some (Some b)
a: A
Hg: g b = Some a
f a = Some b
    rewrite Hg in HB.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
b: B
a: A
HB: Some a = None \/ map f (Some a) = Some (Some b)
Hg: g b = Some a
f a = Some b
    cbn in HB.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
b: B
a: A
HB: Some a = None \/ Some (f a) = Some (Some b)
Hg: g b = Some a
f a = Some b
    inversion HB.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
b: B
a: A
HB: Some a = None \/ Some (f a) = Some (Some b)
Hg: g b = Some a
H: Some a = None
f a = Some b
A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
b: B
a: A
HB: Some a = None \/ Some (f a) = Some (Some b)
Hg: g b = Some a
H: Some (f a) = Some (Some b)
f a = Some b
    +A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
b: B
a: A
HB: Some a = None \/ Some (f a) = Some (Some b)
Hg: g b = Some a
H: Some a = None
f a = Some b inversion H.
    +A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
b: B
a: A
HB: Some a = None \/ Some (f a) = Some (Some b)
Hg: g b = Some a
H: Some (f a) = Some (Some b)
f a = Some b inversion H.A, B: Type
f: A -> option B
g: B -> option A
HA: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
b: B
a: A
HB: Some a = None \/ Some (f a) = Some (Some b)
Hg: g b = Some a
H: Some (f a) = Some (Some b)
H1: f a = Some b
f a = f a
      reflexivity.
Qed.

Theorem partial_bijection_spec2:
  forall (A B: Type) (f: A -> option B) (g: B -> option A),
    (forall (a: A) (b: B), f a = Some b <-> g b = Some a) ->
    (forall (a: A), f a = None \/ map g (f a) = Some (Some a)).forall (A B : Type) (f : A -> option B)
  (g : B -> option A),
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) ->
forall a : A,
f a = None \/ map g (f a) = Some (Some a)
Proof.forall (A B : Type) (f : A -> option B)
  (g : B -> option A),
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) ->
forall a : A,
f a = None \/ map g (f a) = Some (Some a)
  introv H.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
forall a : A,
f a = None \/ map g (f a) = Some (Some a) intro a.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
a: A
f a = None \/ map g (f a) = Some (Some a)
  specialize (H a).A, B: Type
f: A -> option B
g: B -> option A
a: A
H: forall b : B, f a = Some b <-> g b = Some a
f a = None \/ map g (f a) = Some (Some a)
  destruct (f a) as [b|].A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
H: forall b0 : B, Some b = Some b0 <-> g b0 = Some a
Some b = None \/ map g (Some b) = Some (Some a)
A, B: Type
f: A -> option B
g: B -> option A
a: A
H: forall b : B, None = Some b <-> g b = Some a
None = None \/ map g None = Some (Some a)
  -A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
H: forall b0 : B, Some b = Some b0 <-> g b0 = Some a
Some b = None \/ map g (Some b) = Some (Some a) right.A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
H: forall b0 : B, Some b = Some b0 <-> g b0 = Some a
map g (Some b) = Some (Some a)
    destruct (H b) as [H1 _].A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
H: forall b0 : B, Some b = Some b0 <-> g b0 = Some a
H1: Some b = Some b -> g b = Some a
map g (Some b) = Some (Some a)
    specialize (H1 ltac:(reflexivity)).A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
H: forall b0 : B, Some b = Some b0 <-> g b0 = Some a
H1: g b = Some a
map g (Some b) = Some (Some a)
    cbn.A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
H: forall b0 : B, Some b = Some b0 <-> g b0 = Some a
H1: g b = Some a
Some (g b) = Some (Some a) fequal.A, B: Type
f: A -> option B
g: B -> option A
a: A
b: B
H: forall b0 : B, Some b = Some b0 <-> g b0 = Some a
H1: g b = Some a
g b = Some a
    assumption.
  -A, B: Type
f: A -> option B
g: B -> option A
a: A
H: forall b : B, None = Some b <-> g b = Some a
None = None \/ map g None = Some (Some a) now left.
Qed.

Theorem partial_bijection_spec3:
  forall (A B: Type) (f: A -> option B) (g: B -> option A),
    (forall (a: A) (b: B), f a = Some b <-> g b = Some a) ->
    (forall (b: B), g b = None \/ map f (g b) = Some (Some b)).forall (A B : Type) (f : A -> option B)
  (g : B -> option A),
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) ->
forall b : B,
g b = None \/ map f (g b) = Some (Some b)
Proof.forall (A B : Type) (f : A -> option B)
  (g : B -> option A),
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) ->
forall b : B,
g b = None \/ map f (g b) = Some (Some b)
  introv H.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
forall b : B,
g b = None \/ map f (g b) = Some (Some b) intro b.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
g b = None \/ map f (g b) = Some (Some b)
  remember (g b) as gb.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
gb: option A
Heqgb: gb = g b
gb = None \/ map f gb = Some (Some b)
  destruct gb as [a|].A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
a: A
Heqgb: Some a = g b
Some a = None \/ map f (Some a) = Some (Some b)
A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
Heqgb: None = g b
None = None \/ map f None = Some (Some b)
  -A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
a: A
Heqgb: Some a = g b
Some a = None \/ map f (Some a) = Some (Some b) right.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
a: A
Heqgb: Some a = g b
map f (Some a) = Some (Some b)
    cbn.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
a: A
Heqgb: Some a = g b
Some (f a) = Some (Some b)
    fequal.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
a: A
Heqgb: Some a = g b
f a = Some b
    apply H.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
a: A
Heqgb: Some a = g b
g b = Some a
    symmetry.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
a: A
Heqgb: Some a = g b
Some a = g b
    assumption.
  -A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
b: B
Heqgb: None = g b
None = None \/ map f None = Some (Some b) now left.
Qed.

(** ** Specification *)
(**********************************************************************)
Theorem partial_bijection_spec:
  forall (A B: Type) (f: A -> option B) (g: B -> option A),
    (forall (a: A) (b: B), f a = Some b <-> g b = Some a) <->
      (forall (b: B), g b = None \/ map f (g b) = Some (Some b)) /\
        (forall (a: A), f a = None \/ map g (f a) = Some (Some a)).forall (A B : Type) (f : A -> option B)
  (g : B -> option A),
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) <->
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) /\
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a))
Proof.forall (A B : Type) (f : A -> option B)
  (g : B -> option A),
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) <->
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) /\
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a))
  intros.A, B: Type
f: A -> option B
g: B -> option A
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) <->
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) /\
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a)) split.A, B: Type
f: A -> option B
g: B -> option A
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) ->
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) /\
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a))
A, B: Type
f: A -> option B
g: B -> option A
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) /\
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a)) ->
forall (a : A) (b : B), f a = Some b <-> g b = Some a
  -A, B: Type
f: A -> option B
g: B -> option A
(forall (a : A) (b : B), f a = Some b <-> g b = Some a) ->
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) /\
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a)) intros.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) /\
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a)) split.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
forall b : B,
g b = None \/ map f (g b) = Some (Some b)
A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
forall a : A,
f a = None \/ map g (f a) = Some (Some a)
    now apply partial_bijection_spec2.A, B: Type
f: A -> option B
g: B -> option A
H: forall (a : A) (b : B),
f a = Some b <-> g b = Some a
forall a : A,
f a = None \/ map g (f a) = Some (Some a)
    now apply partial_bijection_spec3.
  -A, B: Type
f: A -> option B
g: B -> option A
(forall b : B,
 g b = None \/ map f (g b) = Some (Some b)) /\
(forall a : A,
 f a = None \/ map g (f a) = Some (Some a)) ->
forall (a : A) (b : B), f a = Some b <-> g b = Some a intros [H1 H2].A, B: Type
f: A -> option B
g: B -> option A
H1: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
H2: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
forall (a : A) (b : B), f a = Some b <-> g b = Some a
    apply partial_bijection_spec1.A, B: Type
f: A -> option B
g: B -> option A
H1: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
H2: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
forall a : A,
f a = None \/ map g (f a) = Some (Some a)
A, B: Type
f: A -> option B
g: B -> option A
H1: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
H2: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
forall b : B,
g b = None \/ map f (g b) = Some (Some b)
    assumption.A, B: Type
f: A -> option B
g: B -> option A
H1: forall b : B,
g b = None \/ map f (g b) = Some (Some b)
H2: forall a : A,
f a = None \/ map g (f a) = Some (Some a)
forall b : B,
g b = None \/ map f (g b) = Some (Some b)
    assumption.
Qed.

(** * Partial Bijections with Domain Specifications *)
(**********************************************************************)
Class PartialBijectionSpec
  (A B: Type)
  (P: A -> Prop) (Q: B -> Prop)
  (f: A -> option B)
  (g: B -> option A) :=
  { pb_spec_iff: forall (a: A) (b: B),
      f a = Some b <-> g b = Some a;
    pb_P: forall (a: A), f a = None <-> ~ (P a);
    pb_Q: forall (b: B), g b = None <-> ~ (Q b);
  }.