Propositional proof search
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]].