Library prosa.util.poet

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Require Export prosa.util.list.

This file contains utility lemmas not used by Prosa itself, but still required for legacy versions of POET. They will eventually be removed from Prosa.

This lemma allows us to check proposition of the form ∀ x ∈ xs, ∃ y ∈ ys, P x y using a boolean expression all P (zip xs ys).

Lemma forall_exists_implied_by_forall_in_zip :
  ∀ {X Y : eqType} (P_bool : X × Y → bool) (P_prop : X → Y → Prop) (xs : seq X),
    (∀ x y, P_bool (x , y ) ↔ P_prop x y ) →
    (∃ ys , size xs = size ys ∧ all P_bool (zip xs ys) == true ) →
    (∀ x, x \in xs → ∃ y , P_prop x y ).