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