Require Export st_logic.

Section Nat_Sets.

   Section natural_numbers.

      Definition N: Set := (List One).

      Definition zero: N := (empty One).

      Definition succ: N -> N := [n](fr One n tt).
      
      Definition natrec: (P:N->Set) (P zero) -> 
                         ((n:N) (P n) -> (P (succ n))) -> (n:N)(P n).
      Intros.
      MElim 'n 'listrec.
      MElim 's 'onerec.
      MApply '(H0 l).
      Defined.

      Definition NatFam: (P:N->Type) (P zero) -> 
                         ((n:N) (P n) -> (P (succ n))) -> (n:N)(P n).
      Intros.
      MElim 'n 'ListFam.
      MElim 's 'OneFam.
      MApply '(X0 l).
      Defined.
           
      Definition one: N := (succ zero).
(*      
Definition two:N := (succ one). 
*)      
   End natural_numbers.
(*
Section sequences.
   
Definition ListS := [S:Set](N -> (List S)).
      
Definition BooleS: Set := N -> Boole.
      
Definition NS := N -> N.      
              
Definition trues:BooleS := [_]true. 

End sequences.
*)   
End Nat_Sets.

Section Nat_Functions.
(*
Section bounded_iteration.

Variable S:Set; e:S; f:S->S->S.
   
Definition bs_iter: (N -> S) -> N -> S := [s](natrec [_]S e [m](f (s m))).
      
Definition rbs_iter: (N -> S) -> N -> S := [s;n](bs_iter s (succ n)).
   
End bounded_iteration.

Section nat_boolean_eq.
         
Variable S:Set.

Definition n_id: N -> N -> Boole := (natrec [_]N->Boole (natrec [_]Boole true [_;_]false) 
                                    [_;pm'](natrec [_]Boole false [n';_](pm' n'))).  

Definition ifeq: N -> N -> S -> S -> S := [m,n;a;b](ite [_]S b a (n_id m n)).

Definition ifz: N -> S -> S -> S := [n;a;b](natrec [_]S a [_;_]b n).

End nat_boolean_eq.
*)
   Section less_equal.
   
      Definition b_le: N -> N -> Boole := (natrec [_]N->Boole [n]true [m';p](natrec [_]Boole false [n';_](p n'))).
      
      Definition LE: N -> N -> Set := [m,n](Id Boole (b_le m n) true).
      
      Definition GT: N -> N -> Set := [m,n](Id Boole (b_le m n) false).
   
   End less_equal.

End Nat_Functions.

Section Nat_Hints.

   Section nat_fold.
   
      Theorem succ_fold: (n:N; P:N->Set) (P (succ n)) -> (P (fr One n tt)). 
      Intros.
      Assumption.
      Qed.
(*
Theorem LE_fold: (m,n:N; P:Set->Set) (P (LE m n)) -> (P (Id Boole (b_le m n) true)).
Intros.
Assumption.
Qed.
*)
   End nat_fold.      

End Nat_Hints.

Section Nat_Results.

   Section nat_indipendence.
   
      Theorem n_p4: (n:N) (Id N zero (succ n)) -> Empty.
      Intros.
      MApply '(list_p4 One n tt).
      Qed.
      
      Theorem n_false: (n:N; P:Set) (Id N zero (succ n)) -> P.
      Intros.
      MCut 'Empty.
      MApply '(n_p4 n).
      MElim 'H0 'efq.
      Qed.
   
   End nat_indipendence.

   Section b_le_results.

      Theorem le_wf: (n:N) (LE zero n). 
      Intros.
      Unfold LE.
      MApply 'id_r.
      Qed.

      Theorem le_comp_succ: (m,n:N) (LE m n) -> (LE (succ m) (succ n)).
      Intros.
      Assumption.
      Qed.
(*      
Theorem le_ssucc: (m,n:N) (LE (succ m) (succ n)) -> (LE m n).
Intros.
Assumption.
Qed.
*)
      Theorem le_false: (n:N; P:Set) (LE (succ n) zero) -> P.
      Intros n P.
      Unfold LE.
      MSimpl.
      Intros.
      MCut 'Empty.
      MApply 'boole_p4.
      MElim 'H0 'efq.
      Qed.

      Theorem le_r: (n:N) (LE n n).
      Intros.
      MElim 'n 'natrec.
      MApply 'le_wf.
      Qed.
   
      Theorem le_succ: (n:N) (LE n (succ n)).
      Intros.
      MElim 'n 'natrec.
      MApply 'le_wf.
      Qed.

      Theorem le_zero: (n:N) (LE n zero) -> (Id N n zero).
      Intros n.
      MElim 'n 'natrec.
      MApply '(le_false n0).
      Qed.

      Theorem le_trans: (b,c,a:N) (LE a b) -> (LE b c) -> (LE a c).
      Intros b.
      Elim b using natrec.
      Intros c a.
      MElim 'a 'natrec.
      MApply '(le_false n).
      Intros b' H c.
      Elim c using natrec.
      Intros.
      MApply '(le_false b').
      Intros c' H' a.
      MElim 'a 'natrec.
      MApply 'le_comp_succ.
      MCut '(LE n b').
      MCut '(LE b' c').
      MApply '(H c' n).
      Qed.
      
      Theorem gt_wf: (n:N) (GT (succ n) zero).
      Intros.
      Unfold GT.
      MApply 'id_r.
      Qed.
      
      Theorem gt_comp_succ: (m,n:N) (GT m n) -> (GT (succ m) (succ n)).
      Intros.
      Assumption.
      Qed.

      Theorem gt_false: (n:N; P:Set) (GT zero n) -> P.
      Intros n P.
      Unfold GT.
      MSimpl.
      Intros.
      MCut 'Empty.
      MApply 'boole_p4.
      MElim 'H0 'efq.
      Qed.

      Theorem le_gt: (m,n:N) (LE (succ n) m) -> (GT m n).
      Intros m.
      Elim m using natrec.
      Intros.
      MApply '(le_false n).
      Intros m' H n.
      Elim n using natrec.
      Intros.
      MApply 'gt_wf.
      Intros n' H1 H2.
      MApply 'gt_comp_succ.
      MApply '(H n').
      Qed.

      Theorem gt_le: (m,n:N) (GT m n) -> (LE (succ n) m).
      Intros m.
      Elim m using natrec.
      Intros.
      MApply '(gt_false n).
      Intros m' H n.
      MElim 'n natrec.
      MApply 'le_comp_succ.
      MApply 'le_wf.
      MApply 'le_comp_succ.
      MApply '(H n0).
      Qed.
      
      Theorem le_gt_trans: (b,c,a:N) (LE b a) -> (GT b c) -> (GT a c).
      Intros.
      MApply 'le_gt.
      MApply '(le_trans b).
      MApply 'gt_le.
      Qed.

      Theorem boole_di: (b:Boole) (LOr (Id Boole b true) (Id Boole b false)).
      Intros.
      MElim 'b 'ite.
      MApply 'in_r.
      MApply 'in_l.
      Qed.
   
      Theorem le_di: (m,n:N) (LOr (LE m n) (GT m n)).
      Intros.
      Unfold LE GT.
      MApply '(boole_di (b_le m n)).
      Qed.
(*
Theorem ble_trip: (m,n:N; P:N->Set) ((n:N) (LE n m) -> (P n)) -> ((n:N) (GT n m) -> (P n)) -> (P n).
Intros.
MApply '(or_e (LE n m) (GT n m)).
MApply '(H n).
MApply '(H0 n).
MApply 'ble_tri.
Qed.
*)
   End b_le_results.

End Nat_Results.