Skip to content

Commit 1a4428f

Browse files
SimonGuilloudSimonGuilloud
committed
add a tactic _INST_TYPE_RENAME that rename variable symbols to maintain invariants that variables ids are unique per types.
1 parent c046c74 commit 1a4428f

4 files changed

Lines changed: 191 additions & 6 deletions

File tree

‎lisa-hol/src/main/scala/lisa/hol/ExtendedHOLSteps.scala‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
package lisa.hol
2+
import lisa.SetTheoryLibrary
3+
import lisa.automation._
4+
import lisa.hol.VarsAndFunctions._
5+
import lisa.maths.SetTheory.Base.Predef.∈
6+
import lisa.maths.SetTheory.Functions.Predef.{_, given}
7+
import lisa.maths.SetTheory.Types
8+
import lisa.maths.SetTheory.Types.Tactics.Typecheck
9+
import lisa.utils.K
10+
import lisa.utils.UserLisaException
11+
import lisa.utils.fol.FOL._
12+
import lisa.utils.prooflib.BasicStepTactic._
13+
import lisa.utils.prooflib.ProofTacticLib.ProofTactic
14+
import scala.collection.mutable
15+
16+
import SetTheoryLibrary.{have, JUSTIFICATION, thesis, THM, Proof, Theorem}
17+
import lisa.utils.prooflib.BasicStepTactic.Weakening
18+
19+
import lisa.hol.Import.mkTypedVar
20+
21+
22+
object ExtendedHOLSteps {
23+
24+
import lisa.hol.HOLHelperTheorems.{One, nonEmptyFuncSpace, assume, eqRefl}
25+
import K.repr
26+
27+
28+
29+
object _INST_TYPE_RENAME extends ProofTactic {
30+
def allTypedVars(e: Expr[?]): Set[(TypedVariable, Expr[Ind])] = e match
31+
case v: TypedVariable => Set((v, v.typ))
32+
case App(func, arg) => allTypedVars(func) ++ allTypedVars(arg)
33+
case Abs(v: TypedVariable, body) =>
34+
allTypedVars(body) + ((v, v.typ): (TypedVariable, Expr[Ind]))
35+
case Abs(v, body) => allTypedVars(v) ++ allTypedVars(body)
36+
case _ => Set.empty
37+
38+
def variableTypesNames(using proof: Proof)(prem: proof.Fact): proof.ProofTacticJudgement = TacticSubproof { ip ?=>
39+
val variablesSubst : mutable.Map[Variable[Ind], Variable[Ind]] = mutable.Map.empty
40+
val allvars = prem.statement.left.flatMap(allTypedVars) ++ prem.statement.right.flatMap(allTypedVars)
41+
val varsToChange: Map[Variable[Ind], TypedVariable] =
42+
allvars.collect { case (v, typ) if v.id.no != typ.hashCode().abs => (v, mkTypedVar(v.id.name, typ)) }.toMap
43+
44+
def changeVarInExpr[A](e: Expr[A]): Expr[A] = e match
45+
case v: Variable[?] =>
46+
varsToChange.toMap.getOrElse(v, v).asInstanceOf[Variable[A]]
47+
case Abs(v: Variable[?], body) =>
48+
val targetVar = varsToChange.toMap.getOrElse(v, v)
49+
val targetBody = changeVarInExpr(body)
50+
if (targetVar eq v) && (targetBody eq body) then e else
51+
Abs(targetVar, targetBody).asInstanceOf[Expr[A]]
52+
case App(func, arg) =>
53+
val targetFunc = changeVarInExpr(func)
54+
val targetArg = changeVarInExpr(arg)
55+
if (targetFunc eq func ) && (targetArg eq arg) then e else
56+
App(targetFunc, targetArg)
57+
case cst: Constant[A] => cst
58+
val targetSequent = prem.statement.left.map(changeVarInExpr) |- prem.statement.right.map(changeVarInExpr)
59+
val instPrem = prem.of( (varsToChange.map { case (from, to) => from := to}).toSeq* )
60+
have(targetSequent) by Restate.from(instPrem)
61+
}
62+
63+
def apply(using proof: Proof)(inst: Seq[(Variable[Ind], Expr[Ind])], prem: proof.Fact): proof.ProofTacticJudgement = TacticSubproof { ip ?=>
64+
val s1 = have(lisa.hol.HOLSteps._INST_TYPE(inst, prem))
65+
have(variableTypesNames(s1))
66+
}
67+
68+
}
69+
}
70+
71+
/*
72+
prelForm.underlying: app(app(=:=(Pi(Pi(A)(lambda(x, B)))(lambda(x, 𝔹))))(app(=:=(Pi(A)(lambda(x, B))))(z)))(app(abs(Pi(A)(lambda(x, B)))(lambda(x, abs(Pi(A)(lambda(x, B)))(lambda(y, app(app(=:=(Pi(A)(lambda(x, B))))(x))(y))))))(z)) === One
73+
targetForm.underlying: app(app(=:=(Pi(Pi(A)(lambda(x_196788543, B)))(lambda(x_196788543, 𝔹))))(app(=:=(Pi(A)(lambda(x_196788543, B))))(z_196788543)))(app(abs(Pi(A)(lambda(x_196788543, B)))(lambda(x_196788543, abs(Pi(A)(lambda(x_196788543, B)))(lambda(y_196788543, app(app(=:=(Pi(A)(lambda(x_196788543, B))))(x_196788543))(y_196788543))))))(z_196788543)) === One
74+
*/

