X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpropositional_sequent_calculus.ma;h=36bb7e86308d07d2869fb0ad45d484d6bb9e8a1a;hb=71b481a2c2c95d9f80ff49f828336098b3de3924;hp=f68cfd22cbba1a47ac928e4b417073bbc00d4924;hpb=59d7f64e2e1a22ded8f9017942ca640fe62d886a;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 f68cfd22c..36bb7e863 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". @@ -396,7 +394,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 +406,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 +420,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 @@ -467,7 +464,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 +488,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 +503,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); + apply (ex_intro ? ? a4); autobatch | 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 +585,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 +607,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 +622,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 +635,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 +659,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 +668,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 +683,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 +701,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 +732,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 ] ]