From a35ba44197f00a9fe431d75990d2ea206a435036 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 9 Dec 2025 12:53:50 +0000 Subject: [PATCH] chore: post-stage0 update fixes --- src/Init/Core.lean | 10 +++----- src/Init/Data/Array/DecidableEq.lean | 10 ++++---- src/Init/Data/List/Basic.lean | 6 ++--- src/Init/Data/List/BasicAux.lean | 2 +- src/Init/Data/Option/Basic.lean | 10 ++++---- src/Init/Data/Option/Instances.lean | 6 ++--- src/Init/Prelude.lean | 26 +++++++++++--------- tests/lean/run/6123_mod_cast.lean | 2 +- tests/lean/run/concatElim.lean | 8 +++--- tests/lean/run/hinj_thm.lean | 15 ++++++++--- tests/lean/run/issue11450.lean | 10 ++++---- tests/lean/run/issue11560.lean | 2 +- tests/lean/run/linearNoConfusion.lean | 21 ++++++++-------- tests/lean/run/listDecEq.lean | 8 +++--- tests/lean/run/noConfusionCtorInjection.lean | 6 ++--- 15 files changed, 75 insertions(+), 67 deletions(-) diff --git a/src/Init/Core.lean b/src/Init/Core.lean index edd95ec580..919797cdc5 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -939,9 +939,7 @@ theorem HEq.subst {p : (T : Sort u) → T → Prop} (h₁ : a ≍ b) (h₂ : p @[symm] theorem HEq.symm (h : a ≍ b) : b ≍ a := h.rec (HEq.refl a) -/-- Propositionally equal terms are also heterogeneously equal. -/ -theorem heq_of_eq (h : a = a') : a ≍ a' := - Eq.subst h (HEq.refl a) + /-- Heterogeneous equality is transitive. -/ theorem HEq.trans (h₁ : a ≍ b) (h₂ : b ≍ c) : a ≍ c := @@ -1370,7 +1368,7 @@ instance {α : Type u} {p : α → Prop} [BEq α] [LawfulBEq α] : LawfulBEq {x instance {α : Sort u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} := fun ⟨a, h₁⟩ ⟨b, h₂⟩ => if h : a = b then isTrue (by subst h; exact rfl) - else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h)) + else isFalse (fun h' => Subtype.noConfusion rfl .rfl (heq_of_eq h') (fun h' => absurd (eq_of_heq h') h)) end Subtype @@ -1429,8 +1427,8 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) := | isTrue e₁ => match decEq b b' with | isTrue e₂ => isTrue (e₁ ▸ e₂ ▸ rfl) - | isFalse n₂ => isFalse fun h => Prod.noConfusion h fun _ e₂' => absurd e₂' n₂ - | isFalse n₁ => isFalse fun h => Prod.noConfusion h fun e₁' _ => absurd e₁' n₁ + | isFalse n₂ => isFalse fun h => Prod.noConfusion rfl rfl (heq_of_eq h) fun _ e₂' => absurd (eq_of_heq e₂') n₂ + | isFalse n₁ => isFalse fun h => Prod.noConfusion rfl rfl (heq_of_eq h) fun e₁' _ => absurd (eq_of_heq e₁') n₁ instance [BEq α] [BEq β] : BEq (α × β) where beq := fun (a₁, b₁) (a₂, b₂) => a₁ == a₂ && b₁ == b₂ diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean index 9d5f866e01..066cdeace6 100644 --- a/src/Init/Data/Array/DecidableEq.lean +++ b/src/Init/Data/Array/DecidableEq.lean @@ -99,23 +99,23 @@ instance instDecidableEq [DecidableEq α] : DecidableEq (Array α) := fun xs ys | ⟨[]⟩ => match ys with | ⟨[]⟩ => isTrue rfl - | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·)) + | ⟨_ :: _⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h)) | ⟨a :: as⟩ => match ys with - | ⟨[]⟩ => isFalse (Array.noConfusion · (List.noConfusion ·)) + | ⟨[]⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h)) | ⟨b :: bs⟩ => instDecidableEqImpl ⟨a :: as⟩ ⟨b :: bs⟩ @[csimp] theorem instDecidableEq_csimp : @instDecidableEq = @instDecidableEqImpl := Subsingleton.allEq _ _ - + /-- Equality with `#[]` is decidable even if the underlying type does not have decidable equality. -/ instance instDecidableEqEmp (xs : Array α) : Decidable (xs = #[]) := match xs with | ⟨[]⟩ => isTrue rfl - | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·)) + | ⟨_ :: _⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h)) /-- Equality with `#[]` is decidable even if the underlying type does not have decidable equality. @@ -123,7 +123,7 @@ Equality with `#[]` is decidable even if the underlying type does not have decid instance instDecidableEmpEq (ys : Array α) : Decidable (#[] = ys) := match ys with | ⟨[]⟩ => isTrue rfl - | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·)) + | ⟨_ :: _⟩ => isFalse (fun h => Array.noConfusion rfl (heq_of_eq h) (fun h => List.noConfusion rfl h)) theorem beq_eq_decide [BEq α] (xs ys : Array α) : (xs == ys) = if h : xs.size = ys.size then diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index a13b64d17e..8e830152a8 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -301,7 +301,7 @@ Examples: def getLast : ∀ (as : List α), as ≠ [] → α | [], h => absurd rfl h | [a], _ => a - | _::b::as, _ => getLast (b::as) (fun h => List.noConfusion h) + | _::b::as, _ => getLast (b::as) (fun h => List.noConfusion rfl (heq_of_eq h)) /-! ### getLast? -/ @@ -318,7 +318,7 @@ Examples: -/ def getLast? : List α → Option α | [] => none - | a::as => some (getLast (a::as) (fun h => List.noConfusion h)) + | a::as => some (getLast (a::as) (fun h => List.noConfusion rfl (heq_of_eq h))) @[simp, grind =] theorem getLast?_nil : @getLast? α [] = none := rfl @@ -337,7 +337,7 @@ Examples: -/ def getLastD : (as : List α) → (fallback : α) → α | [], a₀ => a₀ - | a::as, _ => getLast (a::as) (fun h => List.noConfusion h) + | a::as, _ => getLast (a::as) (fun h => List.noConfusion rfl (heq_of_eq h)) -- These aren't `simp` lemmas since we always simplify `getLastD` in terms of `getLast?`. theorem getLastD_nil {a : α} : getLastD [] a = a := rfl diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index 7cf062540c..123f322713 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -57,7 +57,7 @@ Examples: @[expose] def getLast! [Inhabited α] : List α → α | [] => panic! "empty list" - | a::as => getLast (a::as) (fun h => List.noConfusion h) + | a::as => getLast (a::as) (fun h => List.noConfusion rfl (heq_of_eq h)) /-! ## Head and tail -/ diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index 8fa868d612..cc6d296dd7 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -22,12 +22,12 @@ instance instDecidableEq {α} [inst : DecidableEq α] : DecidableEq (Option α) match a with | none => match b with | none => .isTrue rfl - | some _ => .isFalse Option.noConfusion + | some _ => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h)) | some a => match b with - | none => .isFalse Option.noConfusion + | none => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h)) | some b => match inst a b with | .isTrue h => .isTrue (h ▸ rfl) - | .isFalse n => .isFalse (Option.noConfusion · n) + | .isFalse n => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h) (fun h' => absurd (eq_of_heq h') n)) /-- Equality with `none` is decidable even if the wrapped type does not have decidable equality. @@ -37,7 +37,7 @@ instance decidableEqNone (o : Option α) : Decidable (o = none) := compatibility with the `DecidableEq` instance. -/ match o with | none => .isTrue rfl - | some _ => .isFalse Option.noConfusion + | some _ => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h)) /-- Equality with `none` is decidable even if the wrapped type does not have decidable equality. @@ -47,7 +47,7 @@ instance decidableNoneEq (o : Option α) : Decidable (none = o) := compatibility with the `DecidableEq` instance. -/ match o with | none => .isTrue rfl - | some _ => .isFalse Option.noConfusion + | some _ => .isFalse (fun h => Option.noConfusion rfl (heq_of_eq h)) deriving instance BEq for Option diff --git a/src/Init/Data/Option/Instances.lean b/src/Init/Data/Option/Instances.lean index c792f12d04..178afe4940 100644 --- a/src/Init/Data/Option/Instances.lean +++ b/src/Init/Data/Option/Instances.lean @@ -16,9 +16,9 @@ namespace Option theorem eq_of_eq_some {α : Type u} : ∀ {x y : Option α}, (∀ z, x = some z ↔ y = some z) → x = y | none, none, _ => rfl - | none, some z, h => Option.noConfusion ((h z).2 rfl) - | some z, none, h => Option.noConfusion ((h z).1 rfl) - | some _, some w, h => Option.noConfusion ((h w).2 rfl) (congrArg some) + | none, some z, h => Option.noConfusion rfl (heq_of_eq ((h z).2 rfl)) + | some z, none, h => Option.noConfusion rfl (heq_of_eq ((h z).1 rfl)) + | some _, some w, h => Option.noConfusion rfl (heq_of_eq ((h w).2 rfl)) (fun h => congrArg some (eq_of_heq h)) theorem eq_none_of_isNone {α : Type u} : ∀ {o : Option α}, o.isNone → o = none | none, _ => rfl diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 807f073e14..b24b98489b 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -496,6 +496,10 @@ theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' := h₁.rec (fun _ => rfl) this α α a a' h rfl +/-- Propositionally equal terms are also heterogeneously equal. -/ +theorem heq_of_eq (h : Eq a a') : HEq a a' := + Eq.subst h (HEq.refl a) + /-- The product type, usually written `α × β`. Product types are also called pair or tuple types. Elements of this type are pairs in which the first element is an `α` and the second element is a @@ -2330,7 +2334,7 @@ def BitVec.decEq (x y : BitVec w) : Decidable (Eq x y) := | ⟨n⟩, ⟨m⟩ => dite (Eq n m) (fun h => isTrue (h ▸ rfl)) - (fun h => isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h))) + (fun h => isFalse (fun h' => BitVec.noConfusion rfl (heq_of_eq h') (fun h' => absurd (eq_of_heq h') h))) instance : DecidableEq (BitVec w) := BitVec.decEq @@ -2921,15 +2925,15 @@ instance {α} : Inhabited (List α) where /-- Implements decidable equality for `List α`, assuming `α` has decidable equality. -/ protected def List.hasDecEq {α : Type u} [DecidableEq α] : (a b : List α) → Decidable (Eq a b) | nil, nil => isTrue rfl - | cons _ _, nil => isFalse (fun h => List.noConfusion h) - | nil, cons _ _ => isFalse (fun h => List.noConfusion h) + | cons _ _, nil => isFalse (fun h => List.noConfusion rfl (heq_of_eq h)) + | nil, cons _ _ => isFalse (fun h => List.noConfusion rfl (heq_of_eq h)) | cons a as, cons b bs => match decEq a b with | isTrue hab => match List.hasDecEq as bs with | isTrue habs => isTrue (hab ▸ habs ▸ rfl) - | isFalse nabs => isFalse (fun h => List.noConfusion h (fun _ habs => absurd habs nabs)) - | isFalse nab => isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab)) + | isFalse nabs => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun _ habs => absurd (eq_of_heq habs) nabs)) + | isFalse nab => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun hab _ => absurd (eq_of_heq hab) nab)) instance {α : Type u} [DecidableEq α] : DecidableEq (List α) := fun xs ys => /- @@ -2939,16 +2943,16 @@ instance {α : Type u} [DecidableEq α] : DecidableEq (List α) := fun xs ys => match xs with | .nil => match ys with | .nil => isTrue rfl - | .cons _ _ => isFalse List.noConfusion + | .cons _ _ => isFalse (fun h => List.noConfusion rfl (heq_of_eq h)) | .cons a as => match ys with - | .nil => isFalse List.noConfusion + | .nil => isFalse (fun h => List.noConfusion rfl (heq_of_eq h)) | .cons b bs => match decEq a b with | isTrue hab => match List.hasDecEq as bs with | isTrue habs => isTrue (hab ▸ habs ▸ rfl) - | isFalse nabs => isFalse (List.noConfusion · (fun _ habs => absurd habs nabs)) - | isFalse nab => isFalse (List.noConfusion · (fun hab _ => absurd hab nab)) + | isFalse nabs => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun _ habs => absurd (eq_of_heq habs) nabs)) + | isFalse nab => isFalse (fun h => List.noConfusion rfl (heq_of_eq h) (fun hab _ => absurd (eq_of_heq hab) nab)) /-- Equality with `List.nil` is decidable even if the underlying type does not have decidable equality. @@ -2956,7 +2960,7 @@ Equality with `List.nil` is decidable even if the underlying type does not have instance List.instDecidableNilEq (a : List α) : Decidable (Eq List.nil a) := match a with | .nil => isTrue rfl - | .cons _ _ => isFalse List.noConfusion + | .cons _ _ => isFalse (fun h => List.noConfusion rfl (heq_of_eq h)) /-- Equality with `List.nil` is decidable even if the underlying type does not have decidable equality. @@ -2964,7 +2968,7 @@ Equality with `List.nil` is decidable even if the underlying type does not have instance List.instDecidableEqNil (a : List α) : Decidable (Eq a List.nil) := match a with | .nil => isTrue rfl - | .cons _ _ => isFalse List.noConfusion + | .cons _ _ => isFalse (fun h => List.noConfusion rfl (heq_of_eq h)) /-- The length of a list. diff --git a/tests/lean/run/6123_mod_cast.lean b/tests/lean/run/6123_mod_cast.lean index 4bfa0cc372..4c3e871f56 100644 --- a/tests/lean/run/6123_mod_cast.lean +++ b/tests/lean/run/6123_mod_cast.lean @@ -142,7 +142,7 @@ theorem coe_le_coe : (a : WithBot α) ≤ b ↔ a ≤ b := by simp [LE.le] instance orderBot : OrderBot (WithBot α) where - bot_le _ := fun _ h => Option.noConfusion h + bot_le _ := fun _ h => Option.noConfusion rfl (heq_of_eq h) theorem le_coe_iff : ∀ {x : WithBot α}, x ≤ b ↔ ∀ a : α, x = ↑a → a ≤ b | (b : α) => by simp diff --git a/tests/lean/run/concatElim.lean b/tests/lean/run/concatElim.lean index f597d8fbaf..8e1c1315b7 100644 --- a/tests/lean/run/concatElim.lean +++ b/tests/lean/run/concatElim.lean @@ -20,7 +20,7 @@ theorem concatEq (xs : List α) (h : xs ≠ []) : concat (dropLast xs) (last xs match xs, h with | [], h => contradiction | [x], h => rfl - | x₁::x₂::xs, h => simp [concat, dropLast, last, concatEq (x₂::xs) List.noConfusion] + | x₁::x₂::xs, h => simp [concat, dropLast, last, concatEq (x₂::xs)] theorem lengthCons {α} (x : α) (xs : List α) : (x::xs).length = xs.length + 1 := rfl @@ -42,11 +42,11 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro intro n h cases n with | zero => - simp [lengthCons] at h + simp at h | succ n => - have : (x₁ :: x₂ :: xs).length = xs.length + 2 := by simp [lengthCons] + have : (x₁ :: x₂ :: xs).length = xs.length + 2 := by simp have : xs.length = n := by rw [this] at h; injection h with h; injection h - simp [dropLast, lengthCons, dropLastLen (x₂::xs) xs.length (lengthCons ..), this] + simp [dropLast, dropLastLen (x₂::xs) xs.length (lengthCons ..), this] @[inline] def concatElim {α} diff --git a/tests/lean/run/hinj_thm.lean b/tests/lean/run/hinj_thm.lean index d888946490..c1db7ce0cb 100644 --- a/tests/lean/run/hinj_thm.lean +++ b/tests/lean/run/hinj_thm.lean @@ -8,15 +8,22 @@ inductive Foo' (α β : Type u) : (n : Nat) → P n -> Type u | odd (b : β) (n : Nat) (v : T n) : Foo' α β (Nat.succ (double n)) (pax _) /-- -info: Foo'.even.hinj.{u} {α β : Type u} {a : α} {n : Nat} {v : T n} {h : P n} {a✝ : α} {n✝ : Nat} {v✝ : T n✝} {h✝ : P n✝} : - double n = double n✝ → ⋯ ≍ ⋯ → Foo'.even a n v h ≍ Foo'.even a✝ n✝ v✝ h✝ → a = a✝ ∧ n = n✝ ∧ v ≍ v✝ +info: Foo'.even.hinj.{u} {α β : Type u} {a : α} {n : Nat} {v : T n} {h : P n} {α✝ β✝ : Type u} {a✝ : α✝} {n✝ : Nat} + {v✝ : T n✝} {h✝ : P n✝} : + α = α✝ → + β = β✝ → + double n = double n✝ → + ⋯ ≍ ⋯ → Foo'.even a n v h ≍ Foo'.even a✝ n✝ v✝ h✝ → α = α✝ ∧ β = β✝ ∧ a ≍ a✝ ∧ n = n✝ ∧ v ≍ v✝ -/ #guard_msgs in #check Foo'.even.hinj /-- -info: Foo'.odd.hinj.{u} {α β : Type u} {b : β} {n : Nat} {v : T n} {b✝ : β} {n✝ : Nat} {v✝ : T n✝} : - (double n).succ = (double n✝).succ → ⋯ ≍ ⋯ → Foo'.odd b n v ≍ Foo'.odd b✝ n✝ v✝ → b = b✝ ∧ n = n✝ ∧ v ≍ v✝ +info: Foo'.odd.hinj.{u} {α β : Type u} {b : β} {n : Nat} {v : T n} {α✝ β✝ : Type u} {b✝ : β✝} {n✝ : Nat} {v✝ : T n✝} : + α = α✝ → + β = β✝ → + (double n).succ = (double n✝).succ → + ⋯ ≍ ⋯ → Foo'.odd b n v ≍ Foo'.odd b✝ n✝ v✝ → α = α✝ ∧ β = β✝ ∧ b ≍ b✝ ∧ n = n✝ ∧ v ≍ v✝ -/ #guard_msgs in #check Foo'.odd.hinj diff --git a/tests/lean/run/issue11450.lean b/tests/lean/run/issue11450.lean index 29f1c681c0..85131ed22d 100644 --- a/tests/lean/run/issue11450.lean +++ b/tests/lean/run/issue11450.lean @@ -17,7 +17,7 @@ inductive Term (L: Nat → Type) (n : Nat) : Nat → Type _ /-- info: @[reducible] def Term.var.noConfusion.{u} : {L : Nat → Type} → - {n : Nat} → {P : Sort u} → {k k' : Fin n} → Term.var k = Term.var k' → (k = k' → P) → P + {n : Nat} → {P : Sort u} → {k k' : Fin n} → Term.var k = Term.var k' → (k ≍ k' → P) → P -/ #guard_msgs in #print sig Term.var.noConfusion @@ -44,7 +44,7 @@ inductive Vec (α : Type u) : Nat → Type u where /-- info: Vec.cons.noConfusion.{u_1, u} {α : Type u} {P : Sort u_1} {n : Nat} {x : α} {xs : Vec α n} {n' : Nat} {x' : α} {xs' : Vec α n'} (eq_1 : n + 1 = n' + 1) (eq_2 : Vec.cons x xs ≍ Vec.cons x' xs') - (k : n = n' → x = x' → xs ≍ xs' → P) : P + (k : n = n' → x ≍ x' → xs ≍ xs' → P) : P -/ #guard_msgs in #check Vec.cons.noConfusion @@ -60,11 +60,11 @@ theorem Vec.cons.hinj' {α : Type u} {x : α} {n : Nat} {xs : Vec α n} {x' : α} {n' : Nat} {xs' : Vec α n'} : Vec.cons x xs ≍ Vec.cons x' xs' → (n + 1 = n' + 1 → (x = x' ∧ xs ≍ xs')) := by intro h eq_1 - apply Vec.cons.noConfusion eq_1 h (fun _ eq_x eq_xs => ⟨eq_x, eq_xs⟩) + apply Vec.cons.noConfusion eq_1 h (fun _ eq_x eq_xs => ⟨eq_of_heq eq_x, eq_xs⟩) /-- -info: Vec.cons.hinj.{u} {α : Type u} {n : Nat} {x : α} {xs : Vec α n} {n✝ : Nat} {x✝ : α} {xs✝ : Vec α n✝} : - n + 1 = n✝ + 1 → Vec.cons x xs ≍ Vec.cons x✝ xs✝ → n = n✝ ∧ x = x✝ ∧ xs ≍ xs✝ +info: Vec.cons.hinj.{u} {α : Type u} {n : Nat} {x : α} {xs : Vec α n} {α✝ : Type u} {n✝ : Nat} {x✝ : α✝} {xs✝ : Vec α✝ n✝} : + α = α✝ → n + 1 = n✝ + 1 → Vec.cons x xs ≍ Vec.cons x✝ xs✝ → α = α✝ ∧ n = n✝ ∧ x ≍ x✝ ∧ xs ≍ xs✝ -/ #guard_msgs in #check Vec.cons.hinj diff --git a/tests/lean/run/issue11560.lean b/tests/lean/run/issue11560.lean index 600e7f557d..f94067de97 100644 --- a/tests/lean/run/issue11560.lean +++ b/tests/lean/run/issue11560.lean @@ -9,7 +9,7 @@ example (h2 : d.succ < b) (hab : a = b) (hcd : @Fin'.mk a c.succ h1 ≍ @Fin'.mk b d.succ h2) : - c = d := Fin'.mk.noConfusion hab hcd (fun h => Nat.succ.noConfusion h fun h' => h') + c = d := Fin'.noConfusion hab hcd (fun h => Nat.succ.noConfusion h fun h' => h') example (a b c d : Nat) diff --git a/tests/lean/run/linearNoConfusion.lean b/tests/lean/run/linearNoConfusion.lean index 16a24b73f0..086c5a9683 100644 --- a/tests/lean/run/linearNoConfusion.lean +++ b/tests/lean/run/linearNoConfusion.lean @@ -20,30 +20,31 @@ inductive Vec.{u} (α : Type) : Nat → Type u where | cons1 {n} : α → Vec α n → Vec α (n + 1) | cons2 {n} : α → Vec α n → Vec α (n + 1) -@[reducible] protected def Vec.noConfusionType'.{u_1, u} : {α : Type} → - Sort u_1 → {a : Nat} → Vec.{u} α a → {a : Nat} → Vec α a → Sort u_1 := -fun P _ x1 _ x2 => +@[reducible] protected def Vec.noConfusionType'.{u_1, u} : Sort u_1 → + {α : Type} → {a : Nat} → Vec.{u} α a → + {α : Type} → {a : Nat} → Vec α a → Sort u_1 := +fun P _ _ x1 _ _ x2 => Vec.casesOn x1 (if h : x2.ctorIdx = 0 then Vec.nil.elim (motive := fun _ _ => Sort u_1) x2 h (P → P) else P) (fun {n} a_1 a_2 => if h : x2.ctorIdx = 1 then - Vec.cons1.elim (motive := fun _ _ => Sort u_1) x2 h fun {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P + Vec.cons1.elim (motive := fun _ _ => Sort u_1) x2 h fun {n_1} a a_3 => (n = n_1 → a_1 ≍ a → a_2 ≍ a_3 → P) → P else P) (fun {n} a_1 a_2 => if h : x2.ctorIdx = 2 then - Vec.cons2.elim (motive := fun _ _ => Sort u_1) x2 h fun {n_1} a a_3 => (n = n_1 → a_1 = a → a_2 ≍ a_3 → P) → P + Vec.cons2.elim (motive := fun _ _ => Sort u_1) x2 h fun {n_1} a a_3 => (n = n_1 → a_1 ≍ a → a_2 ≍ a_3 → P) → P else P) /-- -info: @[reducible] protected def Vec.noConfusionType.{u_1, u} : {α : Type} → - Sort u_1 → {a : Nat} → Vec α a → {a' : Nat} → Vec α a' → Sort u_1 := -fun {α} P {a} t {a'} t' => +info: @[reducible] protected def Vec.noConfusionType.{u_1, u} : Sort u_1 → + {α : Type} → {a : Nat} → Vec α a → {α' : Type} → {a' : Nat} → Vec α' a' → Sort u_1 := +fun P {α} {a} t {α'} {a'} t' => Vec.casesOn t (if h : t'.ctorIdx = 0 then Vec.nil.elim t' h (P → P) else P) (fun {n} a a_1 => - if h : t'.ctorIdx = 1 then Vec.cons1.elim t' h fun {n_1} a_2 a_3 => (n = n_1 → a = a_2 → a_1 ≍ a_3 → P) → P + if h : t'.ctorIdx = 1 then Vec.cons1.elim t' h fun {n_1} a_2 a_3 => (n = n_1 → a ≍ a_2 → a_1 ≍ a_3 → P) → P else P) fun {n} a a_1 => - if h : t'.ctorIdx = 2 then Vec.cons2.elim t' h fun {n_1} a_2 a_3 => (n = n_1 → a = a_2 → a_1 ≍ a_3 → P) → P else P + if h : t'.ctorIdx = 2 then Vec.cons2.elim t' h fun {n_1} a_2 a_3 => (n = n_1 → a ≍ a_2 → a_1 ≍ a_3 → P) → P else P -/ #guard_msgs in #print Vec.noConfusionType diff --git a/tests/lean/run/listDecEq.lean b/tests/lean/run/listDecEq.lean index d59e1f6c44..a9d01093a8 100644 --- a/tests/lean/run/listDecEq.lean +++ b/tests/lean/run/listDecEq.lean @@ -31,15 +31,15 @@ end -- List decidable equality using `withPtrEqDecEq` def listDecEqAux {α} [s : DecidableEq α] : ∀ (as bs : List α), Decidable (as = bs) | [], [] => isTrue rfl -| [], b::bs => isFalse $ fun h => List.noConfusion h -| a::as, [] => isFalse $ fun h => List.noConfusion h +| [], b::bs => isFalse $ fun h => List.noConfusion rfl (heq_of_eq h) +| a::as, [] => isFalse $ fun h => List.noConfusion rfl (heq_of_eq h) | a::as, b::bs => match s a b with | isTrue h₁ => match withPtrEqDecEq as bs (fun _ => listDecEqAux as bs) with | isTrue h₂ => isTrue $ h₁ ▸ h₂ ▸ rfl - | isFalse h₂ => isFalse $ fun h => List.noConfusion h $ fun _ h₃ => absurd h₃ h₂ - | isFalse h₁ => isFalse $ fun h => List.noConfusion h $ fun h₂ _ => absurd h₂ h₁ + | isFalse h₂ => isFalse $ fun h => List.noConfusion rfl (heq_of_eq h) (fun _ h₃ => absurd (eq_of_heq h₃) h₂) + | isFalse h₁ => isFalse $ fun h => List.noConfusion rfl (heq_of_eq h) (fun h₂ _ => absurd (eq_of_heq h₂) h₁) instance List.optimizedDecEq {α} [DecidableEq α] : DecidableEq (List α) := fun a b => withPtrEqDecEq a b (fun _ => listDecEqAux a b) diff --git a/tests/lean/run/noConfusionCtorInjection.lean b/tests/lean/run/noConfusionCtorInjection.lean index 64caa1adb4..29d3faa6b1 100644 --- a/tests/lean/run/noConfusionCtorInjection.lean +++ b/tests/lean/run/noConfusionCtorInjection.lean @@ -6,8 +6,7 @@ inductive L (α : Type u) : Type u where /-- info: theorem L.cons.inj.{u} : ∀ {α : Type u} {x : α} {xs : L α} {x_1 : α} {xs_1 : L α}, L.cons x xs = L.cons x_1 xs_1 → x = x_1 ∧ xs = xs_1 := -fun {α} {x} {xs} {x_1} {xs_1} x_2 => - L.cons.noConfusion (Eq.refl α) (heq_of_eq x_2) fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩ +fun {α} {x} {xs} {x_1} {xs_1} x_2 => L.cons.noConfusion x_2 fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩ -/ #guard_msgs in #print L.cons.inj @@ -21,8 +20,7 @@ theorem ex1 (h : L.cons x xs = L.cons y ys) : x = y ∧ xs = ys := by /-- info: theorem ex1.{u_1} : ∀ {α : Type u_1} {x : α} {xs : L α} {y : α} {ys : L α}, L.cons x xs = L.cons y ys → x = y ∧ xs = ys := -fun {α} {x} {xs} {y} {ys} h => - L.cons.noConfusion (Eq.refl α) (heq_of_eq h) fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩ +fun {α} {x} {xs} {y} {ys} h => L.cons.noConfusion h fun x_eq xs_eq => ⟨eq_of_heq x_eq, eq_of_heq xs_eq⟩ -/ #guard_msgs in #print ex1