helm/coq-contribs/SUBSETS/st_base.v

   1 Section Base_Definitions.
   2
   3    Section inductive_sets.
   4
   5       Inductive Set Empty := .
   6
   7       Inductive Set List [S:Set] := empty: (List S) | fr: (List S) -> S -> (List S).
   8
   9       Inductive Id [S:Set; a:S]: S -> Set := id_r: (Id S a a).
  10
  11       Inductive Set Pi [S:Set; P:S->Set] := abst: ((a:S) (P a)) -> (Pi S P).
  12
  13       Inductive Set Sigma [S:Set; P:S->Set] := pair: (a:S) (P a) -> (Sigma S P).
  14
  15       Inductive Set Plus [S,T:Set] := in_l : S -> (Plus S T) | in_r : T -> (Plus S T).
  16 (*
  17 Inductive SId [A:Set] : Set -> Set := sid_r: (SId A A).
  18 *)
  19    End inductive_sets.
  20
  21    Section eliminators.
  22
  23       Definition efq := Empty_rec.
  24
  25       Definition listrec := List_rec.
  26
  27       Definition idrec := Id_rec.
  28
  29       Definition fsplit := Pi_rec.
  30
  31       Definition psplit := Sigma_rec.
  32
  33       Definition when := Plus_rec.
  34
  35       Definition EmptyFam := Empty_rect.
  36
  37       Definition ListFam := List_rect.
  38
  39       Definition IdFam := Id_rect.
  40
  41       Definition PiFam := Pi_rect.
  42
  43       Definition SigmaFam := Sigma_rect.
  44
  45       Definition PlusFam := Plus_rect.
  46
  47       Definition ap: (S:Set; P:S->Set) (Pi S P) -> (a:S) (P a).
  48       Intros.
  49       Elim H.
  50       Intros.
  51       Apply (p a).
  52       Defined.
  53
  54       Definition sp: (S:Set; P:S->Set) (Sigma S P) -> S.
  55       Intros.
  56       Elim H.
  57       Intros.
  58       Assumption.
  59       Defined.
  60
  61       Definition sq: (S:Set; P:S->Set; p:(Sigma S P)) (P (sp S P p)).
  62       Intros.
  63       Elim p.
  64       Intros.
  65       Unfold sp.
  66       Simpl.
  67       Assumption.
  68       Defined.
  69
  70    End eliminators.
  71
  72    Section functions.
  73
  74       Definition id: (S:Set) S -> S.
  75       Intros.
  76       Assumption.
  77       Defined.
  78
  79       Definition comp: (R,S,T:Set) (R -> S) -> (S -> T) -> (R -> T).
  80       Intros.
  81       Apply H0.
  82       Apply H.
  83       Assumption.
  84       Defined.
  85
  86    End functions.
  87
  88 End Base_Definitions.
  89
  90 Section Base_Results.
  91
  92    Section general_results.
  93
  94       Theorem mcut: (S,T:Set) S -> (S -> T) -> T.
  95       Intros.
  96       Apply H0.
  97       Assumption.
  98       Qed.
  99
 100    End general_results.
 101
 102    Section ID_results.
 103
 104       Theorem id_repl: (S:Set; a,b:S; P:S->Set) (Id ? b a) -> (P b) -> (P a).
 105       Intros.
 106       Elim H.
 107       Assumption.
 108       Qed.
 109
 110       Theorem id_comm: (S:Set; a,b:S) (Id ? b a) -> (Id ? a b).
 111       Intros.
 112       Apply (id_repl S a b).
 113       Assumption.
 114       Apply id_r.
 115       Qed.
 116
 117       Theorem id_trans: (S:Set; c,a,b:S) (Id S a c) -> (Id S c b) -> (Id S a b).
 118       Intros.
 119       Apply (id_repl S b c).
 120       Assumption.
 121       Assumption.
 122       Qed.
 123
 124       Theorem id_comp: (S,T:Set; f:S->T; a,b:S) (Id S a b) -> (Id T (f a) (f b)).
 125       Intros.
 126       Apply (id_repl ? b a).
 127       Assumption.
 128       Apply id_r.
 129       Qed.
 130
 131       Axiom id_ext: (S,T:Set; f,g:S->T) ((a:S) (Id T (f a) (g a))) -> (Id S->T f g).
 132
 133    End ID_results.
 134 (*
 135 Section SID_results.
 136
 137 Theorem sid_repl: (A,B:Set; P:Set->Set) (SId B A) -> (P B) -> (P A).
 138 Intros.
 139 Elim H.
 140 Assumption.
 141 Qed.
 142
 143 Theorem sid_comp: (P:Set->Set; A,B:Set) (SId A B) -> (SId (P A) (P B)).
 144 Intros.
 145 Apply (sid_repl B A).
 146 Assumption.
 147 Apply sid_r.
 148 Qed.
 149
 150 Axiom sid_ext: (S:Set; P:(S->Set)->Set; Q,R:S->Set) ((a:S) (SId (Q a) (R a))) -> (SId (P Q) (P R)).
 151
 152 End SID_results.
 153 *)
 154    Section indipendence.
 155
 156       Axiom list_p4: (S:Set; l:(List S); a:S) (Id (List S) (empty S) (fr S l a)) -> Empty.
 157
 158       Axiom plus_p4: (S:Set; a:S; T:Set; b:T) (Id (Plus S T) (in_l S T a) (in_r S T b)) -> Empty.
 159 (*
 160 Axiom id_ctt: (S:Set) (P:(a:S)(Id S a a) -> Set) ((a:S) (P a (id_r S a))) -> (a:S; p:(Id S a a)) (P a p).
 161 *)
 162    End indipendence.
 163
 164 End Base_Results.
 165
 166 Tactic Definition MTrivial := Try Apply id_r; (* Try Apply sid_r; *)
 167 (*|*)                         Try Assumption; Try Apply id_comm;
 168                               Try Assumption; Try Apply id_comm.
 169
 170 Tactic Definition MFold := Idtac.
 171
 172 Tactic Definition MRed := Idtac.
 173
 174 Tactic Definition MAuto := MTrivial; MFold; MRed.
 175
 176 Tactic Definition MSimpl := Simpl; MAuto.
 177
 178 Tactic Definition MElim v e := Pattern v; Elim v using e; Simpl;
 179                                Intros; MAuto.
 180
 181 Tactic Definition MApply t := Apply t; Intros; MTrivial.
 182
 183 Tactic Definition MCut t := MApply '(mcut t).
 184
 185 Tactic Definition UnIntros T t := Apply (mcut T); Try Assumption; Clear t.