proposition: Lemma Vforall2_opt_filter A p (ts us : vector A p) (R : relation A) : forall n (ks : vector nat n), sorted ks -> (forall i (ip : i < p), Vin i ks -> R (Vnth ts ip) (Vnth us ip)) -> Vforall2_opt R (Vopt_filter ks ts) (Vopt_filter ks us).
proof: Proof. induction ks as [|k n ks IH]; intros kks_sorted tsus; simpl. ex 0 (Nat.le_refl 0). rewrite !Vsub_nil, !Vforall2_cast. split; refl. destruct (lt_dec k p). gen (sorted_cons_elim kks_sorted); intro ks_sorted. assert (tsus' : forall i (ip:i<p), Vin i ks -> R (Vnth ts ip) (Vnth us ip)). intros i ip hi. apply tsus. simpl. auto. gen (IH ks_sorted tsus'). intros [i [i1 [i2 i3]]]. assert (a : S i <= S n). lia. ex (S i) a. split. apply Vforall2_intro_nth. intros j jSi. rewrite !Vnth_sub, !Vnth_cons. simpl. destruct (lt_ge_dec 0 j). assert (b : j - 1 < i). lia. gen (Vforall2_elim_nth b i2). rewrite !Vnth_sub. erewrite Vnth_eq. erewrite Vnth_eq with (v := Vopt_filter ks us). apply impl_refl. lia. lia. apply opt_intro. apply tsus. fo. apply Vforall2_intro_nth. intros j hj. rewrite !Vnth_sub, !Vnth_cons. destruct (lt_ge_dec 0 (S i + j)). 2: lia. assert (b : j < n - i). lia. gen (Vforall2_elim_nth b i3). rewrite !Vnth_sub. erewrite Vnth_eq. erewrite Vnth_eq with (v := Vopt_filter ks us). apply impl_refl. lia. lia. assert (a : 0 <= S n). lia. ex 0 a. split. apply Vforall2_intro_nth. intros j hj. lia. apply Vforall2_intro_nth. intros j hj. rewrite !Vnth_sub, !Vnth_cons. simpl. destruct (lt_ge_dec 0 j). 2: apply opt_r_None. rewrite !Vnth_opt_filter. match goal with |- context C [lt_dec (Vnth ks ?x) p] => set (h := x) end. destruct (lt_dec (Vnth ks h) p). 2: apply opt_r_None. exfalso. unfold sorted in kks_sorted. assert (ai : 0 < S n). lia. assert (aj : j < S n). lia. gen (kks_sorted _ ai _ aj l). rewrite !Vnth_cons. destruct (lt_ge_dec 0 0). lia. destruct (lt_ge_dec 0 j). 2: lia. rewrite Vnth_eq with (h2:=h). lia. lia. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)