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