Lvc.Infra.SafeFirst

Require Import CSet Util NaturalRep PidgeonHole OrderedTypeMax.

Set Implicit Arguments.

Section SafeFirst.
  Variable N : Type.
  Context `{NaturalRepresentationSucc N}.

  Hypothesis Q : N Prop.
  Hypothesis Qpr : Proper (_eq ==> iff) Q.

  Inductive safe : N Prop :=
  | Isafe n : (¬ (Q n) safe (succ n)) safe n.

  Lemma safe_eq x y
    : safe x x === y safe y.
  Proof.
    unfold Proper, respectful; intros.
    general induction H2; eauto.
    econstructor; intros. eapply H3; eauto.
    rewrite H4. eauto. rewrite H4; eauto.
  Qed.

  Global Instance safe_proper
    : Proper (_eq ==> iff) safe.
  Proof.
    unfold Proper, respectful; split; eauto using safe_eq.
  Qed.

  Lemma safe_antitone' (m n:nat)
  : safe (ofNat n)
     m < n
     safe (ofNat m).
  Proof.
    intros.
    general induction H3; eauto using safe.
    - rewrite <- succ_ofNat in H2.
      econstructor; eauto.
    - rewrite <- succ_ofNat in H2.
      assert (safe (ofNat m0)) by (econstructor; eauto).
      eapply IHle in H4; eauto.
  Qed.

  Lemma safe_antitone m n
    : safe n
       _lt m n
       safe m.
  Proof.
    intros. rewrite <- ofNat_asNat.
    rewrite <- ofNat_asNat in H2.
    eapply order_respecting' in H3.
    eapply safe_antitone'; eauto.
  Qed.

  Lemma exists_is_safe
  : ( x, Q x) n, safe n.
  Proof.
    intros. destruct H2; eexists; econstructor; intros.
    exfalso; eauto.
  Qed.

  Lemma safe_upward n
  : safe n ¬ Q n safe (succ n).
  Proof.
    intros. inv H2. eauto.
  Defined.

  Hypothesis comp : n, Computable (Q n).
  Fixpoint safe_first n (s:safe n) : N.
  refine (if [ Q n ] then n else safe_first (succ n) _).
  destruct s; eauto.
  Defined.

  Hypothesis P : N Prop.
  Hypothesis I : N Prop.
  Hypothesis PQ : n, P n Q n.
  Hypothesis Step : n, I n ¬ Q n I (succ n).
  Hypothesis Final : n , I n Q n P n.

  Fixpoint safe_first_spec n s
    : I n P (@safe_first n s).
  Proof.
    unfold safe_first.
    destruct s.
    - simpl. destruct (decision_procedure (Q n)); eauto.
  Qed.

End SafeFirst.

Fixpoint safe_first_ext N `{NaturalRepresentationSucc N} P Q n
      (PC: n, Computable (P n))
      (QC: n, Computable (Q n))
      (PS:safe P n)
      (QS:safe Q n)
      (EXT:( x, P x Q x)) {struct QS}
: safe_first PC PS = safe_first QC QS.
Proof.
  destruct PS. destruct QS. simpl. repeat cases. reflexivity.
  - exfalso. eapply n0. rewrite <- EXT. eauto.
  - exfalso. eapply n0. rewrite EXT. eauto.
  - eapply safe_first_ext. eauto.
Qed.

Lemma safe_impl N `{NaturalRepresentationSucc N} (P Q: N Prop) n
: safe P n ( x, P x Q x) safe Q n.
Proof.
  intros. general induction H2; eauto 20 using @safe.
Qed.