Logic, basic definitions
Formulas, Sequents, Proofs
Require Export dep_lists reorder.
Record modal_operators : Type := {
operator : Type;
arity : operator → nat
}.
Section Formulas.
Variable V : Type.
Variable L : modal_operators.
Inductive lambda_formula : Type :=
| lf_prop : V → lambda_formula
| lf_neg : lambda_formula → lambda_formula
| lf_and : lambda_formula → lambda_formula → lambda_formula
| lf_modal : ∀(op : operator L),
counted_list lambda_formula (arity L op) → lambda_formula.
The recursion and induction schemes from Coq are not useful,
because of the use of counted_list. I don't like the usual
workaround, namely unrolling counted_list and lambda_formula
into two mutually recursive types, because it is less modular
and, generally, makes a mess. Therefore I have to define my own
recursion and induction schemes.
Fixpoint lambda_formula_rect(T : lambda_formula → Type)
(prop_fun : ∀(v : V), T (lf_prop v))
(neg_fun : ∀(f : lambda_formula), T f → T (lf_neg f))
(and_fun : ∀(f1 f2 : lambda_formula),
T f1 → T f2 → T (lf_and f1 f2))
(modal_fun : ∀(op : operator L)
(args : counted_list lambda_formula (arity L op)),
(dep_list lambda_formula T (list_of_counted_list args))
→ T (lf_modal op args))
(f : lambda_formula) : T f :=
let rec_fn : ∀(f : lambda_formula), T f :=
lambda_formula_rect T prop_fun neg_fun and_fun modal_fun
in
match f with
| lf_prop v ⇒ prop_fun v
| lf_neg f ⇒ neg_fun f (rec_fn f)
| lf_and f1 f2 ⇒
and_fun f1 f2 (rec_fn f1) (rec_fn f2)
| lf_modal op args ⇒
modal_fun op args
((fix map_args(len : nat)(args : counted_list lambda_formula len)
: dep_list lambda_formula T (list_of_counted_list args) :=
match args with
| counted_nil ⇒ dep_nil
| counted_cons n f rargs ⇒
dep_cons f (list_of_counted_list rargs)
(rec_fn f) (map_args n rargs)
end
) (arity L op) args)
end.
(prop_fun : ∀(v : V), T (lf_prop v))
(neg_fun : ∀(f : lambda_formula), T f → T (lf_neg f))
(and_fun : ∀(f1 f2 : lambda_formula),
T f1 → T f2 → T (lf_and f1 f2))
(modal_fun : ∀(op : operator L)
(args : counted_list lambda_formula (arity L op)),
(dep_list lambda_formula T (list_of_counted_list args))
→ T (lf_modal op args))
(f : lambda_formula) : T f :=
let rec_fn : ∀(f : lambda_formula), T f :=
lambda_formula_rect T prop_fun neg_fun and_fun modal_fun
in
match f with
| lf_prop v ⇒ prop_fun v
| lf_neg f ⇒ neg_fun f (rec_fn f)
| lf_and f1 f2 ⇒
and_fun f1 f2 (rec_fn f1) (rec_fn f2)
| lf_modal op args ⇒
modal_fun op args
((fix map_args(len : nat)(args : counted_list lambda_formula len)
: dep_list lambda_formula T (list_of_counted_list args) :=
match args with
| counted_nil ⇒ dep_nil
| counted_cons n f rargs ⇒
dep_cons f (list_of_counted_list rargs)
(rec_fn f) (map_args n rargs)
end
) (arity L op) args)
end.
Induction over lambda_formula's
Lemma lambda_formula_ind :
∀(P : lambda_formula → Prop),
(∀(v : V), P (lf_prop v)) →
(∀(f : lambda_formula), P f → P (lf_neg f)) →
(∀(f1 f2 : lambda_formula), P f1 → P f2 → P (lf_and f1 f2)) →
(∀(op : operator L)
(args : counted_list lambda_formula (arity L op)),
every_nth P (list_of_counted_list args) → P (lf_modal op args))
→
∀(f : lambda_formula), P f.
∀(P : lambda_formula → Prop),
(∀(v : V), P (lf_prop v)) →
(∀(f : lambda_formula), P f → P (lf_neg f)) →
(∀(f1 f2 : lambda_formula), P f1 → P f2 → P (lf_and f1 f2)) →
(∀(op : operator L)
(args : counted_list lambda_formula (arity L op)),
every_nth P (list_of_counted_list args) → P (lf_modal op args))
→
∀(f : lambda_formula), P f.
Define non-dependent recursion over lambda_formula's.
As lambda_formula_rect, this contains a nested, inlined,
mutually recursive map over counted_list, because, otherwise,
Coq won't accept the definition. This is fixed with the next
lemma, which references counted_map.
Instead of a separate definition, one could probably derive this
from lambda_formula_rect, but for this one needs to transform
a dep_list into a counted_list.
Fixpoint lambda_formula_rec(A : Type)
(prop_fun : V → A)
(neg_fun : A → A)
(and_fun : A → A → A)
(modal_fun : ∀(op : operator L),
counted_list A (arity L op) → A)
(f : lambda_formula) : A :=
let rec_fn : ∀(f : lambda_formula), A :=
lambda_formula_rec A prop_fun neg_fun and_fun modal_fun
in
match f with
| lf_prop v ⇒ prop_fun v
| lf_neg f ⇒ neg_fun (rec_fn f)
| lf_and f1 f2 ⇒
and_fun (rec_fn f1) (rec_fn f2)
| lf_modal op args ⇒
modal_fun op
((fix map_args(len : nat)(args : counted_list lambda_formula len)
: counted_list A len :=
match args with
| counted_nil ⇒ counted_nil
| counted_cons n f rargs ⇒
counted_cons (rec_fn f) (map_args n rargs)
end
) (arity L op) args)
end.
Lemma lambda_formula_rec_char :
∀(A : Type)(pf : V → A)(nf : A → A)(af : A → A → A)
(mf : ∀(op : operator L), counted_list A (arity L op) → A)
(f : lambda_formula),
lambda_formula_rec A pf nf af mf f =
match f with
| lf_prop v ⇒ pf v
| lf_neg f ⇒ nf (lambda_formula_rec A pf nf af mf f)
| lf_and f1 f2 ⇒
af (lambda_formula_rec A pf nf af mf f1)
(lambda_formula_rec A pf nf af mf f2)
| lf_modal op args ⇒
mf op (counted_map (lambda_formula_rec A pf nf af mf) args)
end.
(prop_fun : V → A)
(neg_fun : A → A)
(and_fun : A → A → A)
(modal_fun : ∀(op : operator L),
counted_list A (arity L op) → A)
(f : lambda_formula) : A :=
let rec_fn : ∀(f : lambda_formula), A :=
lambda_formula_rec A prop_fun neg_fun and_fun modal_fun
in
match f with
| lf_prop v ⇒ prop_fun v
| lf_neg f ⇒ neg_fun (rec_fn f)
| lf_and f1 f2 ⇒
and_fun (rec_fn f1) (rec_fn f2)
| lf_modal op args ⇒
modal_fun op
((fix map_args(len : nat)(args : counted_list lambda_formula len)
: counted_list A len :=
match args with
| counted_nil ⇒ counted_nil
| counted_cons n f rargs ⇒
counted_cons (rec_fn f) (map_args n rargs)
end
) (arity L op) args)
end.
Lemma lambda_formula_rec_char :
∀(A : Type)(pf : V → A)(nf : A → A)(af : A → A → A)
(mf : ∀(op : operator L), counted_list A (arity L op) → A)
(f : lambda_formula),
lambda_formula_rec A pf nf af mf f =
match f with
| lf_prop v ⇒ pf v
| lf_neg f ⇒ nf (lambda_formula_rec A pf nf af mf f)
| lf_and f1 f2 ⇒
af (lambda_formula_rec A pf nf af mf f1)
(lambda_formula_rec A pf nf af mf f2)
| lf_modal op args ⇒
mf op (counted_map (lambda_formula_rec A pf nf af mf) args)
end.
Utility functions for formulas
Definition is_prop (l : lambda_formula) : bool :=
match l with
| lf_prop _ ⇒ true
| _ ⇒ false
end.
Definition is_neg (l : lambda_formula) : bool :=
match l with
| lf_neg _ ⇒ true
| _ ⇒ false
end.
Definition is_and (l : lambda_formula) : bool :=
match l with
| lf_and _ _ ⇒ true
| _ ⇒ false
end.
Definition is_modal (l : lambda_formula) : bool :=
match l with
| lf_modal _ _ ⇒ true
| _ ⇒ false
end.
Accessor functions. These accessor functions work with the decidable
recognizers from above.
Definition get_prop_var(f : lambda_formula)(is_prop_f : is_prop f = true) : V.
Definition get_neg_form(f : lambda_formula)(is_neg_f : is_neg f = true)
: lambda_formula.
Definition get_and_forms(f : lambda_formula)(is_and_f : is_and f = true)
: lambda_formula × lambda_formula.
Definition get_modal_args(f : lambda_formula)(is_modal_f : is_modal f = true)
: (operator L) × (list lambda_formula).
Definition get_neg_form(f : lambda_formula)(is_neg_f : is_neg f = true)
: lambda_formula.
Definition get_and_forms(f : lambda_formula)(is_and_f : is_and f = true)
: lambda_formula × lambda_formula.
Definition get_modal_args(f : lambda_formula)(is_modal_f : is_modal f = true)
: (operator L) × (list lambda_formula).
standard propositional connectives, page 5
Definition lambda_or(A B : lambda_formula) : lambda_formula :=
lf_neg(lf_and (lf_neg A) (lf_neg B)).
Definition lambda_false(nonempty_v : V) : lambda_formula :=
lf_and (lf_prop nonempty_v) (lf_neg (lf_prop nonempty_v)).
lf_neg(lf_and (lf_neg A) (lf_neg B)).
Definition lambda_false(nonempty_v : V) : lambda_formula :=
lf_and (lf_prop nonempty_v) (lf_neg (lf_prop nonempty_v)).
Lemma lf_modal_inversion_op :
∀(op1 op2 : operator L)
(args1 : counted_list lambda_formula (arity L op1))
(args2 : counted_list lambda_formula (arity L op2)),
lf_modal op1 args1 = lf_modal op2 args2 →
op1 = op2.
Lemma lf_modal_inversion_args :
∀(op : operator L)
(args1 args2 : counted_list lambda_formula (arity L op)),
lf_modal op args1 = lf_modal op args2 →
args1 = args2.
Definition sequent : Type := list lambda_formula.
Definition empty_sequent_set : set sequent := empty_set (sequent).
Record sequent_rule : Type := {
assumptions: list sequent;
conclusion: sequent
}.
Definition prop_form(f : lambda_formula) : Prop :=
match f with
| lf_prop _ ⇒ True
| _ ⇒ False
end.
Definition prop_form_acc(f : lambda_formula)(prop_f : prop_form f) : V.
Lemma prop_form_acc_tcc_irr :
∀(f : lambda_formula)(prop_f_1 prop_f_2 : prop_form f),
prop_form_acc f prop_f_1 = prop_form_acc f prop_f_2.
Definition neg_form(f : lambda_formula) : Prop :=
match f with
| lf_neg _ ⇒ True
| _ ⇒ False
end.
Lemma neg_form_is_neg :
∀(f : lambda_formula), is_neg f = true ↔ neg_form f.
Definition neg_form_maybe(F : set lambda_formula)(f : lambda_formula)
: Prop :=
match f with
| lf_neg f ⇒ F f
| _ ⇒ F f
end.
Definition prop_sequent(s : sequent) : Prop :=
every_nth (neg_form_maybe prop_form) s.
Lemma prop_sequent_cons :
∀(s : sequent)(f : lambda_formula),
neg_form_maybe prop_form f →
prop_sequent s →
prop_sequent (f :: s).
Lemma prop_sequent_tail :
∀(s : sequent)(f : lambda_formula),
prop_sequent (f :: s) →
prop_sequent s.
Lemma prop_sequent_head :
∀(s : sequent)(f : lambda_formula),
prop_sequent (f :: s) →
neg_form_maybe prop_form f.
Lemma prop_sequent_list_reorder :
∀(s1 s2 : sequent),
list_reorder s1 s2 →
prop_sequent s1 →
prop_sequent s2.
Fixpoint neg_and_over(fs : set lambda_formula)(f : lambda_formula) : Prop :=
match f with
| lf_neg f ⇒ neg_and_over fs f
| lf_and f1 f2 ⇒ neg_and_over fs f1 ∧ neg_and_over fs f2
| _ ⇒ fs f
end.
Definition formula_measure(f : lambda_formula) : nat :=
lambda_formula_rec nat
(fun _ ⇒ 0)
(fun m ⇒ 1 + m)
(fun m1 m2 ⇒ 2 + m1 + m2)
(fun _ cl ⇒ 1 + nat_list_sum (list_of_counted_list cl))
f.
Lemma formula_measure_char :
∀(f : lambda_formula),
formula_measure f =
match f with
| lf_prop _ ⇒ 0
| lf_neg f ⇒ 1 + (formula_measure f)
| lf_and f1 f2 ⇒ 2 + (formula_measure f1) + (formula_measure f2)
| lf_modal _ args ⇒
1 + nat_list_sum (map formula_measure
(list_of_counted_list args))
end.
Definition sequent_measure(s : sequent) : nat :=
nat_list_sum (map formula_measure s).
Lemma sequent_measure_cons :
∀(s : sequent)(f : lambda_formula),
sequent_measure (f :: s) =
(formula_measure f) + (sequent_measure s).
Lemma sequent_measure_append :
∀(sl sr : sequent),
sequent_measure (sl ++ sr) =
sequent_measure sl + sequent_measure sr.
Lemma sequent_measure_context_lt :
∀(os ns: sequent)(n : nat)(n_less : n < length os),
sequent_measure ns
< formula_measure (nth os n n_less)
→
sequent_measure (firstn n os ++ ns ++ skipn (1 + n) os)
< sequent_measure os.
Lemma sequent_measure_simple_context_lt :
∀(s : sequent)(n : nat)(n_less : n < length s)(f : lambda_formula),
formula_measure f
< formula_measure (nth s n n_less)
→
sequent_measure (firstn n s ++ f :: skipn (1 + n) s)
< sequent_measure s.
Proofs
- The multiset coq library uses functions A -> nat, therefore one cannot use intentional equality on those multisets
- In a simple list representation I would have to identify lists up to reorderings.
- This reordering could be built into the rules, complicating all rules.
- Assuming a total order on V and L I could implement a total order on the formulas and use ordered lists for sequents only. Then intentional equality would be sequent equality. However, reordering calls would be needed in the rules.
- I therefore push the whole problem now to the conceptual level: I use simple unordered lists and standard equality on them in proofs. Rules and hypothesis must be order invariant.
Inductive proof(rules : set sequent_rule)(hypotheses : set sequent)
: sequent → Type :=
| assume : ∀(gamma : sequent),
hypotheses gamma → proof rules hypotheses gamma
| rule : ∀(r : sequent_rule), rules r →
dep_list sequent (proof rules hypotheses) (assumptions r) →
proof rules hypotheses (conclusion r).
Fixpoint proof_rect(rules : set sequent_rule)
(hypotheses : set sequent)
(T : sequent → Type)
(assume_fn : ∀(gamma : sequent), hypotheses gamma → T gamma)
(rule_fn :
∀(r : sequent_rule)(in_rules : rules r),
(dep_list sequent T (assumptions r)) →
T (conclusion r))
(s : sequent)(p : proof rules hypotheses s)
: T s :=
match p with
| assume g g_hyp ⇒ assume_fn g g_hyp
| rule r r_rules subproofs ⇒
rule_fn r r_rules
((fix map_subproofs(sl : list sequent)
(subproofs : dep_list sequent (proof rules hypotheses) sl)
: dep_list sequent T sl :=
match subproofs with
| dep_nil ⇒ dep_nil
| dep_cons s sl p tl ⇒
dep_cons s sl
(proof_rect rules hypotheses T assume_fn rule_fn s p)
(map_subproofs sl tl)
end)
(assumptions r) subproofs)
end.
Lemma proof_rect_rule :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(T : sequent → Type)
(assume_fn : ∀(g : sequent), hypotheses g → T g)
(rule_fn : ∀(r : sequent_rule)(in_rules : rules r),
(dep_list sequent T (assumptions r)) → T (conclusion r))
(r : sequent_rule)(r_rules : rules r)
(subproofs : dep_list sequent (proof rules hypotheses)
(assumptions r)),
proof_rect rules hypotheses T assume_fn rule_fn (conclusion r)
(rule rules hypotheses r r_rules subproofs)
= rule_fn r r_rules
(dep_map_dep_dep
(proof_rect rules hypotheses T assume_fn rule_fn)
(assumptions r) subproofs).
Definition proof_depth{rules : sequent_rule → Prop}
{hypotheses : sequent → Prop}
{s : sequent}
(p : proof rules hypotheses s) : nat :=
proof_rect rules hypotheses (fun _ ⇒ nat)
(fun _ _ ⇒ 1)
(fun r _ l ⇒ S (nat_list_max (list_of_dep_list (assumptions r) l)))
s p.
Lemma proof_depth_assume :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(s : sequent)(in_hyp : hypotheses s),
proof_depth (assume rules hypotheses s in_hyp) = 1.
Lemma proof_depth_rule :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(r : sequent_rule)(r_rules : rules r)
(subproofs : dep_list sequent (proof rules hypotheses)
(assumptions r)),
proof_depth (rule rules hypotheses r r_rules subproofs) =
1 + (nat_list_max (dep_map_dep_const
(@proof_depth rules hypotheses)
(assumptions r)
subproofs)).
Lemma proof_depth_rule_le :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(r : sequent_rule)(r_rules : rules r)(n : nat)
(subproofs : dep_list sequent (proof rules hypotheses)
(assumptions r)),
every_dep_nth
(fun(s : sequent)(p : proof rules hypotheses s) ⇒ proof_depth p ≤ n)
(assumptions r)
subproofs
→ proof_depth (rule rules hypotheses r r_rules subproofs) ≤ S n.
Lemma proof_depth_rule_le_inv :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(r : sequent_rule)(r_rules : rules r)(n : nat)
(subproofs : dep_list sequent (proof rules hypotheses)
(assumptions r)),
proof_depth (rule rules hypotheses r r_rules subproofs) ≤ S n →
every_dep_nth
(fun(s : sequent)(p : proof rules hypotheses s) ⇒
proof_depth p ≤ n)
(assumptions r)
subproofs.
Lemma proof_depth_0 :
∀(X : Type)
(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
(s : sequent)(p : proof rules hypotheses s),
proof_depth p ≤ 0 → X.
Lemma proof_depth_rule_1 :
∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
(r : sequent_rule)(in_rules : rules r)
(subproofs :
dep_list sequent (proof rules hypotheses) (assumptions r)),
proof_depth (rule rules hypotheses r in_rules subproofs) ≤ 1
→ assumptions r = [].
Lemma proof_ind :
∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
(P : ∀(s : sequent), proof rules hypotheses s → Prop),
(∀(gamma : sequent)(in_hypotheses : hypotheses gamma),
P gamma (assume rules hypotheses gamma in_hypotheses)) →
(∀(r : sequent_rule)(in_rules : rules r)
(pl : dep_list sequent (proof rules hypotheses) (assumptions r)),
every_dep_nth P (assumptions r) pl →
P (conclusion r) (rule rules hypotheses r in_rules pl)) →
∀(s : sequent)(p : proof rules hypotheses s), P s p.
Another, simpler induction scheme. Often, this simple induction
suffices.
Lemma proof_sequent_ind :
∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
(P : sequent → Prop),
(∀(gamma : sequent), hypotheses gamma → P gamma) →
(∀(r : sequent_rule),
rules r → every_nth P (assumptions r) → P (conclusion r))
→ ∀(s : sequent), proof rules hypotheses s → P s.
∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
(P : sequent → Prop),
(∀(gamma : sequent), hypotheses gamma → P gamma) →
(∀(r : sequent_rule),
rules r → every_nth P (assumptions r) → P (conclusion r))
→ ∀(s : sequent), proof rules hypotheses s → P s.
Definition provable(rules : set sequent_rule)(hypotheses : set sequent)
(s : sequent) : Prop :=
∃ _ : proof rules hypotheses s, True.
Lemma provable_with_assumption :
∀(rules : set sequent_rule)(hypotheses : set sequent)(s : sequent),
hypotheses s →
provable rules hypotheses s.
Lemma provable_with_rule :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(assum : list sequent)(s : sequent),
rules {| assumptions := assum; conclusion := s |} →
every_nth (provable rules hypotheses) assum →
provable rules hypotheses s.
Definition provable_at_depth(rules : set sequent_rule)
(hypotheses : set sequent)
(d : nat)
(s : sequent) : Prop :=
∃ p : proof rules hypotheses s, proof_depth p ≤ d.
Lemma provable_at_proof_depth :
∀(rules : set sequent_rule)(hypotheses : set sequent)(s : sequent)
(p : proof rules hypotheses s),
provable_at_depth rules hypotheses (proof_depth p) s.
Lemma provable_at_depth_provable :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(n : nat)(s : sequent),
provable_at_depth rules hypotheses n s →
provable rules hypotheses s.
Lemma provable_at_depth_0 :
∀(P : Prop)
(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
(s : sequent),
provable_at_depth rules hypotheses 0 s → P.
Lemma provable_at_depth_with_rule :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(assum : list sequent)(d : nat)(s : sequent),
rules {| assumptions := assum; conclusion := s |} →
every_nth (provable_at_depth rules hypotheses d) assum →
provable_at_depth rules hypotheses (S d) s.
Lemma provable_at_depth_destruct :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(d : nat)(s : sequent),
provable_at_depth rules hypotheses (S d) s →
hypotheses s ∨
(provable rules hypotheses s ∧
∃(r : sequent_rule), rules r ∧
s = conclusion r ∧
every_nth (provable_at_depth rules hypotheses d) (assumptions r)).
Induction on the proof depth, formulated with provability
Lemma proof_depth_sequent_ind :
∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
(P : nat → sequent → Prop),
(∀(n : nat),
(∀(s : sequent),
provable_at_depth rules hypotheses n s → P n s) →
∀(s : sequent),
provable_at_depth rules hypotheses (S n) s → P (S n) s)
→ ∀(s : sequent)(p : proof rules hypotheses s),
P (proof_depth p) s.
∀(rules : sequent_rule → Prop)(hypotheses : sequent → Prop)
(P : nat → sequent → Prop),
(∀(n : nat),
(∀(s : sequent),
provable_at_depth rules hypotheses n s → P n s) →
∀(s : sequent),
provable_at_depth rules hypotheses (S n) s → P (S n) s)
→ ∀(s : sequent)(p : proof rules hypotheses s),
P (proof_depth p) s.
Interpretation of sequents, page 9
Fixpoint or_formula_of_sequent_iter(res : lambda_formula)
(l : sequent) : lambda_formula :=
match l with
| [] ⇒ res
| f :: r ⇒ or_formula_of_sequent_iter (lambda_or res f) r
end.
Lemma or_formula_of_sequent_iter_append :
∀(s1 s2 : sequent)(f : lambda_formula),
or_formula_of_sequent_iter f (s1 ++ s2) =
or_formula_of_sequent_iter (or_formula_of_sequent_iter f s1) s2.
Lemma or_formula_of_sequent_iter_rev :
∀(f g : lambda_formula)(s : sequent),
or_formula_of_sequent_iter f (rev (g :: s)) =
lambda_or (or_formula_of_sequent_iter f (rev s)) g.
Definition or_formula_of_sequent(l : sequent)(nonempty_v : V)
: lambda_formula :=
match l with
| [] ⇒ lambda_false nonempty_v
| f :: r ⇒ or_formula_of_sequent_iter f r
end.
Definition or_formula_of_ne_sequent(l : sequent)(nonempty_l : l ≠ [])
: lambda_formula :=
match l return l ≠ [] → lambda_formula with
| [] ⇒ fun(H : [] ≠ []) ⇒ False_rect lambda_formula (H (eq_refl []))
| f :: r ⇒ fun _ ⇒ or_formula_of_sequent_iter f r
end nonempty_l.
Lemma or_formula_of_ne_sequent_tcc_irr :
∀(l : sequent)(nonempty_l_1 nonempty_l_2 : l ≠ []),
or_formula_of_ne_sequent l nonempty_l_1 =
or_formula_of_ne_sequent l nonempty_l_2.
Lemma or_formula_of_sequent_nonempty :
∀(s : sequent)(nonempty_v : V)(nonempty_s : s ≠ []),
or_formula_of_sequent s nonempty_v =
or_formula_of_ne_sequent s nonempty_s.
(l : sequent) : lambda_formula :=
match l with
| [] ⇒ res
| f :: r ⇒ or_formula_of_sequent_iter (lambda_or res f) r
end.
Lemma or_formula_of_sequent_iter_append :
∀(s1 s2 : sequent)(f : lambda_formula),
or_formula_of_sequent_iter f (s1 ++ s2) =
or_formula_of_sequent_iter (or_formula_of_sequent_iter f s1) s2.
Lemma or_formula_of_sequent_iter_rev :
∀(f g : lambda_formula)(s : sequent),
or_formula_of_sequent_iter f (rev (g :: s)) =
lambda_or (or_formula_of_sequent_iter f (rev s)) g.
Definition or_formula_of_sequent(l : sequent)(nonempty_v : V)
: lambda_formula :=
match l with
| [] ⇒ lambda_false nonempty_v
| f :: r ⇒ or_formula_of_sequent_iter f r
end.
Definition or_formula_of_ne_sequent(l : sequent)(nonempty_l : l ≠ [])
: lambda_formula :=
match l return l ≠ [] → lambda_formula with
| [] ⇒ fun(H : [] ≠ []) ⇒ False_rect lambda_formula (H (eq_refl []))
| f :: r ⇒ fun _ ⇒ or_formula_of_sequent_iter f r
end nonempty_l.
Lemma or_formula_of_ne_sequent_tcc_irr :
∀(l : sequent)(nonempty_l_1 nonempty_l_2 : l ≠ []),
or_formula_of_ne_sequent l nonempty_l_1 =
or_formula_of_ne_sequent l nonempty_l_2.
Lemma or_formula_of_sequent_nonempty :
∀(s : sequent)(nonempty_v : V)(nonempty_s : s ≠ []),
or_formula_of_sequent s nonempty_v =
or_formula_of_ne_sequent s nonempty_s.
Lemma proof_depth_mono :
∀(rules1 rules2 : set sequent_rule)(hyp1 hyp2 : set sequent)
(n : nat)(s : sequent),
subset rules1 rules2 →
subset hyp1 hyp2 →
provable_at_depth rules1 hyp1 n s →
provable_at_depth rules2 hyp2 n s.
Lemma proof_mono :
∀(rules1 rules2 : set sequent_rule)(hyp1 hyp2 : set sequent)
(s : sequent),
subset rules1 rules2 →
subset hyp1 hyp2 →
provable rules1 hyp1 s →
provable rules2 hyp2 s.
Lemma proof_mono_hyp :
∀(rules : set sequent_rule)(hyp1 hyp2 : set sequent)(s : sequent),
subset hyp1 hyp2 →
provable rules hyp1 s →
provable rules hyp2 s.
Lemma proof_mono_rules :
∀(rules1 rules2 : set sequent_rule)(hyp : set sequent)(s : sequent),
subset rules1 rules2 →
provable rules1 hyp s →
provable rules2 hyp s.
Lemma proof_set_equal :
∀(rules1 rules2 : set sequent_rule)(hyp1 hyp2 : set sequent)
(s : sequent),
set_equal rules1 rules2 →
set_equal hyp1 hyp2 →
provable rules1 hyp1 s →
provable rules2 hyp2 s.
Lemma proof_set_equal_rules :
∀(rules1 rules2 : set sequent_rule)(hyp : set sequent)
(s : sequent),
set_equal rules1 rules2 →
provable rules1 hyp s →
provable rules2 hyp s.
Definition sequent_multiset(ss : set sequent) : Prop :=
∀(s r : sequent), ss s → list_reorder s r → ss r.
Lemma sequent_multiset_empty : sequent_multiset empty_sequent_set.
Definition reordered_rule(or : sequent_rule)(s : sequent)(rr : sequent_rule)
: Prop :=
s = conclusion rr ∧
length (assumptions or) = length (assumptions rr) ∧
∀(n : nat)(n_less_rs : n < length (assumptions or))
(n_less_rr : n < length (assumptions rr)),
list_reorder (nth (assumptions or) n n_less_rs)
(nth (assumptions rr) n n_less_rr).
Definition rule_multiset(rs : set sequent_rule) : Prop :=
∀(or : sequent_rule)(s : sequent),
rs or →
list_reorder (conclusion or) s →
∃(rr : sequent_rule),
reordered_rule or s rr ∧
rs rr.
Lemma set_equal_multiset : ∀(rs1 rs2 : set sequent_rule),
set_equal rs1 rs2 →
rule_multiset rs1 →
rule_multiset rs2.
Lemma multiset_union : ∀(rs1 rs2 : set sequent_rule),
rule_multiset rs1 →
rule_multiset rs2 →
rule_multiset (union rs1 rs2).
Lemma multiset_depth_provability :
∀(rules : set sequent_rule)(hypothesis : set sequent)
(d : nat)(s r : sequent),
rule_multiset rules →
sequent_multiset hypothesis →
list_reorder s r →
provable_at_depth rules hypothesis d s →
provable_at_depth rules hypothesis d r.
Lemma multiset_provability :
∀(rules : set sequent_rule)(hypothesis : set sequent)(s r : sequent),
rule_multiset rules →
sequent_multiset hypothesis →
list_reorder s r →
provable rules hypothesis s →
provable rules hypothesis r.
Definition reordered_sequent_list_set(l : list sequent) : set sequent :=
fun(s1 : sequent) ⇒ ∃(s2 : sequent), list_reorder s1 s2 ∧ In s2 l.
Lemma sequent_multiset_reordered_sequent_list_set :
∀(l : list sequent), sequent_multiset (reordered_sequent_list_set l).
Lemma plug_hypothesis_proof :
∀(rules : set sequent_rule)(provable_hyp hyp : set sequent)
(s : sequent),
(∀(h : sequent), provable_hyp h → provable rules hyp h) →
provable rules (union provable_hyp hyp) s →
provable rules hyp s.
Lemma plug_empty_hypothesis_proof :
∀(rules : set sequent_rule)(provable_hyp : set sequent)
(s : sequent),
(∀(h : sequent), provable_hyp h →
provable rules empty_sequent_set h) →
provable rules provable_hyp s →
provable rules empty_sequent_set s.
Lemma change_rules_hyp_provability :
∀(rules1 rules2 : set sequent_rule)(hyp1 hyp2 : set sequent),
sequent_multiset hyp2 →
rule_multiset rules2 →
(∀(r : sequent_rule), rules1 r →
provable rules2
(union (reordered_sequent_list_set (assumptions r)) hyp2)
(conclusion r)) →
(∀(h : sequent), hyp1 h → provable rules2 hyp2 h) →
∀(s : sequent),
provable rules1 hyp1 s →
provable rules2 hyp2 s.
Lemma change_rules_provability :
∀(rules1 rules2 : set sequent_rule),
rule_multiset rules2 →
(∀(r : sequent_rule), rules1 r →
provable rules2 (reordered_sequent_list_set (assumptions r))
(conclusion r)) →
∀(s : sequent),
provable rules1 empty_sequent_set s →
provable rules2 empty_sequent_set s.
Modal rank, page 5
Definition modal_rank : lambda_formula → nat :=
lambda_formula_rec nat (fun _ ⇒ 1) id max
(fun _ (subranks : counted_list nat _) ⇒
1 + (nat_list_max (1 :: (list_of_counted_list subranks)))).
Lemma modal_rank_char :
∀(f : lambda_formula),
modal_rank f =
match f with
| lf_prop _ ⇒ 1
| lf_neg f ⇒ modal_rank f
| lf_and f1 f2 ⇒ max (modal_rank f1) (modal_rank f2)
| lf_modal op args ⇒
1 + (nat_list_max
(1 :: (map modal_rank (list_of_counted_list args))))
end.
Definition minimal_sequent_rank(s : sequent) : nat :=
nat_list_max (map modal_rank s).
Lemma modal_rank_ge_1 : ∀(f : lambda_formula),
0 < modal_rank f.
Lemma minimal_sequent_rank_gt_0 : ∀(s : sequent),
s ≠ [] → 0 < minimal_sequent_rank s.
lambda_formula_rec nat (fun _ ⇒ 1) id max
(fun _ (subranks : counted_list nat _) ⇒
1 + (nat_list_max (1 :: (list_of_counted_list subranks)))).
Lemma modal_rank_char :
∀(f : lambda_formula),
modal_rank f =
match f with
| lf_prop _ ⇒ 1
| lf_neg f ⇒ modal_rank f
| lf_and f1 f2 ⇒ max (modal_rank f1) (modal_rank f2)
| lf_modal op args ⇒
1 + (nat_list_max
(1 :: (map modal_rank (list_of_counted_list args))))
end.
Definition minimal_sequent_rank(s : sequent) : nat :=
nat_list_max (map modal_rank s).
Lemma modal_rank_ge_1 : ∀(f : lambda_formula),
0 < modal_rank f.
Lemma minimal_sequent_rank_gt_0 : ∀(s : sequent),
s ≠ [] → 0 < minimal_sequent_rank s.
This is used for F_n(\Lambda), page 6
Definition rank_formula(n : nat) : set lambda_formula :=
fun(f : lambda_formula) ⇒ modal_rank f ≤ n.
Lemma rank_formula_zero :
set_equal (rank_formula 0) (empty_set lambda_formula).
Lemma rank_formula_zero_TCC :
∀(A : Type)(f : lambda_formula), rank_formula 0 f → A.
Lemma rank_formula_ge :
∀(f : lambda_formula)(n1 n2 : nat),
n1 ≤ n2 →
rank_formula n1 f →
rank_formula n2 f.
Lemma rank_formula_lf_prop : ∀(v : V)(n : nat),
1 ≤ n → rank_formula n (lf_prop v).
Lemma rank_formula_lf_neg : ∀(n : nat)(f : lambda_formula),
rank_formula n (lf_neg f) ↔ rank_formula n f.
Lemma rank_formula_lf_neg_TCC : ∀(n : nat)(f : lambda_formula),
rank_formula n (lf_neg f) → rank_formula n f.
Lemma rank_formula_lf_and : ∀(n : nat)(f1 f2 : lambda_formula),
rank_formula n f1 → rank_formula n f2 → rank_formula n (lf_and f1 f2).
Lemma rank_formula_and_left : ∀(n : nat)(f1 f2 : lambda_formula),
rank_formula n (lf_and f1 f2) → rank_formula n f1.
Lemma rank_formula_and_right : ∀(n : nat)(f1 f2 : lambda_formula),
rank_formula n (lf_and f1 f2) → rank_formula n f2.
Lemma rank_formula_false : ∀(nonempty_v : V)(n : nat),
1 ≤ n → rank_formula n (lambda_false nonempty_v).
Lemma rank_formula_neg_form_maybe :
∀(fs : set lambda_formula)(n : nat)(f : lambda_formula),
(∀(f : lambda_formula), fs f → rank_formula n f) →
neg_form_maybe fs f →
rank_formula n f.
Lemma rank_formula_neg_and_over :
∀(fs : set lambda_formula)(n : nat)(f : lambda_formula),
(∀(f : lambda_formula), fs f → rank_formula n f) →
neg_and_over fs f →
rank_formula n f.
fun(f : lambda_formula) ⇒ modal_rank f ≤ n.
Lemma rank_formula_zero :
set_equal (rank_formula 0) (empty_set lambda_formula).
Lemma rank_formula_zero_TCC :
∀(A : Type)(f : lambda_formula), rank_formula 0 f → A.
Lemma rank_formula_ge :
∀(f : lambda_formula)(n1 n2 : nat),
n1 ≤ n2 →
rank_formula n1 f →
rank_formula n2 f.
Lemma rank_formula_lf_prop : ∀(v : V)(n : nat),
1 ≤ n → rank_formula n (lf_prop v).
Lemma rank_formula_lf_neg : ∀(n : nat)(f : lambda_formula),
rank_formula n (lf_neg f) ↔ rank_formula n f.
Lemma rank_formula_lf_neg_TCC : ∀(n : nat)(f : lambda_formula),
rank_formula n (lf_neg f) → rank_formula n f.
Lemma rank_formula_lf_and : ∀(n : nat)(f1 f2 : lambda_formula),
rank_formula n f1 → rank_formula n f2 → rank_formula n (lf_and f1 f2).
Lemma rank_formula_and_left : ∀(n : nat)(f1 f2 : lambda_formula),
rank_formula n (lf_and f1 f2) → rank_formula n f1.
Lemma rank_formula_and_right : ∀(n : nat)(f1 f2 : lambda_formula),
rank_formula n (lf_and f1 f2) → rank_formula n f2.
Lemma rank_formula_false : ∀(nonempty_v : V)(n : nat),
1 ≤ n → rank_formula n (lambda_false nonempty_v).
Lemma rank_formula_neg_form_maybe :
∀(fs : set lambda_formula)(n : nat)(f : lambda_formula),
(∀(f : lambda_formula), fs f → rank_formula n f) →
neg_form_maybe fs f →
rank_formula n f.
Lemma rank_formula_neg_and_over :
∀(fs : set lambda_formula)(n : nat)(f : lambda_formula),
(∀(f : lambda_formula), fs f → rank_formula n f) →
neg_and_over fs f →
rank_formula n f.
Unusual argument order because this is used to instantiate
form_prop_or in some_neg_form.v.
Lemma rank_formula_lambda_or :
∀(n : nat)(f1 f2 : lambda_formula),
rank_formula n f1 →
rank_formula n f2 →
rank_formula n (lambda_or f1 f2).
Lemma rank_formula_lambda_or_rev :
∀(f1 f2 : lambda_formula)(n : nat),
rank_formula n (lambda_or f1 f2) →
rank_formula n f1 ∧ rank_formula n f2.
Lemma rank_formula_prop_form : ∀(f : lambda_formula),
prop_form f → rank_formula 1 f.
Lemma rank_formula_modal :
∀(op : operator L)
(args : counted_list lambda_formula (arity L op))
(n : nat),
1 < n →
every_nth (rank_formula (pred n)) (list_of_counted_list args) →
rank_formula n (lf_modal op args).
∀(n : nat)(f1 f2 : lambda_formula),
rank_formula n f1 →
rank_formula n f2 →
rank_formula n (lambda_or f1 f2).
Lemma rank_formula_lambda_or_rev :
∀(f1 f2 : lambda_formula)(n : nat),
rank_formula n (lambda_or f1 f2) →
rank_formula n f1 ∧ rank_formula n f2.
Lemma rank_formula_prop_form : ∀(f : lambda_formula),
prop_form f → rank_formula 1 f.
Lemma rank_formula_modal :
∀(op : operator L)
(args : counted_list lambda_formula (arity L op))
(n : nat),
1 < n →
every_nth (rank_formula (pred n)) (list_of_counted_list args) →
rank_formula n (lf_modal op args).
Definition rank_sequent(n : nat) : set sequent :=
fun(s : sequent) ⇒ every_nth (rank_formula n) s.
Lemma rank_sequent_mono : ∀(n1 n2 : nat),
n1 ≤ n2 → subset (rank_sequent n1) (rank_sequent n2).
Lemma rank_sequent_list_reorder :
∀(s1 s2 : sequent)(n : nat), list_reorder s1 s2 →
((rank_sequent n s1) ↔ (rank_sequent n s2)).
Lemma rank_sequent_empty : ∀(n : nat), rank_sequent n [].
Lemma rank_sequent_cons : ∀(n : nat)(f : lambda_formula)(s : sequent),
rank_formula n f → rank_sequent n s → rank_sequent n (f :: s).
Lemma rank_sequent_head : ∀(n : nat)(f : lambda_formula)(s : sequent),
rank_sequent n (f :: s) → rank_formula n f.
Lemma rank_sequent_tail : ∀(n : nat)(f : lambda_formula)(s : sequent),
rank_sequent n (f :: s) → rank_sequent n s.
Lemma rank_sequent_append :
∀(s1 s2 : sequent)(n : nat),
rank_sequent n s1 → rank_sequent n s2 → rank_sequent n (s1 ++ s2).
Lemma rank_sequent_append_left :
∀(s1 s2 : sequent)(n : nat),
rank_sequent n (s1 ++ s2) → rank_sequent n s1.
Lemma rank_sequent_append_right :
∀(s1 s2 : sequent)(n : nat),
rank_sequent n (s1 ++ s2) → rank_sequent n s2.
Lemma rank_sequent_different_head :
∀(n : nat)(f : lambda_formula)(s1 s2 : sequent),
rank_sequent n (f :: s2) →
(rank_formula n f → rank_sequent n s1) →
rank_sequent n (s1 ++ s2).
Lemma rank_formula_or_formula_iter :
∀(s : sequent)(f : lambda_formula)(n : nat),
rank_sequent n s →
rank_formula n f →
rank_formula n (or_formula_of_sequent_iter f s).
Lemma rank_formula_or_formula_iter_rev :
∀(s : sequent)(f : lambda_formula)(n : nat),
rank_formula n (or_formula_of_sequent_iter f s) →
rank_formula n f ∧ rank_sequent n s.
Lemma rank_formula_or_formula_of_sequent :
∀(s : sequent)(n : nat)(nonempty_v : V),
1 ≤ n →
rank_sequent n s →
rank_formula n (or_formula_of_sequent s nonempty_v).
The unusual argument order simplifies the proof of
state_seq_step_semantics_correct
Lemma rank_formula_succ_or_formula_of_sequent :
∀(n : nat)(nonempty_v : V)(s : sequent),
rank_sequent (S n) s →
rank_formula (S n) (or_formula_of_sequent s nonempty_v).
Lemma rank_formula_or_formula_of_ne_sequent :
∀(s : sequent)(n : nat)(nonempty_s : s ≠ []),
rank_sequent n s →
rank_formula n (or_formula_of_ne_sequent s nonempty_s).
Lemma rank_prop_sequent : ∀(s : sequent),
prop_sequent s → rank_sequent 1 s.
Lemma rank_sequent_minimal_sequent_rank : ∀(s : sequent),
rank_sequent (minimal_sequent_rank s) s.
Lemma rank_sequent_succ_minimal_nonempty_sequent_rank :
∀(s : sequent),
s ≠ [] → rank_sequent (S (pred (minimal_sequent_rank s))) s.
Lemma rank_sequent_le_minimal : ∀(s : sequent)(n : nat),
minimal_sequent_rank s ≤ n →
rank_sequent n s.
Lemma rank_sequent_ge_minimal : ∀(s : sequent)(n : nat),
rank_sequent n s → minimal_sequent_rank s ≤ n.
Lemma rank_formula_modal_ge_2 :
∀(op : operator L)
(args : counted_list lambda_formula (arity L op))
(n : nat),
rank_formula n (lf_modal op args) →
1 < n.
Lemma rank_formula_modal_1_TCC :
∀(A : Type)(op : operator L)
(args : counted_list lambda_formula (arity L op)),
rank_formula 1 (lf_modal op args) → A.
Lemma rank_formula_modal_args_TCC :
∀(op : operator L)
(args : counted_list lambda_formula (arity L op))
(n : nat),
rank_formula n (lf_modal op args) →
every_nth (rank_formula (pred n)) (list_of_counted_list args).
∀(n : nat)(nonempty_v : V)(s : sequent),
rank_sequent (S n) s →
rank_formula (S n) (or_formula_of_sequent s nonempty_v).
Lemma rank_formula_or_formula_of_ne_sequent :
∀(s : sequent)(n : nat)(nonempty_s : s ≠ []),
rank_sequent n s →
rank_formula n (or_formula_of_ne_sequent s nonempty_s).
Lemma rank_prop_sequent : ∀(s : sequent),
prop_sequent s → rank_sequent 1 s.
Lemma rank_sequent_minimal_sequent_rank : ∀(s : sequent),
rank_sequent (minimal_sequent_rank s) s.
Lemma rank_sequent_succ_minimal_nonempty_sequent_rank :
∀(s : sequent),
s ≠ [] → rank_sequent (S (pred (minimal_sequent_rank s))) s.
Lemma rank_sequent_le_minimal : ∀(s : sequent)(n : nat),
minimal_sequent_rank s ≤ n →
rank_sequent n s.
Lemma rank_sequent_ge_minimal : ∀(s : sequent)(n : nat),
rank_sequent n s → minimal_sequent_rank s ≤ n.
Lemma rank_formula_modal_ge_2 :
∀(op : operator L)
(args : counted_list lambda_formula (arity L op))
(n : nat),
rank_formula n (lf_modal op args) →
1 < n.
Lemma rank_formula_modal_1_TCC :
∀(A : Type)(op : operator L)
(args : counted_list lambda_formula (arity L op)),
rank_formula 1 (lf_modal op args) → A.
Lemma rank_formula_modal_args_TCC :
∀(op : operator L)
(args : counted_list lambda_formula (arity L op))
(n : nat),
rank_formula n (lf_modal op args) →
every_nth (rank_formula (pred n)) (list_of_counted_list args).
Definition rank_sequent_set(n : nat)(ss : set sequent) : Prop :=
∀(s : sequent), ss s → rank_sequent n s.
Lemma rank_sequent_set_empty : ∀(n : nat),
rank_sequent_set n (empty_sequent_set).
Lemma rank_sequent_set_mono : ∀(n1 n2 : nat)(ss : set sequent),
n1 ≤ n2 →
rank_sequent_set n1 ss →
rank_sequent_set n2 ss.
Lemma rank_sequent_set_sequent_list_set :
∀(n : nat)(sl : list sequent),
every_nth (rank_sequent n) sl →
rank_sequent_set n (reordered_sequent_list_set sl).
Definition rule_has_rank(n : nat)(r : sequent_rule) : Prop :=
every_nth (rank_sequent n) (assumptions r) ∧
rank_sequent n (conclusion r).
Definition rank_rules(n : nat)(rules : set sequent_rule) : set sequent_rule :=
fun(r : sequent_rule) ⇒
rules r ∧ rule_has_rank n r.
Lemma subset_rank_rules :
∀(n : nat)(rules : set sequent_rule),
subset (rank_rules n rules) rules.
Lemma rank_rules_mono :
∀(n : nat)(rules1 rules2 : set sequent_rule),
subset rules1 rules2 →
subset (rank_rules n rules1) (rank_rules n rules2).
Lemma rank_rules_set_eq :
∀(n : nat)(rules1 rules2 : set sequent_rule),
set_equal rules1 rules2 →
set_equal (rank_rules n rules1) (rank_rules n rules2).
Lemma rank_rules_subset_rank :
∀(n1 n2 : nat)(rules : set sequent_rule),
n1 ≤ n2 →
subset (rank_rules n1 rules) (rank_rules n2 rules).
Lemma multiset_rank_rules : ∀(n : nat)(rules : set sequent_rule),
rule_multiset rules → rule_multiset (rank_rules n rules).
Lemma provable_rank_rules_hyp_has_rank_n :
∀(rules : set sequent_rule)(hyp : set sequent)
(n : nat)(s : sequent),
rank_sequent_set n hyp →
provable (rank_rules n rules) hyp s →
rank_sequent n s.
Lemma provable_rank_rules_has_rank_n :
∀(rules : set sequent_rule)(n : nat)(s : sequent),
provable (rank_rules n rules) empty_sequent_set s →
rank_sequent n s.
Lemma rank_rules_distribute_union :
∀(n : nat)(rules1 rules2 : set sequent_rule),
set_equal (rank_rules n (union rules1 rules2))
(union (rank_rules n rules1) (rank_rules n rules2)).
every_nth (rank_sequent n) (assumptions r) ∧
rank_sequent n (conclusion r).
Definition rank_rules(n : nat)(rules : set sequent_rule) : set sequent_rule :=
fun(r : sequent_rule) ⇒
rules r ∧ rule_has_rank n r.
Lemma subset_rank_rules :
∀(n : nat)(rules : set sequent_rule),
subset (rank_rules n rules) rules.
Lemma rank_rules_mono :
∀(n : nat)(rules1 rules2 : set sequent_rule),
subset rules1 rules2 →
subset (rank_rules n rules1) (rank_rules n rules2).
Lemma rank_rules_set_eq :
∀(n : nat)(rules1 rules2 : set sequent_rule),
set_equal rules1 rules2 →
set_equal (rank_rules n rules1) (rank_rules n rules2).
Lemma rank_rules_subset_rank :
∀(n1 n2 : nat)(rules : set sequent_rule),
n1 ≤ n2 →
subset (rank_rules n1 rules) (rank_rules n2 rules).
Lemma multiset_rank_rules : ∀(n : nat)(rules : set sequent_rule),
rule_multiset rules → rule_multiset (rank_rules n rules).
Lemma provable_rank_rules_hyp_has_rank_n :
∀(rules : set sequent_rule)(hyp : set sequent)
(n : nat)(s : sequent),
rank_sequent_set n hyp →
provable (rank_rules n rules) hyp s →
rank_sequent n s.
Lemma provable_rank_rules_has_rank_n :
∀(rules : set sequent_rule)(n : nat)(s : sequent),
provable (rank_rules n rules) empty_sequent_set s →
rank_sequent n s.
Lemma rank_rules_distribute_union :
∀(n : nat)(rules1 rules2 : set sequent_rule),
set_equal (rank_rules n (union rules1 rules2))
(union (rank_rules n rules1) (rank_rules n rules2)).
Definition minimal_rule_rank(r : sequent_rule) : nat :=
nat_list_max ((minimal_sequent_rank (conclusion r)) ::
(map minimal_sequent_rank (assumptions r))).
Lemma minimal_rule_rank_gt_0 : ∀(r : sequent_rule),
conclusion r ≠ [] →
0 < minimal_rule_rank r.
Lemma minimal_rule_rank_assumptions : ∀(r : sequent_rule),
every_nth (rank_sequent (minimal_rule_rank r)) (assumptions r).
Lemma minimal_rule_rank_conclusion : ∀(r : sequent_rule),
rank_sequent (minimal_rule_rank r) (conclusion r).
Lemma rank_rules_minimal_rule_rank :
∀(rules : set (sequent_rule))(r : sequent_rule)(n : nat),
rules r →
minimal_rule_rank r ≤ n →
rank_rules n rules r.
Lemma rank_rules_ge_minimal : ∀(r : sequent_rule)(n : nat),
rule_has_rank n r → minimal_rule_rank r ≤ n.
Definition minimal_proof_rank{rules : sequent_rule → Prop}
{hypotheses : sequent → Prop}
{s : sequent}
(p : proof rules hypotheses s) : nat :=
proof_rect rules hypotheses (fun _ ⇒ nat)
(fun(s : sequent) _ ⇒ minimal_sequent_rank s)
(fun(r : sequent_rule) _
(l : dep_list sequent (fun _ ⇒ nat) (assumptions r)) ⇒
max (minimal_rule_rank r)
(nat_list_max (list_of_dep_list (assumptions r) l)))
s p.
Lemma minimal_proof_rank_char :
∀(rules : set sequent_rule)(hypotheses : set sequent)
(s : sequent)(p : proof rules hypotheses s),
minimal_proof_rank p = match p with
| assume g _ ⇒ minimal_sequent_rank g
| rule r _ subp ⇒
max (minimal_rule_rank r)
(nat_list_max
(dep_map_dep_const (@minimal_proof_rank rules hypotheses)
(assumptions r) subp))
end.
Definition prop_var_formula : lambda_formula → list V :=
lambda_formula_rec (list V)
(fun(v : V) ⇒ [v])
id
(@app V)
(fun(op : operator L)(pl : counted_list (list V) (arity L op)) ⇒
flatten (list_of_counted_list pl)).
Definition prop_var_modal_args(n : nat)
(args : counted_list lambda_formula n) : list V :=
flatten ((map prop_var_formula) (list_of_counted_list args)).
Lemma prop_var_formula_char : ∀(f : lambda_formula),
prop_var_formula f = match f with
| lf_prop v ⇒ [v]
| lf_neg f ⇒ prop_var_formula f
| lf_and f1 f2 ⇒ (prop_var_formula f1) ++ (prop_var_formula f2)
| lf_modal op args ⇒ prop_var_modal_args (arity L op) args
end.
Lemma prop_var_modal_args_cons :
∀(n : nat)(form : lambda_formula)
(args : counted_list lambda_formula n),
prop_var_modal_args (S n) (counted_cons form args) =
(prop_var_formula form) ++ (prop_var_modal_args n args).
Definition prop_var_sequent(s : sequent) : list V :=
flatten (map prop_var_formula s).
Lemma prop_var_sequent_cons :
∀(f : lambda_formula)(s : sequent),
prop_var_sequent (f :: s) = (prop_var_formula f) ++ prop_var_sequent s.
Lemma prop_var_sequent_append : ∀(s1 s2 : sequent),
prop_var_sequent (s1 ++ s2) =
(prop_var_sequent s1) ++ (prop_var_sequent s2).
Lemma prop_var_sequent_list_reorder : ∀(s1 s2 : sequent),
list_reorder s1 s2 →
list_reorder (prop_var_sequent s1) (prop_var_sequent s2).
Lemma In_prop_var_sequent :
∀(v : V)(s : sequent),
In v (prop_var_sequent s) →
∃(f : lambda_formula),
In v (prop_var_formula f) ∧ In f s.
Lemma incl_prop_var_formula_sequent :
∀(f : lambda_formula)(s : sequent),
In f s →
incl (prop_var_formula f) (prop_var_sequent s).
Lemma prop_var_sequent_cutout_nth : ∀(n : nat)(s : sequent),
every_nth (fun f ⇒ length (prop_var_formula f) = 1) s →
prop_var_sequent (cutout_nth s n) = cutout_nth (prop_var_sequent s) n.
End Formulas.
Implicit Arguments lf_prop [[V] [L]].
Implicit Arguments lf_neg [[V] [L]].
Implicit Arguments lf_and [[V] [L]].
Implicit Arguments lf_modal [[V] [L]].
Implicit Arguments lambda_formula_rect [V L].
Implicit Arguments lambda_formula_rec [V L A].
Implicit Arguments is_prop [[V] [L]].
Implicit Arguments is_neg [[V] [L]].
Implicit Arguments is_and [[V] [L]].
Implicit Arguments is_modal [[V] [L]].
Implicit Arguments get_prop_var [V L].
Implicit Arguments get_neg_form [V L].
Implicit Arguments get_and_forms [V L].
Implicit Arguments get_modal_args [V L].
Implicit Arguments lambda_or [V L].
Implicit Arguments lambda_false [V L].
Implicit Arguments lf_modal_inversion_op [V L].
Implicit Arguments assumptions [V L].
Implicit Arguments conclusion [V L].
Implicit Arguments prop_form [[V] [L]].
Implicit Arguments prop_form_acc [V L].
Implicit Arguments neg_form [[V] [L]].
Implicit Arguments neg_form_maybe [V L].
Implicit Arguments prop_sequent [[V] [L]].
Implicit Arguments prop_sequent_head [V L].
Implicit Arguments prop_sequent_tail [V L].
Implicit Arguments neg_and_over [V L].
Implicit Arguments formula_measure [V L].
Implicit Arguments formula_measure_char [V L].
Implicit Arguments sequent_measure [[V] [L]].
Implicit Arguments proof [V L].
Implicit Arguments assume [V L].
Implicit Arguments rule [V L].
Implicit Arguments proof_depth [V L rules hypotheses s].
Implicit Arguments proof_depth_rule [V L].
Implicit Arguments provable [V L].
Implicit Arguments provable_at_depth [V L].
Implicit Arguments proof_depth_sequent_ind [V L].
Implicit Arguments or_formula_of_sequent_iter [V L].
Implicit Arguments or_formula_of_sequent [V L].
Implicit Arguments or_formula_of_ne_sequent [V L].
Implicit Arguments sequent_multiset [V L].
Implicit Arguments reordered_rule [V L].
Implicit Arguments rule_multiset [V L].
Implicit Arguments reordered_sequent_list_set [V L].
Implicit Arguments modal_rank [V L].
Implicit Arguments modal_rank_char [V L].
Implicit Arguments minimal_sequent_rank [V L].
Implicit Arguments modal_rank_ge_1 [V L].
Implicit Arguments rank_formula [V L].
Implicit Arguments rank_formula_ge [V L].
Implicit Arguments rank_formula_lf_neg_TCC [V L].
Implicit Arguments rank_formula_modal_ge_2 [V L].
Implicit Arguments rank_formula_modal_1_TCC [V L].
Implicit Arguments rank_formula_modal_args_TCC [V L].
Implicit Arguments rank_formula_lf_neg [V L].
Implicit Arguments rank_formula_and_left [V L].
Implicit Arguments rank_formula_and_right [V L].
Implicit Arguments rank_formula_lambda_or [V L].
Implicit Arguments rank_sequent [V L].
Implicit Arguments rank_sequent_head [V L].
Implicit Arguments rank_sequent_cons [V L].
Implicit Arguments rank_sequent_list_reorder [V L].
Implicit Arguments rank_sequent_head [V L].
Implicit Arguments rank_sequent_tail [V L].
Implicit Arguments rank_sequent_append [V L].
Implicit Arguments rank_sequent_append_left [V L].
Implicit Arguments rank_sequent_append_right [V L].
Implicit Arguments rank_formula_or_formula_iter_rev [V L].
Implicit Arguments rank_formula_succ_or_formula_of_sequent [V L].
Implicit Arguments rank_sequent_succ_minimal_nonempty_sequent_rank [V L].
Implicit Arguments rank_sequent_set [V L].
Implicit Arguments rule_has_rank [V L].
Implicit Arguments rank_rules [V L].
Implicit Arguments provable_rank_rules_hyp_has_rank_n [V L].
Implicit Arguments rank_rules_distribute_union [V L].
Implicit Arguments minimal_rule_rank [V L].
Implicit Arguments rank_rules_minimal_rule_rank [V L].
Implicit Arguments minimal_proof_rank [V L rules hypotheses s].
Implicit Arguments prop_var_formula [V L].
Implicit Arguments prop_var_formula_char [V L].
Implicit Arguments prop_var_modal_args [V L].
Implicit Arguments prop_var_sequent [[V] [L]].