‎lisa-hol/src/main/scala/lisa/hol/HOLExtStepsTests.scala‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
package lisa.hol
2+
3+
import lisa.automation.Substitution.{Apply => Substitute}
4+
import lisa.hol.HOLHelperTheorems._
5+
import lisa.hol.HOLSteps._
6+
import lisa.hol.VarsAndFunctions._
7+
import lisa.maths.SetTheory.Base.Pair.given
8+
import lisa.maths.SetTheory.Base.Replacement.|
9+
import lisa.maths.SetTheory.Types.Tactics.Typecheck
10+
import lisa.maths.SetTheory.Types.TypingRules.BetaReduction
11+
import lisa.maths.SetTheory.Types.TypingRules.TAbs
12+
import lisa.utils.prooflib.BasicStepTactic._
13+
import lisa.utils.prooflib.Library
14+
import lisa.utils.prooflib.ProofTacticLib._
15+
import lisa.utils.prooflib.SimpleDeducedSteps._
16+
import lisa.utils.unification.UnificationUtils.Substitution
17+
import lisa.utils.prooflib.BasicStepTactic.RightSubstEq
18+
import lisa.utils.prooflib.BasicStepTactic.Restate
19+
import lisa.utils.prooflib.BasicStepTactic.RightAnd
20+
import lisa.utils.prooflib.BasicStepTactic.Weakening
21+
import lisa.utils.prooflib.BasicStepTactic.RightSubstEq
22+
import lisa.utils.prooflib.BasicStepTactic.Weakening
23+
import lisa.utils.unification.UnificationUtils.Substitution
24+
import lisa.utils.prooflib.BasicStepTactic.RightSubstEq
25+
import lisa.utils.prooflib.SimpleDeducedSteps.Discharge
26+
import lisa.utils.unification.UnificationUtils.Substitution
27+
import lisa.utils.prooflib.BasicStepTactic.LeftSubstEq
28+
29+
import lisa.hol.ExtendedHOLSteps._INST_TYPE_RENAME
30+
import lisa.hol.Import.mkTypedVar
31+
32+
import lisa.hol.HOLBasics.{SYM}
33+
34+
object HOLExtStepsTests extends lisa.HOL {
35+
draft()
36+
37+
val A = typevar
38+
val B = typevar
39+
val T = typevar
40+
41+
val x = typedvar(A)
42+
val y = typedvar(A)
43+
val z = typedvar(A)
44+
val P = typedvar(A ->: 𝔹)
45+
46+
val f = typedvar(A ->: B)
47+
val g = typedvar(A ->: B)
48+
49+
val p = typedvar(𝔹)
50+
val q = typedvar(𝔹)
51+
52+
val φ = variable[Prop]
53+
54+
val lib = summon[Library]
55+
56+
57+
val holeqBetaReduced = HOLTheorem(
58+
holeq(A) =:= fun(x, fun(y, x =:= y))
59+
):
60+
SYM(TRANS(
61+
ABS(x)( // fun(x, fun(y, x =:= y)) =:= fun(x, holeq(A) * x)
62+
ETA(y, holeq(A) * x) // fun(y, holeq(A) * x * y) =:= holeq(A) * x
63+
),
64+
ETA(x, holeq(A)) // fun(x, holeq(A) * x) =:= holeq(A)
65+
))
66+
67+
val holeqBetaReducedFull = HOLTheorem(
68+
holeq(A)*z*z =:= fun(x, fun(y, x =:= y))*z*z
69+
):
70+
sorry
71+
72+
73+
74+
75+
val xb = mkTypedVar("x", B)
76+
val yb = mkTypedVar("y", B)
77+
val instTypeTest1 = HOLTheorem(
78+
holeq(B) =:= fun(xb, fun(yb, xb =:= yb))
79+
):
80+
have(_INST_TYPE_RENAME(Seq((A, B)), holeqBetaReduced))
81+
82+
83+
84+
val xba = mkTypedVar("x", A ->: B)
85+
val yba = mkTypedVar("y", A ->: B)
86+
val instTypeTest2 = HOLTheorem(
87+
holeq(A ->: B) =:= fun(xba, fun(yba, xba =:= yba))
88+
):
89+
have(_INST_TYPE_RENAME(Seq((A, A ->: B)), holeqBetaReduced))
90+
91+
92+
93+
val fba = mkTypedVar("f", A ->: B)
94+
val zba = mkTypedVar("z", A ->: B)
95+
val instTypeTest3 = HOLTheorem(
96+
(holeq(A ->: B)*zba*zba) =:= (fun(xba, fun(yba, xba =:= yba))*zba*zba)
97+
):
98+
val s1 = have(_INST_TYPE_RENAME(Seq((A, A ->: B)), holeqBetaReducedFull))
99+
100+
101+
102+
103+
val instTypeTest4 = HOLTheorem(
104+
(holeq(A ->: B)*fba*fba) =:= (fun(xba, fun(yba, xba =:= yba))*fba*fba)
105+
):
106+
val s1 = have(_INST_TYPE_RENAME(Seq((A, A ->: B)), holeqBetaReducedFull))
107+
have(_INST(Seq((zba, fba)), s1))
108+
109+
}

