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