--- /dev/null
+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.
+
+
projects / helm.git / blobdiff