2 include "arithmetics/bounded_quantifiers.ma".
3 include "basics/lists/search.ma".
5 (* A bit of combinatorics *)
6 interpretation "list membership" 'mem a l = (mem ? a l).
8 \ 5img class="anchor" src="icons/tick.png" id="decidable_mem_nat"
\ 6lemma decidable_mem_nat: ∀n:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6.∀l.
\ 5a href="cic:/matita/basics/logic/decidable.def(1)"
\ 6decidable
\ 5/a
\ 6 (n
\ 5a title="list membership" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 l).
10 [%2 % @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 |#a #tl #Htl @
\ 5a href="cic:/matita/arithmetics/bounded_quantifiers/decidable_or.def(3)"
\ 6decidable_or
\ 5/a
\ 6 //]
13 \ 5img class="anchor" src="icons/tick.png" id="length_unique_le"
\ 6lemma length_unique_le: ∀n,l.
\ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"
\ 6unique
\ 5/a
\ 6 ? l → (∀x. x
\ 5a title="list membership" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 l → x
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n) → |l
\ 5a title="list length" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n.
15 [* // #a #tl #_ #H @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 (a
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"
\ 60
\ 5/a
\ 6))
16 [@H %1 % | @
\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"
\ 6le_to_not_lt
\ 5/a
\ 6 //]
17 |#m #Hind #l #Huni #Hmem <(
\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"
\ 6filter_length2
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 m) l)
18 lapply (
\ 5a href="cic:/matita/basics/lists/search/length_filter_eqb.def(8)"
\ 6length_filter_eqb
\ 5/a
\ 6 … m l Huni) #Hle
19 @(
\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"
\ 6transitive_le
\ 5/a
\ 6 ? (
\ 5a title="natural number" href="cic:/fakeuri.def(1)"
\ 61
\ 5/a
\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6|
\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"
\ 6filter
\ 5/a
\ 6 ? (λx.
\ 5a title="boolean not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 m x) l
\ 5a title="list length" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6))
20 [@
\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"
\ 6le_plus
\ 5/a
\ 6 //
21 |@
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6 @Hind
22 [@
\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"
\ 6unique_filter
\ 5/a
\ 6 //
23 |#x #memx cut (x
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 m)
24 [@
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 @Hmem @(
\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"
\ 6mem_filter
\ 5/a
\ 6 … memx)] #Hcut
25 cases(
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … Hcut) // #eqxm @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6
26 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 ? eqxm) @
\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"
\ 6sym_not_eq
\ 5/a
\ 6 @
\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"
\ 6eqb_false_to_not_eq
\ 5/a
\ 6
27 @
\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"
\ 6injective_notb
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"
\ 6mem_filter_true
\ 5/a
\ 6 ???? memx)
33 \ 5img class="anchor" src="icons/tick.png" id="eq_length_to_mem"
\ 6lemma eq_length_to_mem : ∀n,l. |l
\ 5a title="list length" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6 \ 5a title="leibnitz's equality" 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 →
\ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"
\ 6unique
\ 5/a
\ 6 ? l →
34 (∀x. x
\ 5a title="list membership" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 l → x
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 n) → n
\ 5a title="list membership" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 l.
35 #n #l #H1 #H2 #H3 cases (
\ 5a href="cic:/matita/arithmetics/pidgeon_hole/decidable_mem_nat.def(6)"
\ 6decidable_mem_nat
\ 5/a
\ 6 n l) //
36 #H4 @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 (|l
\ 5a title="list length" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6 \ 5a title="natural 'greater than'" href="cic:/fakeuri.def(1)"
\ 6>
\ 5/a
\ 6 n))
38 |@
\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"
\ 6le_to_not_lt
\ 5/a
\ 6 @
\ 5a href="cic:/matita/arithmetics/pidgeon_hole/length_unique_le.def(9)"
\ 6length_unique_le
\ 5/a
\ 6 //
39 #x #memx cases(
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … (H3 x memx)) //
40 #Heq @
\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"
\ 6not_le_to_lt
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … H4) #_ <Heq //
44 \ 5img class="anchor" src="icons/tick.png" id="eq_length_to_mem_all"
\ 6lemma eq_length_to_mem_all: ∀n,l. |l
\ 5a title="list length" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 n →
\ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"
\ 6unique
\ 5/a
\ 6 ? l →
45 (∀x. x
\ 5a title="list membership" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 l → x
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n) → ∀i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n → i
\ 5a title="list membership" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 l.
47 [#l #_ #_ #_ #i #lti0 @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 ? lti0 (
\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"
\ 6not_le_Sn_O
\ 5/a
\ 6 ?))
48 |#m #Hind #l #H #H1 #H2 #i #lei cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … lei)
49 [#leim @(
\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"
\ 6mem_filter
\ 5/a
\ 6… (λi.
\ 5a title="boolean not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6(
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 m i)))
50 cases (
\ 5a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"
\ 6filter_eqb
\ 5/a
\ 6 m … H1)
51 [2: * #H @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 ?? H) @
\ 5a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"
\ 6eq_length_to_mem
\ 5/a
\ 6 //
52 #x #memx @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 @H2 //]
53 * #memm #Hfilter @Hind
54 [@
\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"
\ 6injective_S
\ 5/a
\ 6 <H <(
\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"
\ 6filter_length2
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 m) l) >Hfilter %
55 |@
\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"
\ 6unique_filter
\ 5/a
\ 6 @H1
56 |#x #memx cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … (H2 x (
\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"
\ 6mem_filter
\ 5/a
\ 6 … memx))) #H3
57 [@
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 @H3
58 |@
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 (m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6x)) [@
\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"
\ 6injective_S
\ 5/a
\ 6 //] @
\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"
\ 6eqb_false_to_not_eq
\ 5/a
\ 6
59 @
\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"
\ 6injective_notb
\ 5/a
\ 6 >(
\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"
\ 6mem_filter_true
\ 5/a
\ 6 ???? memx) %
61 |@
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 @leim
63 |#eqi @
\ 5a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"
\ 6eq_length_to_mem
\ 5/a
\ 6 >eqi [@H |@H1 |#x #Hx @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 >eqi @H2 //]
68 \ 5img class="anchor" src="icons/tick.png" id="lt_length_to_not_mem"
\ 6lemma lt_length_to_not_mem: ∀n,l.
\ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"
\ 6unique
\ 5/a
\ 6 ? l → (∀x. x
\ 5a title="list membership" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 l → x
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n) → |l
\ 5a title="list length" href="cic:/fakeuri.def(1)"
\ 6|
\ 5/a
\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n →
69 \ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6i. i
\ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"
\ 6<
\ 5/a
\ 6 n
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6 (i
\ 5a title="list membership" href="cic:/fakeuri.def(1)"
\ 6∈
\ 5/a
\ 6 l).
71 [#l #_ #_ #H @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
72 |#m #Hind #l #Huni #Hmem #Hlen cases (
\ 5a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"
\ 6filter_eqb
\ 5/a
\ 6 m … Huni)
74 |* #memm #Hfilter cases (Hind (
\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"
\ 6filter
\ 5/a
\ 6 ? (λx.
\ 5a title="boolean not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6(
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 m x)) l) ? ? ?)
75 [#i * #ltim #memi %{i} % [@
\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"
\ 6le_S
\ 5/a
\ 6 // ]
76 @(
\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"
\ 6not_to_not
\ 5/a
\ 6 … memi) @
\ 5a href="cic:/matita/basics/lists/search/mem_filter_l.def(4)"
\ 6mem_filter_l
\ 5/a
\ 6 @
\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"
\ 6injective_notb
\ 5/a
\ 6 >
\ 5a href="cic:/matita/basics/bool/notb_notb.def(2)"
\ 6notb_notb
\ 5/a
\ 6
77 @
\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"
\ 6not_eq_to_eqb_false
\ 5/a
\ 6 @
\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"
\ 6sym_not_eq
\ 5/a
\ 6 @
\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"
\ 6lt_to_not_eq
\ 5/a
\ 6 //
78 |@
\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"
\ 6unique_filter
\ 5/a
\ 6 //
79 |#x #memx cases (
\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"
\ 6le_to_or_lt_eq
\ 5/a
\ 6 … (Hmem x ?))
80 [#H @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 @H
81 |#H @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 @(
\ 5a href="cic:/matita/basics/logic/absurd.def(2)"
\ 6absurd
\ 5/a
\ 6 (m
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6x)) [@
\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"
\ 6injective_S
\ 5/a
\ 6 //] @
\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"
\ 6eqb_false_to_not_eq
\ 5/a
\ 6
82 @
\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"
\ 6injective_notb
\ 5/a
\ 6 >(
\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"
\ 6mem_filter_true
\ 5/a
\ 6 ???? memx) %
83 |@(
\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"
\ 6mem_filter
\ 5/a
\ 6 … memx)
85 |<(
\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"
\ 6filter_length2
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"
\ 6eqb
\ 5/a
\ 6 m)) in Hlen; >Hfilter #H
86 @
\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"
\ 6le_S_S_to_le
\ 5/a
\ 6 @H