Skip to content

Commit

Permalink
refactor(data/list/forall2): consistent names of relations (#16098)
Browse files Browse the repository at this point in the history 


Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz>
  • Loading branch information
@madvorak
madvorak and madvorak committed Sep 2, 2022
1 parent 3c92748 commit d6789b8
Showing 1 changed file with 60 additions and 62 deletions.
122 changes: 60 additions & 62 deletions src/data/list/forall2.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,35 +17,35 @@ open nat function

namespace list

variables {α β γ δ : Type*} {r : α → β → Prop} {p : γ → δ → Prop}
variables {α β γ δ : Type*} {R S : α → β → Prop} {P : γ → δ → Prop} {Rₐ : α → α → Prop}
open relator

mk_iff_of_inductive_prop list.forall₂ list.forall₂_iff

@[simp] theorem forall₂_cons {R : α → β → Prop} {a b l₁ l₂} :
@[simp] theorem forall₂_cons {a b l₁ l₂} :
forall₂ R (a :: l₁) (b :: l₂) ↔ R a b ∧ forall₂ R l₁ l₂ :=
⟨λ h, by cases h with h₁ h₂; split; assumption, λ ⟨h₁, h₂⟩, forall₂.cons h₁ h₂⟩

theorem forall₂.imp {R S : α → β → Prop}
theorem forall₂.imp
(H : ∀ a b, R a b → S a b) {l₁ l₂}
(h : forall₂ R l₁ l₂) : forall₂ S l₁ l₂ :=
by induction h; constructor; solve_by_elim

lemma forall₂.mp {r q s : α → β → Prop} (h : ∀ a b, r a b → q a b → s a b) :
∀ {l₁ l₂}, forall₂ r l₁ l₂ → forall₂ q l₁ l₂ → forall₂ s l₁ l₂
lemma forall₂.mp {Q : α → β → Prop} (h : ∀ a b, Q a b → R a b → S a b) :
∀ {l₁ l₂}, forall₂ Q l₁ l₂ → forall₂ R l₁ l₂ → forall₂ S l₁ l₂
| [] [] forall₂.nil forall₂.nil := forall₂.nil
| (a :: l₁) (b :: l₂) (forall₂.cons hr hrs) (forall₂.cons hq hqs) :=
forall₂.cons (h a b hr hq) (forall₂.mp hrs hqs)

lemma forall₂.flip : ∀ {a b}, forall₂ (flip r) b a → forall₂ r a b
lemma forall₂.flip : ∀ {a b}, forall₂ (flip R) b a → forall₂ R a b
| _ _ forall₂.nil := forall₂.nil
| (a :: as) (b :: bs) (forall₂.cons h₁ h₂) := forall₂.cons h₁ h₂.flip

@[simp] lemma forall₂_same {r : α → α → Prop} : ∀ {l : list α}, forall₂ r l l ↔ ∀ x ∈ l, r x x
@[simp] lemma forall₂_same : ∀ {l : list α}, forall₂ Rₐ l l ↔ ∀ x ∈ l, Rₐ x x
| [] := by simp
| (a :: l) := by simp [@forall₂_same l]

lemma forall₂_refl {r} [is_refl α r] (l : list α) : forall₂ r l l :=
lemma forall₂_refl [is_refl α Rₐ] (l : list α) : forall₂ Rₐ l l :=
forall₂_same.2 $ λ a h, refl _

@[simp] lemma forall₂_eq_eq_eq : forall₂ ((=) : α → α → Prop) = (=) :=
Expand All @@ -56,92 +56,92 @@ begin
{ rintro rfl, exact forall₂_refl _ }
end

@[simp, priority 900] lemma forall₂_nil_left_iff {l} : forall₂ r nil l ↔ l = nil :=
@[simp, priority 900] lemma forall₂_nil_left_iff {l} : forall₂ R nil l ↔ l = nil :=
⟨λ H, by cases H; refl, by rintro rfl; exact forall₂.nil⟩

@[simp, priority 900] lemma forall₂_nil_right_iff {l} : forall₂ r l nil ↔ l = nil :=
@[simp, priority 900] lemma forall₂_nil_right_iff {l} : forall₂ R l nil ↔ l = nil :=
⟨λ H, by cases H; refl, by rintro rfl; exact forall₂.nil⟩

lemma forall₂_cons_left_iff {a l u} :
forall₂ r (a :: l) u ↔ (∃b u', r a b ∧ forall₂ r l u' ∧ u = b :: u') :=
forall₂ R (a :: l) u ↔ (∃b u', R a b ∧ forall₂ R l u' ∧ u = b :: u') :=
iff.intro
(λ h, match u, h with (b :: u'), forall₂.cons h₁ h₂ := ⟨b, u', h₁, h₂, rfl⟩ end)
(λ h, match u, h with _, ⟨b, u', h₁, h₂, rfl⟩ := forall₂.cons h₁ h₂ end)

lemma forall₂_cons_right_iff {b l u} :
forall₂ r u (b :: l) ↔ (∃a u', r a b ∧ forall₂ r u' l ∧ u = a :: u') :=
forall₂ R u (b :: l) ↔ (∃a u', R a b ∧ forall₂ R u' l ∧ u = a :: u') :=
iff.intro
(λ h, match u, h with (b :: u'), forall₂.cons h₁ h₂ := ⟨b, u', h₁, h₂, rfl⟩ end)
(λ h, match u, h with _, ⟨b, u', h₁, h₂, rfl⟩ := forall₂.cons h₁ h₂ end)

lemma forall₂_and_left {r : α → β → Prop} {p : α → Prop} :
∀ l u, forall₂ (λa b, p a ∧ r a b) l u ↔ (∀ a∈l, p a) ∧ forall₂ r l u
lemma forall₂_and_left {p : α → Prop} :
∀ l u, forall₂ (λa b, p a ∧ R a b) l u ↔ (∀ a∈l, p a) ∧ forall₂ R l u
| [] u := by simp only [forall₂_nil_left_iff, forall_prop_of_false (not_mem_nil _),
imp_true_iff, true_and]
| (a :: l) u := by simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons,
and_assoc, and_comm, and.left_comm, exists_and_distrib_left.symm]

@[simp] lemma forall₂_map_left_iff {f : γ → α} :
∀ {l u}, forall₂ r (map f l) u ↔ forall₂ (λc b, r (f c) b) l u
∀ {l u}, forall₂ R (map f l) u ↔ forall₂ (λc b, R (f c) b) l u
| [] _ := by simp only [map, forall₂_nil_left_iff]
| (a :: l) _ := by simp only [map, forall₂_cons_left_iff, forall₂_map_left_iff]

@[simp] lemma forall₂_map_right_iff {f : γ → β} :
∀ {l u}, forall₂ r l (map f u) ↔ forall₂ (λa c, r a (f c)) l u
∀ {l u}, forall₂ R l (map f u) ↔ forall₂ (λa c, R a (f c)) l u
| _ [] := by simp only [map, forall₂_nil_right_iff]
| _ (b :: u) := by simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]

lemma left_unique_forall₂' (hr : left_unique r) :
∀ {a b c}, forall₂ r a c → forall₂ r b c → a = b
lemma left_unique_forall₂' (hr : left_unique R) :
∀ {a b c}, forall₂ R a c → forall₂ R b c → a = b
| a₀ nil a₁ forall₂.nil forall₂.nil := rfl
| (a₀ :: l₀) (b :: l) (a₁ :: l₁) (forall₂.cons ha₀ h₀) (forall₂.cons ha₁ h₁) :=
hr ha₀ ha₁ ▸ left_unique_forall₂' h₀ h₁ ▸ rfl

lemma _root_.relator.left_unique.forall₂ (hr : left_unique r) : left_unique (forall₂ r) :=
lemma _root_.relator.left_unique.forall₂ (hr : left_unique R) : left_unique (forall₂ R) :=
@left_unique_forall₂' _ _ _ hr

lemma right_unique_forall₂' (hr : right_unique r) : ∀ {a b c}, forall₂ r a b → forall₂ r a c → b = c
lemma right_unique_forall₂' (hr : right_unique R) : ∀ {a b c}, forall₂ R a b → forall₂ R a c → b = c
| nil a₀ a₁ forall₂.nil forall₂.nil := rfl
| (b :: l) (a₀ :: l₀) (a₁ :: l₁) (forall₂.cons ha₀ h₀) (forall₂.cons ha₁ h₁) :=
hr ha₀ ha₁ ▸ right_unique_forall₂' h₀ h₁ ▸ rfl

lemma _root_.relator.right_unique.forall₂ (hr : right_unique r) : right_unique (forall₂ r) :=
lemma _root_.relator.right_unique.forall₂ (hr : right_unique R) : right_unique (forall₂ R) :=
@right_unique_forall₂' _ _ _ hr

lemma _root_.relator.bi_unique.forall₂ (hr : bi_unique r) : bi_unique (forall₂ r) :=
lemma _root_.relator.bi_unique.forall₂ (hr : bi_unique R) : bi_unique (forall₂ R) :=
⟨hr.left.forall₂, hr.right.forall₂⟩

theorem forall₂.length_eq {R : α → β → Prop} :
theorem forall₂.length_eq :
∀ {l₁ l₂}, forall₂ R l₁ l₂ → length l₁ = length l₂
| _ _ forall₂.nil := rfl
| _ _ (forall₂.cons h₁ h₂) := congr_arg succ (forall₂.length_eq h₂)

theorem forall₂.nth_le :
∀ {x : list α} {y : list β} (h : forall₂ r x y) ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length),
r (x.nth_le i hx) (y.nth_le i hy)
∀ {x : list α} {y : list β} (h : forall₂ R x y) ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length),
R (x.nth_le i hx) (y.nth_le i hy)
| (a₁ :: l₁) (a₂ :: l₂) (forall₂.cons ha hl) 0 hx hy := ha
| (a₁ :: l₁) (a₂ :: l₂) (forall₂.cons ha hl) (succ i) hx hy := hl.nth_le _ _

lemma forall₂_of_length_eq_of_nth_le : ∀ {x : list α} {y : list β},
x.length = y.length → (∀ i h₁ h₂, r (x.nth_le i h₁) (y.nth_le i h₂)) → forall₂ r x y
x.length = y.length → (∀ i h₁ h₂, R (x.nth_le i h₁) (y.nth_le i h₂)) → forall₂ R x y
| [] [] hl h := forall₂.nil
| (a₁ :: l₁) (a₂ :: l₂) hl h := forall₂.cons
(h 0 (nat.zero_lt_succ _) (nat.zero_lt_succ _))
(forall₂_of_length_eq_of_nth_le (succ.inj hl) (
λ i h₁ h₂, h i.succ (succ_lt_succ h₁) (succ_lt_succ h₂)))

theorem forall₂_iff_nth_le {l₁ : list α} {l₂ : list β} :
forall₂ r l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ i h₁ h₂, r (l₁.nth_le i h₁) (l₂.nth_le i h₂) :=
forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ i h₁ h₂, R (l₁.nth_le i h₁) (l₂.nth_le i h₂) :=
⟨λ h, ⟨h.length_eq, h.nth_le⟩, and.rec forall₂_of_length_eq_of_nth_le⟩

theorem forall₂_zip {R : α → β → Prop} :
theorem forall₂_zip :
∀ {l₁ l₂}, forall₂ R l₁ l₂ → ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b
| _ _ (forall₂.cons h₁ h₂) x y (or.inl rfl) := h₁
| _ _ (forall₂.cons h₁ h₂) x y (or.inr h₃) := forall₂_zip h₂ h₃

theorem forall₂_iff_zip {R : α → β → Prop} {l₁ l₂} : forall₂ R l₁ l₂ ↔
theorem forall₂_iff_zip {l₁ l₂} : forall₂ R l₁ l₂ ↔
length l₁ = length l₂ ∧ ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b :=
⟨λ h, ⟨h.length_eq, @forall₂_zip _ _ _ _ _ h⟩,
⟨λ h, ⟨forall₂.length_eq h, @forall₂_zip _ _ _ _ _ h⟩,
λ h, begin
cases h with h₁ h₂,
induction l₁ with a l₁ IH generalizing l₂,
Expand All @@ -150,73 +150,73 @@ theorem forall₂_iff_zip {R : α → β → Prop} {l₁ l₂} : forall₂ R l
exact forall₂.cons (h₂ $ or.inl rfl) (IH h₁ $ λ a b h, h₂ $ or.inr h) }
end⟩

theorem forall₂_take {R : α → β → Prop} :
theorem forall₂_take :
∀ n {l₁ l₂}, forall₂ R l₁ l₂ → forall₂ R (take n l₁) (take n l₂)
| 0 _ _ _ := by simp only [forall₂.nil, take]
| (n+1) _ _ (forall₂.nil) := by simp only [forall₂.nil, take]
| (n+1) _ _ (forall₂.cons h₁ h₂) := by simp [and.intro h₁ h₂, forall₂_take n]

theorem forall₂_drop {R : α → β → Prop} :
theorem forall₂_drop :
∀ n {l₁ l₂}, forall₂ R l₁ l₂ → forall₂ R (drop n l₁) (drop n l₂)
| 0 _ _ h := by simp only [drop, h]
| (n+1) _ _ (forall₂.nil) := by simp only [forall₂.nil, drop]
| (n+1) _ _ (forall₂.cons h₁ h₂) := by simp [and.intro h₁ h₂, forall₂_drop n]

theorem forall₂_take_append {R : α → β → Prop} (l : list α) (l₁ : list β) (l₂ : list β)
theorem forall₂_take_append (l : list α) (l₁ : list β) (l₂ : list β)
(h : forall₂ R l (l₁ ++ l₂)) : forall₂ R (list.take (length l₁) l) l₁ :=
have h': forall₂ R (take (length l₁) l) (take (length l₁) (l₁ ++ l₂)),
from forall₂_take (length l₁) h,
by rwa [take_left] at h'

theorem forall₂_drop_append {R : α → β → Prop} (l : list α) (l₁ : list β) (l₂ : list β)
theorem forall₂_drop_append (l : list α) (l₁ : list β) (l₂ : list β)
(h : forall₂ R l (l₁ ++ l₂)) : forall₂ R (list.drop (length l₁) l) l₂ :=
have h': forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)),
from forall₂_drop (length l₁) h,
by rwa [drop_left] at h'

lemma rel_mem (hr : bi_unique r) : (r ⇒ forall₂ r ⇒ iff) (∈) (∈)
lemma rel_mem (hr : bi_unique R) : (R ⇒ forall₂ R ⇒ iff) (∈) (∈)
| a b h [] [] forall₂.nil := by simp only [not_mem_nil]
| a b h (a' :: as) (b' :: bs) (forall₂.cons h₁ h₂) := rel_or (rel_eq hr h h₁) (rel_mem h h₂)

lemma rel_map : ((r ⇒ p) ⇒ forall₂ r ⇒ forall₂ p) map map
lemma rel_map : ((R ⇒ P) ⇒ forall₂ R ⇒ forall₂ P) map map
| f g h [] [] forall₂.nil := forall₂.nil
| f g h (a :: as) (b :: bs) (forall₂.cons h₁ h₂) := forall₂.cons (h h₁) (rel_map @h h₂)

lemma rel_append : (forall₂ r ⇒ forall₂ r ⇒ forall₂ r) append append
lemma rel_append : (forall₂ R ⇒ forall₂ R ⇒ forall₂ R) append append
| [] [] h l₁ l₂ hl := hl
| (a :: as) (b :: bs) (forall₂.cons h₁ h₂) l₁ l₂ hl := forall₂.cons h₁ (rel_append h₂ hl)

lemma rel_reverse : (forall₂ r ⇒ forall₂ r) reverse reverse
lemma rel_reverse : (forall₂ R ⇒ forall₂ R) reverse reverse
| [] [] forall₂.nil := forall₂.nil
| (a :: as) (b :: bs) (forall₂.cons h₁ h₂) := begin
simp only [reverse_cons],
exact rel_append (rel_reverse h₂) (forall₂.cons h₁ forall₂.nil)
end

@[simp]
lemma forall₂_reverse_iff {l₁ l₂} : forall₂ r (reverse l₁) (reverse l₂) ↔ forall₂ r l₁ l₂ :=
lemma forall₂_reverse_iff {l₁ l₂} : forall₂ R (reverse l₁) (reverse l₂) ↔ forall₂ R l₁ l₂ :=
iff.intro
(λ h, by { rw [← reverse_reverse l₁, ← reverse_reverse l₂], exact rel_reverse h })
(λ h, rel_reverse h)

lemma rel_join : (forall₂ (forall₂ r) ⇒ forall₂ r) join join
lemma rel_join : (forall₂ (forall₂ R) ⇒ forall₂ R) join join
| [] [] forall₂.nil := forall₂.nil
| (a :: as) (b :: bs) (forall₂.cons h₁ h₂) := rel_append h₁ (rel_join h₂)

lemma rel_bind : (forall₂ r ⇒ (r ⇒ forall₂ p) ⇒ forall₂ p) list.bind list.bind :=
lemma rel_bind : (forall₂ R ⇒ (R ⇒ forall₂ P) ⇒ forall₂ P) list.bind list.bind :=
λ a b h₁ f g h₂, rel_join (rel_map @h₂ h₁)

lemma rel_foldl : ((p ⇒ r ⇒ p) ⇒ p ⇒ forall₂ r ⇒ p) foldl foldl
lemma rel_foldl : ((P ⇒ R ⇒ P) ⇒ P ⇒ forall₂ R ⇒ P) foldl foldl
| f g hfg _ _ h _ _ forall₂.nil := h
| f g hfg x y hxy _ _ (forall₂.cons hab hs) := rel_foldl @hfg (hfg hxy hab) hs

lemma rel_foldr : ((r ⇒ p ⇒ p) ⇒ p ⇒ forall₂ r ⇒ p) foldr foldr
lemma rel_foldr : ((R ⇒ P ⇒ P) ⇒ P ⇒ forall₂ R ⇒ P) foldr foldr
| f g hfg _ _ h _ _ forall₂.nil := h
| f g hfg x y hxy _ _ (forall₂.cons hab hs) := hfg hab (rel_foldr @hfg hxy hs)

lemma rel_filter {p : α → Prop} {q : β → Prop} [decidable_pred p] [decidable_pred q]
(hpq : (r ⇒ (↔)) p q) :
(forall₂ r ⇒ forall₂ r) (filter p) (filter q)
(hpq : (R ⇒ (↔)) p q) :
(forall₂ R ⇒ forall₂ R) (filter p) (filter q)
| _ _ forall₂.nil := forall₂.nil
| (a :: as) (b :: bs) (forall₂.cons h₁ h₂) :=
begin
Expand All @@ -228,7 +228,7 @@ lemma rel_filter {p : α → Prop} {q : β → Prop} [decidable_pred p] [decidab
simp only [filter_cons_of_neg _ h, filter_cons_of_neg _ this, rel_filter h₂], },
end

lemma rel_filter_map : ((r ⇒ option.rel p) ⇒ forall₂ r ⇒ forall₂ p) filter_map filter_map
lemma rel_filter_map : ((R ⇒ option.rel P) ⇒ forall₂ R ⇒ forall₂ P) filter_map filter_map
| f g hfg _ _ forall₂.nil := forall₂.nil
| f g hfg (a :: as) (b :: bs) (forall₂.cons h₁ h₂) :=
by rw [filter_map_cons, filter_map_cons];
Expand All @@ -239,19 +239,19 @@ lemma rel_filter_map : ((r ⇒ option.rel p) ⇒ forall₂ r ⇒ forall₂ p) fi

@[to_additive]
lemma rel_prod [monoid α] [monoid β]
(h : r 1 1) (hf : (r ⇒ r ⇒ r) (*) (*)) : (forall₂ r ⇒ r) prod prod :=
(h : R 1 1) (hf : (R ⇒ R ⇒ R) (*) (*)) : (forall₂ R ⇒ R) prod prod :=
rel_foldl hf h

/-- Given a relation `r`, `sublist_forall₂ r l₁ l₂` indicates that there is a sublist of `l₂` such
/-- Given a relation `R`, `sublist_forall₂ r l₁ l₂` indicates that there is a sublist of `l₂` such
that `forall₂ r l₁ l₂`. -/
inductive sublist_forall₂ (r : α → β → Prop) : list α → list β → Prop
inductive sublist_forall₂ (R : α → β → Prop) : list α → list β → Prop
| nil {l} : sublist_forall₂ [] l
| cons {a₁ a₂ l₁ l₂} : r a₁ a₂ → sublist_forall₂ l₁ l₂ →
| cons {a₁ a₂ l₁ l₂} : R a₁ a₂ → sublist_forall₂ l₁ l₂ →
sublist_forall₂ (a₁ :: l₁) (a₂ :: l₂)
| cons_right {a l₁ l₂} : sublist_forall₂ l₁ l₂ → sublist_forall₂ l₁ (a :: l₂)

lemma sublist_forall₂_iff {l₁ : list α} {l₂ : list β} :
sublist_forall₂ r l₁ l₂ ↔ ∃ l, forall₂ r l₁ l ∧ l <+ l₂ :=
sublist_forall₂ R l₁ l₂ ↔ ∃ l, forall₂ R l₁ l ∧ l <+ l₂ :=
begin
split; intro h,
{ induction h with _ a b l1 l2 rab rll ih b l1 l2 hl ih,
Expand All @@ -270,14 +270,12 @@ begin
exact sublist_forall₂.cons hr (ih hl) } }
end

variable {ra : α → α → Prop}

instance sublist_forall₂.is_refl [is_refl α ra] :
is_refl (list α) (sublist_forall₂ ra) :=
instance sublist_forall₂.is_refl [is_refl α Rₐ] :
is_refl (list α) (sublist_forall₂ Rₐ) :=
⟨λ l, sublist_forall₂_iff.2 ⟨l, forall₂_refl l, sublist.refl l⟩⟩

instance sublist_forall₂.is_trans [is_trans α ra] :
is_trans (list α) (sublist_forall₂ ra) :=
instance sublist_forall₂.is_trans [is_trans α Rₐ] :
is_trans (list α) (sublist_forall₂ Rₐ) :=
⟨λ a b c, begin
revert a b,
induction c with _ _ ih,
Expand All @@ -294,12 +292,12 @@ instance sublist_forall₂.is_trans [is_trans α ra] :
{ exact sublist_forall₂.cons_right (ih _ _ h1 btc), } }
end⟩

lemma sublist.sublist_forall₂ {l₁ l₂ : list α} (h : l₁ <+ l₂) (r : α → α → Prop) [is_refl α r] :
sublist_forall₂ r l₁ l₂ :=
lemma sublist.sublist_forall₂ {l₁ l₂ : list α} (h : l₁ <+ l₂) [is_refl α Rₐ] :
sublist_forall₂ Rₐ l₁ l₂ :=
sublist_forall₂_iff.2 ⟨l₁, forall₂_refl l₁, h⟩

lemma tail_sublist_forall₂_self [is_refl α ra] (l : list α) :
sublist_forall₂ ra l.tail l :=
l.tail_sublist.sublist_forall₂ ra
lemma tail_sublist_forall₂_self [is_refl α Rₐ] (l : list α) :
sublist_forall₂ Rₐ l.tail l :=
l.tail_sublist.sublist_forall₂

end list

0 comments on commit d6789b8

Please sign in to comment.