Skip to content

Commit

Permalink
Drop polymorphic Type/Sort level restrictions (part 1). (#151)
Browse files Browse the repository at this point in the history
  • Loading branch information
@abdoo8080
abdoo8080 authored Nov 27, 2024
1 parent 9cc24d5 commit 3afa2c8
Show file tree
Hide file tree
Showing 16 changed files with 140 additions and 107 deletions.
33 changes: 20 additions & 13 deletions Smt/Reconstruct.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,17 @@ namespace Smt
open Lean
open Attribute

structure Reconstruct.state where
userNames : Std.HashMap String FVarId
termCache : Std.HashMap cvc5.Term Expr
proofCache : Std.HashMap cvc5.Proof Expr
count : Nat
currAssums : Array Expr
skippedGoals : Array MVarId
structure Reconstruct.Context where
userNames : Std.HashMap String FVarId := {}

abbrev ReconstructM := StateT Reconstruct.state MetaM
structure Reconstruct.State where
termCache : Std.HashMap cvc5.Term Expr := {}
proofCache : Std.HashMap cvc5.Proof Expr := {}
count : Nat := 0
currAssums : Array Expr := #[]
skippedGoals : Array MVarId := #[]

abbrev ReconstructM := ReaderT Reconstruct.Context (StateT Reconstruct.State MetaM)

abbrev SortReconstructor := cvc5.Sort → ReconstructM (Option Expr)

Expand Down Expand Up @@ -57,6 +59,11 @@ where
return e
throwError "Failed to reconstruct sort {s} with kind {s.getKind}"

def reconstructSortLevelAndSort (s : cvc5.Sort) : ReconstructM (Level × Expr) := do
let t ← reconstructSort s
let .sort u ← Meta.inferType t | throwError "expected a sort, but got\n{t}"
return ⟨u, t⟩

def withNewTermCache (k : ReconstructM α) : ReconstructM α := do
let termCache := (← get).termCache
modify fun state => { state with termCache := {} }
Expand Down Expand Up @@ -181,10 +188,10 @@ def traceReconstructProof (r : Except Exception (Expr × Expr × List MVarId)) :
| _ => m!"{bombEmoji}"

open Qq in
partial def reconstructProof (pf : cvc5.Proof) (fvNames : Std.HashMap String FVarId) : MetaM (Expr × Expr × List MVarId) := do
partial def reconstructProof (pf : cvc5.Proof) (userNames : Std.HashMap String FVarId) : MetaM (Expr × Expr × List MVarId) := do
withTraceNode `smt.reconstruct.proof traceReconstructProof do
let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨fvNames, {}, {}, 0, #[], #[]⟩
let (h, .mk _ _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state
let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run { userNames } {}
let (h, ⟨_, _, _, _, mvs⟩) ← (Reconstruct.reconstructProof pf).run { userNames } state
if pf.getArguments.isEmpty then
let h : Q(True → $p) ← pure h
return (p, q($h trivial), mvs.toList)
Expand Down Expand Up @@ -231,13 +238,13 @@ open Lean.Elab Tactic in
match r with
| .error e => logInfo (repr e)
| .ok pf =>
let (p, hp, mvs) ← reconstructProof pf (← getFVarNames)
let (p, hp, mvs) ← reconstructProof pf (← getUserNames)
let mv ← Tactic.getMainGoal
let mv ← mv.assert (Name.num `s 0) p hp
let (_, mv) ← mv.intro1
replaceMainGoal (mv :: mvs)
where
getFVarNames : MetaM (Std.HashMap String FVarId) := do
getUserNames : MetaM (Std.HashMap String FVarId) := do
let lCtx ← getLCtx
return lCtx.getFVarIds.foldl (init := {}) fun m fvarId =>
m.insert (lCtx.getRoundtrippingUserName? fvarId).get!.toString fvarId
Expand Down
55 changes: 30 additions & 25 deletions Smt/Reconstruct/Builtin.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,10 @@ open Lean Qq

