]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/decidable_kit/decidable.ma
3478ef628e44c5871298100c970e3f36c9b05370
[helm.git] / helm / software / matita / library / decidable_kit / decidable.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 (* classical connectives for decidable properties *)
16
17 include "decidable_kit/streicher.ma".
18 include "datatypes/bool.ma".
19 include "logic/connectives.ma".
20 include "nat/compare.ma".
21  
22 (* se non includi connectives accade un errore in modo reproducibile*)
23
24 (* ### Prop <-> bool reflection predicate and lemmas for switching ### *)
25 inductive reflect (P : Prop) : bool  → Type ≝
26   | reflect_true : P → reflect P true
27   | reflect_false: ¬P → reflect P false.
28   
29 lemma b2pT : ∀P,b. reflect P b → b = true → P.
30 intros 3 (P b H); 
31 (* XXX generalize in match H; clear H; rewrite > Db;*)
32 (* la rewrite pare non andare se non faccio la generalize *)
33 (* non va inversion: intros (H);inversion H; *)
34 cases H; [intros; assumption | intros 1 (ABS); destruct ABS ]
35 qed.
36
37 lemma b2pF : ∀P,b. reflect P b → b = false → ¬P.
38 intros 3 (P b H); 
39 cases H; [intros 1 (ABS); destruct ABS| intros; assumption]
40 qed.
41
42 lemma p2bT : ∀P,b. reflect P b → P → b = true.
43 intros 4 (P b H Hp);
44 cases H (Ht Hf); [ intros; reflexivity | cases (Hf Hp)]
45 qed.
46
47 lemma p2bF : ∀P,b. reflect P b → ¬P → b = false.
48 intros 4 (P b H Hp);
49 cases H (Ht Hf); [ cases (Hp Ht) | reflexivity ]
50 qed.
51
52 lemma idP : ∀b:bool.reflect (b=true) b.
53 intros (b); cases b; [ constructor 1; reflexivity | constructor 2;]
54 unfold Not; intros (H); destruct H;
55 qed.
56
57 lemma prove_reflect : ∀P:Prop.∀b:bool.
58   (b = true → P) → (b = false → ¬P) → reflect P b.
59 intros 2 (P b); cases b; intros; [left|right] autobatch.
60 qed.   
61   
62 (* ### standard connectives/relations with reflection predicate ### *)
63
64 definition negb : bool → bool ≝ λb.match b with [ true ⇒ false | false ⇒ true].
65
66 lemma negbP : ∀b:bool.reflect (b = false) (negb b).
67 intros (b); cases b; simplify; [apply reflect_false | apply reflect_true]
68 [unfold Not; intros (H); destruct H | reflexivity]
69 qed.  
70
71 definition andb : bool → bool → bool ≝
72   λa,b:bool. match a with [ true ⇒ b | false ⇒ false ].
73   
74 lemma andbP : ∀a,b:bool. reflect (a = true ∧ b = true) (andb a b).
75 intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
76 [1,2,3,4: rewrite > H; split; reflexivity;
77 |5,6,7,8: unfold Not; intros (H1); cases H1; 
78           [destruct H|destruct H3|destruct H2|destruct H2]]
79 qed.
80
81 lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
82 intros (a b); apply prove_reflect; cases a; cases b; simplify; intros (H);
83 [1,2,3,4: try rewrite > H; [1,2:right|3,4:left] reflexivity
84 |5,6,7,8: unfold Not; intros (H1); [2,3,4: destruct H]; cases H1; destruct H2]
85 qed.
86
87 definition orb : bool → bool → bool ≝
88   λa,b.match a in bool with [true ⇒ true | false ⇒ b].
89   
90 lemma orbP : ∀a,b:bool. reflect (a = true ∨ b = true) (orb a b).
91 intros (a b); cases a; cases b; simplify;
92 [1,2,3: apply reflect_true; [1,2: left | right ]; reflexivity 
93 | apply reflect_false; unfold Not; intros (H); cases H (E E); destruct E]
94 qed. 
95
96 lemma orbC : ∀a,b. orb a b = orb b a.
97 intros (a b); cases a; cases b; autobatch. qed.
98
99 lemma lebP: ∀x,y. reflect (x ≤ y) (leb x y).
100 intros (x y); generalize in match (leb_to_Prop x y); 
101 cases (leb x y); simplify; intros (H); 
102 [apply reflect_true | apply reflect_false ] assumption.
103 qed. 
104
105 lemma leb_refl : ∀n.leb n n = true.
106 intros (n); apply (p2bT ? ? (lebP ? ?)); apply le_n; qed.
107
108 lemma lebW : ∀n,m. leb (S n) m = true → leb n m = true.
109 intros (n m H); lapply (b2pT ? ? (lebP ? ?) H); clear H;
110 apply (p2bT ? ? (lebP ? ?)); apply lt_to_le; assumption.
111 qed. 
112
113 definition ltb ≝ λx,y.leb (S x) y.
114
115 lemma ltbP: ∀x,y. reflect (x < y) (ltb x y). 
116 intros (x y); apply (lebP (S x) y);
117 qed.
118
119 lemma ltb_refl : ∀n.ltb n n = false.
120 intros (n); apply (p2bF ? ? (ltbP ? ?)); autobatch; 
121 qed.
122     
123 (* ### = between booleans as <-> in Prop ### *)    
124 lemma eq_to_bool : 
125   ∀a,b:bool. a = b → (a = true → b = true) ∧ (b = true → a = true).
126 intros (a b Eab); split; rewrite > Eab; intros; assumption;
127 qed.
128  
129 lemma bool_to_eq : 
130   ∀a,b:bool. (a = true → b = true) ∧ (b = true → a = true) → a = b.
131 intros (a b Eab); decompose;
132 generalize in match H; generalize in match H1; clear H; clear H1;
133 cases a; cases b; intros (H1 H2);
134 [2: rewrite > (H2 ?) | 3: rewrite > (H1 ?)] reflexivity;
135 qed.
136
137
138 lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
139 intros (n m); apply bool_to_eq; split; intros (H);
140 [1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch type] 
141    rewrite > (eqb_true_to_eq ? ? H1); autobatch
142 |2:cases (b2pT ? ? (lebP ? ?) H); 
143    [ elim n; [reflexivity|assumption] 
144    | simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ]
145    reflexivity]
146 qed.
147
148
149 (* OUT OF PLACE *)
150 lemma ltW : ∀n,m. n < m → n < (S m).
151 intros; unfold lt; unfold lt in H; autobatch. qed.
152
153 lemma ltbW : ∀n,m. ltb n m = true → ltb n (S m) = true.
154 intros (n m H); letin H1 ≝ (b2pT ? ? (ltbP ? ?) H); clearbody H1;
155 apply (p2bT ? ? (ltbP ? ?) (ltW ? ? H1));
156 qed.
157
158 lemma ltS : ∀n,m.n < m → S n < S m.
159 intros (n m H); apply (b2pT ? ? (ltbP ? ?)); simplify; apply (p2bT ? ? (ltbP ? ?) H);
160 qed.
161
162 lemma ltS' : ∀n,m.S n < S m → n < m.
163 intros (n m H); apply (b2pT ? ? (ltbP ? ?)); simplify; apply (p2bT ? ? (ltbP ? ?) H);
164 qed.
165
166 lemma ltb_n_Sm : ∀m.∀n:nat. (orb (ltb n m) (eqb n m)) = ltb n (S m).
167 intros (m n); apply bool_to_eq; split;
168 [1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
169     rewrite > (eqb_true_to_eq ? ? H1); simplify; 
170     rewrite > leb_refl; reflexivity  
171 |2: elim n in m ⊢ % 0;
172     [1: simplify; intros; cases n1; reflexivity;
173     |2: intros 1 (m); elim m 0;
174         [1: intros; apply (p2bT ? ? (orbP ? ?));
175             lapply (H (pred n1) ?); [1: reflexivity] clear H;
176             generalize in match H1; 
177             generalize in match Hletin;
178             cases n1; [1: simplify; intros; destruct H2]
179             intros; unfold pred in H; simplify in H;
180             cases (b2pT ? ? (orbP ? ?) H); [left|right] assumption; 
181         |2: clear m; intros (m IH1 IH2 w);
182             lapply (IH1 ? (pred w));
183             [3: generalize in match H; cases w; [2: intros; assumption]
184                 simplify; intros; destruct H1;
185             |1: intros; apply (IH2 (S n1)); assumption;
186             |2: generalize in match H; generalize in match Hletin; 
187                 cases w; [1: simplify; intros; destruct H2]
188                 intros (H H1); cases (b2pT ? ? (orbP ? ?) H);
189                 apply (p2bT ? ? (orbP ? ?));[left|right] assumption]]]]
190 qed.
191         
192 (* non mi e' chiaro a cosa serva ... *)
193 lemma congr_S : ∀n,m.n = m → S n = S m.
194 intros 1; cases n; intros; rewrite > H; reflexivity.
195 qed.