Require Export HFS.Extensionality.

Inductive tree: Type :=
| treeN : tree
| treeA : tree -> tree -> tree.

Implicit Types s t u : tree.

Notation "0" := treeN.
Notation "s '@' t" := (treeA s t) (at level 65, right associativity). (* x.y *)

Instance tree_eq_dec : eq_dec tree.
Proof.
  intros x y. unfold dec. decide equality.
Defined.

Section Evaluation.
  Variable X: Type.
  Variable eset: X.
  Variable adj: X -> X -> X.
  Variable sip: forall (p: X -> Type), p eset -> (forall x y, p x -> p y -> p (adj x y)) -> forall x, p x.
  Implicit Types x y: X.

  Fixpoint S' s: X :=
    match s with
      | 0 => eset
      | s@t => adj (S' s) (S' t)
    end.

  Lemma F' x :
    Sigma s, S' s = x.
  Proof.
    pattern x. revert x. apply sip.
    - now exists 0.
    - intros x1 x2 (y1&IHx1) (y2&IHx2).
      exists (y1 @ y2). simpl. congruence.
  Qed.

  Definition I' x := projT1 (F' x).

  Fact SI' x:
    S' (I' x) = x.
  Proof.
    unfold I'. now destruct (F' x).
  Qed.
End Evaluation.

Section HF_Evaluation.
  Variable X: HF.

  Definition S := S' eset (@adj X).
  Definition I := I' (@hf_ind X).

  Fact SI x :
    S (I x) = x.
  Proof.
    apply SI'.
  Qed.
End HF_Evaluation.

Section SIP.
  Variable X: Type.
  Variable eset: X.
  Variable adj: X -> X -> X.
  Variable S: tree -> X.
  Variable I: X -> tree.
  Variable SI: forall x, S (I x) = x.
  Variable S_emp: S 0 = eset.
  Variable S_adj: forall s t, S (s@t) = adj (S s) (S t).

  Fact SI2sip (p: X -> Type):
    p eset -> (forall x y, p x -> p y -> p (adj x y)) -> forall x, p x.
  Proof.
    intros base IH.
    assert (forall s, p (S s)).
    { intros s. induction s.
      - congruence.
      - rewrite S_adj. now apply IH. }
    intros x. now rewrite <- SI.
  Qed.
End SIP.

Section WIP.
  Variable X: eqType.
  Variable eset: X.
  Variable adj: X -> X -> X.
  Variable wip: forall (p: X -> Prop), p eset -> (forall x y , p x -> p y -> p (adj x y)) -> forall x, p x.
  Variable gamma: forall p: decPred tree, (exists x, p x) -> tree.
  Variable choice: forall (p: decPred tree) (A: exists x, p x), p (gamma A).

  Fact wip2sip (p: X -> Type):
    p eset -> (forall x y, p x -> p y -> p (adj x y)) -> forall x, p x.
  Proof.
    pose (S := S' eset adj).
    pose (q x := DecPred (fun s => S s = x)).

    assert (F: forall x, exists s, q x s).
    { intros x. pattern x. revert x. apply wip.
      - now exists 0.
      - intros a x (b&IHa) (y&IHx). exists (b@y). simpl. congruence. }

    assert (G: forall x, {s | q x s}).
    { intros x. exists (gamma (F x)). apply choice. }

    pose (I x := proj1_sig (G x)).

    assert (SI: forall x, S (I x) = x).
    { intros x. unfold I. now destruct (G x). }

    apply (SI2sip SI); auto.
  Qed.

End WIP.