@[smt_sort_reconstruct] def reconstructBuiltinSort : SortReconstructor := fun s => do match s.getKind with
| .FUNCTION_SORT =>
let mut ct : Q(Type) ← reconstructSort s.getFunctionCodomainSort!
let f s (a : Q(Type)) := do
let t : Q(Type) ← reconstructSort s
return q($t → $a)
let ct ← reconstructSort s.getFunctionCodomainSort!
let f := fun s a => do
let t ← reconstructSort s
return .forallE .anonymous t a .default
let t ← s.getFunctionDomainSorts!.foldrM f ct
return t
| _ => return none
Expand All @@ -30,32 +30,37 @@ def getFVarExpr! (n : Name) : MetaM Expr := do
| none => throwError "unknown free variable '{n}'"

def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
match (← get).userNames[n]? with
match (← read).userNames[n]? with
| some fv => return .fvar fv
| none => match (← getLCtx).findFromUserName? n.toName with
| some d => return d.toExpr
| none =>
let c ← getConstInfo n.toName
return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])

def buildDistinct (u : Level) (α : Q(Sort u)) (xs : List Q($α)) : Q(Prop) :=
go xs
where
go : List Q($α) → Q(Prop)
| [] => q(True)
| [_] => q(True)
| [x, y] => q($x ≠ $y)
| x :: ys => ys.foldr (fun y ys => q($x ≠ $y ∧ $ys)) (go ys)

