Require Export st_nat.

Section Arith_Functions.

   Section head_tail_append.

      Variable S:Set.
(*
Definition hd: (List S) -> (List S) := (listrec S [_](List S) (empty ?) [_;_](fr ? (empty ?))).
*)
      Definition hde: S -> (List S) -> S := [a](listrec S [_]S a [_;_;a]a).
      
      Definition tl: (List S) -> (List S) := (listrec S [_](List S) (empty ?) [v;_;_]v).

      Definition app: (List S) -> (List S) -> (List S) := [v](listrec S [_](List S) v [_;p;a](fr S p a)). 

      Definition app_three: (List S) -> (List S) -> (List S) -> (List S) := [v,w](app (app v w)). 
(*
Definition bs_app: (ListS S) -> N -> (List S) := (bs_iter (List S) (empty S) app). 

Definition rbs_app: (ListS S)->N->(List S) := (rbs_iter (List S) (empty S) app).
*)
      Definition LIn: S -> (List S) -> Set := [a;l](LEx (List S) [v](LEx (List S) [w](Id (List S) (app (fr S v a) w) l))).

   End head_tail_append.

   Section slicing.

      Variable S:Set; n:N; v:(List S).

      Definition lskip: N -> (List S) -> (List S) := (natrec [_](List S)->(List S) [w]w [_;p;w](p (tl ? w))).
(*
Definition lfirst: N -> (List S) -> (List S) := (natrec [_](List S)->(List S) [_](empty S) [_;p;w](app ? (p (tl ? w)) (hd ? w))).  

Definition lslice: N -> N -> (List S) -> (List S) := [m;n;v](lfirst n (lskip m v)).

Definition lix: N -> (List S) -> (List S) := [n;v](hd S (lskip n v)).

Definition lixe: S -> N -> (List S) -> S := [a;n;v](hde S a (lskip n v)).

Definition llen: (List S) -> N := (listrec S [_]N zero [_;p;_](succ p)).
*)
   End slicing.

   Section arithmetic.

      Definition pred: N -> N := (tl One).

      Definition add: N -> N -> N := (app One). 

      Definition add_three: N -> N -> N -> N := (app_three One). 
(*
Definition bs_add: NS -> N -> N := (bs_app One). 

Definition rbs_add:NS->N->N := (rbs_app One).
*)
      Definition sub: N -> N -> N := [m;n](lskip One n m).
(*      
Definition sub_t: N -> N -> N -> N := [m,n](sub (sub m n)).

Definition absv: N -> N -> N := [m;n](plus (minus m n) (minus n m)).
*)
   End arithmetic.

End Arith_Functions.

Section Arith_Hints.

   Section arith_fold.
(*
Theorem bs_app_fold: (n:N; S:Set; ls:(ListS S); P:(List S)->Set) (P (bs_app S ls n)) -> (P (bs_iter (List S) (empty S) (app S) ls n)).
Intros.
Assumption.
Qed.
*)
      Theorem pred_fold: (n:N; P:N->Set) (P (pred n)) -> (P (tl One n)).
      Intros.
      Assumption.
      Qed.
(*
Theorem add_fold: (m,n:N; P:N->Set) (P (add m n)) -> (P (app One m n)).
Intros.
Apply (id_repl N (app One m n) (add m n)).
Apply id_r.
Assumption.
Qed.

Theorem bs_add_fold: (n:N; ns:NS; P:N->Set) (P (bs_add ns n)) -> (P (bs_app One ns n)).
Intros.
Assumption.
Qed.
*)
   End arith_fold.
   
End Arith_Hints.

Section Arith_Results.

   Section head_tail_results.

      Theorem fr_ini1: (S:Set; a,b:S; v,w:(List S)) (Id (List S) (fr S v a) (fr S w b)) -> (Id (List S) v w).
      Intros.
      MApply '(id_repl (List S) v (tl S (fr S v a))).
      MApply '(id_repl (List S) w (tl S (fr S w b))).
      MApply '(id_comp (List S)).
      Qed.

      Theorem fr_ini2: (S:Set; v,w:(List S); a,b:S) (Id (List S) (fr S v a) (fr S w b)) -> (Id S a b).
      Intros.
      MApply '(id_repl S a (hde S a (fr S v a))).
      MApply '(id_repl S b (hde S a (fr S w b))).
      MApply '(id_comp (List S)).
      Qed.
