iter_to_impred.v

Require Import Lia.

Section Iter_to_ind.

  Variable B : Prop.
  Variable F : Prop -> Prop.

  Hypothesis F_ext : forall P Q, (P <-> Q) -> (F P <-> F Q).
  
  Fixpoint iter_prop (n : nat) : Prop :=
    match n with
    | 0 => B
    | S m => F (iter_prop m)
    end.      
  

  Definition Psi W n := (W 0 <-> B) /\ (forall i, i < n -> W (S i) <-> F (W i)).

  Lemma exists_psi : forall n, exists W, Psi W n.
  Proof.
    induction n.
    - exists (fun _ => B).
      unfold Psi; intuition; lia.
    - destruct IHn as [W h].
      exists (fun k => (k < S n /\ W k) \/ (k = S n /\ F (W n))).
      unfold Psi.
      split.
      + unfold Psi in h.
        intuition; lia.
      + intros i lti.
        assert (i < n \/ i = n) by lia.
        destruct H.
        {
          assert ((S i < S n /\ W (S i) \/ S i = S n /\ F (W n))
                 <->
                   (W (S i))) by (intuition; lia).
          rewrite H0.
          assert (F (i < S n /\ W i \/ i = S n /\ F (W n))
                  <->
                    F (W i)) by (apply F_ext with (Q := W i); intuition; lia).
          rewrite H1.
          apply h; auto.
        }
        { subst; clear lti.
          assert (S n < S n /\ W (S n) \/ S n = S n /\ F (W n) <->
                    F (W n)) by (intuition; lia).
          rewrite H.
          assert (F (n < S n /\ W n \/ n = S n /\ F (W n)) <->
                    F (W n)) by (apply F_ext with (Q := W n); intuition; lia).
          rewrite H0.
          intuition.
        }
  Qed.

  Lemma forall_exists : forall n, (forall W, Psi W n -> W n) -> exists W, (Psi W n) /\ W n.
  Proof.
    intros n h.
    edestruct (exists_psi n).
    exists x; split; auto.
    apply h; auto.
  Qed.

  Lemma exists_forall : forall n, (exists W, (Psi W n) /\ W n) -> (forall W, Psi W n -> W n).
  Proof.
    destruct n; intros h; destruct h as [X h] ; unfold Psi in h.
    - unfold Psi.
      intros W h'.
      destruct h as [[h _] x0].
      destruct h' as [h' _].
      intuition.
    - intros W h'.
      apply h'; auto.
      assert (X n <-> W n).
      { unfold Psi in h'.
        destruct h as [[x0 xs] _].
        destruct h' as [wo ws].
        induction n.
        - intuition.
        - rewrite ws, xs; try lia.
          apply F_ext, IHn; auto. }
      erewrite F_ext; [ | symmetry; now eauto].
      destruct h as [[_ xs] xn].
      apply xs; auto.
  Qed.

  Theorem iter_impred : forall n, (exists W, Psi W n /\ W n) <-> iter_prop n.
  Proof.
    intros n.
    split.
    - intros h; assert (h' := exists_forall _ h).
      apply h'; unfold Psi; simpl; intuition.
    - intros h; exists iter_prop.
      unfold Psi; intuition.
  Qed.
  
  Lemma impred_base : (exists W, Psi W 0 /\ W 0) <-> B.
  Proof.
    split.
    - intros (W&(w0&ws)&wn); intuition.
    - intros b; exists (fun _ => B); unfold Psi; intros; intuition; lia.
  Qed.

  
  Lemma impred_succ : forall n, (exists W, Psi W (S n) /\ W (S n))
                                <-> F (exists W, Psi W n /\ W n).
  Proof.
    split; intros h.
    - destruct h as [W [w_ind wn]].
      apply F_ext with (Q := Psi W n /\ W n).
      + split; intros; [| exists W; auto].
        unfold Psi.
        unfold Psi in w_ind.
        split; [split; [now intuition|] |].
        { intros; apply w_ind; lia.}
        destruct H as [W' [h wn']].
        assert (forall k, k < (S n) -> W k <-> W' k).
        { induction k.
          - intros _; split; intros; try apply w_ind; try apply h; intuition.
          - intros.
            split; intros.
            { apply h; try lia.
              eapply F_ext; [symmetry; apply IHk; lia |].
              apply w_ind; try lia; auto.}
            apply w_ind; try lia.
            eapply F_ext; [apply IHk; lia|].
            apply h; try lia; auto. }
        rewrite H; [| lia]; auto.
      + destruct w_ind as [h1 h2].
        apply F_ext with (Q := W n).
        { split; try now intuition.
          intro h; split; auto.
          unfold Psi.
          split; auto. }
        apply h2; auto.
    - apply forall_exists.
      unfold Psi.
      intros W [w0 ws].
      apply ws; auto.
      revert h.
      rewrite F_ext with (Q := W n); auto.
      split.
      + intros [W' [[h0 hs] hn]].
        revert hn.
        assert (forall k, k < S n -> W' k <-> W k).
        {
          induction k; intuition.
          - apply ws; try lia.
            rewrite F_ext with (Q := W' k); [| rewrite IHk; intuition; lia].
            apply hs; try lia.
            auto.
          - apply hs; try lia.
            rewrite F_ext with (Q := W k); [| rewrite IHk; intuition; lia].
            apply ws; try lia.
            auto.
        }
        {
          apply H; lia.
        }
      + intros h; exists W; unfold Psi.
        split; [split |]; auto.
  Qed.