(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/".
-
include "nat/plus.ma".
include "nat/compare.ma".
include "list/sort.ma".
| cons F l' ⇒ FAnd F (and_of_list l')
].
-alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)".
let rec or_of_list l ≝
match l with
- [ Nil ⇒ FFalse
- | Cons F l' ⇒ FOr F (or_of_list l')
+ [ nil ⇒ FFalse
+ | cons F l' ⇒ FOr F (or_of_list l')
].
definition formula_of_sequent ≝
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;
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;
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;
[ 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);
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
]
[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
|4,5:
simplify in H2;
destruct H2
- | simplify in H2;
+ | simplify in H1;
destruct H1
]
|4,5:
[ 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
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;
| 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
]);
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;
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
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
]
]
| intro;
- elim t;
+ elim a;
[ elim H;
[ left;
elim H4;
- apply (ex_intro ? ? (FTrue::a));
+ apply (ex_intro ? ? (FTrue::a1));
simplify;
elim H5;
autobatch
| elim H;
[ left;
elim H4;
- apply (ex_intro ? ? (FAtom n::a));
+ apply (ex_intro ? ? (FAtom n::a1));
simplify;
elim H5;
autobatch
| 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
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;
]
[ autobatch
- | generalize in match H4; clear H4;
- generalize in match H2; clear H2;
- elim t1;
+ | elim t1 in H4 H2 ⊢ %;
[
|
|
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 axiom
- | elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2);
+ apply (ExchangeL ? a2 a3 (FAtom a1));
+ apply (ExchangeR ? a4 a5 (FAtom a1));
+ apply Axiom
+ | elim (sizel_0_no_axiom_is_tautology a b H H1 H2);
[ decompose;
rewrite > H3;
- apply (exchangeL ? a a1 FFalse);
- apply falseL
+ apply (ExchangeL ? a1 a2 FFalse);
+ apply FalseL
| decompose;
rewrite > H3;
- apply (exchangeR ? a a1 FTrue);
- apply trueR
+ apply (ExchangeR ? a1 a2 FTrue);
+ apply TrueR
]
]
qed.