@[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with
| .VARIABLE => getFVarExpr! (getVariableName t)
| .CONSTANT => getFVarOrConstExpr! t.getSymbol!
| .EQUAL =>
let α : Q(Type) ← reconstructSort t[0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort t[0]!.getSort
let x : Q($α) ← reconstructTerm t[0]!
let y : Q($α) ← reconstructTerm t[1]!
return q($x = $y)
| .DISTINCT =>
let n := t.getNumChildren
let α : Q(Type) ← reconstructSort t[0]!.getSort
let mut xs : Q(List $α) := q([])
for i in [0:n] do
let x : Q($α) ← reconstructTerm t[n - i - 1]!
xs := q($x :: $xs)
return q(Builtin.distinct $xs)
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort t[0]!.getSort
let xs ← t.getChildren.mapM reconstructTerm
return buildDistinct u α xs.toList
| .ITE =>
let α : Q(Type) ← reconstructSort t.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort t.getSort
let c : Q(Prop) ← reconstructTerm t[0]!
let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
let x : Q($α) ← reconstructTerm t[1]!
Expand All @@ -77,60 +82,60 @@ where
def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
match pf.getRewriteRule with
| .DISTINCT_ELIM =>
let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getResult[0]!.getSort
let t : Q($α) ← reconstructTerm pf.getResult[0]!
let t' : Q($α) ← reconstructTerm pf.getResult[1]!
addThm q($t = $t') q(Eq.refl $t)
| .ITE_TRUE_COND =>
let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[1]!.getSort
let x : Q($α) ← reconstructTerm pf.getArguments[1]!
let y : Q($α) ← reconstructTerm pf.getArguments[2]!
addThm q(ite True $x $y = $x) q(@Builtin.ite_true_cond $α $x $y)
| .ITE_FALSE_COND =>
let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[1]!.getSort
let x : Q($α) ← reconstructTerm pf.getArguments[1]!
let y : Q($α) ← reconstructTerm pf.getArguments[2]!
addThm q(ite False $x $y = $y) q(@Builtin.ite_false_cond $α $x $y)
| .ITE_NOT_COND =>
let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[2]!.getSort
let x : Q($α) ← reconstructTerm pf.getArguments[2]!
let y : Q($α) ← reconstructTerm pf.getArguments[3]!
let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
addThm q(ite (¬$c) $x $y = ite $c $y $x) q(@Builtin.ite_not_cond $c $α $x $y $h)
| .ITE_EQ_BRANCH =>
let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[2]!.getSort
let x : Q($α) ← reconstructTerm pf.getArguments[2]!
let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
addThm q(ite $c $x $x = $x) q(@Builtin.ite_eq_branch $c $α $x $h)
| .ITE_THEN_LOOKAHEAD =>
let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[2]!.getSort
let x : Q($α) ← reconstructTerm pf.getArguments[2]!
let y : Q($α) ← reconstructTerm pf.getArguments[3]!
let z : Q($α) ← reconstructTerm pf.getArguments[4]!
let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
addThm q(ite $c (ite $c $x $y) $z = ite $c $x $z) q(@Builtin.ite_then_lookahead $c $α $x $y $z $h)
| .ITE_ELSE_LOOKAHEAD =>
let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[2]!.getSort
let x : Q($α) ← reconstructTerm pf.getArguments[2]!
let y : Q($α) ← reconstructTerm pf.getArguments[3]!
let z : Q($α) ← reconstructTerm pf.getArguments[4]!
let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
addThm q(ite $c $x (ite $c $y $z) = ite $c $x $z) q(@Builtin.ite_else_lookahead $c $α $x $y $z $h)
| .ITE_THEN_NEG_LOOKAHEAD =>
let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[2]!.getSort
let x : Q($α) ← reconstructTerm pf.getArguments[2]!
let y : Q($α) ← reconstructTerm pf.getArguments[3]!
let z : Q($α) ← reconstructTerm pf.getArguments[4]!
let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
addThm q(ite $c (ite (¬$c) $x $y) $z = ite $c $y $z) q(@Builtin.ite_then_neg_lookahead $c $α $x $y $z $h)
| .ITE_ELSE_NEG_LOOKAHEAD =>
let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[2]!.getSort
let x : Q($α) ← reconstructTerm pf.getArguments[2]!
let y : Q($α) ← reconstructTerm pf.getArguments[3]!
let z : Q($α) ← reconstructTerm pf.getArguments[4]!
Expand Down Expand Up @@ -158,7 +163,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
mv.assign h₂
addThm q(andN $ps → $q) q(Builtin.scopes $h₁)
| .EVALUATE =>
let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getResult[0]!.getSort
let t : Q($α) ← reconstructTerm pf.getResult[0]!
let t' : Q($α) ← reconstructTerm pf.getResult[1]!
if pf.getResult[0]! == pf.getResult[1]! then
Expand Down Expand Up @@ -237,7 +242,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]!
addThm q(ite $c $p $q ∨ ¬$p ∨ ¬$q) q(@Builtin.cnfIteNeg3 $c $p $q $h)
| .SKOLEM_INTRO =>
let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getResult[0]!.getSort
let k : Q($α) ← reconstructTerm pf.getResult[0]!
let t : Q($α) ← reconstructTerm pf.getResult[1]!
addThm q($k = $t) q(Eq.refl $t)
Expand Down
6 changes: 0 additions & 6 deletions Smt/Reconstruct/Builtin/Lemmas.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,6 @@ import Smt.Reconstruct.Util

namespace Smt.Reconstruct.Builtin

@[reducible] def distinct : List α → Prop
| [] => True
| [_] => True
| [x, y] => x ≠ y
| x :: ys => ys.foldr (x ≠ · ∧ ·) (distinct ys)

theorem iteElim1 [hc : Decidable c] : ite c a b → ¬ c ∨ a := by
intros h
cases hc with
Expand Down
2 changes: 1 addition & 1 deletion Smt/Reconstruct/Prop.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -288,7 +288,7 @@ def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : Rec
@[smt_proof_reconstruct] def reconstructPropProof : ProofReconstructor := fun pf => do match pf.getRule with
| .DSL_REWRITE => reconstructRewrite pf
| .ITE_EQ =>
let α : Q(Type) ← reconstructSort pf.getArguments[0]![1]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getArguments[0]![1]!.getSort
let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]!
let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
let x : Q($α) ← reconstructTerm pf.getArguments[0]![1]!
Expand Down
40 changes: 23 additions & 17 deletions Smt/Reconstruct/Quant.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ where
xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort)
let F := q[1]!
for i in [0:n + 1] do
let α : Q(Type) ← reconstructSort q[0]![i]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort q[0]![i]!.getSort
let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
let e ← Meta.withLocalDeclsD xs fun xs => withNewTermCache do
let F ← reconstructTerm F
Expand All @@ -89,7 +89,7 @@ where
def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
match pf.getRewriteRule with
| .BETA_REDUCE =>
let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getResult[0]!.getSort
let t : Q($α) ← reconstructTerm pf.getResult[0]!
let t' : Q($α) ← reconstructTerm pf.getResult[1]!
addThm q($t = $t') q(Eq.refl $t)
Expand All @@ -101,7 +101,8 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
let b : Q(Prop) ← reconstructTerm pf.getResult[0]![1]!
let h := q(Classical.not_not_eq $b)
let f := fun x (p, q, h) => do
let α : Q(Type) ← Meta.inferType x
let u ← Meta.getLevel (← Meta.inferType x)
let α : Q(Sort u) ← Meta.inferType x
let lp : Q($α → Prop) ← Meta.mkLambdaFVars #[x] p
let lq : Q($α → Prop) ← Meta.mkLambdaFVars #[x] q
let hx : Q(∀ x : $α, (¬$lp x) = $lq x) ← Meta.mkLambdaFVars #[x] h
Expand All @@ -119,7 +120,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
let b : Q(Prop) ← reconstructTerm pf.getResult[0]![1]!
let h : Q($b = $b) := q(Eq.refl $b)
let f := fun i (j, p, q, (h : Q($p = $q))) => do
let α : Q(Type) ← reconstructSort pf.getResult[0]![0]![i]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getResult[0]![0]![i]!.getSort
if let some j := j then
if pf.getResult[0]![0]![i]! == pf.getResult[1]![0]![j]! then
let lp : Q($α → Prop) ← Meta.mkLambdaFVars #[ys[j]!] p
Expand All @@ -136,7 +137,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
(List.range i).foldrM f (j, b, b, h)
addThm q($p = $q) h
| .QUANT_MERGE_PRENEX =>
let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getResult[0]!.getSort
let t : Q($α) ← reconstructTerm pf.getResult[0]!
let t' : Q($α) ← reconstructTerm pf.getResult[1]!
addThm q($t = $t') q(Eq.refl $t)
Expand All @@ -151,14 +152,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
ps := ps.push q($p)
let b : Q(Prop) ← reconstructTerm pf.getResult[0]![1]!
let h : Q($b = $b) := q(Eq.refl $b)
let lf := fun x (α : Q(Type)) p lps => do
let lf := fun x (u, (α : Q(Sort u))) p lps => do
let lp : Q($α → Prop) ← (return ← Meta.mkLambdaFVars #[x] p)
return q($lp :: $lps)
return .app q(PList.cons $lp) lps
let f := fun x (p, ps, h) => do
let α : Q(Type) ← Meta.inferType x
let u ← Meta.getLevel (← Meta.inferType x)
let α : Q(Sort u) ← Meta.inferType x
let lp : Q($α → Prop) ← Meta.mkLambdaFVars #[x] p
let lps : Q(List ($α → Prop)) ← ps.foldrM (lf x α) q([])
let hx : Q(∀ x, $lp x = andN («$lps».map (· x))) ← Meta.mkLambdaFVars #[x] h
let (lps : Q(PList ($α → Prop))) ← ps.foldrM (lf x (u, α)) q(@PList.nil ($α → Prop))
let hx : Q(∀ x, $lp x = pAndN («$lps».map (· x))) ← Meta.mkLambdaFVars #[x] h
let ap ← Meta.mkForallFVars #[x] p
let aps ← liftM (ps.mapM (Meta.mkForallFVars #[x]))
return (ap, aps, q(Eq.trans (forall_congr $hx) (@miniscope_andN $α $lps)))
Expand All @@ -181,7 +183,8 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
let b : Q(Prop) ← reconstructTerm pf.getResult[0]![1]!
let h : Q($b = $b) := q(Eq.refl $b)
let fin := fun x (p, ps, q, rs, h) => do
let α : Q(Type) ← Meta.inferType x
let u ← Meta.getLevel (← Meta.inferType x)
let α : Q(Sort u) ← Meta.inferType x
let lp : Q($α → Prop) ← Meta.mkLambdaFVars #[x] p
let lq : Q($α → Prop) ← Meta.mkLambdaFVars #[x] q
let qps : Q(List Prop) ← pure (ps.foldr (fun (p : Q(Prop)) qps => q($p :: $qps)) q([]))
Expand All @@ -198,7 +201,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
| .QUANT_VAR_ELIM_EQ =>
let lb := pf.getResult[0]![1]!
if lb.getKind == .OR then
let α : Q(Type) ← reconstructSort lb[0]![0]![0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort lb[0]![0]![0]!.getSort
let n : Name := getVariableName lb[0]![0]![0]!
let t : Q($α) ← reconstructTerm lb[0]![0]![1]!
let p : Q($α → Prop) ← Meta.withLocalDeclD n α fun x => withNewTermCache do
Expand All @@ -209,7 +212,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
Meta.mkLambdaFVars #[x] b
addThm (← reconstructTerm pf.getResult) q(@Quant.var_elim_eq_or $α $t $p)
else
let α : Q(Type) ← reconstructSort lb[0]![0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort lb[0]![0]!.getSort
let t : Q($α) ← reconstructTerm lb[0]![1]!
addThm (← reconstructTerm pf.getResult) q(@Quant.var_elim_eq $α $t)
| _ => return none
Expand All @@ -233,7 +236,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
es := es.push (← reconstructTerm t)
addThm (← reconstructTerm pf.getResult) (mkAppN xsF es)
| .ALPHA_EQUIV =>
let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort
let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort pf.getResult[0]!.getSort
let t : Q($α) ← reconstructTerm pf.getResult[0]!
let t' : Q($α) ← reconstructTerm pf.getResult[1]!
addThm q($t = $t') q(Eq.refl $t)
Expand Down Expand Up @@ -269,7 +272,8 @@ where
let q : Q(Prop) ← reconstructTerm pf.getResult[1]![1]!
let h : Q($p = $q) ← reconstructProof pf.getChildren[0]!
let f := fun x (p, q, h) => do
let α : Q(Type) ← Meta.inferType x
let u ← Meta.getLevel (← Meta.inferType x)
let α : Q(Sort u) ← Meta.inferType x
let lp : Q($α → Prop) ← Meta.mkLambdaFVars #[x] p
let lq : Q($α → Prop) ← Meta.mkLambdaFVars #[x] q
let hx : Q(∀ x : $α, $lp x = $lq x) ← Meta.mkLambdaFVars #[x] h
Expand All @@ -287,7 +291,8 @@ where
let q : Q(Prop) ← reconstructTerm pf.getResult[1]![1]!
let h : Q($p = $q) ← reconstructProof pf.getChildren[0]!
let f := fun x (p, q, h) => do
let α : Q(Type) ← Meta.inferType x
let u ← Meta.getLevel (← Meta.inferType x)
let α : Q(Sort u) ← Meta.inferType x
let lp : Q($α → Prop) ← Meta.mkLambdaFVars #[x] p
let lq : Q($α → Prop) ← Meta.mkLambdaFVars #[x] q
let hx : Q(∀ x : $α, $lp x = $lq x) ← Meta.mkLambdaFVars #[x] h
Expand All @@ -300,7 +305,8 @@ where
let chRes := pf.getChildren[0]!.getResult
let es ← reconstructQuant.reconstructForallSkolems chRes[0]! (chRes[0]![0]!.getNumChildren - 1)
let f := fun h e => do
let α : Q(Type) ← pure (e.getArg! 0)
let u ← Meta.getLevel (e.getArg! 0)
let α : Q(Sort u) ← pure (e.getArg! 0)
let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
let .lam n _ (.app _ b) bi := e.getArg! 2 | throwError "[skolemize]: expected a predicate with a negated body: {e}"
let p : Q($α → Prop) ← pure (.lam n α b bi)
Expand Down
Loading

0 comments on commit 3afa2c8

Please sign in to comment.