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.