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.
  Proof.
    intros P.
    apply negbTE; rewrite negb_exists; apply/forall_inP.
    intros x; destruct x as [x LT].
    by exfalso; rewrite ltn0 in LT.
  Qed.

  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).
  Proof.
    intros n P.
    apply/idP/idP.
    {
      move ⇒ /exists_inP EX; destruct EX as [x IN Px].
      destruct x as [x LT].
      remember LT as LT'; clear HeqLT'.
      rewrite ltnS leq_eqVlt in LT; move: LT ⇒ /orP [/eqP EQ | LT].
      {
        apply/orP; right.
        unfold ord_max; subst x.
        apply eq_trans with (y := P (Ordinal LT')); last by done.
        by f_equal; apply ord_inj.
      }
      {
        apply/orP; left.
        apply/exists_inP; ∃ (Ordinal LT); first by done.
        apply eq_trans with (y := P (Ordinal LT')); last by done.
        by f_equal; apply ord_inj.
      }
    }
    {
      intro OR; apply/exists_inP.
      move: OR ⇒ /orP [/exists_inP EX | MAX].
      {
        by destruct EX as [x IN Px]; ∃ (widen_ord (leqnSn n) x).
      }
      by ∃ ord_max.
    }
  Qed.

End OrdExists.

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

  Lemma forall_ord0:
    ∀ P,
      [∀ x in 'I_0, P x].
  Proof.
    intros P; apply/forall_inP.
    by intros x IN0; destruct x.
  Qed.

  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).
  Proof.
    intros n P.
    apply/idP/idP.
    {
      move ⇒ /forall_inP ALL.
      apply/andP; split; last by apply ALL.
      by apply/forall_inP; intros x IN; apply ALL.
    }
    {
      move ⇒ /andP [/forall_inP ALL MAX].
      apply/forall_inP; intros x IN.
      destruct x as [x LT].
      unfold ord_max in ×.
      remember LT as LT'; clear HeqLT'.
      rewrite ltnS leq_eqVlt in LT; move: LT ⇒ /orP [/eqP EQ | LT].
      {
        subst n.
        apply/eqP; rewrite -MAX; apply/eqP.
        by unfold ord_max; apply f_equal, ord_inj.
      }
      {
        feed (ALL (Ordinal LT)); first by done.
        apply/eqP; rewrite -ALL; apply/eqP.
        by apply f_equal, ord_inj.
      }
    }
  Qed.

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 /=.