Require Export build_proof rule_sets.

Section Build_prop_proof.

  Variable V : Type.
  Variable L : modal_operators.

  Variable v_eq : eq_type V.

  Definition rule_oracle_G_property(s : sequent V L)
                                   (r : sequent_rule V L) : Prop :=
    G_set V L r ∧ r.(conclusion) = s.

  Definition is_negated_prop(v : V)(l : lambda_formula V L) : bool :=
    match l with
      | lf_neg (lf_prop vo) ⇒ if v_eq v vo then true else false
      | _ ⇒ false
    end.

  Fixpoint find_trivial(l orig : sequent V L)(count : nat)
                                                   : option (nat × nat × V) :=
    match l with
      | [] ⇒ None
      | (lf_prop v) :: r ⇒
          match list_search orig 0 (is_negated_prop v) with
            | None ⇒ find_trivial r orig (1 + count)
            | Some nvo ⇒ Some(count, nvo, v)
          end
      | _ :: r ⇒ find_trivial r orig (1 + count)
    end.

  Lemma find_trivial_some_ind :
    ∀(l1 l2 : sequent V L)(v : V)(vo nvo : nat),
      find_trivial l2 (l1 ++ l2) (length l1) = Some(vo, nvo, v) →
        simple_tautology_witness (l1 ++ l2) vo nvo v.

  Lemma find_trivial_some :
    ∀(l : sequent V L)(v : V)(vo nvo : nat),
      find_trivial l l 0 = Some(vo, nvo, v) →
        simple_tautology l.

  Lemma find_trivial_none_ind :
    ∀(s1 s2 : sequent V L)(v : V)(vo nvo : nat),
      vo ≥ length s1 →
      find_trivial s2 (s1 ++ s2) (length s1) = None →
        not (simple_tautology_witness (s1 ++ s2) vo nvo v).

  Lemma find_trivial_none :
    ∀(s : sequent V L),
      find_trivial s s 0 = None →
        not (simple_tautology s).

  Definition build_ax_rule(s : sequent V L) : sequent_rule V L :=
    {| assumptions := [];
       conclusion := s
    |}.

  Lemma well_founded_ax_rule : ∀(s : sequent V L),
    well_founded_rule V L (build_ax_rule s) sequent_measure.

  Lemma ax_oracle_tcc :
    ∀(s : sequent V L)(v : V)(vo nvo : nat),
      find_trivial s s 0 = Some(vo, nvo, v) →
        rule_oracle_G_property s (build_ax_rule s).

  Definition ax_oracle(s : sequent V L) :
                            (rule_oracle_result V L (G_set V L) s) :=
    match find_trivial s s 0 as ft
    return find_trivial s s 0 = ft →
                            (rule_oracle_result V L (G_set V L) s)
    with
      | None ⇒ fun _ ⇒ None
      | Some(vo, nvo, v) ⇒ fun(H : find_trivial s s 0 = Some(vo, nvo,v)) ⇒
        Some(dep_conj (sequent_rule V L)
                      (fun(r : sequent_rule V L) ⇒ rule_oracle_G_property s r)
               (build_ax_rule s)
               (ax_oracle_tcc s v vo nvo H))
    end (eq_refl (find_trivial s s 0)).

  Lemma ax_oracle_some :
    ∀(s : sequent V L)
          (d : r # sequent_rule V L /#\ (rule_oracle_G_property s r)),
      ax_oracle s = Some d →
        ∃(p : rule_oracle_G_property s (build_ax_rule s)),
            d = dep_conj (sequent_rule V L) (rule_oracle_G_property s)
                  (build_ax_rule s) p.

  Definition find_and(l : sequent V L)
                : option((lambda_formula V L) × (lambda_formula V L) × nat) :=
    let ls := list_search l 0 is_and in
    match ls as ls0
             return ls = ls0 →
                     option((lambda_formula V L) × (lambda_formula V L) × nat)
    with
      | None ⇒ fun _ ⇒ None
      | Some ao ⇒ fun(H : ls = Some ao) ⇒
          let and_f := nth l ao (list_search_some_less l is_and ao H) in
          let (conj_1, conj_2) := get_and_forms and_f
                (list_search_some_test l is_and ao H)
          in
            Some(conj_1, conj_2, ao)
    end (eq_refl ls).

  Lemma find_and_some :
    ∀(l : sequent V L)(f1 f2 : lambda_formula V L)(ao : nat),
      find_and l = Some(f1, f2, ao) →
        ao_less # ao < length l /#\
          nth l ao ao_less = lf_and f1 f2.

  Lemma find_and_none :
    ∀(s : sequent V L)(f1 f2 : lambda_formula V L)(ao : nat)
          (ao_less : ao < length s),
      find_and s = None →
        nth s ao ao_less ≠ lf_and f1 f2.

  Definition build_and_rule(s : sequent V L)(n : nat)
                           (f1 f2 : lambda_formula V L) : sequent_rule V L :=
    {| assumptions := [(firstn n s) ++ f1 :: (skipn (1 + n) s);
                       (firstn n s) ++ f2 :: (skipn (1 + n) s)];
       conclusion := s
    |}.

  Lemma well_founded_and_rule :
    ∀(s : sequent V L)(f1 f2 : lambda_formula V L)(ao : nat)
          (ao_less : ao < length s),
      nth s ao ao_less = lf_and f1 f2 →
        well_founded_rule V L (build_and_rule s ao f1 f2) sequent_measure.

  Lemma and_oracle_tcc :
    ∀(s : sequent V L)(f1 f2 : lambda_formula V L)(ao : nat),
      find_and s = Some(f1, f2, ao) →
        rule_oracle_G_property s (build_and_rule s ao f1 f2).

  Definition and_oracle(s : sequent V L) :
                            rule_oracle_result V L (G_set V L) s :=
    match find_and s as fa
    return find_and s = fa → rule_oracle_result V L (G_set V L) s
    with
      | None ⇒ fun _ ⇒ None
      | Some(f1, f2, ao) ⇒ fun(H : find_and s = Some(f1, f2, ao)) ⇒
        Some(dep_conj (sequent_rule V L)
                      (fun(r : sequent_rule V L) ⇒ rule_oracle_G_property s r)
               (build_and_rule s ao f1 f2)
               (and_oracle_tcc s f1 f2 ao H))
    end (eq_refl (find_and s)).

  Lemma and_oracle_some :
    ∀(s : sequent V L)
          (d : r # sequent_rule V L /#\ (rule_oracle_G_property s r)),
      and_oracle s = Some d →
        ∃(f1 f2 : lambda_formula V L)(ao : nat)
              (p : rule_oracle_G_property s (build_and_rule s ao f1 f2)),
          d = dep_conj (sequent_rule V L) (rule_oracle_G_property s)
                  (build_and_rule s ao f1 f2) p
          ∧ ao_less # ao < length s /#\ nth s ao ao_less = lf_and f1 f2.

  Definition is_neg_and(f : lambda_formula V L) : bool :=
    match f with
      | lf_neg (lf_and _ _) ⇒ true
      | _ ⇒ false
    end.

  Lemma find_neg_and_tcc_is_neg :
    ∀(l : sequent V L)(nao : nat)
          (ls_res : list_search l 0 is_neg_and = Some nao),
      let neg_f := nth l nao (list_search_some_less l is_neg_and nao ls_res)
      in
        is_neg neg_f = true.

  Lemma find_neg_and_tcc_is_and :
    ∀(l : sequent V L)(nao : nat)
          (ls_res : list_search l 0 is_neg_and = Some nao),
      let neg_f := nth l nao (list_search_some_less l is_neg_and nao ls_res) in
      let and_f := get_neg_form neg_f (find_neg_and_tcc_is_neg l nao ls_res)
      in
        is_and and_f = true.

  Definition find_neg_and(l : sequent V L)
                : option((lambda_formula V L) × (lambda_formula V L) × nat) :=
    let ls := list_search l 0 is_neg_and in
    match ls as ls0
             return ls = ls0 →
                    option((lambda_formula V L) × (lambda_formula V L) × nat)
    with
      | None ⇒ fun _ ⇒ None
      | Some nao ⇒ fun(H : ls = Some nao) ⇒
          let neg_f := nth l nao (list_search_some_less l is_neg_and nao H) in
          let and_f := get_neg_form neg_f (find_neg_and_tcc_is_neg l nao H) in
          let (conj_1, conj_2) := get_and_forms and_f
                 (find_neg_and_tcc_is_and l nao H)
          in
             Some(conj_1, conj_2, nao)
    end (eq_refl ls).

  Lemma find_neg_and_some :
    ∀(l : sequent V L)(f1 f2 : lambda_formula V L)(nao : nat),
      find_neg_and l = Some(f1, f2, nao) →
        nao_less # nao < length l /#\
          nth l nao nao_less = lf_neg (lf_and f1 f2).

  Lemma find_neg_and_none :
    ∀(s : sequent V L)(f1 f2 : lambda_formula V L)(nao : nat)
          (nao_less : nao < length s),
      find_neg_and s = None →
        nth s nao nao_less ≠ lf_neg (lf_and f1 f2).

  Definition build_neg_and_rule(s : sequent V L)(n : nat)
                           (f1 f2 : lambda_formula V L) : sequent_rule V L :=
    {| assumptions := [(firstn n s) ++
                       (lf_neg f1) :: (lf_neg f2) :: (skipn (1 + n) s)];
       conclusion := s
    |}.

  Lemma well_founded_neg_and_rule :
    ∀(s : sequent V L)(f1 f2 : lambda_formula V L)(nao : nat)
          (nao_less : nao < length s),
      nth s nao nao_less = lf_neg (lf_and f1 f2) →
        well_founded_rule V L
          (build_neg_and_rule s nao f1 f2) sequent_measure.

  Lemma neg_and_oracle_tcc :
    ∀(s : sequent V L)(f1 f2 : lambda_formula V L)(nao : nat),
      find_neg_and s = Some(f1, f2, nao) →
        rule_oracle_G_property s (build_neg_and_rule s nao f1 f2).

  Definition neg_and_oracle(s : sequent V L) :
                            rule_oracle_result V L (G_set V L) s :=
    match find_neg_and s as fna
    return find_neg_and s = fna → rule_oracle_result V L (G_set V L) s
    with
      | None ⇒ fun _ ⇒ None
      | Some(f1, f2, nao) ⇒ fun H ⇒
        Some(dep_conj (sequent_rule V L)
                      (fun(r : sequent_rule V L) ⇒ rule_oracle_G_property s r)
               (build_neg_and_rule s nao f1 f2)
               (neg_and_oracle_tcc s f1 f2 nao H))
    end (eq_refl (find_neg_and s)).

  Lemma neg_and_oracle_some :
    ∀(s : sequent V L)
          (d : r # sequent_rule V L /#\ (rule_oracle_G_property s r)),
      neg_and_oracle s = Some d →
        ∃(f1 f2 : lambda_formula V L)(nao : nat)
              (p : rule_oracle_G_property s (build_neg_and_rule s nao f1 f2)),
          d = dep_conj (sequent_rule V L) (rule_oracle_G_property s)
                  (build_neg_and_rule s nao f1 f2) p
          ∧ nao_less # nao < length s
             /#\ nth s nao nao_less = lf_neg (lf_and f1 f2).

  Definition is_neg_neg(f : lambda_formula V L) : bool :=
    match f with
      | lf_neg (lf_neg _) ⇒ true
      | _ ⇒ false
    end.

  Lemma find_neg_neg_tcc_neg_neg :
    ∀(l : sequent V L)(nno : nat)
          (H : list_search l 0 is_neg_neg = Some nno),
        let neg_neg_f := nth l nno (list_search_some_less l is_neg_neg nno H)
        in
          is_neg neg_neg_f = true.

  Lemma find_neg_neg_tcc_neg :
    ∀(l : sequent V L)(nno : nat)
          (H : list_search l 0 is_neg_neg = Some nno),
        let neg_neg_f := nth l nno (list_search_some_less l is_neg_neg nno H) in
        let neg_f := get_neg_form neg_neg_f (find_neg_neg_tcc_neg_neg l nno H)
        in
          is_neg neg_f = true.

  Definition find_neg_neg(l : sequent V L)
                                       : option((lambda_formula V L) × nat) :=
    let ls := list_search l 0 is_neg_neg in
    match ls as ls0 return ls = ls0 → option((lambda_formula V L) × nat)
    with
      | None ⇒ fun _ ⇒ None
      | Some nno ⇒ fun(H : ls = Some nno) ⇒
          let neg_neg_f :=
                    nth l nno (list_search_some_less l is_neg_neg nno H) in
          let neg_f := get_neg_form neg_neg_f
                            (find_neg_neg_tcc_neg_neg l nno H) in
          let f := get_neg_form neg_f (find_neg_neg_tcc_neg l nno H)
          in
            Some(f, nno)
    end (eq_refl ls).

  Lemma find_neg_neg_some :
    ∀(l : sequent V L)(f : lambda_formula V L)(nno : nat),
      find_neg_neg l = Some(f, nno) →
        nno_less # nno < length l /#\
          nth l nno nno_less = lf_neg (lf_neg f).

  Lemma find_neg_neg_none :
    ∀(s : sequent V L)(f : lambda_formula V L)(nno : nat)
          (nno_less : nno < length s),
      find_neg_neg s = None →
        nth s nno nno_less ≠ lf_neg (lf_neg f).

  Definition build_neg_neg_rule(s : sequent V L)(n : nat)
                               (f : lambda_formula V L) : sequent_rule V L :=
    {| assumptions := [(firstn n s) ++ f :: (skipn (1 + n) s)];
       conclusion := s
    |}.

  Lemma well_founded_neg_neg_rule :
    ∀(s : sequent V L)(f : lambda_formula V L)(nno : nat)
          (nno_less : nno < length s),
      nth s nno nno_less = lf_neg (lf_neg f) →
        well_founded_rule V L (build_neg_neg_rule s nno f) sequent_measure.

  Lemma neg_neg_oracle_tcc :
    ∀(s : sequent V L)(f : lambda_formula V L)(nno : nat),
      find_neg_neg s = Some(f, nno) →
        rule_oracle_G_property s (build_neg_neg_rule s nno f).

  Definition neg_neg_oracle(s : sequent V L) :
                            rule_oracle_result V L (G_set V L) s :=
    match find_neg_neg s as fnn
    return find_neg_neg s = fnn → rule_oracle_result V L (G_set V L) s
    with
      | None ⇒ fun _ ⇒ None
      | Some(f, nno) ⇒ fun H ⇒
        Some(dep_conj (sequent_rule V L)
                      (fun(r : sequent_rule V L) ⇒ rule_oracle_G_property s r)
               (build_neg_neg_rule s nno f)
               (neg_neg_oracle_tcc s f nno H))
    end (eq_refl (find_neg_neg s)).

  Lemma neg_neg_oracle_some :
    ∀(s : sequent V L)
          (d : r # sequent_rule V L /#\ (rule_oracle_G_property s r)),
      neg_neg_oracle s = Some d →
        ∃(f : lambda_formula V L)(nno : nat)
              (p : rule_oracle_G_property s (build_neg_neg_rule s nno f)),
          d = dep_conj (sequent_rule V L) (rule_oracle_G_property s)
                  (build_neg_neg_rule s nno f) p
          ∧ nno_less # nno < length s
             /#\ nth s nno nno_less = lf_neg (lf_neg f).

  Definition prop_G_oracle : rule_oracle_type V L (G_set V L) :=
    fun(s : sequent V L) ⇒
      match ax_oracle s with
        | Some r ⇒ Some r
        | None ⇒
          match and_oracle s with
            | Some r ⇒ Some r
            | None ⇒
              match neg_and_oracle s with
                | Some r ⇒ Some r
                | None ⇒ neg_neg_oracle s
              end
          end
      end.

  Lemma well_founded_G_oracle :
    well_founded_rule_oracle prop_G_oracle sequent_measure.

  Lemma prop_G_oracle_None : ∀(s : sequent V L),
    prop_G_oracle s = None →
      find_trivial s s 0 = None ∧
      find_and s = None ∧
      find_neg_and s = None ∧
      find_neg_neg s = None.


  Lemma prop_G_oracle_None_simple : ∀(s : sequent V L),
    propositional_sequent s →
    prop_G_oracle s = None →
      prop_sequent s.

  Lemma prop_G_oracle_None_tautology : ∀(s : sequent V L),
    prop_G_oracle s = None →
      not (simple_tautology s).

  Lemma rank_G_n_inductive : ∀(n : nat),
    rule_inductive (G_n_set V L n) (rank_sequent n).

End Build_prop_proof.

Implicit Arguments find_trivial [V L].
Implicit Arguments find_trivial_none [V L].
Implicit Arguments prop_G_oracle [[V] [L]].