a contribution about subset theory in an intuitionistic and predicative foundation

[helm.git] / helm / coq-contribs / SUBSETS / st_base.v

diff --git a/helm/coq-contribs/SUBSETS/st_base.v b/helm/coq-contribs/SUBSETS/st_base.v
new file mode 100644 (file)
index 0000000..79b2507
--- /dev/null
+++ b/helm/coq-contribs/SUBSETS/st_base.v
@@ -0,0 +1,185 @@
+Section Base_Definitions.
+
+   Section inductive_sets.
+
+      Inductive Set Empty := .
+
+      Inductive Set List [S:Set] := empty: (List S) | fr: (List S) -> S -> (List S).
+
+      Inductive Id [S:Set; a:S]: S -> Set := id_r: (Id S a a).
+
+      Inductive Set Pi [S:Set; P:S->Set] := abst: ((a:S) (P a)) -> (Pi S P).
+
+      Inductive Set Sigma [S:Set; P:S->Set] := pair: (a:S) (P a) -> (Sigma S P).
+      
+      Inductive Set Plus [S,T:Set] := in_l : S -> (Plus S T) | in_r : T -> (Plus S T). 
+(*      
+Inductive SId [A:Set] : Set -> Set := sid_r: (SId A A).
+*)
+   End inductive_sets.
+   
+   Section eliminators.
+
+      Definition efq := Empty_rec.
+
+      Definition listrec := List_rec.
+
+      Definition idrec := Id_rec.
+
+      Definition fsplit := Pi_rec.
+
+      Definition psplit := Sigma_rec.
+
+      Definition when := Plus_rec.
+      
+      Definition EmptyFam := Empty_rect.
+
+      Definition ListFam := List_rect.
+      
+      Definition IdFam := Id_rect.
+      
+      Definition PiFam := Pi_rect.
+      
+      Definition SigmaFam := Sigma_rect.
+
+      Definition PlusFam := Plus_rect.
+
+      Definition ap: (S:Set; P:S->Set) (Pi S P) -> (a:S) (P a).
+      Intros.
+      Elim H.
+      Intros.
+      Apply (p a).
+      Defined.
+
+      Definition sp: (S:Set; P:S->Set) (Sigma S P) -> S.
+      Intros.
+      Elim H.
+      Intros.
+      Assumption.
+      Defined.
+
+      Definition sq: (S:Set; P:S->Set; p:(Sigma S P)) (P (sp S P p)).
+      Intros.
+      Elim p.
+      Intros.
+      Unfold sp.
+      Simpl.
+      Assumption.
+      Defined.
+
+   End eliminators.
+
+   Section functions.
+   
+      Definition id: (S:Set) S -> S.
+      Intros.
+      Assumption.
+      Defined.
+
+      Definition comp: (R,S,T:Set) (R -> S) -> (S -> T) -> (R -> T).
+      Intros.
+      Apply H0.
+      Apply H.
+      Assumption.
+      Defined.
+
+   End functions.
+
+End Base_Definitions.
+
+Section Base_Results.
+
+   Section general_results.
+
+      Theorem mcut: (S,T:Set) S -> (S -> T) -> T.
+      Intros.
+      Apply H0.
+      Assumption.
+      Qed.
+
+   End general_results.
+
+   Section ID_results.
+
+      Theorem id_repl: (S:Set; a,b:S; P:S->Set) (Id ? b a) -> (P b) -> (P a).
+      Intros.
+      Elim H.
+      Assumption.
+      Qed.
+
+      Theorem id_comm: (S:Set; a,b:S) (Id ? b a) -> (Id ? a b).
+      Intros.
+      Apply (id_repl S a b).
+      Assumption.
+      Apply id_r.
+      Qed.
+   
+      Theorem id_trans: (S:Set; c,a,b:S) (Id S a c) -> (Id S c b) -> (Id S a b).
+      Intros.
+      Apply (id_repl S b c).
+      Assumption.
+      Assumption.
+      Qed.
+
+      Theorem id_comp: (S,T:Set; f:S->T; a,b:S) (Id S a b) -> (Id T (f a) (f b)).
+      Intros.
+      Apply (id_repl ? b a).
+      Assumption.
+      Apply id_r.
+      Qed.
+   
+      Axiom id_ext: (S,T:Set; f,g:S->T) ((a:S) (Id T (f a) (g a))) -> (Id S->T f g).
+   
+   End ID_results.
+(*
+Section SID_results.
+
+Theorem sid_repl: (A,B:Set; P:Set->Set) (SId B A) -> (P B) -> (P A).
+Intros.
+Elim H.
+Assumption.
+Qed.
+
+Theorem sid_comp: (P:Set->Set; A,B:Set) (SId A B) -> (SId (P A) (P B)).
+Intros.
+Apply (sid_repl B A).
+Assumption.
+Apply sid_r.
+Qed.
+
+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)).
+
+End SID_results.
+*)
+   Section indipendence.
+   
+      Axiom list_p4: (S:Set; l:(List S); a:S) (Id (List S) (empty S) (fr S l a)) -> Empty.
+
+      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.
+(*
+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). 
+*)   
+   End indipendence.
+
+End Base_Results.
+
+Tactic Definition MTrivial := Try Apply id_r; (* Try Apply sid_r; *) 
+(*|*)                         Try Assumption; Try Apply id_comm; 
+                              Try Assumption; Try Apply id_comm.
+
+Tactic Definition MFold := Idtac. 
+
+Tactic Definition MRed := Idtac.
+
+Tactic Definition MAuto := MTrivial; MFold; MRed.
+
+Tactic Definition MSimpl := Simpl; MAuto.
+
+Tactic Definition MElim v e := Pattern v; Elim v using e; Simpl; 
+                               Intros; MAuto.
+
+Tactic Definition MApply t := Apply t; Intros; MTrivial.
+
+Tactic Definition MCut t := MApply '(mcut t).
+
+Tactic Definition UnIntros T t := Apply (mcut T); Try Assumption; Clear t.