From 18bbb9cb0a4b39618d609f21753b8729af932626 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Tue, 6 Feb 2024 15:44:23 -0800 Subject: [PATCH] feat: Introduce #check_simp command and usage. (#583) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: François G. Dorais --- Std.lean | 1 + Std/Data/Array/Lemmas.lean | 32 ++++++++++++++++ Std/Util/CheckTactic.lean | 77 ++++++++++++++++++++++++++++++++++++++ test/array.lean | 21 +++++++++++ 4 files changed, 131 insertions(+) create mode 100644 Std/Util/CheckTactic.lean create mode 100644 test/array.lean diff --git a/Std.lean b/Std.lean index aa7d2f2e4c..5085b56362 100644 --- a/Std.lean +++ b/Std.lean @@ -147,6 +147,7 @@ import Std.Tactic.Unreachable import Std.Tactic.Where import Std.Test.Internal.DummyLabelAttr import Std.Util.Cache +import Std.Util.CheckTactic import Std.Util.ExtendedBinder import Std.Util.LibraryNote import Std.Util.Pickle diff --git a/Std/Data/Array/Lemmas.lean b/Std/Data/Array/Lemmas.lean index ab628d786a..c5dc10f4ea 100644 --- a/Std/Data/Array/Lemmas.lean +++ b/Std/Data/Array/Lemmas.lean @@ -41,10 +41,26 @@ attribute [simp] isEmpty uget @[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl +/-- # mem -/ + theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := (mem_def _ _).symm theorem not_mem_nil (a : α) : ¬ a ∈ #[] := fun. +/-- # set -/ + +@[simp] theorem set!_is_setD : @set! = @setD := rfl + +@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) : + (Array.setD a index val).size = a.size := by + if h : index < a.size then + simp [setD, h] + else + simp [setD, h] + + +/-- # get lemmas -/ + theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by erw [Array.mem_def, getElem_eq_data_get] apply List.get_mem @@ -131,6 +147,22 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by if h : i.1 = j then subst j; simp [*] else simp [*] +@[simp] theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) : + (setD a i v)[i]'h = v := by + simp at h + simp only [setD, h, dite_true, get_set, ite_true] + +/-- +This lemma simplifies a normal form from `get!` +-/ +@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) : + Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by + if h : i < a.size then + simp [setD, h, getElem?, get_set] + else + have p : i ≥ a.size := Nat.le_of_not_gt h + simp [setD, h, get?_len_le, p] + theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) : (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set] diff --git a/Std/Util/CheckTactic.lean b/Std/Util/CheckTactic.lean new file mode 100644 index 0000000000..76cfedf473 --- /dev/null +++ b/Std/Util/CheckTactic.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2024 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joe Hendrix +-/ +import Lean.Elab.Tactic.ElabTerm + +/- +This file is the home for commands to tactics behave as expected. + +It currently includes two tactixs: + +#check_tactic t ~> res + + +only a #check_simp command that applies simp +IT +-/ + +namespace Std.Tactic + +open Lean +open Elab.Tactic +open Meta + +/-- +Type used to lift an arbitrary value into a type parameter so it can +appear in a proof goal. + +It is used by the #check_tactic command. +-/ +private inductive CheckGoalType {α : Sort u} : (val : α) → Prop where +| intro : (val : α) → CheckGoalType val + +/-- +`check_tactic_goal t` verifies that the goal has is equal to +`CheckGoalType t` with reducible transparency. It closes the goal if so +and otherwise reports an error. + +It is used by #check_tactic. +-/ +local syntax (name := check_tactic_goal) "check_tactic_goal " term : tactic + + +/-- +Implementation of `check_tactic_goal` +-/ +@[tactic check_tactic_goal] private def evalCheckTacticGoal : Tactic := fun stx => + match stx with + | `(tactic| check_tactic_goal $exp) => + closeMainGoalUsing (checkUnassigned := false) fun goalType => do + let u ← mkFreshLevelMVar + let type ← mkFreshExprMVar (.some (.sort u)) + let val ← mkFreshExprMVar (.some type) + let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val] + if !(← isDefEq goalType extType) then + throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}" + let expTerm ← elabTermEnsuringType exp type + if !(← Meta.withReducible <| isDefEq val expTerm) then + throwErrorAt stx + m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}" + return mkAppN (.const ``CheckGoalType.intro [u]) #[type, val] + | _ => throwErrorAt stx "check_goal syntax error" + +/-- +`#check_tactic t ~> r by commands` runs the tactic sequence `commands` +on a goal with t in the type and sees if the resulting expression has +reduced it to `r`. +-/ +macro "#check_tactic " t:term "~>" result:term "by" tac:tactic : command => + `(command|example : CheckGoalType $t := by $tac; check_tactic_goal $result) + +/-- +`#check_simp t ~> r` checks `try simp` reduces `t` to `r`. +-/ +macro "#check_simp " t:term "~>" exp:term : command => + `(command|#check_tactic $t ~> $exp by try simp) diff --git a/test/array.lean b/test/array.lean new file mode 100644 index 0000000000..487ac93581 --- /dev/null +++ b/test/array.lean @@ -0,0 +1,21 @@ +import Std.Util.CheckTactic +import Std.Data.Array + +section +variable {α : Type _} +variable [Inhabited α] +variable (a : Array α) +variable (i : Nat) +variable (v d : α) +variable (g : i < (a.set! i v).size) + +#check_simp (a.set! i v).get ⟨i, g⟩ ~> v +#check_simp (a.set! i v).get! i ~> if i < a.size then v else default +#check_simp (a.set! i v).getD i d ~> if i < a.size then v else d +#check_simp (a.set! i v)[i] ~> v + +-- This doesn't work currently. +-- It will be address in the comprehensive overhaul of array lemmas. +-- #check_simp (a.set! i v)[i]? ~> .some v + +end