refactor: add LawfulCmpEq + post-PR cleanup
This commit is contained in:
tydeu
parent
32f870a994
commit
23a578c37c
5 changed files with 103 additions and 111 deletions
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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 := {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue