Dependent casts

This file contains type classes for dependent or custom cast operations

This allows us to state theorems with more refined casts, without which we cannot make progress in proving them

theorem cast_eq_cast_iff {α β γ : Sort u} {h : α = γ} {h' : β = γ} {a : α} {b : β} : cast h a = cast h' b ↔ a = cast ⋯ b

theorem cast_symm {α β : Sort u} {h : α = β} {a : α} {b : β} : cast h a = b ↔ a = cast ⋯ b

theorem congrArg₃ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {f : α → β → γ → δ} {a a' : α} {b b' : β} {c c' : γ} (h : a = a') (h' : b = b') (h'' : c = c') : f a b c = f a' b' c'

theorem congrArg₄ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} {ε : Sort u_5} {f : α → β → γ → δ → ε} {a a' : α} {b b' : β} {c c' : γ} {d d' : δ} (h : a = a') (h' : b = b') (h'' : c = c') (h''' : d = d') : f a b c d = f a' b' c' d'

class DCast (α : Sort u_1) (β : α → Sort u_2) : Sort (max (max 1 u_1) u_2)

DCast is a type class for custom cast operations on an indexed type family β a

We require the cast operation dcast, along with the property that dcast reduces to id under reflexivity.

• dcast {a a' : α} : a = a' → β a → β a'
• dcast_id {a : α} : dcast ⋯ = id

@[implicit_reducible, instance 100]

instance instDCast {α : Sort u_1} {β : α → Sort u_2} : DCast α β

The default instance for DCast

@[simp]

theorem dcast_eq {α : Sort u_1} {β : α → Sort u_2} [DCast α β] {a : α} {b : β a} : dcast ⋯ b = b

theorem dcast_symm {α : Sort u_1} {β : α → Sort u_2} [DCast α β] {a a' : α} {b : β a} {b' : β a'} (ha : a = a') (hb : dcast ha b = b') : dcast ⋯ b' = b

@[simp]

theorem dcast_trans {α : Sort u_1} {β : α → Sort u_2} [DCast α β] {a a' a'' : α} {b : β a} (h : a = a') (h' : a' = a'') : dcast h' (dcast h b) = dcast ⋯ b

theorem dcast_eq_dcast_iff {α : Sort u_1} {β : α → Sort u_2} [DCast α β] {a a' a'' : α} {b : β a} {b' : β a'} (h : a = a'') (h' : a' = a'') : dcast h b = dcast h' b' ↔ b = dcast ⋯ b'

theorem heq_of_dcast {α : Sort u_1} {β : α → Sort u_2} [DCast α β] {a a' : α} {b : β a} {b' : β a'} (ha : a = a') (hb : dcast ha b = b') : b ≍ b'

theorem dcast_fun {α : Sort u_1} {β : α → Sort u_2} [DCast α β] {a : α} {b : β a} {γ : (a : α) → β a → Sort u_3} {f : (b : β a) → γ a b} : f (dcast ⋯ b) = dcast ⋯ (f b)

theorem dcast_fun₂ {α : Sort u_1} {β : α → Sort u_2} [DCast α β] {a₁ a₂ a₁' a₂' : α} {h₁ : a₁ = a₁'} {h₂ : a₂ = a₂'} {f : α → α → α} {g : (a₁ a₂ : α) → β a₁ → β a₂ → β (f a₁ a₂)} {b₁ : β a₁} {b₂ : β a₂} : dcast ⋯ (g a₁ a₂ b₁ b₂) = g a₁' a₂' (dcast h₁ b₁) (dcast h₂ b₂)

theorem dcast_eq_root_cast {α : Sort u_1} {β : α → Sort u_2} [DCast α β] {a a' : α} {b : β a} (h : a = a') : dcast h b = cast ⋯ b

class DCast₂ (α : Sort u_1) (β : α → Sort u_2) (γ : (a : α) → β a → Sort u_3) [DCast α β] : Sort (max (max (max 1 u_1) u_2) u_3)

DCast₂ is a type class for custom cast operations on a doubly-indexed type family γ a b, given an underlying dependent cast DCast α β

We require the cast operation dcast₂, along with the property that dcast₂ reduces to id under reflexivity.

• dcast₂ {a a' : α} {b : β a} {b' : β a'} (ha : a = a') : dcast ha b = b' → γ a b → γ a' b'
• dcast₂_id {a : α} {b : β a} : dcast₂ ⋯ ⋯ = id

@[implicit_reducible, instance 100]

instance instDCast₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] : DCast₂ α β γ

Default instance for DCast₂

@[simp]

theorem dcast₂_eq {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] {a : α} {b : β a} {c : γ a b} : dcast₂ ⋯ ⋯ c = c

@[simp]

theorem dcast₂_eq' {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] {a : α} {b : β a} {c : γ a b} (h : a = a) (h' : dcast h b = b) : dcast₂ h h' c = c

theorem dcast₂_symm {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] {a a' : α} {b : β a} {b' : β a'} {c : γ a b} {c' : γ a' b'} (ha : a = a') (hb : dcast ha b = b') (hc : dcast₂ ha hb c = c') : dcast₂ ⋯ ⋯ c' = c

@[simp]

theorem dcast₂_trans {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] {a a' a'' : α} {b : β a} {b' : β a'} {b'' : β a''} {c : γ a b} (ha : a = a') (ha' : a' = a'') (hb : dcast ha b = b') (hb' : dcast ha' b' = b'') : dcast₂ ha' hb' (dcast₂ ha hb c) = dcast₂ ⋯ ⋯ c

theorem dcast₂_eq_dcast₂_iff {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] {a a' a'' : α} {b : β a} {b' : β a'} {b'' : β a''} {c : γ a b} {c' : γ a' b'} (ha : a = a'') (ha' : a' = a'') (hb : dcast ha b = b'') (hb' : dcast ha' b' = b'') : dcast₂ ha hb c = dcast₂ ha' hb' c' ↔ c = dcast₂ ⋯ ⋯ c'

theorem dcast₂_dcast {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] {a : α} {b : β a} {c : γ a b} : dcast₂ ⋯ ⋯ c = dcast ⋯ c

@[implicit_reducible]

instance instDCast₁₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] {a : α} : DCast (β a) (γ a)

@[implicit_reducible]

instance instDCastPSigma {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] : DCast ((a : α) ×' β a) fun (a : (a : α) ×' β a) => γ a.fst a.snd

@[implicit_reducible]

instance instDCastSigma {α : Type u_4} {β : α → Type u_5} {γ : (a : α) → β a → Type u_6} [DCast α β] [DCast₂ α β γ] : DCast ((a : α) × β a) fun (a : (a : α) × β a) => γ a.fst a.snd

@[implicit_reducible]

instance instDCastForall {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} [DCast α β] [DCast₂ α β γ] : DCast α fun (a : α) => (b : β a) → γ a b

class DCast₃ (α : Sort u_1) (β : α → Sort u_2) (γ : (a : α) → β a → Sort u_3) (δ : (a : α) → (b : β a) → γ a b → Sort u_4) [DCast α β] [DCast₂ α β γ] : Sort (max (max (max (max 1 u_1) u_2) u_3) u_4)

DCast₃ is a type class for custom cast operations on a triply-indexed type family δ a b c, given underlying dependent casts DCast α β and DCast₂ α β γ

We require the cast operation dcast₃, along with the property that dcast₃ reduces to id under reflexivity.

• dcast₃ {a a' : α} {b : β a} {b' : β a'} {c : γ a b} {c' : γ a' b'} (ha : a = a') (hb : dcast ha b = b') (hc : dcast₂ ha hb c = c') : δ a b c → δ a' b' c'
• dcast₃_id {a : α} {b : β a} {c : γ a b} : dcast₃ ⋯ ⋯ ⋯ = id

@[implicit_reducible, instance 100]

instance instDCast₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] : DCast₃ α β γ δ

Default instance for DCast₃

@[simp]

theorem dcast₃_eq {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] {a : α} {b : β a} {c : γ a b} {d : δ a b c} : dcast₃ ⋯ ⋯ ⋯ d = d

theorem dcast₃_symm {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] {a a' : α} {b : β a} {b' : β a'} {c : γ a b} {c' : γ a' b'} {d : δ a b c} {d' : δ a' b' c'} (ha : a = a') (hb : dcast ha b = b') (hc : dcast₂ ha hb c = c') (hd : dcast₃ ha hb hc d = d') : dcast₃ ⋯ ⋯ ⋯ d' = d

@[simp]

theorem dcast₃_trans {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] {a a' a'' : α} {b : β a} {b' : β a'} {b'' : β a''} {c : γ a b} {c' : γ a' b'} {c'' : γ a'' b''} {d : δ a b c} (ha : a = a') (ha' : a' = a'') (hb : dcast ha b = b') (hb' : dcast ha' b' = b'') (hc : dcast₂ ha hb c = c') (hc' : dcast₂ ha' hb' c' = c'') : dcast₃ ha' hb' hc' (dcast₃ ha hb hc d) = dcast₃ ⋯ ⋯ ⋯ d

theorem dcast₃_eq_dcast₃_iff {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] {a a' : α} {b : β a} {b' : β a'} {c : γ a b} {c' : γ a' b'} {d : δ a b c} {d' : δ a' b' c'} (ha : a = a') (hb : dcast ha b = b') (hc : dcast₂ ha hb c = c') : dcast₃ ha hb hc d = d' ↔ d = dcast₃ ⋯ ⋯ ⋯ d'

theorem dcast₃_dcast₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] {a : α} {b : β a} {c : γ a b} {d : δ a b c} : dcast₃ ⋯ ⋯ ⋯ d = dcast₂ ⋯ ⋯ d

@[implicit_reducible]

instance instDCast₂₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] {a : α} : DCast₂ (β a) (γ a) (δ a)

@[implicit_reducible]

instance instDCast₁₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] {a : α} {b : β a} : DCast (γ a b) (δ a b)

@[implicit_reducible]

instance instDCast₂PSigma {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] : DCast₂ ((a : α) ×' β a) (fun (a : (a : α) ×' β a) => γ a.fst a.snd) fun (a : (a : α) ×' β a) => δ a.fst a.snd

@[implicit_reducible]

instance instDCast₂Sigma {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} {δ : (a : α) → (b : β a) → γ a b → Type u_8} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] : DCast₂ ((a : α) × β a) (fun (a : (a : α) × β a) => γ a.fst a.snd) fun (a : (a : α) × β a) => δ a.fst a.snd

@[implicit_reducible]

instance instDCast₂Forall {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] : DCast₂ α (fun (a : α) => (b : β a) → γ a b) fun (a : α) (f : (b : β a) → γ a b) => (b : β a) → δ a b (f b)

@[implicit_reducible]

instance instDCastPSigmaPSigma {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] : DCast ((a : α) ×' (b : β a) ×' γ a b) fun (a : (a : α) ×' (b : β a) ×' γ a b) => δ a.fst a.snd.fst a.snd.snd

@[implicit_reducible]

instance instDCastSigmaSigma {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} {δ : (a : α) → (b : β a) → γ a b → Type u_8} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] : DCast ((a : α) × (b : β a) × γ a b) fun (a : (a : α) × (b : β a) × γ a b) => δ a.fst a.snd.fst a.snd.snd

@[implicit_reducible]

instance instDCastForallForall {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] : DCast α fun (a : α) => (b : β a) → (c : γ a b) → δ a b c

@[implicit_reducible]

instance instDCastPSigmaForall {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] : DCast ((a : α) ×' β a) fun (ab : (a : α) ×' β a) => (c : γ ab.fst ab.snd) → δ ab.fst ab.snd c

@[implicit_reducible]

instance instDCastSigmaForallForall {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} {δ : (a : α) → (b : β a) → γ a b → Type u_8} [DCast α β] [DCast₂ α β γ] [DCast₃ α β γ δ] : DCast ((a : α) × β a) fun (ab : (a : α) × β a) => (c : γ ab.fst ab.snd) → δ ab.fst ab.snd c

@[implicit_reducible]

instance Fin.instDCast : DCast ℕ Fin

Fin.cast as a DCast (which should override the default instance).

theorem Fin.cast_eq_dcast {m n : ℕ} (h : m = n) (a : Fin m) : Fin.cast h a = dcast h a