(*
Theorem hd_hde_id: (S:Set; a:S; v:(List S)) (GT (llen S v) zero) -> (Id (List S) (hd S v) (fr S (empty S) (hde S a v))).
Intros S a v.
MElim 'v 'listrec.
MApply '(gt_false zero).
Qed.

Theorem tl_len: (S:Set; v:(List S)) (Id N (llen S (tl S v)) (pred (llen S v))).
Intros.
MElim 'v 'listrec.
Qed.
*)   
      Theorem app_empty: (S:Set; v:(List S)) (Id (List S) (app S (empty S) v) v). 
      Intros.
      MElim 'v 'listrec.
      MApply '(id_comp (List S) (List S) [v:?](fr S v s)).
      Qed.
(*
Theorem app_ass: (S:Set; u,v,w:(List S)) (Id (List S) (app S (app S u v) w) (app S u (app S v w))).
Intros.
MElim 'w 'listrec.
MApply '(id_comp (List S) (List S) [v:?](fr S v y)).
Qed.
*)
      Theorem lin_i: (S:Set; v,w,l:(List S); a:S) (Id (List S) (app S (fr S v a) w) l) -> (LIn S a l).
      Intros.
      Unfold LIn.
      MApply '(lex_i (List S) v).
      MApply '(lex_i (List S) w).
      Qed.

      Theorem lin_e: (S:Set; a:S; l:(List S); P:Set) (LIn S a l) -> ((v,w:(List S)) (Id (List S) (app S (fr S v a) w) l) -> P) -> P.
      Intros.
      MElim 'H 'lex_e.
      MElim 'y 'lex_e.
      MApply '(H0 a0 a1).
      Qed.

      Theorem lin_fr_i: (S:Set; a,b:S; l:(List S)) (LOr (LIn S a l) (Id S a b)) -> (LIn S a (fr S l b)).
      Intros.
      MElim 'H '(when (LIn S a l) (Id S a b)).
      MApply '(lin_e S a l).
      MApply '(id_repl (List S) l (app S (fr S v a) w)).
      MApply '(lin_i S v (fr S w b)).
      MApply '(id_repl S b a).
      MApply '(lin_i S l (empty S)).
      Qed.

   End head_tail_results.
(*
Section slicing_results. 

Theorem lskip_empty: (S:Set; n:N) (Id (List S) (lskip S n (empty S)) (empty S)).
Intros.
MElim 'n 'natrec.
Qed.

Theorem lskip_tl: (S:Set; n:N; v:(List S)) (Id (List S) (lskip S n (tl S v)) (tl S (lskip S n v))).
Intros S n.
MElim 'n 'natrec.
MElim 'v 'listrec.
(MApply '(id_repl ? (lskip S n0 (empty S)) (empty S)); MApply 'id_comm).
MApply 'lskip_empty.
MApply '(H l).
Qed.

Theorem lixe_empty: (n:N; S:Set; a:S) (Id S (lixe S a n (empty S)) a).
Intros.
MElim 'n 'natrec.
Qed.

Theorem lixe_app_v: (S:Set; a,b:S; w,v:(List S); n:N) (GT (llen S v) n) -> (Id S (lixe S a n (app S w v)) (lixe S b n v)).
Intros S a b w v.
(Elim v using listrec; MSimpl).
Intros.
MApply '(gt_false n).
Intros l H y n.
MElim 'n 'natrec.
(Unfold lixe; Simpl).
Fold (lixe S a n0 (app S w l)) (lixe S b n0 l). (**)
MApply '(H n0).
Qed.

Theorem lixe_le: (S:Set; a:S; v:(List S); n:N) (LE (llen S v) n) -> (Id S (lixe S a n v) a).
Intros S a v.
(Elim v using listrec; Simpl).
Intros n.
MElim 'n 'natrec.
MApply 'lixe_empty.
Intros l H y n. 
MElim 'n 'natrec.
MApply '(le_false (succ (llen S l))). 
(Unfold lixe; Simpl).
Fold (lixe S a n0 l). (**)
MApply '(H n0).
Qed.

Theorem lslice_lix: (S:Set; k:N; v:(List S)) (Id (List S) (lslice S k one v) (lix S k v)).
Intros.
Unfold lslice lfirst.
MSimpl.
MApply 'app_empty.
Qed.

End slicing_results.
*)
   Section arithmetics_results.

      Theorem succ_ini: (m,n:N) (Id N (succ m) (succ n)) -> (Id N m n).
      Intros.
      MApply '(fr_ini1 One tt tt).
      Qed.

      Theorem sub_succ: (m,n:N) (LE m n) -> 
                        (Id N (sub (succ n) m) (succ (sub n m))).
      Intros m.
      Elim m using natrec.
      Intros.
      MSimpl.
      Intros m' H n.
      MElim 'n 'natrec.
      MApply '(le_false m').
      MApply '(H n0).
      Qed.
