Library probsa.probability.prob
Require Export prosa.util.all.
From probsa.util Require Import iota indicator min.
From probsa.probability Require Import pred.
From probsa.util Require Import iota indicator min.
From probsa.probability Require Import pred.
Lemma pr_pos :
∀ {Ω} (μ : measure Ω) (P : pred Ω) (ω : Ω),
P ω →
μ ω > 0 →
ℙ<μ>{[ P ]} > 0.
Proof.
intros × Pω POS.
eapply Series_strict_pos with (n := pickle ω).
{ intros n; rewrite /countable_sum.
destruct pickle_inv ⇒ //=; last by apply Rge_refl.
destruct (P s); last by apply Rge_refl.
by destruct μ.
}
{ by rewrite /countable_sum pickleK_inv //= Pω. }
{ eapply ex_finite_lim_seq_incr; last by apply pr_sum_n.
intros; rewrite sum_Sn /plus ⇒ //=.
rewrite -{1}[sum_n _ _]Rplus_0_r; apply Rplus_le_compat_l.
rewrite /countable_sum.
destruct pickle_inv ⇒ //=; last by apply Rge_refl.
destruct (P s); last by apply Rge_refl.
by destruct μ ⇒ //=; apply Rge_le.
}
Qed.
Lemma pr_zero :
∀ {Ω} (μ : measure Ω) (P : pred Ω),
(∀ ω, μ ω > 0 → P ω = false) →
ℙ<μ>{[ P ]} = 0.
Proof.
intros × FA; apply SeriesC_0 ⇒ ω.
destruct (P ω) eqn:Pω ⇒ //.
destruct μ; move: (pmf_pos ω) ⇒ [POS|ZE]; last by done.
by specialize (FA _ POS); rewrite FA in Pω.
Qed.
Lemma pr_xpredT_ext :
∀ {Ω} (μ : measure Ω) P,
P =1 xpredT →
ℙ<μ>{[ P ]} = 1.
Proof.
intros × EQU; erewrite <-pr_xpredT.
by apply pr_eq_pred ⇒ ω; apply EQU.
Qed.
Lemma pr_pos_inv :
∀ {Ω} {μ : measure Ω} (P : pred Ω),
ℙ<μ>{[ P ]} > 0 →
∃ ω, P ω ∧ μ ω > 0.
Proof.
intros × POS; apply Series_strict_pos_inv in POS; first last.
{ intros ?.
rewrite /countable_sum.
destruct pickle_inv; rewrite //=; last by nra.
by destruct P, μ; rewrite //=; nra.
}
{ destruct POS as [i GT]; destruct (@pickle_inv Ω i) eqn:EQ;
last by rewrite /countable_sum EQ //= in GT; nra.
∃ s; rewrite /countable_sum EQ //= in GT.
by destruct P; auto; nra.
}
Qed.
Lemma pr_pos_or_zero :
∀ {Ω} (μ : measure Ω) (P : pred Ω),
ℙ<μ>{[ P ]} = 0 ∨ ℙ<μ>{[ P ]} > 0.
Proof.
have F: ∀ a, a ≥ 0 → a = 0 ∨ a > 0 by intros; nra.
intros; apply F, ge_pr_0.
Qed.
Lemma pr_leq_intersectionl :
∀ {Ω} (μ : measure Ω) (A B : pred Ω),
ℙ<μ>{[ A ∩ B ]} ≤ ℙ<μ>{[ A ]}.
Proof.
intros *; apply pr_mono_pred.
by intros ω; rewrite /intersection ⇒ /andP [Aω _].
Qed.
Lemma pr_leq_intersectionr :
∀ {Ω} (μ : measure Ω) (A B : pred Ω),
ℙ<μ>{[ A ∩ B ]} ≤ ℙ<μ>{[ B ]}.
Proof.
intros *; apply pr_mono_pred.
by intros ω; rewrite /intersection ⇒ /andP [_ Bω].
Qed.
We show that a sample space cannot be empty.
Lemma nonempty_sample_space :
∀ {Ω} {μ : measure Ω},
∃ (ω : Ω), μ ω > 0.
Proof.
intros ? [] ⇒ //=; apply Classical_Pred_Type.not_all_not_ex ⇒ NE.
have ZE : is_series (countable_sum pmf) 0.
{ apply is_seriesC_0 ⇒ ω; specialize (pmf_pos ω); specialize (NE ω).
apply Rle_antisym.
{ by apply Rnot_gt_le. }
{ by apply Rge_le, pmf_pos. }
}
apply is_series_unique in pmf_sum1, ZE.
rewrite ZE in pmf_sum1; apply R1_neq_R0.
by rewrite pmf_sum1.
Qed.
∀ {Ω} {μ : measure Ω},
∃ (ω : Ω), μ ω > 0.
Proof.
intros ? [] ⇒ //=; apply Classical_Pred_Type.not_all_not_ex ⇒ NE.
have ZE : is_series (countable_sum pmf) 0.
{ apply is_seriesC_0 ⇒ ω; specialize (pmf_pos ω); specialize (NE ω).
apply Rle_antisym.
{ by apply Rnot_gt_le. }
{ by apply Rge_le, pmf_pos. }
}
apply is_series_unique in pmf_sum1, ZE.
rewrite ZE in pmf_sum1; apply R1_neq_R0.
by rewrite pmf_sum1.
Qed.
Given two events A and B, the probability that A or B
occurs is equal to the sum of the probabilities of A and B
minus the probability of their intersection.
In other words, if we want to calculate the probability of an
event that can be expressed as the union of two events A and
B, we can find the probabilities of A and B separately, and
then subtract the probability of their intersection to avoid
double-counting.
Lemma pr_of_union :
∀ {Ω} {μ : measure Ω} (A B : pred Ω),
ℙ<μ>{[ A ∪ B ]} = ℙ<μ>{[ A ]} + ℙ<μ>{[ B ]} - ℙ<μ>{[ A ∩ B ]}.
Proof.
intros; rewrite -Series_plus; try apply pr_ex_series.
have EQU: ∀ a b c, (a + b = c → a = c - b)%R
by intros × EQ; rewrite -EQ; ring.
apply: EQU.
rewrite -Series_plus; try apply pr_ex_series; last first.
apply Series_ext ⇒ n.
rewrite -!countable_sum_plus.
apply countable_sum_ext ⇒ ω.
unfold "∪", "∩", pred_union, pred_intersection; destruct (A ω) eqn:Aω, (B ω) eqn:Bω ⇒ //=.
by rewrite Rplus_0_r Rplus_0_l.
Qed.
Lemma pr_bool_move :
∀ {Ω} {μ : measure Ω} (P : pred Ω) (B : bool),
ℙ<μ>{[ λ ω : Ω, B && P ω ]} = I[B] × ℙ<μ>{[ P ]}.
Proof.
intros ? ? ? [] ⇒ //=.
- by rewrite Rmult_1_l.
- by rewrite Rmult_0_l pr_xpred0.
Qed.
Lemma pr_eq_measure :
∀ {Ω} {μ1 μ2 : measure Ω} (P : pred Ω),
(∀ ω, μ1 ω = μ2 ω) →
ℙ<μ1>{[ P ]} = ℙ<μ2>{[ P ]}.
Proof.
by intros × EQ; apply SeriesC_ext ⇒ ω; rewrite EQ.
Qed.
Lemma pr_mono_pred_pos :
∀ {Ω} (μ : measure Ω) (P Q : pred Ω),
(∀ ω, μ ω > 0 → P ω → Q ω) →
ℙ<μ>{[ P ]} ≤ ℙ<μ>{[ Q ]}.
Proof.
intros × EQU; apply SeriesC_le; last by apply pr_ex_series.
intros ω; destruct μ ⇒ //=.
destruct (Rle_lt_or_eq_dec 0 (pmf ω)) as [POS | Z];
first by eapply Rge_le, pmf_pos.
- destruct P eqn:Pω, Q eqn:Qω.
+ by split; [apply Rge_le, pmf_pos | apply Rle_refl].
+ by move: (EQU ω POS Pω) ⇒ QωT; rewrite Qω in QωT.
+ by split; [apply Rle_refl | apply Rge_le, pmf_pos].
+ by split; apply Rle_refl.
- by rewrite -Z; destruct P, Q; split; apply Rle_refl.
Qed.
Lemma pr_eq_pred_pos :
∀ {Ω} {μ : measure Ω} (P Q : pred Ω),
(∀ ω, μ ω > 0 → P ω = Q ω) →
ℙ<μ>{[ P ]} = ℙ<μ>{[ Q ]}.
Proof.
intros × EQU; apply Series_ext ⇒ n.
rewrite /countable_sum; destruct (@pickle_inv _ n) ⇒ //=.
destruct μ ⇒ //=.
destruct (Rle_lt_or_eq_dec 0 (pmf s)) as [POS | Z];
first by eapply Rge_le, pmf_pos.
- by rewrite EQU; [reflexivity | apply Rlt_gt].
- by rewrite -Z; destruct P, Q.
Qed.
Lemma pr_pred_compl :
∀ {Ω} {μ : measure Ω} (P : pred Ω),
ℙ<μ>{[ P ]} = 1 - ℙ<μ>{[ !P ]}.
Proof.
intros.
have EQ: ∀ a b, (a + b = 1 → a = 1 - b)%R by clear; intros; nra.
apply:EQ; rewrite -[(_ + _)%R]Rminus_0_r.
replace 0%R with (ℙ< μ >{[ predI P (! P)]} )%R; first last.
{ erewrite pr_eq_pred with (Q:= xpred0).
- by apply pr_xpred0.
- by intros ?; rewrite !unfold_in /neg_op /neg_pred; destruct (P x).
}
rewrite -pr_union; erewrite <-pr_xpredT; apply pr_eq_pred.
by intros ?; rewrite !unfold_in /neg_op /neg_pred; destruct (P x).
Qed.
Lemma law_of_total_probability_simple :
∀ {Ω} {μ : measure Ω} (E P : pred Ω),
ℙ<μ>{[ E ]} = ℙ<μ>{[ E ∩ P ]} + ℙ<μ>{[ E ∩ !P ]}.
Proof.
intros; rewrite -Series_plus; try by apply pr_ex_series.
apply Series_ext ⇒ n; rewrite -countable_sum_plus.
apply countable_sum_ext ⇒ ω.
unfold "∩", pred_intersection, neg_op, neg_pred.
by destruct P, E ⇒ //=; rewrite ?Rplus_0_r ?Rplus_0_l.
Qed.
Lemma pr_ineq_compl :
∀ {ΩX ΩY} {μX : measure ΩX} {μY : measure ΩY} (X : ΩX → nat) (Y : ΩY → nat) (c : nat),
ℙ<μX>{[ λ ω, (c ≥ X ω)%N ]} ≥ ℙ<μY>{[ λ ω, (c ≥ Y ω)%N ]} →
ℙ<μX>{[ λ ω, (c < X ω)%N ]} ≤ ℙ<μY>{[ λ ω, (c < Y ω)%N ]}.
Proof.
intros × GE; rewrite pr_pred_compl [in X in (_ ≤ X)%R]pr_pred_compl.
have EQ: ∀ a b, (a ≥ b → 1 - a ≤ 1 - b)%R by clear; intros; nra.
apply: EQ; erewrite pr_eq_pred with (Q := λ ω : ΩX, (X ω ≤ c)%N);
first erewrite pr_eq_pred with (Q := λ ω : ΩY, (Y ω ≤ c)%N);
first by done.
all: by intros ω; rewrite !unfold_in -leqNgt.
Qed.
Lemma frechet_min :
∀ {Ω} {μ : measure Ω} {X : eqType} (P : X → pred Ω) (xs : seq X),
ℙ<μ>{[ λ ω : Ω, all (fun x ⇒ P x ω) xs ]}
≤ min1 [seq ℙ<μ>{[ P x ]} | x <- xs].
Proof.
induction xs.
{ by rewrite /min1 //=; apply pr_le_1. }
{ rewrite map_cons min1_cons; apply Rmin_glb.
{ by eapply Rle_trans; [apply pr_leq_intersectionl | apply Rle_refl]. }
{ by eapply Rle_trans; [apply pr_leq_intersectionr | apply IHxs]. }
}
Qed.
∀ {Ω} {μ : measure Ω} (A B : pred Ω),
ℙ<μ>{[ A ∪ B ]} = ℙ<μ>{[ A ]} + ℙ<μ>{[ B ]} - ℙ<μ>{[ A ∩ B ]}.
Proof.
intros; rewrite -Series_plus; try apply pr_ex_series.
have EQU: ∀ a b c, (a + b = c → a = c - b)%R
by intros × EQ; rewrite -EQ; ring.
apply: EQU.
rewrite -Series_plus; try apply pr_ex_series; last first.
apply Series_ext ⇒ n.
rewrite -!countable_sum_plus.
apply countable_sum_ext ⇒ ω.
unfold "∪", "∩", pred_union, pred_intersection; destruct (A ω) eqn:Aω, (B ω) eqn:Bω ⇒ //=.
by rewrite Rplus_0_r Rplus_0_l.
Qed.
Lemma pr_bool_move :
∀ {Ω} {μ : measure Ω} (P : pred Ω) (B : bool),
ℙ<μ>{[ λ ω : Ω, B && P ω ]} = I[B] × ℙ<μ>{[ P ]}.
Proof.
intros ? ? ? [] ⇒ //=.
- by rewrite Rmult_1_l.
- by rewrite Rmult_0_l pr_xpred0.
Qed.
Lemma pr_eq_measure :
∀ {Ω} {μ1 μ2 : measure Ω} (P : pred Ω),
(∀ ω, μ1 ω = μ2 ω) →
ℙ<μ1>{[ P ]} = ℙ<μ2>{[ P ]}.
Proof.
by intros × EQ; apply SeriesC_ext ⇒ ω; rewrite EQ.
Qed.
Lemma pr_mono_pred_pos :
∀ {Ω} (μ : measure Ω) (P Q : pred Ω),
(∀ ω, μ ω > 0 → P ω → Q ω) →
ℙ<μ>{[ P ]} ≤ ℙ<μ>{[ Q ]}.
Proof.
intros × EQU; apply SeriesC_le; last by apply pr_ex_series.
intros ω; destruct μ ⇒ //=.
destruct (Rle_lt_or_eq_dec 0 (pmf ω)) as [POS | Z];
first by eapply Rge_le, pmf_pos.
- destruct P eqn:Pω, Q eqn:Qω.
+ by split; [apply Rge_le, pmf_pos | apply Rle_refl].
+ by move: (EQU ω POS Pω) ⇒ QωT; rewrite Qω in QωT.
+ by split; [apply Rle_refl | apply Rge_le, pmf_pos].
+ by split; apply Rle_refl.
- by rewrite -Z; destruct P, Q; split; apply Rle_refl.
Qed.
Lemma pr_eq_pred_pos :
∀ {Ω} {μ : measure Ω} (P Q : pred Ω),
(∀ ω, μ ω > 0 → P ω = Q ω) →
ℙ<μ>{[ P ]} = ℙ<μ>{[ Q ]}.
Proof.
intros × EQU; apply Series_ext ⇒ n.
rewrite /countable_sum; destruct (@pickle_inv _ n) ⇒ //=.
destruct μ ⇒ //=.
destruct (Rle_lt_or_eq_dec 0 (pmf s)) as [POS | Z];
first by eapply Rge_le, pmf_pos.
- by rewrite EQU; [reflexivity | apply Rlt_gt].
- by rewrite -Z; destruct P, Q.
Qed.
Lemma pr_pred_compl :
∀ {Ω} {μ : measure Ω} (P : pred Ω),
ℙ<μ>{[ P ]} = 1 - ℙ<μ>{[ !P ]}.
Proof.
intros.
have EQ: ∀ a b, (a + b = 1 → a = 1 - b)%R by clear; intros; nra.
apply:EQ; rewrite -[(_ + _)%R]Rminus_0_r.
replace 0%R with (ℙ< μ >{[ predI P (! P)]} )%R; first last.
{ erewrite pr_eq_pred with (Q:= xpred0).
- by apply pr_xpred0.
- by intros ?; rewrite !unfold_in /neg_op /neg_pred; destruct (P x).
}
rewrite -pr_union; erewrite <-pr_xpredT; apply pr_eq_pred.
by intros ?; rewrite !unfold_in /neg_op /neg_pred; destruct (P x).
Qed.
Lemma law_of_total_probability_simple :
∀ {Ω} {μ : measure Ω} (E P : pred Ω),
ℙ<μ>{[ E ]} = ℙ<μ>{[ E ∩ P ]} + ℙ<μ>{[ E ∩ !P ]}.
Proof.
intros; rewrite -Series_plus; try by apply pr_ex_series.
apply Series_ext ⇒ n; rewrite -countable_sum_plus.
apply countable_sum_ext ⇒ ω.
unfold "∩", pred_intersection, neg_op, neg_pred.
by destruct P, E ⇒ //=; rewrite ?Rplus_0_r ?Rplus_0_l.
Qed.
Lemma pr_ineq_compl :
∀ {ΩX ΩY} {μX : measure ΩX} {μY : measure ΩY} (X : ΩX → nat) (Y : ΩY → nat) (c : nat),
ℙ<μX>{[ λ ω, (c ≥ X ω)%N ]} ≥ ℙ<μY>{[ λ ω, (c ≥ Y ω)%N ]} →
ℙ<μX>{[ λ ω, (c < X ω)%N ]} ≤ ℙ<μY>{[ λ ω, (c < Y ω)%N ]}.
Proof.
intros × GE; rewrite pr_pred_compl [in X in (_ ≤ X)%R]pr_pred_compl.
have EQ: ∀ a b, (a ≥ b → 1 - a ≤ 1 - b)%R by clear; intros; nra.
apply: EQ; erewrite pr_eq_pred with (Q := λ ω : ΩX, (X ω ≤ c)%N);
first erewrite pr_eq_pred with (Q := λ ω : ΩY, (Y ω ≤ c)%N);
first by done.
all: by intros ω; rewrite !unfold_in -leqNgt.
Qed.
Lemma frechet_min :
∀ {Ω} {μ : measure Ω} {X : eqType} (P : X → pred Ω) (xs : seq X),
ℙ<μ>{[ λ ω : Ω, all (fun x ⇒ P x ω) xs ]}
≤ min1 [seq ℙ<μ>{[ P x ]} | x <- xs].
Proof.
induction xs.
{ by rewrite /min1 //=; apply pr_le_1. }
{ rewrite map_cons min1_cons; apply Rmin_glb.
{ by eapply Rle_trans; [apply pr_leq_intersectionl | apply Rle_refl]. }
{ by eapply Rle_trans; [apply pr_leq_intersectionr | apply IHxs]. }
}
Qed.
The following lemma states that the measure of the union of a
disjoint sequence of events (represented as λ ω, has (fun i ⇒ p i
ω) (index_iota t1 t2)) is equal to the sum of the measures of the
individual events. Note that the predicate λ ω, has (fun i ⇒ p i ω)
(index_iota t1 t2) has a simple intuitive interpretation -- the
predicate is true for a given ω : Ω if and only if p i ω is
true for at least one of the indices i from the range t1 to
t2-1.
More specifically, given a probability space (Ω,μ) and a
sequence of predicates p i : Ω → Prop for i ranging from t1 to
t2-1, the lemma asserts that if the predicates are pairwise
disjoint (i.e., p i and p j have no common points for distinct
i and j), then the probability of the union of these events is
equal to the sum of the probabilities of each individual event.
The proof of the lemma relies on the fact that the sequence of
events we consider is pairwise disjoint. This allows us to apply
the additivity property of measures, which states that the measure
of the union of a sequence of pairwise disjoint events is equal to
the sum of the measures of the individual events.
The condition that the predicates p i are pairwise disjoint is
essential for the proof of the lemma to hold. Without this
condition, the events we consider may have overlapping points, and
the additivity property of measures would not apply. In fact, the
sum of the probabilities of the individual events can be greater
than the probability of the union of events with overlapping
points.
Lemma union_disj_eq_sum_prob :
∀ {Ω} {μ : measure Ω} (t1 t2 : nat) (p : nat → pred Ω),
(∀ (ω : Ω) (i1 i2 : nat), p i1 ω → p i2 ω → i1 = i2) →
ℙ<μ>{[ λ ω, has (fun i ⇒ p i ω) (index_iota t1 t2) ]} = ∑_{t1 ≤ i < t2} ℙ<μ>{[ p i ]}.
Proof.
intros × DISJ.
destruct (leqP t1 t2); [rename i into LE | rename i into GT]; first last.
- rewrite big_geq; last by ssrlia.
unfold index_iota; replace (t2 - t1)%nat with 0%nat ⇒ //=; last by ssrlia.
by apply pr_xpred0.
- interval_to_duration t1 t2 δ.
induction δ.
+ rewrite addn0 big_geq; last by ssrlia.
rewrite /index_iota subnn //=.
by apply pr_xpred0.
+ rewrite addnS big_nat_recr //=; last by rewrite leq_addr.
rewrite -IHδ; clear IHδ.
rewrite (@pr_eq_pred'
_ _ _ (fun ω ⇒ p (t1 + δ)%nat ω || has (p^~ ω) (index_iota t1 (t1 + δ)))); last first.
{ intros ?; rewrite index_iota_recr ?has_cat ?has_seq1; last by rewrite leq_addr.
by split; move ⇒ /orP [T|T]; apply/orP; [right|left|right|left]. }
rewrite pr_of_union -[(_ + ℙ<μ>{[ p (t1 + δ)%N]})%R]Rminus_0_r.
rewrite Rplus_comm; apply Rminus_eq_compat_l.
rewrite -(@pr_xpred0 Ω μ).
apply pr_eq_pred' ⇒ ω; split; intros; last by done.
move: H ⇒ /andP [Pδ /hasP [i IN Pi]]; move: IN; rewrite mem_iota ⇒ /andP [LE1 LT2].
by specialize (DISJ _ _ _ Pδ Pi); ssrlia.
Qed.
Remark allpairs_rvar :
∀ {Ω} {μ : measure Ω} {X Y Z : eqType} (f : X → Ω → Y → Z) (xs : seq X) (ys : X → seq Y),
[seq mkRvar μ (fun ω ⇒ f x ω y) | x <- xs, y <- ys x]
= map (fun '(x,y) ⇒ mkRvar μ (fun ω ⇒ f x ω y)) [seq (x,y) | x <- xs, y <- ys x].
Proof.
clear; intros.
induction xs; first by done.
rewrite //= map_cat //= IHxs; f_equal.
clear IHxs; induction (ys a); first by done.
by rewrite //= IHl.
Qed.
∀ {Ω} {μ : measure Ω} (t1 t2 : nat) (p : nat → pred Ω),
(∀ (ω : Ω) (i1 i2 : nat), p i1 ω → p i2 ω → i1 = i2) →
ℙ<μ>{[ λ ω, has (fun i ⇒ p i ω) (index_iota t1 t2) ]} = ∑_{t1 ≤ i < t2} ℙ<μ>{[ p i ]}.
Proof.
intros × DISJ.
destruct (leqP t1 t2); [rename i into LE | rename i into GT]; first last.
- rewrite big_geq; last by ssrlia.
unfold index_iota; replace (t2 - t1)%nat with 0%nat ⇒ //=; last by ssrlia.
by apply pr_xpred0.
- interval_to_duration t1 t2 δ.
induction δ.
+ rewrite addn0 big_geq; last by ssrlia.
rewrite /index_iota subnn //=.
by apply pr_xpred0.
+ rewrite addnS big_nat_recr //=; last by rewrite leq_addr.
rewrite -IHδ; clear IHδ.
rewrite (@pr_eq_pred'
_ _ _ (fun ω ⇒ p (t1 + δ)%nat ω || has (p^~ ω) (index_iota t1 (t1 + δ)))); last first.
{ intros ?; rewrite index_iota_recr ?has_cat ?has_seq1; last by rewrite leq_addr.
by split; move ⇒ /orP [T|T]; apply/orP; [right|left|right|left]. }
rewrite pr_of_union -[(_ + ℙ<μ>{[ p (t1 + δ)%N]})%R]Rminus_0_r.
rewrite Rplus_comm; apply Rminus_eq_compat_l.
rewrite -(@pr_xpred0 Ω μ).
apply pr_eq_pred' ⇒ ω; split; intros; last by done.
move: H ⇒ /andP [Pδ /hasP [i IN Pi]]; move: IN; rewrite mem_iota ⇒ /andP [LE1 LT2].
by specialize (DISJ _ _ _ Pδ Pi); ssrlia.
Qed.
Remark allpairs_rvar :
∀ {Ω} {μ : measure Ω} {X Y Z : eqType} (f : X → Ω → Y → Z) (xs : seq X) (ys : X → seq Y),
[seq mkRvar μ (fun ω ⇒ f x ω y) | x <- xs, y <- ys x]
= map (fun '(x,y) ⇒ mkRvar μ (fun ω ⇒ f x ω y)) [seq (x,y) | x <- xs, y <- ys x].
Proof.
clear; intros.
induction xs; first by done.
rewrite //= map_cat //= IHxs; f_equal.
clear IHxs; induction (ys a); first by done.
by rewrite //= IHl.
Qed.