cody_iter_ind.v

(* https://twitter.com/codydroux/status/1570158204243288066 *)

Section Iter_to_ind.

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

  (* F is a monad *)
  Variable fmap : forall (a b : Prop), (a -> b) -> F a -> F b.
  Variable pure : forall (a : Prop),   a -> F a.
  Variable join : forall a,            F (F a) -> F a.

  Fixpoint iter_prop (n : nat) : Prop :=
    match n with
    | 0 => B
    | S m => F (iter_prop m)
    end.

  Definition ind_prop : nat -> Prop :=
      fun n =>
        forall P : nat -> Prop,
          (B -> P 0) ->
          (forall m, F (P m) -> P (S m)) ->
          P n.

  Lemma ind_to_iter : forall n, ind_prop n -> iter_prop n.
    Proof.
      induction n; unfold ind_prop; simpl; intros; apply (H (fun n => iter_prop n)); auto.
    Qed.

  Lemma iter_to_ind : forall n, iter_prop n -> ind_prop n.
    Proof.
      intros.
      induction n.
      - intro. intros. apply H0. simpl in H. assumption.
      - intro. intros. simpl in H. apply H1.

        destruct n.
        + simpl in H. simpl in IHn. apply (fmap B); assumption.
        + pose (H1 n).

          apply IHn.
          apply join. apply H.
          intro.
          apply pure.
          apply H0. assumption.
          intros.
          apply pure.
          apply H1.
          apply join. apply H2.
    Qed.