max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use abbrev in denote functions (#11092)

Browse source 
This PR ensures that `grind ac` denotation functions used in proof by
reflection are marked as `abbrev`.
This commit is contained in:
Leonardo de Moura 2025-11-05 08:51:36 -05:00 • committed by GitHub
parent 8b43fc54b2
commit ccecac5a56
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Grind/AC.lean
View file

@ -24,10 +24,10 @@ inductive Expr where
| op (lhs rhs : Expr)
deriving Inhabited, Repr, BEq
noncomputable def Var.denote {α : Sort u} (ctx : Context α) (x : Var) : α :=
noncomputable abbrev Var.denote {α : Sort u} (ctx : Context α) (x : Var) : α :=
PLift.rec (fun x => x) (ctx.vars.get x)
noncomputable def Expr.denote {α} (ctx : Context α) (e : Expr) : α :=
noncomputable abbrev Expr.denote {α} (ctx : Context α) (e : Expr) : α :=
Expr.rec (fun x => x.denote ctx) (fun _ _ ih₁ ih₂ => ctx.op ih₁ ih₂) e
theorem Expr.denote_var {α} (ctx : Context α) (x : Var) : (Expr.var x).denote ctx = x.denote ctx := rfl
@ -55,9 +55,12 @@ theorem Seq.beq'_eq (s₁ s₂ : Seq) : s₁.beq' s₂ = (s₁ = s₂) := by
attribute [local simp] Seq.beq'_eq
noncomputable def Seq.denote {α} (ctx : Context α) (s : Seq) : α :=
noncomputable abbrev Seq.denote {α} (ctx : Context α) (s : Seq) : α :=
Seq.rec (fun x => x.denote ctx) (fun x _ ih => ctx.op (x.denote ctx) ih) s
set_option allowUnsafeReducibility true
attribute [semireducible] Seq.denote
theorem Seq.denote_var {α} (ctx : Context α) (x : Var) : (Seq.var x).denote ctx = x.denote ctx := rfl
theorem Seq.denote_op {α} (ctx : Context α) (x : Var) (s : Seq) : (Seq.cons x s).denote ctx = ctx.op (x.denote ctx) (s.denote ctx) := rfl