-
Notifications
You must be signed in to change notification settings - Fork 258
/
Pi.lean
161 lines (138 loc) · 6.13 KB
/
Pi.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
import Mathlib.Data.Multiset.Bind
#align_import data.multiset.pi from "leanprover-community/mathlib"@"b2c89893177f66a48daf993b7ba5ef7cddeff8c9"
/-!
# The cartesian product of multisets
-/
namespace Multiset
section Pi
variable {α : Type*}
open Function
/-- Given `δ : α → Type*`, `Pi.empty δ` is the trivial dependent function out of the empty
multiset. -/
def Pi.empty (δ : α → Sort*) : ∀ a ∈ (0 : Multiset α), δ a :=
nofun
#align multiset.pi.empty Multiset.Pi.empty
universe u v
variable [DecidableEq α] {β : α → Type u} {δ : α → Sort v}
/-- Given `δ : α → Type*`, a multiset `m` and a term `a`, as well as a term `b : δ a` and a
function `f` such that `f a' : δ a'` for all `a'` in `m`, `Pi.cons m a b f` is a function `g` such
that `g a'' : δ a''` for all `a''` in `a ::ₘ m`. -/
def Pi.cons (m : Multiset α) (a : α) (b : δ a) (f : ∀ a ∈ m, δ a) : ∀ a' ∈ a ::ₘ m, δ a' :=
fun a' ha' => if h : a' = a then Eq.ndrec b h.symm else f a' <| (mem_cons.1 ha').resolve_left h
#align multiset.pi.cons Multiset.Pi.cons
theorem Pi.cons_same {m : Multiset α} {a : α} {b : δ a} {f : ∀ a ∈ m, δ a} (h : a ∈ a ::ₘ m) :
Pi.cons m a b f a h = b :=
dif_pos rfl
#align multiset.pi.cons_same Multiset.Pi.cons_same
theorem Pi.cons_ne {m : Multiset α} {a a' : α} {b : δ a} {f : ∀ a ∈ m, δ a} (h' : a' ∈ a ::ₘ m)
(h : a' ≠ a) : Pi.cons m a b f a' h' = f a' ((mem_cons.1 h').resolve_left h) :=
dif_neg h
#align multiset.pi.cons_ne Multiset.Pi.cons_ne
theorem Pi.cons_swap {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : ∀ a ∈ m, δ a}
(h : a ≠ a') : HEq (Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' f))
(Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b f)) := by
apply hfunext rfl
simp only [heq_iff_eq]
rintro a'' _ rfl
refine' hfunext (by rw [Multiset.cons_swap]) fun ha₁ ha₂ _ => _
rcases ne_or_eq a'' a with (h₁ | rfl)
on_goal 1 => rcases eq_or_ne a'' a' with (rfl | h₂)
all_goals simp [*, Pi.cons_same, Pi.cons_ne]
#align multiset.pi.cons_swap Multiset.Pi.cons_swap
@[simp, nolint simpNF] -- Porting note: false positive, this lemma can prove itself
theorem pi.cons_eta {m : Multiset α} {a : α} (f : ∀ a' ∈ a ::ₘ m, δ a') :
(Pi.cons m a (f _ (mem_cons_self _ _)) fun a' ha' => f a' (mem_cons_of_mem ha')) = f := by
ext a' h'
by_cases h : a' = a
· subst h
rw [Pi.cons_same]
· rw [Pi.cons_ne _ h]
#align multiset.pi.cons_eta Multiset.pi.cons_eta
theorem Pi.cons_injective {a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) :
Function.Injective (Pi.cons s a b) := fun f₁ f₂ eq =>
funext fun a' =>
funext fun h' =>
have ne : a ≠ a' := fun h => hs <| h.symm ▸ h'
have : a' ∈ a ::ₘ s := mem_cons_of_mem h'
calc
f₁ a' h' = Pi.cons s a b f₁ a' this := by rw [Pi.cons_ne this ne.symm]
_ = Pi.cons s a b f₂ a' this := by rw [eq]
_ = f₂ a' h' := by rw [Pi.cons_ne this ne.symm]
#align multiset.pi.cons_injective Multiset.Pi.cons_injective
/-- `pi m t` constructs the Cartesian product over `t` indexed by `m`. -/
def pi (m : Multiset α) (t : ∀ a, Multiset (β a)) : Multiset (∀ a ∈ m, β a) :=
m.recOn {Pi.empty β}
(fun a m (p : Multiset (∀ a ∈ m, β a)) => (t a).bind fun b => p.map <| Pi.cons m a b)
(by
intro a a' m n
by_cases eq : a = a'
· subst eq; rfl
· simp only [map_bind, map_map, comp_apply, bind_bind (t a') (t a)]
apply bind_hcongr
· rw [cons_swap a a']
intro b _
apply bind_hcongr
· rw [cons_swap a a']
intro b' _
apply map_hcongr
· rw [cons_swap a a']
intro f _
exact Pi.cons_swap eq)
#align multiset.pi Multiset.pi
@[simp]
theorem pi_zero (t : ∀ a, Multiset (β a)) : pi 0 t = {Pi.empty β} :=
rfl
#align multiset.pi_zero Multiset.pi_zero
@[simp]
theorem pi_cons (m : Multiset α) (t : ∀ a, Multiset (β a)) (a : α) :
pi (a ::ₘ m) t = (t a).bind fun b => (pi m t).map <| Pi.cons m a b :=
recOn_cons a m
#align multiset.pi_cons Multiset.pi_cons
theorem card_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
card (pi m t) = prod (m.map fun a => card (t a)) :=
Multiset.induction_on m (by simp) (by simp (config := { contextual := true }) [mul_comm])
#align multiset.card_pi Multiset.card_pi
protected theorem Nodup.pi {s : Multiset α} {t : ∀ a, Multiset (β a)} :
Nodup s → (∀ a ∈ s, Nodup (t a)) → Nodup (pi s t) :=
Multiset.induction_on s (fun _ _ => nodup_singleton _)
(by
intro a s ih hs ht
have has : a ∉ s := by simp only [nodup_cons] at hs; exact hs.1
have hs : Nodup s := by simp only [nodup_cons] at hs; exact hs.2
simp only [pi_cons, nodup_bind]
refine'
⟨fun b _ => ((ih hs) fun a' h' => ht a' <| mem_cons_of_mem h').map (Pi.cons_injective has),
_⟩
refine' (ht a <| mem_cons_self _ _).pairwise _
exact fun b₁ _ b₂ _ neb =>
disjoint_map_map.2 fun f _ g _ eq =>
have : Pi.cons s a b₁ f a (mem_cons_self _ _) = Pi.cons s a b₂ g a (mem_cons_self _ _) :=
by rw [eq]
neb <| show b₁ = b₂ by rwa [Pi.cons_same, Pi.cons_same] at this)
#align multiset.nodup.pi Multiset.Nodup.pi
theorem mem_pi (m : Multiset α) (t : ∀ a, Multiset (β a)) :
∀ f : ∀ a ∈ m, β a, f ∈ pi m t ↔ ∀ (a) (h : a ∈ m), f a h ∈ t a := by
intro f
induction' m using Multiset.induction_on with a m ih
· have : f = Pi.empty β := funext (fun _ => funext fun h => (not_mem_zero _ h).elim)
simp only [this, pi_zero, mem_singleton, true_iff]
intro _ h; exact (not_mem_zero _ h).elim
simp_rw [pi_cons, mem_bind, mem_map, ih]
constructor
· rintro ⟨b, hb, f', hf', rfl⟩ a' ha'
by_cases h : a' = a
· subst h
rwa [Pi.cons_same]
· rw [Pi.cons_ne _ h]
apply hf'
· intro hf
refine' ⟨_, hf a (mem_cons_self _ _), _, fun a ha => hf a (mem_cons_of_mem ha), _⟩
rw [pi.cons_eta]
#align multiset.mem_pi Multiset.mem_pi
end Pi
end Multiset