Require Import RingLike.IterAnd.

From Stdlib Require Import Utf8 Arith.
Import List.ListNotations.

Require Import Misc Utils.

Notation "'⋀' ( i = b , e ) , g" :=
  (iter_seq b e (λ c i, (c && g)%bool) true)
  (at level 36, i at level 0, b at level 60, e at level 60,
   right associativity,
   format "'[hv ' ⋀ ( i = b , e ) , '/' '[' g ']' ']'").

Notation "'⋀' ( i ∈ l ) , g" :=
  (iter_list l (λ c i, (c && g)%bool) true)
  (at level 36, i at level 0, l at level 60,
   right associativity,
   format "'[hv ' ⋀ ( i ∈ l ) , '/' '[' g ']' ']'").

Theorem all_true_rngl_and_list_true_iff : ∀ A (l : list A) f,
  (∀ a, a ∈ l → f a = true)
  ↔ ⋀ (a ∈ l), f a = true.
Theorem rngl_and_list_cons : ∀ A (a : A) la f,
  ⋀ (i ∈ a :: la), f i = (f a && ⋀ (i ∈ la), f i)%bool.

Theorem rngl_and_list_empty : ∀ A g (l : list A),
  l = [] → ⋀ (i ∈ l), g i = true.

Theorem fold_left_rngl_and_fun_from_true : ∀ A a l (f : A → _),
  (List.fold_left (λ c i, c && f i) l a =
   a && List.fold_left (λ c i, c && f i) l true)%bool.

Theorem rngl_and_list_app : ∀ A (la lb : list A) f,
  ⋀ (i ∈ la ++ lb), f i = (⋀ (i ∈ la), f i && ⋀ (i ∈ lb), f i)%bool.

Theorem rngl_and_list_map : ∀ A B (f : A → B) (g : B → _) l,
  ⋀ (j ∈ ListDef.map f l), g j = ⋀ (i ∈ l), g (f i).

Theorem rngl_and_eq_compat : ∀ g h b k,
  (∀ i, b ≤ i ≤ k → g i = h i)
  → ⋀ (i = b, k), g i = ⋀ (i = b, k), h i.

Theorem rngl_and_list_eq_compat : ∀ A g h (l : list A),
  (∀ i, i ∈ l → g i = h i)
  → ⋀ (i ∈ l), g i = ⋀ (i ∈ l), h i.