‎lisa-hol/src/main/scala/lisa/hol/Import.scala‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,10 @@ object Import extends lisa.HOL:
5050
import Logging.*
5151
private var currentLoggingMode: LoggingMode = LoggingMode.Silent
5252
given LoggingMode = currentLoggingMode
53-
53+
def mkTypedVar(name: String, tpe: Expr[Ind]): TypedVariable =
54+
// unfortunate to double the clashes, but identifier indices are
55+
// expected to be positive
56+
TypedVariable(K.Identifier(name, tpe.hashCode().abs), tpe)
5457
private object Transformers:
5558

5659
extension (typ: h.Type)
@@ -73,13 +76,12 @@ object Import extends lisa.HOL:
7376
// this is runtime checked wherever used
7477
(typeConstant #@@ typeArgs).asInstanceOf
7578

79+
80+
7681
extension (v: h.Variable)
7782
def toLisaVar : TypedVariable =
7883
val tpe = v.tpe.toLisaType
79-
// unfortunate to double the clashes, but identifier indices are
80-
// expected to be positive
81-
val name = K.Identifier(v.name, v.tpe.hashCode().abs)
82-
TypedVariable(name, tpe)
84+
mkTypedVar(name, tpe)
8385

8486
extension (v: h.TypeVariable)
8587
def toLisaVar : TypeVariable =

‎lisa-sets/src/main/scala/lisa/maths/SetTheory/Relations/WellFoundedRelation.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
package lisa.maths.SetTheory.Relations
22

3-
import lisa.maths.SetTheory.Base.Predef._
3+
import lisa.maths.SetTheory.Base.Predef.{_, given}
44
import lisa.maths.SetTheory.Functions.Predef._
55
import lisa.maths.SetTheory.Order.Extrema.minimal
66

0 commit comments

Comments
 (0)