1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
16 include "nat/relevant_equations.ma".
18 alias num (instance 0) = "natural number".
20 theorem plus_inv_O3: \forall m,n. 0 = n + m \to 0 = n \land 0 = m.
21 intros 2; elim n names 0; clear n; simplify; intros;
22 [ autobatch | destruct ].
25 theorem times_inv_O3_S: \forall x,y. 0 = x * (S y) -> x = 0.
26 intros; rewrite < times_n_Sm in H;
27 lapply linear plus_inv_O3 to H; decompose; destruct; autobatch.
30 theorem not_3_divides_1: \forall n. 1 = n * 3 \to False.
31 intros 1; rewrite > sym_times; simplify;
32 elim n names 0; simplify; intros; destruct;
33 rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
36 theorem le_inv_S_S: \forall m,n. S m <= S n \to m <= n.
37 intros; inversion H; clear H; intros; destruct; autobatch.
40 theorem plus_inv_S_S_S: \forall x,y,z. S x = S y + S z \to S y <= x \land S z <= x.
41 simplify; intros; destruct;
42 rewrite < plus_n_Sm in \vdash (? (? ? %) ?); autobatch depth = 3.
45 theorem times_inv_S_m_SS: \forall k,n,m. S n = m * (S (S k)) \to m \le n.
46 intros 3; elim m names 0; clear m; simplify; intros; destruct;
47 clear H; apply le_S_S; rewrite < sym_times; simplify;
51 theorem plus_3_S3n: \forall n. S (S n * 3) = 3 + S (n * 3).
52 intros; simplify; autobatch.
55 theorem times_exp_x_y_Sz: \forall x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
56 intros; simplify; autobatch depth = 1.
59 definition acc_nat \def \lambda P:nat \to Prop. \lambda n.
60 \forall m. m <= n \to P m.
62 theorem wf_le: \forall P.
63 P 0 \to (\forall n. acc_nat P n \to P (S n)) \to
64 \forall n. acc_nat P n.
65 unfold acc_nat; intros 4; elim n names 0; clear n;
66 [ intros; lapply linear le_n_O_to_eq to H2; destruct; autobatch
67 | intros 3; elim m; clear m; intros; clear H3;
68 [ clear H H1; autobatch
69 | clear H; lapply linear le_inv_S_S to H4;
70 apply H1; clear H1; intros;
71 apply H2; clear H2; autobatch depth = 2
76 theorem wf_nat_ind: \forall P:nat \to Prop.
78 (\forall n. (\forall m. m <= n \to P m) \to P (S n)) \to
80 intros; lapply linear depth=2 wf_le to H, H1 as H0;
81 unfold acc_nat in H0; apply (H0 n n); autobatch.