X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpropositional_sequent_calculus.ma;h=42ae9682532ce8f65811f23944ec7e0f2a83cf0c;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=32e11054c5d19bdb699f77578b4fa60fd1c83154;hpb=8007484b3da47896a36ced930b1174adba42579b;p=helm.git diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma index 32e11054c..42ae96825 100644 --- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma +++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/". - include "nat/plus.ma". include "nat/compare.ma". include "list/sort.ma". @@ -183,6 +181,8 @@ axiom symm_andb: symmetric ? andb. axiom associative_andb: associative ? andb. axiom distributive_andb_orb: distributive ? andb orb. +lemma andb_true: ∀x.(true ∧ x) = x. intro; reflexivity. qed. + lemma and_of_list_permut: ∀i,f,l1,l2. eval i (and_of_list (l1 @ (f::l2))) = eval i (and_of_list (f :: l1 @ l2)). intros; @@ -244,11 +244,20 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F). lapply (H4 i); clear H4; rewrite > symm_orb in ⊢ (? ? (? ? %) ?); rewrite > distributive_orb_andb; + demodulate. + reflexivity. + (* autobatch paramodulation + by distributive_orb_andb,symm_orb,symm_orb, + Hletin, Hletin1,andb_true. + *) | simplify in H2 ⊢ %; intros; lapply (H2 i); clear H2; - autobatch + pump 100. pump 100. + demodulate. + reflexivity. + (* autobatch paramodulation by andb_assoc, Hletin. *) | simplify in H2 H4 ⊢ %; intros; lapply (H2 i); clear H2; @@ -258,11 +267,13 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F). rewrite > demorgan2; rewrite > symm_orb; rewrite > distributive_orb_andb; - autobatch paramodulation + demodulate. + reflexivity. + (* autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1. *) | simplify in H2 ⊢ %; intros; lapply (H2 i); clear H2; - autobatch + autobatch paramodulation; | simplify in H2 ⊢ %; intros; lapply (H2 i); clear H2; @@ -396,7 +407,7 @@ theorem mem_to_exists_l1_l2: [ simplify in H1; destruct H1 | simplify in H2; - apply (bool_elim ? (eq n t)); + apply (bool_elim ? (eq n a)); intro; [ apply (ex_intro ? ? []); apply (ex_intro ? ? l1); @@ -408,8 +419,8 @@ theorem mem_to_exists_l1_l2: elim (H H1 H2); elim H4; rewrite > H5; - apply (ex_intro ? ? (t::a)); - apply (ex_intro ? ? a1); + apply (ex_intro ? ? (a::a1)); + apply (ex_intro ? ? a2); simplify; reflexivity ] @@ -422,8 +433,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2. [1,2: simplify in H; destruct H - | generalize in match H; clear H; - elim f2; + | elim f2 in H ⊢ %; [1,2: simplify in H; destruct H @@ -433,7 +443,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2. |4,5: simplify in H2; destruct H2 - | simplify in H2; + | simplify in H1; destruct H1 ] |4,5: @@ -467,7 +477,7 @@ lemma mem_same_atom_to_exists: [ simplify in H; destruct H | simplify in H1; - apply (bool_elim ? (same_atom f t)); + apply (bool_elim ? (same_atom f a)); intros; [ elim (same_atom_to_exists ? ? H2); autobatch @@ -491,14 +501,14 @@ lemma look_for_axiom: simplify; reflexivity | intros; - generalize in match (refl_eq ? (mem ? same_atom t l2)); - elim (mem ? same_atom t l2) in ⊢ (? ? ? %→?); + generalize in match (refl_eq ? (mem ? same_atom a l2)); + elim (mem ? same_atom a l2) in ⊢ (? ? ? %→?); [ left; elim (mem_to_exists_l1_l2 ? ? ? ? same_atom_to_eq H1); elim H2; clear H2; elim (mem_same_atom_to_exists ? ? H1); rewrite > H2 in H3; - apply (ex_intro ? ? a2); + apply (ex_intro ? ? a3); rewrite > H2; apply (ex_intro ? ? []); simplify; @@ -506,22 +516,22 @@ lemma look_for_axiom: | elim (H l2); [ left; decompose; - apply (ex_intro ? ? a); - apply (ex_intro ? ? (t::a1)); + apply (ex_intro ? ? a1); + apply (ex_intro ? ? (a::a2)); simplify; - apply (ex_intro ? ? a2); apply (ex_intro ? ? a3); - autobatch + apply (ex_intro ? ? a4); + autobatch depth=4 | right; intro; - apply (bool_elim ? (same_atom t (FAtom n1))); + apply (bool_elim ? (same_atom a (FAtom n1))); [ intro; rewrite > (eq_to_eq_mem ? ? transitiveb_same_atom ? ? ? H3) in H1; rewrite > H1; autobatch | intro; change in ⊢ (? ? (? % ?) ?) with - (match same_atom (FAtom n1) t with + (match same_atom (FAtom n1) a with [true ⇒ true |false ⇒ mem ? same_atom (FAtom n1) l ]); @@ -588,22 +598,16 @@ lemma sizel_0_no_axiom_is_tautology: intros; lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1; simplify in Hletin; - generalize in match Hletin; clear Hletin; - generalize in match H2; clear H2; - generalize in match H; clear H; - elim l1 0; + elim l1 in Hletin H2 H ⊢ % 0; [ intros; simplify in H2; - generalize in match H2; clear H2; - generalize in match H1; clear H1; - generalize in match H; clear H; - elim l2 0; + elim l2 in H2 H1 H ⊢ % 0; [ intros; simplify in H2; destruct H2 | simplify; intro; - elim t; + elim a; [ right; apply (ex_intro ? ? []); simplify; @@ -616,10 +620,10 @@ lemma sizel_0_no_axiom_is_tautology: elim (not_eq_nil_append_cons ? ? ? ? H6) | elim H4; right; - apply (ex_intro ? ? (FFalse::a)); + apply (ex_intro ? ? (FFalse::a1)); simplify; elim H5; - apply (ex_intro ? ? a1); + apply (ex_intro ? ? a2); autobatch |3,4: autobatch | assumption @@ -631,7 +635,7 @@ lemma sizel_0_no_axiom_is_tautology: elim (not_eq_nil_append_cons ? ? ? ? H5) | right; elim H4; - apply (ex_intro ? ? (FAtom n::a)); + apply (ex_intro ? ? (FAtom n::a1)); simplify; elim H; autobatch @@ -644,11 +648,11 @@ lemma sizel_0_no_axiom_is_tautology: ] ] | intro; - elim t; + elim a; [ elim H; [ left; elim H4; - apply (ex_intro ? ? (FTrue::a)); + apply (ex_intro ? ? (FTrue::a1)); simplify; elim H5; autobatch @@ -668,7 +672,7 @@ lemma sizel_0_no_axiom_is_tautology: | elim H; [ left; elim H4; - apply (ex_intro ? ? (FAtom n::a)); + apply (ex_intro ? ? (FAtom n::a1)); simplify; elim H5; autobatch @@ -677,8 +681,7 @@ lemma sizel_0_no_axiom_is_tautology: | assumption | lapply (H2 n1); clear H2; simplify in Hletin; - generalize in match Hletin; clear Hletin; - elim (eqb n1 n); + elim (eqb n1 n) in Hletin ⊢ %; [ simplify in H2; rewrite > H2; autobatch @@ -693,10 +696,7 @@ lemma sizel_0_no_axiom_is_tautology: rewrite > eqb_n_n in H3; simplify in H3; (* - generalize in match H3; - generalize in match H1; clear H1; - generalize in match H; clear H; - elim l 0; + elim l in H3 H1 H ⊢ % 0; [ elim l2 0; [ intros; simplify in H2; @@ -714,9 +714,7 @@ lemma sizel_0_no_axiom_is_tautology: ] [ autobatch - | generalize in match H4; clear H4; - generalize in match H2; clear H2; - elim t1; + | elim t1 in H4 H2 ⊢ %; [ | | @@ -747,21 +745,21 @@ lemma completeness_base: elim S 1; clear S; simplify in ⊢ (?→%→?); intros; - elim (look_for_axiom t t1); + elim (look_for_axiom a b); [ decompose; rewrite > H2; clear H2; rewrite > H4; clear H4; - apply (ExchangeL ? a1 a2 (FAtom a)); - apply (ExchangeR ? a3 a4 (FAtom a)); + apply (ExchangeL ? a2 a3 (FAtom a1)); + apply (ExchangeR ? a4 a5 (FAtom a1)); apply Axiom - | elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2); + | elim (sizel_0_no_axiom_is_tautology a b H H1 H2); [ decompose; rewrite > H3; - apply (ExchangeL ? a a1 FFalse); + apply (ExchangeL ? a1 a2 FFalse); apply FalseL | decompose; rewrite > H3; - apply (ExchangeR ? a a1 FTrue); + apply (ExchangeR ? a1 a2 FTrue); apply TrueR ] ]