]> matita.cs.unibo.it Git - helm.git/blob - helm/coq-contribs/SUBSETS/st_logic.v
reorganization continues ...
[helm.git] / helm / coq-contribs / SUBSETS / st_logic.v
1 Require Export st_base.
2
3 Section Logic_Sets.
4
5    Section logic_aliases.
6 (*
7 Definition All := Pi.
8 *)
9       Definition LEx := Sigma.
10
11       Definition LBot := Empty.
12       
13       Definition LOr := Plus.
14
15       Definition LImp: Set -> Set -> Set := [S,T](Pi S [_:S]T).
16
17       Definition LAnd: Set -> Set -> Set := [S,T](Sigma S [_:S]T).
18       
19       Definition LNot: Set -> Set := [S](LImp S LBot).
20       
21       Definition LTop: Set := (LNot LBot).
22
23       Definition LIff: Set -> Set -> Set := [S,T](LAnd (LImp S T) (LImp T S)). 
24
25       Definition limp_i: (S,T:Set) (S -> T) -> (LImp S T).
26       Intros.
27       MApply '(abst S [_]T H).
28       Defined.
29
30       Definition limp_e: (S,T:Set) (LImp S T) -> (S->T).
31       Intros.
32       MApply '(ap S [_:S]T H H0).
33       Defined.
34           
35       Definition land_i: (S,T:Set) S -> T -> (LAnd S T).
36       Intros.
37       MApply '(pair S [_:S]T H H0).
38       Defined.
39
40       Definition land_e2: (T,S:Set) (LAnd S T) -> S.
41       Intros.
42       MElim H psplit.
43       Defined.
44
45       Definition land_e1: (S,T:Set) (LAnd S T) -> T.
46       Intros.
47       MElim H psplit.
48       Defined.
49 (*      
50 Definition all_e: (S:Set; a:S; P:S->Set) (All S P) -> (P a) := [S;a;P,f](ap S P f a).
51 *)      
52       Definition lex_i: (S:Set; a:S; P:S->Set) (P a) -> (LEx S P).
53       Intros.
54       MApply '(pair S P a H).
55       Defined. 
56
57       Definition lex_e: (S:Set; P:S->Set; P0:(LEx S P)->Set) ((a:S; y:(P a)) (P0 (lex_i S a P y))) -> (s:(LEx S P)) (P0 s).
58       Intros.
59       MElim s psplit.
60       MApply '(H a p).
61       Defined.
62       
63    End logic_aliases.
64
65    Section unit.
66
67       Definition One: Set := (List Empty).
68
69       Definition tt: One := (empty Empty).
70
71       Definition onerec: (P:One->Set) (P tt) -> (u:One) (P u).
72       Intros.
73       MElim 'u 'listrec.
74       MElim 's 'efq.
75       Defined.
76       
77       Definition OneFam: (P:One->Type) (P tt) -> (u:One) (P u).
78       Intros.
79       MElim 'u 'ListFam.
80       MElim 's 'EmptyFam.
81       Defined.
82       
83    End unit.
84
85    Section booleans.
86
87       Definition Boole: Set := (Plus One One).
88
89       Definition false: Boole := (in_l One One tt).
90
91       Definition true: Boole := (in_r One One tt). 
92
93       Definition ite: (P:Boole->Set) (P false) -> (P true) -> (b:Boole) (P b).
94       Intros.
95       MElim 'b 'when.
96       MElim 's 'onerec.
97       MElim 't 'onerec.
98       Defined.
99
100       Definition BooleFam: (P:Boole->Type) 
101                            (P false) -> (P true) -> (b:Boole) (P b).
102       Intros.
103       MElim 'b 'PlusFam.
104       MElim 's 'OneFam.
105       MElim 't 'OneFam.
106       Defined.
107 (*
108 Definition BF: Set -> Set -> Boole -> Set := (BooleFam [_]Set).
109       
110 Definition Two: Set := Boole.
111 *)
112    End booleans.
113    
114 End Logic_Sets.
115
116 Section Logic_Hints.
117 (*
118 Section logic_fold.
119
120 Theorem Top_fold: (P:Set->Set) (P Top) -> (P (Imp Bot Bot)).
121 Intros.
122 Apply (sid_repl (Imp Bot Bot) Top).
123 Apply sid_r.
124 Assumption.
125 Qed.
126
127 End logic_fold.
128 *)
129    Section logic_red.
130
131       Theorem LTop_red: LTop.
132       Unfold LTop LNot.
133       Apply limp_i.
134       Intros.
135       Assumption.
136       Qed.
137 (*
138 Theorem Top_And_red: (A:Set) A -> (And Top A).
139 Intros.
140 Apply and_i.
141 Apply Top_red.
142 Assumption.
143 Qed.
144 *)
145    End logic_red.
146
147 End Logic_Hints.
148
149 Section Logic_Results.
150
151    Section boole_indipendence.
152
153       Axiom lor_p4: (A,B:Set; a:A; b:B) 
154                     (Id (LOr A B) (in_l A B a) (in_r A B b)) -> Empty.
155
156       Axiom boole_p4: (Id Boole false true) -> Empty. (**)
157
158    End boole_indipendence.
159
160    Section logic_results.
161    
162       Theorem lor_e: (A,B,C:Set) (A -> C) -> (B -> C) -> (LOr A B) -> C.
163       Intros.
164       MApply '(when A B [_:?]C).
165       MApply '(H s).
166       MApply '(H0 t).
167       Qed.
168
169       Theorem lnot_i: (S:Set) (S -> LBot) -> (LNot S).
170       Intros.
171       Unfold LNot.
172       MApply 'limp_i.
173       MApply 'H.
174       Qed.
175       
176       Theorem lnot_e: (S:Set) (LNot S) -> S -> LBot.
177       Unfold LNot.
178       Intros.
179       MApply '(limp_e S).
180       Qed.
181
182       Theorem liff_i: (A,B:Set) (A -> B) -> (B -> A) -> (LIff A B). 
183       Intros.
184       Unfold LIff.
185       (MApply land_i; MApply limp_i).
186       MApply H.
187       MApply H0.
188       Qed.
189
190       Theorem liff_e1: (A,B:Set) A -> (LIff A B) -> B.
191       Unfold LIff.
192       Intros.
193       MApply '(limp_e A).
194       MApply '(land_e2 (LImp B A)).
195       Qed.
196
197       Theorem liff_e2: (B,A:Set) B -> (LIff A B) -> A.
198       Unfold LIff.
199       Intros.
200       MApply '(limp_e B).
201       MApply '(land_e1 (LImp A B)).
202       Qed.
203 (*
204 Theorem iff_trans: (C,A,B:Set) (Iff A C) -> (Iff C B) -> (Iff A B).
205 Intros.
206 MApply iff_i.
207 MApply (iff_e1 C).
208 MApply (iff_e1 A).
209 MApply (iff_e2 C).
210 MApply (iff_e2 B).
211 Qed.
212    
213 Theorem iff_sym: (A,B:Set) (Iff B A) -> (Iff A B).
214 Intros.
215 MApply iff_i.
216 MApply (iff_e2 A).
217 MApply (iff_e1 B).
218 Qed.
219 *)      
220       Theorem lnot_liff_lbot: (A:Set) (LIff A (LNot A)) -> LBot.
221       Intros.
222       MApply '(lnot_e (LNot A)).
223       MApply 'lnot_i.
224       MApply '(lnot_e A).
225       MApply '(liff_e2 (LNot A)).
226       MApply 'lnot_i.
227       MApply '(lnot_e A).
228       MApply '(liff_e1 A).
229       Qed.
230 (*
231 Theorem imp_r: (A:Set) (Imp A A).
232 Intros.
233 MApply imp_i.
234 Qed.
235
236 Theorem imp_trans: (C,A,B:Set) (Imp A C) -> (Imp C B) -> (Imp A B).
237 Intros.
238 MApply imp_i.
239 MApply (imp_e C).
240 MApply (imp_e A).
241 Qed.       
242       
243 Theorem all_sigma_l: (S:Set; T:S->Set; P:(Sigma S T)->Set) ((a:S; b:(T a)) (P (pair S T a b))) -> (p:(Sigma S T)) (P p).
244 Intros.
245 MElim p psplit.
246 Apply (H a y).
247 Qed.
248 *)   
249    End logic_results.
250
251 End Logic_Results.
252
253