]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/character/classes/props_pt.ma
milestone update in ground
[helm.git] / matitaB / matita / contribs / character / classes / props_pt.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "classes/defs.ma".
16
17 theorem p_inv_O: P 0 → False.
18  intros; inversion H;intros;
19  [apply (not_eq_O_S ? H1)
20  |autobatch.
21  ]
22 qed.
23
24 theorem t_inv_O: T 0 → False.
25  intros; inversion H; clear H; intros;
26  [ lapply linear times_inv_O3_S to H1; destruct; autobatch depth = 2
27  | lapply linear times_inv_O3_S to H2; destruct; autobatch depth = 2
28  ].
29 qed.
30
31 theorem p_pos: ∀i. P i → ∃k. i = S k.
32  intros 1; elim i 0; clear i; intros;
33  [ lapply linear p_inv_O to H; decompose
34  | autobatch depth = 2
35  ].
36 qed.
37
38 theorem t_pos: ∀i. T i → ∃k. i = S k.
39  intros 1; elim i names 0; clear i; intros;
40  [ lapply linear t_inv_O to H; decompose
41  | autobatch depth = 2
42  ].
43 qed.
44
45 theorem t_1: T 1 → False.
46  intros; inversion H; clear H; intros;
47  [ lapply not_3_divides_1 to H1; decompose
48  | lapply not_3_divides_1 to H2; decompose
49  ].
50 qed.
51
52 theorem t_3: T 3.
53  change in ⊢ (? %) with (1 * 3);
54  autobatch depth = 2.
55 qed.
56
57 theorem pt_inv_gen: ∀i. 
58                     (P i → ∃h. i = S (h * 3)) ∧
59                     (T i → ∃h,k. i = S (h * 3) * 3 \sup (S k)).
60  intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
61  [ lapply linear p_inv_O to H; decompose
62  | lapply linear t_inv_O to H; decompose
63  | inversion H1; clear H1; intros;
64    [ destruct; autobatch paramodulation
65    | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
66      lapply linear plus_inv_S_S_S to H4; decompose;
67      lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;
68      lapply linear H to H2; lapply linear H5 to H1; decompose;
69      rewrite > H; rewrite > H2; clear H H2;
70      rewrite < plus_n_Sm; rewrite > times_exp_x_y_Sz; autobatch depth = 2
71    ]
72  | inversion H1; clear H1; intros;
73    [ lapply linear times_inv_S_m_SS to H2 as H0;
74      lapply linear H to H0; decompose; clear H2;
75      lapply linear H to H1; decompose; destruct;
76      autobatch depth = 4
77    | clear H2; lapply linear times_inv_S_m_SS to H3 as H0;
78      lapply linear H to H0; decompose; clear H;
79      lapply linear H2 to H1; decompose; destruct;
80      autobatch depth = 4
81    ]
82  ].
83 qed.
84
85 theorem p_inv_gen: ∀i. P i → ∃h. i = S (h * 3).
86  intros; lapply depth = 1 pt_inv_gen; decompose;
87  lapply linear H1 to H as H0; autobatch depth = 1.
88 qed.
89
90 theorem t_inv_gen: ∀i. T i → ∃h,k. i = (S (h * 3)) * 3 \sup (S k).
91  intros; lapply depth = 1 pt_inv_gen; decompose;
92  lapply linear H2 to H as H0; autobatch depth = 2.
93 qed.
94
95 theorem p_gen: ∀i. P (S (i * 3)).
96  intros; elim i names 0; clear i; intros;
97  [ simplify; autobatch depth = 2
98  | rewrite > plus_3_S3n ; autobatch depth = 2
99  ].
100 qed.
101
102 theorem t_gen: ∀i,j. T (S (i * 3) * 3 \sup (S j)).
103  intros; elim j names 0; clear j; intros;
104  [ simplify in ⊢ (? (? ? %)); autobatch depth = 2
105  | rewrite > times_exp_x_y_Sz; autobatch depth = 2
106  ].
107 qed.