Require Export formulas.

Section Build_proof.
  Variable V : Type.
  Variable L : modal_operators.

  Variable rules : sequent_rule V L → Prop.
  Variable hypotheses : sequent V L → Prop.

  Definition hypotheses_oracle_type : Type :=
    ∀(s : sequent V L), option (hypotheses s).

  Definition rule_oracle_result(s : sequent V L) : Type :=
    option (r # sequent_rule V L /#\ (rules r ∧ r.(conclusion) = s)).

  Definition rule_oracle_type : Type :=
    ∀(s : sequent V L), rule_oracle_result s.

  Fixpoint build_proof(i : nat)(ho : hypotheses_oracle_type)
                      (ro : rule_oracle_type)(s : sequent V L) :
                                 (proof rules hypotheses s) + (sequent V L) :=
    match i with
      | O ⇒ inr s
      | S i ⇒
        match ho s with
          | Some in_hyp ⇒
            inl (assume rules hypotheses s in_hyp)
          | None ⇒
            match ro s with
              | None ⇒ inr s
              | Some (dep_conj r (conj in_rules concl_prop)) ⇒
                match dep_list_proj_left r.(assumptions)
                      (dep_map_const_dep (build_proof i ho ro) r.(assumptions))
                with
                  | inr s ⇒ inr s
                  | inl subproofs ⇒
                      inl (eq_rect (conclusion r)
                             (fun(s : sequent V L) ⇒ proof rules hypotheses s)
                             (rule rules hypotheses r in_rules subproofs)
                             s
                             concl_prop)
                end
            end
        end
    end.

  Definition well_founded_rule(r : sequent_rule V L)
                                      (measure : sequent V L → nat) : Prop :=
    ∀(i : nat)(i_less : i < length (assumptions r)),
      measure (nth (assumptions r) i i_less) < measure (conclusion r).

  Definition well_founded_rule_oracle(ro : rule_oracle_type)
                                      (measure : sequent V L → nat) : Prop :=
    ∀(s : sequent V L),
      match ro s with
        | None ⇒ True
        | Some (dep_conj r _) ⇒ well_founded_rule r measure
      end.

  Lemma build_proof_right_result :
    ∀(i : nat)(ho : hypotheses_oracle_type)
          (ro : rule_oracle_type)(measure : sequent V L → nat)
          (s r : sequent V L),
      well_founded_rule_oracle ro measure →
      measure s < i →
      build_proof i ho ro s = inr r →
        ro r = None ∧ ho r = None.

  Definition rule_inductive(P : sequent V L → Prop) : Prop :=
    ∀(r : sequent_rule V L),
      rules r →
      P (conclusion r) →
      every_nth P (assumptions r).

  Lemma build_proof_right_property :
    ∀(i : nat)(ho : hypotheses_oracle_type)
          (ro : rule_oracle_type)(measure : sequent V L → nat)
          (P : sequent V L → Prop)
          (s r : sequent V L),
      well_founded_rule_oracle ro measure →
      measure s < i →
      rule_inductive P →
      P s →
      build_proof i ho ro s = inr r →
        P r.

  Fixpoint restrict_hypothesis(P : sequent V L → Prop)
           (ri : rule_inductive P)
           (s : sequent V L)(ps : P s)(p : proof rules hypotheses s)
                                : proof rules (intersection hypotheses P) s :=
    match p
      in proof _ _ s
      return P s → proof rules (intersection hypotheses P) s
    with
      | assume s hyp_s ⇒ fun(ps : P s) ⇒
        assume rules (intersection hypotheses P) s (conj hyp_s ps)
      | rule r r_rules subproofs ⇒
        fun(ps : P (conclusion r)) ⇒
          rule rules (intersection hypotheses P) r r_rules
            ((fix map_subproofs(sl : list (sequent V L))
                  (subproofs : dep_list (sequent V L)
                                        (proof rules hypotheses) sl)
                  (psl : every_nth P sl)
                       : dep_list (sequent V L)
                               (proof rules (intersection hypotheses P)) sl :=
              match subproofs
                in dep_list _ _ sl
                return
                  every_nth P sl →
                     dep_list (sequent V L)
                              (proof rules (intersection hypotheses P)) sl
              with
                | dep_nil ⇒ fun _ ⇒ dep_nil
                | dep_cons s sl p tl ⇒ fun(psl : every_nth P (s :: sl)) ⇒
                  dep_cons s sl
                    (restrict_hypothesis P ri s (every_nth_head _ _ _ psl) p)
                    (map_subproofs sl tl (every_nth_tail _ _ _ psl))
              end psl)
             (assumptions r) subproofs (ri r r_rules ps))
    end ps.

End Build_proof.

Implicit Arguments build_proof [V L rules hypotheses].
Implicit Arguments build_proof_right_result [V L rules hypotheses].
Implicit Arguments well_founded_rule_oracle [V L rules].
Implicit Arguments rule_inductive [V L].
Implicit Arguments build_proof_right_property [V L rules hypotheses].
Implicit Arguments restrict_hypothesis [V L rules hypotheses].