Library prosa.classic.util.ord_quantifier

Require Import prosa.classic.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.

(* Lemmas about the exists for Ordinals: ∃ x, P x. *)
Section OrdExists.

  Lemma exists_ord0:
    ∀ P,
      [∃ x in 'I_0, P x] = false.

  Lemma exists_recr:
    ∀ n P,
      [∃ x in 'I_n.+1, P x] =
      [∃ x in 'I_n, P (widen_ord (leqnSn n) x)] || P (ord_max).

End OrdExists.

(* Lemmas about the forall for Ordinals: ∃ x, P x. *)
Section OrdForall.

  Lemma forall_ord0:
    ∀ P,
      [∀ x in 'I_0, P x].

  Lemma forall_recr:
    ∀ n P,
      [∀ x in 'I_n.+1, P x] =
      [∀ x in 'I_n, P (widen_ord (leqnSn n) x)] && P (ord_max).

End OrdForall.

(* Tactics for simplifying exists and forall. *)
Ltac simpl_exists_ord := rewrite !exists_recr !exists_ord0 /=.
Ltac simpl_forall_ord := rewrite !forall_recr !forall_ord0 /=.