1 include "basics/list2.ma".
2 include "basics/types.ma".
3 include "arithmetics/nat.ma".
5 include "Cerco/utilities/pair.ma".
6 include "Cerco/ASM/JMCoercions.ma".
8 (* let's implement a daemon not used by automation *)
9 inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX.
10 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.
11 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.
12 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.
14 notation "⊥" with precedence 90
15 for @{ match ? in False with [ ] }.
18 λm, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
19 \ 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.
22 λm, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
23 \ 5a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"
\ 6ltb
\ 5/a
\ 6 n m.
26 λm, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
27 \ 5a href="cic:/matita/Cerco/ASM/Utils/ltb.def(2)"
\ 6ltb
\ 5/a
\ 6 n m.
29 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
30 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 ≝
32 [ 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 ]
33 | 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 ]
37 (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)
40 [ nil ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6
41 | cons hd tl ⇒ f hd
\ 5a title="boolean and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 forall A f tl
45 (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)
48 [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
51 [ O ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
52 | S k' ⇒ hd
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6: prefix A k' tl
57 (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A)
58 (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|)
60 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
62 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
63 [ nil ⇒ λnil_nil_prf. accu
64 | cons hd tl ⇒ λcons_nil_absrd. ?
66 | cons hd tl ⇒ λcons_prf.
67 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
68 [ nil ⇒ λcons_nil_absrd. ?
69 | cons hd' tl' ⇒ λcons_cons_prf.
70 fold_left2 … f (f accu hd hd') tl tl' ?
73 [ 1: normalize in cons_nil_absrd;
74 destruct(cons_nil_absrd)
75 | 2: normalize in cons_nil_absrd;
76 destruct(cons_nil_absrd)
77 | 3: normalize in cons_cons_prf;
78 @
\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"
\ 6injective_S
\ 5/a
\ 6
83 let rec remove_n_first_internal
84 (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)
87 [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
89 match
\ 5a href="cic:/matita/Cerco/ASM/Utils/eq_nat.fix(0,0,1)"
\ 6eq_nat
\ 5/a
\ 6 i n with
91 | _ ⇒ remove_n_first_internal (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 i) A tl n
95 definition remove_n_first ≝
97 λn:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
98 λl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
99 \ 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.
101 let rec foldi_from_until_internal
102 (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)
107 match
\ 5a href="cic:/matita/Cerco/ASM/Utils/geb.def(3)"
\ 6geb
\ 5/a
\ 6 i m with
109 | _ ⇒ 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
113 definition foldi_from_until ≝
114 λ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.
116 definition foldi_from ≝
122 \ 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.
124 definition foldi_until ≝
130 \ 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.
137 \ 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.
141 λl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
142 λ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|.
143 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
144 [ nil ⇒ λnil_absrd. ?
145 | cons hd tl ⇒ λcons_prf. hd
147 normalize in nil_absrd;
148 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)
153 definition tail_safe ≝
155 λl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
156 λ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|.
157 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
158 [ nil ⇒ λnil_absrd. ?
159 | cons hd tl ⇒ λcons_prf. tl
161 normalize in nil_absrd;
162 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)
168 (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|)
170 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
171 [ 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〉
172 | S index' ⇒ λsucc_prf.
173 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
174 [ nil ⇒ λnil_absrd. ?
175 | cons hd tl ⇒ λcons_prf.
176 let 〈l1, l2〉 ≝ split A tl index' ? in
177 \ 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〉
180 [1: normalize in nil_absrd;
181 cases(
\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"
\ 6not_le_Sn_O
\ 5/a
\ 6 index')
184 |2: normalize in cons_prf;
185 @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6
191 (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)
192 (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 |)
194 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
196 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
197 [ nil ⇒ λnil_absurd. ?
198 | cons hd tl ⇒ λcons_proof. hd
201 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
202 [ nil ⇒ λnil_absurd. ?
204 λcons_proof. nth_safe elt_type index' tl ?
207 [ normalize in nil_absurd;
208 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)
210 elim (ABSURD nil_absurd)
211 | normalize in nil_absurd;
212 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'))
214 elim (ABSURD nil_absurd)
215 | normalize in cons_proof
216 @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6
221 definition last_safe ≝
223 λthe_list:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 elt_type.
224 λ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 |.
225 \ 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 ?.
226 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/
230 (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 ≝
232 [ 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〉〉
235 [ 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 ]〉〉
237 let 〈cleft, cright〉 ≝ reduce A B tl tl' in
238 let 〈commonl, restl〉 ≝ cleft in
239 let 〈commonr, restr〉 ≝ cright in
240 \ 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〉〉
249 Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
253 let rec reduce_strong
254 (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
255 on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)| ≝
257 [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
260 [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
262 let 〈cleft, cright〉 ≝ reduce_strong A B tl tl' in
263 let 〈commonl, restl〉 ≝ cleft in
264 let 〈commonr, restr〉 ≝ cright in
265 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
271 generalize in match (sig2 … (reduce_strong A B tl tl1));
272 >p2 >p3 >p4 normalize in ⊢ (% → ?)
278 (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
279 (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 ≝
283 [ 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)
284 | _ ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 ?
288 [ nil ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 ?
290 match map2_opt A B C f tl tl' with
291 [ None ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 ?
292 | 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)
298 (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
299 (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 ≝
300 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
302 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
303 [ nil ⇒ λnil_prf.
\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"
\ 6nil
\ 5/a
\ 6 C
307 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
308 [ nil ⇒ λnil_absrd. ?
309 | 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' ?
312 [1: normalize in cons_absrd;
314 |2: normalize in nil_absrd;
316 |3: normalize in cons_prf;
322 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 ≝
326 [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
331 [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
333 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
339 λf: A → A →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6.
340 λl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
341 \ 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).
343 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 ≝
345 [ nil ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6
346 | cons hd tl ⇒
\ 5a href="cic:/matita/basics/bool/orb.def(1)"
\ 6orb
\ 5/a
\ 6 (eq a hd) (member A eq a tl)
349 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 ≝
351 [ O ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
354 [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
355 | cons hd tl ⇒ hd
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6: take A n tl
359 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 ≝
364 [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
365 | cons hd tl ⇒ drop A n tl
369 definition list_split ≝
371 λn:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
372 λl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
373 \ 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〉.
375 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)
376 (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 ≝
378 [ nil ⇒
\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"
\ 6nil
\ 5/a
\ 6 ?
379 | 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)
384 λf:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → A → B.
385 λl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
386 \ 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.
389 (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)
392 [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
395 [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ]
396 | 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'
402 (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
404 match left return λx. |x| = |right| → list (A × B) with
406 match right return λx. |[ ]| = |x| → list (A × B) with
407 [ nil ⇒ λnil_nil_prf. [ ]
408 | cons hd tl ⇒ λnil_cons_absrd. ?
410 | cons hd tl ⇒ λcons_prf.
411 match right return λx. |hd::tl| = |x| → list (A × B) with
412 [ nil ⇒ λcons_nil_absrd. ?
413 | cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ?
416 [ 1: normalize in nil_cons_absrd;
417 destruct(nil_cons_absrd)
418 | 2: normalize in cons_nil_absrd;
419 destruct(cons_nil_absrd)
420 | 3: normalize in cons_cons_prf;
426 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)) ≝
428 [ 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))
431 [ nil ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 ?
433 match zip ? ? tl tl' with
434 [ None ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 ?
435 | 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)
440 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 ≝
443 | cons hd tl ⇒ foldl A B f (f a hd) tl
451 ∀pre:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 B.
453 \ 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).
454 #A #B #H #acc #pre generalize in match acc; -acc; elim pre
456 | #hd #tl #IH #acc #X normalize; @IH ]
464 ∀suff,pre:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 B.
465 \ 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).
466 #A #B #H #acc #suff elim suff
467 [ #pre >
\ 5a href="cic:/matita/basics/list/append_nil.def(4)"
\ 6append_nil
\ 5/a
\ 6 %
468 | #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])) ]
473 λ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).
474 \ 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.
476 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 ≝
478 [ nil ⇒
\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"
\ 6nil
\ 5/a
\ 6 A
479 | 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 ]
486 |(l @ r)| = |l| + |r|.
506 rev A (l @ r) = rev A r @ rev A l.
509 [ normalize >append_nil %
525 >(append_length A (rev A TL) [HD])
530 lemma nth_append_first:
532 ∀n:nat.∀l1,l2:list A.∀d:A.
533 n < |l1| → nth n A (l1@l2) d = nth n A l1 d.
535 generalize in match n; -n; elim l1
536 [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O
537 | #h #t #Hind #k normalize
539 [ #Hk normalize @refl
540 | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
545 lemma nth_append_second:
546 ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 ->
547 nth n A (l1@l2) d = nth (n - length A l1) A l2 d.
549 generalize in match n; -n; elim l1
550 [ normalize #k #Hk <(minus_n_O) @refl
551 | #h #t #Hind #k normalize
553 [ #Hk @⊥ @(absurd (S (|t|) ≤ 0)) [ @Hk | @not_le_Sn_O ]
554 | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
560 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
561 for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f] }.
562 notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp)" non associative with precedence 19
563 for @{ match $e with [ true ⇒ $t | false ⇒ $f] }.
565 let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
566 (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 ≝
569 | 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
572 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.
574 (* notation "hvbox(t\lceil o \mapsto h\rceil )"
576 for @{ match (? : $o=$h) with [ refl \Rightarrow $t ] }. *)
578 definition function_apply ≝
584 notation "f break $ x"
585 left associative with precedence 99
586 for @{ 'function_apply $f $x }.
588 interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
590 notation "f break $ x"
591 left associative with precedence 99
592 for @{ 'function_apply $f $x }.
594 interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
596 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 ≝
599 | S o ⇒ f (iterate A f a o)
602 (* Yeah, I probably ought to do something more general... *)
603 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
604 with precedence 90 for @{ 'triple $a $b $c}.
605 interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
607 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
608 with precedence 90 for @{ 'quadruple $a $b $c $d}.
609 interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
611 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
613 for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.
615 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
617 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
619 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
621 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
627 ∀P: A
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6B → C → Prop.
628 (∀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)) →
629 P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
636 ∀P: A
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6B → C → C' → Prop.
637 (∀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)) →
638 P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
640 lemma pair_destruct_1:
641 ∀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.
642 #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/
645 lemma pair_destruct_2:
646 ∀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.
647 #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/
651 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 ≝
655 [ false ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6
656 | true ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6
660 [ false ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6
661 | true ⇒
\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6
665 (* dpm: conflicts with library definitions
666 interpretation "Nat less than" 'lt m n = (ltb m n).
667 interpretation "Nat greater than" 'gt m n = (gtb m n).
668 interpretation "Nat greater than eq" 'geq m n = (geb m n).
671 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) ≝
672 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
673 [ true ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
676 [ O ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
677 | (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)
681 definition division ≝
682 λm, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
684 [ O ⇒
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m
685 | S o ⇒
\ 5a href="cic:/matita/Cerco/ASM/Utils/division_aux.fix(0,0,3)"
\ 6division_aux
\ 5/a
\ 6 m m o
688 notation "hvbox(n break ÷ m)"
689 right associative with precedence 47
690 for @{ 'division $n $m }.
692 interpretation "Nat division" 'division n m = (division n m).
694 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) ≝
695 match
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 n p with
700 | 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
705 λm, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
708 | S o ⇒
\ 5a href="cic:/matita/Cerco/ASM/Utils/modulus_aux.fix(0,0,2)"
\ 6modulus_aux
\ 5/a
\ 6 m m o
711 notation "hvbox(n break 'mod' m)"
712 right associative with precedence 47
713 for @{ 'modulus $n $m }.
715 interpretation "Nat modulus" 'modulus m n = (modulus m n).
717 definition divide_with_remainder ≝
718 λm, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
719 \ 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).
721 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 ≝
723 [ 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
724 | S o ⇒ m
\ 5a title="natural times" href="cic:/fakeuri.def(1)"
\ 6*
\ 5/a
\ 6 exponential m o
727 interpretation "Nat exponential" 'exp n m = (exponential n m).
729 notation "hvbox(a break ⊎ b)"
730 left associative with precedence 50
731 for @{ 'disjoint_union $a $b }.
732 interpretation "sum" 'disjoint_union A B = (Sum A B).
734 theorem less_than_or_equal_monotone:
735 ∀m, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
736 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).
739 /
\ 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/
742 theorem less_than_or_equal_b_complete:
743 ∀m, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
744 \ 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).
754 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace {}
\ 5/span
\ 6\ 5/span
\ 6/
755 | /
\ 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/
760 theorem less_than_or_equal_b_correct:
761 ∀m, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
762 \ 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.
771 | #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/
775 definition less_than_or_equal_b_elim:
776 ∀m, n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.
777 ∀P:
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6 → Type[0].
778 (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).
780 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)
781 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)
782 cases (
\ 5a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"
\ 6leb
\ 5/a
\ 6 m n)
783 /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace {}
\ 5/span
\ 6\ 5/span
\ 6/
786 lemma inclusive_disjunction_true:
787 ∀b, c:
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6.
788 (
\ 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.
794 @
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6
797 /
\ 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/
801 lemma conjunction_true:
802 ∀b, c:
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6.
803 \ 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.
808 [ /
\ 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/
814 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.
819 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.
825 definition bool_to_Prop ≝
826 λ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 ].
828 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].
830 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.
831 *; /
\ 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/