Update test

Author: nomeata

tests/lean/run/lift_match.lean

@@ -8,7 +8,7 @@ def test1 : Nat → Nat
 -- set_option pp.match false
 
 /--
-info: test1.match_1.float.{u, v} {α : Sort u} {β : Sort v} (f : α → β) (x✝ : Nat) (h_1 : Unit → (fun x => α) 0)
+info: test1.match_1.lifter.{u, v} {α : Sort u} {β : Sort v} (f : α → β) (x✝ : Nat) (h_1 : Unit → (fun x => α) 0)
   (h_2 : (n : Nat) → (fun x => α) n.succ) :
   f
       (match x✝ with
@@ -19,15 +19,15 @@ info: test1.match_1.float.{u, v} {α : Sort u} {β : Sort v} (f : α → β) (x
     | n.succ => f (h_2 n)
 -/
 #guard_msgs in
-#check test1.match_1.float
+#check test1.match_1.lifter
 
 def test2 (α β) : α ∨ β → γ → (β ∨ α) ∧ γ
   | .inl x, y => ⟨.inr x, y⟩
   | .inr x, y => ⟨.inl x, y⟩
 
 set_option pp.proofs true in
 /--
-info: test2.match_1.float {α β : Prop} (f : α → β) {γ : Prop} (α✝ β✝ : Prop) (x✝ : α✝ ∨ β✝) (x✝¹ : γ)
+info: test2.match_1.lifter {α β : Prop} (f : α → β) {γ : Prop} (α✝ β✝ : Prop) (x✝ : α✝ ∨ β✝) (x✝¹ : γ)
   (h_1 : ∀ (x : α✝) (y : γ), (fun x x => α) (Or.inl x) y) (h_2 : ∀ (x : β✝) (y : γ), (fun x x => α) (Or.inr x) y) :
   f
       (match x✝, x✝¹ with
@@ -38,28 +38,28 @@ info: test2.match_1.float {α β : Prop} (f : α → β) {γ : Prop} (α✝ β
     | Or.inr x, y => f (h_2 x y)
 -/
 #guard_msgs in
-#check test2.match_1.float
+#check test2.match_1.lifter
 
 -- This fails if there is no splitter theorem for a match
 
 /--
-error: Failed to realize constant Nat.lt_or_gt_of_ne.match_1.float:
-  Cannot construct match floating theorem:
+error: Failed to realize constant Nat.lt_or_gt_of_ne.match_1.lifter:
+  Cannot construct match lifter:
     Could not construct splitter for Nat.lt_or_gt_of_ne.match_1
 ---
-error: Failed to realize constant Nat.lt_or_gt_of_ne.match_1.float:
-  Cannot construct match floating theorem:
+error: Failed to realize constant Nat.lt_or_gt_of_ne.match_1.lifter:
+  Cannot construct match lifter:
     Could not construct splitter for Nat.lt_or_gt_of_ne.match_1
 ---
-error: unknown identifier 'Nat.lt_or_gt_of_ne.match_1.float'
+error: unknown identifier 'Nat.lt_or_gt_of_ne.match_1.lifter'
 -/
 #guard_msgs in
-#check Nat.lt_or_gt_of_ne.match_1.float
+#check Nat.lt_or_gt_of_ne.match_1.lifter
 
 -- A typical example
 
 theorem List.filter_map' (f : β → α) (l : List β) : filter p (map f l) = map f (filter (p ∘ f) l) := by
-  induction l <;> simp [filter, *, lift_match]
+  induction l <;> simp [filter, *, liftMatch]
 
 -- Using the lift_match conv tactic
 
@@ -93,7 +93,7 @@ theorem List.filter_map''' (f : β → α) (l : List β) : filter p (map f l) =
 example (o : Option Bool) :
   (match o with | some b => b | none => false)
     = !(match o with | some b => !b | none => true) := by
-  simp [lift_match]
+  simp [liftMatch]
 
 -- Can float out of ite-condition
 /--
@@ -108,13 +108,13 @@ P : Nat → Prop
 #guard_msgs in
 example (o : Option Bool) (P : Nat → Prop):
   P (if (match o with | some b => b | none => true) then 1 else 2) := by
-  simp only [lift_match]
+  simp only [liftMatch]
   fail
 
--- Cannot float out of ite-branch
+-- Cannot lift out of ite-branch
 example (b : Bool) (o : Option Bool) (P : Bool → Prop) (abort : ∀ b, P b):
   P (if b then (match o with | some b => b | none => true) else b) := by
-  fail_if_success simp only [lift_match]
+  fail_if_success simp only [liftMatch]
   apply abort
 
 -- Can float out of a match target (aka case-of-case)
@@ -133,43 +133,43 @@ P : Nat → Prop
 #guard_msgs in
 example (o : Option Bool) (P : Nat → Prop):
   P (match (match o with | some b => b | none => true) with | true => 1 | false => 2) := by
-  simp only [lift_match]
+  simp only [liftMatch]
   fail
 
 -- Dependent motive; must not rewrite
 
 set_option trace.lift_match true in
-/-- info: [lift_match] Cannot float match: motive depends on targets -/
+/-- info: [lift_match] Cannot lift match: motive depends on targets -/
 #guard_msgs in
 example (o : Option Bool) (motive : Bool → Type) (P : {b : Bool} → motive b → Prop)
   (f : (x : Bool) → motive x) (g : {x : Bool} → motive x → motive x)
   (abort : ∀ b (x : motive b), P x) :
   P (g (match (motive := ∀ b, motive b.isSome) o with | some _ => f true | none => f false)) := by
-  fail_if_success simp [lift_match]
+  fail_if_success simp [liftMatch]
   apply abort
 
 -- Dependent context; must not rewrite
 
 set_option trace.lift_match true in
-/-- info: [lift_match] Cannot float match: f is dependent -/
+/-- info: [lift_match] Cannot lift match: f is dependent -/
 #guard_msgs in
 example (o : Option Bool) (motive : Bool → Type) (P : {b : Bool} → motive b → Prop)
   (f : (x : Bool) → motive x)
   (abort : ∀ b (x : motive b), P x) :
   P (f (match (motive := ∀ _, Bool) o with | some b => b | none => false)) := by
-  fail_if_success simp [lift_match]
+  fail_if_success simp [liftMatch]
   apply abort
 
 -- Context depends on the concrete value of the match, must not rewrite
 
 set_option trace.lift_match true in
-/-- info: [lift_match] Cannot float match: context is not type correct -/
+/-- info: [lift_match] Cannot lift match: context is not type correct -/
 #guard_msgs in
 example (o : Option Bool)
   (f : (x : Bool) → (h : x = (match o with | some b => b | none => false)) → Bool)
   (abort : ∀ (P : Prop), P) :
   f (match (motive := ∀ _, Bool) o with | some b => b | none => false) rfl = true := by
-  fail_if_success simp [lift_match]
+  fail_if_success simp [liftMatch]
   apply abort
 
 -- Can float out of a let (Only relevant with zeta := false)
@@ -190,7 +190,7 @@ P : Bool → Prop
 #guard_msgs in
 example (o : Option Bool) (P : Bool → Prop):
   P (let b := match o with | some b => b | none => true; !b) := by
-  simp -zeta only [lift_match]
+  simp -zeta only [liftMatch]
   fail
 
 /-
@@ -234,21 +234,21 @@ b : Bool
 #guard_msgs in
 example (P : Nat → Prop) (f : Nat → Nat) (b : Bool) :
   P (f (if b then 1 else 2)) := by
-  simp only [lift_match]
+  simp only [liftMatch]
   fail
 
 -- Dependent f
 
 /--
 error: simp made no progress
 ---
-info: [lift_match] Cannot float match: f is dependent
+info: [lift_match] Cannot lift match: f is dependent
 -/
 #guard_msgs in
 set_option trace.lift_match true in
 example (P : {n : Nat} → Fin n → Prop) (f : (n : Nat) → Fin n) (b : Bool) :
   P (f (if b then 1 else 2)) := by
-  simp only [lift_match]
+  simp only [liftMatch]
   fail
 
 -- Somewhat dependent f, but abstracting still succeeds
@@ -263,7 +263,7 @@ b : Bool
 #guard_msgs in
 example (P : Nat → Prop) (f : (n : Nat) → DecidableEq (Fin n) → Nat) (b : Bool) :
   P (f (if b then 1 else 2) inferInstance) := by
-  simp only [lift_match]
+  simp only [liftMatch]
   fail
 
 -- Testing dependent if-then-else
@@ -278,21 +278,21 @@ b : Bool
 #guard_msgs in
 example (P : Nat → Prop) (f : Nat → Nat) (b : Bool) :
   P (f (if h : b then 1 else 2)) := by
-  simp only [lift_match]
+  simp only [liftMatch]
   fail
 
 -- Dependent f
 
 /--
 error: simp made no progress
 ---
-info: [lift_match] Cannot float match: f is dependent
+info: [lift_match] Cannot lift match: f is dependent
 -/
 #guard_msgs in
 set_option trace.lift_match true in
 example (P : {n : Nat} → Fin n → Prop) (f : (n : Nat) → Fin n) (b : Bool) :
   P (f (if h : b then 1 else 2)) := by
-  simp only [lift_match]
+  simp only [liftMatch]
   fail
 
 -- Somewhat dependent f, but abstracting still succeeds
@@ -307,5 +307,5 @@ b : Bool
 #guard_msgs in
 example (P : Nat → Prop) (f : (n : Nat) → DecidableEq (Fin n) → Nat) (b : Bool) :
   P (f (if h : b then 1 else 2) inferInstance) := by
-  simp only [lift_match]
+  simp only [liftMatch]
   fail