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 (**************************************************************************)
15 include "classes/defs.ma".
17 theorem p_inv_O: P 0 \to False.
18 intros; inversion H; clear H; intros;
20 | lapply linear plus_inv_O3 to H3; decompose; destruct;
25 theorem t_inv_O: T 0 \to False.
26 intros; inversion H; clear H; intros;
27 [ lapply linear times_inv_O3_S to H1; destruct; autobatch depth = 2
28 | lapply linear times_inv_O3_S to H2; destruct; autobatch depth = 2
32 theorem p_pos: \forall i. P i \to \exists k. i = S k.
33 intros 1; elim i names 0; clear i; intros;
34 [ lapply linear p_inv_O to H; decompose
39 theorem t_pos: \forall i. T i \to \exists k. i = S k.
40 intros 1; elim i names 0; clear i; intros;
41 [ lapply linear t_inv_O to H; decompose
46 theorem t_1: T 1 \to False.
47 intros; inversion H; clear H; intros;
48 [ lapply not_3_divides_1 to H1; decompose
49 | lapply not_3_divides_1 to H2; decompose
54 change in \vdash (? %) with (1 * 3);
58 theorem pt_inv_gen: \forall i.
59 (P i \to \exists h. i = S (h * 3)) \land
60 (T i \to \exists h,k. i = S (h * 3) * 3 \sup (S k)).
61 intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
62 [ lapply linear p_inv_O to H; decompose
63 | lapply linear t_inv_O to H; decompose
64 | inversion H1; clear H1; intros;
65 [ destruct; autobatch depth = 3
66 | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
67 lapply linear plus_inv_S_S_S to H4; decompose;
68 lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;
69 lapply linear H to H2; lapply linear H5 to H1; decompose;
70 rewrite > H; rewrite > H2; clear H H2;
71 rewrite < plus_n_Sm; rewrite > times_exp_x_y_Sz; autobatch depth = 2
73 | inversion H1; clear H1; intros;
74 [ lapply linear times_inv_S_m_SS to H2 as H0;
75 lapply linear H to H0; decompose; clear H2;
76 lapply linear H to H1; decompose; destruct;
78 | clear H2; lapply linear times_inv_S_m_SS to H3 as H0;
79 lapply linear H to H0; decompose; clear H;
80 lapply linear H2 to H1; decompose; destruct;
86 theorem p_inv_gen: \forall i. P i \to \exists h. i = S (h * 3).
87 intros; lapply depth = 1 pt_inv_gen; decompose;
88 lapply linear H1 to H as H0; autobatch depth = 1.
91 theorem t_inv_gen: \forall i. T i \to \exists h,k. i = (S (h * 3)) * 3 \sup (S k).
92 intros; lapply depth = 1 pt_inv_gen; decompose;
93 lapply linear H2 to H as H0; autobatch depth = 2.
96 theorem p_gen: \forall i. P (S (i * 3)).
97 intros; elim i names 0; clear i; intros;
98 [ simplify; autobatch depth = 2
99 | rewrite > plus_3_S3n ; autobatch depth = 2
103 theorem t_gen: \forall i,j. T (S (i * 3) * 3 \sup (S j)).
104 intros; elim j names 0; clear j; intros;
105 [ simplify in \vdash (? (? ? %)); autobatch depth = 2
106 | rewrite > times_exp_x_y_Sz; autobatch depth = 2