(*
Theorem succ_pred: (n:N) (GT n zero) -> (Id N (succ (pred n)) n).
Intros n.
MElim 'n 'natrec.
MApply '(gt_false zero).
Qed.
*) 
      Theorem add_zero: (n:N) (Id N (add zero n) n).
      Intros.
      Unfold N add zero.
      MApply 'app_empty.
      Qed.
(*
Theorem add_ass: (l,m,n:N) (Id N (add (add l m) n) (add l (add m n))).
Intros.
Unfold N add.
MApply 'app_ass.
Qed.
*)   
      Theorem add_succ: (m,n:N) (Id N (add (succ m) n) (succ (add m n))).
      Intros.
      (MElim 'n 'natrec; Apply succ_fold). (**)
      MApply '(id_comp N).
      Qed.

      Theorem add_comm: (m,n:N) (Id N (add m n) (add n m)).
      Intros m.
      MElim 'm 'natrec.
      MApply 'add_zero.
      MApply '(id_trans ? (succ (add n n0))).
      MApply 'add_succ. 
      Apply succ_fold. (**)
      MApply '(id_comp N).
      MApply '(H n0).
      Qed.
(*
Theorem add_pred: (n,m:N) (GT n zero) -> (Id N (succ (add (pred n) m)) (add n m)).
Intros n m.
MElim 'm 'natrec.
MApply 'succ_pred. 
(Apply succ_fold; Apply succ_fold). (**)
MApply '(id_comp N).
MApply 'H.
Qed.
*)
      Theorem le_comp_pred: (m,n:N) (LE m n) -> (LE (pred m) (pred n)). 
      Intros m.
      Elim m using natrec.
      Intros.
      MApply 'le_wf.
      Intros m' H n.
      MElim 'n 'natrec.
      MApply '(le_false m').
      Qed.

      Theorem le_add: (m,n:N) (LE m (add m n)).
      Intros.
      MElim 'n 'natrec.
      MApply 'le_r.
      MApply '(le_trans (add m n0)).
      Apply succ_fold. (**)
      MApply 'le_succ.
      Qed.
      
      Theorem le_comp_add: (m1,m2,n:N) (LE m1 m2) -> (LE (add m1 n) (add m2 n)).
      Intros m1 m2 n.
      MElim 'n 'natrec.
      (Apply succ_fold; Apply succ_fold). (**)
      MApply 'le_comp_succ.
      MApply 'H.
      Qed.

      Theorem le_comp_add2: (m,n1,n2:N) (LE n1 n2) -> (LE (add m n1) (add m n2)).
      Intros.
      MApply '(id_repl N (add m n1) (add n1 m)).
      MApply 'add_comm.
      MApply '(id_repl N (add m n2) (add n2 m)).
      MApply 'add_comm.
      MApply 'le_comp_add.
      Qed.

      Theorem gt_comp_add2: (m,n1,n2:N) (GT n1 n2) -> (GT (add m n1) (add m n2)).
      Intros.
      MApply 'le_gt.
      MApply '(id_repl N (succ (add m n2)) (add m (succ n2))).
      MApply 'le_comp_add2.
      MApply 'gt_le.
      Qed.

      Theorem le_comp_sub: (n,m1,m2:N) (LE m1 m2) -> (LE (sub m1 n) (sub m2 n)).
      Intros n.
      MElim 'n 'natrec.
      MApply '(H (pred m1) (pred m2)).
      MApply 'le_comp_pred.
      Qed.
      
      Theorem gt_comp_sub: (m1,m2,n:N) (LE n m2) -> (GT m1 m2) -> (GT (sub m1 n) (sub m2 n)).
      Intros.
      MApply 'le_gt.
      MApply '(id_repl N (succ (sub m2 n)) (sub (succ m2) n)).
      MApply 'sub_succ.
      MApply 'le_comp_sub.
      MApply gt_le.
      Qed.
