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

chore: allow RArray to be universe polymorphic (#8013)

Browse source 
This PR ensures that `RArray` can be made universe polymorphic. We need
an update-stage0 before finalizing this modification.
This commit is contained in:
Leonardo de Moura 2025-04-17 18:10:44 -07:00 • committed by GitHub
parent a21377b9ec
commit 807182d63e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 50 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/Lean/Data/RArray.lean
View file

@ -6,6 +6,8 @@ Authors: Joachim Breitner
prelude
import Init.Data.RArray
import Lean.Meta.InferType
import Lean.Meta.DecLevel
import Lean.ToExpr
/-!
@ -57,19 +59,22 @@ where
case case1 => simp [ofFn.go, size]
case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega
section Meta
open Lean
def RArray.toExpr (ty : Expr) (f : α → Expr) : RArray α → Expr
| .leaf x =>
mkApp2 (mkConst ``RArray.leaf) ty (f x)
| .branch p l r =>
mkApp4 (mkConst ``RArray.branch) ty (mkRawNatLit p) (l.toExpr ty f) (r.toExpr ty f)
instance [ToExpr α] : ToExpr (RArray α) where
toTypeExpr := mkApp (mkConst ``RArray) (toTypeExpr α)
toExpr a := a.toExpr (toTypeExpr α) toExpr
end Meta
open Meta
def RArray.toExpr (ty : Expr) (f : α → Expr) (a : RArray α) : MetaM Expr := do
let k (leaf branch : Expr) : MetaM Expr :=
let rec go (a : RArray α) : MetaM Expr := do
match a with
| .leaf x =>
return mkApp2 leaf ty (f x)
| .branch p l r =>
return mkApp4 branch ty (mkRawNatLit p) (← go l) (← go r)
go a
let info ← getConstInfo ``RArray
-- TODO: remove after bootstrapping hell
if info.levelParams.isEmpty then
k (mkConst ``RArray.leaf) (mkConst ``RArray.branch)
else
let u ← getDecLevel ty
k (mkConst ``RArray.leaf [u]) (mkConst ``RArray.branch [u])
end Lean

2
src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
View file

@ -288,7 +288,7 @@ where
let ras := Lean.RArray.ofArray as h
let packedType := mkConst ``BVExpr.PackedBitVec
let pack := fun (width, expr) => mkApp2 (mkConst ``BVExpr.PackedBitVec.mk) (toExpr width) expr
let newAtomsAssignment := ras.toExpr packedType pack
let newAtomsAssignment ← ras.toExpr packedType pack
modify fun s => { s with atomsAssignmentCache := some newAtomsAssignment }
return newAtomsAssignment
else

6
src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
View file

@ -82,14 +82,14 @@ private def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr)
i := i - 1
return e
private def toContextExprCore (vars : PArray Expr) (type : Expr) : Expr :=
private def toContextExprCore (vars : PArray Expr) (type : Expr) : MetaM Expr :=
if h : 0 < vars.size then
RArray.toExpr type id (RArray.ofFn (vars[·]) h)
else
RArray.toExpr type id (RArray.leaf (mkIntLit 0))
private def toContextExpr : GoalM Expr := do
return toContextExprCore (← getVars) (mkConst ``Int)
toContextExprCore (← getVars) (mkConst ``Int)
private def withForeignContexts (k : Std.HashMap ForeignType Expr → GoalM α) : GoalM α := do
go 1 (← get').foreignVars.toList {}
@ -99,7 +99,7 @@ where
| [] => k r
| (type, ctx) :: ctxs =>
let typeExpr := type.denoteType
let ctxExpr := toContextExprCore ctx typeExpr
let ctxExpr ← toContextExprCore ctx typeExpr
withLetDecl ((`ctx).appendIndexAfter i) (mkApp (mkConst ``RArray) typeExpr) ctxExpr fun ctx => do
go (i+1) ctxs (r.insert type ctx)

2
src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
View file

@ -245,7 +245,7 @@ def dvdCnstr? (e : Expr) : MetaM (Option (Int × Int.Linear.Expr × Array Expr))
let e := e.applyPerm perm
return some (d, e, atoms)
def toContextExpr (ctx : Array Expr) : Expr :=
def toContextExpr (ctx : Array Expr) : MetaM Expr :=
if h : 0 < ctx.size then
RArray.toExpr (mkConst ``Int) id (RArray.ofArray ctx h)
else

36
src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
View file

@ -36,37 +36,37 @@ def simpEq? (e : Expr) : MetaM (Option (Expr × Expr)) := do
let p := a.sub b |>.norm
if p.isUnsatEq then
let r := mkConst ``False
let h := mkApp4 (mkConst ``Int.Linear.eq_eq_false) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
let h := mkApp4 (mkConst ``Int.Linear.eq_eq_false) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
else if p.isValidEq then
let r := mkConst ``True
let h := mkApp4 (mkConst ``Int.Linear.eq_eq_true) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
let h := mkApp4 (mkConst ``Int.Linear.eq_eq_true) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
else if p.toExpr == a && b == .num 0 then
return none
else match p with
| .add 1 x (.add (-1) y (.num 0)) =>
let r := mkIntEq atoms[x]! atoms[y]!
let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr y) reflBoolTrue
let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr y) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
| .add 1 x (.num k) =>
let r := mkIntEq atoms[x]! (toExpr (-k))
let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var_const) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr (-k)) reflBoolTrue
let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var_const) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr (-k)) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
| _ =>
let k := p.gcdCoeffs'
if k == 1 then
let r := mkIntEq (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
let h := mkApp5 (mkConst ``Int.Linear.norm_eq) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
let h := mkApp5 (mkConst ``Int.Linear.norm_eq) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
else if p.getConst % k == 0 then
let p := p.div k
let r := mkIntEq (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
let h := mkApp6 (mkConst ``Int.Linear.norm_eq_coeff) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
let h := mkApp6 (mkConst ``Int.Linear.norm_eq_coeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
else
let r := mkConst ``False
let h := mkApp5 (mkConst ``Int.Linear.eq_eq_false_of_divCoeff) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr (Int.ofNat k)) reflBoolTrue
let h := mkApp5 (mkConst ``Int.Linear.eq_eq_false_of_divCoeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr (Int.ofNat k)) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
@ -79,11 +79,11 @@ def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr))
let p := a.sub b |>.norm
if p.isUnsatLe then
let r := mkConst ``False
let h := mkApp4 (mkConst ``Int.Linear.le_eq_false) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
let h := mkApp4 (mkConst ``Int.Linear.le_eq_false) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
else if p.isValidLe then
let r := mkConst ``True
let h := mkApp4 (mkConst ``Int.Linear.le_eq_true) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
let h := mkApp4 (mkConst ``Int.Linear.le_eq_true) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
else if checkIfModified && p.toExpr == a && b == .num 0 then
return none
@ -91,16 +91,16 @@ def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr))
let k := p.gcdCoeffs'
if k == 1 then
let r := mkIntLE (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
let h := mkApp5 (mkConst ``Int.Linear.norm_le) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
let h := mkApp5 (mkConst ``Int.Linear.norm_le) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
else
let tight := p.getConst % k != 0
let p := p.div k
let r := mkIntLE (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
let h := if tight then
mkApp6 (mkConst ``Int.Linear.norm_le_coeff_tight) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
let h ← if tight then
pure <| mkApp6 (mkConst ``Int.Linear.norm_le_coeff_tight) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
else
mkApp6 (mkConst ``Int.Linear.norm_le_coeff) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
pure <| mkApp6 (mkConst ``Int.Linear.norm_le_coeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
return some (r, ← mkExpectedTypeHint h (← mkEq e r))
def simpRel? (e : Expr) : MetaM (Option (Expr × Expr)) := do
@ -151,14 +151,14 @@ def simpDvd? (e : Expr) : MetaM (Option (Expr × Expr)) := do
if e == p.toExpr then
return none
let rhs := mkIntDvd (toExpr d') (← p.denoteExpr (atoms[·]!))
let h := if g == 1 then
mkApp5 (mkConst ``Int.Linear.norm_dvd) (toContextExpr atoms) (toExpr d) (toExpr e) (toExpr p) reflBoolTrue
let h ← if g == 1 then
pure <| mkApp5 (mkConst ``Int.Linear.norm_dvd) (← toContextExpr atoms) (toExpr d) (toExpr e) (toExpr p) reflBoolTrue
else
mkApp7 (mkConst ``Int.Linear.norm_dvd_gcd) (toContextExpr atoms) (toExpr d) (toExpr e) (toExpr d') (toExpr p) (toExpr g) reflBoolTrue
pure <| mkApp7 (mkConst ``Int.Linear.norm_dvd_gcd) (← toContextExpr atoms) (toExpr d) (toExpr e) (toExpr d') (toExpr p) (toExpr g) reflBoolTrue
return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
else
let rhs := mkConst ``False
let h := mkApp4 (mkConst ``Int.Linear.dvd_eq_false) (toContextExpr atoms) (toExpr d) (toExpr e) reflBoolTrue
let h := mkApp4 (mkConst ``Int.Linear.dvd_eq_false) (← toContextExpr atoms) (toExpr d) (toExpr e) reflBoolTrue
return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
def simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr)) := do
@ -167,7 +167,7 @@ def simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr)) := do
let e' := p.toExpr
if e != e' then
-- We only return some if monomials were fused
let h := mkApp4 (mkConst ``Int.Linear.Expr.eq_of_norm_eq) (toContextExpr atoms) (toExpr e) (toExpr p) reflBoolTrue
let h := mkApp4 (mkConst ``Int.Linear.Expr.eq_of_norm_eq) (← toContextExpr atoms) (toExpr e) (toExpr p) reflBoolTrue
let rhs ← p.denoteExpr (atoms[·]!)
return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
else

2
src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean
View file

@ -179,7 +179,7 @@ def toLinearCnstr? (e : Expr) : MetaM (Option (LinearCnstr × Array Expr)) := do
let c := c.applyPerm perm
return some (c, atoms)
def toContextExpr (ctx : Array Expr) : Expr :=
def toContextExpr (ctx : Array Expr) : MetaM Expr := do
if h : 0 < ctx.size then
RArray.toExpr (mkConst ``Nat) id (RArray.ofArray ctx h)
else

8
src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean
View file

@ -18,17 +18,17 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
let c₂ := c₁.norm
if c₂.isUnsat then
let r := mkConst ``False
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (toContextExpr atoms) (toExpr c) reflBoolTrue
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr atoms) (toExpr c) reflBoolTrue
return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
else if c₂.isValid then
let r := mkConst ``True
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (toContextExpr atoms) (toExpr c) reflBoolTrue
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr atoms) (toExpr c) reflBoolTrue
return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
else
let c₂ : LinearCnstr := c₂.toExpr
let r ← c₂.toArith atoms
if r != lhs then
let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (toContextExpr atoms) (toExpr c) (toExpr c₂) reflBoolTrue
let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr atoms) (toExpr c) (toExpr c₂) reflBoolTrue
return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
else
return none
@ -74,7 +74,7 @@ def simpExpr? (input : Expr) : MetaM (Option (Expr × Expr)) := do
let e' : LinearExpr := p'.toExpr
if e' == e then
return none
let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
let r ← e'.toArith ctx
return some (r, ← mkExpectedTypeHint p (← mkEq input r))

2
tests/lean/run/liaByRefl.lean
View file

@ -7,7 +7,7 @@ elab tk:"#R[" ts:term,* "]" : term => do
let ts : Array Lean.Syntax := ts
let es ← ts.mapM fun stx => Lean.Elab.Term.elabTerm stx none
if h : 0 < es.size then
return (Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h))
Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h)
else
throwErrorAt tk "RArray cannot be empty"

2
tests/lean/run/linearByRefl.lean
View file

@ -7,7 +7,7 @@ elab tk:"#R[" ts:term,* "]" : term => do
let ts : Array Lean.Syntax := ts
let es ← ts.mapM fun stx => Lean.Elab.Term.elabTerm stx none
if h : 0 < es.size then
return (Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h))
Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h)
else
throwErrorAt tk "RArray cannot be empty"

2
tests/lean/run/som1.lean
View file

@ -7,7 +7,7 @@ elab tk:"#R[" ts:term,* "]" : term => do
let ts : Array Lean.Syntax := ts
let es ← ts.mapM fun stx => Lean.Elab.Term.elabTerm stx none
if h : 0 < es.size then
return (Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h))
Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h)
else
throwErrorAt tk "RArray cannot be empty"