diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean index 1020cc9..1330d55 100644 --- a/Auto/Translation/Monomorphization.lean +++ b/Auto/Translation/Monomorphization.lean @@ -223,16 +223,16 @@ def ConstInst.matchExpr (e : Expr) (ci : ConstInst) : MetaM Bool := do return false return true -/- - Given an hypothesis `t`, we will traverse the hypothesis to find - instances of polymorphic constants +/-- + Given an hypothesis `t`, we will traverse the hypothesis and + call `ConstInst.ofExpr?` to find instances of polymorphic constants\ · Binders of the hypothesis are introduced as fvars, these fvars are - recorded in `bvars` - · `param` records universe level parameters of the hypothesis are + recorded in `bvars`\ + · `param` records universe level parameters of the hypothesis\ So, the criterion that an expression `e` is a valid instance is that - · All dependent arguments and instance arguments are applied - · The head does not contain expressions in `bvars` - · Dependent arguments does not contains expressions in `bvars` + · All dependent arguments and instance arguments are present\ + · The head does not contain expressions in `bvars`\ + · Dependent arguments does not contains expressions in `bvars`\ · The expression does not contain level parameters in `params` -/ def ConstInst.ofExpr? (params : Array Name) (bvars : Array Expr) (e : Expr) : MetaM (Option ConstInst) := do @@ -651,7 +651,16 @@ where def postprocessSaturate : MonoM LemmaInsts := do let lisArr ← getLisArr let lisArr ← liftM <| lisArr.mapM (fun lis => lis.filterMapM LemmaInst.monomorphic?) + let lis := lisArr.flatMap id + -- Since typeclasses might have been instantiated during `LemmaInst.monomorphic?`, + -- we need to run ``collectConstInst`` again. Also, this must precede + -- collecting definitional equalities related to `ConstInst`s + refreshConstInsts lis -- Collect definitional equalities related to `ConstInst`s + -- **TODO:** Collect definitional equalities during monomorphization + -- and make uses of the `active` field. This is because new `ConstInst`s + -- might be generated during collection of definitional equalities, + -- and they may produce more definitional equalities let mut cieqs : Array LemmaInst := #[] let cis := ((← getCiMap).toArray.map Prod.snd).flatMap id for (ci₁, idx₁) in cis.zipWithIndex do @@ -663,16 +672,16 @@ def postprocessSaturate : MonoM LemmaInsts := do let newLi ← LemmaInst.ofLemma ⟨⟨proof, eq, .leaf "ciInstDefEq"⟩, #[]⟩ cieqs := cieqs.push newLi trace[auto.mono.ciInstDefEq] "{eq}" - -- Since typeclasses might have been instantiated during `LemmaInst.monomorphic?`, - -- and new `ConstInst`s might be produced during definitional equality + -- Since new `ConstInst`s might be produced during definitional equality -- generation, we need to ``collectConstInst`` again - let ret := lisArr.flatMap id ++ cieqs - for li in ret do - let newCis ← collectConstInsts li.params #[] li.type - for newCi in newCis do - processConstInst newCi - return ret + refreshConstInsts cieqs + return lis ++ cieqs where + refreshConstInsts (lis : LemmaInsts) : MonoM Unit := + for li in lis do + let newCis ← collectConstInsts li.params #[] li.type + for newCi in newCis do + processConstInst newCi bidirectionalOfInstanceEq (ci₁ ci₂ : ConstInst) : MetaM (Option (Expr × Expr)) := Meta.withNewMCtxDepth <| Meta.withDefault <| do return (← Expr.instanceOf? (← ci₁.toExpr) (← ci₂.toExpr)) <|> diff --git a/Doc/Monomorphization.lean b/Doc/Monomorphization.lean deleted file mode 100644 index b6142ac..0000000 --- a/Doc/Monomorphization.lean +++ /dev/null @@ -1,42 +0,0 @@ -import Lean -import Mathlib.Data.Set.Intervals.Basic -import Mathlib.FieldTheory.Fixed -import Mathlib.Algebra.Hom.Group -import Mathlib.Order.Circular - -section InstExamples - - /- - No subterm of the type of `@Bool.not_beq_false` depends on the - binder `b`, so `b` does not have to be instantiated. - -/ - set_option pp.all true in - #check @Bool.not_beq_false - - /- - No subterm of the type of `@Set.mem_Icc` depends on the binder - `a, b, x`, so `a, b, x` does not have to be instantiated - - On the other hand, the type of the bound variable `x` inside - `x ∈ Set.Icc a b ↔ a ≤ x ∧ x ≤ b` depends on `α`, so `α` - must be instantiated - -/ - #check @Set.mem_Icc - - /- - Subterm `[inst_2 : MulSemiringAction G F]` depends on both - `F` and `G`, so both `F` and `G` must be instantiated - - In fact, all the dependent `∀` binders must be instantiated, - since those apart from `F` and `G` are all `instImplicit`. - -/ - #check @FixedPoints.linearIndependent_smul_of_linearIndependent - - /- - Subterm `btw a b c` depends on `a, b` and `c`, but `btw a b c : Prop`, - so this does not count. Also no other subterms depend on `a, b` and - `c`, so they don't need to be instantiated - -/ - #check @CircularPartialOrder.btw_antisymm - -end InstExamples \ No newline at end of file diff --git a/Test/Test_Regression.lean b/Test/Test_Regression.lean index fb4ddd0..e206b5e 100644 --- a/Test/Test_Regression.lean +++ b/Test/Test_Regression.lean @@ -293,6 +293,26 @@ section ConstInstDefEq example (x y : Int) (xs ys : List α) : x + y = Int.add x y ∧ xs ++ ys = List.append xs ys := by auto + opaque mpop₁ {α} [Mul α] : α → α → α := fun _ => id + def mpop₂ := @mpop₁ + + /- + To solve this problem, Lean-auto must succeed in doing all of + the following steps consecutively + · Instantiate `α` in `h` by unifying the `@op α` in `h` + with the `@op α` in the goal. + · The `[inst : Mul α]` in `h` is instantiated by `Lemma.monomorphic?` + · The constant instance `@mpop₁ α inst` is collected and processed + · During constant instance definitional equality production + `@mpop₁ α inst` is matched with `@mpop₂ α inst` by `Expr.instanceOf?` + -/ + example + (α : Type) + (op : ∀ {α}, α → α → α) + (h : ∀ α [inst : Mul α] (x y : α), op x y = mpop₁ x y) : + ∀ α [inst : Mul α] (x y : α), op x y = mpop₂ x y := by + auto + end ConstInstDefEq -- First Order