--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* ********************************************************************** *)
+
+include "freescale/theory.ma".
+include "freescale/nat_lemmas.ma".
+include "freescale/option.ma".
+
+(* ************** *)
+(* Non-Empty List *)
+(* ************** *)
+
+(* lista non vuota *)
+ninductive ne_list (A:Type) : Type ≝
+ | ne_nil: A → ne_list A
+ | ne_cons: A → ne_list A → ne_list A.
+
+nlet rec ne_list_ind (A:Type) (P:ne_list A → Prop) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
+ match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_ind A P f f1 t) ].
+
+nlet rec ne_list_rec (A:Type) (P:ne_list A → Set) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
+ match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rec A P f f1 t) ].
+
+nlet rec ne_list_rect (A:Type) (P:ne_list A → Type) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
+ match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rect A P f f1 t) ].
+
+(* append *)
+nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
+ match l1 with
+ [ ne_nil hd ⇒ ne_cons A hd l2
+ | ne_cons hd tl ⇒ ne_cons A hd (ne_append A tl l2) ].
+
+notation "hvbox(hd break §§ tl)"
+ right associative with precedence 46
+ for @{'ne_cons $hd $tl}.
+
+notation "« list0 x sep ; break £ y break »"
+ non associative with precedence 90
+ for ${fold right @{'ne_nil $y } rec acc @{'ne_cons $x $acc}}.
+
+notation "hvbox(l1 break & l2)"
+ right associative with precedence 47
+ for @{'ne_append $l1 $l2 }.
+
+interpretation "ne_nil" 'ne_nil hd = (ne_nil ? hd).
+interpretation "ne_cons" 'ne_cons hd tl = (ne_cons ? hd tl).
+interpretation "ne_append" 'ne_append l1 l2 = (ne_append ? l1 l2).
+
+(* ************ *)
+(* List Utility *)
+(* ************ *)
+
+(* listlen *)
+nlet rec len_list (T:Type) (l:list T) on l ≝
+ match l with [ nil ⇒ O | cons _ t ⇒ S (len_list T t) ].
+
+nlet rec len_neList (T:Type) (nl:ne_list T) on nl ≝
+ match nl with [ ne_nil _ ⇒ 1 | ne_cons _ t ⇒ S (len_neList T t) ].
+
+(* vuota? *)
+ndefinition is_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ True | cons _ _ ⇒ False ].
+
+ndefinition isb_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ true | cons _ _ ⇒ false ].
+
+ndefinition isnot_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ False | cons _ _ ⇒ True ].
+
+ndefinition isnotb_empty_list ≝
+λT:Type.λl:list T.match l with [ nil ⇒ false | cons _ _ ⇒ true ].
+
+(* conversione *)
+nlet rec neList_to_list (T:Type) (nl:ne_list T) on nl : list T ≝
+ match nl with [ ne_nil h ⇒ [h] | ne_cons h t ⇒ [h]@(neList_to_list T t) ].
+
+nlet rec list_to_neList_aux (T:Type) (l:list T) on l : option (ne_list T) ≝
+ match l with
+ [ nil ⇒ None (ne_list T)
+ | cons h t ⇒ match list_to_neList_aux T t with
+ [ None ⇒ Some (ne_list T) «£h»
+ | Some t' ⇒ Some (ne_list T) («£h»&t') ]].
+
+ndefinition list_to_neList ≝
+λT:Type.λl:list T.
+ match l
+ return λl:list T.isnot_empty_list T l → ne_list T
+ with
+ [ nil ⇒ λp:isnot_empty_list T (nil T).False_rect ? p
+ | cons h t ⇒ λp:isnot_empty_list T (cons T h t).
+ match list_to_neList_aux T t with
+ [ None ⇒ «£h»
+ | Some t' ⇒ «£h»&t'
+ ]
+ ].
+
+(* nth elem *)
+nlet rec nth_list (T:Type) (l:list T) (n:nat) on l ≝
+ match l with
+ [ nil ⇒ None ?
+ | cons h t ⇒ match n with
+ [ O ⇒ Some ? h | S n' ⇒ nth_list T t n' ]
+ ].
+
+nlet rec nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
+ match nl with
+ [ ne_nil h ⇒ match n with
+ [ O ⇒ Some ? h | S _ ⇒ None ? ]
+ | ne_cons h t ⇒ match n with
+ [ O ⇒ Some ? h | S n' ⇒ nth_neList T t n' ]
+ ].
+
+nlet rec abs_nth_neList (T:Type) (nl:ne_list T) (n:nat) on nl ≝
+ match nl with
+ [ ne_nil h ⇒ h
+ | ne_cons h t ⇒ match n with
+ [ O ⇒ h | S n' ⇒ abs_nth_neList T t n' ]
+ ].
+
+(* reverse *)
+nlet rec reverse_list (T:Type) (l:list T) on l ≝
+ match l with
+ [ nil ⇒ nil T
+ | cons h t ⇒ (reverse_list T t)@[h]
+ ].
+
+nlet rec reverse_neList (T:Type) (nl:ne_list T) on nl ≝
+ match nl with
+ [ ne_nil h ⇒ ne_nil T h
+ | ne_cons h t ⇒ (reverse_neList T t)&(ne_nil T h)
+ ].
+
+(* getLast *)
+ndefinition get_last_list ≝
+λT:Type.λl:list T.match reverse_list T l with
+ [ nil ⇒ None ?
+ | cons h _ ⇒ Some ? h ].
+
+ndefinition get_last_neList ≝
+λT:Type.λnl:ne_list T.match reverse_neList T nl with
+ [ ne_nil h ⇒ h
+ | ne_cons h _ ⇒ h ].
+
+(* cutLast *)
+ndefinition cut_last_list ≝
+λT:Type.λl:list T.match reverse_list T l with
+ [ nil ⇒ nil T
+ | cons _ t ⇒ reverse_list T t ].
+
+ndefinition cut_last_neList ≝
+λT:Type.λnl:ne_list T.match reverse_neList T nl with
+ [ ne_nil h ⇒ ne_nil T h
+ | ne_cons _ t ⇒ reverse_neList T t ].
+
+(* getFirst *)
+ndefinition get_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ None ?
+ | cons h _ ⇒ Some ? h ].
+
+ndefinition get_first_neList ≝
+λT:Type.λnl:ne_list T.match nl with
+ [ ne_nil h ⇒ h
+ | ne_cons h _ ⇒ h ].
+
+(* cutFirst *)
+ndefinition cut_first_list ≝
+λT:Type.λl:list T.match l with
+ [ nil ⇒ nil T
+ | cons _ t ⇒ t ].
+
+ndefinition cut_first_neList ≝
+λT:Type.λnl:ne_list T.match nl with
+ [ ne_nil h ⇒ ne_nil T h
+ | ne_cons _ t ⇒ t ].
+
+(* apply f *)
+nlet rec apply_f_list (T1,T2:Type) (l:list T1) (f:T1 → T2) on l ≝
+match l with
+ [ nil ⇒ nil T2
+ | cons h t ⇒ cons T2 (f h) (apply_f_list T1 T2 t f) ].
+
+nlet rec apply_f_neList (T1,T2:Type) (nl:ne_list T1) (f:T1 → T2) on nl ≝
+match nl with
+ [ ne_nil h ⇒ ne_nil T2 (f h)
+ | ne_cons h t ⇒ ne_cons T2 (f h) (apply_f_neList T1 T2 t f) ].
+
+(* fold right *)
+nlet rec fold_right_list (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (l:list T1) on l ≝
+ match l with
+ [ nil ⇒ acc
+ | cons h t ⇒ f h (fold_right_list T1 T2 f acc t)
+ ].
+
+nlet rec fold_right_neList (T1,T2:Type) (f:T1 → T2 → T2) (acc:T2) (nl:ne_list T1) on nl ≝
+ match nl with
+ [ ne_nil h ⇒ f h acc
+ | ne_cons h t ⇒ f h (fold_right_neList T1 T2 f acc t)
+ ].
+
+(* double fold right *)
+nlemma fold_right_list2_aux1 :
+∀T.∀h,t.len_list T [] = len_list T (h::t) → False.
+ #T; #h; #t;
+ nnormalize;
+ #H;
+ napply (nat_destruct_0_S ? H).
+nqed.
+
+nlemma fold_right_list2_aux2 :
+∀T.∀h,t.len_list T (h::t) = len_list T [] → False.
+ #T; #h; #t;
+ nnormalize;
+ #H;
+ napply (nat_destruct_S_0 ? H).
+nqed.
+
+nlemma fold_right_list2_aux3 :
+∀T.∀h,h',t,t'.len_list T (h::t) = len_list T (h'::t') → len_list T t = len_list T t'.
+ #T; #h; #h'; #t; #t';
+ napply (list_ind T ??? t);
+ napply (list_ind T ??? t');
+ ##[ ##1: nnormalize; #H; napply (refl_eq ??)
+ ##| ##2: #a; #l'; #H; #H1;
+ nchange in H1:(%) with ((S O) = (S (S (len_list T l'))));
+ nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1))
+ ##| ##3: #a; #l'; #H; #H1;
+ nchange in H1:(%) with ((S (S (len_list T l'))) = (S O));
+ nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1))
+ ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
+ nchange in H2:(%) with ((S (S (len_list T l1))) = (S (S (len_list T l))));
+ nchange with ((S (len_list T l1)) = (S (len_list T l)));
+ nrewrite > (nat_destruct_S_S ?? H2);
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlet rec fold_right_list2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:list T1) on l1 ≝
+ match l1
+ return λl1.Πl2.len_list T1 l1 = len_list T1 l2 → T2
+ with
+ [ nil ⇒ λl2.match l2 return λl2.len_list T1 [] = len_list T1 l2 → T2 with
+ [ nil ⇒ λp:len_list T1 [] = len_list T1 [].acc
+ | cons h t ⇒ λp:len_list T1 [] = len_list T1 (h::t).
+ False_rect ? (fold_right_list2_aux1 T1 h t p)
+ ]
+ | cons h t ⇒ λl2.match l2 return λl2.len_list T1 (h::t) = len_list T1 l2 → T2 with
+ [ nil ⇒ λp:len_list T1 (h::t) = len_list T1 [].
+ False_rect ? (fold_right_list2_aux2 T1 h t p)
+ | cons h' t' ⇒ λp:len_list T1 (h::t) = len_list T1 (h'::t').
+ f h h' (fold_right_list2 T1 T2 f acc t t' (fold_right_list2_aux3 T1 h h' t t' p))
+ ]
+ ].
+
+nlemma fold_right_neList2_aux1 :
+∀T.∀h,h',t'.len_neList T «£h» = len_neList T (h'§§t') → False.
+ #T; #h; #h'; #t';
+ nnormalize;
+ ncases t';
+ nnormalize;
+ ##[ ##1: #x; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H))
+ ##| ##2: #x; #l; #H; nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H))
+ ##]
+nqed.
+
+nlemma fold_right_neList2_aux2 :
+∀T.∀h,h',t.len_neList T (h§§t) = len_neList T «£h'» → False.
+ #T; #h; #h'; #t;
+ nnormalize;
+ ncases t;
+ nnormalize;
+ ##[ ##1: #x; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H))
+ ##| ##2: #x; #l; #H; nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H))
+ ##]
+nqed.
+
+nlemma fold_right_neList2_aux3 :
+∀T.∀h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
+ #T; #h; #h'; #t; #t';
+ napply (ne_list_ind T ??? t);
+ napply (ne_list_ind T ??? t');
+ ##[ ##1: nnormalize; #x; #y; #H; napply (refl_eq ??)
+ ##| ##2: #a; #l'; #H; #x; #H1;
+ nchange in H1:(%) with ((S (len_neList T «£x»)) = (S (len_neList T (a§§l'))));
+ nrewrite > (nat_destruct_S_S ?? H1);
+ napply (refl_eq ??)
+ ##| ##3: #x; #a; #l'; #H; #H1;
+ nchange in H1:(%) with ((S (len_neList T (a§§l')))= (S (len_neList T «£x»)));
+ nrewrite > (nat_destruct_S_S ?? H1);
+ napply (refl_eq ??)
+ ##| ##4: #a; #l; #H; #a1; #l1; #H1; #H2;
+ nchange in H2:(%) with ((S (len_neList T (a1§§l1))) = (S (len_neList T (a§§l))));
+ nrewrite > (nat_destruct_S_S ?? H2);
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlet rec fold_right_neList2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:ne_list T1) on l1 ≝
+ match l1
+ return λl1.Πl2.len_neList T1 l1 = len_neList T1 l2 → T2
+ with
+ [ ne_nil h ⇒ λl2.match l2 return λl2.len_neList T1 «£h» = len_neList T1 l2 → T2 with
+ [ ne_nil h' ⇒ λp:len_neList T1 «£h» = len_neList T1 «£h'».
+ f h h' acc
+ | ne_cons h' t' ⇒ λp:len_neList T1 «£h» = len_neList T1 (h'§§t').
+ False_rect ? (fold_right_neList2_aux1 T1 h h' t' p)
+ ]
+ | ne_cons h t ⇒ λl2.match l2 return λl2.len_neList T1 (h§§t) = len_neList T1 l2 → T2 with
+ [ ne_nil h' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 «£h'».
+ False_rect ? (fold_right_neList2_aux2 T1 h h' t p)
+ | ne_cons h' t' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 (h'§§t').
+ f h h' (fold_right_neList2 T1 T2 f acc t t' (fold_right_neList2_aux3 T1 h h' t t' p))
+ ]
+ ].
+
+(* ******** *)
+(* naturali *)
+(* ******** *)
+
+ndefinition isZero ≝ λn:nat.match n with [ O ⇒ True | S _ ⇒ False ].
+
+ndefinition isZerob ≝ λn:nat.match n with [ O ⇒ true | S _ ⇒ false ].
+
+ndefinition ltb ≝ λn1,n2:nat.(le_nat n1 n2) ⊗ (⊖ (eq_nat n1 n2)).
+
+ndefinition geb ≝ λn1,n2:nat.(⊖ (le_nat n1 n2)) ⊕ (eq_nat n1 n2).
+
+ndefinition gtb ≝ λn1,n2:nat.⊖ (le_nat n1 n2).
projects / helm.git / blobdiff