From 23a578c37cf4c4fc2e416f9137709c0565713c0a Mon Sep 17 00:00:00 2001 From: tydeu Date: Thu, 14 Jul 2022 18:11:12 -0400 Subject: [PATCH] refactor: add `LawfulCmpEq` + post-PR cleanup --- Lake/Build/Data.lean | 10 ++-- Lake/Build/Key.lean | 3 +- Lake/DSL/Facets.lean | 6 +-- Lake/Util/Compare.lean | 109 +++++++++++++++++++++++------------------ Lake/Util/Name.lean | 86 ++++++++++++-------------------- 5 files changed, 103 insertions(+), 111 deletions(-) diff --git a/Lake/Build/Data.lean b/Lake/Build/Data.lean index 10fa88109d..ccb14ed1a8 100644 --- a/Lake/Build/Data.lean +++ b/Lake/Build/Data.lean @@ -75,21 +75,21 @@ abbrev BuildData : BuildKey → Type scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment) "package_data " id:ident " : " ty:term : command => do let dty := mkCIdentFrom (← getRef) ``PackageData - let key := Lake.quoteNameFrom id id.getId + let key := Name.quoteFrom id id.getId `($[$doc?]? family_def $id : $dty $key := $ty) /-- Macro for declaring new `ModuleData`. -/ scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment) "module_data " id:ident " : " ty:term : command => do let dty := mkCIdentFrom (← getRef) ``ModuleData - let key := Lake.quoteNameFrom id id.getId + let key := Name.quoteFrom id id.getId `($[$doc?]? family_def $id : $dty $key := $ty) /-- Macro for declaring new `TargetData`. -/ scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment) "target_data " id:ident " : " ty:term : command => do let dty := mkCIdentFrom (← getRef) ``TargetData - let key := Lake.quoteNameFrom id id.getId + let key := Name.quoteFrom id id.getId `($[$doc?]? family_def $id : $dty $key := $ty) /-- Macro for declaring new `CustomData`. -/ @@ -97,6 +97,6 @@ scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment) "custom_data " pkg:ident tgt:ident " : " ty:term : command => do let dty := mkCIdentFrom (← getRef) ``CustomData let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId) - let pkg := Lake.quoteNameFrom pkg pkg.getId - let tgt := Lake.quoteNameFrom pkg tgt.getId + let pkg := Name.quoteFrom pkg pkg.getId + let tgt := Name.quoteFrom pkg tgt.getId `($[$doc?]? family_def $id : $dty ($pkg, $tgt) := $ty) diff --git a/Lake/Build/Key.lean b/Lake/Build/Key.lean index e42eba78b9..6b1ebd9377 100644 --- a/Lake/Build/Key.lean +++ b/Lake/Build/Key.lean @@ -99,5 +99,6 @@ quickCmp k k' = Ordering.eq → k = k' := by next => intro; contradiction all_goals (intro; contradiction) -instance : EqOfCmp BuildKey quickCmp where +instance : LawfulCmpEq BuildKey quickCmp where eq_of_cmp := eq_of_quickCmp + cmp_rfl {k} := by cases k <;> simp [quickCmp] diff --git a/Lake/DSL/Facets.lean b/Lake/DSL/Facets.lean index d575af0ee7..754a86af5f 100644 --- a/Lake/DSL/Facets.lean +++ b/Lake/DSL/Facets.lean @@ -22,7 +22,7 @@ kw:"module_facet " sig:simpleDeclSig : command => do let attr ← withRef kw `(Term.attrInstance| moduleFacet) let attrs := #[attr] ++ expandAttrs attrs? let axm := mkIdentFrom id <| ``ModuleData ++ id.getId - let name := Lake.quoteNameFrom id id.getId + let name := Name.quoteFrom id id.getId `(module_data $id : ActiveBuildTarget $ty $[$doc?]? @[$attrs,*] def $id : ModuleFacetDecl := { name := $name @@ -43,7 +43,7 @@ kw:"package_facet " sig:simpleDeclSig : command => do let attr ← withRef kw `(Term.attrInstance| packageFacet) let attrs := #[attr] ++ expandAttrs attrs? let axm := mkIdentFrom id <| ``PackageData ++ id.getId - let name := Lake.quoteNameFrom id id.getId + let name := Name.quoteFrom id id.getId `(package_data $id : ActiveBuildTarget $ty $[$doc?]? @[$attrs,*] def $id : PackageFacetDecl := { name := $name @@ -64,7 +64,7 @@ kw:"target " sig:simpleDeclSig : command => do let attr ← withRef kw `(Term.attrInstance| target) let attrs := #[attr] ++ expandAttrs attrs? let axm := mkIdentFrom id <| ``CustomData ++ id.getId - let name := Lake.quoteNameFrom id id.getId + let name := Name.quoteFrom id id.getId let pkgName := mkIdentFrom id `_package.name `(family_def $id : CustomData ($pkgName, $name) := ActiveBuildTarget $ty $[$doc?]? @[$attrs,*] def $id : TargetConfig := { diff --git a/Lake/Util/Compare.lean b/Lake/Util/Compare.lean index 15ce28695c..8179ff8743 100644 --- a/Lake/Util/Compare.lean +++ b/Lake/Util/Compare.lean @@ -7,89 +7,104 @@ Authors: Mac Malone namespace Lake /-- -Proof that that equality of a compare function corresponds +Proof that the equality of a compare function corresponds to propositional equality. -/ class EqOfCmp (α : Type u) (cmp : α → α → Ordering) where - eq_of_cmp {a a' : α} : cmp a a' = Ordering.eq → a = a' + eq_of_cmp {a a' : α} : cmp a a' = .eq → a = a' export EqOfCmp (eq_of_cmp) /-- -Proof that that equality of a compare function corresponds +Proof that the equality of a compare function corresponds +to propositional equality and vice versa. +-/ +class LawfulCmpEq (α : Type u) (cmp : α → α → Ordering) extends EqOfCmp α cmp where + cmp_rfl {a : α} : cmp a a = .eq + +export LawfulCmpEq (cmp_rfl) + +attribute [simp] cmp_rfl + +@[simp] theorem cmp_iff_eq [LawfulCmpEq α cmp] : cmp a a' = .eq ↔ a = a' := + Iff.intro eq_of_cmp fun a_eq => a_eq ▸ cmp_rfl + +/-- +Proof that the equality of a compare function corresponds to propositional equality with respect to a given function. -/ class EqOfCmpWrt (α : Type u) {β : Type v} (f : α → β) (cmp : α → α → Ordering) where - eq_of_cmp_wrt {a a' : α} : cmp a a' = Ordering.eq → f a = f a' + eq_of_cmp_wrt {a a' : α} : cmp a a' = .eq → f a = f a' export EqOfCmpWrt (eq_of_cmp_wrt) +instance : EqOfCmpWrt α (fun _ => α) cmp := ⟨fun _ => rfl⟩ + instance [EqOfCmp α cmp] : EqOfCmpWrt α f cmp where eq_of_cmp_wrt h := by rw [eq_of_cmp h] -instance [EqOfCmpWrt α id cmp] : EqOfCmp α cmp where - eq_of_cmp h := eq_of_cmp_wrt (f := id) h - instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where eq_of_cmp h := eq_of_cmp_wrt (f := fun a => a) h -instance : EqOfCmpWrt α (fun _ => α) cmp := ⟨fun _ => rfl⟩ -theorem eq_of_compareOfLessAndEq -{a a' : α} [LT α] [DecidableEq α] [Decidable (a < a')] -(h : compareOfLessAndEq a a' = Ordering.eq) : a = a' := by +-- ## Basic Instances + +theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α} +[Decidable (a < a')] (h : compareOfLessAndEq a a' = .eq) : a = a' := by unfold compareOfLessAndEq at h split at h; case inl => exact False.elim h split at h; case inr => exact False.elim h assumption -theorem Nat.eq_of_compare -{n n' : Nat} : compare n n' = Ordering.eq → n = n' := by - simp only [compare]; exact eq_of_compareOfLessAndEq +theorem compareOfLessAndEq_rfl [LT α] [DecidableEq α] {a : α} +[Decidable (a < a)] (lt_irrefl : ¬ a < a) : compareOfLessAndEq a a = .eq := by + simp [compareOfLessAndEq, lt_irrefl] -@[simp] -theorem Nat.compare_iff_eq -{n n' : Nat} : compare n n' = Ordering.eq ↔ n = n' := by - refine ⟨eq_of_compare, fun h => ?_⟩ - simp [h, compare, compareOfLessAndEq] +instance : LawfulCmpEq Nat compare where + eq_of_cmp := eq_of_compareOfLessAndEq + cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _ -instance : EqOfCmp Nat compare where - eq_of_cmp h := Nat.eq_of_compare h +theorem Fin.eq_of_compare {n n' : Fin m} (h : compare n n' = .eq) : n = n' := by + dsimp only [compare] at h + have h' := eq_of_compareOfLessAndEq h + exact Fin.eq_of_val_eq h' -theorem String.eq_of_compare -{s s' : String} : compare s s' = Ordering.eq → s = s' := by - simp only [compare]; exact eq_of_compareOfLessAndEq +instance : LawfulCmpEq (Fin n) compare where + eq_of_cmp := Fin.eq_of_compare + cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _ + +instance : LawfulCmpEq UInt64 compare where + eq_of_cmp h := eq_of_compareOfLessAndEq h + cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _ theorem List.lt_irrefl [LT α] (irrefl_α : ∀ a : α, ¬ a < a) : (a : List α) → ¬ a < a - | _, .head _ _ h => irrefl_α _ h - | _, .tail _ _ h3 => lt_irrefl irrefl_α _ h3 +| _, .head _ _ h => irrefl_α _ h +| _, .tail _ _ h3 => lt_irrefl irrefl_α _ h3 -@[simp] -theorem String.lt_irrefl (s : String) : ¬ s < s := +@[simp] theorem String.lt_irrefl (s : String) : ¬ s < s := List.lt_irrefl (fun c => Nat.lt_irrefl c.1.1) _ -@[simp] -theorem String.compare_iff_eq -{n n' : String} : compare n n' = Ordering.eq ↔ n = n' := by - refine ⟨eq_of_compare, fun h => ?_⟩ - simp [h, compare, compareOfLessAndEq] +instance : LawfulCmpEq String compare where + eq_of_cmp := eq_of_compareOfLessAndEq + cmp_rfl := compareOfLessAndEq_rfl <| String.lt_irrefl _ -instance : EqOfCmp String compare where - eq_of_cmp h := String.eq_of_compare h - -@[inline] +@[macroInline] def Option.compareWith (cmp : α → α → Ordering) : Option α → Option α → Ordering -| none, none => Ordering.eq -| none, some _ => Ordering.lt -| some _, none => Ordering.gt +| none, none => .eq +| none, some _ => .lt +| some _, none => .gt | some x, some y => cmp x y -theorem Option.eq_of_compareWith [EqOfCmp α cmp] -{o o' : Option α} : compareWith cmp o o' = Ordering.eq → o = o' := by - unfold compareWith - cases o <;> cases o' <;> simp - exact eq_of_cmp - instance [EqOfCmp α cmp] : EqOfCmp (Option α) (Option.compareWith cmp) where - eq_of_cmp h := Option.eq_of_compareWith h + eq_of_cmp := by + intro o o' + unfold Option.compareWith + cases o <;> cases o' <;> simp + exact eq_of_cmp + +instance [LawfulCmpEq α cmp] : LawfulCmpEq (Option α) (Option.compareWith cmp) where + cmp_rfl := by + intro o + unfold Option.compareWith + cases o <;> simp diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index 5a0be2a4f3..8fd5fad59b 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -15,6 +15,7 @@ export Lean (Name NameMap) -- # Name Helpers namespace Name +open Lean.Name def ofString (str : String) : Name := str.splitOn "." |>.foldl (fun n p => .str n p.trim) .anonymous @@ -23,70 +24,45 @@ def ofString (str : String) : Name := rw [← beq_iff_eq m n]; cases m == n <;> simp @[simp] theorem isPrefixOf_self {n : Name} : n.isPrefixOf n := by - cases n <;> simp [Name.isPrefixOf] + cases n <;> simp [isPrefixOf] @[simp] theorem isPrefixOf_append {n m : Name} : n.isPrefixOf (n ++ m) := by show n.isPrefixOf (n.append m) - induction m <;> simp [Name.isPrefixOf, Name.append, *] + induction m <;> simp [isPrefixOf, Name.append, *] -attribute [local simp] Name.quickCmpAux +@[simp] theorem quickCmpAux_iff_eq : ∀ {n n'}, quickCmpAux n n' = .eq ↔ n = n' +| .anonymous, n => by cases n <;> simp [quickCmpAux] +| n, .anonymous => by cases n <;> simp [quickCmpAux] +| .num .., .str .. => by simp [quickCmpAux] +| .str .., .num .. => by simp [quickCmpAux] +| .num p₁ n₁, .num p₂ n₂ => by + simp only [quickCmpAux]; split <;> + simp_all [quickCmpAux_iff_eq, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl] +| .str p₁ s₁, .str p₂ s₂ => by + simp only [quickCmpAux]; split <;> + simp_all [quickCmpAux_iff_eq, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl] -@[simp] -theorem quickCmpAux_iff_eq : ∀ n n', Name.quickCmpAux n n' = Ordering.eq ↔ n = n' - | .anonymous, n => by cases n <;> simp - | n, .anonymous => by cases n <;> simp - | .num .., .str .. => by simp - | .str .., .num .. => by simp - | .num p₁ n₁, .num p₂ n₂ => by - simp only [Name.quickCmpAux]; split <;> - simp_all [quickCmpAux_iff_eq p₁ p₂, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl] - | .str p₁ s₁, .str p₂ s₂ => by - simp only [Name.quickCmpAux]; split <;> - simp_all [quickCmpAux_iff_eq p₁ p₂, show ∀ p, (p → False) ↔ ¬ p from fun _ => .rfl] +instance : LawfulCmpEq Name quickCmpAux where + eq_of_cmp := quickCmpAux_iff_eq.mp + cmp_rfl := quickCmpAux_iff_eq.mpr rfl -theorem eq_of_quickCmpAux (n n') : Name.quickCmpAux n n' = Ordering.eq → n = n' := - (quickCmpAux_iff_eq n n').1 - -end Name - --- # Subtype Helpers - -namespace Subtype - -theorem val_eq_of_eq {a b : Subtype p} (h : a = b) : a.val = b.val := - h ▸ rfl - -theorem eq_of_val_eq : ∀ {a b : Subtype p}, a.val = b.val → a = b - | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl - -theorem eq_iff_val_eq {a b : Subtype p} : a = b ↔ a.val = b.val := - Iff.intro val_eq_of_eq eq_of_val_eq - -theorem ne_of_val_ne {a b : Subtype p} (h : a.val ≠ b.val) : a ≠ b := - fun h' => absurd (val_eq_of_eq h') h - -theorem val_ne_of_ne {a b : Subtype p} (h : a ≠ b) : a.val ≠ b.val := - fun h' => absurd (eq_of_val_eq h') h - -theorem ne_iff_val_ne {a b : Subtype p} : a ≠ b ↔ a.val ≠ b.val := - Iff.intro val_ne_of_ne ne_of_val_ne - -end Subtype - -theorem eq_of_quickCmp {n n' : Name} : n.quickCmp n' = Ordering.eq → n = n' := by - simp only [Lean.Name.quickCmp, Name.quickCmp, Subtype.eq_iff_val_eq] +theorem eq_of_quickCmp {n n' : Name} : n.quickCmp n' = .eq → n = n' := by + unfold Name.quickCmp intro h_cmp; split at h_cmp - next => exact Name.eq_of_quickCmpAux n n' h_cmp + next => exact eq_of_cmp h_cmp next => contradiction -instance : EqOfCmp Name Name.quickCmp where - eq_of_cmp h := eq_of_quickCmp h +theorem quickCmp_rfl {n : Name} : n.quickCmp n = .eq := by + unfold Name.quickCmp + split <;> exact cmp_rfl + +instance : LawfulCmpEq Name Name.quickCmp where + eq_of_cmp := eq_of_quickCmp + cmp_rfl := quickCmp_rfl open Syntax -def quoteNameFrom (ref : Syntax) : Name → Term -| .anonymous => mkCIdentFrom ref ``Name.anonymous -| .str p s => mkApp (mkCIdentFrom ref ``Name.mkStr) - #[quoteNameFrom ref p, quote s] -| .num p v => mkApp (mkCIdentFrom ref ``Name.mkNum) - #[quoteNameFrom ref p, quote v] +def quoteFrom (ref : Syntax) : Name → Term +| .anonymous => mkCIdentFrom ref ``anonymous +| .str p s => mkApp (mkCIdentFrom ref ``mkStr) #[quoteFrom ref p, quote s] +| .num p v => mkApp (mkCIdentFrom ref ``mkNum) #[quoteFrom ref p, quote v]