-include "basics/list.ma".
+include "basics/list2.ma".
include "basics/types.ma".
include "arithmetics/nat.ma".
-include "utilities/pair.ma".
-include "ASM/JMCoercions.ma".
+include "Cerco/utilities/pair.ma".
+include "Cerco/ASM/JMCoercions.ma".
(* let's implement a daemon not used by automation *)
inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX.
-axiom IMPOSSIBLE: K1DAEMONXXX = K2DAEMONXXX.
-example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
-example not_implemented: False. cases daemon qed.
+axiom IMPOSSIBLE: \ 5a href="cic:/matita/Cerco/ASM/Utils/DAEMONXXX.con(0,1,0)"\ 6K1DAEMONXXX\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/Cerco/ASM/Utils/DAEMONXXX.con(0,2,0)"\ 6K2DAEMONXXX\ 5/a\ 6.
+example daemon: \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6. generalize in match \ 5a href="cic:/matita/Cerco/ASM/Utils/IMPOSSIBLE.dec"\ 6IMPOSSIBLE\ 5/a\ 6; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
+example not_implemented: \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6. cases \ 5a href="cic:/matita/Cerco/ASM/Utils/daemon.def(2)" title="null"\ 6daemon\ 5/a\ 6 qed.
notation "⊥" with precedence 90
for @{ match ? in False with [ ] }.
definition ltb ≝
- λm, n: nat.
- leb (S m) n.
+ λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) n.
definition geb ≝
- λm, n: nat.
- ltb n m.
+ λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"\ 6ltb\ 5/a\ 6 n m.
definition gtb ≝
- λm, n: nat.
- ltb n m.
+ λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"\ 6ltb\ 5/a\ 6 n m.
(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
-let rec eq_nat (n: nat) (m: nat) on n: bool ≝
+let rec eq_nat (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) on n: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
match n with
- [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
- | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
+ [ O ⇒ match m with [ O ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ]
+ | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ]
].
let rec forall
- (A: Type[0]) (f: A → bool) (l: list A)
+ (A: Type[0]) (f: A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A)
on l ≝
match l with
- [ nil ⇒ true
- | cons hd tl ⇒ f hd ∧ forall A f tl
+ [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
+ | cons hd tl ⇒ f hd \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 forall A f tl
].
let rec prefix
- (A: Type[0]) (k: nat) (l: list A)
+ (A: Type[0]) (k: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A)
on l ≝
match l with
- [ nil ⇒ [ ]
+ [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
| cons hd tl ⇒
match k with
- [ O ⇒ [ ]
- | S k' ⇒ hd :: prefix A k' tl
+ [ O ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
+ | S k' ⇒ hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: prefix A k' tl
]
].
-
+
let rec fold_left2
(A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A)
- (left: list B) (right: list C) (proof: |left| = |right|)
+ (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 C) (proof: \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6left| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6right|)
on left: A ≝
- match left return λx. |x| = |right| → A with
+ match left return λx. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6right| → A with
[ nil ⇒ λnil_prf.
- match right return λx. |[ ]| = |x| → A with
+ match right return λx. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → A with
[ nil ⇒ λnil_nil_prf. accu
| cons hd tl ⇒ λcons_nil_absrd. ?
] nil_prf
| cons hd tl ⇒ λcons_prf.
- match right return λx. |hd::tl| = |x| → A with
+ match right return λx. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6hd\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → A with
[ nil ⇒ λcons_nil_absrd. ?
| cons hd' tl' ⇒ λcons_cons_prf.
fold_left2 … f (f accu hd hd') tl tl' ?
| 2: normalize in cons_nil_absrd;
destruct(cons_nil_absrd)
| 3: normalize in cons_cons_prf;
- @injective_S
+ @\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6
assumption
]
-qed.
+qed.
let rec remove_n_first_internal
- (i: nat) (A: Type[0]) (l: list A) (n: nat)
+ (i: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (A: Type[0]) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6)
on l ≝
match l with
- [ nil ⇒ [ ]
+ [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
| cons hd tl ⇒
- match eq_nat i n with
+ match \ 5a href="cic:/matita/Cerco/ASM/Utils/eq_nat.fix(0,0,1)"\ 6eq_nat\ 5/a\ 6 i n with
[ true ⇒ l
- | _ ⇒ remove_n_first_internal (S i) A tl n
+ | _ ⇒ remove_n_first_internal (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) A tl n
]
].
definition remove_n_first ≝
λA: Type[0].
- λn: nat.
- λl: list A.
- remove_n_first_internal 0 A l n.
+ λn: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/remove_n_first_internal.fix(0,2,2)"\ 6remove_n_first_internal\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 A l n.
let rec foldi_from_until_internal
- (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A)
+ (A: Type[0]) (i: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (res: ?) (rem: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → A → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A)
on rem ≝
match rem with
[ nil ⇒ res
| cons e tl ⇒
- match geb i m with
+ match \ 5a href="cic:/matita/Cerco/ASM/Utils/geb.def(3)"\ 6geb\ 5/a\ 6 i m with
[ true ⇒ res
- | _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f
+ | _ ⇒ foldi_from_until_internal A (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) (f i res e) tl m f
]
].
definition foldi_from_until ≝
- λA: Type[0].
- λn: nat.
- λm: nat.
- λf: ?.
- λa: ?.
- λl: ?.
- foldi_from_until_internal A 0 a (remove_n_first A n l) m f.
+ λA,n,m,f,a,l. \ 5a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until_internal.fix(0,3,4)"\ 6foldi_from_until_internal\ 5/a\ 6 A \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 a (\ 5a href="cic:/matita/Cerco/ASM/Utils/remove_n_first.def(3)"\ 6remove_n_first\ 5/a\ 6 A n l) m f.
definition foldi_from ≝
λA: Type[0].
λf.
λa.
λl.
- foldi_from_until A n (|l|) f a l.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"\ 6foldi_from_until\ 5/a\ 6 A n (\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|) f a l.
definition foldi_until ≝
λA: Type[0].
λf.
λa.
λl.
- foldi_from_until A 0 m f a l.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"\ 6foldi_from_until\ 5/a\ 6 A \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 m f a l.
definition foldi ≝
λA: Type[0].
λf.
λa.
λl.
- foldi_from_until A 0 (|l|) f a l.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/foldi_from_until.def(5)"\ 6foldi_from_until\ 5/a\ 6 A \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 (\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|) f a l.
definition hd_safe ≝
λA: Type[0].
- λl: list A.
- λproof: 0 < |l|.
- match l return λx. 0 < |x| → A with
+ λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+ λproof: \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|.
+ match l return λx. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → A with
[ nil ⇒ λnil_absrd. ?
| cons hd tl ⇒ λcons_prf. hd
] proof.
normalize in nil_absrd;
- cases(not_le_Sn_O 0)
+ cases(\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6)
#HYP
cases(HYP nil_absrd)
qed.
definition tail_safe ≝
λA: Type[0].
- λl: list A.
- λproof: 0 < |l|.
- match l return λx. 0 < |x| → list A with
+ λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+ λproof: \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|.
+ match l return λx. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A with
[ nil ⇒ λnil_absrd. ?
| cons hd tl ⇒ λcons_prf. tl
] proof.
normalize in nil_absrd;
- cases(not_le_Sn_O 0)
+ cases(\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6)
#HYP
cases(HYP nil_absrd)
qed.
let rec split
- (A: Type[0]) (l: list A) (index: nat) (proof: index ≤ |l|)
+ (A: Type[0]) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (index: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (proof: index \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l|)
on index ≝
- match index return λx. x ≤ |l| → (list A) × (list A) with
- [ O ⇒ λzero_prf. 〈[], l〉
+ match index return λx. x \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6l| → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) with
+ [ O ⇒ λzero_prf. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6], l〉
| S index' ⇒ λsucc_prf.
- match l return λx. S index' ≤ |x| → (list A) × (list A) with
+ match l return λx. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 index' \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6x| → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) with
[ nil ⇒ λnil_absrd. ?
| cons hd tl ⇒ λcons_prf.
let 〈l1, l2〉 ≝ split A tl index' ? in
- 〈hd :: l1, l2〉
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: l1, l2〉
] succ_prf
] proof.
[1: normalize in nil_absrd;
- cases(not_le_Sn_O index')
+ cases(\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 index')
#HYP
cases(HYP nil_absrd)
|2: normalize in cons_prf;
- @le_S_S_to_le
+ @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6
assumption
]
qed.
let rec nth_safe
- (elt_type: Type[0]) (index: nat) (the_list: list elt_type)
- (proof: index < | the_list |)
+ (elt_type: Type[0]) (index: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (the_list: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 elt_type)
+ (proof: index \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 the_list |)
on index ≝
- match index return λs. s < | the_list | → elt_type with
+ match index return λs. s \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 the_list | → elt_type with
[ O ⇒
- match the_list return λt. 0 < | t | → elt_type with
+ match the_list return λt. \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 t | → elt_type with
[ nil ⇒ λnil_absurd. ?
| cons hd tl ⇒ λcons_proof. hd
]
| S index' ⇒
- match the_list return λt. S index' < | t | → elt_type with
+ match the_list return λt. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 index' \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 t | → elt_type with
[ nil ⇒ λnil_absurd. ?
| cons hd tl ⇒
λcons_proof. nth_safe elt_type index' tl ?
]
] proof.
[ normalize in nil_absurd;
- cases (not_le_Sn_O 0)
+ cases (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6)
#ABSURD
elim (ABSURD nil_absurd)
| normalize in nil_absurd;
- cases (not_le_Sn_O (S index'))
+ cases (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 index'))
#ABSURD
elim (ABSURD nil_absurd)
| normalize in cons_proof
- @le_S_S_to_le
+ @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6
assumption
]
qed.
definition last_safe ≝
λelt_type: Type[0].
- λthe_list: list elt_type.
- λproof : 0 < | the_list |.
- nth_safe elt_type (|the_list| - 1) the_list ?.
- normalize /2/
-qed.
+ λthe_list: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 elt_type.
+ λproof : \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 the_list |.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/nth_safe.fix(0,1,6)"\ 6nth_safe\ 5/a\ 6 elt_type (\ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6the_list| \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) the_list ?.
+ normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/lt_plus_to_minus.def(12)"\ 6lt_plus_to_minus\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
let rec reduce
- (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝
+ (A: Type[0]) (B: Type[0]) (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on left ≝
match left with
- [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
+ [ nil ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ], \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]〉, \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ], right〉〉
| cons hd tl ⇒
match right with
- [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
+ [ nil ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ], left〉, \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ], \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]〉〉
| cons hd' tl' ⇒
let 〈cleft, cright〉 ≝ reduce A B tl tl' in
let 〈commonl, restl〉 ≝ cleft in
let 〈commonr, restr〉 ≝ cright in
- 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: commonl, restl〉, \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd' \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: commonr, restr〉〉
]
].
Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
*)
+(*
let rec reduce_strong
(A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)| ≝
>p2 >p3 >p4 normalize in ⊢ (% → ?)
#HYP //
]
-qed.
+qed.*)
let rec map2_opt
(A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
- (left: list A) (right: list B) on left ≝
+ (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on left ≝
match left with
[ nil ⇒
match right with
- [ nil ⇒ Some ? (nil C)
- | _ ⇒ None ?
+ [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 C)
+ | _ ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
]
| cons hd tl ⇒
match right with
- [ nil ⇒ None ?
+ [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
| cons hd' tl' ⇒
match map2_opt A B C f tl tl' with
- [ None ⇒ None ?
- | Some tail ⇒ Some ? (f hd hd' :: tail)
+ [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
+ | Some tail ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (f hd hd' \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: tail)
]
]
].
let rec map2
(A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
- (left: list A) (right: list B) (proof: | left | = | right |) on left ≝
- match left return λx. | x | = | right | → list C with
+ (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) (proof: \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 left | \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 right |) on left ≝
+ match left return λx. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 x | \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 right | → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 C with
[ nil ⇒
- match right return λy. | [] | = | y | → list C with
- [ nil ⇒ λnil_prf. nil C
+ match right return λy. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 y | → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 C with
+ [ nil ⇒ λnil_prf. \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 C
| _ ⇒ λcons_absrd. ?
]
| cons hd tl ⇒
- match right return λy. | hd::tl | = | y | → list C with
+ match right return λy. \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 hd\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl | \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="norm" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 y | → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 C with
[ nil ⇒ λnil_absrd. ?
- | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ?
+ | cons hd' tl' ⇒ λcons_prf. (f hd hd') \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: map2 A B C f tl tl' ?
]
] proof.
[1: normalize in cons_absrd;
assumption
]
qed.
-
-let rec map3
- (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D)
- (left: list A) (centre: list B) (right: list C)
- (prflc: |left| = |centre|) (prfcr: |centre| = |right|) on left ≝
- match left return λx. |x| = |centre| → list D with
- [ nil ⇒ λnil_prf.
- match centre return λx. |x| = |right| → list D with
- [ nil ⇒ λnil_nil_prf.
- match right return λx. |nil ?| = |x| → list D with
- [ nil ⇒ λnil_nil_nil_prf. nil D
- | cons hd tl ⇒ λcons_nil_nil_absrd. ?
- ] nil_nil_prf
- | cons hd tl ⇒ λnil_cons_absrd. ?
- ] prfcr
- | cons hd tl ⇒ λcons_prf.
- match centre return λx. |x| = |right| → list D with
- [ nil ⇒ λcons_nil_absrd. ?
- | cons hd' tl' ⇒ λcons_cons_prf.
- match right return λx. |right| = |x| → |cons ? hd' tl'| = |x| → list D with
- [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ?
- | cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf.
- (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?)
- ] (refl ? (|right|)) cons_cons_prf
- ] prfcr
- ] prflc.
- [ 1: normalize in cons_nil_nil_absrd;
- destruct(cons_nil_nil_absrd)
- | 2: generalize in match nil_cons_absrd;
- \ 5prfcr\ 6\ 5nil_prf #hyp="" normalize="" hyp;="" destruct(hyp)="" |="" 3:="" generalize="" in="" match="" cons_nil_absrd;=""\ 6\ 5prfcr\ 6\ 5cons_prf #hyp="" hyp;="" destruct(hyp)="" 4:="" cons_cons_nil_absrd;="" destruct(cons_cons_nil_absrd)="" 5:="" normalize="" destruct(cons_cons_cons_prf)="" assumption="" |="" 6:="" generalize="" in="" match="" cons_cons_cons_prf;=""\ 6\ 5refl_prf\ 6\ 5prfcr\ 6\ 5cons_prf #hyp="" normalize="" hyp;="" destruct(hyp)="" @sym_eq="" assumption="" ]="" lemma="" eq_rect_type0_r="" :="" ∀a:="" ∀a:a.="" ∀p:="" ∀x:a.="" eq="" type[0].="" (refl="" a="" →="" ∀x:="" a.∀p:eq="" ?="" a.="" x="" p.="" #a="" #h="" #x="" #p="" h="" generalize="" in="" match="" cases="" p="" qed.="" let="" rec="" safe_nth="" (a:="" type[0])="" (n:="" nat)="" (l:="" list="" a)="" (p:="" n=""\ 6< length A l) on n: A ≝
- match n return λo. o < length A l → A with
- [ O ⇒
- match l return λm. 0 < length A m → A with
- [ nil ⇒ λabsd1. ?
- | cons hd tl ⇒ λprf1. hd
- ]
- | S n' ⇒
- match l return λm. S n' < length A m → A with
- [ nil ⇒ λabsd2. ?
- | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
- ]
- ] ?.
- [ 1:
- @ p
- | 4:
- normalize in prf2
- normalize
- @ le_S_S_to_le
- assumption
- | 2:
- normalize in absd1;
- cases (not_le_Sn_O O)
- # H
- elim (H absd1)
- | 3:
- normalize in absd2;
- cases (not_le_Sn_O (S n'))
- # H
- elim (H absd2)
- ]
-qed.
-let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
+let rec nub_by_internal (A: Type[0]) (f: A → A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) on n ≝
match n with
[ O ⇒
match l with
- [ nil ⇒ [ ]
+ [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
| cons hd tl ⇒ l
]
| S n ⇒
match l with
- [ nil ⇒ [ ]
+ [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
| cons hd tl ⇒
- hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n
+ hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: nub_by_internal A f (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λy. \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (f y hd)) tl) n
]
].
definition nub_by ≝
λA: Type[0].
- λf: A → A → bool.
- λl: list A.
- nub_by_internal A f l (length ? l).
+ λf: A → A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+ λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/nub_by_internal.fix(0,3,3)"\ 6nub_by_internal\ 5/a\ 6 A f l (\ 5a href="cic:/matita/basics/list2/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l).
-let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝
+let rec member (A: Type[0]) (eq: A → A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (a: A) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
match l with
- [ nil ⇒ false
- | cons hd tl ⇒ orb (eq a hd) (member A eq a tl)
+ [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
+ | cons hd tl ⇒ \ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 (eq a hd) (member A eq a tl)
].
-let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝
+let rec take (A: Type[0]) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on n: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A ≝
match n with
- [ O ⇒ [ ]
+ [ O ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
| S n ⇒
match l with
- [ nil ⇒ [ ]
- | cons hd tl ⇒ hd :: take A n tl
+ [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
+ | cons hd tl ⇒ hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: take A n tl
]
].
-let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝
+let rec drop (A: Type[0]) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on n ≝
match n with
[ O ⇒ l
| S n ⇒
match l with
- [ nil ⇒ [ ]
+ [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
| cons hd tl ⇒ drop A n tl
]
].
definition list_split ≝
λA: Type[0].
- λn: nat.
- λl: list A.
- 〈take A n l, drop A n l〉.
+ λn: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/Cerco/ASM/Utils/take.fix(0,1,1)"\ 6take\ 5/a\ 6 A n l, \ 5a href="cic:/matita/Cerco/ASM/Utils/drop.fix(0,1,1)"\ 6drop\ 5/a\ 6 A n l〉.
-let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B)
- (l: list A) on l: list B ≝
+let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → A → B)
+ (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
match l with
- [ nil ⇒ nil ?
- | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl)
+ [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ?
+ | cons hd tl ⇒ (f n hd) \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: (mapi_internal A B (n \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6) f tl)
].
definition mapi ≝
λA, B: Type[0].
- λf: nat → A → B.
- λl: list A.
- mapi_internal A B 0 f l.
+ λf: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → A → B.
+ λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/mapi_internal.fix(0,4,2)"\ 6mapi_internal\ 5/a\ 6 A B \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6 f l.
let rec zip_pottier
- (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
+ (A: Type[0]) (B: Type[0]) (left: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (right: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B)
on left ≝
match left with
- [ nil ⇒ [ ]
+ [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
| cons hd tl ⇒
match right with
- [ nil ⇒ [ ]
- | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl'
+ [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
+ | cons hd' tl' ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd, hd'〉 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: zip_pottier A B tl tl'
]
].
+(*
let rec zip_safe
(A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
on left ≝
@injective_S
assumption
]
-qed.
+qed. *)
-let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
+let rec zip (A: Type[0]) (B: Type[0]) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (r: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on l: \ 5a href="cic:/matita/basics/types/option.ind(1,0,1)"\ 6option\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B)) ≝
match l with
- [ nil ⇒ Some ? (nil (A × B))
+ [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 (A \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 B))
| cons hd tl ⇒
match r with
- [ nil ⇒ None ?
+ [ nil ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
| cons hd' tl' ⇒
match zip ? ? tl tl' with
- [ None ⇒ None ?
- | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail)
+ [ None ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,1,1)"\ 6None\ 5/a\ 6 ?
+ | Some tail ⇒ \ 5a href="cic:/matita/basics/types/option.con(0,2,1)"\ 6Some\ 5/a\ 6 ? (\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6hd, hd'〉 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: tail)
]
]
].
-let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
+let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on l ≝
match l with
[ nil ⇒ a
| cons hd tl ⇒ foldl A B f (f a hd) tl
∀B: Type[0].
∀H: A → B → A.
∀acc: A.
- ∀pre: list B.
+ ∀pre: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B.
∀hd:B.
- foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd).
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H acc (pre\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6hd]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (H (\ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H acc pre) hd).
#A #B #H #acc #pre generalize in match acc; -acc; elim pre
[ normalize; //
| #hd #tl #IH #acc #X normalize; @IH ]
∀B: Type[0].
∀H: A → B → A.
∀acc: A.
- ∀suff,pre: list B.
- foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff).
+ ∀suff,pre: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B.
+ \ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H acc (pre\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6suff) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H (\ 5a href="cic:/matita/Cerco/ASM/Utils/foldl.fix(0,4,1)"\ 6foldl\ 5/a\ 6 A B H acc pre) suff).
#A #B #H #acc #suff elim suff
- [ #pre >append_nil %
- | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
+ [ #pre >\ 5a href="cic:/matita/basics/list/append_nil.def(4)"\ 6append_nil\ 5/a\ 6 %
+ | #hd #tl #IH #pre whd in ⊢ (???%) <(\ 5a href="cic:/matita/Cerco/ASM/Utils/foldl_step.def(2)"\ 6foldl_step\ 5/a\ 6 … H ??) applyS (IH (pre\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6hd])) ]
qed.
definition flatten ≝
λA: Type[0].
- λl: list (list A).
- foldr ? ? (append ?) [ ] l.
+ λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A).
+ \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 ? ? (\ 5a href="cic:/matita/basics/list/append.fix(0,1,1)"\ 6append\ 5/a\ 6 ?) \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] l.
-let rec rev (A: Type[0]) (l: list A) on l ≝
+let rec rev (A: Type[0]) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
match l with
- [ nil ⇒ nil A
- | cons hd tl ⇒ (rev A tl) @ [ hd ]
+ [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A
+ | cons hd tl ⇒ (rev A tl) \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 hd ]
].
+(*
lemma append_length:
∀A: Type[0].
∀l, r: list A.
| #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
]
]
-qed.
+qed.*)
notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
for @{ match $e with [ true ⇒ $t | false ⇒ $f] }.
let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
- (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
+ (f: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 → A → B → A) (x: A) (i: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B) on l ≝
match l with
[ nil ⇒ x
- | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
+ | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 i) tl
].
-definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
+definition fold_left_i ≝ λA,B,f,x. \ 5a href="cic:/matita/Cerco/ASM/Utils/fold_left_i_aux.fix(0,5,1)"\ 6fold_left_i_aux\ 5/a\ 6 A B f x \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
-notation "hvbox(t⌈o ↦ h⌉)"
+(* notation "hvbox(t\lceil o \mapsto h\rceil )"
with precedence 45
- for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
+ for @{ match (? : $o=$h) with [ refl \Rightarrow $t ] }. *)
definition function_apply ≝
λA, B: Type[0].
for @{ 'function_apply $f $x }.
interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
+
+notation "f break $ x"
+ left associative with precedence 99
+ for @{ 'function_apply $f $x }.
+
+interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
-let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
+let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) on n ≝
match n with
[ O ⇒ a
| S o ⇒ f (iterate A f a o)
∀A,B,C: Type[0].
∀T: A → B → C.
∀p.
- ∀P: A×B → C → Prop.
- (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
+ ∀P: A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B → C → Prop.
+ (∀lft, rgt. p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt〉 → P \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt〉 (T lft rgt)) →
P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
axiom pair_elim'':
∀T: A → B → C.
∀T': A → B → C'.
∀p.
- ∀P: A×B → C → C' → Prop.
- (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
+ ∀P: A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B → C → C' → Prop.
+ (∀lft, rgt. p \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt〉 → P \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6lft,rgt〉 (T lft rgt) (T' lft rgt)) →
P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
lemma pair_destruct_1:
- ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
- #A #B #a #b *; /2/
+ ∀A,B.∀a:A.∀b:B.∀c. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6a,b〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 c → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 c.
+ #A #B #a #b *; /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
lemma pair_destruct_2:
- ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
- #A #B #a #b *; /2/
+ ∀A,B.∀a:A.∀b:B.∀c. \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6a,b〉 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 c → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 c.
+ #A #B #a #b *; /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/trans_eq.def(4)"\ 6trans_eq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
+let rec exclusive_disjunction (b: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (c: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) on b ≝
match b with
[ true ⇒
match c with
- [ false ⇒ true
- | true ⇒ false
+ [ false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
+ | true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
]
| false ⇒
match c with
- [ false ⇒ false
- | true ⇒ true
+ [ false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
+ | true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
]
].
interpretation "Nat greater than eq" 'geq m n = (geb m n).
*)
-let rec division_aux (m: nat) (n : nat) (p: nat) ≝
- match ltb n (S p) with
- [ true ⇒ O
+let rec division_aux (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (n : \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (p: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) ≝
+ match \ 5a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"\ 6ltb\ 5/a\ 6 n (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 p) with
+ [ true ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
| false ⇒
match m with
- [ O ⇒ O
- | (S q) ⇒ S (division_aux q (n - (S p)) p)
+ [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
+ | (S q) ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (division_aux q (n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 p)) p)
]
].
definition division ≝
- λm, n: nat.
+ λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
match n with
- [ O ⇒ S m
- | S o ⇒ division_aux m m o
+ [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m
+ | S o ⇒ \ 5a href="cic:/matita/Cerco/ASM/Utils/division_aux.fix(0,0,3)"\ 6division_aux\ 5/a\ 6 m m o
].
notation "hvbox(n break ÷ m)"
interpretation "Nat division" 'division n m = (division n m).
-let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
- match leb n p with
+let rec modulus_aux (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (p: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) ≝
+ match \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 n p with
[ true ⇒ n
| false ⇒
match m with
[ O ⇒ n
- | S o ⇒ modulus_aux o (n - (S p)) p
+ | S o ⇒ modulus_aux o (n \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 p)) p
]
].
definition modulus ≝
- λm, n: nat.
+ λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
match n with
[ O ⇒ m
- | S o ⇒ modulus_aux m m o
+ | S o ⇒ \ 5a href="cic:/matita/Cerco/ASM/Utils/modulus_aux.fix(0,0,2)"\ 6modulus_aux\ 5/a\ 6 m m o
].
notation "hvbox(n break 'mod' m)"
interpretation "Nat modulus" 'modulus m n = (modulus m n).
definition divide_with_remainder ≝
- λm, n: nat.
- pair ? ? (m ÷ n) (modulus m n).
+ λm, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ \ 5a href="cic:/matita/basics/types/Prod.con(0,1,2)"\ 6pair\ 5/a\ 6 ? ? (m \ 5a title="Nat division" href="cic:/fakeuri.def(1)"\ 6÷\ 5/a\ 6 n) (\ 5a href="cic:/matita/Cerco/ASM/Utils/modulus.def(3)"\ 6modulus\ 5/a\ 6 m n).
-let rec exponential (m: nat) (n: nat) on n ≝
+let rec exponential (m: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) (n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6) on n ≝
match n with
- [ O ⇒ S O
- | S o ⇒ m * exponential m o
+ [ O ⇒ \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
+ | S o ⇒ m \ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6 exponential m o
].
interpretation "Nat exponential" 'exp n m = (exponential n m).
interpretation "sum" 'disjoint_union A B = (Sum A B).
theorem less_than_or_equal_monotone:
- ∀m, n: nat.
- m ≤ n → (S m) ≤ (S n).
+ ∀m, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m) \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 (\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n).
#m #n #H
elim H
- /2/
+ /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le.con(0,1,1)"\ 6le_n\ 5/a\ 6, \ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
theorem less_than_or_equal_b_complete:
- ∀m, n: nat.
- leb m n = false → ¬(m ≤ n).
+ ∀m, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n).
#m;
elim m;
normalize
cases z
normalize
[ #H
- /2/
- | /3/
+ /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace {}\ 5/span\ 6\ 5/span\ 6/
+ | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/not_le_to_not_le_S_S.def(5)"\ 6not_le_to_not_le_S_S\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
]
qed.
theorem less_than_or_equal_b_correct:
- ∀m, n: nat.
- leb m n = true → m ≤ n.
+ ∀m, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ \ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
#m
elim m
//
normalize
[ #H
destruct
- | #n #H lapply (H1 … H) /2/
+ | #n #H lapply (H1 … H) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_monotone.def(2)"\ 6less_than_or_equal_monotone\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.
definition less_than_or_equal_b_elim:
- ∀m, n: nat.
- ∀P: bool → Type[0].
- (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
+ ∀m, n: \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.
+ ∀P: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Type[0].
+ (m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n → P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n) → P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → P (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n).
#m #n #P #H1 #H2;
- lapply (less_than_or_equal_b_correct m n)
- lapply (less_than_or_equal_b_complete m n)
- cases (leb m n)
- /3/
+ lapply (\ 5a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_b_correct.def(3)"\ 6less_than_or_equal_b_correct\ 5/a\ 6 m n)
+ lapply (\ 5a href="cic:/matita/Cerco/ASM/Utils/less_than_or_equal_b_complete.def(6)"\ 6less_than_or_equal_b_complete\ 5/a\ 6 m n)
+ cases (\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"\ 6leb\ 5/a\ 6 m n)
+ /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace {}\ 5/span\ 6\ 5/span\ 6/
qed.
lemma inclusive_disjunction_true:
- ∀b, c: bool.
- (orb b c) = true → b = true ∨ c = true.
+ ∀b, c: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+ (\ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 c \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
# b
# c
elim b
[ normalize
# H
- @ or_introl
+ @ \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6
%
| normalize
- /2/
+ /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
]
qed.
lemma conjunction_true:
- ∀b, c: bool.
- andb b c = true → b = true ∧ c = true.
+ ∀b, c: \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+ \ 5a href="cic:/matita/basics/bool/andb.def(1)"\ 6andb\ 5/a\ 6 b c \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 c \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
# b
# c
elim b
normalize
- [ /2/
+ [ /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
| # K
destruct
]
qed.
-lemma eq_true_false: false=true → False.
+lemma eq_true_false: \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
# K
destruct
qed.
-lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
+lemma inclusive_disjunction_b_true: ∀b. \ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 b \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
# b
cases b
%
qed.
definition bool_to_Prop ≝
- λb. match b with [ true ⇒ True | false ⇒ False ].
+ λb. match b with [ true ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | false ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
-coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
-
-lemma eq_false_to_notb: ∀b. b = false → ¬ b.
- *; /2/
-qed.
+coercion bool_to_Prop: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. Prop ≝ \ 5a href="cic:/matita/Cerco/ASM/Utils/bool_to_Prop.def(1)"\ 6bool_to_Prop\ 5/a\ 6 on _b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 to Type[0].
-lemma length_append:
- ∀A.∀l1,l2:list A.
- |l1 @ l2| = |l1| + |l2|.
- #A #l1 elim l1
- [ //
- | #hd #tl #IH #l2 normalize \ 5ih ]="" qed.=""\ 6\ 5/ih\ 6\ 5/cons_prf\ 6\ 5/prfcr\ 6\ 5/refl_prf\ 6\ 5/cons_prf\ 6\ 5/prfcr\ 6\ 5/nil_prf\ 6\ 5/prfcr\ 6
\ No newline at end of file
+lemma eq_false_to_notb: ∀b. b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 b.
+ *; /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/True.con(0,1,0)"\ 6I\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
\ No newline at end of file
interpretation "nil" 'nil = (nil ?).
interpretation "cons" 'cons hd tl = (cons ? hd tl).
-definition not_nil: ∀A:Type[0].\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
- λA.λl.match l with [ nil ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 | cons hd tl ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6 ].
+definition not_nil: ∀A:Type[0].list A → Prop ≝
+ λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
theorem nil_cons:
- ∀A:Type[0].∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a:A. a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
- #A #l #a @\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq (change with (\ 5a href="cic:/matita/basics/list/not_nil.def(1)"\ 6not_nil\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))) >Heq //
+ ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
+ #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
qed.
(*
[ nil => []
| (cons hd tl) => hd :: id_list A tl ]. *)
-let rec append A (l1: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝
+let rec append A (l1: list A) l2 on l1 ≝
match l1 with
[ nil ⇒ l2
- | cons hd tl ⇒ hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: append A tl l2 ].
+ | cons hd tl ⇒ hd :: append A tl l2 ].
-definition hd ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
+definition hd ≝ λA.λl: list A.λd:A.
match l with [ nil ⇒ d | cons a _ ⇒ a].
-definition tail ≝ λA.λl: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
- match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons hd tl ⇒ tl].
+definition tail ≝ λA.λl: list A.
+ match l with [ nil ⇒ [] | cons hd tl ⇒ tl].
interpretation "append" 'append l1 l2 = (append ? l1 l2).
-theorem append_nil: ∀A.∀l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+theorem append_nil: ∀A.∀l:list A.l @ [] = l.
#A #l (elim l) normalize // qed.
theorem associative_append:
- ∀A.\ 5a href="cic:/matita/basics/relations/associative.def(1)"\ 6associative\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/append.fix(0,1,1)"\ 6append\ 5/a\ 6 A).
+ ∀A.associative (list A) (append A).
#A #l1 #l2 #l3 (elim l1) normalize // qed.
(* deleterio per auto
a :: (l1 @ l2) = (a :: l1) @ l2.
//; nqed. *)
-theorem append_cons:∀A.∀a:A.∀l,l1.l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1)\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6(l\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a])\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l1.
-/2/ qed.
+theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace trans_eq\ 5/span\ 6\ 5/span\ 6/ qed.
-theorem nil_append_elim: ∀A.∀l1,l2: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀P:?→?→Prop.
- l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 A) → P l1 l2.
+theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop.
+ l1@l2=[] → P (nil A) (nil A) → P l1 l2.
#A #l1 #l2 #P (cases l1) normalize //
#a #l3 #heq destruct
qed.
-theorem nil_to_nil: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
- l1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] → l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 l2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
-#A #l1 #l2 #isnil @(\ 5a href="cic:/matita/basics/list/nil_append_elim.def(3)"\ 6nil_append_elim\ 5/a\ 6 A l1 l2) /2/
+theorem nil_to_nil: ∀A.∀l1,l2:list A.
+ l1@l2 = [] → l1 = [] ∧ l2 = [].
+#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace conj\ 5/span\ 6\ 5/span\ 6/
qed.
(* iterators *)
-let rec map (A,B:Type[0]) (f: A → B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 B ≝
- match l with [ nil ⇒ \ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ? | cons x tl ⇒ f x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: (map A B f tl)].
+let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
+ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
-let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
definition filter ≝
- λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
- \ 5a href="cic:/matita/basics/list/foldr.fix(0,4,1)"\ 6foldr\ 5/a\ 6 T (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T) (λx,l0.\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p x) (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l0) l0) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 T).
+ λT.λp:T → bool.
+ foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
-lemma filter_true : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
- \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
+lemma filter_true : ∀A,l,a,p. p a = true →
+ filter A p (a::l) = a :: filter A p l.
#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
-lemma filter_false : ∀A,l,a,p. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 →
- \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l.
+lemma filter_false : ∀A,l,a,p. p a = false →
+ filter A p (a::l) = filter A p l.
#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
-theorem eq_map : ∀A,B,f,g,l. (∀x.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g x) → \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B f l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 A B g l.
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
#A #B #f #g #l #eqfg (elim l) normalize // qed.
(*
**************************** fold *******************************)
-let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) (f:A→B) (l:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l :B ≝
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝
match l with
[ nil ⇒ b
- | cons a l ⇒ \ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"\ 6if_then_else\ 5/a\ 6 ? (p a) (op (f a) (fold A B op b p f l))
+ | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
(fold A B op b p f l)].
notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
theorem fold_true:
-∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 →
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
- op (f a) \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
+ \fold[op,nil]_{i ∈ a::l| p i} (f i) =
+ op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
theorem fold_false:
∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
-p a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
+p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
+ \fold[op,nil]_{i ∈ l| p i} (f i).
#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
theorem fold_filter:
∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ (\ 5a href="cic:/matita/basics/list/filter.def(2)"\ 6filter\ 5/a\ 6 A p l)} (f i).
+ \fold[op,nil]_{i ∈ l| p i} (f i) =
+ \fold[op,nil]_{i ∈ (filter A p l)} (f i).
#A #B #a #l #p #op #nil #f elim l //
-#a #tl #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #pa
- [ >\ 5a href="cic:/matita/basics/list/filter_true.def(3)"\ 6filter_true\ 5/a\ 6 // > \ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_true.def(3)"\ 6fold_true\ 5/a\ 6 //
- | >\ 5a href="cic:/matita/basics/list/filter_false.def(3)"\ 6filter_false\ 5/a\ 6 // >\ 5a href="cic:/matita/basics/list/fold_false.def(3)"\ 6fold_false\ 5/a\ 6 // ]
+#a #tl #Hind cases(true_or_false (p a)) #pa
+ [ >filter_true // > fold_true // >fold_true //
+ | >filter_false // >fold_false // ]
qed.
record Aop (A:Type[0]) (nil:A) : Type[0] ≝
{op :2> A → A → A;
- nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
- nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
- assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
+ nill:∀a. op nil a = a;
+ nilr:∀a. op a nil = a;
+ assoc: ∀a,b,c.op a (op b c) = op (op a b) c
}.
-theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/basics/list/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f.
- op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈I} (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈J} (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)} (f i).
+theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
+ op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
+ \fold[op,nil]_{i∈(I@J)} (f i).
#A #B #I #J #nil #op #f (elim I) normalize
- [>\ 5a href="cic:/matita/basics/list/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/basics/list/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
-qed.
-
+ [>nill //|#a #tl #Hind <assoc //]
+qed.
\ No newline at end of file
projects / helm.git / commitdiff