let s = BoxPp.render_to_string ?map_unicode_to_tex render n mpres in
remove_closed_substs s
-let txt_of_cic_object ?map_unicode_to_tex n style prefix obj =
+let txt_of_cic_object
+ ?map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj
+=
let get_aobj obj =
try
let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
let lazy_term_pp = term_pp in
let obj_pp = CicNotationPp.pp_obj term_pp in
let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
- let script = Acic2Procedural.acic2procedural
- ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
+ let script =
+ Acic2Procedural.acic2procedural
+ ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed
+ ?skip_initial_lambdas prefix aobj
+ in
String.concat "" (List.map aux script) ^ "\n\n"
let txt_of_inline_macro style suri prefix =
(* columns, rendering style, name prefix, object *)
val txt_of_cic_object:
- ?map_unicode_to_tex:bool -> int -> GrafiteAst.presentation_style -> string ->
+ ?map_unicode_to_tex:bool ->
+ ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:bool ->
+ int -> GrafiteAst.presentation_style -> string ->
Cic.obj ->
string
[1,3:elim Hcut;elim H4;elim H5;clear Hcut H4 H5;rewrite > (H H6 H8);
rewrite > (H1 H7 H9);reflexivity
|*:split
- [1,3:split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;auto
- |*:split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;auto]]]
+ [1,3:split;unfold;intro;apply H2;apply natinG_or_inH_to_natinGH;autobatch
+ |*:split;unfold;intro;apply H3;apply natinG_or_inH_to_natinGH;autobatch]]]
qed.
lemma subst_type_nat_swap : \forall u,v,T,X,m.
|intros;lapply (inj_tail ? ? ? ? ? H9);
rewrite < Hletin3 in H6;rewrite < H8 in H6;
apply (H1 ? H4 H6)]]]
- |elim (leb a t);auto]]]]
+ |elim (leb a t);autobatch]]]]
qed.
(*** lemmas on well-formedness ***)
[rewrite > H;rewrite > H in Hletin;simplify;constructor 1
|rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin;
unfold;apply le_S_S;assumption]
- |elim (leb (t_len T1) (t_len T2));auto]
+ |elim (leb (t_len T1) (t_len T2));autobatch]
|elim T1;simplify;reflexivity]
qed.
lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;unfold;
constructor 2;assumption
|rewrite > H;simplify;unfold;constructor 1]
- |elim (leb (t_len T1) (t_len T2));auto]
+ |elim (leb (t_len T1) (t_len T2));autobatch]
|elim T1;simplify;reflexivity]
qed.
[rewrite > H;rewrite > H in Hletin;simplify;constructor 1
|rewrite > H;rewrite > H in Hletin;simplify;simplify in Hletin;
unfold;apply le_S_S;assumption]
- |elim (leb (t_len T1) (t_len T2));auto]
+ |elim (leb (t_len T1) (t_len T2));autobatch]
|elim T1;simplify;reflexivity]
qed.
lapply (not_le_to_lt ? ? Hletin);unfold in Hletin1;unfold;
constructor 2;assumption
|rewrite > H;simplify;unfold;constructor 1]
- |elim (leb (t_len T1) (t_len T2));auto]
+ |elim (leb (t_len T1) (t_len T2));autobatch]
|elim T1;simplify;reflexivity]
qed.
|intros;destruct H10
|intros;destruct H14
|intros;destruct H14;rewrite > Hcut1;assumption]]
- |split;unfold;intro;apply H5;apply natinG_or_inH_to_natinGH;auto]]
+ |split;unfold;intro;apply H5;apply natinG_or_inH_to_natinGH;autobatch]]
qed.
(*
(*** useful definitions and lemmas not really related to Fsub ***)
lemma eqb_case : \forall x,y.(eqb x y) = true \lor (eqb x y) = false.
-intros;elim (eqb x y);auto;
+intros;elim (eqb x y);autobatch;
qed.
lemma eq_eqb_case : \forall x,y.((x = y) \land (eqb x y) = true) \lor
((x \neq y) \land (eqb x y) = false).
intros;lapply (eqb_to_Prop x y);elim (eqb_case x y)
- [rewrite > H in Hletin;simplify in Hletin;left;auto
- |rewrite > H in Hletin;simplify in Hletin;right;auto]
+ [rewrite > H in Hletin;simplify in Hletin;left;autobatch
+ |rewrite > H in Hletin;simplify in Hletin;right;autobatch]
qed.
let rec max m n \def
[apply sym_eq.
apply div_plus_times.
assumption
- |auto
+ |autobatch
]
|apply lt_mod_m_m.
assumption
apply p_ord_exp1
[apply lt_O_nth_prime_n
|assumption
- |auto
+ |autobatch
]
qed.
(ord_rem n (nth_prime (max_prime_factor n))))
[apply lt_to_le.assumption
|apply le_n
- |auto
+ |autobatch
|assumption
]
|left.apply sym_eq.assumption
absurd (j = (h n1))
[rewrite < H10.
rewrite > H5
- [reflexivity|assumption|auto]
+ [reflexivity|assumption|autobatch]
|apply eqb_false_to_not_eq.
generalize in match H11.
elim (eqb j (h n1))
apply eq_f.
rewrite > sym_plus.
apply plus_minus_m_m.
- auto
+ autobatch
]
]
|intros.
change with ((i/S m) < S n).
apply (lt_times_to_lt_l m).
apply (le_to_lt_to_lt ? i)
- [auto|assumption]
+ [autobatch|assumption]
|apply le_exp
[assumption
|apply le_S_S_to_le.
elim (H1 e) 0.
clear H1.
intros (H4 H5).
-auto new.
+autobatch new.
qed.
(*
astepr (e[+]f).
%\begin{convention}% Whenever possible, we will denote the functional construction corresponding to an algebraic operation by the same symbol enclosed in curly braces.
%\end{convention}%
-At this stage, we will always consider automorphisms; we %{\em %could%}% treat this in a more general setting, but we feel that it wouldn't really be a useful effort.
+At this stage, we will always consider autobatchmorphisms; we %{\em %could%}% treat this in a more general setting, but we feel that it wouldn't really be a useful effort.
%\begin{convention}% Let [G:CSemiGroup] and [F,F':(PartFunct G)] and denote by [P] and [Q], respectively, the predicates characterizing their domains.
%\end{convention}%
qed.
-(* Questa coercion composta non e' stata generata automaticamente *)
+(* Questa coercion composta non e' stata generata autobatchmaticamente *)
lemma mycor: ∀S. CSetoid_bin_op S → (S → S → S).
intros;
unfold in c;
letin H40 \def (csf_strext A B g).
unfold in H40.
elim (H10 (csf_fun ? ? g x1) (csf_fun ? ? g x2) (csf_fun ? ? g y1) (csf_fun ? ? g y2) H0);
-[left | right]; auto.
+[left | right]; autobatch.
qed.
definition compose_CSetoid_bin_fun: \forall A, B, C : CSetoid.
right. apply I|intros (a at).simplify. left. apply I]]
simplify.
left.
-auto new|intros 2 (c l).
+autobatch new|intros 2 (c l).
intros 2 (Hy).
elim y 0[
intros 2 (H z).
elim x 0[
intro y.
elim y 0[
- split[simplify.intro.auto new|simplify.intros.exact H1]|
+ split[simplify.intro.autobatch new|simplify.intros.exact H1]|
intros (a at).
simplify.
-split[intro.auto new|intros. exact H1]
+split[intro.autobatch new|intros. exact H1]
]
|
intros (a at IHx).
elim y 0[simplify.
- split[intro.auto new|intros.exact H]
+ split[intro.autobatch new|intros.exact H]
|
intros 2 (c l).
generalize in match (IHx l).
exact (eq_imp_not_ap ? ? ? H).
qed.
-(* Similar for automorphisms. *)
+(* Similar for autobatchmorphisms. *)
record PartFunct (S : CSetoid) : Type \def
{pfdom : S -> Type;
intros.
generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).
-auto.assumption.
+autobatch.assumption.
qed.
lemma Dir_bij : \forall A, B:CSetoid.
apply (eq_to_ap_to_ap ? ? ? ? (H1 ?)).
apply ap_symmetric_unfolded.assumption
|unfold surjective.intros.
- elim f.auto.
+ elim f.autobatch.
]
qed.
apply ap_symmetric_unfolded.
apply (eq_to_ap_to_ap ? ? ? ? (H3 ?)).
apply ap_symmetric_unfolded.assumption|
- intros.auto]
+ intros.autobatch]
qed.
(* End bijections.*)
generalize in match (ap_symmetric S y x). intro.
elim H1. clear H1.
elim H2. clear H2.
-apply H1. unfold. intro. auto.
+apply H1. unfold. intro. autobatch.
qed.
*)
lemma eq_transitive : \forall S : CSetoid. transitive S (cs_eq S).
lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
intros.
-(* perche' auto non arriva in fondo ??? *)
+(* perche' autobatch non arriva in fondo ??? *)
apply (eq_transitive_unfolded ? ? x).
apply eq_symmetric_unfolded.
exact H1.
intro x; intros y H H0.
elim (csp'_strext P x y H).
-auto.
+autobatch.
intro H1.
elimtype False.
intro H1.
elim (H1 H0).
-auto.
+autobatch.
intro H3.
elim H3; intro H4.
-auto.
+autobatch.
elim (ap_irreflexive _ _ H4).
Qed.
generalize (H x x y1 y2 H0); intro H1.
elim H1; intro H2.
-auto.
+autobatch.
elim H2; intro H3.
elim (ap_irreflexive _ _ H3).
-auto.
+autobatch.
Qed.
Lemma Crel_strextarg_imp_strext :
Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
intros H H0 x1 x2 y1 y2 H1.
-elim (H x1 y1 y2 H1); auto.
+elim (H x1 y1 y2 H1); autobatch.
intro H2.
-elim (H0 x1 x2 y2 H2); auto.
+elim (H0 x1 x2 y2 H2); autobatch.
Qed.
*)
red in |- *; intros x y z H H0.
elim (Ccsr_strext R x x y z H).
-auto.
+autobatch.
intro H1; elimtype False.
elim H1; intro H2.
red in |- *; intros x y z H H0.
elim (Ccsr_strext R x z y y H).
-auto.
+autobatch.
intro H1; elimtype False.
elim H1; intro H2.
red in |- *; intros x1 x2 y1 y2 H.
case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
-auto.
+autobatch.
case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
-auto.
+autobatch.
right; right.
apply ap_symmetric_unfolded.
apply eq_symmetric_unfolded.assumption.
apply eq_symmetric_unfolded.assumption.
apply H.
-auto new.
+autobatch new.
qed.
(*
lemma prove_reflect : ∀P:Prop.∀b:bool.
(b = true → P) → (b = false → ¬P) → reflect P b.
-intros 2 (P b); cases b; intros; [left|right] auto.
+intros 2 (P b); cases b; intros; [left|right] autobatch.
qed.
(* ### standard connectives/relations with reflection predicate ### *)
qed.
lemma orbC : ∀a,b. orb a b = orb b a.
-intros (a b); cases a; cases b; auto. qed.
+intros (a b); cases a; cases b; autobatch. qed.
lemma lebP: ∀x,y. reflect (x ≤ y) (leb x y).
intros (x y); generalize in match (leb_to_Prop x y);
qed.
lemma ltb_refl : ∀n.ltb n n = false.
-intros (n); apply (p2bF ? ? (ltbP ? ?)); auto;
+intros (n); apply (p2bF ? ? (ltbP ? ?)); autobatch;
qed.
(* ### = between booleans as <-> in Prop ### *)
lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
intros (n m); apply bool_to_eq; split; intros (H);
-[1:cases (b2pT ? ? (orbP ? ?) H); [2: auto]
- rewrite > (eqb_true_to_eq ? ? H1); auto
+[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch]
+ rewrite > (eqb_true_to_eq ? ? H1); autobatch
|2:cases (b2pT ? ? (lebP ? ?) H);
[ elim n; [reflexivity|assumption]
| simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ]
(* OUT OF PLACE *)
lemma ltW : ∀n,m. n < m → n < (S m).
-intros; unfold lt; unfold lt in H; auto. qed.
+intros; unfold lt; unfold lt in H; autobatch. qed.
lemma ltbW : ∀n,m. ltb n m = true → ltb n (S m) = true.
intros (n m H); letin H1 ≝ (b2pT ? ? (ltbP ? ?) H); clearbody H1;
[2:intros (Hpt); apply H; intros; apply H1; simplify;
generalize in match (refl_eq ? (cmp d x t));
generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b1);
- cases b1; simplify; intros; [2:rewrite > H2] auto.
-|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; auto]
+ cases b1; simplify; intros; [2:rewrite > H2] autobatch.
+|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; autobatch]
rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin]
qed.
generalize in match (refl_eq ? (eqb n p));
generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b); cases b; clear b;
intros (Enp); simplify;
- [2:rewrite > IH; [1,3: auto]
+ [2:rewrite > IH; [1,3: autobatch]
rewrite < ltb_n_Sm in Hm; rewrite > Enp in Hm;
generalize in match Hm; cases (ltb n p); intros; [reflexivity]
simplify in H1; destruct H1;
simplify;
apply f_eq_extensional;
intro;
- auto.
+ autobatch.
qed.
lemma Fmult_zero_f: ∀f:R→R.0·f=0.
simplify;
apply f_eq_extensional;
intro;
- auto.
+ autobatch.
qed.
lemma Fmult_commutative: symmetric ? Fmult.
unfold Fmult;
apply f_eq_extensional;
intros;
- auto.
+ autobatch.
qed.
lemma Fmult_associative: associative ? Fmult.
unfold Fmult;
apply f_eq_extensional;
intros;
- auto.
+ autobatch.
qed.
lemma Fmult_Fplus_distr: distributive ? Fmult Fplus.
apply f_eq_extensional;
intros;
simplify;
- auto.
+ autobatch.
qed.
lemma monomio_product:
[ simplify;
apply f_eq_extensional;
intro;
- auto
+ autobatch
| simplify;
apply f_eq_extensional;
intro;
cut (x\sup (n1+m) = x \sup n1 · x \sup m);
[ rewrite > Hcut;
- auto
+ autobatch
| change in ⊢ (? ? % ?) with ((λx:R.x\sup(n1+m)) x);
rewrite > H;
reflexivity
intros;
elim n;
[ simplify;
- auto
+ autobatch
| simplify;
clear x;
clear H;
[ simplify;
elim m;
[ simplify;
- auto
+ autobatch
| simplify;
rewrite < H;
- auto
+ autobatch
]
| simplify;
rewrite < H;
clear H;
elim n;
[ simplify;
- auto
+ autobatch
| simplify;
- auto
+ autobatch
]
]
].
for @{ 'iff $a $b }.
theorem iff_intro: \forall A,B. (A \to B) \to (B \to A) \to (A \liff B).
- unfold Iff. intros. split; intros; auto.
+ unfold Iff. intros. split; intros; autobatch.
qed.
theorem iff_refl: \forall A. A \liff A.
- intros. apply iff_intro; intros; auto.
+ intros. apply iff_intro; intros; autobatch.
qed.
theorem iff_sym: \forall A,B. A \liff B \to B \liff A.
qed.
theorem iff_trans: \forall A,B,C. A \liff B \to B \liff C \to A \liff C.
- intros. elim H. elim H1. apply iff_intro;intros;auto.
+ intros. elim H. elim H1. apply iff_intro;intros;autobatch.
qed.
elim H1;
split;
intro;
- auto.
+ autobatch.
qed.
(*rewrite > (sym_times p (m/p)).*)
(*rewrite > sym_times.*)
rewrite > assoc_plus.
-auto paramodulation.
+autobatch paramodulation.
rewrite < div_mod.
assumption.
assumption.
theorem div_mod_spec_div_mod:
\forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
-intros.auto.
+intros.autobatch.
(*
apply div_mod_spec_intro.
apply lt_mod_m_m.assumption.
[apply (lt_to_not_le r b H2 Hcut2)
|elim Hcut.assumption
]
- |auto depth=4. apply (trans_le ? ((q1-q)*b))
+ |autobatch depth=4. apply (trans_le ? ((q1-q)*b))
[apply le_times_n.
apply le_SO_minus.exact H6
|rewrite < sym_plus.
|rewrite < sym_times.
rewrite > distr_times_minus.
rewrite > plus_minus
- [auto.
+ [autobatch.
(*
rewrite > sym_times.
rewrite < H5.
apply plus_to_minus.
apply H3
*)
- |auto.
+ |autobatch.
(*
apply le_times_r.
apply lt_to_le.
[rewrite > pi_p_S.
cut (eqb (gcd (S O) n) (S O) = true)
[rewrite > Hcut.
- change with ((gcd n (S O)) = (S O)).auto
- |apply eq_to_eqb_true.auto
+ change with ((gcd n (S O)) = (S O)).autobatch
+ |apply eq_to_eqb_true.autobatch
]
|rewrite > pi_p_S.
apply eqb_elim
|apply mod_O_to_divides
[assumption
|rewrite > distr_times_minus.
- auto
+ autobatch
]
]
]
- |auto
+ |autobatch
]
]
|intro.assumption
|apply mod_O_to_divides
[assumption
|rewrite > distr_times_minus.
- auto
+ autobatch
]
]
]
- |auto
+ |autobatch
]
]
]
[ apply (trans_lt ? (S O));
[ unfold lt; apply le_n;
| apply lt_SO_smallest_factor; assumption; ]
- | letin x \def le.auto new.
+ | letin x \def le.autobatch new.
(*
apply divides_smallest_factor_n;
apply (trans_lt ? (S O));
[ unfold lt; apply le_n;
| assumption; ] *) ] ]
- | auto.
+ | autobatch.
(*
apply prime_to_nth_prime;
apply prime_smallest_factor_n;
cut (prime (nth_prime (max_prime_factor n))).
apply lt_O_nth_prime_n.apply prime_nth_prime.
cut (nth_prime (max_prime_factor n) \divides n).
-auto.
-auto.
+autobatch.
+autobatch.
(*
[ apply (transitive_divides ? n);
[ apply divides_max_prime_factor_n.
assumption.unfold Not.
intro.
cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
- [unfold Not in Hcut1.auto new.
+ [unfold Not in Hcut1.autobatch new.
(*
apply Hcut1.apply divides_to_mod_O;
[ apply lt_O_nth_prime_n.
*)
|letin z \def le.
cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n)));
- [2: rewrite < H1.assumption.|letin x \def le.auto width = 4 depth = 2]
+ [2: rewrite < H1.assumption.|letin x \def le.autobatch width = 4 depth = 2]
(* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
].
(*
absurd (j = (h n1))
[rewrite < H10.
rewrite > H5
- [reflexivity|assumption|auto]
+ [reflexivity|assumption|autobatch]
|apply eqb_false_to_not_eq.
generalize in match H11.
elim (eqb j (h n1))
apply eq_f.
rewrite > sym_plus.
apply plus_minus_m_m.
- auto
+ autobatch
]
]
|intros.
change with ((i/S m) < S n).
apply (lt_times_to_lt_l m).
apply (le_to_lt_to_lt ? i)
- [auto|assumption]
+ [autobatch|assumption]
|apply le_exp
[assumption
|apply le_S_S_to_le.
(a*exp a (card n1 p) * ((S n1) * (pi_p p n1)) =
a*(S n1)*map_iter_p n1 p (\lambda n.a*n) (S O) times).
rewrite < H.
- auto
+ autobatch
|intro.assumption
]
]
apply le_S.
assumption
]
- |apply H2[auto|apply le_n]
+ |apply H2[autobatch|apply le_n]
]
]
]
apply lt_to_not_eq.
apply (le_to_lt_to_lt ? m)
[apply (trans_le ? (m-k))
- [assumption|auto]
+ [assumption|autobatch]
|apply le_S.apply le_n
]
]
|apply not_eq_to_eqb_false.
apply lt_to_not_eq.
- unfold.auto
+ unfold.autobatch
]
]
|apply le_S_S_to_le.assumption
cut (k1 = n1 - (n1 -k1))
[rewrite > Hcut.
apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
- [cut (k1 \le n1)[auto|auto]
+ [cut (k1 \le n1)[autobatch|autobatch]
|assumption
|rewrite < Hcut.assumption
|rewrite < Hcut.intros.
- apply (H9 i H10).unfold.auto
+ apply (H9 i H10).unfold.autobatch
]
|apply sym_eq.
apply plus_to_minus.
- auto.
+ autobatch.
]
|intros.
cut ((S n1) \neq k1)
apply eq_f.
apply (H3 H5)
[elim (le_to_or_lt_eq ? ? H6)
- [auto
+ [autobatch
|absurd (S n1=k2)[apply sym_eq.assumption|assumption]
]
|assumption
[rewrite > map_iter_p_S_false
[apply (H3 H5)
[elim (le_to_or_lt_eq ? ? H6)
- [auto
+ [autobatch
|absurd (S n1=k2)[apply sym_eq.assumption|assumption]
]
|assumption
\forall n,m,p. n - m < p \to n < m + p.
intros 2.
apply (nat_elim2 ? ? ? ? n m)
- [simplify.intros.auto.
+ [simplify.intros.autobatch.
|intros 2.rewrite < minus_n_O.
intro.assumption
|intros.
simplify.
cut (n1 < m1+p)
- [auto
+ [autobatch
|apply H.
apply H1
]
intros.
apply sym_eq.
apply plus_to_minus.
-auto.
+autobatch.
qed.
theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
elim (decidable_n2 p n (S n -m) H4 H6)
[apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
[assumption.
- |unfold.auto.
+ |unfold.autobatch.
|apply le_n
|assumption
|assumption
theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m).
apply nat_elim2
[intro.reflexivity
- |intro.simplify.auto
+ |intro.simplify.autobatch
|intros.simplify.assumption
]
qed.
apply nat_elim2
[intros.apply False_ind.apply (not_le_Sn_O ? H)
|intros.rewrite < minus_n_O.
- auto
+ autobatch
|intros.
generalize in match H2.
apply (nat_case n1)
rewrite > eq_minus_S_pred.
apply lt_pred
[unfold lt.apply le_plus_to_minus_r.applyS H1
- |apply H[auto|assumption]
+ |apply H[autobatch|assumption]
]
]
qed.
include "datatypes/constructors.ma".
include "nat/exp.ma".
include "nat/gcd.ma".
-include "nat/relevant_equations.ma". (* required by auto paramod *)
+include "nat/relevant_equations.ma". (* required by autobatch paramod *)
let rec p_ord_aux p n m \def
match n \mod m with
apply (absurd ? ? H10 H7).
(* rewrite > H6.
rewrite > H8. *)
-auto paramodulation.
+autobatch paramodulation.
unfold prime in H. elim H. assumption.
qed.
apply (lt_to_not_eq O ? H).
rewrite > H7.
rewrite < H10.
- auto
+ autobatch
]
|elim c
[rewrite > sym_gcd.
|apply lt_O_exp.apply lt_to_le.assumption
|rewrite > sym_gcd.
(* hint non trova prime_to_gcd_SO e
- auto non chiude il goal *)
+ autobatch non chiude il goal *)
apply prime_to_gcd_SO
[assumption|assumption]
|assumption
|apply lt_O_exp.apply lt_to_le.assumption
|rewrite > sym_gcd.
(* hint non trova prime_to_gcd_SO e
- auto non chiude il goal *)
+ autobatch non chiude il goal *)
apply prime_to_gcd_SO
[assumption|assumption]
|rewrite > sym_gcd. assumption
apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
apply (H2 O ? ? (S(m1+i))).
-unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.id.
apply (trans_le ? i).assumption.
change with (i \le (S m1)+i).apply le_plus_n.
exact H4.
unfold transitive in H;
unfold symmetric in sym;
intro;
- auto new
+ autobatch new
].
qed.
intro;
unfold transitive in H;
unfold symmetric in sym;
- auto depth=4.
+ autobatch depth=4.
]
qed.
intros;
whd;
intros;
- auto
+ autobatch
].
qed.
intros;
whd;
intro;
- auto
+ autobatch
].
qed.
whd;
unfold impl;
intros;
- auto.
+ autobatch.
qed.
(*DA PORTARE: Add Relation Prop impl
(* impl IS A MORPHISM *)
Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
-unfold impl; tauto.
+unfold impl; tautobatch.
Qed.
(* and IS A MORPHISM *)
Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
- tauto.
+ tautobatch.
Qed.
(* or IS A MORPHISM *)
Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
- tauto.
+ tautobatch.
Qed.
(* not IS A MORPHISM *)
Add Morphism not with signature iff ==> iff as Not_Morphism.
- tauto.
+ tautobatch.
Qed.
(* THE SAME EXAMPLES ON impl *)
Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
Qed.
Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
Qed.
Add Morphism not with signature impl -→ impl as Not_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
Qed.
*)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/Q/q".
+set "baseuri" "cic:/matita/library_autobatch/Q/q".
include "auto/Z/compare.ma".
include "auto/Z/plus.ma".
| elim g
[ apply H2
| apply H3
- | auto
+ | autobatch
(*apply H4.
apply H5*)
]
unfold injective.
intros.
change with ((aux(pp x)) = (aux (pp y))).
-auto.
+autobatch.
(*apply eq_f.
assumption.*)
qed.
unfold injective.
intros.
change with ((aux (nn x)) = (aux (nn y))).
-auto.
+autobatch.
(*apply eq_f.
assumption.*)
qed.
(cons x f) = (cons y g) \to x = y.
intros.
change with ((fhd (cons x f)) = (fhd (cons y g))).
-auto.
+autobatch.
(*apply eq_f.assumption.*)
qed.
(cons x f) = (cons y g) \to f = g.
intros.
change with ((ftl (cons x f)) = (ftl (cons y g))).
-auto.
+autobatch.
(*apply eq_f.assumption.*)
qed.
[ intros.
elim g1
[ elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False))
- [ auto
+ [ autobatch
(*left.
apply eq_f.
assumption*)
| right.
intro.
- auto
+ autobatch
(*apply H.
apply injective_pp.
assumption*)
]
- | auto
+ | autobatch
(*right.
apply not_eq_pp_nn*)
- | auto
+ | autobatch
(*right.
apply not_eq_pp_cons*)
]
[ right.
intro.
apply (not_eq_pp_nn n1 n).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False))
- [ auto
+ [ autobatch
(*left.
apply eq_f.
assumption*)
| right.
intro.
- auto
+ autobatch
(*apply H.
apply injective_nn.
assumption*)
]
- | auto
+ | autobatch
(*right.
apply not_eq_nn_cons*)
]
right.
intro.
apply (not_eq_pp_cons m x f1).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| intros.
right.
intro.
apply (not_eq_nn_cons m x f1).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| intros.
elim H
[ elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False))
- [ auto
+ [ autobatch
(*left.
apply eq_f2;
assumption*)
| right.
intro.
- auto
+ autobatch
(*apply H2.
apply (eq_cons_to_eq1 f1 g1).
assumption*)
]
| right.
intro.
- auto
+ autobatch
(*apply H1.
apply (eq_cons_to_eq2 x y f1 g1).
assumption*)
apply eqb_elim
[ intro.
simplify.
- auto
+ autobatch
(*apply eq_f.
assumption*)
| intro.
simplify.
unfold Not.
intro.
- auto
+ autobatch
(*apply H.
apply injective_pp.
assumption*)
unfold Not.
intro.
apply (not_eq_pp_nn n1 n).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| simplify.
apply eqb_elim
[ intro.
simplify.
- auto
+ autobatch
(*apply eq_f.
assumption*)
| intro.
simplify.
unfold Not.
intro.
- auto
+ autobatch
(*apply H.
apply injective_nn.
assumption*)
unfold Not.
intro.
apply (not_eq_pp_cons m x f1).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| intros.
unfold Not.
intro.
apply (not_eq_nn_cons m x f1).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| intros.
[ simplify.
apply eq_f2
[ assumption
- | (*qui auto non chiude il goal*)
+ | (*qui autobatch non chiude il goal*)
apply H2
]
| simplify.
unfold Not.
intro.
apply H2.
- auto
+ autobatch
(*apply (eq_cons_to_eq2 x y).
assumption*)
]
simplify.
unfold Not.
intro.
- auto
+ autobatch
(*apply H1.
apply (eq_cons_to_eq1 f1 g1).
assumption*)
[ intros.
elim g
[ change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
- auto
+ autobatch
(*apply eq_f.
apply sym_Zplus*)
| change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
- auto
+ autobatch
(*apply eq_f.
apply sym_Zplus*)
| change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
- auto
+ autobatch
(*rewrite < sym_Zplus.
reflexivity*)
]
| intros.
elim g
[ change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
- auto
+ autobatch
(*apply eq_f.
apply sym_Zplus*)
| change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)).
- auto
+ autobatch
(*apply eq_f.
apply sym_Zplus*)
| change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
- auto
+ autobatch
(*rewrite < sym_Zplus.
reflexivity*)
]
| intros.
change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
- auto
+ autobatch
(*rewrite < sym_Zplus.
reflexivity*)
| intros.
change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
- auto
+ autobatch
(*rewrite < sym_Zplus.
reflexivity*)
| intros.
intro.
elim f
[ change with (Z_to_ratio (pos n + - (pos n)) = one).
- auto
+ autobatch
(*rewrite > Zplus_Zopp.
reflexivity*)
| change with (Z_to_ratio (neg n + - (neg n)) = one).
- auto
+ autobatch
(*rewrite > Zplus_Zopp.
reflexivity*)
|
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/Z/compare".
+set "baseuri" "cic:/matita/library_autobatch/Z/compare".
include "auto/Z/orders.ma".
include "auto/nat/compare.ma".
unfold Not.
intro.
apply (not_eq_OZ_pos n).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| simplify.
apply eqb_elim
[ intro.
simplify.
- auto
+ autobatch
(*apply eq_f.
assumption*)
| intro.
simplify.
unfold Not.
intro.
- auto
+ autobatch
(*apply H.
apply inj_pos.
assumption*)
unfold Not.
intro.
apply (not_eq_OZ_neg n).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| simplify.
unfold Not.
intro.
apply (not_eq_pos_neg n1 n).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| simplify.
apply eqb_elim
[ intro.
simplify.
- auto
+ autobatch
(*apply eq_f.
assumption*)
| intro.
simplify.
unfold Not.
intro.
- auto
+ autobatch
(*apply H.
apply inj_neg.
assumption*)
[ true \Rightarrow x=y
| false \Rightarrow x \neq y] \to P (eqZb x y))
[ apply Hcut.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
apply eqZb_to_Prop
| elim (eqZb)
- [ (*NB qui auto non chiude il goal*)
+ [ (*NB qui autobatch non chiude il goal*)
apply (H H2)
- | (*NB qui auto non chiude il goal*)
+ | (*NB qui autobatch non chiude il goal*)
apply (H1 H2)
]
]
| EQ \Rightarrow pos n = pos n1
| GT \Rightarrow (S n1) \leq n])
[ apply Hcut.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
apply nat_compare_to_Prop
| elim (nat_compare n n1)
[ simplify.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
exact H
| simplify.
apply eq_f.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
exact H
| simplify.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
exact H
]
]
| EQ \Rightarrow neg n = neg n1
| GT \Rightarrow (S n) \leq n1])
[ apply Hcut.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
apply nat_compare_to_Prop
| elim (nat_compare n1 n)
[ simplify.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
exact H
| simplify.
apply eq_f.
apply sym_eq.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
exact H
| simplify.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
exact H
]
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/Z/orders".
+set "baseuri" "cic:/matita/library_autobatch/Z/orders".
include "auto/Z/z.ma".
include "auto/nat/orders.ma".
| (neg m) \Rightarrow m \leq n ]].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/library_auto/Z/orders/Zle.con x y).
+interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/library_autobatch/Z/orders/Zle.con x y).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "integer 'neither less nor equal to'" 'nleq x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/Z/orders/Zle.con x y)).
+ (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/Z/orders/Zle.con x y)).
definition Zlt : Z \to Z \to Prop \def
\lambda x,y:Z.
| (neg m) \Rightarrow m<n ]].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less than'" 'lt x y = (cic:/matita/library_auto/Z/orders/Zlt.con x y).
+interpretation "integer 'less than'" 'lt x y = (cic:/matita/library_autobatch/Z/orders/Zlt.con x y).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "integer 'not less than'" 'nless x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/Z/orders/Zlt.con x y)).
+ (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/Z/orders/Zlt.con x y)).
theorem irreflexive_Zlt: irreflexive Z Zlt.
unfold irreflexive.
unfold Not.
intro.
elim x
-[ (*qui auto non chiude il goal*)
+[ (*qui autobatch non chiude il goal*)
exact H
| cut (neg n < neg n \to False)
[ apply Hcut.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply H
- | auto
+ | autobatch
(*simplify.
unfold lt.
apply not_le_Sn_n*)
]
| cut (pos n < pos n \to False)
[ apply Hcut.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply H
- | auto
+ | autobatch
(*simplify.
unfold lt.
apply not_le_Sn_n*)
theorem Zlt_neg_neg_to_lt:
\forall n,m:nat. neg n < neg m \to m < n.
intros.
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
apply H.
qed.
theorem Zlt_pos_pos_to_lt:
\forall n,m:nat. pos n < pos m \to n < m.
intros.
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
apply H.
qed.
elim x
[ (* goal: x=OZ *)
cut (OZ < y \to Zsucc OZ \leq y)
- [ auto
+ [ autobatch
(*apply Hcut.
assumption*)
| simplify.
elim y
[ simplify.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
exact H1
| simplify.
apply le_O_n
| simplify.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
exact H1
]
]
exact H
| (* goal: x=neg *)
cut (neg n < y \to Zsucc (neg n) \leq y)
- [ auto
+ [ autobatch
(*apply Hcut.
assumption*)
| elim n
[ cut (neg O < y \to Zsucc (neg O) \leq y)
- [ auto
+ [ autobatch
(*apply Hcut.
assumption*)
| simplify.
| simplify.
exact I
| simplify.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply (not_le_Sn_O n1 H2)
]
]
| cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y)
- [ auto
+ [ autobatch
(*apply Hcut.
assumption*)
| simplify.
| simplify.
exact I
| simplify.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply (le_S_S_to_le n2 n1 H3)
]
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/Z/plus".
+set "baseuri" "cic:/matita/library_autobatch/Z/plus".
include "auto/Z/z.ma".
include "auto/nat/minus.ma".
| (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer plus" 'plus x y = (cic:/matita/library_auto/Z/plus/Zplus.con x y).
+interpretation "integer plus" 'plus x y = (cic:/matita/library_autobatch/Z/plus/Zplus.con x y).
theorem Zplus_z_OZ: \forall z:Z. z+OZ = z.
intro.
-elim z;auto.
+elim z;autobatch.
(*simplify;reflexivity.*)
qed.
theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
intros.
elim x
-[ auto
+[ autobatch
(*rewrite > Zplus_z_OZ.
reflexivity*)
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| simplify.
- auto
+ autobatch
(*rewrite < plus_n_Sm.
rewrite < plus_n_Sm.
rewrite < sym_plus.
| simplify.
rewrite > nat_compare_n_m_m_n.
simplify.
- elim nat_compare;auto
+ elim nat_compare;autobatch
(*[ simplify.
reflexivity
| simplify.
]*)
]
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| simplify.
rewrite > nat_compare_n_m_m_n.
simplify.
- elim nat_compare;auto
+ elim nat_compare;autobatch
(*[ simplify.
reflexivity
| simplify.
reflexivity
]*)
| simplify.
- auto
+ autobatch
(*rewrite < plus_n_Sm.
rewrite < plus_n_Sm.
rewrite < sym_plus.
theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
intros.
elim z
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
-| elim n;auto
+| elim n;autobatch
(*[ simplify.
reflexivity
| simplify.
theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z.
intros.
elim z
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
-| auto
+| autobatch
(*simplify.
reflexivity*)
-| elim n;auto
+| elim n;autobatch
(*[ simplify.
reflexivity
| simplify.
\forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
intros.
elim n
-[ elim m;auto
+[ elim m;autobatch
(*[ simplify.
reflexivity
| simplify.
reflexivity
]*)
| elim m
- [ auto
+ [ autobatch
(*simplify.
rewrite < plus_n_Sm.
rewrite < plus_n_O.
reflexivity*)
| simplify.
- auto
+ autobatch
(*rewrite < plus_n_Sm.
rewrite < plus_n_Sm.
reflexivity*)
\forall n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
intros.
elim n
-[ elim m;auto
+[ elim m;autobatch
(*[ simplify.
reflexivity
| simplify.
reflexivity
]*)
-| elim m;auto
+| elim m;autobatch
(*[ simplify.
reflexivity
| simplify.
\forall n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
intros.
elim n
-[ auto
+[ autobatch
(*elim m
[ simplify.
reflexivity
reflexivity
]*)
| elim m
- [ auto
+ [ autobatch
(*simplify.
rewrite > plus_n_Sm.
reflexivity*)
| simplify.
- auto
+ autobatch
(*rewrite > plus_n_Sm.
reflexivity*)
]
\forall x,y. x+y = (Zsucc x)+(Zpred y).
intros.
elim x
-[ auto
+[ autobatch
(*elim y
[ simplify.
reflexivity
| simplify.
reflexivity
]*)
-| elim y;auto
+| elim y;autobatch
(*[ simplify.
reflexivity
| apply Zplus_pos_pos
| apply Zplus_pos_neg
]*)
-| elim y;auto
+| elim y;autobatch
(*[ rewrite < sym_Zplus.
rewrite < (sym_Zplus (Zpred OZ)).
rewrite < Zpred_Zplus_neg_O.
apply (nat_elim2
(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
[ intro.
- elim n1;auto
+ elim n1;autobatch
(*[ simplify.
reflexivity
| elim n2; simplify; reflexivity
]*)
| intros.
- auto
+ autobatch
(*elim n1;simplify;reflexivity*)
| intros.
rewrite < (Zplus_pos_neg ? m1).
apply (nat_elim2
(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
[ intros.
- auto
+ autobatch
(*elim n1
[ simplify.
reflexivity
| elim n2;simplify;reflexivity
]*)
| intros.
- auto
+ autobatch
(*elim n1;simplify;reflexivity*)
| intros.
- auto.
+ autobatch.
(*rewrite < (Zplus_neg_neg ? m1).
reflexivity*)
]
apply (nat_elim2
(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)))
[ intros.
- auto
+ autobatch
(*elim n1
[ simplify.
reflexivity
| elim n2;simplify;reflexivity
]*)
| intros.
- auto
+ autobatch
(*elim n1;simplify;reflexivity*)
| intros.
- auto
+ autobatch
(*rewrite < H.
rewrite < (Zplus_neg_pos ? (S m1)).
reflexivity*)
theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y).
intros.
elim x
-[ auto
+[ autobatch
(*elim y
[ simplify.
reflexivity
| rewrite < Zsucc_Zplus_pos_O.
reflexivity
]*)
-| elim y;auto
+| elim y;autobatch
(*[ rewrite < (sym_Zplus OZ).
reflexivity
| apply Zplus_Zsucc_pos_pos
| apply Zplus_Zsucc_pos_neg
]*)
-| elim y;auto
+| elim y;autobatch
(*[ rewrite < sym_Zplus.
rewrite < (sym_Zplus OZ).
simplify.
theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
intros.
-cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y));auto.
+cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y));autobatch.
(*[ rewrite > Hcut.
rewrite > Zplus_Zsucc.
rewrite > Zpred_Zsucc.
(* simplify. *)
intros.
elim x
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| elim n
[ rewrite < Zsucc_Zplus_pos_O.
- auto
+ autobatch
(*rewrite < Zsucc_Zplus_pos_O.
rewrite > Zplus_Zsucc.
reflexivity*)
| rewrite > (Zplus_Zsucc (pos n1)).
rewrite > (Zplus_Zsucc (pos n1)).
- auto
+ autobatch
(*rewrite > (Zplus_Zsucc ((pos n1)+y)).
apply eq_f.
assumption*)
]
| elim n
[ rewrite < (Zpred_Zplus_neg_O (y+z)).
- auto
+ autobatch
(*rewrite < (Zpred_Zplus_neg_O y).
rewrite < Zplus_Zpred.
reflexivity*)
| rewrite > (Zplus_Zpred (neg n1)).
rewrite > (Zplus_Zpred (neg n1)).
- auto
+ autobatch
(*rewrite > (Zplus_Zpred ((neg n1)+y)).
apply eq_f.
assumption*)
| (neg n) \Rightarrow (pos n) ].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer unary minus" 'uminus x = (cic:/matita/library_auto/Z/plus/Zopp.con x).
+interpretation "integer unary minus" 'uminus x = (cic:/matita/library_autobatch/Z/plus/Zopp.con x).
theorem Zopp_Zplus: \forall x,y:Z. -(x+y) = -x + -y.
intros.
elim x
-[ elim y;auto
+[ elim y;autobatch
(*simplify;reflexivity*)
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
- | auto
+ | autobatch
(*simplify.
reflexivity*)
| simplify.
apply nat_compare_elim;
- intro;auto (*simplify;reflexivity*)
+ intro;autobatch (*simplify;reflexivity*)
]
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| simplify.
apply nat_compare_elim;
- intro;auto
+ intro;autobatch
(*simplify;reflexivity*)
- | auto
+ | autobatch
(*simplify.
reflexivity*)
]
[ apply refl_eq
| simplify.
rewrite > nat_compare_n_n.
- auto
+ autobatch
(*simplify.
apply refl_eq*)
| simplify.
rewrite > nat_compare_n_n.
- auto
+ autobatch
(*simplify.
apply refl_eq*)
]
(* minus *)
definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
-interpretation "integer minus" 'minus x y = (cic:/matita/library_auto/Z/plus/Zminus.con x y).
+interpretation "integer minus" 'minus x y = (cic:/matita/library_autobatch/Z/plus/Zminus.con x y).
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/Z/times".
+set "baseuri" "cic:/matita/library_autobatch/Z/times".
include "auto/nat/lt_arith.ma".
include "auto/Z/plus.ma".
| (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer times" 'times x y = (cic:/matita/library_auto/Z/times/Ztimes.con x y).
+interpretation "integer times" 'times x y = (cic:/matita/library_autobatch/Z/times/Ztimes.con x y).
theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
intro.
-elim z;auto.
+elim z;autobatch.
(*simplify;reflexivity.*)
qed.
theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
neg n * x = - (pos n * x).
intros.
-elim x;auto.
+elim x;autobatch.
(*simplify;reflexivity.*)
qed.
change with (\forall x,y:Z. x*y = y*x).
intros.
elim x
-[ auto
+[ autobatch
(*rewrite > Ztimes_z_OZ.
reflexivity*)
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
- auto
+ autobatch
(*rewrite < sym_times.
reflexivity*)
| change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
- auto
+ autobatch
(*rewrite < sym_times.
reflexivity*)
]
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
- auto
+ autobatch
(*rewrite < sym_times.
reflexivity*)
| change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
- auto
+ autobatch
(*rewrite < sym_times.
reflexivity*)
]
unfold associative.
intros.
elim x
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| elim z
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with
(pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
(neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
]
]
| elim z
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with
(neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
(pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
]
]
| elim y
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| elim z
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with
(neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
(pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
]
]
| elim z
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| change with
(pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
(neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred
- [ rewrite < S_pred;auto
+ [ rewrite < S_pred;autobatch
(*[ rewrite < assoc_times.
reflexivity
| apply lt_O_times_S_S
intros.
rewrite < S_pred
[ rewrite > minus_pred_pred
- [ auto
+ [ autobatch
(*rewrite < distr_times_minus.
reflexivity*)
| apply lt_O_times_S_S
| apply lt_O_times_S_S
]
-| unfold lt.auto
+| unfold lt.autobatch
(*simplify.
unfold lt.
apply le_SO_minus.
rewrite < (times_minus1 n q p H).
reflexivity
| intro.
- auto
+ autobatch
(*rewrite < H.
simplify.
reflexivity*)
lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
(pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
intros.
-auto.
+autobatch.
(*rewrite < sym_Zplus.
rewrite > Ztimes_Zplus_pos_neg_pos.
apply sym_Zplus.*)
| change with
(pos (pred ((S n) * ((S n1) + (S n2)))) =
pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
- auto
+ autobatch
(*rewrite < distr_times_plus.
reflexivity*)
| apply Ztimes_Zplus_pos_pos_neg
| change with
(neg (pred ((S n) * ((S n1) + (S n2)))) =
neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
- auto
+ autobatch
(*rewrite < distr_times_plus.
reflexivity*)
]
intros.
rewrite > Ztimes_neg_Zopp.
rewrite > distr_Ztimes_Zplus_pos.
-auto.
+autobatch.
(*rewrite > Zopp_Zplus.
rewrite < Ztimes_neg_Zopp.
rewrite < Ztimes_neg_Zopp.
theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
intros.
-elim x;auto.
+elim x;autobatch.
(*[ simplify.
reflexivity
| apply distr_Ztimes_Zplus_pos
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/Z/z".
+set "baseuri" "cic:/matita/library_autobatch/Z/z".
include "datatypes/bool.ma".
include "auto/nat/nat.ma".
[ O \Rightarrow OZ
| (S n)\Rightarrow pos n].
-coercion cic:/matita/library_auto/Z/z/Z_of_nat.con.
+coercion cic:/matita/library_autobatch/Z/z/Z_of_nat.con.
definition neg_Z_of_nat \def
\lambda n. match n with
|false \Rightarrow z \neq OZ].
intros.
elim z
-[ (*qui auto non chiude il goal*)
+[ (*qui autobatch non chiude il goal*)
simplify.
reflexivity
| simplify.
unfold Not.
intros (H).
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
destruct H
| simplify.
unfold Not.
intros (H).
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
destruct H
]
qed.
intros.
apply inj_S.
change with (abs (pos x) = abs (pos y)).
-auto.
+autobatch.
(*apply eq_f.
assumption.*)
qed.
intros.
apply inj_S.
change with (abs (neg x) = abs (neg y)).
-auto.
+autobatch.
(*apply eq_f.
assumption.*)
qed.
theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
unfold Not.
intros (n H).
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
destruct H.
qed.
theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
unfold Not.
intros (n H).
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
destruct H.
qed.
theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
unfold Not.
intros (n m H).
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
destruct H.
qed.
[ (* goal: x=OZ *)
elim y
[ (* goal: x=OZ y=OZ *)
- auto
+ autobatch
(*left.
reflexivity*)
| (* goal: x=OZ 2=2 *)
- auto
+ autobatch
(*right.
apply not_eq_OZ_pos*)
| (* goal: x=OZ 2=3 *)
- auto
+ autobatch
(*right.
apply not_eq_OZ_neg*)
]
unfold Not.
intro.
apply (not_eq_OZ_pos n).
- auto
+ autobatch
(*symmetry.
assumption*)
| (* goal: x=pos y=pos *)
elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False)))
- [ auto
+ [ autobatch
(*left.
apply eq_f.
assumption*)
| right.
unfold Not.
intros (H_inj).
- auto
+ autobatch
(*apply H.
destruct H_inj.
assumption*)
]
| (* goal: x=pos y=neg *)
- auto
+ autobatch
(*right.
unfold Not.
intro.
unfold Not.
intro.
apply (not_eq_OZ_neg n).
- auto
+ autobatch
(*symmetry.
assumption*)
| (* goal: x=neg y=pos *)
unfold Not.
intro.
apply (not_eq_pos_neg n1 n).
- auto
+ autobatch
(*symmetry.
assumption*)
| (* goal: x=neg y=neg *)
elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False)))
- [ auto
+ [ autobatch
(*left.
apply eq_f.
assumption*)
| right.
unfold Not.
intro.
- auto
+ autobatch
(*apply H.
apply injective_neg.
assumption*)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/chinese_reminder".
+set "baseuri" "cic:/matita/library_autobatch/nat/chinese_reminder".
include "auto/nat/exp.ma".
include "auto/nat/gcd.ma".
rewrite < assoc_times.
rewrite < times_plus_l.
rewrite > eq_minus_plus_plus_minus
- [ auto
+ [ autobatch
(*rewrite < times_minus_l.
rewrite > sym_plus.
apply (eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2))
| apply le_times_l.
apply (trans_le ? ((a+b*m)*a2))
[ apply le_times_l.
- apply (trans_le ? (b*m));auto
+ apply (trans_le ? (b*m));autobatch
(*[ rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
assumption
[ apply lt_to_le.
change with (O + a2*m < a1*n).
apply lt_minus_to_plus.
- auto
+ autobatch
(*rewrite > H5.
unfold lt.
apply le_n*)
rewrite > distr_times_minus.
rewrite < assoc_times.
rewrite < eq_plus_minus_minus_minus
- [ auto
+ [ autobatch
(*rewrite < times_n_SO.
rewrite < times_minus_l.
rewrite < sym_plus.
]*)
| rewrite > assoc_times.
apply le_times_r.
- (*auto genera un'esecuzione troppo lunga*)
- apply (trans_le ? (a1*n - a2*m));auto
+ (*autobatch genera un'esecuzione troppo lunga*)
+ apply (trans_le ? (a1*n - a2*m));autobatch
(*[ rewrite > H5.
apply le_n
| apply (le_minus_m ? (a2*m))
]*)
| apply le_times_l.
apply le_times_l.
- auto
+ autobatch
(*apply (trans_le ? (b*m))
[ rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
[ apply lt_to_le.
change with (O + a2*m < a1*n).
apply lt_minus_to_plus.
- auto
+ autobatch
(*rewrite > H5.
unfold lt.
apply le_n*)
rewrite > distr_times_minus.
rewrite < assoc_times.
rewrite < eq_plus_minus_minus_minus
- [ auto
+ [ autobatch
(*rewrite < times_n_SO.
rewrite < times_minus_l.
rewrite < sym_plus.
]*)
| rewrite > assoc_times.
apply le_times_r.
- apply (trans_le ? (a2*m - a1*n));auto
+ apply (trans_le ? (a2*m - a1*n));autobatch
(*[ rewrite > H5.
apply le_n
| apply (le_minus_m ? (a1*n))
| rewrite > assoc_times.
rewrite > assoc_times.
apply le_times_l.
- auto
+ autobatch
(*apply (trans_le ? (a*n))
[ rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
[ apply lt_to_le.
change with (O + a1*n < a2*m).
apply lt_minus_to_plus.
- auto
+ autobatch
(*rewrite > H5.
unfold lt.
apply le_n*)
rewrite > assoc_plus.
rewrite < times_plus_l.
rewrite > eq_minus_plus_plus_minus
- [ auto
+ [ autobatch
(*rewrite < times_minus_l.
rewrite > sym_plus.
apply (eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1))
| apply le_times_l.
apply (trans_le ? ((b+a*n)*a1))
[ apply le_times_l.
- auto
+ autobatch
(*apply (trans_le ? (a*n))
[ rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
[ apply lt_to_le.
change with (O + a1*n < a2*m).
apply lt_minus_to_plus.
- auto
+ autobatch
(*rewrite > H5.
unfold lt.
apply le_n*)
]
]
(* proof of the cut *)
-| (* qui auto non conclude il goal *)
+| (* qui autobatch non conclude il goal *)
rewrite < H2.
apply eq_minus_gcd
]
apply sym_eq.
change with (congruent a1 (a1 \mod (m*n)) m).
rewrite < sym_times.
- auto
+ autobatch
(*apply congruent_n_mod_times;assumption*)
| assumption
]
[ unfold congruent.
apply sym_eq.
change with (congruent a1 (a1 \mod (m*n)) n).
- auto
+ autobatch
(*apply congruent_n_mod_times;assumption*)
| assumption
]
]
| apply lt_mod_m_m.
- auto
+ autobatch
(*rewrite > (times_n_O O).
apply lt_times;assumption*)
]
qed.
theorem cr_pair2: cr_pair (S(S O)) (S(S(S O))) (S O) O = (S(S(S O))).
-auto.
+autobatch.
(*simplify.
reflexivity.*)
qed.
[ rewrite > H3.
simplify.
intro.
- auto
+ autobatch
(*split
[ reflexivity
| apply eqb_true_to_eq.
]*)
| simplify.
intro.
- (* l'invocazione di auto qui genera segmentation fault *)
+ (* l'invocazione di autobatch qui genera segmentation fault *)
apply False_ind.
- (* l'invocazione di auto qui genera segmentation fault *)
+ (* l'invocazione di autobatch qui genera segmentation fault *)
apply not_eq_true_false.
- (* l'invocazione di auto qui genera segmentation fault *)
+ (* l'invocazione di autobatch qui genera segmentation fault *)
apply sym_eq.
assumption
]
[ apply (ex_intro ? ? a1).
split
[ split
- [ auto
+ [ autobatch
(*rewrite < minus_n_n.
apply le_O_n*)
| elim H3.
| apply (nat_case (m*n))
[ apply le_O_n
| intro.
- auto
+ autobatch
(*rewrite < pred_Sn.
apply le_n*)
]
[ cut (a1 \mod n = b)
[ rewrite > (eq_to_eqb_true ? ? Hcut).
rewrite > (eq_to_eqb_true ? ? Hcut1).
- (* l'invocazione di auto qui non chiude il goal *)
+ (* l'invocazione di autobatch qui non chiude il goal *)
simplify.
reflexivity
| rewrite < (lt_to_eq_mod b n);
| rewrite < (lt_to_eq_mod a m);assumption
]
]
- | auto
+ | autobatch
(*apply (le_to_lt_to_lt ? b)
[ apply le_O_n
| assumption
]*)
- | auto
+ | autobatch
(*apply (le_to_lt_to_lt ? a)
[ apply le_O_n
| assumption
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/compare".
+set "baseuri" "cic:/matita/library_autobatch/nat/compare".
include "datatypes/bool.ma".
include "datatypes/compare.ma".
[ true \Rightarrow n = m
| false \Rightarrow n \neq m]))
[ intro.
- elim n1;simplify;auto
+ elim n1;simplify;autobatch
(*[ simplify
reflexivity
| simplify.
unfold Not.
intro.
apply (not_eq_O_S n1).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| intros.
| unfold Not.
intro.
apply H1.
- auto
+ autobatch
(*apply inj_S.
assumption*)
]
[ true \Rightarrow n = m
| false \Rightarrow n \neq m] \to (P (eqb n m)))
[ apply Hcut.
- (* qui auto non conclude il goal*)
+ (* qui autobatch non conclude il goal*)
apply eqb_to_Prop
| elim (eqb n m)
- [ (*qui auto non conclude il goal*)
+ [ (*qui autobatch non conclude il goal*)
apply ((H H2))
- | (*qui auto non conclude il goal*)
+ | (*qui autobatch non conclude il goal*)
apply ((H1 H2))
]
]
theorem eqb_n_n: \forall n. eqb n n = true.
intro.
-elim n;simplify;auto.
+elim n;simplify;autobatch.
(*[ simplify.reflexivity
| simplify.assumption.
]*)
[ true \Rightarrow n = m
| false \Rightarrow n \neq m].
rewrite < H.
-(*qui auto non conclude il goal*)
+(*qui autobatch non conclude il goal*)
apply eqb_to_Prop.
qed.
[ true \Rightarrow n = m
| false \Rightarrow n \neq m].
rewrite < H.
-(*qui auto non conclude il goal*)
+(*qui autobatch non conclude il goal*)
apply eqb_to_Prop.
qed.
theorem eq_to_eqb_true: \forall n,m:nat.
n = m \to eqb n m = true.
intros.
-auto.
+autobatch.
(*apply (eqb_elim n m)
[ intros. reflexivity
| intros.apply False_ind.apply (H1 H)
simplify.
elim ((leb n1 m1));simplify
[ apply le_S_S.
- (*qui auto non conclude il goal*)
+ (*qui autobatch non conclude il goal*)
apply H
| unfold Not.
intros.
apply H.
- auto
+ autobatch
(*apply le_S_S_to_le.
assumption*)
]
[ true \Rightarrow n \leq m
| false \Rightarrow n \nleq m] \to (P (leb n m)))
[ apply Hcut.
- (*qui auto non conclude il goal*)
+ (*qui autobatch non conclude il goal*)
apply leb_to_Prop
| elim (leb n m)
- [ (*qui auto non conclude il goal*)
+ [ (*qui autobatch non conclude il goal*)
apply ((H H2))
- | (*qui auto non conclude il goal*)
+ | (*qui autobatch non conclude il goal*)
apply ((H1 H2))
]
]
(**********)
theorem nat_compare_n_n: \forall n:nat. nat_compare n n = EQ.
intro.elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| simplify.
theorem nat_compare_S_S: \forall n,m:nat.
nat_compare n m = nat_compare (S n) (S m).
-intros.auto.
+intros.autobatch.
(*simplify.reflexivity.*)
qed.
theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
intro.
-elim n;auto.
+elim n;autobatch.
(*[ apply False_ind.
exact (not_le_Sn_O O H)
| apply eq_f.
apply (lt_O_n_elim n H).
apply (lt_O_n_elim m H1).
intros.
-auto.
+autobatch.
(*simplify.reflexivity.*)
qed.
| EQ \Rightarrow n=m
| GT \Rightarrow m < n ]))
[ intro.
- elim n1;simplify;auto
+ elim n1;simplify;autobatch
(*[ reflexivity
| unfold lt.
apply le_S_S.
]*)
| intro.
simplify.
- auto
+ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
elim ((nat_compare n1 m1));simplify
[ unfold lt.
apply le_S_S.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply H
| apply eq_f.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply H
| unfold lt.
apply le_S_S.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply H
]
]
nat_compare n m = compare_invert (nat_compare m n).
intros.
apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n)));intros
-[ elim n1;auto(*;simplify;reflexivity*)
-| elim n1;auto(*;simplify;reflexivity*)
-| auto
+[ elim n1;autobatch(*;simplify;reflexivity*)
+| elim n1;autobatch(*;simplify;reflexivity*)
+| autobatch
(*simplify.elim H.reflexivity*)
]
qed.
| GT \Rightarrow m < n] \to
(P (nat_compare n m)))
[ apply Hcut.
- (*auto non chiude il goal*)
+ (*autobatch non chiude il goal*)
apply nat_compare_to_Prop
| elim ((nat_compare n m))
- [ (*auto non chiude il goal*)
+ [ (*autobatch non chiude il goal*)
apply ((H H3))
- | (*auto non chiude il goal*)
+ | (*autobatch non chiude il goal*)
apply ((H1 H3))
- | (*auto non chiude il goal*)
+ | (*autobatch non chiude il goal*)
apply ((H2 H3))
]
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/congruence".
+set "baseuri" "cic:/matita/library_autobatch/nat/congruence".
include "auto/nat/relevant_equations.ma".
include "auto/nat/primes.ma".
\lambda n,m,p:nat. mod n p = mod m p.
interpretation "congruent" 'congruent n m p =
- (cic:/matita/library_auto/nat/congruence/congruent.con n m p).
+ (cic:/matita/library_autobatch/nat/congruence/congruent.con n m p).
notation < "hvbox(n break \cong\sub p m)"
(*non associative*) with precedence 45
intros.
whd.
apply (trans_eq ? ? (y \mod p))
-[ (*qui auto non chiude il goal*)
+[ (*qui autobatch non chiude il goal*)
apply H
-| (*qui auto non chiude il goal*)
+| (*qui autobatch non chiude il goal*)
apply H1
]
qed.
theorem le_to_mod: \forall n,m:nat. n \lt m \to n = n \mod m.
intros.
-auto.
+autobatch.
(*apply (div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
[ constructor 1
[ assumption
theorem mod_mod : \forall n,p:nat. O<p \to n \mod p = (n \mod p) \mod p.
intros.
-auto.
+autobatch.
(*rewrite > (div_mod (n \mod p) p) in \vdash (? ? % ?)
[ rewrite > (eq_div_O ? p)
[ reflexivity
intros.
apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p)
(n/(m*p)*m + (n \mod (m*p)/p)))
-[ auto.
+[ autobatch.
(*apply div_mod_spec_div_mod.
assumption*)
| constructor 1
- [ auto
+ [ autobatch
(*apply lt_mod_m_m.
assumption*)
| rewrite > times_plus_l.
rewrite > assoc_plus.
rewrite < div_mod
[ rewrite > assoc_times.
- rewrite < div_mod;auto
+ rewrite < div_mod;autobatch
(*[ reflexivity
| rewrite > (times_n_O O).
apply lt_times;assumption
\forall n,p:nat. O < p \to congruent n (n \mod p) p.
intros.
unfold congruent.
-auto.
+autobatch.
(*apply mod_mod.
assumption.*)
qed.
intros.
unfold congruent.
apply (div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
-[ auto
+[ autobatch
(*apply div_mod_spec_div_mod.
assumption*)
| constructor 1
- [ auto
+ [ autobatch
(*apply lt_mod_m_m.
assumption*)
|
(*rewrite > (sym_times p (m/p)).*)
(*rewrite > sym_times.*)
rewrite > assoc_plus.
- auto paramodulation.
+ autobatch paramodulation.
rewrite < div_mod.
assumption.
assumption.
apply (eq_times_plus_to_congruent n m p n2)
[ assumption
| rewrite < sym_plus.
- apply minus_to_plus;auto
+ apply minus_to_plus;autobatch
(*[ assumption
| rewrite > sym_times. assumption
]*)
rewrite > (div_mod n p) in \vdash (? ? % ?)
[ rewrite > (div_mod m p) in \vdash (? ? % ?)
[ rewrite < (sym_plus (m \mod p)).
- auto
+ autobatch
(*rewrite < H1.
rewrite < (eq_minus_minus_minus_plus ? (n \mod p)).
rewrite < minus_plus_m_m.
((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p)))
[ assumption
| apply (trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
- [ apply eq_f2;auto(*;apply div_mod.assumption.*)
+ [ apply eq_f2;autobatch(*;apply div_mod.assumption.*)
| apply (trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
(n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
[ apply times_plus_plus
| apply eq_f2
[ rewrite < assoc_times.
- auto
+ autobatch
(*rewrite > (assoc_times (n/p) p (m \mod p)).
rewrite > (sym_times p (m \mod p)).
rewrite < (assoc_times (n/p) (m \mod p) p).
rewrite > (mod_times n m p H).
rewrite > H1.
rewrite > H2.
-auto.
+autobatch.
(*
apply sym_eq.
apply mod_times.
congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
intros.
elim n;simplify
-[ auto
+[ autobatch
(*apply congruent_n_mod_n.
assumption*)
| apply congruent_times
[ assumption
- | auto
+ | autobatch
(*apply congruent_n_mod_n.
assumption*)
| (*NB: QUI AUTO NON RIESCE A CHIUDERE IL GOAL*)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/count".
+set "baseuri" "cic:/matita/library_autobatch/nat/count".
include "auto/nat/relevant_equations.ma".
include "auto/nat/sigma_and_pi.ma".
elim n;simplify
[ reflexivity
| rewrite > H.
- auto
+ autobatch
(*rewrite > assoc_plus.
rewrite < (assoc_plus (g (S (n1+m)))).
rewrite > (sym_plus (g (S (n1+m)))).
sigma (S (p+n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
intros.
elim p;simplify
-[ auto
+[ autobatch
(*rewrite < (sym_plus n m).
reflexivity*)
| rewrite > assoc_plus in \vdash (? ? ? %).
rewrite < H.
- auto
+ autobatch
(*simplify.
rewrite < plus_n_Sm.
rewrite > (sym_plus n).
| rewrite > assoc_plus in \vdash (? ? ? %).
rewrite < H.
rewrite < plus_n_Sm.
- auto
+ autobatch
(*rewrite < plus_n_Sm.simplify.
rewrite < (sym_plus n).
rewrite > assoc_plus.
| rewrite > sigma_f_g.
rewrite < plus_n_O.
rewrite < H.
- auto
+ autobatch
(*rewrite > (S_pred ((S n1)*(S m)))
[ apply sigma_plus1
theorem bool_to_nat_andb: \forall a,b:bool.
bool_to_nat (andb a b) = (bool_to_nat a)*(bool_to_nat b).
intros.
-elim a;auto.
+elim a;autobatch.
(*[elim b
[ simplify.
reflexivity
((i1*(S n) + i) \mod (S n)) i1 i)
[ rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n))
((i1*(S n) + i) \mod (S n)) i1 i)
- [ rewrite > H3;auto (*qui auto impiega parecchio tempo*)
+ [ rewrite > H3;autobatch (*qui autobatch impiega parecchio tempo*)
(*[ apply bool_to_nat_andb
| unfold lt.
apply le_S_S.
apply le_S_S.
assumption
]*)
- | auto
+ | autobatch
(*apply div_mod_spec_div_mod.
unfold lt.
apply le_S_S.
apply le_O_n*)
- | constructor 1;auto
+ | constructor 1;autobatch
(*[ unfold lt.
apply le_S_S.
assumption
| reflexivity
]*)
]
- | auto
+ | autobatch
(*apply div_mod_spec_div_mod.
unfold lt.
apply le_S_S.
apply le_O_n*)
- | constructor 1;auto
+ | constructor 1;autobatch
(*[ unfold lt.
apply le_S_S.
assumption
(sigma m (\lambda n.bool_to_nat (f2 n)) O))) O))
[ apply eq_sigma.
intros.
- auto
+ autobatch
(*rewrite > sym_times.
apply (trans_eq ? ?
(sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O))
| apply sym_eq.
apply sigma_times
]*)
- | auto
+ | autobatch
(*simplify.
apply sym_eq.
apply sigma_times*)
rewrite < S_pred in \vdash (? ? %)
[ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
apply H
- [ auto
+ [ autobatch
(*apply lt_mod_m_m.
unfold lt.
apply le_S_S.
apply le_O_n*)
| apply (lt_times_to_lt_l n).
apply (le_to_lt_to_lt ? i)
- [ auto
+ [ autobatch
(*rewrite > (div_mod i (S n)) in \vdash (? ? %)
[ rewrite > sym_plus.
apply le_plus_n
| unfold lt.
rewrite > S_pred in \vdash (? ? %)
[ apply le_S_S.
- auto
+ autobatch
(*rewrite > plus_n_O in \vdash (? ? %).
rewrite > sym_times.
assumption*)
- | auto
+ | autobatch
(*rewrite > (times_n_O O).
apply lt_times;
unfold lt;apply le_S_S;apply le_O_n*)
]
]
]
- | auto
+ | autobatch
(*rewrite > (times_n_O O).
apply lt_times;
unfold lt;apply le_S_S;apply le_O_n *)
rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
- auto
+ autobatch
(*rewrite > H6.
reflexivity*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
]
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
]
| apply (lt_times_to_lt_l n).
apply (le_to_lt_to_lt ? j)
- [ auto.
+ [ autobatch.
(*rewrite > (div_mod j (S n)) in \vdash (? ? %)
[ rewrite > sym_plus.
apply le_plus_n
assumption
]
]
- | auto
+ | autobatch
(*apply lt_mod_m_m.
unfold lt. apply le_S_S.
apply le_O_n*)
]
| apply (lt_times_to_lt_l n).
apply (le_to_lt_to_lt ? i)
- [ auto
+ [ autobatch
(*rewrite > (div_mod i (S n)) in \vdash (? ? %)
[ rewrite > sym_plus.
apply le_plus_n
assumption
]
]
- | auto
+ | autobatch
(*apply lt_mod_m_m.
unfold lt. apply le_S_S.
apply le_O_n*)
]
| unfold lt.
- auto
+ autobatch
(*rewrite > S_pred in \vdash (? ? %)
[ apply le_S_S.
assumption
]*)
]
| unfold lt.
- auto
+ autobatch
(*rewrite > S_pred in \vdash (? ? %)
[ apply le_S_S.
assumption
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/div_and_mod".
+set "baseuri" "cic:/matita/library_autobatch/nat/div_and_mod".
include "datatypes/constructors.ma".
include "auto/nat/minus.ma".
| (S p) \Rightarrow mod_aux n n p].
interpretation "natural remainder" 'module x y =
- (cic:/matita/library_auto/nat/div_and_mod/mod.con x y).
+ (cic:/matita/library_autobatch/nat/div_and_mod/mod.con x y).
let rec div_aux p m n : nat \def
match (leb m n) with
| (S p) \Rightarrow div_aux n n p].
interpretation "natural divide" 'divide x y =
- (cic:/matita/library_auto/nat/div_and_mod/div.con x y).
+ (cic:/matita/library_autobatch/nat/div_and_mod/div.con x y).
theorem le_mod_aux_m_m:
\forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
intro.
elim p
[ apply (le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m)).
- auto
+ autobatch
(*simplify.
apply le_O_n*)
| simplify.
[ assumption
| apply H.
cut (n1 \leq (S n) \to n1-(S m) \leq n)
- [ auto
+ [ autobatch
(*apply Hcut.
assumption*)
- | elim n1;simplify;auto
+ | elim n1;simplify;autobatch
(*[ apply le_O_n.
| apply (trans_le ? n2 n)
[ apply le_minus_m
[ apply False_ind.
apply (not_le_Sn_O O H)
| simplify.
- auto
+ autobatch
(*unfold lt.
apply le_S_S.
apply le_mod_aux_m_m.
(n=(div_aux p n m)*(S m) + (mod_aux p n m)).
intro.
elim p;simplify
-[ elim (leb n m);auto
+[ elim (leb n m);autobatch
(*simplify;apply refl_eq.*)
| apply (leb_elim n1 m);simplify;intro
[ apply refl_eq
elim (H (n1-(S m)) m).
change with (n1=(S m)+(n1-(S m))).
rewrite < sym_plus.
- auto
+ autobatch
(*apply plus_minus_m_m.
change with (m < n1).
apply not_le_to_lt.
unfold Not.
intros.
elim H.
-absurd (le (S r) O);auto.
+absurd (le (S r) O);autobatch.
(*[ rewrite < H1.
assumption
| exact (not_le_Sn_O r).
theorem div_mod_spec_div_mod:
\forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
intros.
-auto.
+autobatch.
(*apply div_mod_spec_intro
[ apply lt_mod_m_m.
assumption
| elim Hcut.
assumption
]
- | apply (trans_le ? ((q1-q)*b));auto
+ | apply (trans_le ? ((q1-q)*b));autobatch
(*[ apply le_times_n.
apply le_SO_minus.
exact H6
]
| rewrite < sym_times.
rewrite > distr_times_minus.
- rewrite > plus_minus;auto
+ rewrite > plus_minus;autobatch
(*[ rewrite > sym_times.
rewrite < H5.
rewrite < sym_times.
]*)
]
| (* eq case *)
- auto
+ autobatch
(*intros.
assumption*)
| (* the following case is symmetric *)
| elim Hcut.
assumption
]
- | apply (trans_le ? ((q-q1)*b));auto
+ | apply (trans_le ? ((q-q1)*b));autobatch
(*[ apply le_times_n.
apply le_SO_minus.
exact H6
]
| rewrite < sym_times.
rewrite > distr_times_minus.
- rewrite > plus_minus;auto
+ rewrite > plus_minus;autobatch
(*[ rewrite > sym_times.
rewrite < H3.
rewrite < sym_times.
theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
intros.
-auto.
+autobatch.
(*constructor 1
[ unfold lt.
apply le_S_S.
theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
intros.
apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
-[2: apply div_mod_spec_div_mod.auto.
+[2: apply div_mod_spec_div_mod.autobatch.
| skip
-| auto
+| autobatch
]
(*unfold lt.apply le_S_S.apply le_O_n.
apply div_mod_spec_times.*)
theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
intros.
-apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O);auto.
+apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O);autobatch.
(*[ apply div_mod_spec_div_mod.
assumption
| constructor 1
theorem eq_div_O: \forall n,m. n < m \to n / m = O.
intros.
-apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n);auto.
+apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n);autobatch.
(*[ apply div_mod_spec_div_mod.
apply (le_to_lt_to_lt O n m)
[ apply le_O_n
theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O.
intros.
-apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O);auto.
+apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O);autobatch.
(*[ apply div_mod_spec_div_mod.
assumption
| constructor 1
((S n) \mod m) = S (n \mod m).
intros.
apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m)))
-[ auto
+[ autobatch
(*apply div_mod_spec_div_mod.
assumption*)
| constructor 1
[ assumption
| rewrite < plus_n_Sm.
- auto
+ autobatch
(*apply eq_f.
apply div_mod.
assumption*)
theorem mod_O_n: \forall n:nat.O \mod n = O.
intro.
-elim n;auto.
+elim n;autobatch.
(*simplify;reflexivity*)
qed.
theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
intros.
-apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n);auto.
+apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n);autobatch.
(*[ apply div_mod_spec_div_mod.
apply (le_to_lt_to_lt O n m)
[ apply le_O_n
change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q).
intros.
rewrite < (div_times n).
-auto.
+autobatch.
(*rewrite < (div_times n q).
apply eq_f2
[ assumption
intros 4.
apply (lt_O_n_elim n H).
intros.
-auto.
+autobatch.
(*apply (inj_times_r m).
assumption.*)
qed.
theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
simplify.
intros.
-auto.
+autobatch.
(*apply (inj_times_r n x y).
rewrite < sym_times.
rewrite < (sym_times y).
intros 4.
apply (lt_O_n_elim n H).
intros.
-auto.
+autobatch.
(*apply (inj_times_l m).
assumption.*)
qed.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/euler_theorem".
+set "baseuri" "cic:/matita/library_autobatch/nat/euler_theorem".
include "auto/nat/map_iter_p.ma".
include "auto/nat/totient.ma".
apply (nat_case m)
[ reflexivity
| intro.
- apply count_card1;auto
+ apply count_card1;autobatch
(*[ reflexivity
- | auto.rewrite > gcd_n_n.
+ | autobatch.rewrite > gcd_n_n.
reflexivity
]*)
]
[ rewrite > pi_p_S.
cut (eqb (gcd (S O) n) (S O) = true)
[ rewrite > Hcut.
- auto
+ autobatch
(*change with ((gcd n (S O)) = (S O)).
- auto*)
- | auto
- (*apply eq_to_eqb_true.auto*)
+ autobatch*)
+ | autobatch
+ (*apply eq_to_eqb_true.autobatch*)
]
| rewrite > pi_p_S.
apply eqb_elim
change with
((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
apply eq_gcd_times_SO
- [ auto
+ [ autobatch
(*unfold.
apply le_S.
assumption*)
| apply lt_O_pi_p.
- | auto
+ | autobatch
(*rewrite > sym_gcd.
assumption.*)
| apply H2.
- auto
+ autobatch
(*apply (trans_le ? (S n1))
[ apply le_n_Sn
| assumption
change with
(gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
apply H2.
- auto
+ autobatch
(*apply (trans_le ? (S n1))
[ apply le_n_Sn
| assumption
(\lambda x.f x \mod a) (S O) times) a.
intros.
elim n
-[ auto
+[ autobatch
(*rewrite > map_iter_p_O.
apply (congruent_n_n ? a)*)
| apply (eqb_elim (gcd (S n1) a) (S O))
[ rewrite > map_iter_p_S_true
[ apply congruent_times
[ assumption
- | auto
+ | autobatch
(*apply congruent_n_mod_n.
assumption*)
- | (*NB qui auto non chiude il goal*)
+ | (*NB qui autobatch non chiude il goal*)
assumption
]
- | auto
+ | autobatch
(*apply eq_to_eqb_true.
assumption*)
]
- | auto
+ | autobatch
(*apply eq_to_eqb_true.
assumption*)
]
| intro.
rewrite > map_iter_p_S_false
[ rewrite > map_iter_p_S_false
- [ (*BN qui auto non chiude il goal*)
+ [ (*BN qui autobatch non chiude il goal*)
assumption
- | auto
+ | autobatch
(*apply not_eq_to_eqb_false.
assumption*)
]
- | auto
+ | autobatch
(*apply not_eq_to_eqb_false.
assumption*)
]
intros.
split
[ split
- [ auto
+ [ autobatch
(*apply lt_to_le.
apply lt_mod_m_m.
assumption*)
apply eq_gcd_times_SO
[ assumption
| apply (gcd_SO_to_lt_O i n H).
- auto
+ autobatch
(*apply eqb_true_to_eq.
assumption*)
- | auto
+ | autobatch
(*rewrite > sym_gcd.
assumption*)
- | auto
+ | autobatch
(*rewrite > sym_gcd.
apply eqb_true_to_eq.
assumption*)
apply (trans_le ? (j -i))
[ apply divides_to_le
[(*fattorizzare*)
- unfold lt.auto.
+ unfold lt.autobatch.
(*apply (lt_plus_to_lt_l i).
simplify.
rewrite < (plus_minus_m_m)
]*)
| apply (gcd_SO_to_divides_times_to_divides a)
[ assumption
- | auto
+ | autobatch
(*rewrite > sym_gcd.
assumption*)
| apply mod_O_to_divides
[ assumption
| rewrite > distr_times_minus.
- auto
+ autobatch
]
]
]
- | auto
+ | autobatch
]
]
- | auto
+ | autobatch
(*intro.
assumption*)
| intro.
apply (trans_le ? (i -j))
[ apply divides_to_le
[(*fattorizzare*)
- unfold lt.auto.
+ unfold lt.autobatch.
(*apply (lt_plus_to_lt_l j).
simplify.
rewrite < (plus_minus_m_m)
]*)
| apply (gcd_SO_to_divides_times_to_divides a)
[ assumption
- | auto
+ | autobatch
(*rewrite > sym_gcd.
assumption*)
| apply mod_O_to_divides
[ assumption
| rewrite > distr_times_minus.
- auto
+ autobatch
]
]
]
- | auto
+ | autobatch
]
]
]
intros.
cut (O < a)
[ apply divides_to_congruent
- [ auto
+ [ autobatch
(*apply (trans_lt ? (S O)).
apply lt_O_S.
assumption*)
- | auto
+ | autobatch
(*change with (O < exp a (totient n)).
apply lt_O_exp.
assumption*)
| apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
- [ auto
+ [ autobatch
(*apply (trans_lt ? (S O)).
apply lt_O_S.
assumption*)
- | auto
+ | autobatch
(*apply gcd_pi_p
[ apply (trans_lt ? (S O)).
apply lt_O_S.
rewrite > totient_card.
rewrite > a_times_pi_p.
apply congruent_to_divides
- [ auto
+ [ autobatch
(*apply (trans_lt ? (S O)).
apply lt_O_S.
assumption*)
| apply (transitive_congruent n ?
(map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
- [ auto
+ [ autobatch
(*apply (congruent_map_iter_p_times ? n n).
apply (trans_lt ? (S O))
[ apply lt_O_S
apply not_eq_to_eqb_false.
unfold.
intro.
- auto
+ autobatch
(*apply (lt_to_not_eq (S O) n)
[ assumption
| apply sym_eq.
]
]
]
-| elim (le_to_or_lt_eq O a (le_O_n a));auto
+| elim (le_to_or_lt_eq O a (le_O_n a));autobatch
(*[ assumption
- | auto.absurd (gcd a n = S O)
+ | autobatch.absurd (gcd a n = S O)
[ assumption
| rewrite < H2.
simplify.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/exp".
+set "baseuri" "cic:/matita/library_autobatch/nat/exp".
include "auto/nat/div_and_mod.ma".
[ O \Rightarrow (S O)
| (S p) \Rightarrow (times n (exp n p)) ].
-interpretation "natural exponent" 'exp a b = (cic:/matita/library_auto/nat/exp/exp.con a b).
+interpretation "natural exponent" 'exp a b = (cic:/matita/library_autobatch/nat/exp/exp.con a b).
theorem exp_plus_times : \forall n,p,q:nat.
n \sup (p + q) = (n \sup p) * (n \sup q).
intros.
-elim p;simplify;auto.
+elim p;simplify;autobatch.
(*[ rewrite < plus_n_O.
reflexivity
| rewrite > H.
theorem exp_n_O : \forall n:nat. S O = n \sup O.
intro.
-auto.
+autobatch.
(*simplify.
reflexivity.*)
qed.
theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
intro.
-auto.
+autobatch.
(*simplify.
rewrite < times_n_SO.
reflexivity.*)
(n \sup p) \sup q = n \sup (p * q).
intros.
elim q;simplify
-[ auto.
+[ autobatch.
(*rewrite < times_n_O.
simplify.
reflexivity*)
| rewrite > H.
rewrite < exp_plus_times.
- auto
+ autobatch
(*rewrite < times_n_Sm.
reflexivity*)
]
theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m.
intros.
-elim m;simplify;auto.
+elim m;simplify;autobatch.
(*unfold lt
[ apply le_n
| rewrite > times_n_SO.
[ simplify.
rewrite < plus_n_Sm.
apply le_S_S.
- auto
+ autobatch
(*apply le_S_S.
rewrite < sym_plus.
apply le_plus_n*)
- | auto
+ | autobatch
(*apply le_times;assumption*)
]
]
apply antisym_le
[ apply le_S_S_to_le.
rewrite < H1.
- auto
+ autobatch
(*change with (m < n \sup m).
apply lt_m_exp_nm.
assumption*)
intros 4.
apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y))
[ intros.
- auto
+ autobatch
(*apply sym_eq.
apply (exp_to_eq_O n)
[ assumption
(* esprimere inj_times senza S *)
cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b)
[ apply Hcut
- [ auto
+ [ autobatch
(*simplify.
unfold lt.
apply le_S_S_to_le.
apply le_S.
assumption*)
- | (*NB qui auto non chiude il goal, chiuso invece chiamando solo la tattica assumption*)
+ | (*NB qui autobatch non chiude il goal, chiuso invece chiamando solo la tattica assumption*)
assumption
]
| intros 2.
- apply (nat_case n);intros;auto
+ apply (nat_case n);intros;autobatch
(*[ apply False_ind.
apply (not_le_Sn_O O H3)
| apply (inj_times_r m1).
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/factorial".
+set "baseuri" "cic:/matita/library_autobatch/nat/factorial".
include "auto/nat/le_arith.ma".
[ O \Rightarrow (S O)
| (S m) \Rightarrow (S m)*(fact m)].
-interpretation "factorial" 'fact n = (cic:/matita/library_auto/nat/factorial/fact.con n).
+interpretation "factorial" 'fact n = (cic:/matita/library_autobatch/nat/factorial/fact.con n).
theorem le_SO_fact : \forall n. (S O) \le n!.
intro.
elim n
-[ auto
+[ autobatch
(*simplify.
apply le_n*)
| change with ((S O) \le (S n1)*n1!).
- auto
+ autobatch
(*apply (trans_le ? ((S n1)*(S O)))
[ simplify.
apply le_S_S.
intro.
apply (nat_case n)
[ intro.
- auto
+ autobatch
(*apply False_ind.
apply (not_le_Sn_O (S O) H).*)
| intros.
change with ((S (S O)) \le (S m)*m!).
- apply (trans_le ? ((S(S O))*(S O)));auto
+ apply (trans_le ? ((S(S O))*(S O)));autobatch
(*[ apply le_n
| apply le_times
[ exact H
elim n
[ apply le_O_n
| change with (S n1 \le (S n1)*n1!).
- apply (trans_le ? ((S n1)*(S O)));auto
+ apply (trans_le ? ((S n1)*(S O)));autobatch
(*[ rewrite < times_n_SO.
apply le_n
| apply le_times.
intro.
apply (nat_case n)
[ intro.
- auto
+ autobatch
(*apply False_ind.
apply (not_le_Sn_O (S(S O)) H)*)
| intros.
simplify.
unfold lt.
apply le_S_S.
- auto
+ autobatch
(*rewrite < plus_n_O.
apply le_plus_n*)
| apply le_times_r.
- auto
+ autobatch
(*apply le_SSO_fact.
simplify.
unfold lt.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/factorization".
+set "baseuri" "cic:/matita/library_autobatch/nat/factorization".
include "auto/nat/ord.ma".
include "auto/nat/gcd.ma".
apply (ex_intro nat ? a).
split
[ apply (trans_le a (nth_prime a))
- [ auto
+ [ autobatch
(*apply le_n_fn.
exact lt_nth_prime_n_nth_prime_Sn*)
| rewrite > H1.
(*CSC: simplify here does something nasty! *)
change with (divides_b (smallest_factor n) n = true).
apply divides_to_divides_b_true
- [ auto
+ [ autobatch
(*apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
| apply lt_SO_smallest_factor.
assumption
]*)
- | auto
+ | autobatch
(*letin x \def le.
- auto new*)
+ autobatch new*)
(*
apply divides_smallest_factor_n;
apply (trans_lt ? (S O));
| assumption; ] *)
]
]
- | auto
+ | autobatch
(*
apply prime_to_nth_prime;
apply prime_smallest_factor_n;
intros.
unfold max_prime_factor.
apply f_m_to_le_max
-[ auto
+[ autobatch
(*apply (trans_le ? n)
[ apply le_max_n
| apply divides_to_le;assumption
]*)
| change with (divides_b (nth_prime (max_prime_factor n)) m = true).
apply divides_to_divides_b_true
- [ auto
+ [ autobatch
(*cut (prime (nth_prime (max_prime_factor n)))
[ apply lt_O_nth_prime_n
| apply prime_nth_prime
]*)
- | auto
+ | autobatch
(*cut (nth_prime (max_prime_factor n) \divides n)
- [ auto
- | auto
+ [ autobatch
+ | autobatch
] *)
(*
[ apply (transitive_divides ? n);
[ assumption
| absurd (nth_prime (max_prime_factor n) \divides r)
[ rewrite < H4.
- auto
+ autobatch
(*apply divides_max_prime_factor_n.
assumption*)
| unfold Not.
intro.
cut (r \mod (nth_prime (max_prime_factor n)) \neq O)
- [ auto
+ [ autobatch
(*unfold Not in Hcut1.
- auto new*)
+ autobatch new*)
(*
apply Hcut1.apply divides_to_mod_O;
[ apply lt_O_nth_prime_n.
[ 2: rewrite < H1.
assumption
| letin x \def le.
- auto width = 4 new
+ autobatch width = 4 new
]
(* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
]
| assumption
| apply (witness r n ((nth_prime p) \sup q)).
rewrite > sym_times.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply (p_ord_aux_to_exp n n)
[ apply lt_O_nth_prime_n.
| assumption
]
| assumption
]
- | apply (p_ord_to_lt_max_prime_factor n ? q);auto
+ | apply (p_ord_to_lt_max_prime_factor n ? q);autobatch
(*[ assumption
| apply sym_eq.
assumption
[1,2:
simplify;
unfold lt;
- rewrite > times_n_SO;auto
+ rewrite > times_n_SO;autobatch
(*apply le_times
[ change with (O < nth_prime i).
apply lt_O_nth_prime_n
[ simplify.
unfold lt.
rewrite > times_n_SO.
- auto
+ autobatch
(*apply le_times
[ change with (S O < nth_prime i).
apply lt_SO_nth_prime_n
unfold lt.
rewrite > times_n_SO.
rewrite > sym_times.
- auto
+ autobatch
(*apply le_times
[ change with (O < exp (nth_prime i) n).
apply lt_O_exp.
[ simplify.
elim H1
[ elim H2.
- auto
+ autobatch
(*rewrite > H3.
rewrite > sym_times.
apply times_n_SO*)
defactorize_aux match (p_ord_aux n1 n1 (nth_prime n)) with
[(pair q r) \Rightarrow (factorize_aux n r (nf_cons q acc))] O =
n1*defactorize_aux acc (S n))
- [ (*invocando auto in questo punto, dopo circa 7 minuti l'esecuzione non era ancora terminata
+ [ (*invocando autobatch in questo punto, dopo circa 7 minuti l'esecuzione non era ancora terminata
ne' con un errore ne' chiudendo il goal
*)
apply (Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n)))
(snd ? ? (p_ord_aux n1 n1 (nth_prime n)))).
- auto
+ autobatch
(*apply sym_eq.apply eq_pair_fst_snd*)
| intros.
rewrite < H3.
cut (n1 = r * (nth_prime n) \sup q)
[ rewrite > H
[ simplify.
- auto
+ autobatch
(*rewrite < assoc_times.
rewrite < Hcut.
reflexivity.*)
- | auto
+ | autobatch
(*cut (O < r \lor O = r)
[ elim Hcut1
[ assumption
[ elim H5.
apply False_ind.
apply (not_eq_O_S n).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
- | auto
+ | autobatch
(*apply le_S_S_to_le.
exact H5*)
]
]
| cut (r=(S O))
[ apply (nat_case n)
- [ auto
+ [ autobatch
(*left.
split
[ assumption
| intro.
right.
rewrite > Hcut2.
- auto
+ autobatch
(*simplify.
unfold lt.
apply le_S_S.
| cut (r < (S O) ∨ r=(S O))
[ elim Hcut2
[ absurd (O=r)
- [ auto
+ [ autobatch
(*apply le_n_O_to_eq.
apply le_S_S_to_le.
exact H5*)
| unfold Not.
intro.
- auto
+ autobatch
(*cut (O=n1)
[ apply (not_le_Sn_O O).
rewrite > Hcut3 in ⊢ (? ? %).
]
| assumption
]
- | auto
+ | autobatch
(*apply (le_to_or_lt_eq r (S O)).
apply not_lt_to_le.
assumption*)
defactorize (match p_ord (S(S m1)) (nth_prime p) with
[ (pair q r) \Rightarrow
nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)))
- [ (*invocando auto qui, dopo circa 300 secondi non si ottiene alcun risultato*)
+ [ (*invocando autobatch qui, dopo circa 300 secondi non si ottiene alcun risultato*)
apply (Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p)))
(snd ? ? (p_ord (S(S m1)) (nth_prime p)))).
- auto
+ autobatch
(*apply sym_eq.
apply eq_pair_fst_snd*)
| intros.
[ (*CSC: simplify here does something really nasty *)
change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
cut ((S (pred q)) = q)
- [ (*invocando auto qui, dopo circa 300 secondi non si ottiene ancora alcun risultato*)
+ [ (*invocando autobatch qui, dopo circa 300 secondi non si ottiene ancora alcun risultato*)
rewrite > Hcut2.
- auto
+ autobatch
(*rewrite > sym_times.
apply sym_eq.
apply (p_ord_aux_to_exp (S(S m1)))
[ assumption
| absurd (nth_prime p \divides S (S m1))
[ apply (divides_max_prime_factor_n (S (S m1))).
- auto
+ autobatch
(*unfold lt.
apply le_S_S.
apply le_S_S.
change with (nth_prime p \divides r \to False).
intro.
apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r) [ apply lt_SO_nth_prime_n
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| apply le_n
| assumption
- | (*invocando auto qui, dopo circa 300 secondi non si ottiene ancora alcun risultato*)
+ | (*invocando autobatch qui, dopo circa 300 secondi non si ottiene ancora alcun risultato*)
apply divides_to_mod_O
[ apply lt_O_nth_prime_n
| assumption
]
]
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
cut ((S O) < r \lor S O \nlt r)
[ elim Hcut2
[ right.
- apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r);auto
+ apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r);autobatch
(*[ unfold lt.
apply le_S_S.
apply le_O_n
]*)
| cut (r=(S O))
[ apply (nat_case p)
- [ auto
+ [ autobatch
(*left.
split
[ assumption
| intro.
right.
rewrite > Hcut3.
- auto
+ autobatch
(*simplify.
unfold lt.
apply le_S_S.
]
| cut (r \lt (S O) \or r=(S O))
[ elim Hcut3
- [ absurd (O=r);auto
+ [ absurd (O=r);autobatch
(*[ apply le_n_O_to_eq.
apply le_S_S_to_le.
exact H2
]*)
| assumption
]
- | auto
+ | autobatch
(*apply (le_to_or_lt_eq r (S O)).
apply not_lt_to_le.
assumption*)
apply (not_eq_O_S (S m1)).
rewrite > Hcut.
rewrite < H1.
- auto
+ autobatch
(*rewrite < times_n_O.
reflexivity*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
]
| (* prova del cut *)
- apply (p_ord_aux_to_exp (S(S m1)));auto
+ apply (p_ord_aux_to_exp (S(S m1)));autobatch
(*[ apply lt_O_nth_prime_n
| assumption
]*)
intro.
elim f
[ simplify.
- auto
+ autobatch
(*apply (witness ? ? ((nth_prime i) \sup n)).
reflexivity*)
| change with
rewrite > H1.
rewrite < sym_times.
rewrite > assoc_times.
- auto
+ autobatch
(*rewrite < plus_n_Sm.
apply (witness ? ? (n2* (nth_prime i) \sup n)).
reflexivity*)
intros 3.
elim m
[ simplify in H1.
- auto
+ autobatch
(*apply (transitive_divides p (S O))
[ assumption
| apply divides_SO_n
| cut (p \divides n \lor p \divides n \sup n1)
[ elim Hcut
[ assumption
- | auto
+ | autobatch
(*apply H;assumption*)
]
- | auto
+ | autobatch
(*apply divides_times_to_divides
[ assumption
| exact H2
elim H1.
apply H4
[ apply (divides_exp_to_divides p q m);assumption
-| (*invocando auto in questo punto, dopo piu' di 8 minuti la computazione non
+| (*invocando autobatch in questo punto, dopo piu' di 8 minuti la computazione non
* era ancora terminata.
*)
unfold prime in H.
- (*invocando auto anche in questo punto, dopo piu' di 10 minuti la computazione
+ (*invocando autobatch anche in questo punto, dopo piu' di 10 minuti la computazione
* non era ancora terminata.
*)
elim H.
(nth_prime i \divides (nth_prime j) \sup (S n) \to False).
intro.
absurd ((nth_prime i) = (nth_prime j))
- [ apply (divides_exp_to_eq ? ? (S n));auto
+ [ apply (divides_exp_to_eq ? ? (S n));autobatch
(*[ apply prime_nth_prime
| apply prime_nth_prime
| assumption
\lor nth_prime i \divides defactorize_aux n1 (S j))
[ elim Hcut
[ absurd ((nth_prime i) = (nth_prime j))
- [ apply (divides_exp_to_eq ? ? n);auto
+ [ apply (divides_exp_to_eq ? ? n);autobatch
(*[ apply prime_nth_prime
| apply prime_nth_prime
| assumption
]
]
| apply (H i (S j))
- [ auto
+ [ autobatch
(*apply (trans_lt ? j)
[ assumption
| unfold lt.
| assumption
]
]
- | auto
+ | autobatch
(*apply divides_times_to_divides.
apply prime_nth_prime.
assumption*)
intro.
cut (S(max_p g)+i= i)
[ apply (not_le_Sn_n i).
- rewrite < Hcut in \vdash (? ? %). (*chiamando auto qui da uno strano errore "di tipo"*)
+ rewrite < Hcut in \vdash (? ? %). (*chiamando autobatch qui da uno strano errore "di tipo"*)
simplify.
- auto
+ autobatch
(*apply le_S_S.
apply le_plus_n*)
| apply injective_nth_prime.
rewrite < plus_n_O.
intro.
apply (not_divides_defactorize_aux f i (S i) ?)
-[ auto
+[ autobatch
(*unfold lt.
apply le_n*)
-| auto
+| autobatch
(*rewrite > H.
rewrite > assoc_times.
apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
apply inj_S.
apply (inj_exp_r (nth_prime i))
[ apply lt_SO_nth_prime_n
- | (*qui auto non conclude il goal attivo*)
+ | (*qui autobatch non conclude il goal attivo*)
assumption
]
| apply False_ind.
- (*auto chiamato qui NON conclude il goal attivo*)
+ (*autobatch chiamato qui NON conclude il goal attivo*)
apply (not_eq_nf_last_nf_cons n2 n n1 i H2)
]
| generalize in match H1.
elim g
[ apply False_ind.
apply (not_eq_nf_last_nf_cons n1 n2 n i).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
| simplify in H3.
nf_cons n n1 = nf_cons n2 n3))
[ intro.
elim n4
- [ auto
+ [ autobatch
(*apply eq_f.
apply (H n3 (S i))
simplify in H4.
assumption*)
| apply False_ind.
apply (not_eq_nf_cons_O_nf_cons n1 n3 n5 i).
- (*auto chiamato qui NON chiude il goal attivo*)
+ (*autobatch chiamato qui NON chiude il goal attivo*)
assumption
]
| intros.
apply False_ind.
apply (not_eq_nf_cons_O_nf_cons n3 n1 n4 i).
apply sym_eq.
- (*auto chiamato qui non chiude il goal*)
+ (*autobatch chiamato qui non chiude il goal*)
assumption
| intros.
cut (nf_cons n4 n1 = nf_cons m n3)
[ cut (n4=m)
[ cut (n1=n3)
- [ auto
+ [ autobatch
(*rewrite > Hcut1.
rewrite > Hcut2.
reflexivity*)
[ (nf_last m) \Rightarrow n1
| (nf_cons m g) \Rightarrow g ] = n3).
rewrite > Hcut.
- auto
+ autobatch
(*simplify.
reflexivity*)
]
(match nf_cons n4 n1 with
[ (nf_last m) \Rightarrow m
| (nf_cons m g) \Rightarrow m ] = m).
- (*invocando auto qui, dopo circa 8 minuti la computazione non era ancora terminata*)
+ (*invocando autobatch qui, dopo circa 8 minuti la computazione non era ancora terminata*)
rewrite > Hcut.
- auto
+ autobatch
(*simplify.
reflexivity*)
]
apply False_ind.
apply (not_le_Sn_n O).
rewrite > H1 in \vdash (? ? %).
- auto
+ autobatch
(*change with (O < defactorize_aux n O).
apply lt_O_defactorize_aux*)
]
[ (* one - zero *)
simplify in H1.
apply False_ind.
- auto
+ autobatch
(*apply (not_eq_O_S O).
apply sym_eq.
assumption*)
apply False_ind.
apply (not_le_Sn_n (S O)).
rewrite > H1 in \vdash (? ? %).
- auto
+ autobatch
(*change with ((S O) < defactorize_aux n O).
apply lt_SO_defactorize_aux*)
]
apply False_ind.
apply (not_le_Sn_n O).
rewrite < H1 in \vdash (? ? %).
- auto
+ autobatch
(*change with (O < defactorize_aux n O).
apply lt_O_defactorize_aux.*)
| (* proper - one *)
apply False_ind.
apply (not_le_Sn_n (S O)).
rewrite < H1 in \vdash (? ? %).
- auto
+ autobatch
(*change with ((S O) < defactorize_aux n O).
apply lt_SO_defactorize_aux.*)
| (* proper - proper *)
apply eq_f.
apply (injective_defactorize_aux O).
- (*invocata qui la tattica auto NON chiude il goal, chiuso invece
+ (*invocata qui la tattica autobatch NON chiude il goal, chiuso invece
*da exact H1
*)
exact H1
theorem factorize_defactorize:
\forall f,g: nat_fact_all. factorize (defactorize f) = f.
intros.
-auto.
+autobatch.
(*apply injective_defactorize.
apply defactorize_factorize.
*)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/fermat_little_theorem".
+set "baseuri" "cic:/matita/library_autobatch/nat/fermat_little_theorem".
include "auto/nat/exp.ma".
include "auto/nat/gcd.ma".
split
[ intros.
unfold S_mod.
- auto
+ autobatch
(*apply le_S_S_to_le.
change with ((S i) \mod (S n) < S n).
apply lt_mod_m_m.
[ (* i < n, j< n *)
rewrite < mod_S
[ rewrite < mod_S
- [ (*qui auto non chiude il goal, chiuso invece dalla tattica
+ [ (*qui autobatch non chiude il goal, chiuso invece dalla tattica
* apply H2
*)
apply H2
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| rewrite > lt_to_eq_mod;
- unfold lt;auto.(*apply le_S_S;assumption*)
+ unfold lt;autobatch.(*apply le_S_S;assumption*)
]
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| rewrite > lt_to_eq_mod
- [ unfold lt.auto
+ [ unfold lt.autobatch
(*apply le_S_S.
assumption*)
- | unfold lt.auto
+ | unfold lt.autobatch
(*apply le_S_S.
assumption*)
]
[ rewrite < H4 in \vdash (? ? ? (? %?)).
rewrite < mod_S
[ assumption
- | unfold lt.auto
+ | unfold lt.autobatch
(*apply le_S_S.
apply le_O_n*)
| rewrite > lt_to_eq_mod;
- unfold lt;auto;(*apply le_S_S;assumption*)
+ unfold lt;autobatch;(*apply le_S_S;assumption*)
]
- | unfold lt.auto
+ | unfold lt.autobatch
(*apply le_S_S.
apply le_O_n*)
]
[ rewrite < H3 in \vdash (? ? (? %?) ?).
rewrite < mod_S
[ assumption
- | unfold lt.auto
+ | unfold lt.autobatch
(*apply le_S_S.
apply le_O_n*)
| rewrite > lt_to_eq_mod;
- unfold lt;auto(*apply le_S_S;assumption*)
+ unfold lt;autobatch(*apply le_S_S;assumption*)
]
- | unfold lt.auto
+ | unfold lt.autobatch
(*apply le_S_S.
apply le_O_n*)
]
|(* i = n, j= n*)
- auto
+ autobatch
(*rewrite > H3.
rewrite > H4.
reflexivity*)
]
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
- | unfold lt.auto
+ | unfold lt.autobatch
(*apply le_S_S.
assumption*)
]
- | unfold lt.auto
+ | unfold lt.autobatch
(*apply le_S_S.
assumption*)
]
[ unfold prime in H.
elim H.
assumption
- | auto
+ | autobatch
(*apply divides_to_le.
unfold lt.
apply le_n.
[ elim Hcut
[ apply (lt_to_not_le (S n1) p)
[ assumption
- | auto
+ | autobatch
(*apply divides_to_le
[ unfold lt.
apply le_S_S.
| assumption
]*)
]
- | auto
+ | autobatch
(*apply H1
[ apply (trans_lt ? (S n1))
[ unfold lt.
| assumption
]*)
]
- | auto
+ | autobatch
(*apply divides_times_to_divides;
assumption*)
]
apply lt_mod_m_m.
unfold prime in H.
elim H.
- auto
+ autobatch
(*unfold lt.
apply (trans_le ? (S (S O)))
[ apply le_n_Sn
[ apply le_n
| unfold prime in H.
elim H.
- auto
+ autobatch
(*apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
absurd (j-i \lt p)
[ unfold lt.
rewrite > (S_pred p)
- [ auto
+ [ autobatch
(*apply le_S_S.
apply le_plus_to_minus.
apply (trans_le ? (pred p))
| rewrite > sym_plus.
apply le_plus_n
]*)
- | unfold prime in H. elim H. auto.
+ | unfold prime in H. elim H. autobatch.
(*
apply (trans_lt ? (S O))
[ unfold lt.
]
| apply (le_to_not_lt p (j-i)).
apply divides_to_le
- [ unfold lt.auto
+ [ unfold lt.autobatch
(*apply le_SO_minus.
assumption*)
| cut (divides p a \lor divides p (j-i))
[ elim Hcut
[ apply False_ind.
- auto
+ autobatch
(*apply H1.
assumption*)
| assumption
[ assumption
| rewrite > distr_times_minus.
apply eq_mod_to_divides
- [ unfold prime in H.elim H.auto
+ [ unfold prime in H.elim H.autobatch
(*apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
| assumption
]*)
- | auto
+ | autobatch
(*apply sym_eq.
apply H4*)
]
]
]
|(* i = j *)
- auto
+ autobatch
(*intro.
assumption*)
| (* j < i *)
absurd (i-j \lt p)
[ unfold lt.
rewrite > (S_pred p)
- [ auto
+ [ autobatch
(*apply le_S_S.
apply le_plus_to_minus.
apply (trans_le ? (pred p))
| rewrite > sym_plus.
apply le_plus_n
]*)
- | unfold prime in H.elim H.auto.
+ | unfold prime in H.elim H.autobatch.
(*
apply (trans_lt ? (S O))
[ unfold lt.
]
| apply (le_to_not_lt p (i-j)).
apply divides_to_le
- [ unfold lt.auto
+ [ unfold lt.autobatch
(*apply le_SO_minus.
assumption*)
| cut (divides p a \lor divides p (i-j))
[ elim Hcut
[ apply False_ind.
- auto
+ autobatch
(*apply H1.
assumption*)
| assumption
[ assumption
| rewrite > distr_times_minus.
apply eq_mod_to_divides
- [ unfold prime in H.elim H.auto.
+ [ unfold prime in H.elim H.autobatch.
(*
apply (trans_lt ? (S O))
[ unfold lt.
[ cut (O < pred p)
[ apply divides_to_congruent
[ assumption
- | auto
+ | autobatch
(*change with (O < exp a (pred p)).
apply lt_O_exp.
assumption*)
| apply False_ind.
apply (prime_to_not_divides_fact p H (pred p))
[ unfold lt.
- auto
+ autobatch
(*rewrite < (S_pred ? Hcut1).
apply le_n*)
| assumption
rewrite < eq_map_iter_i_pi.
apply (permut_to_eq_map_iter_i ? ? ? ? ? (λm.m))
[ apply assoc_times
- | (*NB qui auto non chiude il goal, chiuso invece dalla sola
+ | (*NB qui autobatch non chiude il goal, chiuso invece dalla sola
( tattica apply sys_times
*)
apply sym_times
| rewrite < plus_n_Sm.
rewrite < plus_n_O.
rewrite < (S_pred ? Hcut2).
- auto
+ autobatch
(*apply permut_mod
[ assumption
| assumption
]*)
| intros.
cut (m=O)
- [ auto
+ [ autobatch
(*rewrite > Hcut3.
rewrite < times_n_O.
apply mod_O_n.*)
- | auto
+ | autobatch
(*apply sym_eq.
apply le_n_O_to_eq.
apply le_S_S_to_le.
]
| unfold prime in H.
elim H.
- auto
+ autobatch
(*apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
| apply False_ind.
apply H1.
rewrite < H2.
- auto
+ autobatch
(*apply (witness ? ? O).
apply times_n_O*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/gcd".
+set "baseuri" "cic:/matita/library_autobatch/nat/gcd".
include "auto/nat/primes.ma".
apply sym_eq.
apply plus_to_minus.
rewrite > sym_times.
- auto.
+ autobatch.
(*letin x \def div.
rewrite < (div_mod ? ? H).
reflexivity.*)
rewrite < assoc_times.
rewrite < H4.
rewrite < sym_times.
-auto.
+autobatch.
(*apply div_mod.
assumption.*)
qed.
gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
intro.
elim p
-[ absurd (O < n);auto
+[ absurd (O < n);autobatch
(*[ assumption
| apply le_to_not_lt.
assumption
elim Hcut
[ rewrite > divides_to_divides_b_true
[ simplify.
- auto
+ autobatch
(*split
[ assumption
| apply (witness n1 n1 (S O)).
cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
gcd_aux n n1 (m \mod n1) \divides mod m n1)
[ elim Hcut1.
- auto width = 4.
+ autobatch width = 4.
(*split
[ apply (divides_mod_to_divides ? ? n1);assumption
| assumption
[ elim Hcut1
[ assumption
| apply False_ind.
- auto
+ autobatch
(*apply H4.
apply mod_O_to_divides
[ assumption
assumption
]*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply lt_mod_m_m.
assumption*)
| apply le_S_S_to_le.
- apply (trans_le ? n1);auto
- (*[ auto.change with (m \mod n1 < n1).
+ apply (trans_le ? n1);autobatch
+ (*[ autobatch.change with (m \mod n1 < n1).
apply lt_mod_m_m.
assumption
| assumption
| assumption
]
]
- | auto
+ | autobatch
(*apply (decidable_divides n1 m).
assumption*)
]
[ apply (nat_case1 n)
[ simplify.
intros.
- auto
+ autobatch
(*split
[ apply (witness m m (S O)).
apply times_n_SO
(gcd_aux (S m1) m (S m1) \divides m
\land
gcd_aux (S m1) m (S m1) \divides (S m1)).
- auto
+ autobatch
(*apply divides_gcd_aux_mn
[ unfold lt.
apply le_S_S.
apply (nat_case1 m)
[ simplify.
intros.
- auto
+ autobatch
(*split
[ apply (witness n O O).
apply times_n_O
\land
gcd_aux (S m1) n (S m1) \divides S m1)
[ elim Hcut.
- auto
+ autobatch
(*split;assumption*)
| apply divides_gcd_aux_mn
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
intro.
apply H.
rewrite > H1.
- auto
+ autobatch
(*apply (trans_le ? (S n))
[ apply le_n_Sn
| assumption
theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
intros.
-exact (proj2 ? ? (divides_gcd_nm n m)). (*auto non termina la dimostrazione*)
+exact (proj2 ? ? (divides_gcd_nm n m)). (*autobatch non termina la dimostrazione*)
qed.
theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
intros.
-exact (proj1 ? ? (divides_gcd_nm n m)). (*auto non termina la dimostrazione*)
+exact (proj1 ? ? (divides_gcd_nm n m)). (*autobatch non termina la dimostrazione*)
qed.
theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
d \divides m \to d \divides n \to d \divides gcd_aux p m n.
intro.
elim p
-[ absurd (O < n);auto
+[ absurd (O < n);autobatch
(*[ assumption
| apply le_to_not_lt.
assumption
cut (n1 \divides m \lor n1 \ndivides m)
[ elim Hcut.
rewrite > divides_to_divides_b_true;
- simplify; auto.
+ simplify; autobatch.
(*[ simplify.
assumption.
| assumption.
[ elim Hcut1
[ assumption
|
- absurd (n1 \divides m);auto
+ absurd (n1 \divides m);autobatch
(*[ apply mod_O_to_divides
[ assumption.
| apply sym_eq.assumption.
| assumption
]*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply lt_mod_m_m.
assumption*)
| apply le_S_S_to_le.
- auto
+ autobatch
(*apply (trans_le ? n1)
[ change with (m \mod n1 < n1).
apply lt_mod_m_m.
| assumption
]*)
| assumption
- | auto
+ | autobatch
(*apply divides_mod;
assumption*)
]
| assumption
| assumption
]
- | auto
+ | autobatch
(*apply (decidable_divides n1 m).
assumption*)
]
| intros.
change with (d \divides gcd_aux (S m1) m (S m1)).
apply divides_gcd_aux
- [ unfold lt.auto
+ [ unfold lt.autobatch
(*apply le_S_S.
apply le_O_n.*)
| assumption.
- | apply le_n. (*chiude il goal anche con auto*)
+ | apply le_n. (*chiude il goal anche con autobatch*)
| assumption.
| rewrite < H2.
assumption
| intros.
change with (d \divides gcd_aux (S m1) n (S m1)).
apply divides_gcd_aux
- [ unfold lt.auto
+ [ unfold lt.autobatch
(*apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*apply lt_to_le.
apply not_le_to_lt.
assumption*)
- | apply le_n (*chiude il goal anche con auto*)
+ | apply le_n (*chiude il goal anche con autobatch*)
| assumption
| rewrite < H2.
assumption
\exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
intro.
elim p
-[ absurd (O < n);auto
+[ absurd (O < n);autobatch
(*[ assumption
| apply le_to_not_lt
assumption.
[ simplify.
apply (ex_intro ? ? (S O)).
apply (ex_intro ? ? O).
- auto
+ autobatch
(*left.
simplify.
rewrite < plus_n_O.
rewrite > distr_times_plus.
rewrite > (sym_times n1).
rewrite > (sym_times n1).
- rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?);auto
+ rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?);autobatch
(*[ rewrite > assoc_times.
rewrite < sym_plus.
rewrite > distr_times_plus.
rewrite < eq_minus_minus_minus_plus.
- rewrite < sym_plus.auto.
+ rewrite < sym_plus.autobatch.
rewrite < plus_minus
[ rewrite < minus_n_n.
reflexivity
[ rewrite > distr_times_plus.
rewrite > assoc_times.
rewrite < eq_minus_minus_minus_plus.
- auto
+ autobatch
(*rewrite < sym_plus.
rewrite < plus_minus
[ rewrite < minus_n_n.
[ cut (O \lt m \mod n1 \lor O = m \mod n1)
[ elim Hcut2
[ assumption
- | absurd (n1 \divides m);auto
+ | absurd (n1 \divides m);autobatch
(*[ apply mod_O_to_divides
[ assumption
| symmetry.
| assumption
]*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply lt_mod_m_m.
assumption*)
| apply le_S_S_to_le.
- auto
+ autobatch
(*apply (trans_le ? n1)
[ change with (m \mod n1 < n1).
apply lt_mod_m_m.
| assumption
]
]
- | auto
+ | autobatch
(*apply (decidable_divides n1 m).
assumption*)
]
- | auto
+ | autobatch
(*apply (lt_to_le_to_lt ? n1);assumption *)
]
]
intros.
apply (ex_intro ? ? O).
apply (ex_intro ? ? (S O)).
- auto
+ autobatch
(*right.simplify.
rewrite < plus_n_O.
apply sym_eq.
(\exists a,b.
a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
- auto
+ autobatch
(*apply eq_minus_gcd_aux
[ unfold lt.
apply le_S_S.
intros.
apply (ex_intro ? ? (S O)).
apply (ex_intro ? ? O).
- auto
+ autobatch
(*left.simplify.
rewrite < plus_n_O.
apply sym_eq.
b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))
[ elim Hcut.
elim H2.
- elim H3;apply (ex_intro ? ? a1);auto
+ elim H3;apply (ex_intro ? ? a1);autobatch
(*[ apply (ex_intro ? ? a1).
apply (ex_intro ? ? a).
right.
left.
assumption
]*)
- | apply eq_minus_gcd_aux;auto
+ | apply eq_minus_gcd_aux;autobatch
(*[ unfold lt.
apply le_S_S.
apply le_O_n
- | auto.apply lt_to_le.
+ | autobatch.apply lt_to_le.
apply not_le_to_lt.
assumption
| apply le_n.
(* some properties of gcd *)
theorem gcd_O_n: \forall n:nat. gcd O n = n.
-auto.
+autobatch.
(*intro.simplify.reflexivity.*)
qed.
intros.
cut (O \divides n \land O \divides m)
[ elim Hcut.
- auto size = 7;
+ autobatch size = 7;
(*
split;
[ apply antisymmetric_divides
theorem lt_O_gcd:\forall m,n:nat. O < n \to O < gcd m n.
intros.
-auto.
+autobatch.
(*
apply (divides_to_lt_O (gcd m n) n ? ?);
[apply (H).
theorem gcd_n_n: \forall n.gcd n n = n.
intro.
-auto.
+autobatch.
(*
apply (antisymmetric_divides (gcd n n) n ? ?);
[apply (divides_gcd_n n n).
unfold.
intro.
apply (lt_to_not_eq (S O) n H).
- auto
+ autobatch
(*apply sym_eq.
assumption*)
]
change with
(\forall n,m:nat. gcd n m = gcd m n).
intros.
-auto size = 7.
+autobatch size = 7.
(*
apply (antisymmetric_divides (gcd n m) (gcd m n) ? ?);
[apply (divides_d_gcd n m (gcd n m) ? ?);
| intro.
apply divides_to_le
[ apply lt_O_gcd.
- auto
+ autobatch
(*rewrite > (times_n_O O).
apply lt_times
- [ auto.unfold lt.
+ [ autobatch.unfold lt.
apply le_S_S.
apply le_O_n
| assumption
]*)
- | apply divides_d_gcd;auto
+ | apply divides_d_gcd;autobatch
(*[ apply (transitive_divides ? (S m1))
[ apply divides_gcd_m
| apply (witness ? ? p).
intros.
apply antisymmetric_le
[ rewrite < H2.
- auto
+ autobatch
(*apply le_gcd_times.
assumption*)
-| auto
+| autobatch
(*change with (O < gcd m n).
apply lt_O_gcd.
assumption*)
intro.
cut (O < n2)
[ elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
- [ cut (gcd n (n*n2) = n);auto
- (*[ auto.apply (lt_to_not_eq (S O) n)
+ [ cut (gcd n (n*n2) = n);autobatch
+ (*[ autobatch.apply (lt_to_not_eq (S O) n)
[ assumption
| rewrite < H4.
assumption
| apply gcd_n_times_nm.
assumption
]*)
- | auto
+ | autobatch
(*apply (trans_lt ? (S O))
[ apply le_n
| assumption
| apply False_ind.
apply (le_to_not_lt n (S O))
[ rewrite < H4.
- apply divides_to_le;auto
+ apply divides_to_le;autobatch
(*[ rewrite > H4.
apply lt_O_S
| apply divides_d_gcd
theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
intro.
-auto.
+autobatch.
(*
apply (symmetric_eq nat (S O) (gcd (S O) n) ?).
apply (antisymmetric_divides (S O) (gcd (S O) n) ? ?);
theorem divides_gcd_mod: \forall m,n:nat. O < n \to
divides (gcd m n) (gcd n (m \mod n)).
intros.
-auto width = 4.
+autobatch width = 4.
(*apply divides_d_gcd
[ apply divides_mod
[ assumption
theorem divides_mod_gcd: \forall m,n:nat. O < n \to
divides (gcd n (m \mod n)) (gcd m n) .
intros.
-auto.
+autobatch.
(*apply divides_d_gcd
[ apply divides_gcd_n
| apply (divides_mod_to_divides ? ? n)
theorem gcd_mod: \forall m,n:nat. O < n \to
(gcd n (m \mod n)) = (gcd m n) .
intros.
-auto.
+autobatch.
(*apply antisymmetric_divides
[ apply divides_mod_gcd.
assumption
intro.
apply H1.
rewrite < (H3 (gcd n m));
- [auto|auto| unfold lt; auto]
+ [autobatch|autobatch| unfold lt; autobatch]
(*[ apply divides_gcd_m
| apply divides_gcd_n
| assumption
[ elim Hcut1.
rewrite < H5 in \vdash (? ? %).
assumption
- | auto
+ | autobatch
(*apply gcd_O_to_eq_O.
apply sym_eq.
assumption*)
]
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
elim H1.
- auto
+ autobatch
(*rewrite > H6.
rewrite < sym_times.rewrite > assoc_times.
rewrite < (assoc_times q).
apply (witness ? ? (n2*a1-q*a)).
reflexivity*)
](* end second case *)
- | rewrite < (prime_to_gcd_SO n p);auto
+ | rewrite < (prime_to_gcd_SO n p);autobatch
(* [ apply eq_minus_gcd
| assumption
| assumption
]
| apply (decidable_divides n p).
apply (trans_lt ? (S O))
- [ auto
+ [ autobatch
(*unfold lt.
apply le_n*)
| unfold prime in H.
change with ((S O) < (S O)).
rewrite < H2 in \vdash (? ? %).
apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p))))
- [ auto
+ [ autobatch
(*apply lt_SO_smallest_factor.
assumption*)
| apply divides_to_le;
- [ auto |
+ [ autobatch |
apply divides_d_gcd
[ assumption
| apply (transitive_divides ? (gcd m (n*p)))
- [ auto.
- | auto.
+ [ autobatch.
+ | autobatch.
]
]
]
[ apply lt_SO_smallest_factor.
assumption
| apply divides_to_le;
- [ auto |
+ [ autobatch |
apply divides_d_gcd
[ assumption
| apply (transitive_divides ? (gcd m (n*p)))
- [ auto.
- | auto.
+ [ autobatch.
+ | autobatch.
]
]
]
]
]
| apply divides_times_to_divides;
- [ auto |
+ [ autobatch |
apply (transitive_divides ? (gcd m (n*p)))
- [ auto.
- | auto.
+ [ autobatch.
+ | autobatch.
]
]
]
(*[ apply prime_smallest_factor_n.
assumption
- | auto.apply (transitive_divides ? (gcd m (n*p)))
+ | autobatch.apply (transitive_divides ? (gcd m (n*p)))
[ apply divides_smallest_factor_n.
apply (trans_lt ? (S O))
[ unfold lt.
| apply divides_gcd_m
]
]*)
-| auto
+| autobatch
(*change with (O < gcd m (n*p)).
apply lt_O_gcd.
rewrite > (times_n_O O).
apply eq_minus_gcd
]
]
-| auto
+| autobatch
(*apply (decidable_divides n p).
assumption.*)
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/le_arith".
+set "baseuri" "cic:/matita/library_autobatch/nat/le_arith".
include "auto/nat/times.ma".
include "auto/nat/orders.ma".
simplify.intros.
elim n;simplify
[ assumption
-| auto
+| autobatch
(*apply le_S_S.assumption*)
]
qed.
simplify.intros.
rewrite < sym_plus.
rewrite < (sym_plus m).
- auto.
+ autobatch.
qed.
*)
theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \le n2 \to m1 \le m2
\to n1 + m1 \le n2 + m2.
intros.
-auto.
+autobatch.
(*apply (trans_le ? (n2 + m1)).
apply le_plus_l.assumption.
apply le_plus_r.assumption.*)
theorem le_plus_n :\forall n,m:nat. m \le n + m.
intros.
change with (O+m \le n+m).
-auto.
+autobatch.
(*apply le_plus_l.
apply le_O_n.*)
qed.
intros.
rewrite > H.
rewrite < sym_plus.
-apply le_plus_n. (* a questo punto funziona anche: auto.*)
+apply le_plus_n. (* a questo punto funziona anche: autobatch.*)
qed.
(* times *)
\forall n:nat.monotonic nat le (\lambda m. n * m).
simplify.intros.elim n;simplify
[ apply le_O_n.
-| auto.
+| autobatch.
(*apply le_plus;
assumption. *) (* chiudo entrambi i goal attivi in questo modo*)
]
simplify.intros.
rewrite < sym_times.
rewrite < (sym_times m).
-auto.
+autobatch.
qed.
*)
theorem le_times: \forall n1,n2,m1,m2:nat. n1 \le n2 \to m1 \le m2
\to n1*m1 \le n2*m2.
intros.
-auto.
+autobatch.
(*apply (trans_le ? (n2*m1)).
apply le_times_l.assumption.
apply le_times_r.assumption.*)
theorem le_times_n: \forall n,m:nat.(S O) \le n \to m \le n*m.
intros.elim H;simplify
-[ auto
+[ autobatch
(*elim (plus_n_O ?).
apply le_n....*)
-| auto
+| autobatch
(*rewrite < sym_plus.
apply le_plus_n.*)
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/lt_arith".
+set "baseuri" "cic:/matita/library_autobatch/nat/lt_arith".
include "auto/nat/div_and_mod.ma".
simplify.intros.
elim n;simplify
[ assumption
-| auto.
+| autobatch.
(*unfold lt.
apply le_S_S.
assumption.*)
rewrite < (sym_plus n).*)
applyS lt_plus_r.assumption.
qed.
-(* IN ALTERNATIVA: mantengo le 2 rewrite, e concludo con auto. *)
+(* IN ALTERNATIVA: mantengo le 2 rewrite, e concludo con autobatch. *)
variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
monotonic_lt_plus_l.
theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
intros.
-auto.
+autobatch.
(*apply (trans_lt ? (n + q)).
apply lt_plus_r.assumption.
apply lt_plus_l.assumption.*)
(* times and zero *)
theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
intros.
-auto.
+autobatch.
(*simplify.
unfold lt.
apply le_S_S.
\forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
simplify.
intros.elim n
-[ auto
+[ autobatch
(*simplify.
rewrite < plus_n_O.
rewrite < plus_n_O.
applyS lt_times_r.assumption.
qed.
-(* IN ALTERNATIVA: mantengo le 2 rewrite, e concludo con auto. *)
+(* IN ALTERNATIVA: mantengo le 2 rewrite, e concludo con autobatch. *)
variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
cut (lt O q)
[ apply (lt_O_n_elim q Hcut).
intro.
- auto
+ autobatch
(*change with (O < (S m1)*(S m2)).
apply lt_O_times_S_S.*)
- | apply (ltn_to_ltO p q H1). (*funziona anche auto*)
+ | apply (ltn_to_ltO p q H1). (*funziona anche autobatch*)
]
| apply (trans_lt ? ((S n1)*q))
- [ auto
+ [ autobatch
(*apply lt_times_r.
assumption.*)
| cut (lt O q)
[ apply (lt_O_n_elim q Hcut).
intro.
- auto
+ autobatch
(*apply lt_times_l.
assumption.*)
- |apply (ltn_to_ltO p q H2). (*funziona anche auto*)
+ |apply (ltn_to_ltO p q H2). (*funziona anche autobatch*)
]
]
]
| absurd (p * (S n) < q * (S n))
[ assumption
| apply le_to_not_lt.
- auto
+ autobatch
(*apply le_times_l.
apply not_lt_to_le.
assumption.*)
reflexivity
| intro.
absurd (p=q)
- [ auto.
+ [ autobatch.
(*apply (inj_times_r n).
assumption*)
- | auto
+ | autobatch
(*apply lt_to_not_eq.
assumption*)
]
| intro.
absurd (q<p)
- [ auto.
+ [ autobatch.
(*apply (lt_times_to_lt_r n).
assumption.*)
- | auto
+ | autobatch
(*apply le_to_not_lt.
apply lt_to_le.
assumption*)
]
].
| intro.
- auto
+ autobatch
(*rewrite < H.
rewrite > nat_compare_n_n.
reflexivity*)
apply nat_compare_elim
[ intro.
absurd (p<q)
- [ auto
+ [ autobatch
(*apply (lt_times_to_lt_r n).
assumption.*)
- | auto
+ | autobatch
(*apply le_to_not_lt.
apply lt_to_le.
assumption.*)
]
| intro.
absurd (q=p)
- [ auto.
+ [ autobatch.
(*symmetry.
apply (inj_times_r n).
assumption*)
- | auto
+ | autobatch
(*apply lt_to_not_eq.
assumption*)
]
rewrite < div_mod
[ rewrite > H2.
assumption.
-| auto
+| autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n.*)
rewrite > H2.
simplify.
unfold lt.
- auto.
+ autobatch.
(*rewrite < plus_n_O.
rewrite < plus_n_Sm.
apply le_S_S.
apply le_S_S.
apply le_plus_n*)
- | auto
+ | autobatch
(*apply le_times_r.
assumption*)
]
- | auto
+ | autobatch
(*rewrite < sym_plus.
apply le_plus_n*)
]
- | auto
+ | autobatch
(*apply (trans_lt ? (S O)).
unfold lt.
apply le_n.
apply (not_le_Sn_n (f x)).
rewrite > H1 in \vdash (? ? %).
change with (f x < f y).
- auto
+ autobatch
(*apply H.
apply H2*)
| intros.
apply (not_le_Sn_n (f y)).
rewrite < H1 in \vdash (? ? %).
change with (f y < f x).
- auto
+ autobatch
(*apply H.
apply H2*)
]
theorem increasing_to_injective: \forall f:nat\to nat.
increasing f \to injective nat nat f.
intros.
-auto.
+autobatch.
(*apply monotonic_to_injective.
apply increasing_to_monotonic.
assumption.*)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/map_iter_p.ma".
+set "baseuri" "cic:/matita/library_autobatch/nat/map_iter_p.ma".
include "auto/nat/permutation.ma".
include "auto/nat/count.ma".
map_iter_p n p g1 a f = map_iter_p n p g2 a f.
intros 6.
elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| simplify.
elim (p (S n1))
[ simplify.
apply eq_f2
- [ auto
+ [ autobatch
(*apply H1.
apply le_n*)
| simplify.
apply H.
intros.
- auto
+ autobatch
(*apply H1.
apply le_S.
assumption*)
| simplify.
apply H.
intros.
- auto
+ autobatch
(*apply H1.
apply le_S.
assumption*)
theorem map_iter_p_O: \forall p.\forall g.\forall f. \forall a:nat.
map_iter_p O p g a f = a.
intros.
-auto.
+autobatch.
(*simplify.reflexivity.*)
qed.
O < pi_p p n.
intros.
elim n
-[ auto
+[ autobatch
(*simplify.
apply le_n*)
| rewrite > pi_p_S.
elim p (S n1)
[ change with (O < (S n1)*(pi_p p n1)).
- auto
+ autobatch
(*rewrite >(times_n_O n1).
apply lt_times
[ apply le_n
intros.
elim n
[ simplify.
- auto
+ autobatch
(*rewrite > H.
reflexivity*)
| simplify.
rewrite < plus_n_O.
apply eq_f.
- (*qui auto non chiude un goal chiuso invece dal solo assumption*)
+ (*qui autobatch non chiude un goal chiuso invece dal solo assumption*)
assumption
]
qed.
apply (nat_case n)
[ intro.
simplify.
- auto
+ autobatch
(*rewrite > H.
reflexivity*)
| intros.rewrite > (count_card ? ? H).
simplify.
- auto
+ autobatch
(*rewrite > H1.
reflexivity*)
]
exp a (card n p) * pi_p p n = map_iter_p n p (\lambda n.a*n) (S O) times.
intros.
elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| simplify.
(a*exp a (card n1 p) * ((S n1) * (pi_p p n1)) =
a*(S n1)*map_iter_p n1 p (\lambda n.a*n) (S O) times).
rewrite < H.
- auto
+ autobatch
| intro.
- (*la chiamata di auto in questo punto dopo circa 8 minuti non aveva
+ (*la chiamata di autobatch in questo punto dopo circa 8 minuti non aveva
* ancora generato un risultato
*)
assumption
[ unfold compose.
assumption
| unfold compose.
- auto
+ autobatch
(*rewrite < H11.
reflexivity*)
]
unfold compose.
apply (H9 (f j))
[ elim (H j H13 H12).
- auto
+ autobatch
(*elim H15.
rewrite < H18.
reflexivity*)
split
[ elim H4.
elim (le_to_or_lt_eq (f i) (S n))
- [ auto
+ [ autobatch
(*apply le_S_S_to_le.
assumption*)
| absurd (f i = (S n))
[ assumption
| rewrite < H1.
apply H5
- [ auto
+ [ autobatch
(*rewrite < H8.
assumption*)
| apply le_n
]
| assumption
]
- | auto
+ | autobatch
(*elim H4.
assumption*)
]
| intros.
elim (H i (le_S i n H2) H3).
- auto
+ autobatch
(*apply H8
[ assumption
| apply le_S.
[ intro.
apply (eqb_elim i1 j)
[ simplify.intro.
- auto
+ autobatch
(*rewrite < H6.
assumption*)
| simplify.intro.
- auto
+ autobatch
(*rewrite < H2.
rewrite < H5.
assumption*)
| intro.
apply (eqb_elim i1 j)
[ simplify.intro.
- auto
+ autobatch
(*rewrite > H2.
rewrite < H6.
assumption*)
| intros.
unfold Not.
intro.
- auto
+ autobatch
(*apply H7.
apply (injective_transpose ? ? ? ? H8)*)
]
map_iter_p (S n) p g a f = map_iter_p (S n-k) p g a f.
intros 5.
elim k 3
-[ auto
+[ autobatch
(*rewrite < minus_n_O.
reflexivity*)
| apply (nat_case n1)
[ intros.
rewrite > map_iter_p_S_false
[ reflexivity
- | auto
+ | autobatch
(*apply H2
[ simplify.
apply lt_O_S.
[ reflexivity
| intros.
apply (H2 i H3).
- auto
+ autobatch
(*apply le_S.
assumption*)
]
- | auto
+ | autobatch
(*apply H2
- [ auto
+ [ autobatch
| apply le_n
]*)
]
(\forall i.i \le n \to p i = false) \to map_iter_p n p g a f = a.
intros 5.
elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| rewrite > map_iter_p_S_false
[ apply H.
intros.
- auto
+ autobatch
(*apply H1.
apply le_S.
assumption*)
- | auto
+ | autobatch
(*apply H1.
apply le_n*)
]
[ intro.
absurd (k < O)
[ assumption
- | auto
+ | autobatch
(*apply le_to_not_lt.
apply le_O_n*)
]
[ rewrite < Hcut.
rewrite < H.
rewrite < H1 in \vdash (? ? (? % ?) ?).
- auto
+ autobatch
(*rewrite > H.
reflexivity*)
| apply eq_map_iter_p.
| apply not_eq_to_eqb_false.
apply lt_to_not_eq.
apply (le_to_lt_to_lt ? m)
- [ auto
+ [ autobatch
(*apply (trans_le ? (m-k))
[ assumption
- | auto
+ | autobatch
]*)
- | auto
+ | autobatch
(*apply le_S.
apply le_n*)
]
]
| apply not_eq_to_eqb_false.
apply lt_to_not_eq.
- auto
+ autobatch
(*unfold.
- auto*)
+ autobatch*)
]
]
- | auto
+ | autobatch
(*apply le_S_S_to_le.
assumption*)
]
elim n 2
[ absurd (k2 \le O)
[ assumption
- | auto
+ | autobatch
(*apply lt_to_not_le.
apply (trans_lt ? k1 ? H2 H3)*)
]
cut (k1 = n1 - (n1 -k1))
[ rewrite > Hcut.
apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
- [ cut (k1 \le n1);auto
+ [ cut (k1 \le n1);autobatch
| assumption
- | auto
+ | autobatch
(*rewrite < Hcut.
assumption*)
| rewrite < Hcut.
intros.
apply (H9 i H10).
- auto
+ autobatch
(*unfold.
- auto*)
+ autobatch*)
]
| apply sym_eq.
- auto
+ autobatch
(*apply plus_to_minus.
- auto*)
+ autobatch*)
]
| intros.
cut ((S n1) \neq k1)
apply eq_f.
apply (H3 H5)
[ elim (le_to_or_lt_eq ? ? H6)
- [ auto
+ [ autobatch
| absurd (S n1=k2)
- [ auto
+ [ autobatch
(*apply sym_eq.
assumption*)
| assumption
[ rewrite > map_iter_p_S_false
[ apply (H3 H5)
[ elim (le_to_or_lt_eq ? ? H6)
- [ auto
- | (*l'invocazione di auto qui genera segmentation fault*)
+ [ autobatch
+ | (*l'invocazione di autobatch qui genera segmentation fault*)
absurd (S n1=k2)
- [ auto
+ [ autobatch
(*apply sym_eq.
assumption*)
| assumption
right.
apply (ex_intro ? ? O).
split
- [ auto
+ [ autobatch
(*split
[ apply le_n
| assumption
| intros.
absurd (O<i)
[ assumption
- | auto
+ | autobatch
(*apply le_to_not_lt.
assumption*)
]
| intros.
absurd (S n1<i)
[ assumption
- | auto
+ | autobatch
(*apply le_to_not_lt.
assumption*)
]
[ left.
intros.
elim (le_to_or_lt_eq m (S n1) H3)
- [ auto
+ [ autobatch
(*apply H1.
apply le_S_S_to_le.
assumption*)
- | auto
+ | autobatch
(*rewrite > H4.
assumption*)
]
elim H4.
apply (ex_intro ? ? a).
split
- [ auto
+ [ autobatch
(*split
[ apply le_S.
assumption
]*)
| intros.
elim (le_to_or_lt_eq i (S n1) H9)
- [ auto
+ [ autobatch
(*apply H5
[ assumption
| apply le_S_S_to_le.
assumption
]*)
- | auto
+ | autobatch
(*rewrite > H10.
assumption*)
]
| unfold.
intro.
apply not_eq_true_false.
- auto
+ autobatch
(*rewrite < H3.
apply H2.
assumption*)
elim H3.clear H3.
elim H4.clear H4.
split
- [ auto
+ [ autobatch
(*split
[ split
[ assumption
rewrite > H2.
left.
elim H3 2.
- (*qui la tattica auto non conclude il goal, concluso invece con l'invocazione
+ (*qui la tattica autobatch non conclude il goal, concluso invece con l'invocazione
*della sola tattica assumption
*)
assumption
apply not_eq_true_false.
rewrite < H4.
elim H3.
- auto
+ autobatch
(*clear H3.
apply (H6 j H2).assumption*)
]
intros.
absurd (m \le O)
[ assumption
- | auto
+ | autobatch
(*apply lt_to_not_le.
assumption*)
]
right.
apply (ex_intro ? ? (S n1)).
split
- [ auto
+ [ autobatch
(*split
[ split
[ assumption
| assumption
]*)
| intros.
- auto
+ autobatch
(*apply (H4 i H6).
apply le_S_S_to_le.
assumption*)
left.
intros.
elim (le_to_or_lt_eq ? ? H7)
- [ auto
+ [ autobatch
(*apply H4
[ assumption
| apply le_S_S_to_le.
assumption
]*)
- | auto
+ | autobatch
(*rewrite > H8.
assumption*)
]
apply (ex_intro ? ? a).
split
[ split
- [ auto
+ [ autobatch
(*split
[ assumption
| apply le_S.
]*)
| assumption
]
- | (*qui auto non chiude il goal, chiuso invece mediante l'invocazione
+ | (*qui autobatch non chiude il goal, chiuso invece mediante l'invocazione
*della sola tattica assumption
*)
assumption
]
]
- | auto
+ | autobatch
(*apply le_S_S_to_le.
assumption*)
]
apply (nat_elim2 ? ? ? ? n m)
[ simplify.
intros.
- auto
+ autobatch
| intros 2.
- auto
+ autobatch
(*rewrite < minus_n_O.
intro.
assumption*)
| intros.
simplify.
cut (n1 < m1+p)
- [ auto
+ [ autobatch
| apply H.
apply H1
]
[ simplify.
intros 3.
apply (le_n_O_elim ? H).
- auto
+ autobatch
(*simplify.
intros.
assumption*)
| intros.
simplify.
apply H
- [ auto
+ [ autobatch
(*apply le_S_S_to_le.
assumption*)
| apply le_S_S_to_le.
theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
intros.
apply sym_eq.
-auto.
+autobatch.
(*apply plus_to_minus.
-auto.*)
+autobatch.*)
qed.
theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
elim (decidable_n2 p n (S n -m) H4 H6)
[ apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
[ assumption
- | auto
+ | autobatch
(*unfold.
- auto*)
+ autobatch*)
| apply le_n
| assumption
| assumption
| intros.
- auto
+ autobatch
(*apply H7
[ assumption
| apply le_S_S_to_le.
[ rewrite > Hcut1.
apply H2
[ apply lt_plus_to_lt_minus
- [ auto
+ [ autobatch
(*apply le_S.
assumption*)
| rewrite < sym_plus.
- auto
+ autobatch
(*apply lt_minus_to_lt_plus.
assumption*)
]
| rewrite < Hcut1.
- auto
+ autobatch
(*apply (trans_lt ? (S n -m));
assumption*)
| rewrite < Hcut1.
assumption
| assumption
- | auto
+ | autobatch
(*rewrite < Hcut1.
assumption*)
]
- | auto
+ | autobatch
(*apply minus_m_minus_mn.
apply le_S.
assumption*)
| apply (eq_map_iter_p_transpose1 p f H H1)
[ assumption
| assumption
- | auto
+ | autobatch
(*apply le_S.
assumption*)
| assumption
| assumption
- | (*qui auto non chiude il goal, chiuso dall'invocazione della singola
+ | (*qui autobatch non chiude il goal, chiuso dall'invocazione della singola
* tattica assumption
*)
assumption
[ cut (a1 = (S n) -(S n -a1))
[ apply H2
[ apply lt_plus_to_lt_minus
- [ auto
+ [ autobatch
(*apply le_S.
assumption*)
| rewrite < sym_plus.
- auto
+ autobatch
(*apply lt_minus_to_lt_plus.
assumption*)
]
| rewrite < Hcut1.
- auto
+ autobatch
(*apply (trans_lt ? (S n -m))
[ assumption
| assumption
| rewrite < Hcut1.
assumption
| assumption
- | auto
+ | autobatch
(*rewrite < Hcut1.
assumption*)
]
- | auto
+ | autobatch
(*apply minus_m_minus_mn.
apply le_S.
assumption*)
rewrite < H12 in \vdash (? (? %) ?).
assumption
]
- | auto
+ | autobatch
(*apply minus_m_minus_mn.
apply le_S.
assumption*)
]
]
]
-| auto
+| autobatch
(*apply minus_m_minus_mn.
apply le_S.
assumption*)
\to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
intros.
elim (le_to_or_lt_eq ? ? H3)
-[ apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2);auto
+[ apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2);autobatch
(*[ apply le_S_S_to_le.
assumption
| assumption
| rewrite > H6.
apply eq_map_iter_p.
intros.
- auto
+ autobatch
(*apply eq_f.
apply sym_eq.
apply transpose_i_i.*)
| apply (le_n_O_elim ? H4).
unfold.
intro.
- (*l'invocazione di auto in questo punto genera segmentation fault*)
+ (*l'invocazione di autobatch in questo punto genera segmentation fault*)
apply not_eq_true_false.
- (*l'invocazione di auto in questo punto genera segmentation fault*)
+ (*l'invocazione di autobatch in questo punto genera segmentation fault*)
rewrite < H9.
- (*l'invocazione di auto in questo punto genera segmentation fault*)
+ (*l'invocazione di autobatch in questo punto genera segmentation fault*)
rewrite < H1.
- (*l'invocazione di auto in questo punto genera segmentation fault*)
+ (*l'invocazione di autobatch in questo punto genera segmentation fault*)
reflexivity
]
qed.
map_iter_p n p g a f = map_iter_p n p (compose ? ? ? g h) a f .
intros 5.
elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| apply (bool_elim ? (p (S n1)))
elim H6.
clear H6.
apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
- [ apply (permut_p_O ? ? ? H3 H4);auto
+ [ apply (permut_p_O ? ? ? H3 H4);autobatch
(*[ apply le_n
| assumption
]*)
cut (h i \neq h (S n1))
[ rewrite > (not_eq_to_eqb_false ? ? Hcut).
simplify.
- auto
+ autobatch
(*apply le_S_S_to_le.
assumption*)
| apply H9
[ apply H5
| apply le_n
| apply lt_to_not_eq.
- auto
+ autobatch
(*unfold.
apply le_S_S.
assumption*)
apply (eqb_elim (S n1) (h (S n1)))
[ intro.
absurd (h i = h (S n1))
- [ auto
+ [ autobatch
(*rewrite > H8.
assumption*)
| apply H9
[ assumption
| apply le_n
| apply lt_to_not_eq.
- auto
+ autobatch
(*unfold.
apply le_S_S.
assumption*)
elim (H3 (S n1) (le_n ? ) H5).
elim H13.clear H13.
elim (le_to_or_lt_eq ? ? H15)
- [ auto
+ [ autobatch
(*apply le_S_S_to_le.
assumption*)
| apply False_ind.
- auto
+ autobatch
(*apply H12.
apply sym_eq.
assumption*)
[ intro.
apply (eqb_elim (h i) (h (S n1)))
[ intro.
- (*NB: qui auto non chiude il goal*)
+ (*NB: qui autobatch non chiude il goal*)
simplify.
assumption
| intro.
simplify.
elim (H3 (S n1) (le_n ? ) H5).
- auto
+ autobatch
(*elim H10.
assumption*)
]
| intro.
apply (eqb_elim (h i) (h (S n1)))
[ intro.
- (*NB: qui auto non chiude il goal*)
+ (*NB: qui autobatch non chiude il goal*)
simplify.
assumption
| intro.
simplify.
elim (H3 i (le_S ? ? H6) H7).
- auto
+ autobatch
(*elim H10.
assumption*)
]
]
| apply eq_map_iter_p.
intros.
- auto
+ autobatch
(*rewrite > transpose_transpose.
reflexivity*)
]
split
[ split
[ elim (le_to_or_lt_eq ? ? H10)
- [ auto
+ [ autobatch
(*apply le_S_S_to_le.assumption*)
| absurd (p (h i) = true)
[ assumption
| rewrite > H12.
rewrite > H5.
unfold.intro.
- (*l'invocazione di auto qui genera segmentation fault*)
+ (*l'invocazione di autobatch qui genera segmentation fault*)
apply not_eq_true_false.
- (*l'invocazione di auto qui genera segmentation fault*)
+ (*l'invocazione di autobatch qui genera segmentation fault*)
apply sym_eq.
- (*l'invocazione di auto qui genera segmentation fault*)
+ (*l'invocazione di autobatch qui genera segmentation fault*)
assumption
]
]
| assumption
]
| intros.
- apply H9;auto
+ apply H9;autobatch
(*[ assumption
| apply (le_S ? ? H13)
| assumption
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/minimization".
+set "baseuri" "cic:/matita/library_autobatch/nat/minimization".
include "auto/nat/minus.ma".
theorem max_O_f : \forall f: nat \to bool. max O f = O.
intro. simplify.
-elim (f O); auto.
+elim (f O); autobatch.
(*[ simplify.
reflexivity
| simplify.
theorem max_S_max : \forall f: nat \to bool. \forall n:nat.
(f (S n) = true \land max (S n) f = (S n)) \lor
(f (S n) = false \land max (S n) f = max n f).
-intros.simplify.elim (f (S n));auto.
+intros.simplify.elim (f (S n));autobatch.
(*[ simplify.
left.
split;reflexivity
[ rewrite > max_O_f.
apply le_n
| simplify.
- elim (f (S n1));simplify;auto.
+ elim (f (S n1));simplify;autobatch.
(*[ simplify.
apply le_n
| simplify.
[ apply H2
| cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor
(f (S n1) = false \land max (S n1) f = max n1 f))
- [ elim Hcut;elim H3;rewrite > H5;auto
+ [ elim Hcut;elim H3;rewrite > H5;autobatch
(*[ elim H3.
rewrite > H5.
apply le_S.
m\le n \to f m = true \to m \le max n f.
intros 3.
elim n
-[ auto.
+[ autobatch.
(*apply (le_n_O_elim m H).
apply le_O_n.*)
| apply (le_n_Sm_elim m n1 H1);intro
- [ apply (trans_le ? (max n1 f)); auto
+ [ apply (trans_le ? (max n1 f)); autobatch
(*[ apply H
[apply le_S_S_to_le.
assumption
| simplify.
rewrite < H3.
rewrite > H2.
- auto
+ autobatch
(*simplify.
apply le_n.*)
]
elim H1.
generalize in match H3.
apply (le_n_O_elim a H2).
- auto
+ autobatch
(*intro.
simplify.
rewrite > H4.
[ true \Rightarrow (S n1)
| false \Rightarrow (max n1 f)])) = true))
- [ auto
+ [ autobatch
(*simplify.
intro.
assumption.*)
apply (le_n_Sm_elim a n1 H4)
[ intros.
apply (ex_intro nat ? a).
- auto
+ autobatch
(*split
[ apply le_S_S_to_le.
assumption.
| assumption.
]*)
| intros.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
apply False_ind.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
apply not_eq_true_false.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
rewrite < H2.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
rewrite < H7.
- (* una chiamata di auto in questo punto genera segmentation fault*)
+ (* una chiamata di autobatch in questo punto genera segmentation fault*)
rewrite > H6.
reflexivity.
]
\forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
intros 2.
elim n
-[ absurd (le m O);auto
+[ absurd (le m O);autobatch
(*[ assumption
| cut (O < m)
[ apply (lt_O_n_elim m Hcut).
| elim H3.
apply (le_n_Sm_elim m n1 H2)
[ intro.
- apply H;auto
+ apply H;autobatch
(*[ rewrite < H6.
assumption
| apply le_S_S_to_le.
assumption
]*)
| intro.
- auto
+ autobatch
(*rewrite > H7.
assumption*)
]
theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
min_aux O i f = i.
intros.simplify.
-(*una chiamata di auto a questo punto porta ad un'elaborazione molto lunga (forse va
+(*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
in loop): dopo circa 3 minuti non era ancora terminata.
*)
rewrite < minus_n_O.
-(*una chiamata di auto a questo punto porta ad un'elaborazione molto lunga (forse va
+(*una chiamata di autobatch a questo punto porta ad un'elaborazione molto lunga (forse va
in loop): dopo circa 3 minuti non era ancora terminata.
*)
-elim (f i); auto.
+elim (f i); autobatch.
(*[ reflexivity.
simplify
| reflexivity
theorem min_O_f : \forall f:nat \to bool.
min O f = O.
intro.
-(* una chiamata di auto a questo punto NON conclude la dimostrazione*)
+(* una chiamata di autobatch a questo punto NON conclude la dimostrazione*)
apply (min_aux_O_f f O).
qed.
theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
(f (n -(S i)) = true \land min_aux (S i) n f = (n - (S i))) \lor
(f (n -(S i)) = false \land min_aux (S i) n f = min_aux i n f).
-intros.simplify.elim (f (n - (S i)));auto.
+intros.simplify.elim (f (n - (S i)));autobatch.
(*[ simplify.
left.
split;reflexivity.
elim H1.
elim H2.
cut (a = m)
- [ auto.
+ [ autobatch.
(*rewrite > (min_aux_O_f f).
rewrite < Hcut.
assumption*)
(f (m-(S n)) = b) \to (f (match b in bool with
[ true \Rightarrow m-(S n)
| false \Rightarrow (min_aux n m f)])) = true))
- [ auto
+ [ autobatch
(*simplify.
intro.
assumption.*)
elim H4.
elim (le_to_or_lt_eq (m-(S n)) a H6)
[ apply (ex_intro nat ? a).
- split;auto
- (*[ auto.split
+ split;autobatch
+ (*[ autobatch.split
[ apply lt_minus_S_n_to_le_minus_n.
assumption
| assumption
| assumption
]*)
| absurd (f a = false)
- [ (* una chiamata di auto in questo punto genera segmentation fault*)
+ [ (* una chiamata di autobatch in questo punto genera segmentation fault*)
rewrite < H8.
assumption.
| rewrite > H5.
| elim H3.
elim (le_to_or_lt_eq (n -(S n1)) m)
[ apply H
- [ auto
+ [ autobatch
(*apply lt_minus_S_n_to_le_minus_n.
assumption*)
| rewrite < H6.
intros 3.
elim off
[ rewrite < minus_n_O.
- auto
+ autobatch
(*rewrite > (min_aux_O_f f n).
apply le_n.*)
| elim (min_aux_S f n1 n)
[ elim H1.
- auto
+ autobatch
(*rewrite > H3.
apply le_n.*)
| elim H1.
rewrite > H3.
- auto
+ autobatch
(*apply (trans_le (n-(S n1)) (n-n1))
[ apply monotonic_le_minus_r.
apply le_n_Sn.
elim off
[ simplify.
rewrite < minus_n_O.
- elim (f n);auto
+ elim (f n);autobatch
(*[simplify.
apply le_n.
| simplify.
apply le_n.
]*)
| simplify.
- elim (f (n -(S n1)));simplify;auto
+ elim (f (n -(S n1)));simplify;autobatch
(*[ apply le_plus_to_minus.
rewrite < sym_plus.
apply le_plus_n
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/minus".
+set "baseuri" "cic:/matita/library_autobatch/nat/minus".
include "auto/nat/le_arith.ma".
include "auto/nat/compare.ma".
| (S q) \Rightarrow minus p q ]].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/library_auto/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (cic:/matita/library_autobatch/nat/minus/minus.con x y).
theorem minus_n_O: \forall n:nat.n=n-O.
intros.
elim n;
-auto. (* applico auto su entrambi i goal aperti*)
+autobatch. (* applico autobatch su entrambi i goal aperti*)
(*simplify;reflexivity.*)
qed.
theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
intro.
elim n
-[ auto
+[ autobatch
(*simplify.reflexivity.*)
| elim H.
reflexivity
apply (nat_elim2
(\lambda n,m.m \leq n \to (S n)-m = S (n-m)));intros
[ apply (le_n_O_elim n1 H).
- auto
+ autobatch
(*simplify.
reflexivity.*)
-| auto
+| autobatch
(*simplify.
reflexivity.*)
| rewrite < H
[ reflexivity
- | auto
+ | autobatch
(*apply le_S_S_to_le.
assumption.*)
]
apply (nat_elim2
(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m));intros
[ apply (le_n_O_elim ? H).
- auto
+ autobatch
(*simplify.
rewrite < minus_n_O.
reflexivity.*)
-| auto
+| autobatch
(*simplify.
reflexivity.*)
| simplify.
- auto
+ autobatch
(*apply H.
apply le_S_S_to_le.
assumption.*)
[ rewrite < minus_n_O.
apply plus_n_O.
| elim n2
- [ auto
+ [ autobatch
(*simplify.
apply minus_n_n.*)
| rewrite < plus_n_Sm.
apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m));intros
[ apply (le_n_O_elim n1 H).
reflexivity
-| auto
+| autobatch
(*simplify.
rewrite < plus_n_O.
reflexivity.*)
simplify.
apply eq_f.
rewrite < sym_plus.
- auto
+ autobatch
(*apply H.
apply le_S_S_to_le.
assumption.*)
theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
n = m+p.
-intros.apply (trans_eq ? ? ((n-m)+m));auto.
+intros.apply (trans_eq ? ? ((n-m)+m));autobatch.
(*[ apply plus_minus_m_m.
apply H.
| elim H1.
rewrite < H.
rewrite < sym_plus.
symmetry.
-auto.
+autobatch.
(*apply plus_minus_m_m.
rewrite > H.
rewrite > sym_plus.
intro.
apply (lt_O_n_elim m H1).
intro.
-auto.
+autobatch.
(*simplify.reflexivity.*)
qed.
n \leq m \to n-m = O.
intros 2.
apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O));intros
-[ auto
+[ autobatch
(*simplify.
reflexivity.*)
| apply False_ind.
- auto
+ autobatch
(*apply not_le_Sn_O.
goal 15.*) (*prima goal 13*)
(* effettuando un'esecuzione passo-passo, quando si arriva a dover
*)
(*apply H.*)
| simplify.
- auto
+ autobatch
(*apply H.
apply le_S_S_to_le.
apply H1.*)
intros.
elim H
[ elim (minus_Sn_n n).apply le_n
-| rewrite > minus_Sn_m;auto
+| rewrite > minus_Sn_m;autobatch
(*apply le_S.assumption.
apply lt_to_le.assumption.*)
]
| rewrite < minus_n_O.
apply le_n.
]
-| auto
+| autobatch
(*simplify.apply le_n_Sn.*)
| simplify.apply H.
]
theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
intros 3.
-auto.
+autobatch.
(*simplify.
intro.
apply (trans_le (m-n) (S (m-(S n))) p).
theorem le_minus_m: \forall n,m:nat. n-m \leq n.
intros.apply (nat_elim2 (\lambda m,n. n-m \leq n));intros
-[ auto
+[ autobatch
(*rewrite < minus_n_O.
apply le_n.*)
-| auto
+| autobatch
(*simplify.
apply le_n.*)
| simplify.
- auto
+ autobatch
(*apply le_S.
assumption.*)
]
apply (lt_O_n_elim m H1).
intro.
simplify.
-auto.
+autobatch.
(*unfold lt.
apply le_S_S.
apply le_minus_m.*)
assumption
| simplify.
intros.
- auto
+ autobatch
(*apply le_S_S.
apply H.
assumption.*)
| rewrite < minus_n_O.
apply le_minus_m.
| elim a
- [ auto
+ [ autobatch
(*simplify.
apply le_n.*)
| simplify.
- auto
+ autobatch
(*apply H.
apply le_S_S_to_le.
assumption.*)
intros 2.
apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)))
[ intros.
- auto
+ autobatch
(*simplify.
apply le_O_n.*)
| intros 2.
rewrite < plus_n_O.
- auto
+ autobatch
(*intro.
simplify.
assumption.*)
apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))));intro
[ rewrite < plus_n_O.
rewrite < minus_n_O.
- auto
+ autobatch
(*intro.
assumption.*)
| intro.
cut (n=O)
- [ auto
+ [ autobatch
(*rewrite > Hcut.
apply le_O_n.*)
| apply sym_eq.
apply le_n_O_to_eq.
- auto
+ autobatch
(*apply (trans_le ? (n+(S n1)))
[ rewrite < sym_plus.
apply le_plus_n
[ intro.
rewrite < plus_n_O.
rewrite < minus_n_O.
- auto
+ autobatch
(*intro.
assumption.*)
| simplify.
unfold lt.
apply le_S_S.
rewrite < plus_n_Sm.
- auto
+ autobatch
(*apply H.
apply H1.*)
]
intros.
apply ((leb_elim z y));intro
[ cut (x*(y-z)+x*z = (x*y-x*z)+x*z)
- [ auto
+ [ autobatch
(*apply (inj_plus_l (x*z)).
assumption.*)
| apply (trans_eq nat ? (x*y))
[ rewrite < distr_times_plus.
- auto
+ autobatch
(*rewrite < (plus_minus_m_m ? ? H).
reflexivity.*)
- | rewrite < plus_minus_m_m;auto
+ | rewrite < plus_minus_m_m;autobatch
(*[ reflexivity.
| apply le_times_r.
assumption.
]
| rewrite > eq_minus_n_m_O
[ rewrite > (eq_minus_n_m_O (x*y))
- [ auto
+ [ autobatch
(*rewrite < sym_times.
simplify.
reflexivity.*)
| apply le_times_r.
apply lt_to_le.
- auto
+ autobatch
(*apply not_le_to_lt.
assumption.*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply not_le_to_lt.
assumption.*)
apply plus_to_minus.
rewrite > sym_plus in \vdash (? ? ? %).
rewrite > assoc_plus.
-auto.
+autobatch.
(*rewrite < plus_minus_m_m.
reflexivity.
assumption.
rewrite > (sym_plus p).
rewrite < plus_minus_m_m
[ rewrite > sym_plus.
- rewrite < plus_minus_m_m ; auto
+ rewrite < plus_minus_m_m ; autobatch
(*[ reflexivity.
| apply (trans_le ? (m+p))
[ rewrite < sym_plus.
| apply le_plus_to_minus.
apply lt_to_le.
rewrite < sym_plus.
- auto
+ autobatch
(*apply not_le_to_lt.
assumption.*)
]
- | auto
+ | autobatch
(*apply lt_to_le.
apply not_le_to_lt.
assumption.*)
rewrite < assoc_plus.
rewrite < plus_minus_m_m;
[ rewrite < sym_plus.
- auto
+ autobatch
(*rewrite < plus_minus_m_m
[ reflexivity
| assumption
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/nat".
+set "baseuri" "cic:/matita/library_autobatch/nat/nat".
include "higher_order_defs/functions.ma".
| (S p) \Rightarrow p ].
theorem pred_Sn : \forall n:nat.n=(pred (S n)).
- auto.
+ autobatch.
(*intros. reflexivity.*)
qed.
intros.
rewrite > pred_Sn.
rewrite > (pred_Sn y).
- auto.
+ autobatch.
(*apply eq_f.
assumption.*)
qed.
intros.
unfold Not.
intros.
- auto.
+ autobatch.
(*apply H.
apply injective_S.
assumption.*)
(n=O \to P O) \to (\forall m:nat. (n=(S m) \to P (S m))) \to P n.
intros 2;
elim n
- [ auto
+ [ autobatch
(*apply H;
reflexivity*)
- | auto
+ | autobatch
(*apply H2;
reflexivity*) ]
qed.
| apply (nat_case m)
[ apply H1
|intro;
- auto
+ autobatch
(*apply H2;
apply H3*)
]
intros.unfold decidable.
apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))))
[ intro; elim n1
- [auto
+ [autobatch
(*left;
reflexivity*)
- |auto
+ |autobatch
(*right;
apply not_eq_O_S*) ]
| intro;
right;
intro;
apply (not_eq_O_S n1);
- auto
+ autobatch
(*apply sym_eq;
assumption*)
| intros; elim H
- [ auto
+ [ autobatch
(*left;
apply eq_f;
assumption*)
| right;
intro;
- auto
+ autobatch
(*apply H1;
apply inj_S;
assumption*)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/nth_prime".
+set "baseuri" "cic:/matita/library_autobatch/nat/nth_prime".
include "auto/nat/primes.ma".
include "auto/nat/lt_arith.ma".
intro.
apply (not_divides_S_fact n (smallest_factor(S n!)))
[ apply lt_SO_smallest_factor.
- unfold lt.auto
+ unfold lt.autobatch
(*apply le_S_S.
apply le_SO_fact*)
| assumption
-| auto
+| autobatch
(*apply divides_smallest_factor_n.
unfold lt.
apply le_S_S.
intros.
elim H
[ apply (ex_intro nat ? (S(S O))).
- split;auto
+ split;autobatch
(*[ split
[ apply (le_n (S(S O)))
| apply (le_n (S(S O)))
]*)
| apply (ex_intro nat ? (smallest_factor (S (S n1)!))).
split
- [ auto
+ [ autobatch
(*split
[ apply smallest_factor_fact
| apply le_smallest_factor_n
]*)
| (* Andrea: ancora hint non lo trova *)
apply prime_smallest_factor_n.
- unfold lt.auto
+ unfold lt.autobatch
(*apply le_S.
apply le_SSO_fact.
unfold lt.
it must compute factorial of 7 ...*)
(*
theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
-auto.
+autobatch.
(*normalize.reflexivity.*)
qed.
theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
-auto.
+autobatch.
(*normalize.reflexivity.*)
qed.
theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
-auto.
+autobatch.
(*normalize.reflexivity.*)
qed.
*)
theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
intro.
apply (nat_case n)
-[ auto
+[ autobatch
(*simplify.
apply (primeb_to_Prop (S(S O)))*)
| intro.
exact (smallest_factor_fact (nth_prime m))
| (* maybe we could factorize this proof *)
apply plus_to_minus.
- auto
+ autobatch
(*apply plus_minus_m_m.
apply le_S_S.
apply le_n_fact_n*)
]
| apply prime_to_primeb_true.
apply prime_smallest_factor_n.
- unfold lt.auto
+ unfold lt.autobatch
(*apply le_S_S.
apply le_SO_fact*)
]
[ rewrite < Hcut in \vdash (? % ?).
apply le_min_aux
| apply plus_to_minus.
- auto
+ autobatch
(*apply plus_minus_m_m.
apply le_S_S.
apply le_n_fact_n*)
(nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
theorem injective_nth_prime: injective nat nat nth_prime.
-auto.
+autobatch.
(*apply increasing_to_injective.
apply increasing_nth_prime.*)
qed.
theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
intros.
-(*usando la tattica auto qui, dopo svariati minuti la computazione non era
+(*usando la tattica autobatch qui, dopo svariati minuti la computazione non era
* ancora terminata
*)
elim n
-[ unfold lt.auto
+[ unfold lt.autobatch
(*apply le_n*)
-| auto
+| autobatch
(*apply (trans_lt ? (nth_prime n1))
[ assumption
| apply lt_nth_prime_n_nth_prime_Sn
theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
intros.
-auto.
+autobatch.
(*apply (trans_lt O (S O))
[ unfold lt.
apply le_n
theorem ex_m_le_n_nth_prime_m:
\forall n: nat. nth_prime O \le n \to
\exists m. nth_prime m \le n \land n < nth_prime (S m).
-auto.
+autobatch.
(*intros.
apply increasing_to_le2
[ exact lt_nth_prime_n_nth_prime_Sn
[ rewrite > Hcut.
assumption
| apply plus_to_minus.
- auto
+ autobatch
(*apply plus_minus_m_m.
apply le_S_S.
apply le_n_fact_n*)
[ elim Hcut1
[ absurd (prime p)
[ assumption
- | auto
+ | autobatch
(*apply (lt_nth_prime_to_not_prime a);assumption*)
]
- | auto
+ | autobatch
(*apply (ex_intro nat ? a).
assumption*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/ord".
+set "baseuri" "cic:/matita/library_autobatch/nat/ord".
include "datatypes/constructors.ma".
include "auto/nat/exp.ma".
include "auto/nat/gcd.ma".
-include "auto/nat/relevant_equations.ma". (* required by auto paramod *)
+include "auto/nat/relevant_equations.ma". (* required by autobatch paramod *)
(* this definition of log is based on pairs, with a remainder *)
[ rewrite > (plus_n_O (m*(n1 / m))).
rewrite < H2.
rewrite > sym_times.
- auto
+ autobatch
(*rewrite < div_mod
[ reflexivity
| assumption
rewrite < plus_n_O.
apply (nat_case p)
[ simplify.
- elim (n \mod m);auto
+ elim (n \mod m);autobatch
(*[ simplify.
reflexivity
| simplify.
cut (O < n \mod m \lor O = n \mod m)
[ elim Hcut
[ apply (lt_O_n_elim (n \mod m) H3).
- intros.auto
+ intros.autobatch
(*simplify.
reflexivity*)
- | apply False_ind.auto
+ | apply False_ind.autobatch
(*apply H1.
apply sym_eq.
assumption*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply le_O_n*)
]
fold simplify (m \sup (S n1)).
cut ((m \sup (S n1) *n) / m = m \sup n1 *n)
[ rewrite > Hcut1.
- rewrite > (H2 m1);auto
+ rewrite > (H2 m1);autobatch
(*[ simplify.
reflexivity
| apply le_S_S_to_le.
| (* mod_exp = O *)
apply divides_to_mod_O
[ assumption
- | simplify.auto
+ | simplify.autobatch
(*rewrite > assoc_times.
apply (witness ? ? (m \sup n1 *n)).
reflexivity*)
[ (pair q r) \Rightarrow r \mod m \neq O].
intro.
elim p
-[ absurd (O < n);auto
+[ absurd (O < n);autobatch
(*[ assumption
| apply le_to_not_lt.
assumption
elim (p_ord_aux n (n1 / m) m).
apply H5
[ assumption
- | auto
+ | autobatch
(*apply eq_mod_O_to_lt_O_div
[ apply (trans_lt ? (S O))
[ unfold lt.
| assumption
| assumption
]*)
- | apply le_S_S_to_le.auto
+ | apply le_S_S_to_le.autobatch
(*apply (trans_le ? n1)
[ change with (n1 / m < n1).
apply lt_div_n_m_n;assumption
]*)
]
| intros.
- simplify.auto
+ simplify.autobatch
(*rewrite > H4.
unfold Not.
intro.
[ assumption
| unfold.
intro.
- auto
+ autobatch
(*apply H1.
apply mod_O_to_divides
[ assumption
]*)
| apply (trans_le ? (p \sup q))
[ cut ((S O) \lt p)
- [ auto
+ [ autobatch
(*elim q
[ simplify.
apply le_n_Sn
| apply not_eq_to_le_to_lt
[ unfold.
intro.
- auto
+ autobatch
(*apply H1.
rewrite < H3.
apply (witness ? r r ?).
change with (O \lt r).
apply not_eq_to_le_to_lt
[ unfold.
- intro.auto
+ intro.autobatch
(*apply H1.rewrite < H3.
apply (witness ? ? O ?).rewrite < times_n_O.
reflexivity*)
unfold p_ord in H2.
split
[ unfold.intro.
- apply (p_ord_aux_to_not_mod_O n n p q r);auto
+ apply (p_ord_aux_to_not_mod_O n n p q r);autobatch
(*[ assumption
| assumption
| apply le_n
| assumption
]
]*)
-| apply (p_ord_aux_to_exp n);auto
+| apply (p_ord_aux_to_exp n);autobatch
(*[ apply (trans_lt ? (S O))
[ unfold.
apply le_n
[ elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
apply p_ord_exp1
- [ auto
+ [ autobatch
(*apply (trans_lt ? (S O))
[ unfold.
apply le_n
]*)
| unfold.
intro.
- elim (divides_times_to_divides ? ? ? H H9);auto
+ elim (divides_times_to_divides ? ? ? H H9);autobatch
(*[ apply (absurd ? ? H10 H5)
| apply (absurd ? ? H10 H7)
]*)
| (* rewrite > H6.
rewrite > H8. *)
- auto paramodulation
+ autobatch paramodulation
]
| unfold prime in H.
elim H.
\to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
intros.
rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
-(fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2);auto.
+(fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2);autobatch.
(*[ simplify.
reflexivity
| apply eq_pair_fst_snd
theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
intros.
apply p_ord_exp1
-[ auto
+[ autobatch
(*apply (trans_lt ? (S O))
[ unfold.
apply le_n
]*)
| unfold.
intro.
- apply (absurd ? ? H).auto
+ apply (absurd ? ? H).autobatch
(*apply le_to_not_lt.
apply divides_to_le
[ unfold.
apply le_n
| assumption
]*)
-| auto
+| autobatch
(*rewrite < times_n_SO.
apply exp_n_SO*)
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/orders".
+set "baseuri" "cic:/matita/library_autobatch/nat/orders".
include "auto/nat/nat.ma".
include "higher_order_defs/ordering.ma".
| le_S : \forall m:nat. le n m \to le n (S m).
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/library_auto/nat/orders/le.ind#xpointer(1/1) x y).
+interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/library_autobatch/nat/orders/le.ind#xpointer(1/1) x y).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'neither less nor equal to'" 'nleq x y =
(cic:/matita/logic/connectives/Not.con
- (cic:/matita/library_auto/nat/orders/le.ind#xpointer(1/1) x y)).
+ (cic:/matita/library_autobatch/nat/orders/le.ind#xpointer(1/1) x y)).
definition lt: nat \to nat \to Prop \def
\lambda n,m:nat.(S n) \leq m.
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'less than'" 'lt x y = (cic:/matita/library_auto/nat/orders/lt.con x y).
+interpretation "natural 'less than'" 'lt x y = (cic:/matita/library_autobatch/nat/orders/lt.con x y).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'not less than'" 'nless x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/nat/orders/lt.con x y)).
+ (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/nat/orders/lt.con x y)).
definition ge: nat \to nat \to Prop \def
\lambda n,m:nat.m \leq n.
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/library_auto/nat/orders/ge.con x y).
+interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/library_autobatch/nat/orders/ge.con x y).
definition gt: nat \to nat \to Prop \def
\lambda n,m:nat.m<n.
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'greater than'" 'gt x y = (cic:/matita/library_auto/nat/orders/gt.con x y).
+interpretation "natural 'greater than'" 'gt x y = (cic:/matita/library_autobatch/nat/orders/gt.con x y).
(*CSC: the URI must disappear: there is a bug now *)
interpretation "natural 'not greater than'" 'ngtr x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/nat/orders/gt.con x y)).
+ (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/nat/orders/gt.con x y)).
theorem transitive_le : transitive nat le.
unfold transitive.
intros.
-elim H1;auto.
+elim H1;autobatch.
(*[ assumption
| apply le_S.
assumption
unfold transitive.
unfold lt.
intros.
-elim H1;auto.
+elim H1;autobatch.
(*apply le_S;assumption.*)
qed.
theorem le_S_S: \forall n,m:nat. n \leq m \to S n \leq S m.
intros.
-elim H;auto.
+elim H;autobatch.
(*[ apply le_n.
| apply le_S.
assumption
theorem le_O_n : \forall n:nat. O \leq n.
intros.
-elim n;auto.
+elim n;autobatch.
(*[ apply le_n
| apply le_S.
assumption
qed.
theorem le_n_Sn : \forall n:nat. n \leq S n.
-intros.auto.
+intros.autobatch.
(*apply le_S.
apply le_n.*)
qed.
theorem le_pred_n : \forall n:nat. pred n \leq n.
intros.
-elim n;auto.
+elim n;autobatch.
(*[ simplify.
apply le_n
| simplify.
theorem le_S_S_to_le : \forall n,m:nat. S n \leq S m \to n \leq m.
intros.
change with (pred (S n) \leq pred (S m)).
-elim H;auto.
+elim H;autobatch.
(*[ apply le_n
| apply (trans_le ? (pred n1))
[ assumption
theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
intros.
elim H
-[ (*qui auto non chiude il goal*)
+[ (*qui autobatch non chiude il goal*)
exact I
-| (*qui auto non chiude il goal*)
+| (*qui autobatch non chiude il goal*)
exact I
]
qed.
unfold Not.
simplify.
intros.
-(*qui auto NON chiude il goal*)
+(*qui autobatch NON chiude il goal*)
apply (leS_to_not_zero ? ? H).
qed.
[ apply not_le_Sn_O
| unfold Not.
simplify.
- intros.auto
+ intros.autobatch
(*cut (S n1 \leq n1).
[ apply H.
assumption
n \leq m \to n < m \lor n = m.
intros.
elim H
-[ auto
+[ autobatch
(*right.
reflexivity*)
| left.
unfold lt.
- auto
+ autobatch
(*apply le_S_S.
assumption*)
]
unfold Not.
intros.
cut ((le (S n) m) \to False)
-[ auto
+[ autobatch
(*apply Hcut.
assumption*)
| rewrite < H1.
theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
simplify.
intros.
-auto.
+autobatch.
(*unfold lt in H.
elim H
[ apply le_S.
qed.
theorem lt_S_to_le : \forall n,m:nat. n < S m \to n \leq m.
-auto.
+autobatch.
(*simplify.
intros.
apply le_S_S_to_le.
intros 2.
apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n))
[ intros.
- apply (absurd (O \leq n1));auto
+ apply (absurd (O \leq n1));autobatch
(*[ apply le_O_n
| assumption
]*)
| unfold Not.
unfold lt.
- intros.auto
+ intros.autobatch
(*apply le_S_S.
apply le_O_n*)
| unfold Not.
apply le_S_S.
apply H.
intros.
- auto
+ autobatch
(*apply H1.
apply le_S_S.
assumption*)
unfold Not.
unfold lt.
intros 3.
-elim H;auto.
+elim H;autobatch.
(*[ apply (not_le_Sn_n n H1)
| apply H2.
apply lt_to_le.
intros.
apply lt_S_to_le.
apply not_le_to_lt.
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
exact H.
qed.
unfold Not.
unfold lt.
apply lt_to_not_le.
-unfold lt.auto.
+unfold lt.autobatch.
(*apply le_S_S.
assumption.*)
qed.
intro.
elim n
[ reflexivity
-| apply False_ind.auto
+| apply False_ind.autobatch
(*apply not_le_Sn_O.
goal 17. apply H1.*)
]
theorem le_n_Sm_elim : \forall n,m:nat.n \leq S m \to
\forall P:Prop. (S n \leq S m \to P) \to (n=S m \to P) \to P.
intros 4.
-elim H;auto.
+elim H;autobatch.
(*[ apply H2.
reflexivity
| apply H3.
lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
apply nat_elim2
[ intros.
- auto
+ autobatch
(*apply le_n_O_to_eq.
assumption*)
-| intros.auto
+| intros.autobatch
(*apply sym_eq.
apply le_n_O_to_eq.
assumption*)
| intros.
- apply eq_f.auto
+ apply eq_f.autobatch
(*apply H
[ apply le_S_S_to_le.assumption
| apply le_S_S_to_le.assumption
(* lt and le trans *)
theorem lt_O_S : \forall n:nat. O < S n.
-intro.auto.
+intro.autobatch.
(*unfold.
apply le_S_S.
apply le_O_n.*)
theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
intros.
-elim H1;auto.
+elim H1;autobatch.
(*[ assumption
| unfold lt.
apply le_S.
intros 4.
elim H
[ assumption
-| apply H2.auto
+| apply H2.autobatch
(*unfold lt.
apply lt_to_le.
assumption*)
qed.
theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
-intros.auto.
+intros.autobatch.
(*apply (trans_lt ? (S n))
[ apply le_n
| assumption
(* other abstract properties *)
theorem antisymmetric_le : antisymmetric nat le.
unfold antisymmetric.
-auto.
+autobatch.
(*intros 2.
apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m)))
[ intros.
qed.
(*NOTA:
- * auto chiude il goal prima della tattica intros 2, tuttavia non chiude gli ultimi
+ * autobatch chiude il goal prima della tattica intros 2, tuttavia non chiude gli ultimi
* 2 rami aperti dalla tattica apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
- * evidentemente auto sfrutta una dimostrazione diversa rispetto a quella proposta
+ * evidentemente autobatch sfrutta una dimostrazione diversa rispetto a quella proposta
* nella libreria
*)
intros.
apply (nat_elim2 (\lambda n,m.decidable (n \leq m)))
[ intros.
- unfold decidable.auto
+ unfold decidable.autobatch
(*left.
apply le_O_n*)
| intros.
unfold decidable.
- auto
+ autobatch
(*right.
exact (not_le_Sn_O n1)*)
| intros 2.
unfold decidable.
intro.
elim H
- [ auto
+ [ autobatch
(*left.
apply le_S_S.
assumption*)
| right.
unfold Not.
- auto
+ autobatch
(*intro.
apply H1.
apply le_S_S_to_le.
theorem decidable_lt: \forall n,m:nat. decidable (n < m).
intros.
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
exact (decidable_le (S n) m).
qed.
(\forall m.(\forall p. (p \lt m) \to P p) \to P m) \to P n.
intros.
cut (\forall q:nat. q \le n \to P q)
-[ auto
+[ autobatch
(*apply (Hcut n).
apply le_n*)
| elim n
| apply H.
intros.
apply H1.
- auto
+ autobatch
(*cut (p < S n1)
[ apply lt_S_to_le.
assumption
unfold increasing.
unfold lt.
intros.
-elim H1;auto.
+elim H1;autobatch.
(*[ apply H
| apply (trans_le ? (f n1))
[ assumption
theorem le_n_fn: \forall f:nat \to nat. (increasing f)
\to \forall n:nat. n \le (f n).
intros.
-elim n;auto.
+elim n;autobatch.
(*[ apply le_O_n
| apply (trans_le ? (S (f n1)))
[ apply le_S_S.
theorem increasing_to_le: \forall f:nat \to nat. (increasing f)
\to \forall m:nat. \exists i. m \le (f i).
-intros.auto.
+intros.autobatch.
(*elim m
[ apply (ex_intro ? ? O).
apply le_O_n
\exists i. (f i) \le m \land m <(f (S i)).
intros.
elim H1
-[ auto.
+[ autobatch.
(*apply (ex_intro ? ? O).
split
[ apply le_n
cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a)))
[ elim Hcut
[ apply (ex_intro ? ? a).
- auto
+ autobatch
(*split
[ apply le_S.
assumption
split
[ rewrite < H7.
apply le_n
- | auto
+ | autobatch
(*rewrite > H7.
apply H*)
]
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply H6*)
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/permutation".
+set "baseuri" "cic:/matita/library_autobatch/nat/permutation".
include "auto/nat/compare.ma".
include "auto/nat/sigma_and_pi.ma".
injn f (S n) \to injn f n.
unfold injn.
intros.
-apply H;auto.
+apply H;autobatch.
(*[ apply le_S.
assumption
| apply le_S.
injective nat nat f \to injn f n.
unfold injective.
unfold injn.
-intros.auto.
+intros.autobatch.
(*apply H.
assumption.*)
qed.
intros.
unfold permut in H.
elim H.
-apply sym_eq.auto.
+apply sym_eq.autobatch.
(*apply le_n_O_to_eq.
apply H1.
apply le_n.*)
[ intros.
cut (f i < S m \lor f i = S m)
[ elim Hcut
- [ auto
+ [ autobatch
(*apply le_S_S_to_le.
assumption*)
| apply False_ind.
assumption
| apply H3
[ apply le_n
- | auto
+ | autobatch
(*apply le_S.
assumption*)
- | auto
+ | autobatch
(*rewrite > H5.
assumption*)
]
]
]
| apply le_to_or_lt_eq.
- auto
+ autobatch
(*apply H2.
apply le_S.
assumption*)
for @{ 'transposition $i $j $n}.
interpretation "natural transposition" 'transposition i j n =
- (cic:/matita/library_auto/nat/permutation/transpose.con i j n).
+ (cic:/matita/library_autobatch/nat/permutation/transpose.con i j n).
lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
intros.
unfold transpose.
-(*dopo circa 6 minuti, l'esecuzione di auto in questo punto non era ancora terminata*)
-rewrite > (eqb_n_n i).auto.
+(*dopo circa 6 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
+rewrite > (eqb_n_n i).autobatch.
(*simplify.
reflexivity.*)
qed.
intros.
unfold transpose.
apply (eqb_elim j i)
-[ auto
+[ autobatch
(*simplify.
intro.
assumption*)
intros.
unfold transpose.
apply (eqb_elim n i)
-[ auto
+[ autobatch
(*intro.
simplify.
apply sym_eq.
assumption*)
| intro.
- auto
+ autobatch
(*simplify.
reflexivity*)
]
apply (eqb_elim n i)
[ apply (eqb_elim n j)
[ intros.
- (*l'esecuzione di auto in questo punto, dopo circa 300 secondi, non era ancora terminata*)
- simplify.auto
+ (*l'esecuzione di autobatch in questo punto, dopo circa 300 secondi, non era ancora terminata*)
+ simplify.autobatch
(*rewrite < H.
rewrite < H1.
reflexivity*)
| intros.
- auto
+ autobatch
(*simplify.
reflexivity*)
]
| apply (eqb_elim n j)
- [ intros.auto
+ [ intros.autobatch
(*simplify.reflexivity *)
- | intros.auto
+ | intros.autobatch
(*simplify.reflexivity*)
]
]
apply (eqb_elim j i)
[ simplify.
intros.
- auto
+ autobatch
(*rewrite > H.
rewrite > H1.
reflexivity*)
| rewrite > (eqb_n_n j).
simplify.
intros.
- auto
+ autobatch
(*apply sym_eq.
assumption*)
]
[ simplify.
rewrite > (eqb_n_n i).
intros.
- auto
+ autobatch
(*simplify.
apply sym_eq.
assumption*)
| simplify.
intros.
- (*l'esecuzione di auto in questo punto, dopo piu' di 6 minuti non era ancora terminata*)
+ (*l'esecuzione di autobatch in questo punto, dopo piu' di 6 minuti non era ancora terminata*)
rewrite > (not_eq_to_eqb_false n i H1).
- (*l'esecuzione di auto in questo punto, dopo piu' alcuni minuti non era ancora terminata*)
- rewrite > (not_eq_to_eqb_false n j H).auto
+ (*l'esecuzione di autobatch in questo punto, dopo piu' alcuni minuti non era ancora terminata*)
+ rewrite > (not_eq_to_eqb_false n j H).autobatch
(*simplify.
reflexivity*)
]
theorem injective_transpose : \forall i,j:nat.
injective nat nat (transpose i j).
unfold injective.
-intros.auto.
+intros.autobatch.
(*rewrite < (transpose_transpose i j x).
rewrite < (transpose_transpose i j y).
apply eq_f.
[ unfold transpose.
intros.
elim (eqb i1 i)
- [ (*qui auto non chiude il goal*)
+ [ (*qui autobatch non chiude il goal*)
simplify.
assumption
| elim (eqb i1 j)
- [ (*aui auto non chiude il goal*)
+ [ (*aui autobatch non chiude il goal*)
simplify.
assumption
- | (*aui auto non chiude il goal*)
+ | (*aui autobatch non chiude il goal*)
simplify.
assumption
]
]
-| auto
+| autobatch
(*apply (injective_to_injn (transpose i j) n).
apply injective_transpose*)
]
split
[ intros.
simplify.
- auto
+ autobatch
(*apply H2.
apply H4.
assumption*)
[ assumption
| assumption
| apply H3
- [ auto
+ [ autobatch
(*apply H4.
assumption*)
- | auto
+ | autobatch
(*apply H4.
assumption*)
| assumption
\forall f:nat \to nat. \forall m,i,j:nat.
i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
intros.
-auto.
+autobatch.
(*apply (permut_fg (transpose i j) f m ? ?)
[ apply permut_transpose;assumption
| assumption
theorem permut_transpose_r:
\forall f:nat \to nat. \forall m,i,j:nat.
i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
-intros.auto.
+intros.autobatch.
(*apply (permut_fg f (transpose i j) m ? ?)
[ assumption
| apply permut_transpose;assumption
simplify.
rewrite > (not_eq_to_eqb_false k i)
[ rewrite > (eqb_n_n k).
- auto
+ autobatch
(*simplify.
reflexivity*)
| unfold Not.
- intro.auto
+ intro.autobatch
(*apply H1.
apply sym_eq.
assumption*)
| assumption
]
| unfold Not.
- intro.auto
+ intro.autobatch
(*apply H2.
apply (trans_eq ? ? n)
[ apply sym_eq.
rewrite > (not_eq_to_eqb_false i j)
[ simplify.
rewrite > (eqb_n_n i).
- auto
+ autobatch
(*simplify.
assumption*)
| unfold Not.
- intro.auto
+ intro.autobatch
(*apply H.
apply sym_eq.
assumption*)
simplify.
rewrite > (not_eq_to_eqb_false n i H3).
rewrite > (not_eq_to_eqb_false n k H5).
- auto
+ autobatch
(*simplify.
reflexivity*)
]
[ apply (not_le_Sn_n m).
rewrite < Hcut.
assumption
- | apply H2;auto
+ | apply H2;autobatch
(*[ apply le_S.
assumption
| apply le_n
cut (f (S m) \lt (S m) \lor f (S m) = (S m))
[ elim Hcut
[ apply le_S_S_to_le.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
assumption
| apply False_ind.
- auto
+ autobatch
(*apply H4.
rewrite > H6.
assumption*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
apply H1.
apply le_n*)
| intro.simplify.
cut (f i \lt (S m) \lor f i = (S m))
[ elim Hcut
- [ auto
+ [ autobatch
(*apply le_S_S_to_le.
assumption*)
| apply False_ind.
- auto
+ autobatch
(*apply H5.
assumption*)
]
| apply le_to_or_lt_eq.
- auto
+ autobatch
(*apply H1.
apply le_S.
assumption*)
]
| unfold injn.
intros.
- apply H2;auto
+ apply H2;autobatch
(*[ apply le_S.
assumption
| apply le_S.
split
[ cut (a < S n \lor a = S n)
[ elim Hcut
- [ auto
+ [ autobatch
(*apply le_S_S_to_le.
assumption*)
| apply False_ind.
rewrite > H5.
assumption
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
| assumption
]
-| auto
+| autobatch
(*apply le_S.
assumption*)
]
[ elim (H m)
[ elim H4.
apply (ex_intro ? ? a).
- auto
+ autobatch
(*split
[ apply le_S.
assumption
| assumption
]*)
- | auto
+ | autobatch
(*apply le_S_S_to_le.
assumption*)
]
- | auto
+ | autobatch
(*apply (ex_intro ? ? (S n)).
split
[ apply le_n
assumption
]*)
]
-| auto
+| autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
[ elim H3.
elim (H1 a)
[ elim H6.
- auto
+ autobatch
(*apply (ex_intro ? ? a1).
split
[ assumption
[ assumption
| apply (eqb_elim j i)
[ intro.
- (*dopo circa 360 secondi l'esecuzione di auto in questo punto non era ancora terminata*)
+ (*dopo circa 360 secondi l'esecuzione di autobatch in questo punto non era ancora terminata*)
simplify.
- auto
+ autobatch
(*rewrite > H3.
rewrite > H4.
reflexivity*)
| rewrite > (eqb_n_n j).
simplify.
intros.
- auto
+ autobatch
(*apply sym_eq.
assumption*)
]
[ apply (ex_intro ? ? i).
split
[ assumption
- | (*dopo circa 5 minuti, l'esecuzione di auto in questo punto non era ancora terminata*)
+ | (*dopo circa 5 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
rewrite > (eqb_n_n i).
- auto
+ autobatch
(*simplify.
apply sym_eq.
assumption*)
split
[ assumption
| rewrite > (not_eq_to_eqb_false m i)
- [ (*dopo circa 5 minuti, l'esecuzione di auto in questo punto non era ancora terminata*)
+ [ (*dopo circa 5 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
rewrite > (not_eq_to_eqb_false m j)
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| assumption
theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
-intros.auto.
+intros.autobatch.
(*apply (bijn_fg f ?)
[ assumption
| apply (bijn_transpose n i j)
theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
intros.
-auto.
+autobatch.
(*apply (bijn_fg ? f)
[ apply (bijn_transpose n i j)
[ assumption
| unfold permut in H.
elim H.
apply sym_eq.
- auto
+ autobatch
(*apply le_n_O_to_eq.
apply H2.
apply le_n*)
| apply (bijn_fg (transpose (f (S n1)) (S n1)))
[ apply bijn_transpose
[ unfold permut in H1.
- elim H1.auto
+ elim H1.autobatch
(*apply H2.
apply le_n*)
| apply le_n
]
| apply bijn_n_Sn
[ apply H.
- auto
+ autobatch
(*apply permut_S_to_permut_transpose.
assumption*)
- | auto
+ | autobatch
(*unfold transpose.
rewrite > (eqb_n_n (f (S n1))).
simplify.
[ apply (nat_case1 m)
[ intro.
simplify.
- (*l'applicazione di auto in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
+ (*l'applicazione di autobatch in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
rewrite > (eqb_n_n (f O)).
- auto
+ autobatch
(*simplify.
reflexivity*)
| intros.simplify.
- (*l'applicazione di auto in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
+ (*l'applicazione di autobatch in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
rewrite > (eqb_n_n (f (S m1))).
- auto
+ autobatch
(*simplify.
reflexivity*)
]
| simplify.
rewrite > (not_eq_to_eqb_false (f m) (f (S n1)))
- [ (*l'applicazione di auto in questo punto, dopo parecchi secondi, non aveva ancora prodotto un risultato*)
+ [ (*l'applicazione di autobatch in questo punto, dopo parecchi secondi, non aveva ancora prodotto un risultato*)
simplify.
- auto
+ autobatch
(*apply H2.
apply injn_Sn_n.
assumption*)
| unfold Not.
intro.
absurd (m = S n1)
- [ apply H3;auto
+ [ apply H3;autobatch
(*[ apply le_S.
assumption
| apply le_n
elim H.
assumption
]
-| auto
+| autobatch
(*apply permut_to_bijn.
assumption*)
]
simplify.
elim n
[ simplify.
- elim (eqb i (f O));auto
+ elim (eqb i (f O));autobatch
(*[ simplify.
apply le_n
| simplify.
]*)
| simplify.
elim (eqb i (f (S n1)))
- [ auto
+ [ autobatch
(*simplify.
apply le_n*)
| simplify.
- auto
+ autobatch
(*apply le_S.
assumption*)
]
]
-| auto
+| autobatch
(*apply injective_invert_permut.
assumption.*)
]
apply H2.
cut (permut (invert_permut n f) n)
[ unfold permut in Hcut.
- elim Hcut.auto
+ elim Hcut.autobatch
(*apply H4.
assumption*)
| apply permut_invert_permut.
- (*NB qui auto non chiude il goal*)
+ (*NB qui autobatch non chiude il goal*)
assumption
]
| assumption
[ cut (permut (invert_permut n f) n)
[ unfold permut in Hcut.
elim Hcut.
- auto
+ autobatch
(*apply H2.
assumption*)
- | auto
+ | autobatch
(*apply permut_invert_permut.
assumption*)
]
[ rewrite < (f_invert_permut h n n) in \vdash (? ? ? %)
[ apply eq_f.
rewrite < (f_invert_permut h n n) in \vdash (? ? % ?)
- [ auto
+ [ autobatch
(*apply H1.
assumption*)
| apply le_n
- | (*qui auto NON chiude il goal*)
+ | (*qui autobatch NON chiude il goal*)
assumption
]
| apply le_n
- | (*qui auto NON chiude il goal*)
+ | (*qui autobatch NON chiude il goal*)
assumption
]
| rewrite < H4 in \vdash (? ? % ?).
apply (f_invert_permut h)
[ apply le_n
- | (*qui auto NON chiude il goal*)
+ | (*qui autobatch NON chiude il goal*)
assumption
]
]
cut (permut (invert_permut n h) n)
[ unfold permut in Hcut.
elim Hcut.
- auto
+ autobatch
(*apply H4.
apply le_n*)
| apply permut_invert_permut.
- (*NB aui auto non chiude il goal*)
+ (*NB aui autobatch non chiude il goal*)
assumption
]
]
cut (h j = j)
[ rewrite < Hcut1.
assumption
- | apply H6;auto
+ | apply H6;autobatch
(*[ apply H5.
assumption
| assumption
]*)
]
]
- | auto
+ | autobatch
(*apply not_lt_to_le.
assumption*)
]
intros 5.
elim n
[ simplify.
- auto
+ autobatch
(*apply H
[ apply le_n
| apply le_n
]*)
| simplify.
apply eq_f2
- [ auto
+ [ autobatch
(*apply H1
[ simplify.
apply le_S.
]*)
| apply H.
intros.
- apply H1;auto
+ apply H1;autobatch
(*[ assumption
| simplify.
apply le_S.
map_iter_i n g plus m = sigma n g m.
intros.
elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| simplify.
- auto
+ autobatch
(*apply eq_f.
assumption*)
]
map_iter_i n g times m = pi n g m.
intros.
elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| simplify.
- auto
+ autobatch
(*apply eq_f.
assumption*)
]
map_iter_i n (\lambda m.m) times (S O) = (S n)!.
intros.
elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| change with
rewrite < plus_n_Sm.
rewrite < plus_n_O.
apply eq_f.
- (*NB: qui auto non chiude il goal!!!*)
+ (*NB: qui autobatch non chiude il goal!!!*)
assumption
]
qed.
[ intros.
simplify.
fold simplify (transpose n (S n) (S n)).
- auto
+ autobatch
(*rewrite > transpose_i_j_i.
rewrite > transpose_i_j_j.
apply H1*)
unfold transpose.
rewrite > (not_eq_to_eqb_false m1 (S m+n))
[ rewrite > (not_eq_to_eqb_false m1 (S (S m)+n))
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| apply (lt_to_not_eq m1 (S ((S m)+n))).
- auto
+ autobatch
(*unfold lt.
apply le_S_S.
change with (m1 \leq S (m+n)).
assumption*)
]
| apply (lt_to_not_eq m1 (S m+n)).
- simplify.auto
+ simplify.autobatch
(*unfold lt.
apply le_S_S.
assumption*)
elim k
[ cut (i=n)
[ rewrite > Hcut.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply (eq_map_iter_i_transpose_l f H H1 g n O)
| apply antisymmetric_le
[ assumption
[ unfold transpose.
rewrite > (not_eq_to_eqb_false (S (S n1)+n) i)
[ rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i))
- [ auto
+ [ autobatch
(*simplify.
reflexivity*)
| simplify.
intro.
apply (lt_to_not_eq i (S n1+n))
[ assumption
- | auto
+ | autobatch
(*apply inj_S.
apply sym_eq.
assumption*)
unfold Not.
intro.
apply (lt_to_not_eq i (S (S n1+n)))
- [ auto
+ [ autobatch
(*simplify.
unfold lt.
apply le_S_S.
assumption*)
- | auto
+ | autobatch
(*apply sym_eq.
assumption*)
]
]
- | apply H2;auto
+ | apply H2;autobatch
(*[ assumption
| apply le_S_S_to_le.
assumption
]*)
]
| rewrite > H5.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
intro.
apply (nat_case m ?)
[ intros.
- apply (eq_map_iter_i_transpose_i_Si ? H H1);auto
+ apply (eq_map_iter_i_transpose_i_Si ? H H1);autobatch
(*[ exact H3
| apply le_S_S_to_le.
assumption
| intros.
apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n))
[ apply H2
- [ auto
+ [ autobatch
(*unfold lt.
apply le_n*)
| assumption
| apply (trans_le ? (S(S (m1+i))))
- [ auto
+ [ autobatch
(*apply le_S.
apply le_n*)
- | (*qui auto non chiude il goal, chiuso invece da assumption*)
+ | (*qui autobatch non chiude il goal, chiuso invece da assumption*)
assumption
]
]
| apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n))
- [ (*qui auto dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
+ [ (*qui autobatch dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
apply (H2 O ? ? (S(m1+i)))
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*apply (trans_le ? i)
[ assumption
| change with (i \le (S m1)+i).
apply le_plus_n
]*)
- | (*qui auto non chiude il goal*)
+ | (*qui autobatch non chiude il goal*)
exact H4
]
| apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
(transpose i (S(m1 + i))
(transpose (S(m1 + i)) (S(S(m1 + i)))
(transpose i (S(m1 + i)) m)))) f n))
- [ (*qui auto dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
+ [ (*qui autobatch dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
apply (H2 m1)
- [ auto
+ [ autobatch
(*unfold lt.
apply le_n*)
| assumption
| apply (trans_le ? (S(S (m1+i))))
- [ auto
+ [ autobatch
(*apply le_S.
apply le_n*)
- | (*qui auto NON CHIUDE il goal*)
+ | (*qui autobatch NON CHIUDE il goal*)
assumption
]
]
intro.
apply (not_le_Sn_n i).
rewrite < H7 in \vdash (? ? %).
- auto
+ autobatch
(*apply le_S_S.
apply le_S.
apply le_plus_n*)
intro.
apply (not_le_Sn_n i).
rewrite > H7 in \vdash (? ? %).
- auto
+ autobatch
(*apply le_S_S.
apply le_plus_n*)
| unfold Not.
intro.
- auto
+ autobatch
(*apply (not_eq_n_Sn (S m1+i)).
apply sym_eq.
assumption*)
assumption
]
| rewrite > plus_n_Sm.
- auto
+ autobatch
(*apply plus_minus_m_m.
apply lt_to_le.
assumption*)
]
| rewrite < H5.
apply (eq_map_iter_i_transpose_i_Si f H H1 g)
- [ auto
+ [ autobatch
(*simplify.
assumption*)
| apply le_S_S_to_le.
- auto
+ autobatch
(*apply (trans_le ? j)
[ assumption
| assumption
]*)
]
]
-| auto
+| autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
intros.
apply (nat_compare_elim i j)
[ intro.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5)
| intro.
rewrite > H6.
apply eq_map_iter_i.
intros.
- auto
+ autobatch
(*rewrite > (transpose_i_i j).
reflexivity*)
| intro.
[ apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3)
| apply eq_map_iter_i.
intros.
- auto
+ autobatch
(*apply eq_f.
apply transpose_i_j_j_i*)
]
[ simplify.
rewrite > (permut_n_to_eq_n h)
[ reflexivity
- | (*qui auto non chiude il goal*)
+ | (*qui autobatch non chiude il goal*)
assumption
- | (*qui auto non chiude il goal*)
+ | (*qui autobatch non chiude il goal*)
assumption
]
| apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1))
apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g)
[ apply (permut_n_to_le h n1 (S n+n1))
[ apply le_plus_n
- | (*qui auto non chiude il goal*)
+ | (*qui autobatch non chiude il goal*)
assumption
- | (*qui auto non chiude il goal*)
+ | (*qui autobatch non chiude il goal*)
assumption
| apply le_plus_n
| apply le_n
]
- | auto
+ | autobatch
(*apply H5.
apply le_n*)
| apply le_plus_n
[ simplify.
fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
apply eq_f2
- [ auto
+ [ autobatch
(*apply eq_f.
rewrite > transpose_i_j_j.
rewrite > transpose_i_j_i.
reflexivity.*)
| apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))))
[ apply permut_S_to_permut_transpose.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
assumption
| intros.
unfold transpose.
rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1)))
[ rewrite > (not_eq_to_eqb_false (h m) (S n+n1))
[ simplify.
- auto
+ autobatch
(*apply H4.
assumption*)
| rewrite > H4
- [ auto
+ [ autobatch
(*apply lt_to_not_eq.
apply (trans_lt ? n1)
[ assumption
unfold Not.
intro.
apply (lt_to_not_eq m (S n+n1))
- [ auto
+ [ autobatch
(*apply (trans_lt ? n1)
[ assumption
| simplify.
]*)
| unfold injn in H7.
apply (H7 m (S n+n1))
- [ auto
+ [ autobatch
(*apply (trans_le ? n1)
[ apply lt_to_le.
assumption
]
| apply eq_map_iter_i.
intros.
- auto
+ autobatch
(*rewrite > transpose_transpose.
reflexivity*)
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/plus".
+set "baseuri" "cic:/matita/library_autobatch/nat/plus".
include "auto/nat/nat.ma".
| (S p) \Rightarrow S (plus p m) ].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural plus" 'plus x y = (cic:/matita/library_auto/nat/plus/plus.con x y).
+interpretation "natural plus" 'plus x y = (cic:/matita/library_autobatch/nat/plus/plus.con x y).
theorem plus_n_O: \forall n:nat. n = n+O.
intros.elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
-| auto
+| autobatch
(*simplify.
apply eq_f.
assumption.*)
theorem plus_n_Sm : \forall n,m:nat. S (n+m) = n+(S m).
intros.elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity.*)
| simplify.
- auto
+ autobatch
(*
apply eq_f.
assumption.*)]
theorem sym_plus: \forall n,m:nat. n+m = m+n.
intros.elim n
-[ auto
+[ autobatch
(*simplify.
apply plus_n_O.*)
| simplify.
- auto
+ autobatch
(*rewrite > H.
apply plus_n_Sm.*)]
qed.
theorem associative_plus : associative nat plus.
unfold associative.intros.elim x
-[auto
+[autobatch
(*simplify.
reflexivity.*)
|simplify.
- auto
+ autobatch
(*apply eq_f.
assumption.*)
]
theorem injective_plus_r: \forall n:nat.injective nat nat (\lambda m.n+m).
intro.simplify.intros 2.elim n
[ exact H
-| auto
+| autobatch
(*apply H.apply inj_S.apply H1.*)
]
qed.
\def injective_plus_r.
theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.n+m).
-intro.simplify.intros.auto.
+intro.simplify.intros.autobatch.
(*apply (injective_plus_r m).
rewrite < sym_plus.
rewrite < (sym_plus y).
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/primes".
+set "baseuri" "cic:/matita/library_autobatch/nat/primes".
include "auto/nat/div_and_mod.ma".
include "auto/nat/minimization.ma".
inductive divides (n,m:nat) : Prop \def
witness : \forall p:nat.m = times n p \to divides n m.
-interpretation "divides" 'divides n m = (cic:/matita/library_auto/nat/primes/divides.ind#xpointer(1/1) n m).
+interpretation "divides" 'divides n m = (cic:/matita/library_autobatch/nat/primes/divides.ind#xpointer(1/1) n m).
interpretation "not divides" 'ndivides n m =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/library_auto/nat/primes/divides.ind#xpointer(1/1) n m)).
+ (cic:/matita/logic/connectives/Not.con (cic:/matita/library_autobatch/nat/primes/divides.ind#xpointer(1/1) n m)).
theorem reflexive_divides : reflexive nat divides.
unfold reflexive.
[ assumption
| apply (lt_O_n_elim n H).
intros.
- auto
+ autobatch
(*rewrite < plus_n_O.
rewrite > div_times.
apply sym_times*)
\forall n,m,p. div_mod_spec m n p O \to n \divides m.
intros.
elim H.
-auto.
+autobatch.
(*apply (witness n m p).
rewrite < sym_times.
rewrite > (plus_n_O (p*n)).
\forall n,m. O < n \to n \divides m \to (m \mod n) = O.
intros.
apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O)
-[ auto
+[ autobatch
(*apply div_mod_spec_div_mod.
assumption*)
-| auto
+| autobatch
(*apply divides_to_div_mod_spec;assumption*)
]
qed.
rewrite > (plus_n_O (n * (m / n))).
rewrite < H1.
rewrite < sym_times.
-auto.
+autobatch.
(* Andrea: perche' hint non lo trova ?*)
(*apply div_mod.
assumption.*)
theorem divides_n_O: \forall n:nat. n \divides O.
intro.
-auto.
+autobatch.
(*apply (witness n O O).
apply times_n_O.*)
qed.
theorem divides_n_n: \forall n:nat. n \divides n.
-auto.
+autobatch.
(*intro.
apply (witness n n (S O)).
apply times_n_SO.*)
theorem divides_SO_n: \forall n:nat. (S O) \divides n.
intro.
-auto.
+autobatch.
(*apply (witness (S O) n n).
simplify.
apply plus_n_O.*)
elim H.
elim H1.
apply (witness n (p+q) (n2+n1)).
-auto.
+autobatch.
(*rewrite > H2.
rewrite > H3.
apply sym_eq.
elim H.
elim H1.
apply (witness n (p-q) (n2-n1)).
-auto.
+autobatch.
(*rewrite > H2.
rewrite > H3.
apply sym_eq.
[ apply assoc_times
| apply eq_f.
apply (trans_eq nat ? ((n2*m)*n1))
- [ auto
+ [ autobatch
(*apply sym_eq.
apply assoc_times*)
| rewrite > (sym_times n2 m).
apply assoc_times
]
]
-| auto
+| autobatch
(*apply sym_eq.
apply assoc_times*)
]
elim H.
elim H1.
apply (witness x z (n2*n)).
-auto.
+autobatch.
(*rewrite > H3.
rewrite > H2.
apply assoc_times.*)
cut (n \le m \or \not n \le m)
[ elim Hcut
[ cut (n-m=O)
- [ auto
+ [ autobatch
(*rewrite > Hcut1.
apply (witness p O O).
apply times_n_O*)
- | auto
+ | autobatch
(*apply eq_minus_n_m_O.
assumption*)
]
rewrite > eq_minus_minus_minus_plus.
rewrite > sym_plus.
rewrite > H1.
- auto
+ autobatch
(*rewrite < div_mod
[ reflexivity
| assumption
| apply sym_eq.
apply plus_to_minus.
rewrite > sym_plus.
- auto
+ autobatch
(*apply div_mod.
assumption*)
]
rewrite > H2.
rewrite > H3.
rewrite > H5.
- auto
+ autobatch
(*rewrite < times_n_O.
reflexivity*)
| intros.
rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
rewrite > H4.
- auto
+ autobatch
(*apply le_S_S.
apply le_O_n*)
| rewrite > H3.
rewrite > times_n_SO in \vdash (? % ?).
apply le_times_r.
rewrite > H5.
- auto
+ autobatch
(*apply le_S_S.
apply le_O_n*)
]
cut (O < n2)
[ apply (lt_O_n_elim n2 Hcut).
intro.
- auto
+ autobatch
(*rewrite < sym_times.
simplify.
rewrite < sym_plus.
[ assumption
| rewrite > H2.
rewrite < H3.
- auto
+ autobatch
(*simplify.
exact (not_le_Sn_n O)*)
]
apply eqb_elim
[ intro.
simplify.
- auto
+ autobatch
(*apply mod_O_to_divides;assumption*)
| intro.
simplify.
unfold Not.
intro.
- auto
+ autobatch
(*apply H1.
apply divides_to_mod_O;assumption*)
]
assumption
| elim (divides_b n m)
[ left.
- (*qui auto non chiude il goal, chiuso dalla sola apply H1*)
+ (*qui autobatch non chiude il goal, chiuso dalla sola apply H1*)
apply H1
| right.
- (*qui auto non chiude il goal, chiuso dalla sola apply H1*)
+ (*qui autobatch non chiude il goal, chiuso dalla sola apply H1*)
apply H1
]
]
[ reflexivity
| absurd (n \divides m)
[ assumption
- | (*qui auto non chiude il goal, chiuso dalla sola applicazione di assumption*)
+ | (*qui autobatch non chiude il goal, chiuso dalla sola applicazione di assumption*)
assumption
]
]
assumption
| elim (divides_b n m)
[ absurd (n \divides m)
- [ (*qui auto non chiude il goal, chiuso dalla sola tattica assumption*)
+ [ (*qui autobatch non chiude il goal, chiuso dalla sola tattica assumption*)
assumption
| assumption
]
elim n
[ simplify.
cut (i = m)
- [ auto
+ [ autobatch
(*rewrite < Hcut.
apply divides_n_n*)
| apply antisymmetric_le
[ elim Hcut
[ apply (transitive_divides ? (pi n1 f m))
[ apply H1.
- auto
+ autobatch
(*apply le_S_S_to_le.
assumption*)
- | auto
+ | autobatch
(*apply (witness ? ? (f (S n1+m))).
apply sym_times*)
]
- | auto
+ | autobatch
(*rewrite > H3.
apply (witness ? ? (pi n1 f m)).
reflexivity*)
]
- | auto
+ | autobatch
(*apply le_to_or_lt_eq.
assumption*)
]
elim n
[ absurd (O<i)
[ assumption
- | auto
+ | autobatch
(*apply (le_n_O_elim i H1).
apply (not_le_Sn_O O)*)
]
apply (le_n_Sm_elim i n1 H2)
[ intro.
apply (transitive_divides ? n1!)
- [ auto
+ [ autobatch
(*apply H1.
apply le_S_S_to_le.
assumption*)
- | auto
+ | autobatch
(*apply (witness ? ? (S n1)).
apply sym_times*)
]
| intro.
- auto
+ autobatch
(*rewrite > H3.
apply (witness ? ? n1!).
reflexivity*)
cut (n! \mod i = O)
[ rewrite < Hcut.
apply mod_S
- [ auto
+ [ autobatch
(*apply (trans_lt O (S O))
[ apply (le_n (S O))
| assumption
| rewrite > Hcut.
assumption
]
-| auto(*
+| autobatch(*
apply divides_to_mod_O
[ apply ltn_to_ltO [| apply H]
| apply divides_fact
(S O) < i \to i \le n \to i \ndivides S n!.
intros.
apply divides_b_false_to_not_divides
-[ auto
+[ autobatch
(*apply (trans_lt O (S O))
[ apply (le_n (S O))
| assumption
]*)
| unfold divides_b.
- rewrite > mod_S_fact;auto
+ rewrite > mod_S_fact;autobatch
(*[ simplify.
reflexivity
| assumption
\forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
intro.
apply (nat_case n)
-[ auto
+[ autobatch
(*intro.
apply False_ind.
apply (not_le_Sn_O (S O) H)*)
| intro.
apply (nat_case m)
- [ auto
+ [ autobatch
(*intro. apply False_ind.
apply (not_le_Sn_n (S O) H)*)
| intros.
apply le_min_aux
| apply sym_eq.
apply plus_to_minus.
- auto
+ autobatch
(*rewrite < sym_plus.
simplify.
reflexivity*)
theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
intro.
apply (nat_case n)
-[ auto
+[ autobatch
(*intro.
apply False_ind.
apply (not_le_Sn_n O H)*)
| intro.
apply (nat_case m)
- [ auto
+ [ autobatch
(*intro.
simplify.
unfold lt.
apply le_n*)
| intros.
apply (trans_lt ? (S O))
- [ auto
+ [ autobatch
(*unfold lt.
apply le_n*)
| apply lt_SO_smallest_factor.
- unfold lt.auto
+ unfold lt.autobatch
(*apply le_S_S.
apply le_S_S.
apply le_O_n*)
intro.
apply (nat_case n)
[ intro.
- auto
+ autobatch
(*apply False_ind.
apply (not_le_Sn_O O H)*)
| intro.
apply (nat_case m)
[ intro.
- auto
+ autobatch
(*simplify.
apply (witness ? ? (S O)).
simplify.
apply f_min_aux_true.
apply (ex_intro nat ? (S(S m1))).
split
- [ auto
+ [ autobatch
(*split
[ apply le_minus_m
| apply le_n
]*)
- | auto
+ | autobatch
(*rewrite > mod_n_n
[ reflexivity
| apply (trans_lt ? (S O))
\forall n:nat. smallest_factor n \le n.
intro.
apply (nat_case n)
-[ auto
+[ autobatch
(*simplify.
apply le_n*)
| intro.
- auto
+ autobatch
(*apply (nat_case m)
[ simplify.
apply le_n
apply (not_le_Sn_n (S O) H)
| intros.
apply divides_b_false_to_not_divides
- [ auto
+ [ autobatch
(*apply (trans_lt O (S O))
[ apply (le_n (S O))
| assumption
exact H1
| apply sym_eq.
apply plus_to_minus.
- auto
+ autobatch
(*rewrite < sym_plus.
simplify.
reflexivity*)
[ apply (transitive_divides m (smallest_factor n))
[ assumption
| apply divides_smallest_factor_n.
- auto
+ autobatch
(*apply (trans_lt ? (S O))
[ unfold lt.
apply le_n
| exact H
]*)
]
- | apply lt_smallest_factor_to_not_divides;auto
+ | apply lt_smallest_factor_to_not_divides;autobatch
(*[ exact H
| assumption
| assumption
intro.
apply (nat_case n)
[ intro.
- auto
+ autobatch
(*apply False_ind.
apply (not_prime_O H)*)
| intro.
apply (nat_case m)
[ intro.
- auto
+ autobatch
(*apply False_ind.
apply (not_prime_SO H)*)
| intro.
smallest_factor (S(S m1)) = (S(S m1))).
intro.
elim H.
- auto
+ autobatch
(*apply H2
[ apply divides_smallest_factor_n.
apply (trans_lt ? (S O))
intro.
apply (nat_case n)
[ simplify.
- auto
+ autobatch
(*unfold Not.
unfold prime.
intro.
| intro.
apply (nat_case m)
[ simplify.
- auto
+ autobatch
(*unfold Not.
unfold prime.
intro.
simplify.
rewrite < H.
apply prime_smallest_factor_n.
- unfold lt.auto
+ unfold lt.autobatch
(*apply le_S_S.
apply le_S_S.
apply le_O_n*)
simplify.
change with (prime (S(S m1)) \to False).
intro.
- auto
+ autobatch
(*apply H.
apply prime_to_smallest_factor.
assumption*)
[ true \Rightarrow prime n
| false \Rightarrow \lnot (prime n)].
rewrite < H.
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
apply primeb_to_Prop.
qed.
[ true \Rightarrow prime n
| false \Rightarrow \lnot (prime n)].
rewrite < H.
-(*qui auto non chiude il goal*)
+(*qui autobatch non chiude il goal*)
apply primeb_to_Prop.
qed.
[ true \Rightarrow prime n
| false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n))
[ apply Hcut.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply primeb_to_Prop
| elim (primeb n)
[ left.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply H
| right.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply H
]
]
[ true \Rightarrow prime n
| false \Rightarrow \lnot (prime n)] \to ((primeb n) = true))
[ apply Hcut.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply primeb_to_Prop
| elim (primeb n)
[ reflexivity.
| absurd (prime n)
[ assumption
- | (*qui auto non chiude il goal*)
+ | (*qui autobatch non chiude il goal*)
assumption
]
]
[ true \Rightarrow prime n
| false \Rightarrow \lnot (prime n)] \to ((primeb n) = false))
[ apply Hcut.
- (*qui auto non chiude il goal*)
+ (*qui autobatch non chiude il goal*)
apply primeb_to_Prop
| elim (primeb n)
[ absurd (prime n)
- [ (*qui auto non chiude il goal*)
+ [ (*qui autobatch non chiude il goal*)
assumption
| assumption
]
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/relevant_equations".
+set "baseuri" "cic:/matita/library_autobatch/nat/relevant_equations".
include "auto/nat/times.ma".
include "auto/nat/minus.ma".
intros.
apply (trans_eq ? ? (p*(n+m)))
[ apply sym_times
-| apply (trans_eq ? ? (p*n+p*m));auto
+| apply (trans_eq ? ? (p*n+p*m));autobatch
(*[ apply distr_times_plus
| apply eq_f2;
apply sym_times
intros.
apply (trans_eq ? ? (p*(n-m)))
[ apply sym_times
-| apply (trans_eq ? ? (p*n-p*m));auto
+| apply (trans_eq ? ? (p*n-p*m));autobatch
(*[ apply distr_times_minus
| apply eq_f2;
apply sym_times
theorem times_plus_plus: \forall n,m,p,q:nat. (n + m)*(p + q) =
n*p + n*q + m*p + m*q.
intros.
-auto.
+autobatch.
(*apply (trans_eq nat ? ((n*(p+q) + m*(p+q))))
[ apply times_plus_l
| rewrite > distr_times_plus.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/sigma_and_pi".
+set "baseuri" "cic:/matita/library_autobatch/nat/sigma_and_pi".
include "auto/nat/factorial.ma".
include "auto/nat/exp.ma".
intros 3.
elim n
[ simplify.
- auto
+ autobatch
(*apply H
[ apply le_n
| rewrite < plus_n_O.
| simplify.
apply eq_f2
[ apply H1
- [ auto
+ [ autobatch
(*change with (m \le (S n1)+m).
apply le_plus_n*)
- | auto
+ | autobatch
(*rewrite > (sym_plus m).
apply le_n*)
]
intros.
apply H1
[ assumption
- | auto
+ | autobatch
(*rewrite < plus_n_Sm.
apply le_S.
assumption*)
intros 3.
elim n
[ simplify.
- auto
+ autobatch
(*apply H
[ apply le_n
| rewrite < plus_n_O.
| simplify.
apply eq_f2
[ apply H1
- [ auto
+ [ autobatch
(*change with (m \le (S n1)+m).
apply le_plus_n*)
- | auto
+ | autobatch
(*rewrite > (sym_plus m).
apply le_n*)
]
intros.
apply H1
[ assumption
- | auto
+ | autobatch
(*rewrite < plus_n_Sm.
apply le_S.
assumption*)
theorem eq_fact_pi: \forall n. (S n)! = pi n (\lambda m.m) (S O).
intro.
elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity*)
| change with ((S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O))).
rewrite < plus_n_Sm.
rewrite < plus_n_O.
- auto
+ autobatch
(*apply eq_f.
assumption*)
]
(exp a (S n))*pi n f m= pi n (\lambda p.a*(f p)) m.
intros.
elim n
-[ auto
+[ autobatch
(*simplify.
rewrite < times_n_SO.
reflexivity*)
apply eq_f.
rewrite < assoc_times.
rewrite < assoc_times.
- auto
+ autobatch
(*apply eq_f2
[ apply sym_times
| reflexivity
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/times".
+set "baseuri" "cic:/matita/library_autobatch/nat/times".
include "auto/nat/plus.ma".
| (S p) \Rightarrow m+(times p m) ].
(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural times" 'times x y = (cic:/matita/library_auto/nat/times/times.con x y).
+interpretation "natural times" 'times x y = (cic:/matita/library_autobatch/nat/times/times.con x y).
theorem times_n_O: \forall n:nat. O = n*O.
intros.elim n
-[ auto
+[ autobatch
(*simplify.
reflexivity.*)
-| simplify. (* qui auto non funziona: Uncaught exception: Invalid_argument ("List.map2")*)
+| simplify. (* qui autobatch non funziona: Uncaught exception: Invalid_argument ("List.map2")*)
assumption.
]
qed.
theorem times_n_Sm :
\forall n,m:nat. n+(n*m) = n*(S m).
intros.elim n
-[ auto.
+[ autobatch.
(*simplify.reflexivity.*)
| simplify.
- auto
+ autobatch
(*apply eq_f.
rewrite < H.
transitivity ((n1+m)+n1*m)
qed.
(* NOTA:
- se non avessi semplificato con auto tutto il secondo ramo della tattica
- elim n, avrei comunque potuto risolvere direttamente con auto entrambi
+ se non avessi semplificato con autobatch tutto il secondo ramo della tattica
+ elim n, avrei comunque potuto risolvere direttamente con autobatch entrambi
i rami generati dalla prima applicazione della tattica transitivity
(precisamente transitivity ((n1+m)+n1*m)
*)
theorem times_n_SO : \forall n:nat. n = n * S O.
intros.
rewrite < times_n_Sm.
-auto paramodulation. (*termina la dim anche solo con auto*)
+autobatch paramodulation. (*termina la dim anche solo con autobatch*)
(*rewrite < times_n_O.
rewrite < plus_n_O.
reflexivity.*)
theorem times_SSO_n : \forall n:nat. n + n = S (S O) * n.
intros.
simplify.
-auto paramodulation. (* termina la dim anche solo con auto*)
+autobatch paramodulation. (* termina la dim anche solo con autobatch*)
(*rewrite < plus_n_O.
reflexivity.*)
qed.
theorem symmetric_times : symmetric nat times.
unfold symmetric.
intros.elim x
-[ auto
+[ autobatch
(*simplify.apply times_n_O.*)
| simplify.
- auto
+ autobatch
(*rewrite > H.apply times_n_Sm.*)
]
qed.
unfold distributive.
intros.elim x;simplify
[ reflexivity.
-| auto
+| autobatch
(*rewrite > H.
rewrite > assoc_plus.
rewrite > assoc_plus.
unfold associative.intros.
elim x;simplify
[ apply refl_eq
-| auto
+| autobatch
(*rewrite < sym_times.
rewrite > distr_times_plus.
rewrite < sym_times.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/library_auto/nat/totient".
+set "baseuri" "cic:/matita/library_autobatch/nat/totient".
include "auto/nat/count.ma".
include "auto/nat/chinese_reminder.ma".
intro.
apply (nat_case n)
[ intros.
- auto
+ autobatch
(*simplify.
reflexivity*)
| intros 2.
apply (le_to_lt_to_lt ? (pred ((S m)*(S m2))))
[ unfold min.
apply le_min_aux_r
- | auto
+ | autobatch
(*unfold lt.
apply (nat_case ((S m)*(S m2)))
[ apply le_n
rewrite > sym_gcd.
rewrite > gcd_mod
[ apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| assumption
]
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
rewrite > sym_gcd.
rewrite > gcd_mod
[ apply (gcd_times_SO_to_gcd_SO ? ? (S m))
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*rewrite > sym_times.
assumption*)
]
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
apply False_ind.
apply H6.
apply eq_gcd_times_SO
- [ auto
+ [ autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
| rewrite < gcd_mod
- [ auto
+ [ autobatch
(*rewrite > H4.
rewrite > sym_gcd.
assumption*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
]
| rewrite < gcd_mod
- [ auto
+ [ autobatch
(*rewrite > H5.
rewrite > sym_gcd.
assumption*)
- | auto
+ | autobatch
(*unfold lt.
apply le_S_S.
apply le_O_n*)
<property name="visible">True</property>
<property name="title" translatable="yes">Auto</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
- <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
<property name="modal">False</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
<property name="decorated">True</property>
<property name="skip_taskbar_hint">False</property>
<property name="skip_pager_hint">False</property>
- <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
- <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_DIALOG</property>
+ <property name="gravity">GDK_GRAVITY_SOUTH_EAST</property>
<property name="focus_on_map">True</property>
<property name="urgency_hint">False</property>
<property name="spacing">2</property>
<child>
- <widget class="GtkScrolledWindow" id="scrolledwindow14">
+ <widget class="GtkScrolledWindow" id="scrolledwindowAREA">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
<property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkViewport" id="viewport3">
+ <widget class="GtkViewport" id="viewportAREA">
<property name="visible">True</property>
<property name="shadow_type">GTK_SHADOW_IN</property>
*)
type status =
- Cic.context * (Cic.term * (int * Cic.term) list) list * Cic.term list *
+ Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
+ (int * Cic.term * int) list *
Cic.term list
let fake_goal = Cic.Implicit None;;
let fake_candidates = [];;
let len = ref 10;;
let pp c t =
- let names = List.map (function None -> None | Some (n,_) -> Some n) c in
+ (*
let t =
ProofEngineReduction.replace
~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t
in
- CicPp.pp t names
+ ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
+ max_int [] c t
+ *)
+ let names = List.map (function None -> None | Some (x,_) -> Some x) c in
+ let txt_t = CicPp.pp t names in
+ Pcre.replace ~pat:"\\?(\\d+)\\[[^]]*\\]" ~templ:"?<sub>$1</sub>" txt_t
;;
let pp_goal context x =
if x == fake_goal then "" else pp context x
let sublist start len l =
let rec aux pos len = function
| [] when pos < start -> aux (pos+1) len []
- | [] when len > 0 -> (fake_goal, fake_candidates) :: aux (pos+1) (len-1) []
+ | [] when len > 0 ->
+ (0,fake_goal, false, 0, fake_candidates) :: aux (pos+1) (len-1) []
| [] (* when len <= 0 *) -> []
| he::tl when pos < start -> aux (pos+1) len tl
| he::tl when pos >= start && len > 0 -> he::aux (pos+1) (len-1) tl
aux 0 len l
;;
-let cell_of_candidate context ?(active=false) g id c =
+let cell_of_candidate height context ?(active=false) g id c =
let tooltip = GData.tooltips () in (* should be only one isn't it? *)
let button =
GButton.button
- ~label:(pp_candidate context c(* ^ " - " ^ string_of_int id*)) ()
+ ~label:(pp_candidate context c(* ^ " - " ^ string_of_int id*))
+ ()
in
+ button#misc#set_size_request ~height ();
if active then
button#misc#set_sensitive false;
let text =
(fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
button
;;
-let cell_of_goal win_width context goal =
- GMisc.label ~text:(pp_goal context goal) ~xalign:0.0 ()
+let cell_of_goal height win_width context goal =
+ GMisc.label
+ ~markup:(pp_goal context goal) ~xalign:0.0
+ ~width:(min (win_width * 60 / 100) 500)
+ ~line_wrap:false
+ ~ellipsize:`END
+ ~height
+ ()
;;
-let cell_of_int n =
- GMisc.label ~text:(string_of_int n)
- ~line_wrap:true ~justify:`RIGHT ()
+let cell_of_row_header height n k id =
+ GMisc.label
+ ~markup:("<span stretch=\"ultracondensed\">" ^ string_of_int n ^ "<sub>(" ^
+ string_of_int id ^ "|" ^ string_of_int k ^ ")</sub></span>")
+ ~line_wrap:true ~justify:`LEFT ~height ~width:80 ()
;;
-let cell_of_candidates context goal cads =
+let cell_of_candidates height grey context goal cads =
let hbox = GPack.hbox () in
match cads with
| [] -> hbox
| (id,c)::tl ->
hbox#pack
- (cell_of_candidate ~active:true context goal id c :> GObj.widget);
+ (cell_of_candidate height ~active:grey
+ context goal id c :> GObj.widget);
List.iter
(fun (id,c) ->
- hbox#pack (cell_of_candidate context goal id c :> GObj.widget)) tl;
+ hbox#pack (cell_of_candidate height context goal id c :> GObj.widget)) tl;
hbox
;;
-let elems_to_rows context win_width (table : GPack.table) (or_list) =
+let elems_to_rows height context win_width (table : GPack.table) (or_list) =
+ let height = height / (List.length or_list) in
let _ =
List.fold_left
- (fun position (goal, candidates) ->
+ (fun position (goal_id, goal, grey, depth, candidates) ->
table#attach ~left:0 ~top:position
- (cell_of_int (position + !start) :> GObj.widget);
- table#attach ~left:1 ~top:position ~expand:`BOTH ~fill:`BOTH
- (cell_of_goal win_width context goal :> GObj.widget);
+ (cell_of_row_header height (position + !start)
+ depth goal_id :> GObj.widget);
+ table#attach ~left:1 ~top:position ~fill:`BOTH
+ (cell_of_goal height win_width context goal :> GObj.widget);
table#attach ~left:2 ~top:position
- (cell_of_candidates context goal candidates :> GObj.widget);
+ (cell_of_candidates height grey context goal candidates :> GObj.widget);
position+1)
0 or_list
in
()
;;
-let old_displayed_status = ref ([]);;
+let old_displayed_status = ref [];;
let old_size = ref 0;;
let fill_win (win : MatitaGeneratedGui.autoWin) cb =
let win_size = win#toplevel#misc#allocation.Gtk.width in
let ctx, or_list, and_list, last_moves = status in
let displayed_status =
- sublist !start !len (or_list @ (List.map (fun x -> x,[]) and_list))
+ sublist !start !len
+ (or_list @ (List.map (fun (id,x,d) -> id,x,false,d,[]) and_list))
in
if displayed_status <> !old_displayed_status || !old_size <> win_size then
begin
win#labelLAST#set_text
(String.concat ";" (List.map (pp_candidate ctx) last_moves));
List.iter win#table#remove win#table#children;
- elems_to_rows ctx win_size win#table displayed_status;
+ let height = win#viewportAREA#misc#allocation.Gtk.height in
+ elems_to_rows height ctx win_size win#table displayed_status;
Printf.eprintf
"REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -. init);
end
let auto_dialog elems =
let win = new MatitaGeneratedGui.autoWin () in
+ let width = Gdk.Screen.width () in
+ let height = Gdk.Screen.height () in
+ let main_w = width * 70 / 100 in
+ let main_h = height * 60 / 100 in
+ win#toplevel#resize ~width:main_w ~height:main_h;
win#check_widgets ();
win#table#set_columns 3;
win#table#set_col_spacings 6;
ignore(win#buttonDOWN#connect#clicked
(fun _ -> incr start; fill_win win elems));
ignore(win#buttonCLOSE#connect#clicked
- (fun _ -> win#toplevel#destroy ();GMain.Main.quit ()));
+ (fun _ ->
+ Auto.pause false;
+ Auto.step ();
+ win#toplevel#destroy ();
+ GMain.Main.quit ()));
let redraw_callback _ = fill_win win elems;true in
let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
ignore(win#buttonPAUSE#connect#clicked
- (fun _ -> Auto.pause true));
+ (fun _ ->
+ Auto.pause true;
+ win#buttonPLAY#misc#set_sensitive true;
+ win#buttonPAUSE#misc#set_sensitive false;));
ignore(win#buttonPLAY#connect#clicked
- (fun _ -> Auto.pause false;Auto.step ()));
+ (fun _ ->
+ Auto.pause false;
+ Auto.step ();
+ win#buttonPLAY#misc#set_sensitive false;
+ win#buttonPAUSE#misc#set_sensitive true;));
ignore(win#buttonNEXT#connect#clicked
(fun _ -> Auto.step ()));
+ Auto.pause true;
+ win#buttonPLAY#misc#set_sensitive true;
+ win#buttonPAUSE#misc#set_sensitive false;
fill_win win elems;
win#toplevel#show ();
GtkThread.main ();
(tac_w_term (A.Transitivity (loc, hole)));
connect_button tbar#assumptionButton (tac (A.Assumption loc));
connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
- connect_button tbar#autoButton (tac (A.Auto (loc,[])));
+ connect_button tbar#autoButton (tac (A.AutoBatch (loc,[])));
MatitaGtkMisc.toggle_widget_visibility
~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
~check:main#tacticsBarMenuItem;
let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
let multiline_RE = Pcre.regexp "^\n[^\n]+$"
let newline_RE = Pcre.regexp "\n"
+let comment_RE = Pcre.regexp "\\(\\*(.|\n)*\\*\\)\n?" ~flags:[`UNGREEDY]
let comment str =
if Pcre.pmatch ~rex:multiline_RE str then
"\n(** " ^ (Pcre.replace ~rex:newline_RE str) ^ " *)"
else
"\n(**\n" ^ str ^ "\n*)"
+
+let strip_comments str =
+ Pcre.qreplace ~templ:"\n" ~pat:"\n\n" (Pcre.qreplace ~rex:comment_RE str)
+;;
let first_line s =
let s = Pcre.replace ~rex:heading_nl_RE s in
let pp_eager_statement_ast =
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
-
+
+(* naive implementation of procedural proof script generation,
+ * starting from an applicatiove *auto generated) proof.
+ * this is out of place, but I like it :-P *)
+let cic2grafite context menv t =
+ (* indents a proof script in a stupid way, better than nothing *)
+ let stupid_indenter s =
+ let next s =
+ let idx_square_o = try String.index s '[' with Not_found -> -1 in
+ let idx_square_c = try String.index s ']' with Not_found -> -1 in
+ let idx_pipe = try String.index s '|' with Not_found -> -1 in
+ let tok =
+ List.sort (fun (i,_) (j,_) -> compare i j)
+ [idx_square_o,'[';idx_square_c,']';idx_pipe,'|']
+ in
+ let tok = List.filter (fun (i,_) -> i <> -1) tok in
+ match tok with
+ | (i,c)::_ -> Some (i,c)
+ | _ -> None
+ in
+ let break_apply n s =
+ let tab = String.make (n+1) ' ' in
+ Pcre.replace ~templ:(".\n" ^ tab ^ "apply") ~pat:"\\.apply" s
+ in
+ let rec ind n s =
+ match next s with
+ | None ->
+ s
+ | Some (position, char) ->
+ try
+ let s1, s2 =
+ String.sub s 0 position,
+ String.sub s (position+1) (String.length s - (position+1))
+ in
+ match char with
+ | '[' -> break_apply n s1 ^ "\n" ^ String.make (n+2) ' ' ^
+ "[" ^ ind (n+2) s2
+ | '|' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^
+ "|" ^ ind n s2
+ | ']' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^
+ "]" ^ ind (n-2) s2
+ | _ -> assert false
+ with
+ Invalid_argument err ->
+ prerr_endline err;
+ s
+ in
+ ind 0 s
+ in
+ let module PT = CicNotationPt in
+ let module GA = GrafiteAst in
+ let pp_t context t =
+ let names =
+ List.map (function Some (n,_) -> Some n | None -> None) context
+ in
+ CicPp.pp t names
+ in
+ let sort_of context t =
+ try
+ let ty,_ =
+ CicTypeChecker.type_of_aux' menv context t
+ CicUniv.oblivion_ugraph
+ in
+ let sort,_ = CicTypeChecker.type_of_aux' menv context ty
+ CicUniv.oblivion_ugraph
+ in
+ match sort with
+ | Cic.Sort Cic.Prop -> true
+ | _ -> false
+ with
+ CicTypeChecker.TypeCheckerFailure _ ->
+ HLog.error "auto proof to sript transformation error"; false
+ in
+ let floc = HExtlib.dummy_floc in
+ (* minimalisti cic.term -> pt.term *)
+ let print_term c t =
+ let rec aux c = function
+ | Cic.Rel _
+ | Cic.MutConstruct _
+ | Cic.MutInd _
+ | Cic.Const _ as t ->
+ PT.Ident (pp_t c t, None)
+ | Cic.Appl l -> PT.Appl (List.map (aux c) l)
+ | Cic.Implicit _ -> PT.Implicit
+ | Cic.Lambda (Cic.Name n, s, t) ->
+ PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
+ aux (Some (Cic.Name n, Cic.Decl s)::c) t)
+ | Cic.Prod (Cic.Name n, s, t) ->
+ PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
+ aux (Some (Cic.Name n, Cic.Decl s)::c) t)
+ | Cic.LetIn (Cic.Name n, s, t) ->
+ PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
+ aux (Some (Cic.Name n, Cic.Def (s,None))::c) t)
+ | Cic.Meta _ -> PT.Implicit
+ | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
+ | Cic.Sort Cic.Set -> PT.Sort `Set
+ | Cic.Sort Cic.CProp -> PT.Sort `CProp
+ | Cic.Sort Cic.Prop -> PT.Sort `Prop
+ | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None)
+ in
+ aux c t
+ in
+ (* prints an applicative proof, that is an auto proof.
+ * don't use in the general case! *)
+ let rec print_proof context = function
+ | Cic.Rel _
+ | Cic.Const _ as t ->
+ [GA.Executable (floc,
+ GA.Tactic (floc,
+ Some (GA.Apply (floc, print_term context t)), GA.Dot floc))]
+ | Cic.Appl (he::tl) ->
+ let tl = List.map (fun t -> t, sort_of context t) tl in
+ let subgoals =
+ HExtlib.filter_map (function (t,true) -> Some t | _ -> None) tl
+ in
+ let args =
+ List.map (function | (t,true) -> Cic.Implicit None | (t,_) -> t) tl
+ in
+ if List.length subgoals > 1 then
+ (* branch *)
+ [GA.Executable (floc,
+ GA.Tactic (floc,
+ Some (GA.Apply (floc, print_term context (Cic.Appl (he::args)))),
+ GA.Semicolon floc))] @
+ [GA.Executable (floc, GA.Tactic (floc, None, GA.Branch floc))] @
+ (HExtlib.list_concat
+ ~sep:[GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))]
+ (List.map (print_proof context) subgoals)) @
+ [GA.Executable (floc, GA.Tactic (floc, None,GA.Merge floc))]
+ else
+ (* simple apply *)
+ [GA.Executable (floc,
+ GA.Tactic (floc,
+ Some (GA.Apply
+ (floc, print_term context (Cic.Appl (he::args)) )), GA.Dot floc))]
+ @
+ (match subgoals with
+ | [] -> []
+ | [x] -> print_proof context x
+ | _ -> assert false)
+ | Cic.Lambda (Cic.Name n, ty, bo) ->
+ [GA.Executable (floc,
+ GA.Tactic (floc,
+ Some (GA.Cut (floc, Some n, (print_term context ty))),
+ GA.Branch floc))] @
+ (print_proof (Some (Cic.Name n, Cic.Decl ty)::context) bo) @
+ [GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))] @
+ [GA.Executable (floc, GA.Tactic (floc,
+ Some (GA.Assumption floc),GA.Merge floc))]
+ | _ -> []
+ (*
+ debug_print (lazy (CicPp.ppterm t));
+ assert false
+ *)
+ in
+ (* performs a lambda closure of the proof term abstracting metas.
+ * this is really an approximation of a closure, local subst of metas
+ * is not kept into account *)
+ let close_pt menv context t =
+ let metas = CicUtil.metas_of_term t in
+ let metas =
+ HExtlib.list_uniq ~eq:(fun (i,_) (j,_) -> i = j)
+ (List.sort (fun (i,_) (j,_) -> compare i j) metas)
+ in
+ let mk_rels_and_collapse_metas metas =
+ let rec aux i map acc acc1 = function
+ | [] -> acc, acc1, map
+ | (j,_ as m)::tl ->
+ let _,_,ty = CicUtil.lookup_meta j menv in
+ try
+ let n = List.assoc ty map in
+ aux i map (Cic.Rel n :: acc) (m::acc1) tl
+ with Not_found ->
+ let map = (ty, i)::map in
+ aux (i+1) map (Cic.Rel i :: acc) (m::acc1) tl
+ in
+ aux 1 [] [] [] metas
+ in
+ let rels, metas, map = mk_rels_and_collapse_metas metas in
+ let n_lambdas = List.length map in
+ let t =
+ if metas = [] then
+ t
+ else
+ let t =
+ ProofEngineReduction.replace_lifting
+ ~what:(List.map (fun (x,_) -> Cic.Meta (x,[])) metas)
+ ~with_what:rels
+ ~context:context
+ ~equality:(fun _ x y ->
+ match x,y with
+ | Cic.Meta(i,_), Cic.Meta(j,_) when i=j -> true
+ | _ -> false)
+ ~where:(CicSubstitution.lift n_lambdas t)
+ in
+ let rec mk_lam = function
+ | [] -> t
+ | (ty,n)::tl ->
+ let name = "fresh_"^ string_of_int n in
+ Cic.Lambda (Cic.Name name, ty, mk_lam tl)
+ in
+ mk_lam
+ (fst (List.fold_left
+ (fun (l,liftno) (ty,_) ->
+ (l @ [CicSubstitution.lift liftno ty,liftno] , liftno+1))
+ ([],0) map))
+ in
+ t
+ in
+ let ast = print_proof context (close_pt menv context t) in
+ let pp t =
+ (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
+ * which will show up using the following command line:
+ * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
+ let width = max_int in
+ let term_pp content_term =
+ let pres_term = TermContentPres.pp_ast content_term in
+ let dummy_tbl = Hashtbl.create 1 in
+ let markup = CicNotationPres.render dummy_tbl pres_term in
+ let s = "(" ^ BoxPp.render_to_string List.hd width markup ^ ")" in
+ Pcre.substitute
+ ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
+ in
+ CicNotationPp.set_pp_term term_pp;
+ let lazy_term_pp = fun x -> assert false in
+ let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
+ GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
+ in
+ let script = String.concat "" (List.map pp ast) in
+ prerr_endline script;
+ stupid_indenter script
+;;
+
let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
let module TAPp = GrafiteAstPp in
let module MQ = MetadataQuery in
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
[], "", parsed_text_length
+ | TA.AutoInteractive (_, params) ->
+ let user_goal' =
+ match user_goal with
+ Some n -> n
+ | None -> raise NoUnfinishedProof
+ in
+ let proof = GrafiteTypes.get_current_proof grafite_status in
+ let proof_status = proof,user_goal' in
+ (try
+ let _,menv,_,_,_,_ = proof in
+ let i,cc,ty = CicUtil.lookup_meta user_goal' menv in
+ let timestamp = Unix.gettimeofday () in
+ let (_,menv,subst,_,_,_), _ =
+ ProofEngineTypes.apply_tactic
+ (Auto.auto_tac ~dbd ~params
+ ~universe:grafite_status.GrafiteTypes.universe) proof_status
+ in
+ let proof_term =
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable cc
+ in
+ CicMetaSubst.apply_subst subst (Cic.Meta (i,irl))
+ in
+ let time = Unix.gettimeofday () -. timestamp in
+ let text =
+ comment parsed_text ^ "\n" ^
+ cic2grafite cc menv proof_term ^
+ (Printf.sprintf "\n(* end auto proof: %4.2f *)" time)
+ in
+ (* alternative using FG stuff
+ let proof_term =
+ Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc
+ in
+ let ty,_ =
+ CicTypeChecker.type_of_aux' menv [] proof_term CicUniv.empty_ugraph
+ in
+ let obj =
+ Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma])
+ in
+ let text =
+ comment parsed_text ^
+ Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+"
+ (strip_comments
+ (ApplyTransformation.txt_of_cic_object
+ ~map_unicode_to_tex:false
+ ~skip_thm_and_qed:true
+ ~skip_initial_lambdas:true
+ 80 (GrafiteAst.Procedural None) "" obj)) ^
+ "(* end auto proof *)"
+ in
+ *)
+ [],text,parsed_text_length
+ with
+ ProofEngineTypes.Fail _ -> [], comment parsed_text, parsed_text_length)
| TA.Inline (_,style,suri,prefix) ->
let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
[], str, String.length parsed_text
projects / helm.git / commitdiff