(*
Theorem le_zero_add: (m,n:N) (LE (add n m) zero) -> (Id N n zero).
Intros.
MApply 'le_zero.
MApply '(le_trans (add n m)).
MApply 'le_add.
Qed.

Theorem sub_pred_l: (n,m:N) (Id N (sub (pred m) n) (pred (sub m n))).
Intros.
Unfold N sub pred.
MApply 'lskip_tl.
Qed.
*)
      Theorem sub_zero: (n,m:N) (LE m n) -> (Id N (sub m n) zero).
      Intros n.
      Elim n using natrec.
      Intros.
      MSimpl.
      MApply 'le_zero.
      Intros n' H m.
      Elim m using natrec.
      Intros.
      MSimpl.
      MApply '(H zero).
      Intros m' H1 H2.
      MSimpl.
      MApply '(H m').
      Qed.

      Theorem succ_pred_e: (m,n:N) (Id N m (succ n)) -> (Id N (pred m) n).
      Intros m.
      Elim m using natrec.
      Intros.
      MApply '(n_false n).
      Intros m' H n H2.
      MSimpl.
      MApply 'succ_ini.
      Qed.

      Theorem add_sub_e: (n,m2,m1:N) (Id N m1 (add m2 n)) -> (Id N (sub m1 m2) n).
      Intros n.
      Elim n using natrec.
      MSimpl.
      Intros.
      MApply 'sub_zero.
      MApply '(id_repl N m2 m1).
      MApply 'le_r.
      Intros n' H m2.
      Elim m2 using natrec.
      Intros.
      MSimpl.
      MApply '(id_repl N (succ n') (add zero (succ n'))).
      MApply 'add_zero.
      Intros m2' H1 m1 H2.
      MSimpl.
      MApply 'pred_fold. (**)
      MApply '(H1 (pred m1)).
      Simpl in H2.
      Fold (succ (add (succ m2') n')) in H2. (**)
      MApply '(id_repl N (add m2' (succ n')) (add (succ m2') n')).
      MApply '(add_succ m2' n').
      MApply 'succ_pred_e.
      Qed.

      Theorem sub_add: (m,n:N) (Id N (sub (add m n) n) m).
      Intros.
      MApply 'add_sub_e.
      MApply 'add_comm.
      Qed.

      Theorem gt_add_di: (a,m,n:N) (GT (add m n) a) -> 
                         (LOr (GT m a) (GT n (sub a m))).
      Intros.
      MApply '(lor_e (LE m a) (GT m a)).
      MCut '(GT n (sub a m)).
      MApply '(id_repl N n (sub (add n m) m)).
      MApply 'sub_add.
      MApply 'gt_comp_sub.
      MApply '(id_repl N (add n m) (add m n)).
      MApply 'add_comm.
      MApply 'in_r.
      MApply 'in_l.
      MApply 'le_di.
      Qed.
(*
Theorem app_llen: (S:Set; w,v:(List S)) (Id N (llen S (app S w v)) (add (llen S w) (llen S v))).
Intros.
MElim 'v 'listrec.
Apply succ_fold. (**)
MApply '(id_comp N).
Qed.

Theorem bsapp_llen: (S:Set; vs:N->(List S); n:N) (Id N (llen S (bs_app S vs n)) (bs_add [n](llen S (vs n)) n)).
Intros.
MElim 'n 'natrec.
MApply '(id_repl ? (bs_add [n:N](llen S (vs n)) n0) (llen S (bs_app S vs n0))).
MApply 'app_llen.
Qed.

Theorem rbsapp_llen: (S:Set; vs:N->(List S); n:N) (Id N (llen S (rbs_app S vs n)) (rbs_add [n](llen S (vs n)) n)).
Intros.
Unfold rbs_add rbs_app rbs_iter.
Apply bs_app_fold. 
Apply bs_app_fold.
Apply bs_add_fold. (**)
MApply 'bsapp_llen.
Qed.

Theorem lskip_llen: (S:Set; v:(List S); n:N) (Id N (llen S (lskip S n v)) (sub (llen S v) n)).
Intros.
MElim 'n 'natrec.
Fold (pred (llen S v)). (**)
MApply '(id_trans ? (pred (llen S (lskip S n0 v)))).
MApply '(id_repl ? (lskip S n0 (tl S v)) (tl S (lskip S n0 v))). 
(MApply 'id_comm; MApply 'lskip_tl).
MApply 'tl_len.
MApply '(id_trans ? (pred (sub (llen S v) n0))).
MApply '(id_comp N).
(MApply 'id_comm; MApply 'sub_pred_l).
Qed.
   
Theorem lskip_le: (S:Set; v:(List S); n:N) (LE (llen S v) n) -> (Id N (llen S (lskip S n v)) zero).
Intros.
MApply '(id_trans ? (sub (llen S v) n)).
MApply 'lskip_llen.
MApply 'sub_zero.
Qed.

Theorem lslice_succ_r: (S:Set; v:(List S); k,n:N) (Id (List S) (lslice S k (succ n) v) (app S (lslice S (succ k) n v) (lix S k v))).
Intros.
(Unfold lslice lix; MSimpl).
MApply '(id_repl ? (tl S (lskip S k v)) (lskip S k (tl S v))).
MApply 'lskip_tl.
Qed.

Theorem lslice_succ_l: (S:Set; v:(List S); n,k:N) (Id (List S) (lslice S k (succ n) v) (app S (lix S (add k n) v) (lslice S k n v))).
Intros S v n.
MElim 'n 'natrec.
MApply 'lslice_lix.
MApply '(id_repl ? (succ (add k n0)) (add (succ k) n0)).
MApply 'add_succ.
MApply '(id_repl ? (lslice S k (succ n0) v) (app S (lslice S (succ k) n0 v) (lix S k v))).
(MApply 'id_comm; MApply 'lslice_succ_r).
MApply '(id_repl ? (lslice S k (succ (succ n0)) v) (app S (lslice S (succ k) (succ n0) v) (lix S k v))).
(MApply 'id_comm; MApply 'lslice_succ_r).
MApply '(id_trans (List S) (app S (app S (lix S (add (succ k) n0) v) (lslice S (succ k) n0 v)) (lix S k v))).
MApply '(id_comp (List S) (List S) [u:?](app S u (lix S k v))).
MApply '(H (succ k)).
Apply succ_fold. (**)
MApply '(id_repl N (succ (add k n0)) (add (succ k) n0)).
MApply 'add_succ.
MApply 'app_ass.
Qed.

Theorem lslice_add: (S:Set; v:(List S); k,m,n:N) (Id (List S) (lslice S k (add m n) v) (app S (lslice S (add k m) n v) (lslice S k m v))).
Intros.
MElim 'n 'natrec.
MApply '(id_repl ? (lslice S (add k m) zero v) (empty S)).
(MApply 'id_comm; MApply 'app_empty).
MApply '(id_trans ? (app S (lix S (add k (add m n0)) v) (lslice S k (add m n0) v))).
Apply succ_fold. (**)
MApply 'lslice_succ_l.
MApply '(id_repl ? (lslice S (add k m) (succ n0) v) (app S (lix S (add (add k m) n0) v) (lslice S (add k m) n0 v))).
(MApply 'id_comm; MApply 'lslice_succ_l).
MApply '(id_trans ? (app S (lix S (add (add k m) n0) v) (app S (lslice S (add k m) n0 v) (lslice S k m v)))).
MApply '(id_repl ? (add k (add m n0)) (add (add k m) n0)).
MApply 'add_ass.
MApply '(id_comp (List S) (List S) [w](app S (lix S (add (add k m) n0) v) w)).
(MApply 'id_comm; MApply 'app_ass).
Qed.
   
Theorem lslice_bsadd: (S:Set; v:(List S); k:N; ms:NS; n:N) (Id (List S) (lslice S k (bs_add ms n) v) (bs_app S [m](lslice S (add k (bs_add ms m)) (ms m) v) n)).
Intros.
(MElim 'n 'natrec; Fold (add (ms n0) (bs_add ms n0))).
MApply '(id_repl ? (bs_app S [m:N](lslice S (add k (bs_add ms m)) (ms m) v) n0) (lslice S k (bs_add ms n0) v)).
MApply '(id_repl ? (add (ms n0) (bs_add ms n0)) (add (bs_add ms n0) (ms n0))).
MApply 'add_comm.   
MApply 'lslice_add.
Qed.
   
Theorem lslice_rbsadd: (S:Set; v:(List S); k:N; ms:NS; n:N) (Id (List S) (lslice S k (rbs_add ms n) v) (rbs_app S [m](lslice S (add k (bs_add ms m)) (ms m) v) n)).
Intros.
Unfold rbs_add rbs_app rbs_iter.
Apply bs_app_fold. 
Apply bs_app_fold.
Apply bs_add_fold. (**)
MApply 'lslice_bsadd.
Qed.
*)   
End arithmetics_results.

End Arith_Results.