X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FSUBSETS%2Fst_logic.v;fp=helm%2Fcoq-contribs%2FSUBSETS%2Fst_logic.v;h=0455d3877ad89ce3684dfed9d0427a589dfd4268;hb=65f400affe20fa3fe66b9a998ced5d6f64a23b45;hp=0000000000000000000000000000000000000000;hpb=50377dde5b5b1a8e5c7b2fb48b47defde9508b50;p=helm.git diff --git a/helm/coq-contribs/SUBSETS/st_logic.v b/helm/coq-contribs/SUBSETS/st_logic.v new file mode 100644 index 000000000..0455d3877 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/st_logic.v @@ -0,0 +1,253 @@ +Require Export st_base. + +Section Logic_Sets. + + Section logic_aliases. +(* +Definition All := Pi. +*) + Definition LEx := Sigma. + + Definition LBot := Empty. + + Definition LOr := Plus. + + Definition LImp: Set -> Set -> Set := [S,T](Pi S [_:S]T). + + Definition LAnd: Set -> Set -> Set := [S,T](Sigma S [_:S]T). + + Definition LNot: Set -> Set := [S](LImp S LBot). + + Definition LTop: Set := (LNot LBot). + + Definition LIff: Set -> Set -> Set := [S,T](LAnd (LImp S T) (LImp T S)). + + Definition limp_i: (S,T:Set) (S -> T) -> (LImp S T). + Intros. + MApply '(abst S [_]T H). + Defined. + + Definition limp_e: (S,T:Set) (LImp S T) -> (S->T). + Intros. + MApply '(ap S [_:S]T H H0). + Defined. + + Definition land_i: (S,T:Set) S -> T -> (LAnd S T). + Intros. + MApply '(pair S [_:S]T H H0). + Defined. + + Definition land_e2: (T,S:Set) (LAnd S T) -> S. + Intros. + MElim H psplit. + Defined. + + Definition land_e1: (S,T:Set) (LAnd S T) -> T. + Intros. + MElim H psplit. + Defined. +(* +Definition all_e: (S:Set; a:S; P:S->Set) (All S P) -> (P a) := [S;a;P,f](ap S P f a). +*) + Definition lex_i: (S:Set; a:S; P:S->Set) (P a) -> (LEx S P). + Intros. + MApply '(pair S P a H). + Defined. + + 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). + Intros. + MElim s psplit. + MApply '(H a p). + Defined. + + End logic_aliases. + + Section unit. + + Definition One: Set := (List Empty). + + Definition tt: One := (empty Empty). + + Definition onerec: (P:One->Set) (P tt) -> (u:One) (P u). + Intros. + MElim 'u 'listrec. + MElim 's 'efq. + Defined. + + Definition OneFam: (P:One->Type) (P tt) -> (u:One) (P u). + Intros. + MElim 'u 'ListFam. + MElim 's 'EmptyFam. + Defined. + + End unit. + + Section booleans. + + Definition Boole: Set := (Plus One One). + + Definition false: Boole := (in_l One One tt). + + Definition true: Boole := (in_r One One tt). + + Definition ite: (P:Boole->Set) (P false) -> (P true) -> (b:Boole) (P b). + Intros. + MElim 'b 'when. + MElim 's 'onerec. + MElim 't 'onerec. + Defined. + + Definition BooleFam: (P:Boole->Type) + (P false) -> (P true) -> (b:Boole) (P b). + Intros. + MElim 'b 'PlusFam. + MElim 's 'OneFam. + MElim 't 'OneFam. + Defined. +(* +Definition BF: Set -> Set -> Boole -> Set := (BooleFam [_]Set). + +Definition Two: Set := Boole. +*) + End booleans. + +End Logic_Sets. + +Section Logic_Hints. +(* +Section logic_fold. + +Theorem Top_fold: (P:Set->Set) (P Top) -> (P (Imp Bot Bot)). +Intros. +Apply (sid_repl (Imp Bot Bot) Top). +Apply sid_r. +Assumption. +Qed. + +End logic_fold. +*) + Section logic_red. + + Theorem LTop_red: LTop. + Unfold LTop LNot. + Apply limp_i. + Intros. + Assumption. + Qed. +(* +Theorem Top_And_red: (A:Set) A -> (And Top A). +Intros. +Apply and_i. +Apply Top_red. +Assumption. +Qed. +*) + End logic_red. + +End Logic_Hints. + +Section Logic_Results. + + Section boole_indipendence. + + Axiom lor_p4: (A,B:Set; a:A; b:B) + (Id (LOr A B) (in_l A B a) (in_r A B b)) -> Empty. + + Axiom boole_p4: (Id Boole false true) -> Empty. (**) + + End boole_indipendence. + + Section logic_results. + + Theorem lor_e: (A,B,C:Set) (A -> C) -> (B -> C) -> (LOr A B) -> C. + Intros. + MApply '(when A B [_:?]C). + MApply '(H s). + MApply '(H0 t). + Qed. + + Theorem lnot_i: (S:Set) (S -> LBot) -> (LNot S). + Intros. + Unfold LNot. + MApply 'limp_i. + MApply 'H. + Qed. + + Theorem lnot_e: (S:Set) (LNot S) -> S -> LBot. + Unfold LNot. + Intros. + MApply '(limp_e S). + Qed. + + Theorem liff_i: (A,B:Set) (A -> B) -> (B -> A) -> (LIff A B). + Intros. + Unfold LIff. + (MApply land_i; MApply limp_i). + MApply H. + MApply H0. + Qed. + + Theorem liff_e1: (A,B:Set) A -> (LIff A B) -> B. + Unfold LIff. + Intros. + MApply '(limp_e A). + MApply '(land_e2 (LImp B A)). + Qed. + + Theorem liff_e2: (B,A:Set) B -> (LIff A B) -> A. + Unfold LIff. + Intros. + MApply '(limp_e B). + MApply '(land_e1 (LImp A B)). + Qed. +(* +Theorem iff_trans: (C,A,B:Set) (Iff A C) -> (Iff C B) -> (Iff A B). +Intros. +MApply iff_i. +MApply (iff_e1 C). +MApply (iff_e1 A). +MApply (iff_e2 C). +MApply (iff_e2 B). +Qed. + +Theorem iff_sym: (A,B:Set) (Iff B A) -> (Iff A B). +Intros. +MApply iff_i. +MApply (iff_e2 A). +MApply (iff_e1 B). +Qed. +*) + Theorem lnot_liff_lbot: (A:Set) (LIff A (LNot A)) -> LBot. + Intros. + MApply '(lnot_e (LNot A)). + MApply 'lnot_i. + MApply '(lnot_e A). + MApply '(liff_e2 (LNot A)). + MApply 'lnot_i. + MApply '(lnot_e A). + MApply '(liff_e1 A). + Qed. +(* +Theorem imp_r: (A:Set) (Imp A A). +Intros. +MApply imp_i. +Qed. + +Theorem imp_trans: (C,A,B:Set) (Imp A C) -> (Imp C B) -> (Imp A B). +Intros. +MApply imp_i. +MApply (imp_e C). +MApply (imp_e A). +Qed. + +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). +Intros. +MElim p psplit. +Apply (H a y). +Qed. +*) + End logic_results. + +End Logic_Results. + +