chore: add test with <->, discharger, contextual, conditional

tests/lean/simp_trace.lean

@@ -1,15 +1,16 @@
 set_option tactic.simp.trace true
+set_option trace.Meta.Tactic.simp.rewrite true
 
 def f (x : α) := x
 
-theorem ex1 (a : α) (b : List α) : f (a::b = []) = False :=
+example (a : α) (b : List α) : f (a::b = []) = False :=
   by simp [f]
 
 def length : List α → Nat
   | []    => 0
   | a::as => length as + 1
 
-theorem ex2 (a b c : α) (as : List α) : length (a :: b :: as) > length as := by
+example (a b c : α) (as : List α) : length (a :: b :: as) > length as := by
   simp [length]
   apply Nat.lt.step
   apply Nat.lt_succ_self
@@ -31,12 +32,12 @@ def head [Inhabited α] : List α → α
   | []   => default
   | a::_ => a
 
-theorem ex4 [Inhabited α] (a : α) (as : List α) : head (a::as) = a :=
+example [Inhabited α] (a : α) (as : List α) : head (a::as) = a :=
   by simp [head]
 
 def foo := 10
 
-theorem ex5 (x : Nat) : foo + x = 10 + x := by
+example (x : Nat) : foo + x = 10 + x := by
   simp [foo]
   done
 
@@ -44,7 +45,7 @@ def g (x : Nat) : Nat := Id.run <| do
   let x := x
   return x
 
-theorem ex6 : g x = x := by
+example : g x = x := by
   simp [g, bind, pure]
   rfl
 
@@ -55,7 +56,7 @@ def f2 : StateM Nat Unit := do
   let s ← get
   set <| g s
 
-theorem ex7 : f1 = f2 := by
+example : f1 = f2 := by
   simp [f1, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, pure, set, StateT.set, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet]
 
 def h (x : Nat) : Sum (Nat × Nat) Nat := Sum.inl (x, x)
@@ -65,5 +66,18 @@ def bla (x : Nat) :=
   | Sum.inl (y, z) => y + z
   | Sum.inr _ => 0
 
-theorem ex8 (x : Nat) : bla x = x + x := by
+example (x : Nat) : bla x = x + x := by
   simp [bla, h]
+
+example (x : Nat) (h : 1 ≤ x) : x - 1 + 1 + 2 = x + 2 := by
+  simp [h, Nat.sub_add_cancel]
+
+example (x : Nat) : (if h : 1 ≤ x then x - 1 + 1 else 0) = (if _h : 1 ≤ x then x else 0) := by
+  simp (config := {contextual := true}) [h, Nat.sub_add_cancel]
+
+theorem my_thm : a ∧ a ↔ a := ⟨fun h => h.1, fun h => ⟨h, h⟩⟩
+
+example : a ∧ (b ∧ b) ↔ a ∧ b := by simp [my_thm]
+example : (a ∧ (b ∧ b)) = (a ∧ b) := by simp only [my_thm]
+
+example : x - 1 + 1 = x := by simp (discharger := sorry) [Nat.sub_add_cancel]

tests/lean/simp_trace.lean.expected.out

@@ -1,8 +1,61 @@
 Try this: simp only [f]
+[Meta.Tactic.simp.rewrite] unfold f, f (a :: b = []) ==> a :: b = []
+[Meta.Tactic.simp.rewrite] @eq_self:1000, False = False ==> True
 Try this: simp only [length]
+[Meta.Tactic.simp.rewrite] unfold length, length (a :: b :: as) ==> length (b :: as) + 1
+[Meta.Tactic.simp.rewrite] unfold length, length (b :: as) ==> length as + 1
 Try this: simp only [fact]
+[Meta.Tactic.simp.rewrite] unfold fact, fact (Nat.succ x) ==> (x + 1) * fact x
 Try this: simp only [head]
+[Meta.Tactic.simp.rewrite] unfold head, head (a :: as) ==> match a :: as with
+    | [] => default
+    | a :: tail => a
+[Meta.Tactic.simp.rewrite] @eq_self:1000, a = a ==> True
 Try this: simp only [foo]
+[Meta.Tactic.simp.rewrite] unfold foo, foo ==> 10
+[Meta.Tactic.simp.rewrite] @eq_self:1000, 10 + x = 10 + x ==> True
 Try this: simp only [g, Id.pure_eq]
+[Meta.Tactic.simp.rewrite] unfold g, g x ==> Id.run
+      (let x := x;
+      pure x)
+[Meta.Tactic.simp.rewrite] @Id.pure_eq:1000, pure x ==> x
 Try this: simp only [f1, modify, StateT.modifyGet, f2, StateT.bind, getThe, StateT.get, StateT.set]
+[Meta.Tactic.simp.rewrite] unfold f1, f1 ==> modify fun x => g x
+[Meta.Tactic.simp.rewrite] unfold modify, modify fun x => g x ==> modifyGet fun s => (PUnit.unit, (fun x => g x) s)
+[Meta.Tactic.simp.rewrite] unfold StateT.modifyGet, StateT.modifyGet fun s =>
+      (PUnit.unit, (fun x => g x) s) ==> fun s => pure ((fun s => (PUnit.unit, (fun x => g x) s)) s)
+[Meta.Tactic.simp.rewrite] unfold f2, f2 ==> do
+      let s ← get
+      set (g s)
+[Meta.Tactic.simp.rewrite] unfold StateT.bind, StateT.bind get fun s => set (g s) ==> fun s => do
+      let discr ← get s
+      match discr with
+        | (a, s) => (fun s => set (g s)) a s
+[Meta.Tactic.simp.rewrite] unfold getThe, getThe Nat s ==> MonadStateOf.get s
+[Meta.Tactic.simp.rewrite] unfold StateT.get, StateT.get s ==> pure (s, s)
+[Meta.Tactic.simp.rewrite] unfold StateT.set, StateT.set (g a) s ==> pure (PUnit.unit, g a)
+[Meta.Tactic.simp.rewrite] @eq_self:1000, (fun s => (PUnit.unit, g s)) = fun s => (PUnit.unit, g s) ==> True
 Try this: simp only [bla, h]
+[Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
+    | Sum.inl (y, z) => y + z
+    | Sum.inr val => 0
+[Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
+[Meta.Tactic.simp.rewrite] @eq_self:1000, x + x = x + x ==> True
+Try this: simp only [h, Nat.sub_add_cancel]
+[Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
+[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
+[Meta.Tactic.simp.rewrite] @eq_self:1000, x + 2 = x + 2 ==> True
+Try this: simp (config := { contextual := true }) only [Nat.sub_add_cancel]
+[Meta.Tactic.simp.rewrite] h:1000, 1 ≤ x ==> True
+[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
+[Meta.Tactic.simp.rewrite] @eq_self:1000, (if h : 1 ≤ x then x else 0) = if _h : 1 ≤ x then x else 0 ==> True
+Try this: simp only [and_self, iff_self]
+[Meta.Tactic.simp.rewrite] and_self:1000, b ∧ b ==> b
+[Meta.Tactic.simp.rewrite] iff_self:1000, a ∧ b ↔ a ∧ b ==> True
+Try this: simp only [my_thm]
+[Meta.Tactic.simp.rewrite] @my_thm:1000, b ∧ b ==> b
+[Meta.Tactic.simp.rewrite] @eq_self:1000, (a ∧ b) = (a ∧ b) ==> True
+Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
+simp_trace.lean:83:0-83:7: warning: declaration uses 'sorry'
+[Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
+[Meta.Tactic.simp.rewrite] @eq_self:1000, x = x ==> True