From 3971da603ee54d373b4c73d6a20b3d83dea7b5b9 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 21 Jun 2023 16:20:25 +0200 Subject: Start working on Arith.lean --- backends/lean/Base/Arith.lean | 221 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 221 insertions(+) create mode 100644 backends/lean/Base/Arith.lean (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean new file mode 100644 index 00000000..6339f218 --- /dev/null +++ b/backends/lean/Base/Arith.lean @@ -0,0 +1,221 @@ +/- This file contains tactics to solve arithmetic goals -/ + +import Lean +import Lean.Meta.Tactic.Simp +import Init.Data.List.Basic +import Mathlib.Tactic.RunCmd +import Mathlib.Tactic.Linarith +import Base.Primitives + +/- +Mathlib tactics: +- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases +- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs +- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num +- should we use linarith or omega? +- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint +- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical +-/ + +namespace List + + -- TODO: I could not find this function?? + @[simp] def flatten {a : Type u} : List (List a) → List a + | [] => [] + | x :: ls => x ++ flatten ls + +end List + +namespace Lean + +namespace LocalContext + + open Lean Lean.Elab Command Term Lean.Meta + + -- Small utility: return the list of declarations in the context, from + -- the last to the first. + def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := + lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) [] + + -- Return the list of declarations in the context, but filter the + -- declarations which are considered as implementation details + def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do + let ls ← lctx.getAllDecls + pure (ls.filter (fun d => not d.isImplementationDetail)) + +end LocalContext + +end Lean + +namespace Arith + +open Primitives + +--set_option pp.explicit true +--set_option pp.notation false +--set_option pp.coercions false + +-- TODO: move +instance Vec.cast (a : Type): Coe (Vec a) (List a) where coe := λ v => v.val + +-- TODO: move +/- Remark: we can't write the following instance because of restrictions about + the type class parameters (`ty` doesn't appear in the return type, which is + forbidden): + + ``` + instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val + ``` + -/ +def Scalar.toInt {ty : ScalarTy} (x : Scalar ty) : Int := x.val + +-- We use this type-class to test if an expression is a scalar (if we manage +-- to lookup an instance of this type-class, then it is) +class IsScalar (a : Type) where + +instance (ty : ScalarTy) : IsScalar (Scalar ty) where + +--example (ty : ScalarTy) : IsScalar (Scalar ty) := _ + +open Lean Lean.Elab Command Term Lean.Meta + +-- Return true if the expression is a scalar expression +def isScalarExpr (e : Expr) : MetaM Bool := do + -- Try to convert the expression to a scalar + -- TODO: I tried to do it with Lean.Meta.mkAppM but it didn't work: how + -- do we allow Lean to perform (controlled) unfoldings for instantiation + -- purposes? + let r ← Lean.observing? do + let ty ← Lean.Meta.inferType e + let isScalar ← mkAppM `Arith.IsScalar #[ty] + let isScalar ← trySynthInstance isScalar + match isScalar with + | LOption.some x => some x + | _ => none + match r with + | .some _ => pure true + | _ => pure false + +-- Explore a term and return the set of scalar expressions found inside +partial def collectScalarExprsAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do + -- We do it in a very simpler manner: we deconstruct applications, + -- and recursively explore the sub-expressions. Note that we do + -- not go inside foralls and abstractions (should we?). + e.withApp fun f args => do + let hs ← if ← isScalarExpr f then pure (hs.insert f) else pure hs + let hs ← args.foldlM collectScalarExprsAux hs + pure hs + +-- Explore a term and return the list of scalar expressions found inside +def collectScalarExprs (e : Expr) : MetaM (HashSet Expr) := + collectScalarExprsAux HashSet.empty e + +-- Collect the scalar expressions in the context +def getScalarExprsFromMainCtx : Tactic.TacticM (HashSet Expr) := do + Lean.Elab.Tactic.withMainContext do + -- Get the local context + let ctx ← Lean.MonadLCtx.getLCtx + -- Just a matter of precaution + let ctx ← instantiateLCtxMVars ctx + -- Initialize the hashset + let hs := HashSet.empty + -- Explore the declarations + let decls ← ctx.getDecls + let hs ← decls.foldlM (fun hs d => collectScalarExprsAux hs d.toExpr) hs + -- Return + pure hs + + +#check TSyntax +#check mkIdent +-- TODO: addDecl? +-- Project the scalar expressions into the context, to retrieve the bound inequalities +-- def projectScalarExpr (e: Expr) : Tactic.TacticM Unit := do +-- let e ← `($e) +-- let e ← Lean.Elab.Term.elabTerm `($e) none +-- Lean.Elab.Tactic.evalCases `($e) + +elab "list_scalar_exprs" : tactic => do + let hs ← getScalarExprsFromMainCtx + hs.forM fun e => do + dbg_trace f!"+ Scalar expression: {e}" + +#check LocalContext + +elab "list_local_decls_1" : tactic => + Lean.Elab.Tactic.withMainContext do + -- Get the local context + let ctx ← Lean.MonadLCtx.getLCtx + let ctx ← instantiateLCtxMVars ctx + let decls ← ctx.getDecls + -- Filter the scalar expressions + let decls ← decls.filterMapM fun decl: Lean.LocalDecl => do + let declExpr := decl.toExpr + let declName := decl.userName + let declType ← Lean.Meta.inferType declExpr + dbg_trace f!"+ local decl: name: {declName} | expr: {declExpr} | ty: {declType}" + -- Try to convert the expression to a scalar + -- TODO: I tried to do it with Lean.Meta.mkAppM but it didn't work: how + -- do we allow Lean to perform (controlled) unfoldings for instantiation + -- purposes? + let r ← Lean.observing? do + let isScalar ← mkAppM `Arith.IsScalar #[declType] + let isScalar ← trySynthInstance isScalar + match isScalar with + | LOption.some x => some x + | _ => none + match r with + | .some _ => dbg_trace f!" Scalar expression"; pure r + | _ => dbg_trace f!" Not a scalar"; pure .none + pure () + -- match ← Lean.observing? (Lean.Meta.mkAppM `Scalar.toInt #[decl.toExpr]) with + -- | .none => dbg_trace f!" Not a scalar" + -- | .some _ => dbg_trace f!" Scalar expression" + +#check Lean.Environment.addDecl +#check Expr +#check LocalContext +#check MVarId +#check Lean.Elab.Tactic.setGoals +#check Lean.Elab.Tactic.Context +#check withLocalDecl +#check Lean.MVarId.assert +#check LocalDecl + +-- Insert x = 3 in the context +elab "custom_let" : tactic => + -- I don't think we need that + Lean.Elab.Tactic.withMainContext do + -- + let type := (Expr.const `Nat []) + let val : Expr := .lit (.natVal 3) + let n := `x -- the name is "x" + withLetDecl n type val fun nval => do + -- For debugging + let lctx ← Lean.MonadLCtx.getLCtx + let fid := nval.fvarId! + let decl := lctx.get! fid + dbg_trace f!" nval: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}" + -- + -- Tranform the main goal `m0?` to `let x = nval in m1?` + let mvarId ← Tactic.getMainGoal + let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType) + let newVal ← mkLetFVars #[nval] newMVar + -- Focus on the current goal + Tactic.focus do + -- Assign the main goal. + -- We must do this *after* we focused on the current goal, because + -- after we assigned the meta variable the goal is considered as solved + mvarId.assign newVal + -- Replace the list of goals with the new goal - we can do this because + -- we focused on the current goal + Lean.Elab.Tactic.setGoals [newMVar.mvarId!] + +example : Nat := by + custom_let + apply x + +example (x : Bool) : Nat := by + cases x <;> custom_let <;> apply x + +end Arith -- cgit v1.3.1 From 34f1f4d877b32002cd292cb1fe27969184efcf94 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Jun 2023 10:37:13 +0200 Subject: Finish the custom_let tactic --- backends/lean/Base/Arith.lean | 44 +++++++++++++++++++++---------------------- 1 file changed, 21 insertions(+), 23 deletions(-) (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean index 6339f218..d4611deb 100644 --- a/backends/lean/Base/Arith.lean +++ b/backends/lean/Base/Arith.lean @@ -168,36 +168,27 @@ elab "list_local_decls_1" : tactic => | .some _ => dbg_trace f!" Scalar expression"; pure r | _ => dbg_trace f!" Not a scalar"; pure .none pure () - -- match ← Lean.observing? (Lean.Meta.mkAppM `Scalar.toInt #[decl.toExpr]) with - -- | .none => dbg_trace f!" Not a scalar" - -- | .some _ => dbg_trace f!" Scalar expression" -#check Lean.Environment.addDecl -#check Expr -#check LocalContext -#check MVarId -#check Lean.Elab.Tactic.setGoals -#check Lean.Elab.Tactic.Context -#check withLocalDecl -#check Lean.MVarId.assert -#check LocalDecl - --- Insert x = 3 in the context -elab "custom_let" : tactic => +def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit := -- I don't think we need that Lean.Elab.Tactic.withMainContext do -- - let type := (Expr.const `Nat []) - let val : Expr := .lit (.natVal 3) - let n := `x -- the name is "x" - withLetDecl n type val fun nval => do + let val ← elabTerm val .none + let type ← inferType val + -- In some situations, the type will be left as a metavariable (for instance, + -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will + -- not choose): we force the instantiation of the meta-variable + synthesizeSyntheticMVarsUsingDefault + -- Insert the new declaration + withLetDecl name type val fun nval => do -- For debugging let lctx ← Lean.MonadLCtx.getLCtx let fid := nval.fvarId! let decl := lctx.get! fid - dbg_trace f!" nval: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}" + -- Remark: logInfo instantiates the mvars (contrary to dbg_trace): + logInfo m!" new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}" -- - -- Tranform the main goal `m0?` to `let x = nval in m1?` + -- Tranform the main goal `?m0` to `let x = nval in ?m1` let mvarId ← Tactic.getMainGoal let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType) let newVal ← mkLetFVars #[nval] newMVar @@ -211,11 +202,18 @@ elab "custom_let" : tactic => -- we focused on the current goal Lean.Elab.Tactic.setGoals [newMVar.mvarId!] +elab "custom_let " n:ident " := " v:term : tactic => + evalCustomLet n.getId v + +-- Insert x = 3 in the context +elab "custom_let " n:ident " := " v:term : tactic => + evalCustomLet n.getId v + example : Nat := by - custom_let + custom_let x := 4 apply x example (x : Bool) : Nat := by - cases x <;> custom_let <;> apply x + cases x <;> custom_let x := 3 <;> apply x end Arith -- cgit v1.3.1 From 9421b215a8911bc545eb524b8b07e7ca2eb717f3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Jun 2023 16:02:09 +0200 Subject: Make intro_has_prop_instances work --- backends/lean/Base/Arith.lean | 171 +++++++++++++++++++++++++++++++++++------- 1 file changed, 145 insertions(+), 26 deletions(-) (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean index d4611deb..a792deb2 100644 --- a/backends/lean/Base/Arith.lean +++ b/backends/lean/Base/Arith.lean @@ -75,7 +75,28 @@ class IsScalar (a : Type) where instance (ty : ScalarTy) : IsScalar (Scalar ty) where ---example (ty : ScalarTy) : IsScalar (Scalar ty) := _ +example (ty : ScalarTy) : IsScalar (Scalar ty) := inferInstance + +-- TODO: lookup doesn't work +class HasProp {a : Type} (x : a) where + prop_ty : Prop + prop : prop_ty + +class HasProp' (a : Type) where + prop_ty : a → Prop + prop : ∀ x:a, prop_ty x + +instance {ty : ScalarTy} (x : Scalar x) : HasProp x where + -- prop_ty is inferred + prop := And.intro x.hmin x.hmax + +instance (ty : ScalarTy) : HasProp' (Scalar ty) where + -- prop_ty is inferred + prop := λ x => And.intro x.hmin x.hmax + +example {a : Type} (x : a) [HasProp x] : Prop := + let i : HasProp x := inferInstance + i.prop_ty open Lean Lean.Elab Command Term Lean.Meta @@ -96,6 +117,40 @@ def isScalarExpr (e : Expr) : MetaM Bool := do | .some _ => pure true | _ => pure false +#check @HasProp'.prop + +-- Return an instance of `HasProp` for `e` if it has some +def lookupHasProp (e : Expr) : MetaM (Option Expr) := do + logInfo f!"lookupHasProp" + -- TODO: do we need Lean.observing? + -- This actually eliminates the error messages + Lean.observing? do + logInfo f!"lookupHasProp: observing" + let ty ← Lean.Meta.inferType e + let hasProp ← mkAppM `Arith.HasProp' #[ty] + let hasPropInst ← trySynthInstance hasProp + match hasPropInst with + | LOption.some i => + logInfo m!"Found HasProp instance" + let i_prop ← mkProjection i `prop + some (← mkAppM' i_prop #[e]) + | _ => none + +-- Auxiliary function for `collectHasPropInstances` +private partial def collectHasPropInstancesAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do + -- We do it in a very simpler manner: we deconstruct applications, + -- and recursively explore the sub-expressions. Note that we do + -- not go inside foralls and abstractions (should we?). + e.withApp fun f args => do + let hasPropInst ← lookupHasProp f + let hs := Option.getD (hasPropInst.map hs.insert) hs + let hs ← args.foldlM collectHasPropInstancesAux hs + pure hs + +-- Explore a term and return the instances of `HasProp` found for the sub-expressions +def collectHasPropInstances (e : Expr) : MetaM (HashSet Expr) := + collectHasPropInstancesAux HashSet.empty e + -- Explore a term and return the set of scalar expressions found inside partial def collectScalarExprsAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do -- We do it in a very simpler manner: we deconstruct applications, @@ -125,22 +180,43 @@ def getScalarExprsFromMainCtx : Tactic.TacticM (HashSet Expr) := do -- Return pure hs - -#check TSyntax -#check mkIdent --- TODO: addDecl? --- Project the scalar expressions into the context, to retrieve the bound inequalities --- def projectScalarExpr (e: Expr) : Tactic.TacticM Unit := do --- let e ← `($e) --- let e ← Lean.Elab.Term.elabTerm `($e) none --- Lean.Elab.Tactic.evalCases `($e) +-- Collect the instances of `HasProp` for the subexpressions in the context +def getHasPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do + Lean.Elab.Tactic.withMainContext do + -- Get the local context + let ctx ← Lean.MonadLCtx.getLCtx + -- Just a matter of precaution + let ctx ← instantiateLCtxMVars ctx + -- Initialize the hashset + let hs := HashSet.empty + -- Explore the declarations + let decls ← ctx.getDecls + let hs ← decls.foldlM (fun hs d => collectHasPropInstancesAux hs d.toExpr) hs + -- Return + pure hs elab "list_scalar_exprs" : tactic => do + logInfo m!"Listing scalar expressions" let hs ← getScalarExprsFromMainCtx hs.forM fun e => do - dbg_trace f!"+ Scalar expression: {e}" + logInfo m!"+ Scalar expression: {e}" + +example (x y : U32) (z : Usize) : True := by + list_scalar_exprs + simp + +elab "display_has_prop_instances" : tactic => do + logInfo m!"Displaying the HasProp instances" + let hs ← getHasPropInstancesFromMainCtx + hs.forM fun e => do + logInfo m!"+ HasProp instance: {e}" -#check LocalContext +example (x : U32) : True := by + let i : HasProp' U32 := inferInstance + have p := @HasProp'.prop _ i x + simp only [HasProp'.prop_ty] at p + display_has_prop_instances + simp elab "list_local_decls_1" : tactic => Lean.Elab.Tactic.withMainContext do @@ -169,18 +245,12 @@ elab "list_local_decls_1" : tactic => | _ => dbg_trace f!" Not a scalar"; pure .none pure () -def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit := +def evalAddDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool := false) : Tactic.TacticM Unit := -- I don't think we need that Lean.Elab.Tactic.withMainContext do - -- - let val ← elabTerm val .none - let type ← inferType val - -- In some situations, the type will be left as a metavariable (for instance, - -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will - -- not choose): we force the instantiation of the meta-variable - synthesizeSyntheticMVarsUsingDefault -- Insert the new declaration - withLetDecl name type val fun nval => do + let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type + withDecl fun nval => do -- For debugging let lctx ← Lean.MonadLCtx.getLCtx let fid := nval.fvarId! @@ -192,6 +262,11 @@ def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit := let mvarId ← Tactic.getMainGoal let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType) let newVal ← mkLetFVars #[nval] newMVar + -- There are two cases: + -- - asLet is true: newVal is `let $name := $val in $newMVar` + -- - asLet is false: ewVal is `λ $name => $newMVar` + -- We need to apply it to `val` + let newVal := if asLet then newVal else mkAppN newVal #[val] -- Focus on the current goal Tactic.focus do -- Assign the main goal. @@ -202,18 +277,62 @@ def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit := -- we focused on the current goal Lean.Elab.Tactic.setGoals [newMVar.mvarId!] -elab "custom_let " n:ident " := " v:term : tactic => - evalCustomLet n.getId v +def evalAddDeclSyntax (name : Name) (val : Syntax) (asLet : Bool := false) : Tactic.TacticM Unit := + -- I don't think we need that + Lean.Elab.Tactic.withMainContext do + -- + let val ← elabTerm val .none + let type ← inferType val + -- In some situations, the type will be left as a metavariable (for instance, + -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will + -- not choose): we force the instantiation of the meta-variable + synthesizeSyntheticMVarsUsingDefault + -- + evalAddDecl name val type asLet --- Insert x = 3 in the context elab "custom_let " n:ident " := " v:term : tactic => - evalCustomLet n.getId v + evalAddDeclSyntax n.getId v (asLet := true) + +elab "custom_have " n:ident " := " v:term : tactic => + evalAddDeclSyntax n.getId v (asLet := false) example : Nat := by custom_let x := 4 - apply x + custom_have y := 4 + apply y example (x : Bool) : Nat := by cases x <;> custom_let x := 3 <;> apply x +#check mkIdent +#check Syntax + +-- Lookup the instances of `HasProp' for all the sub-expressions in the context, +-- and introduce the corresponding assumptions +elab "intro_has_prop_instances" : tactic => do + logInfo m!"Introducing the HasProp instances" + let hs ← getHasPropInstancesFromMainCtx + hs.forM fun e => do + let type ← inferType e + let name := `h + evalAddDecl name e type (asLet := false) + -- Simplify to unfold the `prop_ty` projector + --let simpTheorems := ++ [``HasProp'.prop_ty] + let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) + -- Add the equational theorem for `HashProp'.prop_ty` + let simpTheorems ← simpTheorems.addDeclToUnfold ``HasProp'.prop_ty + let congrTheorems ← getSimpCongrTheorems + let ctx : Simp.Context := { simpTheorems := #[simpTheorems], congrTheorems } + -- Where to apply the simplifier + let loc := Tactic.Location.targets #[mkIdent name] false + -- Apply the simplifier + let _ ← Tactic.simpLocation ctx (discharge? := .none) loc + pure () + -- simpLocation + +example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by + intro_has_prop_instances + simp [*] + + end Arith -- cgit v1.3.1 From 6b319ece09b0f8a02529dd98bc20ffcb843020d6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 26 Jun 2023 17:33:17 +0200 Subject: Make minor modifications to Arith.lean --- backends/lean/Base/Arith.lean | 64 +++++++++++++++++++++++++------------------ 1 file changed, 37 insertions(+), 27 deletions(-) (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean index a792deb2..bb776b55 100644 --- a/backends/lean/Base/Arith.lean +++ b/backends/lean/Base/Arith.lean @@ -5,6 +5,8 @@ import Lean.Meta.Tactic.Simp import Init.Data.List.Basic import Mathlib.Tactic.RunCmd import Mathlib.Tactic.Linarith +-- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet +--import Mathlib.Tactic.Omega import Base.Primitives /- @@ -77,26 +79,19 @@ instance (ty : ScalarTy) : IsScalar (Scalar ty) where example (ty : ScalarTy) : IsScalar (Scalar ty) := inferInstance --- TODO: lookup doesn't work -class HasProp {a : Type} (x : a) where - prop_ty : Prop - prop : prop_ty - -class HasProp' (a : Type) where +-- Remark: I tried a version of the shape `HasProp {a : Type} (x : a)` +-- but the lookup didn't work +class HasProp (a : Type) where prop_ty : a → Prop prop : ∀ x:a, prop_ty x -instance {ty : ScalarTy} (x : Scalar x) : HasProp x where - -- prop_ty is inferred - prop := And.intro x.hmin x.hmax - -instance (ty : ScalarTy) : HasProp' (Scalar ty) where +instance (ty : ScalarTy) : HasProp (Scalar ty) where -- prop_ty is inferred prop := λ x => And.intro x.hmin x.hmax -example {a : Type} (x : a) [HasProp x] : Prop := - let i : HasProp x := inferInstance - i.prop_ty +instance (a : Type) : HasProp (Vec a) where + prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize + prop := λ ⟨ _, l ⟩ => l open Lean Lean.Elab Command Term Lean.Meta @@ -117,8 +112,6 @@ def isScalarExpr (e : Expr) : MetaM Bool := do | .some _ => pure true | _ => pure false -#check @HasProp'.prop - -- Return an instance of `HasProp` for `e` if it has some def lookupHasProp (e : Expr) : MetaM (Option Expr) := do logInfo f!"lookupHasProp" @@ -127,7 +120,7 @@ def lookupHasProp (e : Expr) : MetaM (Option Expr) := do Lean.observing? do logInfo f!"lookupHasProp: observing" let ty ← Lean.Meta.inferType e - let hasProp ← mkAppM `Arith.HasProp' #[ty] + let hasProp ← mkAppM ``Arith.HasProp #[ty] let hasPropInst ← trySynthInstance hasProp match hasPropInst with | LOption.some i => @@ -212,9 +205,9 @@ elab "display_has_prop_instances" : tactic => do logInfo m!"+ HasProp instance: {e}" example (x : U32) : True := by - let i : HasProp' U32 := inferInstance - have p := @HasProp'.prop _ i x - simp only [HasProp'.prop_ty] at p + let i : HasProp U32 := inferInstance + have p := @HasProp.prop _ i x + simp only [HasProp.prop_ty] at p display_has_prop_instances simp @@ -304,10 +297,7 @@ example : Nat := by example (x : Bool) : Nat := by cases x <;> custom_let x := 3 <;> apply x -#check mkIdent -#check Syntax - --- Lookup the instances of `HasProp' for all the sub-expressions in the context, +-- Lookup the instances of `HasProp for all the sub-expressions in the context, -- and introduce the corresponding assumptions elab "intro_has_prop_instances" : tactic => do logInfo m!"Introducing the HasProp instances" @@ -317,10 +307,9 @@ elab "intro_has_prop_instances" : tactic => do let name := `h evalAddDecl name e type (asLet := false) -- Simplify to unfold the `prop_ty` projector - --let simpTheorems := ++ [``HasProp'.prop_ty] let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) -- Add the equational theorem for `HashProp'.prop_ty` - let simpTheorems ← simpTheorems.addDeclToUnfold ``HasProp'.prop_ty + let simpTheorems ← simpTheorems.addDeclToUnfold ``HasProp.prop_ty let congrTheorems ← getSimpCongrTheorems let ctx : Simp.Context := { simpTheorems := #[simpTheorems], congrTheorems } -- Where to apply the simplifier @@ -328,11 +317,32 @@ elab "intro_has_prop_instances" : tactic => do -- Apply the simplifier let _ ← Tactic.simpLocation ctx (discharge? := .none) loc pure () - -- simpLocation example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by intro_has_prop_instances simp [*] +example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by + intro_has_prop_instances + simp_all [Scalar.max, Scalar.min] + +-- A tactic to solve linear arithmetic goals +syntax "int_tac" : tactic +macro_rules + | `(tactic| int_tac) => + `(tactic| + intro_has_prop_instances; + have := Scalar.cMin_bound ScalarTy.Usize; + have := Scalar.cMin_bound ScalarTy.Isize; + have := Scalar.cMax_bound ScalarTy.Usize; + have := Scalar.cMax_bound ScalarTy.Isize; + simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *; + linarith) + +example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by + int_tac + +example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by + int_tac end Arith -- cgit v1.3.1 From 0d1ac53f88f947ae94f6afb57b2a7e18a77460a7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 9 Jul 2023 10:11:13 +0200 Subject: Make progress on the int tactic --- backends/lean/Base/Arith.lean | 413 +++++++++++++++++++------------ backends/lean/Base/ArithBase.lean | 10 + backends/lean/Base/Diverge/ElabBase.lean | 112 --------- 3 files changed, 267 insertions(+), 268 deletions(-) create mode 100644 backends/lean/Base/ArithBase.lean (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean index bb776b55..df48a6a2 100644 --- a/backends/lean/Base/Arith.lean +++ b/backends/lean/Base/Arith.lean @@ -8,6 +8,7 @@ import Mathlib.Tactic.Linarith -- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet --import Mathlib.Tactic.Omega import Base.Primitives +import Base.ArithBase /- Mathlib tactics: @@ -53,9 +54,24 @@ namespace Arith open Primitives ---set_option pp.explicit true ---set_option pp.notation false ---set_option pp.coercions false +-- TODO: move? +theorem ne_zero_is_lt_or_gt {x : Int} (hne : x ≠ 0) : x < 0 ∨ x > 0 := by + cases h: x <;> simp_all + . rename_i n; + cases n <;> simp_all + . apply Int.negSucc_lt_zero + +-- TODO: move? +theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by + have hne : x - y ≠ 0 := by + simp + intro h + have: x = y := by linarith + simp_all + have h := ne_zero_is_lt_or_gt hne + match h with + | .inl _ => left; linarith + | .inr _ => right; linarith -- TODO: move instance Vec.cast (a : Type): Coe (Vec a) (List a) where coe := λ v => v.val @@ -71,17 +87,9 @@ instance Vec.cast (a : Type): Coe (Vec a) (List a) where coe := λ v => v.val -/ def Scalar.toInt {ty : ScalarTy} (x : Scalar ty) : Int := x.val --- We use this type-class to test if an expression is a scalar (if we manage --- to lookup an instance of this type-class, then it is) -class IsScalar (a : Type) where - -instance (ty : ScalarTy) : IsScalar (Scalar ty) where - -example (ty : ScalarTy) : IsScalar (Scalar ty) := inferInstance - -- Remark: I tried a version of the shape `HasProp {a : Type} (x : a)` -- but the lookup didn't work -class HasProp (a : Type) where +class HasProp (a : Sort u) where prop_ty : a → Prop prop : ∀ x:a, prop_ty x @@ -93,73 +101,50 @@ instance (a : Type) : HasProp (Vec a) where prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize prop := λ ⟨ _, l ⟩ => l -open Lean Lean.Elab Command Term Lean.Meta - --- Return true if the expression is a scalar expression -def isScalarExpr (e : Expr) : MetaM Bool := do - -- Try to convert the expression to a scalar - -- TODO: I tried to do it with Lean.Meta.mkAppM but it didn't work: how - -- do we allow Lean to perform (controlled) unfoldings for instantiation - -- purposes? - let r ← Lean.observing? do - let ty ← Lean.Meta.inferType e - let isScalar ← mkAppM `Arith.IsScalar #[ty] - let isScalar ← trySynthInstance isScalar - match isScalar with - | LOption.some x => some x - | _ => none - match r with - | .some _ => pure true - | _ => pure false +class PropHasImp (x : Prop) where + concl : Prop + prop : x → concl --- Return an instance of `HasProp` for `e` if it has some -def lookupHasProp (e : Expr) : MetaM (Option Expr) := do - logInfo f!"lookupHasProp" - -- TODO: do we need Lean.observing? - -- This actually eliminates the error messages - Lean.observing? do - logInfo f!"lookupHasProp: observing" - let ty ← Lean.Meta.inferType e - let hasProp ← mkAppM ``Arith.HasProp #[ty] - let hasPropInst ← trySynthInstance hasProp - match hasPropInst with - | LOption.some i => - logInfo m!"Found HasProp instance" - let i_prop ← mkProjection i `prop - some (← mkAppM' i_prop #[e]) - | _ => none +-- This also works for `x ≠ y` because this expression reduces to `¬ x = y` +-- and `Ne` is marked as `reducible` +instance (x y : Int) : PropHasImp (¬ x = y) where + concl := x < y ∨ x > y + prop := λ (h:x ≠ y) => ne_is_lt_or_gt h --- Auxiliary function for `collectHasPropInstances` -private partial def collectHasPropInstancesAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do - -- We do it in a very simpler manner: we deconstruct applications, - -- and recursively explore the sub-expressions. Note that we do - -- not go inside foralls and abstractions (should we?). - e.withApp fun f args => do - let hasPropInst ← lookupHasProp f - let hs := Option.getD (hasPropInst.map hs.insert) hs - let hs ← args.foldlM collectHasPropInstancesAux hs - pure hs +open Lean Lean.Elab Command Term Lean.Meta --- Explore a term and return the instances of `HasProp` found for the sub-expressions -def collectHasPropInstances (e : Expr) : MetaM (HashSet Expr) := - collectHasPropInstancesAux HashSet.empty e +-- Small utility: print all the declarations in the context +elab "print_all_decls" : tactic => do + let ctx ← Lean.MonadLCtx.getLCtx + for decl in ← ctx.getDecls do + let ty ← Lean.Meta.inferType decl.toExpr + logInfo m!"{decl.toExpr} : {ty}" + pure () --- Explore a term and return the set of scalar expressions found inside -partial def collectScalarExprsAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do +-- Explore a term by decomposing the applications (we explore the applied +-- functions and their arguments, but ignore lambdas, forall, etc. - +-- should we go inside?). +partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do -- We do it in a very simpler manner: we deconstruct applications, -- and recursively explore the sub-expressions. Note that we do -- not go inside foralls and abstractions (should we?). e.withApp fun f args => do - let hs ← if ← isScalarExpr f then pure (hs.insert f) else pure hs - let hs ← args.foldlM collectScalarExprsAux hs - pure hs - --- Explore a term and return the list of scalar expressions found inside -def collectScalarExprs (e : Expr) : MetaM (HashSet Expr) := - collectScalarExprsAux HashSet.empty e - --- Collect the scalar expressions in the context -def getScalarExprsFromMainCtx : Tactic.TacticM (HashSet Expr) := do + let s ← k s f + args.foldlM (foldTermApps k) s + +-- Provided a function `k` which lookups type class instances on an expression, +-- collect all the instances lookuped by applying `k` on the sub-expressions of `e`. +def collectInstances + (k : Expr → MetaM (Option Expr)) (s : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do + let k s e := do + match ← k e with + | none => pure s + | some i => pure (s.insert i) + foldTermApps k s e + +-- Similar to `collectInstances`, but explores all the local declarations in the +-- main context. +def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do Lean.Elab.Tactic.withMainContext do -- Get the local context let ctx ← Lean.MonadLCtx.getLCtx @@ -169,40 +154,37 @@ def getScalarExprsFromMainCtx : Tactic.TacticM (HashSet Expr) := do let hs := HashSet.empty -- Explore the declarations let decls ← ctx.getDecls - let hs ← decls.foldlM (fun hs d => collectScalarExprsAux hs d.toExpr) hs - -- Return - pure hs + decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs + +-- Return an instance of `HasProp` for `e` if it has some +def lookupHasProp (e : Expr) : MetaM (Option Expr) := do + trace[Arith] "lookupHasProp" + -- TODO: do we need Lean.observing? + -- This actually eliminates the error messages + Lean.observing? do + trace[Arith] "lookupHasProp: observing" + let ty ← Lean.Meta.inferType e + let hasProp ← mkAppM ``HasProp #[ty] + let hasPropInst ← trySynthInstance hasProp + match hasPropInst with + | LOption.some i => + trace[Arith] "Found HasProp instance" + let i_prop ← mkProjection i (Name.mkSimple "prop") + some (← mkAppM' i_prop #[e]) + | _ => none -- Collect the instances of `HasProp` for the subexpressions in the context -def getHasPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do - Lean.Elab.Tactic.withMainContext do - -- Get the local context - let ctx ← Lean.MonadLCtx.getLCtx - -- Just a matter of precaution - let ctx ← instantiateLCtxMVars ctx - -- Initialize the hashset - let hs := HashSet.empty - -- Explore the declarations - let decls ← ctx.getDecls - let hs ← decls.foldlM (fun hs d => collectHasPropInstancesAux hs d.toExpr) hs - -- Return - pure hs +def collectHasPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do + collectInstancesFromMainCtx lookupHasProp -elab "list_scalar_exprs" : tactic => do - logInfo m!"Listing scalar expressions" - let hs ← getScalarExprsFromMainCtx +elab "display_has_prop_instances" : tactic => do + trace[Arith] "Displaying the HasProp instances" + let hs ← collectHasPropInstancesFromMainCtx hs.forM fun e => do - logInfo m!"+ Scalar expression: {e}" + trace[Arith] "+ HasProp instance: {e}" -example (x y : U32) (z : Usize) : True := by - list_scalar_exprs - simp -elab "display_has_prop_instances" : tactic => do - logInfo m!"Displaying the HasProp instances" - let hs ← getHasPropInstancesFromMainCtx - hs.forM fun e => do - logInfo m!"+ HasProp instance: {e}" +set_option trace.Arith true example (x : U32) : True := by let i : HasProp U32 := inferInstance @@ -211,34 +193,45 @@ example (x : U32) : True := by display_has_prop_instances simp -elab "list_local_decls_1" : tactic => - Lean.Elab.Tactic.withMainContext do - -- Get the local context - let ctx ← Lean.MonadLCtx.getLCtx - let ctx ← instantiateLCtxMVars ctx - let decls ← ctx.getDecls - -- Filter the scalar expressions - let decls ← decls.filterMapM fun decl: Lean.LocalDecl => do - let declExpr := decl.toExpr - let declName := decl.userName - let declType ← Lean.Meta.inferType declExpr - dbg_trace f!"+ local decl: name: {declName} | expr: {declExpr} | ty: {declType}" - -- Try to convert the expression to a scalar - -- TODO: I tried to do it with Lean.Meta.mkAppM but it didn't work: how - -- do we allow Lean to perform (controlled) unfoldings for instantiation - -- purposes? - let r ← Lean.observing? do - let isScalar ← mkAppM `Arith.IsScalar #[declType] - let isScalar ← trySynthInstance isScalar - match isScalar with - | LOption.some x => some x - | _ => none - match r with - | .some _ => dbg_trace f!" Scalar expression"; pure r - | _ => dbg_trace f!" Not a scalar"; pure .none - pure () +set_option trace.Arith false -def evalAddDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool := false) : Tactic.TacticM Unit := +-- Return an instance of `PropHasImp` for `e` if it has some +def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do + trace[Arith] "lookupPropHasImp" + -- TODO: do we need Lean.observing? + -- This actually eliminates the error messages + Lean.observing? do + trace[Arith] "lookupPropHasImp: observing" + let ty ← Lean.Meta.inferType e + trace[Arith] "lookupPropHasImp: ty: {ty}" + let cl ← mkAppM ``PropHasImp #[ty] + let inst ← trySynthInstance cl + match inst with + | LOption.some i => + trace[Arith] "Found PropHasImp instance" + let i_prop ← mkProjection i (Name.mkSimple "prop") + some (← mkAppM' i_prop #[e]) + | _ => none + +-- Collect the instances of `PropHasImp` for the subexpressions in the context +def collectPropHasImpInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do + collectInstancesFromMainCtx lookupPropHasImp + +elab "display_prop_has_imp_instances" : tactic => do + trace[Arith] "Displaying the PropHasImp instances" + let hs ← collectPropHasImpInstancesFromMainCtx + hs.forM fun e => do + trace[Arith] "+ PropHasImp instance: {e}" + +set_option trace.Arith true + +example (x y : Int) (h0 : x ≠ y) (h1 : ¬ x = y) : True := by + display_prop_has_imp_instances + simp + +set_option trace.Arith false + +def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit := -- I don't think we need that Lean.Elab.Tactic.withMainContext do -- Insert the new declaration @@ -248,8 +241,7 @@ def evalAddDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool := false) let lctx ← Lean.MonadLCtx.getLCtx let fid := nval.fvarId! let decl := lctx.get! fid - -- Remark: logInfo instantiates the mvars (contrary to dbg_trace): - logInfo m!" new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}" + trace[Arith] " new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}" -- -- Tranform the main goal `?m0` to `let x = nval in ?m1` let mvarId ← Tactic.getMainGoal @@ -260,17 +252,14 @@ def evalAddDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool := false) -- - asLet is false: ewVal is `λ $name => $newMVar` -- We need to apply it to `val` let newVal := if asLet then newVal else mkAppN newVal #[val] - -- Focus on the current goal - Tactic.focus do - -- Assign the main goal. - -- We must do this *after* we focused on the current goal, because - -- after we assigned the meta variable the goal is considered as solved + -- Assign the main goal and update the current goal mvarId.assign newVal - -- Replace the list of goals with the new goal - we can do this because - -- we focused on the current goal - Lean.Elab.Tactic.setGoals [newMVar.mvarId!] + let goals ← Tactic.getUnsolvedGoals + Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals) + -- Call the continuation + k nval -def evalAddDeclSyntax (name : Name) (val : Syntax) (asLet : Bool := false) : Tactic.TacticM Unit := +def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit := -- I don't think we need that Lean.Elab.Tactic.withMainContext do -- @@ -281,13 +270,13 @@ def evalAddDeclSyntax (name : Name) (val : Syntax) (asLet : Bool := false) : Tac -- not choose): we force the instantiation of the meta-variable synthesizeSyntheticMVarsUsingDefault -- - evalAddDecl name val type asLet + addDecl name val type asLet k elab "custom_let " n:ident " := " v:term : tactic => - evalAddDeclSyntax n.getId v (asLet := true) + addDeclSyntax n.getId v (asLet := true) (λ _ => pure ()) elab "custom_have " n:ident " := " v:term : tactic => - evalAddDeclSyntax n.getId v (asLet := false) + addDeclSyntax n.getId v (asLet := false) (λ _ => pure ()) example : Nat := by custom_let x := 4 @@ -297,26 +286,32 @@ example : Nat := by example (x : Bool) : Nat := by cases x <;> custom_let x := 3 <;> apply x --- Lookup the instances of `HasProp for all the sub-expressions in the context, --- and introduce the corresponding assumptions -elab "intro_has_prop_instances" : tactic => do - logInfo m!"Introducing the HasProp instances" - let hs ← getHasPropInstancesFromMainCtx +-- Lookup instances in a context and introduce them with additional declarations. +def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit := do + let hs ← collectInstancesFromMainCtx lookup hs.forM fun e => do let type ← inferType e - let name := `h - evalAddDecl name e type (asLet := false) - -- Simplify to unfold the `prop_ty` projector + let name ← mkFreshUserName `h + -- Add a declaration + addDecl name e type (asLet := false) λ nval => do + -- Simplify to unfold the declaration to unfold (i.e., the projector) let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) - -- Add the equational theorem for `HashProp'.prop_ty` - let simpTheorems ← simpTheorems.addDeclToUnfold ``HasProp.prop_ty + -- Add the equational theorem for the decl to unfold + let simpTheorems ← simpTheorems.addDeclToUnfold declToUnfold let congrTheorems ← getSimpCongrTheorems let ctx : Simp.Context := { simpTheorems := #[simpTheorems], congrTheorems } -- Where to apply the simplifier let loc := Tactic.Location.targets #[mkIdent name] false -- Apply the simplifier let _ ← Tactic.simpLocation ctx (discharge? := .none) loc - pure () + -- Call the continuation + k nval + +-- Lookup the instances of `HasProp for all the sub-expressions in the context, +-- and introduce the corresponding assumptions +elab "intro_has_prop_instances" : tactic => do + trace[Arith] "Introducing the HasProp instances" + introInstances ``HasProp.prop_ty lookupHasProp (fun _ => pure ()) example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by intro_has_prop_instances @@ -326,23 +321,129 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by intro_has_prop_instances simp_all [Scalar.max, Scalar.min] --- A tactic to solve linear arithmetic goals -syntax "int_tac" : tactic +-- Tactic to split on a disjunction +def splitDisj (h : Expr) : Tactic.TacticM Unit := do + trace[Arith] "assumption on which to split: {h}" + -- Retrieve the main goal + Lean.Elab.Tactic.withMainContext do + let goalType ← Lean.Elab.Tactic.getMainTarget + -- Case disjunction + let hTy ← inferType h + hTy.withApp fun f xs => do + trace[Arith] "as app: {f} {xs}" + -- Sanity check + if ¬ (f.isConstOf ``Or ∧ xs.size = 2) then throwError "Invalid argument to splitDisj" + let a := xs.get! 0 + let b := xs.get! 1 + -- Introduce the new goals + -- Returns: + -- - the match branch + -- - a fresh new mvar id + let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do + -- Introduce a variable for the assumption (`a` or `b`) + let asmName ← mkFreshUserName `h + withLocalDeclD asmName hTy fun var => do + -- The new goal + let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName) + -- The branch expression + let branch ← mkLambdaFVars #[var] mgoal + pure (branch, mgoal.mvarId!) + let (inl, mleft) ← mkGoal a "left" + let (inr, mright) ← mkGoal b "right" + trace[Arith] "left: {inl}: {mleft}" + trace[Arith] "right: {inr}: {mright}" + -- Create the match expression + withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do + let motive ← mkLambdaFVars #[hVar] goalType + let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr] + let mgoal ← Tactic.getMainGoal + trace[Arith] "goals: {← Tactic.getUnsolvedGoals}" + trace[Arith] "main goal: {mgoal}" + mgoal.assign casesExpr + let goals ← Tactic.getUnsolvedGoals + Tactic.setGoals (mleft :: mright :: goals) + trace[Arith] "new goals: {← Tactic.getUnsolvedGoals}" + +elab "split_disj " n:ident : tactic => do + Lean.Elab.Tactic.withMainContext do + let decl ← Lean.Meta.getLocalDeclFromUserName n.getId + let fvar := mkFVar decl.fvarId + splitDisj fvar + +example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by + split_disj h0 + . left; assumption + . right; assumption + +-- Lookup the instances of `PropHasImp for all the sub-expressions in the context, +-- and introduce the corresponding assumptions +elab "intro_prop_has_imp_instances" : tactic => do + trace[Arith] "Introducing the PropHasImp instances" + introInstances ``PropHasImp.concl lookupPropHasImp (fun _ => pure ()) + +example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by + intro_prop_has_imp_instances + rename_i h + split_disj h + . linarith + . linarith + +syntax "int_tac_preprocess" : tactic + +/- Boosting a bit the linarith tac. + + We do the following: + - for all the assumptions of the shape `(x : Int) ≠ y` or `¬ (x = y), we + introduce two goals with the assumptions `x < y` and `x > y` + TODO: we could create a PR for mathlib. + -/ +def intTacPreprocess : Tactic.TacticM Unit := do + Lean.Elab.Tactic.withMainContext do + -- Get the local context + let ctx ← Lean.MonadLCtx.getLCtx + -- Just a matter of precaution + let ctx ← instantiateLCtxMVars ctx + -- Explore the declarations - Remark: we don't explore the subexpressions + -- (we could, but it is rarely necessary, because terms of the shape `x ≠ y` + -- are often introduced because of branchings in the code, and using `split` + -- introduces exactly the assumptions `x = y` and `x ≠ y`). + let decls ← ctx.getDecls + for decl in decls do + let ty ← Lean.Meta.inferType decl.toExpr + ty.withApp fun f args => do + trace[Arith] "decl: {f} {args}" + -- Check if this is an inequality between integers + pure () + +-- TODO: int_tac + +elab "int_tac_preprocess" : tactic => + intTacPreprocess + +example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by + int_tac_preprocess + simp_all + int_tac_preprocess + +-- A tactic to solve linear arithmetic goals in the presence of scalars +syntax "scalar_tac" : tactic macro_rules - | `(tactic| int_tac) => + | `(tactic| scalar_tac) => `(tactic| intro_has_prop_instances; have := Scalar.cMin_bound ScalarTy.Usize; have := Scalar.cMin_bound ScalarTy.Isize; have := Scalar.cMax_bound ScalarTy.Usize; have := Scalar.cMax_bound ScalarTy.Isize; + -- TODO: not too sure about that simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *; + -- TODO: use int_tac linarith) example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by - int_tac + scalar_tac example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by - int_tac + scalar_tac end Arith diff --git a/backends/lean/Base/ArithBase.lean b/backends/lean/Base/ArithBase.lean new file mode 100644 index 00000000..ddd2dc24 --- /dev/null +++ b/backends/lean/Base/ArithBase.lean @@ -0,0 +1,10 @@ +import Lean + +namespace Arith + +open Lean Elab Term Meta + +-- We can't define and use trace classes in the same file +initialize registerTraceClass `Arith + +end Arith diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean index aaaea6f7..fedb1c74 100644 --- a/backends/lean/Base/Diverge/ElabBase.lean +++ b/backends/lean/Base/Diverge/ElabBase.lean @@ -12,116 +12,4 @@ initialize registerTraceClass `Diverge.def.genBody initialize registerTraceClass `Diverge.def.valid initialize registerTraceClass `Diverge.def.unfold --- Useful helper to explore definitions and figure out the variant --- of their sub-expressions. -def explore_term (incr : String) (e : Expr) : MetaM Unit := - match e with - | .bvar _ => do logInfo m!"{incr}bvar: {e}"; return () - | .fvar _ => do logInfo m!"{incr}fvar: {e}"; return () - | .mvar _ => do logInfo m!"{incr}mvar: {e}"; return () - | .sort _ => do logInfo m!"{incr}sort: {e}"; return () - | .const _ _ => do logInfo m!"{incr}const: {e}"; return () - | .app fn arg => do - logInfo m!"{incr}app: {e}" - explore_term (incr ++ " ") fn - explore_term (incr ++ " ") arg - | .lam _bName bTy body _binfo => do - logInfo m!"{incr}lam: {e}" - explore_term (incr ++ " ") bTy - explore_term (incr ++ " ") body - | .forallE _bName bTy body _bInfo => do - logInfo m!"{incr}forallE: {e}" - explore_term (incr ++ " ") bTy - explore_term (incr ++ " ") body - | .letE _dName ty val body _nonDep => do - logInfo m!"{incr}letE: {e}" - explore_term (incr ++ " ") ty - explore_term (incr ++ " ") val - explore_term (incr ++ " ") body - | .lit _ => do logInfo m!"{incr}lit: {e}"; return () - | .mdata _ e => do - logInfo m!"{incr}mdata: {e}" - explore_term (incr ++ " ") e - | .proj _ _ struct => do - logInfo m!"{incr}proj: {e}" - explore_term (incr ++ " ") struct - -def explore_decl (n : Name) : TermElabM Unit := do - logInfo m!"Name: {n}" - let env ← getEnv - let decl := env.constants.find! n - match decl with - | .defnInfo val => - logInfo m!"About to explore defn: {decl.name}" - logInfo m!"# Type:" - explore_term "" val.type - logInfo m!"# Value:" - explore_term "" val.value - | .axiomInfo _ => throwError m!"axiom: {n}" - | .thmInfo _ => throwError m!"thm: {n}" - | .opaqueInfo _ => throwError m!"opaque: {n}" - | .quotInfo _ => throwError m!"quot: {n}" - | .inductInfo _ => throwError m!"induct: {n}" - | .ctorInfo _ => throwError m!"ctor: {n}" - | .recInfo _ => throwError m!"rec: {n}" - -syntax (name := printDecl) "print_decl " ident : command - -open Lean.Elab.Command - -@[command_elab printDecl] def elabPrintDecl : CommandElab := fun stx => do - liftTermElabM do - let id := stx[1] - addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none - let cs ← resolveGlobalConstWithInfos id - explore_decl cs[0]! - -private def test1 : Nat := 0 -private def test2 (x : Nat) : Nat := x - -print_decl test1 -print_decl test2 - --- A map visitor function for expressions (adapted from `AbstractNestedProofs.visit`) --- The continuation takes as parameters: --- - the current depth of the expression (useful for printing/debugging) --- - the expression to explore -partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr := do - let mapVisitBinders (xs : Array Expr) (k2 : MetaM Expr) : MetaM Expr := do - let localInstances ← getLocalInstances - let mut lctx ← getLCtx - for x in xs do - let xFVarId := x.fvarId! - let localDecl ← xFVarId.getDecl - let type ← mapVisit k localDecl.type - let localDecl := localDecl.setType type - let localDecl ← match localDecl.value? with - | some value => let value ← mapVisit k value; pure <| localDecl.setValue value - | none => pure localDecl - lctx :=lctx.modifyLocalDecl xFVarId fun _ => localDecl - withLCtx lctx localInstances k2 - -- TODO: use a cache? (Lean.checkCache) - let rec visit (i : Nat) (e : Expr) : MetaM Expr := do - -- Explore - let e ← k i e - match e with - | .bvar _ - | .fvar _ - | .mvar _ - | .sort _ - | .lit _ - | .const _ _ => pure e - | .app .. => do e.withApp fun f args => return mkAppN f (← args.mapM (visit (i + 1))) - | .lam .. => - lambdaLetTelescope e fun xs b => - mapVisitBinders xs do mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false) - | .forallE .. => do - forallTelescope e fun xs b => mapVisitBinders xs do mkForallFVars xs (← visit (i + 1) b) - | .letE .. => do - lambdaLetTelescope e fun xs b => mapVisitBinders xs do - mkLambdaFVars xs (← visit (i + 1) b) (usedLetOnly := false) - | .mdata _ b => return e.updateMData! (← visit (i + 1) b) - | .proj _ _ b => return e.updateProj! (← visit (i + 1) b) - visit 0 e - end Diverge -- cgit v1.3.1 From 1c251c13b1e6698f3c7c974ea88c2c8a28777cc1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 9 Jul 2023 10:50:50 +0200 Subject: Implement a first working version of int_tac --- backends/lean/Base/Arith.lean | 96 ++++++++++++++++++++++++++----------------- 1 file changed, 58 insertions(+), 38 deletions(-) (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean index df48a6a2..8cdf75a3 100644 --- a/backends/lean/Base/Arith.lean +++ b/backends/lean/Base/Arith.lean @@ -231,7 +231,7 @@ example (x y : Int) (h0 : x ≠ y) (h1 : ¬ x = y) : True := by set_option trace.Arith false -def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit := +def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr := -- I don't think we need that Lean.Elab.Tactic.withMainContext do -- Insert the new declaration @@ -256,10 +256,11 @@ def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) (k : Expr mvarId.assign newVal let goals ← Tactic.getUnsolvedGoals Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals) - -- Call the continuation - k nval + -- Return the new value - note: we are in the *new* context, created + -- after the declaration was added, so it will persist + pure nval -def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit := +def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit := -- I don't think we need that Lean.Elab.Tactic.withMainContext do -- @@ -270,13 +271,13 @@ def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) (k : Expr → Tact -- not choose): we force the instantiation of the meta-variable synthesizeSyntheticMVarsUsingDefault -- - addDecl name val type asLet k + let _ ← addDecl name val type asLet -elab "custom_let " n:ident " := " v:term : tactic => - addDeclSyntax n.getId v (asLet := true) (λ _ => pure ()) +elab "custom_let " n:ident " := " v:term : tactic => do + addDeclSyntax n.getId v (asLet := true) elab "custom_have " n:ident " := " v:term : tactic => - addDeclSyntax n.getId v (asLet := false) (λ _ => pure ()) + addDeclSyntax n.getId v (asLet := false) example : Nat := by custom_let x := 4 @@ -287,13 +288,13 @@ example (x : Bool) : Nat := by cases x <;> custom_let x := 3 <;> apply x -- Lookup instances in a context and introduce them with additional declarations. -def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit := do +def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do let hs ← collectInstancesFromMainCtx lookup - hs.forM fun e => do + hs.toArray.mapM fun e => do let type ← inferType e let name ← mkFreshUserName `h -- Add a declaration - addDecl name e type (asLet := false) λ nval => do + let nval ← addDecl name e type (asLet := false) -- Simplify to unfold the declaration to unfold (i.e., the projector) let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) -- Add the equational theorem for the decl to unfold @@ -304,14 +305,14 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) let loc := Tactic.Location.targets #[mkIdent name] false -- Apply the simplifier let _ ← Tactic.simpLocation ctx (discharge? := .none) loc - -- Call the continuation - k nval + -- Return the new value + pure nval -- Lookup the instances of `HasProp for all the sub-expressions in the context, -- and introduce the corresponding assumptions elab "intro_has_prop_instances" : tactic => do trace[Arith] "Introducing the HasProp instances" - introInstances ``HasProp.prop_ty lookupHasProp (fun _ => pure ()) + let _ ← introInstances ``HasProp.prop_ty lookupHasProp example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by intro_has_prop_instances @@ -322,7 +323,7 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by simp_all [Scalar.max, Scalar.min] -- Tactic to split on a disjunction -def splitDisj (h : Expr) : Tactic.TacticM Unit := do +def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do trace[Arith] "assumption on which to split: {h}" -- Retrieve the main goal Lean.Elab.Tactic.withMainContext do @@ -361,14 +362,23 @@ def splitDisj (h : Expr) : Tactic.TacticM Unit := do trace[Arith] "main goal: {mgoal}" mgoal.assign casesExpr let goals ← Tactic.getUnsolvedGoals - Tactic.setGoals (mleft :: mright :: goals) + -- Focus on the left + Tactic.setGoals [mleft] + kleft + let leftGoals ← Tactic.getUnsolvedGoals + -- Focus on the right + Tactic.setGoals [mright] + kright + let rightGoals ← Tactic.getUnsolvedGoals + -- Put all the goals back + Tactic.setGoals (leftGoals ++ rightGoals ++ goals) trace[Arith] "new goals: {← Tactic.getUnsolvedGoals}" elab "split_disj " n:ident : tactic => do Lean.Elab.Tactic.withMainContext do let decl ← Lean.Meta.getLocalDeclFromUserName n.getId let fvar := mkFVar decl.fvarId - splitDisj fvar + splitDisj fvar (fun _ => pure ()) (fun _ => pure ()) example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by split_disj h0 @@ -379,7 +389,7 @@ example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by -- and introduce the corresponding assumptions elab "intro_prop_has_imp_instances" : tactic => do trace[Arith] "Introducing the PropHasImp instances" - introInstances ``PropHasImp.concl lookupPropHasImp (fun _ => pure ()) + let _ ← introInstances ``PropHasImp.concl lookupPropHasImp example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by intro_prop_has_imp_instances @@ -388,7 +398,7 @@ example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by . linarith . linarith -syntax "int_tac_preprocess" : tactic +--syntax "int_tac_preprocess" : tactic /- Boosting a bit the linarith tac. @@ -399,31 +409,41 @@ syntax "int_tac_preprocess" : tactic -/ def intTacPreprocess : Tactic.TacticM Unit := do Lean.Elab.Tactic.withMainContext do - -- Get the local context - let ctx ← Lean.MonadLCtx.getLCtx - -- Just a matter of precaution - let ctx ← instantiateLCtxMVars ctx - -- Explore the declarations - Remark: we don't explore the subexpressions - -- (we could, but it is rarely necessary, because terms of the shape `x ≠ y` - -- are often introduced because of branchings in the code, and using `split` - -- introduces exactly the assumptions `x = y` and `x ≠ y`). - let decls ← ctx.getDecls - for decl in decls do - let ty ← Lean.Meta.inferType decl.toExpr - ty.withApp fun f args => do - trace[Arith] "decl: {f} {args}" - -- Check if this is an inequality between integers - pure () - --- TODO: int_tac + -- Lookup the instances of PropHasImp (this is how we detect assumptions + -- of the proper shape), introduce assumptions in the context and split + -- on those + -- TODO: get rid of the assumption that we split + let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit := + match asms with + | [] => pure () + | asm :: asms => + let k := splitOnAsms asms + splitDisj asm k k + -- Introduce + let asms ← introInstances ``PropHasImp.concl lookupPropHasImp + -- Split + splitOnAsms asms.toList elab "int_tac_preprocess" : tactic => intTacPreprocess example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by int_tac_preprocess - simp_all - int_tac_preprocess + linarith + linarith + +syntax "int_tac" : tactic +macro_rules + | `(tactic| int_tac) => + `(tactic| + int_tac_preprocess <;> + linarith) + +example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by int_tac + +-- Checking that things append correctly when there are several disjunctions +example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by + int_tac_preprocess <;> apply And.intro <;> linarith -- A tactic to solve linear arithmetic goals in the presence of scalars syntax "scalar_tac" : tactic -- cgit v1.3.1 From d9a11b312ef0df13795d9a1982ca1cd2eba0e124 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 9 Jul 2023 22:27:44 +0200 Subject: Improve int_tac --- backends/lean/Base/Arith.lean | 41 ++++++++++++++++++----------------------- 1 file changed, 18 insertions(+), 23 deletions(-) (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean index 8cdf75a3..364447ed 100644 --- a/backends/lean/Base/Arith.lean +++ b/backends/lean/Base/Arith.lean @@ -183,9 +183,6 @@ elab "display_has_prop_instances" : tactic => do hs.forM fun e => do trace[Arith] "+ HasProp instance: {e}" - -set_option trace.Arith true - example (x : U32) : True := by let i : HasProp U32 := inferInstance have p := @HasProp.prop _ i x @@ -193,8 +190,6 @@ example (x : U32) : True := by display_has_prop_instances simp -set_option trace.Arith false - -- Return an instance of `PropHasImp` for `e` if it has some def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do trace[Arith] "lookupPropHasImp" @@ -223,14 +218,10 @@ elab "display_prop_has_imp_instances" : tactic => do hs.forM fun e => do trace[Arith] "+ PropHasImp instance: {e}" -set_option trace.Arith true - -example (x y : Int) (h0 : x ≠ y) (h1 : ¬ x = y) : True := by +example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by display_prop_has_imp_instances simp -set_option trace.Arith false - def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr := -- I don't think we need that Lean.Elab.Tactic.withMainContext do @@ -322,12 +313,15 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by intro_has_prop_instances simp_all [Scalar.max, Scalar.min] --- Tactic to split on a disjunction +-- Tactic to split on a disjunction. +-- The expression `h` should be an fvar. def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do trace[Arith] "assumption on which to split: {h}" -- Retrieve the main goal Lean.Elab.Tactic.withMainContext do let goalType ← Lean.Elab.Tactic.getMainTarget + let hDecl := (← getLCtx).get! h.fvarId! + let hName := hDecl.userName -- Case disjunction let hTy ← inferType h hTy.withApp fun f xs => do @@ -341,14 +335,16 @@ def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM U -- - the match branch -- - a fresh new mvar id let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do - -- Introduce a variable for the assumption (`a` or `b`) - let asmName ← mkFreshUserName `h - withLocalDeclD asmName hTy fun var => do + -- Introduce a variable for the assumption (`a` or `b`). Note that we reuse + -- the name of the assumption we split. + withLocalDeclD hName hTy fun var => do -- The new goal let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName) + -- Clear the assumption that we split + let mgoal ← mgoal.mvarId!.tryClearMany #[h.fvarId!] -- The branch expression - let branch ← mkLambdaFVars #[var] mgoal - pure (branch, mgoal.mvarId!) + let branch ← mkLambdaFVars #[var] (mkMVar mgoal) + pure (branch, mgoal) let (inl, mleft) ← mkGoal a "left" let (inr, mright) ← mkGoal b "right" trace[Arith] "left: {inl}: {mleft}" @@ -398,8 +394,6 @@ example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by . linarith . linarith ---syntax "int_tac_preprocess" : tactic - /- Boosting a bit the linarith tac. We do the following: @@ -412,7 +406,7 @@ def intTacPreprocess : Tactic.TacticM Unit := do -- Lookup the instances of PropHasImp (this is how we detect assumptions -- of the proper shape), introduce assumptions in the context and split -- on those - -- TODO: get rid of the assumption that we split + -- TODO: get rid of the assumptions that we split let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit := match asms with | [] => pure () @@ -436,14 +430,16 @@ syntax "int_tac" : tactic macro_rules | `(tactic| int_tac) => `(tactic| + (repeat (apply And.intro)) <;> -- TODO: improve this int_tac_preprocess <;> linarith) -example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by int_tac +example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by + int_tac -- Checking that things append correctly when there are several disjunctions example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by - int_tac_preprocess <;> apply And.intro <;> linarith + int_tac -- A tactic to solve linear arithmetic goals in the presence of scalars syntax "scalar_tac" : tactic @@ -457,8 +453,7 @@ macro_rules have := Scalar.cMax_bound ScalarTy.Isize; -- TODO: not too sure about that simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *; - -- TODO: use int_tac - linarith) + int_tac) example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by scalar_tac -- cgit v1.3.1 From 7206b48a73d6204baea99f4f4675be2518a8f8c2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 10 Jul 2023 15:06:12 +0200 Subject: Start working on the progress tactic --- backends/lean/Base.lean | 2 + backends/lean/Base/Arith.lean | 464 ----------------------------------- backends/lean/Base/Arith/Arith.lean | 409 ++++++++++++++++++++++++++++++ backends/lean/Base/Arith/Base.lean | 10 + backends/lean/Base/ArithBase.lean | 10 - backends/lean/Base/Diverge/Elab.lean | 17 +- backends/lean/Base/Utils.lean | 95 +++++++ 7 files changed, 517 insertions(+), 490 deletions(-) delete mode 100644 backends/lean/Base/Arith.lean create mode 100644 backends/lean/Base/Arith/Arith.lean create mode 100644 backends/lean/Base/Arith/Base.lean delete mode 100644 backends/lean/Base/ArithBase.lean (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base.lean b/backends/lean/Base.lean index 1f8cbc8e..51211704 100644 --- a/backends/lean/Base.lean +++ b/backends/lean/Base.lean @@ -1,3 +1,5 @@ +import Base.Utils import Base.Primitives import Base.Diverge import Base.Arith +import Base.Progress diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean deleted file mode 100644 index 364447ed..00000000 --- a/backends/lean/Base/Arith.lean +++ /dev/null @@ -1,464 +0,0 @@ -/- This file contains tactics to solve arithmetic goals -/ - -import Lean -import Lean.Meta.Tactic.Simp -import Init.Data.List.Basic -import Mathlib.Tactic.RunCmd -import Mathlib.Tactic.Linarith --- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet ---import Mathlib.Tactic.Omega -import Base.Primitives -import Base.ArithBase - -/- -Mathlib tactics: -- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases -- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs -- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num -- should we use linarith or omega? -- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint -- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical --/ - -namespace List - - -- TODO: I could not find this function?? - @[simp] def flatten {a : Type u} : List (List a) → List a - | [] => [] - | x :: ls => x ++ flatten ls - -end List - -namespace Lean - -namespace LocalContext - - open Lean Lean.Elab Command Term Lean.Meta - - -- Small utility: return the list of declarations in the context, from - -- the last to the first. - def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := - lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) [] - - -- Return the list of declarations in the context, but filter the - -- declarations which are considered as implementation details - def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do - let ls ← lctx.getAllDecls - pure (ls.filter (fun d => not d.isImplementationDetail)) - -end LocalContext - -end Lean - -namespace Arith - -open Primitives - --- TODO: move? -theorem ne_zero_is_lt_or_gt {x : Int} (hne : x ≠ 0) : x < 0 ∨ x > 0 := by - cases h: x <;> simp_all - . rename_i n; - cases n <;> simp_all - . apply Int.negSucc_lt_zero - --- TODO: move? -theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by - have hne : x - y ≠ 0 := by - simp - intro h - have: x = y := by linarith - simp_all - have h := ne_zero_is_lt_or_gt hne - match h with - | .inl _ => left; linarith - | .inr _ => right; linarith - --- TODO: move -instance Vec.cast (a : Type): Coe (Vec a) (List a) where coe := λ v => v.val - --- TODO: move -/- Remark: we can't write the following instance because of restrictions about - the type class parameters (`ty` doesn't appear in the return type, which is - forbidden): - - ``` - instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val - ``` - -/ -def Scalar.toInt {ty : ScalarTy} (x : Scalar ty) : Int := x.val - --- Remark: I tried a version of the shape `HasProp {a : Type} (x : a)` --- but the lookup didn't work -class HasProp (a : Sort u) where - prop_ty : a → Prop - prop : ∀ x:a, prop_ty x - -instance (ty : ScalarTy) : HasProp (Scalar ty) where - -- prop_ty is inferred - prop := λ x => And.intro x.hmin x.hmax - -instance (a : Type) : HasProp (Vec a) where - prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize - prop := λ ⟨ _, l ⟩ => l - -class PropHasImp (x : Prop) where - concl : Prop - prop : x → concl - --- This also works for `x ≠ y` because this expression reduces to `¬ x = y` --- and `Ne` is marked as `reducible` -instance (x y : Int) : PropHasImp (¬ x = y) where - concl := x < y ∨ x > y - prop := λ (h:x ≠ y) => ne_is_lt_or_gt h - -open Lean Lean.Elab Command Term Lean.Meta - --- Small utility: print all the declarations in the context -elab "print_all_decls" : tactic => do - let ctx ← Lean.MonadLCtx.getLCtx - for decl in ← ctx.getDecls do - let ty ← Lean.Meta.inferType decl.toExpr - logInfo m!"{decl.toExpr} : {ty}" - pure () - --- Explore a term by decomposing the applications (we explore the applied --- functions and their arguments, but ignore lambdas, forall, etc. - --- should we go inside?). -partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do - -- We do it in a very simpler manner: we deconstruct applications, - -- and recursively explore the sub-expressions. Note that we do - -- not go inside foralls and abstractions (should we?). - e.withApp fun f args => do - let s ← k s f - args.foldlM (foldTermApps k) s - --- Provided a function `k` which lookups type class instances on an expression, --- collect all the instances lookuped by applying `k` on the sub-expressions of `e`. -def collectInstances - (k : Expr → MetaM (Option Expr)) (s : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do - let k s e := do - match ← k e with - | none => pure s - | some i => pure (s.insert i) - foldTermApps k s e - --- Similar to `collectInstances`, but explores all the local declarations in the --- main context. -def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do - Lean.Elab.Tactic.withMainContext do - -- Get the local context - let ctx ← Lean.MonadLCtx.getLCtx - -- Just a matter of precaution - let ctx ← instantiateLCtxMVars ctx - -- Initialize the hashset - let hs := HashSet.empty - -- Explore the declarations - let decls ← ctx.getDecls - decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs - --- Return an instance of `HasProp` for `e` if it has some -def lookupHasProp (e : Expr) : MetaM (Option Expr) := do - trace[Arith] "lookupHasProp" - -- TODO: do we need Lean.observing? - -- This actually eliminates the error messages - Lean.observing? do - trace[Arith] "lookupHasProp: observing" - let ty ← Lean.Meta.inferType e - let hasProp ← mkAppM ``HasProp #[ty] - let hasPropInst ← trySynthInstance hasProp - match hasPropInst with - | LOption.some i => - trace[Arith] "Found HasProp instance" - let i_prop ← mkProjection i (Name.mkSimple "prop") - some (← mkAppM' i_prop #[e]) - | _ => none - --- Collect the instances of `HasProp` for the subexpressions in the context -def collectHasPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do - collectInstancesFromMainCtx lookupHasProp - -elab "display_has_prop_instances" : tactic => do - trace[Arith] "Displaying the HasProp instances" - let hs ← collectHasPropInstancesFromMainCtx - hs.forM fun e => do - trace[Arith] "+ HasProp instance: {e}" - -example (x : U32) : True := by - let i : HasProp U32 := inferInstance - have p := @HasProp.prop _ i x - simp only [HasProp.prop_ty] at p - display_has_prop_instances - simp - --- Return an instance of `PropHasImp` for `e` if it has some -def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do - trace[Arith] "lookupPropHasImp" - -- TODO: do we need Lean.observing? - -- This actually eliminates the error messages - Lean.observing? do - trace[Arith] "lookupPropHasImp: observing" - let ty ← Lean.Meta.inferType e - trace[Arith] "lookupPropHasImp: ty: {ty}" - let cl ← mkAppM ``PropHasImp #[ty] - let inst ← trySynthInstance cl - match inst with - | LOption.some i => - trace[Arith] "Found PropHasImp instance" - let i_prop ← mkProjection i (Name.mkSimple "prop") - some (← mkAppM' i_prop #[e]) - | _ => none - --- Collect the instances of `PropHasImp` for the subexpressions in the context -def collectPropHasImpInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do - collectInstancesFromMainCtx lookupPropHasImp - -elab "display_prop_has_imp_instances" : tactic => do - trace[Arith] "Displaying the PropHasImp instances" - let hs ← collectPropHasImpInstancesFromMainCtx - hs.forM fun e => do - trace[Arith] "+ PropHasImp instance: {e}" - -example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by - display_prop_has_imp_instances - simp - -def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr := - -- I don't think we need that - Lean.Elab.Tactic.withMainContext do - -- Insert the new declaration - let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type - withDecl fun nval => do - -- For debugging - let lctx ← Lean.MonadLCtx.getLCtx - let fid := nval.fvarId! - let decl := lctx.get! fid - trace[Arith] " new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}" - -- - -- Tranform the main goal `?m0` to `let x = nval in ?m1` - let mvarId ← Tactic.getMainGoal - let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType) - let newVal ← mkLetFVars #[nval] newMVar - -- There are two cases: - -- - asLet is true: newVal is `let $name := $val in $newMVar` - -- - asLet is false: ewVal is `λ $name => $newMVar` - -- We need to apply it to `val` - let newVal := if asLet then newVal else mkAppN newVal #[val] - -- Assign the main goal and update the current goal - mvarId.assign newVal - let goals ← Tactic.getUnsolvedGoals - Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals) - -- Return the new value - note: we are in the *new* context, created - -- after the declaration was added, so it will persist - pure nval - -def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit := - -- I don't think we need that - Lean.Elab.Tactic.withMainContext do - -- - let val ← elabTerm val .none - let type ← inferType val - -- In some situations, the type will be left as a metavariable (for instance, - -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will - -- not choose): we force the instantiation of the meta-variable - synthesizeSyntheticMVarsUsingDefault - -- - let _ ← addDecl name val type asLet - -elab "custom_let " n:ident " := " v:term : tactic => do - addDeclSyntax n.getId v (asLet := true) - -elab "custom_have " n:ident " := " v:term : tactic => - addDeclSyntax n.getId v (asLet := false) - -example : Nat := by - custom_let x := 4 - custom_have y := 4 - apply y - -example (x : Bool) : Nat := by - cases x <;> custom_let x := 3 <;> apply x - --- Lookup instances in a context and introduce them with additional declarations. -def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do - let hs ← collectInstancesFromMainCtx lookup - hs.toArray.mapM fun e => do - let type ← inferType e - let name ← mkFreshUserName `h - -- Add a declaration - let nval ← addDecl name e type (asLet := false) - -- Simplify to unfold the declaration to unfold (i.e., the projector) - let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) - -- Add the equational theorem for the decl to unfold - let simpTheorems ← simpTheorems.addDeclToUnfold declToUnfold - let congrTheorems ← getSimpCongrTheorems - let ctx : Simp.Context := { simpTheorems := #[simpTheorems], congrTheorems } - -- Where to apply the simplifier - let loc := Tactic.Location.targets #[mkIdent name] false - -- Apply the simplifier - let _ ← Tactic.simpLocation ctx (discharge? := .none) loc - -- Return the new value - pure nval - --- Lookup the instances of `HasProp for all the sub-expressions in the context, --- and introduce the corresponding assumptions -elab "intro_has_prop_instances" : tactic => do - trace[Arith] "Introducing the HasProp instances" - let _ ← introInstances ``HasProp.prop_ty lookupHasProp - -example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by - intro_has_prop_instances - simp [*] - -example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by - intro_has_prop_instances - simp_all [Scalar.max, Scalar.min] - --- Tactic to split on a disjunction. --- The expression `h` should be an fvar. -def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do - trace[Arith] "assumption on which to split: {h}" - -- Retrieve the main goal - Lean.Elab.Tactic.withMainContext do - let goalType ← Lean.Elab.Tactic.getMainTarget - let hDecl := (← getLCtx).get! h.fvarId! - let hName := hDecl.userName - -- Case disjunction - let hTy ← inferType h - hTy.withApp fun f xs => do - trace[Arith] "as app: {f} {xs}" - -- Sanity check - if ¬ (f.isConstOf ``Or ∧ xs.size = 2) then throwError "Invalid argument to splitDisj" - let a := xs.get! 0 - let b := xs.get! 1 - -- Introduce the new goals - -- Returns: - -- - the match branch - -- - a fresh new mvar id - let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do - -- Introduce a variable for the assumption (`a` or `b`). Note that we reuse - -- the name of the assumption we split. - withLocalDeclD hName hTy fun var => do - -- The new goal - let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName) - -- Clear the assumption that we split - let mgoal ← mgoal.mvarId!.tryClearMany #[h.fvarId!] - -- The branch expression - let branch ← mkLambdaFVars #[var] (mkMVar mgoal) - pure (branch, mgoal) - let (inl, mleft) ← mkGoal a "left" - let (inr, mright) ← mkGoal b "right" - trace[Arith] "left: {inl}: {mleft}" - trace[Arith] "right: {inr}: {mright}" - -- Create the match expression - withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do - let motive ← mkLambdaFVars #[hVar] goalType - let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr] - let mgoal ← Tactic.getMainGoal - trace[Arith] "goals: {← Tactic.getUnsolvedGoals}" - trace[Arith] "main goal: {mgoal}" - mgoal.assign casesExpr - let goals ← Tactic.getUnsolvedGoals - -- Focus on the left - Tactic.setGoals [mleft] - kleft - let leftGoals ← Tactic.getUnsolvedGoals - -- Focus on the right - Tactic.setGoals [mright] - kright - let rightGoals ← Tactic.getUnsolvedGoals - -- Put all the goals back - Tactic.setGoals (leftGoals ++ rightGoals ++ goals) - trace[Arith] "new goals: {← Tactic.getUnsolvedGoals}" - -elab "split_disj " n:ident : tactic => do - Lean.Elab.Tactic.withMainContext do - let decl ← Lean.Meta.getLocalDeclFromUserName n.getId - let fvar := mkFVar decl.fvarId - splitDisj fvar (fun _ => pure ()) (fun _ => pure ()) - -example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by - split_disj h0 - . left; assumption - . right; assumption - --- Lookup the instances of `PropHasImp for all the sub-expressions in the context, --- and introduce the corresponding assumptions -elab "intro_prop_has_imp_instances" : tactic => do - trace[Arith] "Introducing the PropHasImp instances" - let _ ← introInstances ``PropHasImp.concl lookupPropHasImp - -example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by - intro_prop_has_imp_instances - rename_i h - split_disj h - . linarith - . linarith - -/- Boosting a bit the linarith tac. - - We do the following: - - for all the assumptions of the shape `(x : Int) ≠ y` or `¬ (x = y), we - introduce two goals with the assumptions `x < y` and `x > y` - TODO: we could create a PR for mathlib. - -/ -def intTacPreprocess : Tactic.TacticM Unit := do - Lean.Elab.Tactic.withMainContext do - -- Lookup the instances of PropHasImp (this is how we detect assumptions - -- of the proper shape), introduce assumptions in the context and split - -- on those - -- TODO: get rid of the assumptions that we split - let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit := - match asms with - | [] => pure () - | asm :: asms => - let k := splitOnAsms asms - splitDisj asm k k - -- Introduce - let asms ← introInstances ``PropHasImp.concl lookupPropHasImp - -- Split - splitOnAsms asms.toList - -elab "int_tac_preprocess" : tactic => - intTacPreprocess - -example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by - int_tac_preprocess - linarith - linarith - -syntax "int_tac" : tactic -macro_rules - | `(tactic| int_tac) => - `(tactic| - (repeat (apply And.intro)) <;> -- TODO: improve this - int_tac_preprocess <;> - linarith) - -example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by - int_tac - --- Checking that things append correctly when there are several disjunctions -example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by - int_tac - --- A tactic to solve linear arithmetic goals in the presence of scalars -syntax "scalar_tac" : tactic -macro_rules - | `(tactic| scalar_tac) => - `(tactic| - intro_has_prop_instances; - have := Scalar.cMin_bound ScalarTy.Usize; - have := Scalar.cMin_bound ScalarTy.Isize; - have := Scalar.cMax_bound ScalarTy.Usize; - have := Scalar.cMax_bound ScalarTy.Isize; - -- TODO: not too sure about that - simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *; - int_tac) - -example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by - scalar_tac - -example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by - scalar_tac - -end Arith diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean new file mode 100644 index 00000000..0ba73d18 --- /dev/null +++ b/backends/lean/Base/Arith/Arith.lean @@ -0,0 +1,409 @@ +/- This file contains tactics to solve arithmetic goals -/ + +import Lean +import Lean.Meta.Tactic.Simp +import Init.Data.List.Basic +import Mathlib.Tactic.RunCmd +import Mathlib.Tactic.Linarith +-- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet +--import Mathlib.Tactic.Omega +import Base.Primitives +import Base.Utils +import Base.Arith.Base + +/- +Mathlib tactics: +- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases +- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs +- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num +- should we use linarith or omega? +- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint +- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical +-/ + +namespace List + + -- TODO: I could not find this function?? + @[simp] def flatten {a : Type u} : List (List a) → List a + | [] => [] + | x :: ls => x ++ flatten ls + +end List + +namespace Lean + +namespace LocalContext + + open Lean Lean.Elab Command Term Lean.Meta + + -- Small utility: return the list of declarations in the context, from + -- the last to the first. + def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := + lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) [] + + -- Return the list of declarations in the context, but filter the + -- declarations which are considered as implementation details + def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do + let ls ← lctx.getAllDecls + pure (ls.filter (fun d => not d.isImplementationDetail)) + +end LocalContext + +end Lean + +namespace Arith + +open Primitives + +-- TODO: move? +theorem ne_zero_is_lt_or_gt {x : Int} (hne : x ≠ 0) : x < 0 ∨ x > 0 := by + cases h: x <;> simp_all + . rename_i n; + cases n <;> simp_all + . apply Int.negSucc_lt_zero + +-- TODO: move? +theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by + have hne : x - y ≠ 0 := by + simp + intro h + have: x = y := by linarith + simp_all + have h := ne_zero_is_lt_or_gt hne + match h with + | .inl _ => left; linarith + | .inr _ => right; linarith + +-- TODO: move +instance Vec.cast (a : Type): Coe (Vec a) (List a) where coe := λ v => v.val + +-- TODO: move +/- Remark: we can't write the following instance because of restrictions about + the type class parameters (`ty` doesn't appear in the return type, which is + forbidden): + + ``` + instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val + ``` + -/ +def Scalar.toInt {ty : ScalarTy} (x : Scalar ty) : Int := x.val + +-- Remark: I tried a version of the shape `HasProp {a : Type} (x : a)` +-- but the lookup didn't work +class HasProp (a : Sort u) where + prop_ty : a → Prop + prop : ∀ x:a, prop_ty x + +instance (ty : ScalarTy) : HasProp (Scalar ty) where + -- prop_ty is inferred + prop := λ x => And.intro x.hmin x.hmax + +instance (a : Type) : HasProp (Vec a) where + prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize + prop := λ ⟨ _, l ⟩ => l + +class PropHasImp (x : Prop) where + concl : Prop + prop : x → concl + +-- This also works for `x ≠ y` because this expression reduces to `¬ x = y` +-- and `Ne` is marked as `reducible` +instance (x y : Int) : PropHasImp (¬ x = y) where + concl := x < y ∨ x > y + prop := λ (h:x ≠ y) => ne_is_lt_or_gt h + +open Lean Lean.Elab Command Term Lean.Meta + +-- Small utility: print all the declarations in the context +elab "print_all_decls" : tactic => do + let ctx ← Lean.MonadLCtx.getLCtx + for decl in ← ctx.getDecls do + let ty ← Lean.Meta.inferType decl.toExpr + logInfo m!"{decl.toExpr} : {ty}" + pure () + +-- Explore a term by decomposing the applications (we explore the applied +-- functions and their arguments, but ignore lambdas, forall, etc. - +-- should we go inside?). +partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do + -- We do it in a very simpler manner: we deconstruct applications, + -- and recursively explore the sub-expressions. Note that we do + -- not go inside foralls and abstractions (should we?). + e.withApp fun f args => do + let s ← k s f + args.foldlM (foldTermApps k) s + +-- Provided a function `k` which lookups type class instances on an expression, +-- collect all the instances lookuped by applying `k` on the sub-expressions of `e`. +def collectInstances + (k : Expr → MetaM (Option Expr)) (s : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do + let k s e := do + match ← k e with + | none => pure s + | some i => pure (s.insert i) + foldTermApps k s e + +-- Similar to `collectInstances`, but explores all the local declarations in the +-- main context. +def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do + Lean.Elab.Tactic.withMainContext do + -- Get the local context + let ctx ← Lean.MonadLCtx.getLCtx + -- Just a matter of precaution + let ctx ← instantiateLCtxMVars ctx + -- Initialize the hashset + let hs := HashSet.empty + -- Explore the declarations + let decls ← ctx.getDecls + decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs + +-- Return an instance of `HasProp` for `e` if it has some +def lookupHasProp (e : Expr) : MetaM (Option Expr) := do + trace[Arith] "lookupHasProp" + -- TODO: do we need Lean.observing? + -- This actually eliminates the error messages + Lean.observing? do + trace[Arith] "lookupHasProp: observing" + let ty ← Lean.Meta.inferType e + let hasProp ← mkAppM ``HasProp #[ty] + let hasPropInst ← trySynthInstance hasProp + match hasPropInst with + | LOption.some i => + trace[Arith] "Found HasProp instance" + let i_prop ← mkProjection i (Name.mkSimple "prop") + some (← mkAppM' i_prop #[e]) + | _ => none + +-- Collect the instances of `HasProp` for the subexpressions in the context +def collectHasPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do + collectInstancesFromMainCtx lookupHasProp + +elab "display_has_prop_instances" : tactic => do + trace[Arith] "Displaying the HasProp instances" + let hs ← collectHasPropInstancesFromMainCtx + hs.forM fun e => do + trace[Arith] "+ HasProp instance: {e}" + +example (x : U32) : True := by + let i : HasProp U32 := inferInstance + have p := @HasProp.prop _ i x + simp only [HasProp.prop_ty] at p + display_has_prop_instances + simp + +-- Return an instance of `PropHasImp` for `e` if it has some +def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do + trace[Arith] "lookupPropHasImp" + -- TODO: do we need Lean.observing? + -- This actually eliminates the error messages + Lean.observing? do + trace[Arith] "lookupPropHasImp: observing" + let ty ← Lean.Meta.inferType e + trace[Arith] "lookupPropHasImp: ty: {ty}" + let cl ← mkAppM ``PropHasImp #[ty] + let inst ← trySynthInstance cl + match inst with + | LOption.some i => + trace[Arith] "Found PropHasImp instance" + let i_prop ← mkProjection i (Name.mkSimple "prop") + some (← mkAppM' i_prop #[e]) + | _ => none + +-- Collect the instances of `PropHasImp` for the subexpressions in the context +def collectPropHasImpInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do + collectInstancesFromMainCtx lookupPropHasImp + +elab "display_prop_has_imp_instances" : tactic => do + trace[Arith] "Displaying the PropHasImp instances" + let hs ← collectPropHasImpInstancesFromMainCtx + hs.forM fun e => do + trace[Arith] "+ PropHasImp instance: {e}" + +example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by + display_prop_has_imp_instances + simp + +-- Lookup instances in a context and introduce them with additional declarations. +def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do + let hs ← collectInstancesFromMainCtx lookup + hs.toArray.mapM fun e => do + let type ← inferType e + let name ← mkFreshUserName `h + -- Add a declaration + let nval ← Utils.addDecl name e type (asLet := false) + -- Simplify to unfold the declaration to unfold (i.e., the projector) + let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems) + -- Add the equational theorem for the decl to unfold + let simpTheorems ← simpTheorems.addDeclToUnfold declToUnfold + let congrTheorems ← getSimpCongrTheorems + let ctx : Simp.Context := { simpTheorems := #[simpTheorems], congrTheorems } + -- Where to apply the simplifier + let loc := Tactic.Location.targets #[mkIdent name] false + -- Apply the simplifier + let _ ← Tactic.simpLocation ctx (discharge? := .none) loc + -- Return the new value + pure nval + +-- Lookup the instances of `HasProp for all the sub-expressions in the context, +-- and introduce the corresponding assumptions +elab "intro_has_prop_instances" : tactic => do + trace[Arith] "Introducing the HasProp instances" + let _ ← introInstances ``HasProp.prop_ty lookupHasProp + +example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by + intro_has_prop_instances + simp [*] + +example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by + intro_has_prop_instances + simp_all [Scalar.max, Scalar.min] + +-- Tactic to split on a disjunction. +-- The expression `h` should be an fvar. +def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do + trace[Arith] "assumption on which to split: {h}" + -- Retrieve the main goal + Lean.Elab.Tactic.withMainContext do + let goalType ← Lean.Elab.Tactic.getMainTarget + let hDecl := (← getLCtx).get! h.fvarId! + let hName := hDecl.userName + -- Case disjunction + let hTy ← inferType h + hTy.withApp fun f xs => do + trace[Arith] "as app: {f} {xs}" + -- Sanity check + if ¬ (f.isConstOf ``Or ∧ xs.size = 2) then throwError "Invalid argument to splitDisj" + let a := xs.get! 0 + let b := xs.get! 1 + -- Introduce the new goals + -- Returns: + -- - the match branch + -- - a fresh new mvar id + let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do + -- Introduce a variable for the assumption (`a` or `b`). Note that we reuse + -- the name of the assumption we split. + withLocalDeclD hName hTy fun var => do + -- The new goal + let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName) + -- Clear the assumption that we split + let mgoal ← mgoal.mvarId!.tryClearMany #[h.fvarId!] + -- The branch expression + let branch ← mkLambdaFVars #[var] (mkMVar mgoal) + pure (branch, mgoal) + let (inl, mleft) ← mkGoal a "left" + let (inr, mright) ← mkGoal b "right" + trace[Arith] "left: {inl}: {mleft}" + trace[Arith] "right: {inr}: {mright}" + -- Create the match expression + withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do + let motive ← mkLambdaFVars #[hVar] goalType + let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr] + let mgoal ← Tactic.getMainGoal + trace[Arith] "goals: {← Tactic.getUnsolvedGoals}" + trace[Arith] "main goal: {mgoal}" + mgoal.assign casesExpr + let goals ← Tactic.getUnsolvedGoals + -- Focus on the left + Tactic.setGoals [mleft] + kleft + let leftGoals ← Tactic.getUnsolvedGoals + -- Focus on the right + Tactic.setGoals [mright] + kright + let rightGoals ← Tactic.getUnsolvedGoals + -- Put all the goals back + Tactic.setGoals (leftGoals ++ rightGoals ++ goals) + trace[Arith] "new goals: {← Tactic.getUnsolvedGoals}" + +elab "split_disj " n:ident : tactic => do + Lean.Elab.Tactic.withMainContext do + let decl ← Lean.Meta.getLocalDeclFromUserName n.getId + let fvar := mkFVar decl.fvarId + splitDisj fvar (fun _ => pure ()) (fun _ => pure ()) + +example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by + split_disj h0 + . left; assumption + . right; assumption + +-- Lookup the instances of `PropHasImp for all the sub-expressions in the context, +-- and introduce the corresponding assumptions +elab "intro_prop_has_imp_instances" : tactic => do + trace[Arith] "Introducing the PropHasImp instances" + let _ ← introInstances ``PropHasImp.concl lookupPropHasImp + +example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by + intro_prop_has_imp_instances + rename_i h + split_disj h + . linarith + . linarith + +/- Boosting a bit the linarith tac. + + We do the following: + - for all the assumptions of the shape `(x : Int) ≠ y` or `¬ (x = y), we + introduce two goals with the assumptions `x < y` and `x > y` + TODO: we could create a PR for mathlib. + -/ +def intTacPreprocess : Tactic.TacticM Unit := do + Lean.Elab.Tactic.withMainContext do + -- Lookup the instances of PropHasImp (this is how we detect assumptions + -- of the proper shape), introduce assumptions in the context and split + -- on those + -- TODO: get rid of the assumptions that we split + let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit := + match asms with + | [] => pure () + | asm :: asms => + let k := splitOnAsms asms + splitDisj asm k k + -- Introduce + let asms ← introInstances ``PropHasImp.concl lookupPropHasImp + -- Split + splitOnAsms asms.toList + +elab "int_tac_preprocess" : tactic => + intTacPreprocess + +example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by + int_tac_preprocess + linarith + linarith + +syntax "int_tac" : tactic +macro_rules + | `(tactic| int_tac) => + `(tactic| + (repeat (apply And.intro)) <;> -- TODO: improve this + int_tac_preprocess <;> + linarith) + +example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by + int_tac + +-- Checking that things append correctly when there are several disjunctions +example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by + int_tac + +-- A tactic to solve linear arithmetic goals in the presence of scalars +syntax "scalar_tac" : tactic +macro_rules + | `(tactic| scalar_tac) => + `(tactic| + intro_has_prop_instances; + have := Scalar.cMin_bound ScalarTy.Usize; + have := Scalar.cMin_bound ScalarTy.Isize; + have := Scalar.cMax_bound ScalarTy.Usize; + have := Scalar.cMax_bound ScalarTy.Isize; + -- TODO: not too sure about that + simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *; + int_tac) + +example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by + scalar_tac + +example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by + scalar_tac + +end Arith diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean new file mode 100644 index 00000000..ddd2dc24 --- /dev/null +++ b/backends/lean/Base/Arith/Base.lean @@ -0,0 +1,10 @@ +import Lean + +namespace Arith + +open Lean Elab Term Meta + +-- We can't define and use trace classes in the same file +initialize registerTraceClass `Arith + +end Arith diff --git a/backends/lean/Base/ArithBase.lean b/backends/lean/Base/ArithBase.lean deleted file mode 100644 index ddd2dc24..00000000 --- a/backends/lean/Base/ArithBase.lean +++ /dev/null @@ -1,10 +0,0 @@ -import Lean - -namespace Arith - -open Lean Elab Term Meta - --- We can't define and use trace classes in the same file -initialize registerTraceClass `Arith - -end Arith diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index 96f7abc0..f109e847 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -14,8 +14,8 @@ namespace Diverge syntax (name := divergentDef) declModifiers "divergent" "def" declId ppIndent(optDeclSig) declVal : command -open Utils open Lean Elab Term Meta Primitives Lean.Meta +open Utils /- The following was copied from the `wfRecursion` function. -/ @@ -47,21 +47,6 @@ def getSigmaTypes (ty : Expr) : MetaM (Expr × Expr) := do else pure (args.get! 0, args.get! 1) -/- Like `lambdaTelescopeN` but only destructs a fixed number of lambdas -/ -def lambdaTelescopeN (e : Expr) (n : Nat) (k : Array Expr → Expr → MetaM α) : MetaM α := - lambdaTelescope e fun xs body => do - if xs.size < n then throwError "lambdaTelescopeN: not enough lambdas"; - let xs := xs.extract 0 n - let ys := xs.extract n xs.size - let body ← mkLambdaFVars ys body - k xs body - -/- Like `lambdaTelescope`, but only destructs one lambda - TODO: is there an equivalent of this function somewhere in the - standard library? -/ -def lambdaOne (e : Expr) (k : Expr → Expr → MetaM α) : MetaM α := - lambdaTelescopeN e 1 λ xs b => k (xs.get! 0) b - /- Generate a Sigma type from a list of *variables* (all the expressions must be variables). diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 161b9ddb..2ce63620 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -116,4 +116,99 @@ partial def mapVisit (k : Nat → Expr → MetaM Expr) (e : Expr) : MetaM Expr : | .proj _ _ b => return e.updateProj! (← visit (i + 1) b) visit 0 e +section Methods + variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadError m] + variable {a : Type} + + /- Like `lambdaTelescopeN` but only destructs a fixed number of lambdas -/ + def lambdaTelescopeN (e : Expr) (n : Nat) (k : Array Expr → Expr → m a) : m a := + lambdaTelescope e fun xs body => do + if xs.size < n then throwError "lambdaTelescopeN: not enough lambdas" + let xs := xs.extract 0 n + let ys := xs.extract n xs.size + let body ← liftMetaM (mkLambdaFVars ys body) + k xs body + + /- Like `lambdaTelescope`, but only destructs one lambda + TODO: is there an equivalent of this function somewhere in the + standard library? -/ + def lambdaOne (e : Expr) (k : Expr → Expr → m a) : m a := + lambdaTelescopeN e 1 λ xs b => k (xs.get! 0) b + + def isExists (e : Expr) : Bool := e.getAppFn.isConstOf ``Exists ∧ e.getAppNumArgs = 2 + + -- Remark: Lean doesn't find the inhabited and nonempty instances if we don' + -- put them explicitely in the signature + partial def existsTelescopeProcess [Inhabited (m a)] [Nonempty (m a)] + (fvars : Array Expr) (e : Expr) (k : Array Expr → Expr → m a) : m a := do + -- Attempt to deconstruct an existential + if isExists e then do + let p := e.appArg! + lambdaOne p fun x ne => + existsTelescopeProcess (fvars.push x) ne k + else + -- No existential: call the continuation + k fvars e + + def existsTelescope [Inhabited (m a)] [Nonempty (m a)] (e : Expr) (k : Array Expr → Expr → m a) : m a := do + existsTelescopeProcess #[] e k + +end Methods + +def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr := + -- I don't think we need that + Lean.Elab.Tactic.withMainContext do + -- Insert the new declaration + let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type + withDecl fun nval => do + -- For debugging + let lctx ← Lean.MonadLCtx.getLCtx + let fid := nval.fvarId! + let decl := lctx.get! fid + trace[Arith] " new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}" + -- + -- Tranform the main goal `?m0` to `let x = nval in ?m1` + let mvarId ← Tactic.getMainGoal + let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType) + let newVal ← mkLetFVars #[nval] newMVar + -- There are two cases: + -- - asLet is true: newVal is `let $name := $val in $newMVar` + -- - asLet is false: ewVal is `λ $name => $newMVar` + -- We need to apply it to `val` + let newVal := if asLet then newVal else mkAppN newVal #[val] + -- Assign the main goal and update the current goal + mvarId.assign newVal + let goals ← Tactic.getUnsolvedGoals + Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals) + -- Return the new value - note: we are in the *new* context, created + -- after the declaration was added, so it will persist + pure nval + +def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit := + -- I don't think we need that + Lean.Elab.Tactic.withMainContext do + -- + let val ← elabTerm val .none + let type ← inferType val + -- In some situations, the type will be left as a metavariable (for instance, + -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will + -- not choose): we force the instantiation of the meta-variable + synthesizeSyntheticMVarsUsingDefault + -- + let _ ← addDecl name val type asLet + +elab "custom_let " n:ident " := " v:term : tactic => do + addDeclSyntax n.getId v (asLet := true) + +elab "custom_have " n:ident " := " v:term : tactic => + addDeclSyntax n.getId v (asLet := false) + +example : Nat := by + custom_let x := 4 + custom_have y := 4 + apply y + +example (x : Bool) : Nat := by + cases x <;> custom_let x := 3 <;> apply x + end Utils -- cgit v1.3.1 From 6166c410a4b3353377e640acbae9f56e877a9118 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 11 Jul 2023 15:23:49 +0200 Subject: Work on the progress tactic --- backends/lean/Base/Arith.lean | 1 + backends/lean/Base/Arith/Arith.lean | 42 ++++--- backends/lean/Base/Progress.lean | 1 + backends/lean/Base/Progress/Base.lean | 175 ++++++++++++++++++++++++++++++ backends/lean/Base/Progress/Progress.lean | 112 +++++++++++++++++++ backends/lean/Base/Utils.lean | 28 +++++ 6 files changed, 346 insertions(+), 13 deletions(-) create mode 100644 backends/lean/Base/Arith.lean create mode 100644 backends/lean/Base/Progress.lean create mode 100644 backends/lean/Base/Progress/Base.lean create mode 100644 backends/lean/Base/Progress/Progress.lean (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean new file mode 100644 index 00000000..fd5698c5 --- /dev/null +++ b/backends/lean/Base/Arith.lean @@ -0,0 +1 @@ +import Base.Arith.Arith diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean index 0ba73d18..ff628cf3 100644 --- a/backends/lean/Base/Arith/Arith.lean +++ b/backends/lean/Base/Arith/Arith.lean @@ -146,7 +146,7 @@ def collectInstances -- Similar to `collectInstances`, but explores all the local declarations in the -- main context. def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do - Lean.Elab.Tactic.withMainContext do + Tactic.withMainContext do -- Get the local context let ctx ← Lean.MonadLCtx.getLCtx -- Just a matter of precaution @@ -263,8 +263,8 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do trace[Arith] "assumption on which to split: {h}" -- Retrieve the main goal - Lean.Elab.Tactic.withMainContext do - let goalType ← Lean.Elab.Tactic.getMainTarget + Tactic.withMainContext do + let goalType ← Tactic.getMainTarget let hDecl := (← getLCtx).get! h.fvarId! let hName := hDecl.userName -- Case disjunction @@ -316,7 +316,7 @@ def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM U trace[Arith] "new goals: {← Tactic.getUnsolvedGoals}" elab "split_disj " n:ident : tactic => do - Lean.Elab.Tactic.withMainContext do + Tactic.withMainContext do let decl ← Lean.Meta.getLocalDeclFromUserName n.getId let fvar := mkFVar decl.fvarId splitDisj fvar (fun _ => pure ()) (fun _ => pure ()) @@ -347,7 +347,7 @@ example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by TODO: we could create a PR for mathlib. -/ def intTacPreprocess : Tactic.TacticM Unit := do - Lean.Elab.Tactic.withMainContext do + Tactic.withMainContext do -- Lookup the instances of PropHasImp (this is how we detect assumptions -- of the proper shape), introduce assumptions in the context and split -- on those @@ -366,19 +366,31 @@ def intTacPreprocess : Tactic.TacticM Unit := do elab "int_tac_preprocess" : tactic => intTacPreprocess +def intTac : Tactic.TacticM Unit := do + Tactic.withMainContext do + Tactic.focus do + -- Preprocess - wondering if we should do this before or after splitting + -- the goal. I think before leads to a smaller proof term? + Tactic.allGoals intTacPreprocess + -- Split the conjunctions in the goal + Utils.repeatTac Utils.splitConjTarget + -- Call linarith + let linarith := + let cfg : Linarith.LinarithConfig := { + -- We do this with our custom preprocessing + splitNe := false + } + Tactic.liftMetaFinishingTactic <| Linarith.linarith false [] cfg + Tactic.allGoals linarith + +elab "int_tac" : tactic => + intTac + example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by int_tac_preprocess linarith linarith -syntax "int_tac" : tactic -macro_rules - | `(tactic| int_tac) => - `(tactic| - (repeat (apply And.intro)) <;> -- TODO: improve this - int_tac_preprocess <;> - linarith) - example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by int_tac @@ -386,6 +398,10 @@ example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by int_tac +-- Checking that things append correctly when there are several disjunctions +example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by + int_tac + -- A tactic to solve linear arithmetic goals in the presence of scalars syntax "scalar_tac" : tactic macro_rules diff --git a/backends/lean/Base/Progress.lean b/backends/lean/Base/Progress.lean new file mode 100644 index 00000000..d812b896 --- /dev/null +++ b/backends/lean/Base/Progress.lean @@ -0,0 +1 @@ +import Base.Progress.Progress diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean new file mode 100644 index 00000000..3f44f46c --- /dev/null +++ b/backends/lean/Base/Progress/Base.lean @@ -0,0 +1,175 @@ +import Lean +import Base.Utils +import Base.Primitives + +namespace Progress + +open Lean Elab Term Meta +open Utils + +-- We can't define and use trace classes in the same file +initialize registerTraceClass `Progress + +-- Return the first conjunct if the expression is a conjunction, or the +-- expression itself otherwise. Also return the second conjunct if it is a +-- conjunction. +def getFirstConj (e : Expr) : MetaM (Expr × Option Expr) := do + e.withApp fun f args => + if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1)) + else pure (e, none) + +-- Destruct an equaliy and return the two sides +def destEq (e : Expr) : MetaM (Expr × Expr) := do + e.withApp fun f args => + if f.isConstOf ``Eq ∧ args.size = 3 then pure (args.get! 1, args.get! 2) + else throwError "Not an equality: {e}" + +-- Return the set of FVarIds in the expression +partial def getFVarIds (e : Expr) (hs : HashSet FVarId := HashSet.empty) : MetaM (HashSet FVarId) := do + e.withApp fun body args => do + let hs := if body.isFVar then hs.insert body.fvarId! else hs + args.foldlM (fun hs arg => getFVarIds arg hs) hs + +/- # Progress tactic -/ + +structure PSpecDesc where + -- The universally quantified variables + fvars : Array Expr + -- The existentially quantified variables + evars : Array Expr + -- The function + fName : Name + -- The function arguments + fLevels : List Level + args : Array Expr + -- The universally quantified variables which appear in the function arguments + argsFVars : Array FVarId + -- The returned value + ret : Expr + -- The postcondition (if there is) + post : Option Expr + +section Methods + variable [MonadLiftT MetaM m] [MonadControlT MetaM m] [Monad m] [MonadOptions m] + variable [MonadTrace m] [MonadLiftT IO m] [MonadRef m] [AddMessageContext m] + variable [MonadError m] + variable {a : Type} + + /- Analyze a pspec theorem to decompose its arguments. + + PSpec theorems should be of the following shape: + ``` + ∀ x1 ... xn, H1 → ... Hn → ∃ y1 ... ym. f x1 ... xn = .ret ... ∧ Post1 ∧ ... ∧ Postk + ``` + + The continuation `k` receives the following inputs: + - universally quantified variables + - assumptions + - existentially quantified variables + - function name + - function arguments + - return + - postconditions + + TODO: generalize for when we do inductive proofs + -/ + partial + def withPSpec [Inhabited (m a)] [Nonempty (m a)] (th : Expr) (k : PSpecDesc → m a) + (sanityChecks : Bool := false) : + m a := do + trace[Progress] "Theorem: {th}" + -- Dive into the quantified variables and the assumptions + forallTelescope th fun fvars th => do + trace[Progress] "All argumens: {fvars}" + /- -- Filter the argumens which are not propositions + let rec getFirstPropIdx (i : Nat) : MetaM Nat := do + if i ≥ fargs.size then pure i + else do + let x := fargs.get! i + if ← Meta.isProp (← inferType x) then pure i + else getFirstPropIdx (i + 1) + let i ← getFirstPropIdx 0 + let fvars := fargs.extract 0 i + let hyps := fargs.extract i fargs.size + trace[Progress] "Quantified variables: {fvars}" + trace[Progress] "Assumptions: {hyps}" + -- Sanity check: all hypotheses are propositions (in particular, all the + -- quantified variables are at the beginning) + let hypsAreProp ← hyps.allM fun x => do Meta.isProp (← inferType x) + if ¬ hypsAreProp then + throwError "The theorem doesn't have the proper shape: all the quantified arguments should be at the beginning" + -/ + -- Dive into the existentials + existsTelescope th fun evars th => do + trace[Progress] "Existentials: {evars}" + -- Take the first conjunct + let (th, post) ← getFirstConj th + -- Destruct the equality + let (th, ret) ← destEq th + -- Destruct the application to get the name + th.withApp fun f args => do + if ¬ f.isConst then throwError "Not a constant: {f}" + -- Compute the set of universally quantified variables which appear in the function arguments + let allArgsFVars ← args.foldlM (fun hs arg => getFVarIds arg hs) HashSet.empty + -- Sanity check + if sanityChecks then + let fvarsSet : HashSet FVarId := HashSet.ofArray (fvars.map (fun x => x.fvarId!)) + let filtArgsFVars := allArgsFVars.toArray.filter (fun fvar => ¬ fvarsSet.contains fvar) + if ¬ filtArgsFVars.isEmpty then + let filtArgsFVars := filtArgsFVars.map (fun fvarId => Expr.fvar fvarId) + throwError "Some of the function inputs are not universally quantified: {filtArgsFVars}" + let argsFVars := fvars.map (fun x => x.fvarId!) + let argsFVars := argsFVars.filter (fun fvar => allArgsFVars.contains fvar) + -- Return + trace[Progress] "Function: {f.constName!}"; + let thDesc := { + fvars := fvars + evars := evars + fName := f.constName! + fLevels := f.constLevels! + args := args + argsFVars + ret := ret + post := post + } + k thDesc +end Methods + + +def getPSpecFunName (th : Expr) : MetaM Name := + withPSpec th (fun d => do pure d.fName) true + +structure PSpecAttr where + attr : AttributeImpl + ext : MapDeclarationExtension Name + deriving Inhabited + +/- The persistent map from function to pspec theorems. -/ +initialize pspecAttr : PSpecAttr ← do + let ext ← mkMapDeclarationExtension `pspecMap + let attrImpl := { + name := `pspec + descr := "Marks theorems to use with the `progress` tactic" + add := fun thName stx attrKind => do + Attribute.Builtin.ensureNoArgs stx + -- TODO: use the attribute kind + unless attrKind == AttributeKind.global do + throwError "invalid attribute 'pspec', must be global" + -- Lookup the theorem + let env ← getEnv + let thDecl := env.constants.find! thName + let fName ← MetaM.run' (getPSpecFunName thDecl.type) + trace[Progress] "Registering spec theorem for {fName}" + let env := ext.addEntry env (fName, thName) + setEnv env + pure () + } + registerBuiltinAttribute attrImpl + pure { attr := attrImpl, ext := ext } + +def PSpecAttr.find? (s : PSpecAttr) (name : Name) : MetaM (Option Name) := do + return (s.ext.getState (← getEnv)).find? name + --return s.ext.find? (← getEnv) name + + +end Progress diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean new file mode 100644 index 00000000..1b9ee55c --- /dev/null +++ b/backends/lean/Base/Progress/Progress.lean @@ -0,0 +1,112 @@ +import Lean +import Base.Arith +import Base.Progress.Base + +namespace Progress + +open Lean Elab Term Meta Tactic +open Utils + +namespace Test + open Primitives + + set_option trace.Progress true + + @[pspec] + theorem vec_index_test (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) : + ∃ x, v.index α i = .ret x := by + apply + sorry + + #eval pspecAttr.find? ``Primitives.Vec.index +end Test + +#check isDefEq +#check allGoals + +def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do + withMainContext do + -- Retrieve the goal + let mgoal ← Tactic.getMainGoal + let goalTy ← mgoal.getType + -- Dive into the goal to lookup the theorem + let (fName, fLevels, args) ← do + withPSpec goalTy fun desc => + -- TODO: check that no universally quantified variables in the arguments + pure (desc.fName, desc.fLevels, desc.args) + -- TODO: also try the assumptions + trace[Progress] "Function: {fName}" + -- TODO: use a list of theorems, and try them one by one? + let thName ← do + match ← pspecAttr.find? fName with + | none => throwError "Could not find a pspec theorem for {fName}" + | some thName => pure thName + trace[Progress] "Lookuped up: {thName}" + /- Apply the theorem + We try to match the theorem with the goal + In order to do so, we introduce meta-variables for all the parameters + (i.e., quantified variables and assumpions), and unify those with the goal. + Remark: we do not introduce meta-variables for the quantified variables + which don't appear in the function arguments (we want to let them + quantified). + We also make sure that all the meta variables which appear in the + function arguments have been instantiated + -/ + let env ← getEnv + let thDecl := env.constants.find! thName + let thTy := thDecl.type + -- TODO: the tactic fails if we uncomment withNewMCtxDepth + -- withNewMCtxDepth do + let (mvars, binders, thExBody) ← forallMetaTelescope thTy + -- Introduce the existentially quantified variables and the post-condition + -- in the context + let thBody ← + existsTelescope thExBody fun _evars thBody => do + let (thBody, _) ← destEq thBody + -- There shouldn't be any existential variables in thBody + pure thBody + -- Match the body with the target + let target := mkAppN (.const fName fLevels) args + trace[Progress] "mvars:\n{mvars.map Expr.mvarId!}" + trace[Progress] "thBody: {thBody}" + trace[Progress] "target: {target}" + let ok ← isDefEq thBody target + if ¬ ok then throwError "Could not unify the theorem with the target:\n- theorem: {thBody}\n- target: {target}" + postprocessAppMVars `progress mgoal mvars binders true true + Term.synthesizeSyntheticMVarsNoPostponing + let thBody ← instantiateMVars thBody + trace[Progress] "thBody (after instantiation): {thBody}" + -- Add the instantiated theorem to the assumptions (we apply it on the metavariables). + let th ← mkAppOptM thName (mvars.map some) + let asmName ← mkFreshUserName `h + let thTy ← inferType th + let thAsm ← Utils.addDecl asmName th thTy (asLet := false) + -- Update the set of goals + let curGoals ← getUnsolvedGoals + let newGoals := mvars.map Expr.mvarId! + let newGoals ← newGoals.filterM fun mvar => not <$> mvar.isAssigned + trace[Progress] "new goals: {newGoals}" + setGoals newGoals.toList + allGoals asmTac + let newGoals ← getUnsolvedGoals + setGoals (newGoals ++ curGoals) + -- + pure () + +elab "progress" : tactic => do + progressLookupTheorem (firstTac [assumptionTac, Arith.intTac]) + +namespace Test + open Primitives + + set_option trace.Progress true + + @[pspec] + theorem vec_index_test2 (α : Type u) (v: Vec α) (i: Usize) (h: i.val < v.val.length) : + ∃ x, v.index α i = .ret x := by + progress + tauto + +end Test + +end Progress diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 2ce63620..1351f3d4 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -1,4 +1,5 @@ import Lean +import Mathlib.Tactic.Core namespace Utils @@ -211,4 +212,31 @@ example : Nat := by example (x : Bool) : Nat := by cases x <;> custom_let x := 3 <;> apply x +-- Repeatedly apply a tactic +partial def repeatTac (tac : Tactic.TacticM Unit) : Tactic.TacticM Unit := do + try + tac + Tactic.allGoals (Tactic.focus (repeatTac tac)) + -- TODO: does this restore the state? + catch _ => pure () + +def firstTac (tacl : List (Tactic.TacticM Unit)) : Tactic.TacticM Unit := do + match tacl with + | [] => pure () + | tac :: tacl => + try tac + catch _ => firstTac tacl + +-- Split the goal if it is a conjunction +def splitConjTarget : Tactic.TacticM Unit := do + Tactic.withMainContext do + let and_intro := Expr.const ``And.intro [] + let mvarIds' ← _root_.Lean.MVarId.apply (← Tactic.getMainGoal) and_intro + Term.synthesizeSyntheticMVarsNoPostponing + Tactic.replaceMainGoal mvarIds' + +-- Taken from Lean.Elab.Tactic.evalAssumption +def assumptionTac : Tactic.TacticM Unit := + Tactic.liftMetaTactic fun mvarId => do mvarId.assumption; pure [] + end Utils -- cgit v1.3.1 From 3e8060b5501ec83940a4309389a68898df26ebd0 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 17 Jul 2023 23:37:31 +0200 Subject: Reorganize the Lean backend --- backends/lean/Base/Arith.lean | 3 +- backends/lean/Base/Arith/Arith.lean | 329 -------------- backends/lean/Base/Arith/Int.lean | 236 ++++++++++ backends/lean/Base/Arith/Scalar.lean | 48 ++ backends/lean/Base/IList.lean | 127 +----- backends/lean/Base/IList/IList.lean | 142 ++++++ backends/lean/Base/Primitives.lean | 718 +----------------------------- backends/lean/Base/Primitives/Base.lean | 130 ++++++ backends/lean/Base/Primitives/Scalar.lean | 507 +++++++++++++++++++++ backends/lean/Base/Primitives/Vec.lean | 113 +++++ backends/lean/Base/Progress/Progress.lean | 2 + 11 files changed, 1184 insertions(+), 1171 deletions(-) create mode 100644 backends/lean/Base/Arith/Int.lean create mode 100644 backends/lean/Base/Arith/Scalar.lean create mode 100644 backends/lean/Base/IList/IList.lean create mode 100644 backends/lean/Base/Primitives/Base.lean create mode 100644 backends/lean/Base/Primitives/Scalar.lean create mode 100644 backends/lean/Base/Primitives/Vec.lean (limited to 'backends/lean/Base/Arith.lean') diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean index fd5698c5..c0d09fd2 100644 --- a/backends/lean/Base/Arith.lean +++ b/backends/lean/Base/Arith.lean @@ -1 +1,2 @@ -import Base.Arith.Arith +import Base.Arith.Int +import Base.Arith.Scalar diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean index da263e86..e69de29b 100644 --- a/backends/lean/Base/Arith/Arith.lean +++ b/backends/lean/Base/Arith/Arith.lean @@ -1,329 +0,0 @@ -/- This file contains tactics to solve arithmetic goals -/ - -import Lean -import Lean.Meta.Tactic.Simp -import Init.Data.List.Basic -import Mathlib.Tactic.RunCmd -import Mathlib.Tactic.Linarith --- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet ---import Mathlib.Tactic.Omega -import Base.Primitives -import Base.Utils -import Base.Arith.Base - -namespace Arith - -open Primitives Utils - --- TODO: move -/- Remark: we can't write the following instance because of restrictions about - the type class parameters (`ty` doesn't appear in the return type, which is - forbidden): - - ``` - instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val - ``` - -/ -def Scalar.toInt {ty : ScalarTy} (x : Scalar ty) : Int := x.val - --- Remark: I tried a version of the shape `HasScalarProp {a : Type} (x : a)` --- but the lookup didn't work -class HasScalarProp (a : Sort u) where - prop_ty : a → Prop - prop : ∀ x:a, prop_ty x - -class HasIntProp (a : Sort u) where - prop_ty : a → Prop - prop : ∀ x:a, prop_ty x - -instance (ty : ScalarTy) : HasScalarProp (Scalar ty) where - -- prop_ty is inferred - prop := λ x => And.intro x.hmin x.hmax - -instance (a : Type) : HasScalarProp (Vec a) where - prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize - prop := λ ⟨ _, l ⟩ => l - -class PropHasImp (x : Prop) where - concl : Prop - prop : x → concl - --- This also works for `x ≠ y` because this expression reduces to `¬ x = y` --- and `Ne` is marked as `reducible` -instance (x y : Int) : PropHasImp (¬ x = y) where - concl := x < y ∨ x > y - prop := λ (h:x ≠ y) => ne_is_lt_or_gt h - -open Lean Lean.Elab Command Term Lean.Meta - --- Small utility: print all the declarations in the context -elab "print_all_decls" : tactic => do - let ctx ← Lean.MonadLCtx.getLCtx - for decl in ← ctx.getDecls do - let ty ← Lean.Meta.inferType decl.toExpr - logInfo m!"{decl.toExpr} : {ty}" - pure () - --- Explore a term by decomposing the applications (we explore the applied --- functions and their arguments, but ignore lambdas, forall, etc. - --- should we go inside?). -partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do - -- We do it in a very simpler manner: we deconstruct applications, - -- and recursively explore the sub-expressions. Note that we do - -- not go inside foralls and abstractions (should we?). - e.withApp fun f args => do - let s ← k s f - args.foldlM (foldTermApps k) s - --- Provided a function `k` which lookups type class instances on an expression, --- collect all the instances lookuped by applying `k` on the sub-expressions of `e`. -def collectInstances - (k : Expr → MetaM (Option Expr)) (s : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do - let k s e := do - match ← k e with - | none => pure s - | some i => pure (s.insert i) - foldTermApps k s e - --- Similar to `collectInstances`, but explores all the local declarations in the --- main context. -def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do - Tactic.withMainContext do - -- Get the local context - let ctx ← Lean.MonadLCtx.getLCtx - -- Just a matter of precaution - let ctx ← instantiateLCtxMVars ctx - -- Initialize the hashset - let hs := HashSet.empty - -- Explore the declarations - let decls ← ctx.getDecls - decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs - --- Helper -def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do - trace[Arith] fName - -- TODO: do we need Lean.observing? - -- This actually eliminates the error messages - Lean.observing? do - trace[Arith] m!"{fName}: observing" - let ty ← Lean.Meta.inferType e - let hasProp ← mkAppM className #[ty] - let hasPropInst ← trySynthInstance hasProp - match hasPropInst with - | LOption.some i => - trace[Arith] "Found HasScalarProp instance" - let i_prop ← mkProjection i (Name.mkSimple "prop") - some (← mkAppM' i_prop #[e]) - | _ => none - --- Return an instance of `HasIntProp` for `e` if it has some -def lookupHasIntProp (e : Expr) : MetaM (Option Expr) := - lookupProp "lookupHasScalarProp" ``HasIntProp e - --- Return an instance of `HasScalarProp` for `e` if it has some -def lookupHasScalarProp (e : Expr) : MetaM (Option Expr) := - lookupProp "lookupHasScalarProp" ``HasScalarProp e - --- Collect the instances of `HasIntProp` for the subexpressions in the context -def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do - collectInstancesFromMainCtx lookupHasIntProp - --- Collect the instances of `HasScalarProp` for the subexpressions in the context -def collectHasScalarPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do - collectInstancesFromMainCtx lookupHasScalarProp - -elab "display_has_prop_instances" : tactic => do - trace[Arith] "Displaying the HasScalarProp instances" - let hs ← collectHasScalarPropInstancesFromMainCtx - hs.forM fun e => do - trace[Arith] "+ HasScalarProp instance: {e}" - -example (x : U32) : True := by - let i : HasScalarProp U32 := inferInstance - have p := @HasScalarProp.prop _ i x - simp only [HasScalarProp.prop_ty] at p - display_has_prop_instances - simp - --- Return an instance of `PropHasImp` for `e` if it has some -def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do - trace[Arith] "lookupPropHasImp" - -- TODO: do we need Lean.observing? - -- This actually eliminates the error messages - Lean.observing? do - trace[Arith] "lookupPropHasImp: observing" - let ty ← Lean.Meta.inferType e - trace[Arith] "lookupPropHasImp: ty: {ty}" - let cl ← mkAppM ``PropHasImp #[ty] - let inst ← trySynthInstance cl - match inst with - | LOption.some i => - trace[Arith] "Found PropHasImp instance" - let i_prop ← mkProjection i (Name.mkSimple "prop") - some (← mkAppM' i_prop #[e]) - | _ => none - --- Collect the instances of `PropHasImp` for the subexpressions in the context -def collectPropHasImpInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do - collectInstancesFromMainCtx lookupPropHasImp - -elab "display_prop_has_imp_instances" : tactic => do - trace[Arith] "Displaying the PropHasImp instances" - let hs ← collectPropHasImpInstancesFromMainCtx - hs.forM fun e => do - trace[Arith] "+ PropHasImp instance: {e}" - -example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by - display_prop_has_imp_instances - simp - --- Lookup instances in a context and introduce them with additional declarations. -def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do - let hs ← collectInstancesFromMainCtx lookup - hs.toArray.mapM fun e => do - let type ← inferType e - let name ← mkFreshUserName `h - -- Add a declaration - let nval ← Utils.addDeclTac name e type (asLet := false) - -- Simplify to unfold the declaration to unfold (i.e., the projector) - Utils.simpAt [declToUnfold] [] [] (Tactic.Location.targets #[mkIdent name] false) - -- Return the new value - pure nval - -def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do - trace[Arith] "Introducing the HasIntProp instances" - introInstances ``HasIntProp.prop_ty lookupHasIntProp - -def introHasScalarPropInstances : Tactic.TacticM (Array Expr) := do - trace[Arith] "Introducing the HasScalarProp instances" - introInstances ``HasScalarProp.prop_ty lookupHasScalarProp - --- Lookup the instances of `HasScalarProp for all the sub-expressions in the context, --- and introduce the corresponding assumptions -elab "intro_has_prop_instances" : tactic => do - let _ ← introHasScalarPropInstances - -example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by - intro_has_prop_instances - simp [*] - -example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by - intro_has_prop_instances - simp_all [Scalar.max, Scalar.min] - --- Lookup the instances of `PropHasImp for all the sub-expressions in the context, --- and introduce the corresponding assumptions -elab "intro_prop_has_imp_instances" : tactic => do - trace[Arith] "Introducing the PropHasImp instances" - let _ ← introInstances ``PropHasImp.concl lookupPropHasImp - -example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by - intro_prop_has_imp_instances - rename_i h - split_disj h - . linarith - . linarith - -/- Boosting a bit the linarith tac. - - We do the following: - - for all the assumptions of the shape `(x : Int) ≠ y` or `¬ (x = y), we - introduce two goals with the assumptions `x < y` and `x > y` - TODO: we could create a PR for mathlib. - -/ -def intTacPreprocess : Tactic.TacticM Unit := do - Tactic.withMainContext do - -- Lookup the instances of PropHasImp (this is how we detect assumptions - -- of the proper shape), introduce assumptions in the context and split - -- on those - -- TODO: get rid of the assumptions that we split - let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit := - match asms with - | [] => pure () - | asm :: asms => - let k := splitOnAsms asms - Utils.splitDisjTac asm k k - -- Introduce - let _ ← introHasIntPropInstances - let asms ← introInstances ``PropHasImp.concl lookupPropHasImp - -- Split - splitOnAsms asms.toList - -elab "int_tac_preprocess" : tactic => - intTacPreprocess - -def intTac : Tactic.TacticM Unit := do - Tactic.withMainContext do - Tactic.focus do - -- Preprocess - wondering if we should do this before or after splitting - -- the goal. I think before leads to a smaller proof term? - Tactic.allGoals intTacPreprocess - -- Split the conjunctions in the goal - Utils.repeatTac Utils.splitConjTarget - -- Call linarith - let linarith := - let cfg : Linarith.LinarithConfig := { - -- We do this with our custom preprocessing - splitNe := false - } - Tactic.liftMetaFinishingTactic <| Linarith.linarith false [] cfg - Tactic.allGoals linarith - -elab "int_tac" : tactic => - intTac - -example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by - int_tac_preprocess - linarith - linarith - -example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by - int_tac - --- Checking that things append correctly when there are several disjunctions -example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by - int_tac - --- Checking that things append correctly when there are several disjunctions -example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by - int_tac - -def scalarTacPreprocess (tac : Tactic.TacticM Unit) : Tactic.TacticM Unit := do - Tactic.withMainContext do - -- Introduce the scalar bounds - let _ ← introHasScalarPropInstances - Tactic.allGoals do - -- Inroduce the bounds for the isize/usize types - let add (e : Expr) : Tactic.TacticM Unit := do - let ty ← inferType e - let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false) - add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []]) - add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) - add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) - -- Reveal the concrete bounds - Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, - ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min, - ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max, - ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min, - ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max - ] [] [] .wildcard - -- Finish the proof - tac - -elab "scalar_tac_preprocess" : tactic => - scalarTacPreprocess intTacPreprocess - --- A tactic to solve linear arithmetic goals in the presence of scalars -def scalarTac : Tactic.TacticM Unit := do - scalarTacPreprocess intTac - -elab "scalar_tac" : tactic => - scalarTac - -example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by - scalar_tac - -example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by - scalar_tac - -end Arith diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean new file mode 100644 index 00000000..5f00ab52 --- /dev/null +++ b/backends/lean/Base/Arith/Int.lean @@ -0,0 +1,236 @@ +/- This file contains tactics to solve arithmetic goals -/ + +import Lean +import Lean.Meta.Tactic.Simp +import Init.Data.List.Basic +import Mathlib.Tactic.RunCmd +import Mathlib.Tactic.Linarith +-- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet +--import Mathlib.Tactic.Omega +import Base.Utils +import Base.Arith.Base + +namespace Arith + +open Utils + +-- Remark: I tried a version of the shape `HasScalarProp {a : Type} (x : a)` +-- but the lookup didn't work +class HasIntProp (a : Sort u) where + prop_ty : a → Prop + prop : ∀ x:a, prop_ty x + +class PropHasImp (x : Prop) where + concl : Prop + prop : x → concl + +-- This also works for `x ≠ y` because this expression reduces to `¬ x = y` +-- and `Ne` is marked as `reducible` +instance (x y : Int) : PropHasImp (¬ x = y) where + concl := x < y ∨ x > y + prop := λ (h:x ≠ y) => ne_is_lt_or_gt h + +open Lean Lean.Elab Lean.Meta + +-- Small utility: print all the declarations in the context +elab "print_all_decls" : tactic => do + let ctx ← Lean.MonadLCtx.getLCtx + for decl in ← ctx.getDecls do + let ty ← Lean.Meta.inferType decl.toExpr + logInfo m!"{decl.toExpr} : {ty}" + pure () + +-- Explore a term by decomposing the applications (we explore the applied +-- functions and their arguments, but ignore lambdas, forall, etc. - +-- should we go inside?). +partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do + -- We do it in a very simpler manner: we deconstruct applications, + -- and recursively explore the sub-expressions. Note that we do + -- not go inside foralls and abstractions (should we?). + e.withApp fun f args => do + let s ← k s f + args.foldlM (foldTermApps k) s + +-- Provided a function `k` which lookups type class instances on an expression, +-- collect all the instances lookuped by applying `k` on the sub-expressions of `e`. +def collectInstances + (k : Expr → MetaM (Option Expr)) (s : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do + let k s e := do + match ← k e with + | none => pure s + | some i => pure (s.insert i) + foldTermApps k s e + +-- Similar to `collectInstances`, but explores all the local declarations in the +-- main context. +def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do + Tactic.withMainContext do + -- Get the local context + let ctx ← Lean.MonadLCtx.getLCtx + -- Just a matter of precaution + let ctx ← instantiateLCtxMVars ctx + -- Initialize the hashset + let hs := HashSet.empty + -- Explore the declarations + let decls ← ctx.getDecls + decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs + +-- Helper +def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do + trace[Arith] fName + -- TODO: do we need Lean.observing? + -- This actually eliminates the error messages + Lean.observing? do + trace[Arith] m!"{fName}: observing" + let ty ← Lean.Meta.inferType e + let hasProp ← mkAppM className #[ty] + let hasPropInst ← trySynthInstance hasProp + match hasPropInst with + | LOption.some i => + trace[Arith] "Found {fName} instance" + let i_prop ← mkProjection i (Name.mkSimple "prop") + some (← mkAppM' i_prop #[e]) + | _ => none + +-- Return an instance of `HasIntProp` for `e` if it has some +def lookupHasIntProp (e : Expr) : MetaM (Option Expr) := + lookupProp "lookupHasIntProp" ``HasIntProp e + +-- Collect the instances of `HasIntProp` for the subexpressions in the context +def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do + collectInstancesFromMainCtx lookupHasIntProp + +-- Return an instance of `PropHasImp` for `e` if it has some +def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do + trace[Arith] "lookupPropHasImp" + -- TODO: do we need Lean.observing? + -- This actually eliminates the error messages + Lean.observing? do + trace[Arith] "lookupPropHasImp: observing" + let ty ← Lean.Meta.inferType e + trace[Arith] "lookupPropHasImp: ty: {ty}" + let cl ← mkAppM ``PropHasImp #[ty] + let inst ← trySynthInstance cl + match inst with + | LOption.some i => + trace[Arith] "Found PropHasImp instance" + let i_prop ← mkProjection i (Name.mkSimple "prop") + some (← mkAppM' i_prop #[e]) + | _ => none + +-- Collect the instances of `PropHasImp` for the subexpressions in the context +def collectPropHasImpInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do + collectInstancesFromMainCtx lookupPropHasImp + +elab "display_prop_has_imp_instances" : tactic => do + trace[Arith] "Displaying the PropHasImp instances" + let hs ← collectPropHasImpInstancesFromMainCtx + hs.forM fun e => do + trace[Arith] "+ PropHasImp instance: {e}" + +example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by + display_prop_has_imp_instances + simp + +-- Lookup instances in a context and introduce them with additional declarations. +def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do + let hs ← collectInstancesFromMainCtx lookup + hs.toArray.mapM fun e => do + let type ← inferType e + let name ← mkFreshUserName `h + -- Add a declaration + let nval ← Utils.addDeclTac name e type (asLet := false) + -- Simplify to unfold the declaration to unfold (i.e., the projector) + Utils.simpAt [declToUnfold] [] [] (Tactic.Location.targets #[mkIdent name] false) + -- Return the new value + pure nval + +def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do + trace[Arith] "Introducing the HasIntProp instances" + introInstances ``HasIntProp.prop_ty lookupHasIntProp + +-- Lookup the instances of `HasIntProp for all the sub-expressions in the context, +-- and introduce the corresponding assumptions +elab "intro_has_int_prop_instances" : tactic => do + let _ ← introHasIntPropInstances + +-- Lookup the instances of `PropHasImp for all the sub-expressions in the context, +-- and introduce the corresponding assumptions +elab "intro_prop_has_imp_instances" : tactic => do + trace[Arith] "Introducing the PropHasImp instances" + let _ ← introInstances ``PropHasImp.concl lookupPropHasImp + +example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by + intro_prop_has_imp_instances + rename_i h + split_disj h + . linarith + . linarith + +/- Boosting a bit the linarith tac. + + We do the following: + - for all the assumptions of the shape `(x : Int) ≠ y` or `¬ (x = y), we + introduce two goals with the assumptions `x < y` and `x > y` + TODO: we could create a PR for mathlib. + -/ +def intTacPreprocess (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM Unit := do + Tactic.withMainContext do + -- Lookup the instances of PropHasImp (this is how we detect assumptions + -- of the proper shape), introduce assumptions in the context and split + -- on those + -- TODO: get rid of the assumptions that we split + let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit := + match asms with + | [] => pure () + | asm :: asms => + let k := splitOnAsms asms + Utils.splitDisjTac asm k k + -- Introduce the scalar bounds + let _ ← introHasIntPropInstances + -- Extra preprocessing, before we split on the disjunctions + extraPreprocess + -- Split + let asms ← introInstances ``PropHasImp.concl lookupPropHasImp + splitOnAsms asms.toList + +elab "int_tac_preprocess" : tactic => + intTacPreprocess (do pure ()) + +def intTac (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM Unit := do + Tactic.withMainContext do + Tactic.focus do + -- Preprocess - wondering if we should do this before or after splitting + -- the goal. I think before leads to a smaller proof term? + Tactic.allGoals (intTacPreprocess extraPreprocess) + -- Split the conjunctions in the goal + Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget) + -- Call linarith + let linarith := + let cfg : Linarith.LinarithConfig := { + -- We do this with our custom preprocessing + splitNe := false + } + Tactic.liftMetaFinishingTactic <| Linarith.linarith false [] cfg + Tactic.allGoals linarith + +elab "int_tac" : tactic => + intTac (do pure ()) + +example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by + int_tac_preprocess + linarith + linarith + +example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by + int_tac + +-- Checking that things append correctly when there are several disjunctions +example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by + int_tac + +-- Checking that things append correctly when there are several disjunctions +example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by + int_tac + +end Arith diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean new file mode 100644 index 00000000..f8903ecf --- /dev/null +++ b/backends/lean/Base/Arith/Scalar.lean @@ -0,0 +1,48 @@ +import Base.Arith.Int +import Base.Primitives.Scalar + +/- Automation for scalars - TODO: not sure it is worth having two files (Int.lean and Scalar.lean) -/ +namespace Arith + +open Lean Lean.Elab Lean.Meta +open Primitives + +def scalarTacExtraPreprocess : Tactic.TacticM Unit := do + Tactic.withMainContext do + -- Inroduce the bounds for the isize/usize types + let add (e : Expr) : Tactic.TacticM Unit := do + let ty ← inferType e + let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false) + add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []]) + add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) + add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) + -- Reveal the concrete bounds + Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, + ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min, + ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max, + ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min, + ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max + ] [] [] .wildcard + +elab "scalar_tac_preprocess" : tactic => + intTacPreprocess scalarTacExtraPreprocess + +-- A tactic to solve linear arithmetic goals in the presence of scalars +def scalarTac : Tactic.TacticM Unit := do + intTac scalarTacExtraPreprocess + +elab "scalar_tac" : tactic => + scalarTac + +instance (ty : ScalarTy) : HasIntProp (Scalar ty) where + -- prop_ty is inferred + prop := λ x => And.intro x.hmin x.hmax + +example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by + intro_has_int_prop_instances + simp [*] + +example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by + scalar_tac + +end Arith diff --git a/backends/lean/Base/IList.lean b/backends/lean/Base/IList.lean index 3db00cbb..31b66ffa 100644 --- a/backends/lean/Base/IList.lean +++ b/backends/lean/Base/IList.lean @@ -1,126 +1 @@ -/- Complementary list functions and lemmas which operate on integers rather - than natural numbers. -/ - -import Std.Data.Int.Lemmas -import Mathlib.Tactic.Linarith -import Base.Arith - -namespace List - -def len (ls : List α) : Int := - match ls with - | [] => 0 - | _ :: tl => 1 + len tl - --- Remark: if i < 0, then the result is none -def optIndex (i : Int) (ls : List α) : Option α := - match ls with - | [] => none - | hd :: tl => if i = 0 then some hd else optIndex (i - 1) tl - --- Remark: if i < 0, then the result is the defaul element -def index [Inhabited α] (i : Int) (ls : List α) : α := - match ls with - | [] => Inhabited.default - | x :: tl => - if i = 0 then x else index (i - 1) tl - --- Remark: the list is unchanged if the index is not in bounds (in particular --- if it is < 0) -def update (ls : List α) (i : Int) (y : α) : List α := - match ls with - | [] => [] - | x :: tl => if i = 0 then y :: tl else x :: update tl (i - 1) y - --- Remark: the whole list is dropped if the index is not in bounds (in particular --- if it is < 0) -def idrop (i : Int) (ls : List α) : List α := - match ls with - | [] => [] - | x :: tl => if i = 0 then x :: tl else idrop (i - 1) tl - -@[simp] theorem len_nil : len ([] : List α) = 0 := by simp [len] -@[simp] theorem len_cons : len ((x :: tl) : List α) = 1 + len tl := by simp [len] - -@[simp] theorem index_zero_cons [Inhabited α] : index 0 ((x :: tl) : List α) = x := by simp [index] -@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index i ((x :: tl) : List α) = index (i - 1) tl := by simp [*, index] - -@[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update] -@[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update] -@[simp] theorem update_nzero_cons (hne : i ≠ 0) : update ((x :: tl) : List α) i y = x :: update tl (i - 1) y := by simp [*, update] - -@[simp] theorem idrop_nil : idrop i ([] : List α) = [] := by simp [idrop] -@[simp] theorem idrop_zero : idrop 0 (ls : List α) = ls := by cases ls <;> simp [idrop] -@[simp] theorem idrop_nzero_cons (hne : i ≠ 0) : idrop i ((x :: tl) : List α) = idrop (i - 1) tl := by simp [*, idrop] - -theorem len_eq_length (ls : List α) : ls.len = ls.length := by - induction ls - . rfl - . simp [*, Int.ofNat_succ, Int.add_comm] - -theorem len_pos : 0 ≤ (ls : List α).len := by - induction ls <;> simp [*] - linarith - -instance (a : Type u) : Arith.HasIntProp (List a) where - prop_ty := λ ls => 0 ≤ ls.len - prop := λ ls => ls.len_pos - -@[simp] theorem len_append (l1 l2 : List α) : (l1 ++ l2).len = l1.len + l2.len := by - -- Remark: simp loops here because of the following rewritings: - -- @Nat.cast_add: ↑(List.length l1 + List.length l2) ==> ↑(List.length l1) + ↑(List.length l2) - -- Int.ofNat_add_ofNat: ↑(List.length l1) + ↑(List.length l2) ==> ↑(List.length l1 + List.length l2) - -- TODO: post an issue? - simp only [len_eq_length] - simp only [length_append] - simp only [Int.ofNat_add] - -theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1'.length) : - l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by - revert l1' - induction l1 - . intro l1'; cases l1' <;> simp [*] - . intro l1'; cases l1' <;> simp_all; tauto - -theorem right_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.length = l2'.length) : - l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by - have := left_length_eq_append_eq l1 l2 l1' l2' - constructor <;> intro heq2 <;> - have : l1.length + l2.length = l1'.length + l2'.length := by - have : (l1 ++ l2).length = (l1' ++ l2').length := by simp [*] - simp only [length_append] at this - apply this - . simp [heq] at this - tauto - . tauto - -theorem left_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.len = l1'.len) : - l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by - simp [len_eq_length] at heq - apply left_length_eq_append_eq - assumption - -theorem right_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.len = l2'.len) : - l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by - simp [len_eq_length] at heq - apply right_length_eq_append_eq - assumption - -open Arith in -theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by - revert i - induction ls <;> simp [*] - rename_i hd tl hi - intro i hineq - if heq: i = 0 then - simp [*] at * - have := tl.len_pos - linarith - else - simp at hineq - have : 0 < i := by int_tac - simp [*] - apply hi - linarith - -end List +import Base.IList.IList diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean new file mode 100644 index 00000000..2a335cac --- /dev/null +++ b/backends/lean/Base/IList/IList.lean @@ -0,0 +1,142 @@ +/- Complementary list functions and lemmas which operate on integers rather + than natural numbers. -/ + +import Std.Data.Int.Lemmas +import Base.Arith + +namespace List + +def len (ls : List α) : Int := + match ls with + | [] => 0 + | _ :: tl => 1 + len tl + +-- Remark: if i < 0, then the result is none +def indexOpt (ls : List α) (i : Int) : Option α := + match ls with + | [] => none + | hd :: tl => if i = 0 then some hd else indexOpt tl (i - 1) + +-- Remark: if i < 0, then the result is the defaul element +def index [Inhabited α] (ls : List α) (i : Int) : α := + match ls with + | [] => Inhabited.default + | x :: tl => + if i = 0 then x else index tl (i - 1) + +-- Remark: the list is unchanged if the index is not in bounds (in particular +-- if it is < 0) +def update (ls : List α) (i : Int) (y : α) : List α := + match ls with + | [] => [] + | x :: tl => if i = 0 then y :: tl else x :: update tl (i - 1) y + +-- Remark: the whole list is dropped if the index is not in bounds (in particular +-- if it is < 0) +def idrop (i : Int) (ls : List α) : List α := + match ls with + | [] => [] + | x :: tl => if i = 0 then x :: tl else idrop (i - 1) tl + +section Lemmas + +variable {α : Type u} + +@[simp] theorem len_nil : len ([] : List α) = 0 := by simp [len] +@[simp] theorem len_cons : len ((x :: tl) : List α) = 1 + len tl := by simp [len] + +@[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index] +@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index] + +@[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update] +@[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update] +@[simp] theorem update_nzero_cons (hne : i ≠ 0) : update ((x :: tl) : List α) i y = x :: update tl (i - 1) y := by simp [*, update] + +@[simp] theorem idrop_nil : idrop i ([] : List α) = [] := by simp [idrop] +@[simp] theorem idrop_zero : idrop 0 (ls : List α) = ls := by cases ls <;> simp [idrop] +@[simp] theorem idrop_nzero_cons (hne : i ≠ 0) : idrop i ((x :: tl) : List α) = idrop (i - 1) tl := by simp [*, idrop] + +theorem len_eq_length (ls : List α) : ls.len = ls.length := by + induction ls + . rfl + . simp [*, Int.ofNat_succ, Int.add_comm] + +@[simp] theorem len_append (l1 l2 : List α) : (l1 ++ l2).len = l1.len + l2.len := by + -- Remark: simp loops here because of the following rewritings: + -- @Nat.cast_add: ↑(List.length l1 + List.length l2) ==> ↑(List.length l1) + ↑(List.length l2) + -- Int.ofNat_add_ofNat: ↑(List.length l1) + ↑(List.length l2) ==> ↑(List.length l1 + List.length l2) + -- TODO: post an issue? + simp only [len_eq_length] + simp only [length_append] + simp only [Int.ofNat_add] + +@[simp] +theorem length_update (ls : List α) (i : Int) (x : α) : (ls.update i x).length = ls.length := by + revert i + induction ls <;> simp_all [length, update] + intro; split <;> simp [*] + +@[simp] +theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.len := by + simp [len_eq_length] + + +theorem len_pos : 0 ≤ (ls : List α).len := by + induction ls <;> simp [*] + linarith + +instance (a : Type u) : Arith.HasIntProp (List a) where + prop_ty := λ ls => 0 ≤ ls.len + prop := λ ls => ls.len_pos + +theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1'.length) : + l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by + revert l1' + induction l1 + . intro l1'; cases l1' <;> simp [*] + . intro l1'; cases l1' <;> simp_all; tauto + +theorem right_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.length = l2'.length) : + l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by + have := left_length_eq_append_eq l1 l2 l1' l2' + constructor <;> intro heq2 <;> + have : l1.length + l2.length = l1'.length + l2'.length := by + have : (l1 ++ l2).length = (l1' ++ l2').length := by simp [*] + simp only [length_append] at this + apply this + . simp [heq] at this + tauto + . tauto + +theorem left_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.len = l1'.len) : + l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by + simp [len_eq_length] at heq + apply left_length_eq_append_eq + assumption + +theorem right_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.len = l2'.len) : + l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by + simp [len_eq_length] at heq + apply right_length_eq_append_eq + assumption + +open Arith in +theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by + revert i + induction ls <;> simp [*] + rename_i hd tl hi + intro i hineq + if heq: i = 0 then + simp [*] at * + have := tl.len_pos + linarith + else + simp at hineq + have : 0 < i := by int_tac + simp [*] + apply hi + linarith + +end Lemmas + +end List diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index 1a0c665d..91823cb6 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -1,715 +1,3 @@ -import Lean -import Lean.Meta.Tactic.Simp -import Init.Data.List.Basic -import Mathlib.Tactic.RunCmd -import Mathlib.Tactic.Linarith - -namespace Primitives - --------------------- --- ASSERT COMMAND --Std. --------------------- - -open Lean Elab Command Term Meta - -syntax (name := assert) "#assert" term: command - -@[command_elab assert] -unsafe -def assertImpl : CommandElab := fun (_stx: Syntax) => do - runTermElabM (fun _ => do - let r ← evalTerm Bool (mkConst ``Bool) _stx[1] - if not r then - logInfo ("Assertion failed for:\n" ++ _stx[1]) - throwError ("Expression reduced to false:\n" ++ _stx[1]) - pure ()) - -#eval 2 == 2 -#assert (2 == 2) - -------------- --- PRELUDE -- -------------- - --- Results & monadic combinators - -inductive Error where - | assertionFailure: Error - | integerOverflow: Error - | divisionByZero: Error - | arrayOutOfBounds: Error - | maximumSizeExceeded: Error - | panic: Error -deriving Repr, BEq - -open Error - -inductive Result (α : Type u) where - | ret (v: α): Result α - | fail (e: Error): Result α - | div -deriving Repr, BEq - -open Result - -instance Result_Inhabited (α : Type u) : Inhabited (Result α) := - Inhabited.mk (fail panic) - -instance Result_Nonempty (α : Type u) : Nonempty (Result α) := - Nonempty.intro div - -/- HELPERS -/ - -def ret? {α: Type u} (r: Result α): Bool := - match r with - | ret _ => true - | fail _ | div => false - -def div? {α: Type u} (r: Result α): Bool := - match r with - | div => true - | ret _ | fail _ => false - -def massert (b:Bool) : Result Unit := - if b then ret () else fail assertionFailure - -def eval_global {α: Type u} (x: Result α) (_: ret? x): α := - match x with - | fail _ | div => by contradiction - | ret x => x - -/- DO-DSL SUPPORT -/ - -def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β := - match x with - | ret v => f v - | fail v => fail v - | div => div - --- Allows using Result in do-blocks -instance : Bind Result where - bind := bind - --- Allows using return x in do-blocks -instance : Pure Result where - pure := fun x => ret x - -@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind] -@[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind] -@[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind] - -/- CUSTOM-DSL SUPPORT -/ - --- Let-binding the Result of a monadic operation is oftentimes not sufficient, --- because we may need a hypothesis for equational reasoning in the scope. We --- rely on subtype, and a custom let-binding operator, in effect recreating our --- own variant of the do-dsl - -def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := - match o with - | ret x => ret ⟨x, rfl⟩ - | fail e => fail e - | div => div - -@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) : - (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind] - -@[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) : - (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind] - -@[simp] theorem bind_tc_div (f : α → Result β) : - (do let y ← div; f y) = div := by simp [Bind.bind, bind] - ----------------------- --- MACHINE INTEGERS -- ----------------------- - --- We redefine our machine integers types. - --- For Isize/Usize, we reuse `getNumBits` from `USize`. You cannot reduce `getNumBits` --- using the simplifier, meaning that proofs do not depend on the compile-time value of --- USize.size. (Lean assumes 32 or 64-bit platforms, and Rust doesn't really support, at --- least officially, 16-bit microcontrollers, so this seems like a fine design decision --- for now.) - --- Note from Chris Bailey: "If there's more than one salient property of your --- definition then the subtyping strategy might get messy, and the property part --- of a subtype is less discoverable by the simplifier or tactics like --- library_search." So, we will not add refinements on the return values of the --- operations defined on Primitives, but will rather rely on custom lemmas to --- invert on possible return values of the primitive operations. - --- Machine integer constants, done via `ofNatCore`, which requires a proof that --- the `Nat` fits within the desired integer type. We provide a custom tactic. - -open System.Platform.getNumBits - --- TODO: is there a way of only importing System.Platform.getNumBits? --- -@[simp] def size_num_bits : Nat := (System.Platform.getNumBits ()).val - --- Remark: Lean seems to use < for the comparisons with the upper bounds by convention. - --- The "structured" bounds -def Isize.smin : Int := - (HPow.hPow 2 (size_num_bits - 1)) -def Isize.smax : Int := (HPow.hPow 2 (size_num_bits - 1)) - 1 -def I8.smin : Int := - (HPow.hPow 2 7) -def I8.smax : Int := HPow.hPow 2 7 - 1 -def I16.smin : Int := - (HPow.hPow 2 15) -def I16.smax : Int := HPow.hPow 2 15 - 1 -def I32.smin : Int := -(HPow.hPow 2 31) -def I32.smax : Int := HPow.hPow 2 31 - 1 -def I64.smin : Int := -(HPow.hPow 2 63) -def I64.smax : Int := HPow.hPow 2 63 - 1 -def I128.smin : Int := -(HPow.hPow 2 127) -def I128.smax : Int := HPow.hPow 2 127 - 1 -def Usize.smin : Int := 0 -def Usize.smax : Int := HPow.hPow 2 size_num_bits - 1 -def U8.smin : Int := 0 -def U8.smax : Int := HPow.hPow 2 8 - 1 -def U16.smin : Int := 0 -def U16.smax : Int := HPow.hPow 2 16 - 1 -def U32.smin : Int := 0 -def U32.smax : Int := HPow.hPow 2 32 - 1 -def U64.smin : Int := 0 -def U64.smax : Int := HPow.hPow 2 64 - 1 -def U128.smin : Int := 0 -def U128.smax : Int := HPow.hPow 2 128 - 1 - --- The "normalized" bounds, that we use in practice -def I8.min := -128 -def I8.max := 127 -def I16.min := -32768 -def I16.max := 32767 -def I32.min := -2147483648 -def I32.max := 2147483647 -def I64.min := -9223372036854775808 -def I64.max := 9223372036854775807 -def I128.min := -170141183460469231731687303715884105728 -def I128.max := 170141183460469231731687303715884105727 -@[simp] def U8.min := 0 -def U8.max := 255 -@[simp] def U16.min := 0 -def U16.max := 65535 -@[simp] def U32.min := 0 -def U32.max := 4294967295 -@[simp] def U64.min := 0 -def U64.max := 18446744073709551615 -@[simp] def U128.min := 0 -def U128.max := 340282366920938463463374607431768211455 -@[simp] def Usize.min := 0 - -def Isize.refined_min : { n:Int // n = I32.min ∨ n = I64.min } := - ⟨ Isize.smin, by - simp [Isize.smin] - cases System.Platform.numBits_eq <;> - unfold System.Platform.numBits at * <;> simp [*] ⟩ - -def Isize.refined_max : { n:Int // n = I32.max ∨ n = I64.max } := - ⟨ Isize.smax, by - simp [Isize.smax] - cases System.Platform.numBits_eq <;> - unfold System.Platform.numBits at * <;> simp [*] ⟩ - -def Usize.refined_max : { n:Int // n = U32.max ∨ n = U64.max } := - ⟨ Usize.smax, by - simp [Usize.smax] - cases System.Platform.numBits_eq <;> - unfold System.Platform.numBits at * <;> simp [*] ⟩ - -def Isize.min := Isize.refined_min.val -def Isize.max := Isize.refined_max.val -def Usize.max := Usize.refined_max.val - -inductive ScalarTy := -| Isize -| I8 -| I16 -| I32 -| I64 -| I128 -| Usize -| U8 -| U16 -| U32 -| U64 -| U128 - -def Scalar.smin (ty : ScalarTy) : Int := - match ty with - | .Isize => Isize.smin - | .I8 => I8.smin - | .I16 => I16.smin - | .I32 => I32.smin - | .I64 => I64.smin - | .I128 => I128.smin - | .Usize => Usize.smin - | .U8 => U8.smin - | .U16 => U16.smin - | .U32 => U32.smin - | .U64 => U64.smin - | .U128 => U128.smin - -def Scalar.smax (ty : ScalarTy) : Int := - match ty with - | .Isize => Isize.smax - | .I8 => I8.smax - | .I16 => I16.smax - | .I32 => I32.smax - | .I64 => I64.smax - | .I128 => I128.smax - | .Usize => Usize.smax - | .U8 => U8.smax - | .U16 => U16.smax - | .U32 => U32.smax - | .U64 => U64.smax - | .U128 => U128.smax - -def Scalar.min (ty : ScalarTy) : Int := - match ty with - | .Isize => Isize.min - | .I8 => I8.min - | .I16 => I16.min - | .I32 => I32.min - | .I64 => I64.min - | .I128 => I128.min - | .Usize => Usize.min - | .U8 => U8.min - | .U16 => U16.min - | .U32 => U32.min - | .U64 => U64.min - | .U128 => U128.min - -def Scalar.max (ty : ScalarTy) : Int := - match ty with - | .Isize => Isize.max - | .I8 => I8.max - | .I16 => I16.max - | .I32 => I32.max - | .I64 => I64.max - | .I128 => I128.max - | .Usize => Usize.max - | .U8 => U8.max - | .U16 => U16.max - | .U32 => U32.max - | .U64 => U64.max - | .U128 => U128.max - -def Scalar.smin_eq (ty : ScalarTy) : Scalar.min ty = Scalar.smin ty := by - cases ty <;> rfl - -def Scalar.smax_eq (ty : ScalarTy) : Scalar.max ty = Scalar.smax ty := by - cases ty <;> rfl - --- "Conservative" bounds --- We use those because we can't compare to the isize bounds (which can't --- reduce at compile-time). Whenever we perform an arithmetic operation like --- addition we need to check that the result is in bounds: we first compare --- to the conservative bounds, which reduce, then compare to the real bounds. --- This is useful for the various #asserts that we want to reduce at --- type-checking time. -def Scalar.cMin (ty : ScalarTy) : Int := - match ty with - | .Isize => Scalar.min .I32 - | _ => Scalar.min ty - -def Scalar.cMax (ty : ScalarTy) : Int := - match ty with - | .Isize => Scalar.max .I32 - | .Usize => Scalar.max .U32 - | _ => Scalar.max ty - -theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by - cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at * - have h := Isize.refined_min.property - cases h <;> simp [*, Isize.min] - -theorem Scalar.cMax_bound ty : Scalar.cMax ty ≤ Scalar.max ty := by - cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at * - . have h := Isize.refined_max.property - cases h <;> simp [*, Isize.max] - . have h := Usize.refined_max.property - cases h <;> simp [*, Usize.max] - -theorem Scalar.cMin_suffices ty (h : Scalar.cMin ty ≤ x) : Scalar.min ty ≤ x := by - have := Scalar.cMin_bound ty - linarith - -theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty := by - have := Scalar.cMax_bound ty - linarith - -structure Scalar (ty : ScalarTy) where - val : Int - hmin : Scalar.min ty ≤ val - hmax : val ≤ Scalar.max ty -deriving Repr - -theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) : - Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty -> - Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty - := - λ h => by - apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith - -def Scalar.ofIntCore {ty : ScalarTy} (x : Int) - (hmin : Scalar.min ty ≤ x) (hmax : x ≤ Scalar.max ty) : Scalar ty := - { val := x, hmin := hmin, hmax := hmax } - --- Tactic to prove that integers are in bounds --- TODO: use this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam -syntax "intlit" : tactic -macro_rules - | `(tactic| intlit) => `(tactic| apply Scalar.bound_suffices; decide) - -def Scalar.ofInt {ty : ScalarTy} (x : Int) - (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by intlit) : Scalar ty := - -- Remark: we initially wrote: - -- let ⟨ hmin, hmax ⟩ := h - -- Scalar.ofIntCore x hmin hmax - -- We updated to the line below because a similar pattern in `Scalar.tryMk` - -- made reduction block. Both versions seem to work for `Scalar.ofInt`, though. - -- TODO: investigate - Scalar.ofIntCore x h.left h.right - -@[simp] def Scalar.check_bounds (ty : ScalarTy) (x : Int) : Bool := - (Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) ∧ (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty) - -theorem Scalar.check_bounds_prop {ty : ScalarTy} {x : Int} (h: Scalar.check_bounds ty x) : - Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by - simp at * - have ⟨ hmin, hmax ⟩ := h - have hbmin := Scalar.cMin_bound ty - have hbmax := Scalar.cMax_bound ty - cases hmin <;> cases hmax <;> apply And.intro <;> linarith - --- Further thoughts: look at what has been done here: --- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean --- and --- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean --- which both contain a fair amount of reasoning already! -def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) := - if h:Scalar.check_bounds ty x then - -- If we do: - -- ``` - -- let ⟨ hmin, hmax ⟩ := (Scalar.check_bounds_prop h) - -- Scalar.ofIntCore x hmin hmax - -- ``` - -- then normalization blocks (for instance, some proofs which use reflexivity fail). - -- However, the version below doesn't block reduction (TODO: investigate): - return Scalar.ofInt x (Scalar.check_bounds_prop h) - else fail integerOverflow - -def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val) - -def Scalar.div {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := - if y.val != 0 then Scalar.tryMk ty (x.val / y.val) else fail divisionByZero - --- Our custom remainder operation, which satisfies the semantics of Rust --- TODO: is there a better way? -def scalar_rem (x y : Int) : Int := - if 0 ≤ x then |x| % |y| - else - (|x| % |y|) - --- Our custom division operation, which satisfies the semantics of Rust --- TODO: is there a better way? -def scalar_div (x y : Int) : Int := - if 0 ≤ x && 0 ≤ y then |x| / |y| - else if 0 ≤ x && y < 0 then - (|x| / |y|) - else if x < 0 && 0 ≤ y then - (|x| / |y|) - else |x| / |y| - --- Checking that the remainder operation is correct -#assert scalar_rem 1 2 = 1 -#assert scalar_rem (-1) 2 = -1 -#assert scalar_rem 1 (-2) = 1 -#assert scalar_rem (-1) (-2) = -1 -#assert scalar_rem 7 3 = (1:Int) -#assert scalar_rem (-7) 3 = -1 -#assert scalar_rem 7 (-3) = 1 -#assert scalar_rem (-7) (-3) = -1 - --- Checking that the division operation is correct -#assert scalar_div 3 2 = 1 -#assert scalar_div (-3) 2 = -1 -#assert scalar_div 3 (-2) = -1 -#assert scalar_div (-3) (-2) = 1 -#assert scalar_div 7 3 = 2 -#assert scalar_div (-7) 3 = -2 -#assert scalar_div 7 (-3) = -2 -#assert scalar_div (-7) (-3) = 2 - -def Scalar.rem {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := - if y.val != 0 then Scalar.tryMk ty (x.val % y.val) else fail divisionByZero - -def Scalar.add {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := - Scalar.tryMk ty (x.val + y.val) - -def Scalar.sub {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := - Scalar.tryMk ty (x.val - y.val) - -def Scalar.mul {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := - Scalar.tryMk ty (x.val * y.val) - --- TODO: instances of +, -, * etc. for scalars - --- Cast an integer from a [src_ty] to a [tgt_ty] --- TODO: check the semantics of casts in Rust -def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Result (Scalar tgt_ty) := - Scalar.tryMk tgt_ty x.val - --- The scalar types --- We declare the definitions as reducible so that Lean can unfold them (useful --- for type class resolution for instance). -@[reducible] def Isize := Scalar .Isize -@[reducible] def I8 := Scalar .I8 -@[reducible] def I16 := Scalar .I16 -@[reducible] def I32 := Scalar .I32 -@[reducible] def I64 := Scalar .I64 -@[reducible] def I128 := Scalar .I128 -@[reducible] def Usize := Scalar .Usize -@[reducible] def U8 := Scalar .U8 -@[reducible] def U16 := Scalar .U16 -@[reducible] def U32 := Scalar .U32 -@[reducible] def U64 := Scalar .U64 -@[reducible] def U128 := Scalar .U128 - --- TODO: below: not sure this is the best way. --- Should we rather overload operations like +, -, etc.? --- Also, it is possible to automate the generation of those definitions --- with macros (but would it be a good idea? It would be less easy to --- read the file, which is not supposed to change a lot) - --- Negation - -/-- -Remark: there is no heterogeneous negation in the Lean prelude: we thus introduce -one here. - -The notation typeclass for heterogeneous addition. -This enables the notation `- a : β` where `a : α`. --/ -class HNeg (α : Type u) (β : outParam (Type v)) where - /-- `- a` computes the negation of `a`. - The meaning of this notation is type-dependent. -/ - hNeg : α → β - -prefix:75 "-" => HNeg.hNeg - -instance : HNeg Isize (Result Isize) where hNeg x := Scalar.neg x -instance : HNeg I8 (Result I8) where hNeg x := Scalar.neg x -instance : HNeg I16 (Result I16) where hNeg x := Scalar.neg x -instance : HNeg I32 (Result I32) where hNeg x := Scalar.neg x -instance : HNeg I64 (Result I64) where hNeg x := Scalar.neg x -instance : HNeg I128 (Result I128) where hNeg x := Scalar.neg x - --- Addition -instance {ty} : HAdd (Scalar ty) (Scalar ty) (Result (Scalar ty)) where - hAdd x y := Scalar.add x y - --- Substraction -instance {ty} : HSub (Scalar ty) (Scalar ty) (Result (Scalar ty)) where - hSub x y := Scalar.sub x y - --- Multiplication -instance {ty} : HMul (Scalar ty) (Scalar ty) (Result (Scalar ty)) where - hMul x y := Scalar.mul x y - --- Division -instance {ty} : HDiv (Scalar ty) (Scalar ty) (Result (Scalar ty)) where - hDiv x y := Scalar.div x y - --- Remainder -instance {ty} : HMod (Scalar ty) (Scalar ty) (Result (Scalar ty)) where - hMod x y := Scalar.rem x y - --- ofIntCore --- TODO: typeclass? -def Isize.ofIntCore := @Scalar.ofIntCore .Isize -def I8.ofIntCore := @Scalar.ofIntCore .I8 -def I16.ofIntCore := @Scalar.ofIntCore .I16 -def I32.ofIntCore := @Scalar.ofIntCore .I32 -def I64.ofIntCore := @Scalar.ofIntCore .I64 -def I128.ofIntCore := @Scalar.ofIntCore .I128 -def Usize.ofIntCore := @Scalar.ofIntCore .Usize -def U8.ofIntCore := @Scalar.ofIntCore .U8 -def U16.ofIntCore := @Scalar.ofIntCore .U16 -def U32.ofIntCore := @Scalar.ofIntCore .U32 -def U64.ofIntCore := @Scalar.ofIntCore .U64 -def U128.ofIntCore := @Scalar.ofIntCore .U128 - --- ofInt --- TODO: typeclass? -def Isize.ofInt := @Scalar.ofInt .Isize -def I8.ofInt := @Scalar.ofInt .I8 -def I16.ofInt := @Scalar.ofInt .I16 -def I32.ofInt := @Scalar.ofInt .I32 -def I64.ofInt := @Scalar.ofInt .I64 -def I128.ofInt := @Scalar.ofInt .I128 -def Usize.ofInt := @Scalar.ofInt .Usize -def U8.ofInt := @Scalar.ofInt .U8 -def U16.ofInt := @Scalar.ofInt .U16 -def U32.ofInt := @Scalar.ofInt .U32 -def U64.ofInt := @Scalar.ofInt .U64 -def U128.ofInt := @Scalar.ofInt .U128 - --- Comparisons -instance {ty} : LT (Scalar ty) where - lt a b := LT.lt a.val b.val - -instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val - -instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt .. -instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe .. - -theorem Scalar.eq_of_val_eq {ty} : ∀ {i j : Scalar ty}, Eq i.val j.val → Eq i j - | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl - -theorem Scalar.val_eq_of_eq {ty} {i j : Scalar ty} (h : Eq i j) : Eq i.val j.val := - h ▸ rfl - -theorem Scalar.ne_of_val_ne {ty} {i j : Scalar ty} (h : Not (Eq i.val j.val)) : Not (Eq i j) := - fun h' => absurd (val_eq_of_eq h') h - -instance (ty : ScalarTy) : DecidableEq (Scalar ty) := - fun i j => - match decEq i.val j.val with - | isTrue h => isTrue (Scalar.eq_of_val_eq h) - | isFalse h => isFalse (Scalar.ne_of_val_ne h) - -def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val - --- -- We now define a type class that subsumes the various machine integer types, so --- -- as to write a concise definition for scalar_cast, rather than exhaustively --- -- enumerating all of the possible pairs. We remark that Rust has sane semantics --- -- and fails if a cast operation would involve a truncation or modulo. - --- class MachineInteger (t: Type) where --- size: Nat --- val: t -> Fin size --- ofNatCore: (n:Nat) -> LT.lt n size -> t - --- set_option hygiene false in --- run_cmd --- for typeName in [`UInt8, `UInt16, `UInt32, `UInt64, `USize].map Lean.mkIdent do --- Lean.Elab.Command.elabCommand (← `( --- namespace $typeName --- instance: MachineInteger $typeName where --- size := size --- val := val --- ofNatCore := ofNatCore --- end $typeName --- )) - --- -- Aeneas only instantiates the destination type (`src` is implicit). We rely on --- -- Lean to infer `src`. - --- def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): Result dst := --- if h: MachineInteger.val x < MachineInteger.size dst then --- .ret (MachineInteger.ofNatCore (MachineInteger.val x).val h) --- else --- .fail integerOverflow - -------------- --- VECTORS -- -------------- - -def Vec (α : Type u) := { l : List α // List.length l ≤ Usize.max } - --- TODO: do we really need it? It should be with Subtype by default -instance Vec.cast (a : Type): Coe (Vec a) (List a) where coe := λ v => v.val - -def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩ - -def Vec.len (α : Type u) (v : Vec α) : Usize := - let ⟨ v, l ⟩ := v - Usize.ofIntCore (List.length v) (by simp [Scalar.min, Usize.min]) l - --- This shouldn't be used -def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := () - --- This is actually the backward function -def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α) - := - let nlen := List.length v.val + 1 - if h : nlen ≤ U32.max || nlen ≤ Usize.max then - have h : nlen ≤ Usize.max := by - simp [Usize.max] at * - have hm := Usize.refined_max.property - cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith - return ⟨ List.concat v.val x, by simp at *; assumption ⟩ - else - fail maximumSizeExceeded - --- This shouldn't be used -def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit := - if i.val < List.length v.val then - .ret () - else - .fail arrayOutOfBounds - --- This is actually the backward function -def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) := - if i.val < List.length v.val then - -- TODO: maybe we should redefine a list library which uses integers - -- (instead of natural numbers) - let i := i.val.toNat - .ret ⟨ List.set v.val i x, by - have h: List.length v.val ≤ Usize.max := v.property - simp [*] at * - ⟩ - else - .fail arrayOutOfBounds - -def Vec.index_to_fin {α : Type u} {v: Vec α} {i: Usize} (h : i.val < List.length v.val) : - Fin (List.length v.val) := - let j := i.val.toNat - let h: j < List.length v.val := by - have heq := @Int.toNat_lt (List.length v.val) i.val i.hmin - apply heq.mpr - assumption - ⟨j, h⟩ - -def Vec.index (α : Type u) (v: Vec α) (i: Usize): Result α := - if h: i.val < List.length v.val then - let i := Vec.index_to_fin h - .ret (List.get v.val i) - else - .fail arrayOutOfBounds - --- This shouldn't be used -def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit := - if i.val < List.length v.val then - .ret () - else - .fail arrayOutOfBounds - -def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize): Result α := - if h: i.val < List.length v.val then - let i := Vec.index_to_fin h - .ret (List.get v.val i) - else - .fail arrayOutOfBounds - -def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) := - if h: i.val < List.length v.val then - let i := Vec.index_to_fin h - .ret ⟨ List.set v.val i x, by - have h: List.length v.val ≤ Usize.max := v.property - simp [*] at * - ⟩ - else - .fail arrayOutOfBounds - ----------- --- MISC -- ----------- - -@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x -@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y - -/-- Aeneas-translated function -- useful to reduce non-recursive definitions. - Use with `simp [ aeneas ]` -/ -register_simp_attr aeneas - -end Primitives +import Base.Primitives.Base +import Base.Primitives.Scalar +import Base.Primitives.Vec diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean new file mode 100644 index 00000000..db462c38 --- /dev/null +++ b/backends/lean/Base/Primitives/Base.lean @@ -0,0 +1,130 @@ +import Lean + +namespace Primitives + +-------------------- +-- ASSERT COMMAND --Std. +-------------------- + +open Lean Elab Command Term Meta + +syntax (name := assert) "#assert" term: command + +@[command_elab assert] +unsafe +def assertImpl : CommandElab := fun (_stx: Syntax) => do + runTermElabM (fun _ => do + let r ← evalTerm Bool (mkConst ``Bool) _stx[1] + if not r then + logInfo ("Assertion failed for:\n" ++ _stx[1]) + throwError ("Expression reduced to false:\n" ++ _stx[1]) + pure ()) + +#eval 2 == 2 +#assert (2 == 2) + +------------- +-- PRELUDE -- +------------- + +-- Results & monadic combinators + +inductive Error where + | assertionFailure: Error + | integerOverflow: Error + | divisionByZero: Error + | arrayOutOfBounds: Error + | maximumSizeExceeded: Error + | panic: Error +deriving Repr, BEq + +open Error + +inductive Result (α : Type u) where + | ret (v: α): Result α + | fail (e: Error): Result α + | div +deriving Repr, BEq + +open Result + +instance Result_Inhabited (α : Type u) : Inhabited (Result α) := + Inhabited.mk (fail panic) + +instance Result_Nonempty (α : Type u) : Nonempty (Result α) := + Nonempty.intro div + +/- HELPERS -/ + +def ret? {α: Type u} (r: Result α): Bool := + match r with + | ret _ => true + | fail _ | div => false + +def div? {α: Type u} (r: Result α): Bool := + match r with + | div => true + | ret _ | fail _ => false + +def massert (b:Bool) : Result Unit := + if b then ret () else fail assertionFailure + +def eval_global {α: Type u} (x: Result α) (_: ret? x): α := + match x with + | fail _ | div => by contradiction + | ret x => x + +/- DO-DSL SUPPORT -/ + +def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β := + match x with + | ret v => f v + | fail v => fail v + | div => div + +-- Allows using Result in do-blocks +instance : Bind Result where + bind := bind + +-- Allows using return x in do-blocks +instance : Pure Result where + pure := fun x => ret x + +@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind] +@[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind] +@[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind] + +/- CUSTOM-DSL SUPPORT -/ + +-- Let-binding the Result of a monadic operation is oftentimes not sufficient, +-- because we may need a hypothesis for equational reasoning in the scope. We +-- rely on subtype, and a custom let-binding operator, in effect recreating our +-- own variant of the do-dsl + +def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := + match o with + | ret x => ret ⟨x, rfl⟩ + | fail e => fail e + | div => div + +@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) : + (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind] + +@[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) : + (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind] + +@[simp] theorem bind_tc_div (f : α → Result β) : + (do let y ← div; f y) = div := by simp [Bind.bind, bind] + +---------- +-- MISC -- +---------- + +@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x +@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y + +/-- Aeneas-translated function -- useful to reduce non-recursive definitions. + Use with `simp [ aeneas ]` -/ +register_simp_attr aeneas + +end Primitives diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean new file mode 100644 index 00000000..241dfa07 --- /dev/null +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -0,0 +1,507 @@ +import Lean +import Lean.Meta.Tactic.Simp +import Mathlib.Tactic.Linarith +import Base.Primitives.Base + +namespace Primitives + +---------------------- +-- MACHINE INTEGERS -- +---------------------- + +-- We redefine our machine integers types. + +-- For Isize/Usize, we reuse `getNumBits` from `USize`. You cannot reduce `getNumBits` +-- using the simplifier, meaning that proofs do not depend on the compile-time value of +-- USize.size. (Lean assumes 32 or 64-bit platforms, and Rust doesn't really support, at +-- least officially, 16-bit microcontrollers, so this seems like a fine design decision +-- for now.) + +-- Note from Chris Bailey: "If there's more than one salient property of your +-- definition then the subtyping strategy might get messy, and the property part +-- of a subtype is less discoverable by the simplifier or tactics like +-- library_search." So, we will not add refinements on the return values of the +-- operations defined on Primitives, but will rather rely on custom lemmas to +-- invert on possible return values of the primitive operations. + +-- Machine integer constants, done via `ofNatCore`, which requires a proof that +-- the `Nat` fits within the desired integer type. We provide a custom tactic. + +open Result Error +open System.Platform.getNumBits + +-- TODO: is there a way of only importing System.Platform.getNumBits? +-- +@[simp] def size_num_bits : Nat := (System.Platform.getNumBits ()).val + +-- Remark: Lean seems to use < for the comparisons with the upper bounds by convention. + +-- The "structured" bounds +def Isize.smin : Int := - (HPow.hPow 2 (size_num_bits - 1)) +def Isize.smax : Int := (HPow.hPow 2 (size_num_bits - 1)) - 1 +def I8.smin : Int := - (HPow.hPow 2 7) +def I8.smax : Int := HPow.hPow 2 7 - 1 +def I16.smin : Int := - (HPow.hPow 2 15) +def I16.smax : Int := HPow.hPow 2 15 - 1 +def I32.smin : Int := -(HPow.hPow 2 31) +def I32.smax : Int := HPow.hPow 2 31 - 1 +def I64.smin : Int := -(HPow.hPow 2 63) +def I64.smax : Int := HPow.hPow 2 63 - 1 +def I128.smin : Int := -(HPow.hPow 2 127) +def I128.smax : Int := HPow.hPow 2 127 - 1 +def Usize.smin : Int := 0 +def Usize.smax : Int := HPow.hPow 2 size_num_bits - 1 +def U8.smin : Int := 0 +def U8.smax : Int := HPow.hPow 2 8 - 1 +def U16.smin : Int := 0 +def U16.smax : Int := HPow.hPow 2 16 - 1 +def U32.smin : Int := 0 +def U32.smax : Int := HPow.hPow 2 32 - 1 +def U64.smin : Int := 0 +def U64.smax : Int := HPow.hPow 2 64 - 1 +def U128.smin : Int := 0 +def U128.smax : Int := HPow.hPow 2 128 - 1 + +-- The "normalized" bounds, that we use in practice +def I8.min := -128 +def I8.max := 127 +def I16.min := -32768 +def I16.max := 32767 +def I32.min := -2147483648 +def I32.max := 2147483647 +def I64.min := -9223372036854775808 +def I64.max := 9223372036854775807 +def I128.min := -170141183460469231731687303715884105728 +def I128.max := 170141183460469231731687303715884105727 +@[simp] def U8.min := 0 +def U8.max := 255 +@[simp] def U16.min := 0 +def U16.max := 65535 +@[simp] def U32.min := 0 +def U32.max := 4294967295 +@[simp] def U64.min := 0 +def U64.max := 18446744073709551615 +@[simp] def U128.min := 0 +def U128.max := 340282366920938463463374607431768211455 +@[simp] def Usize.min := 0 + +def Isize.refined_min : { n:Int // n = I32.min ∨ n = I64.min } := + ⟨ Isize.smin, by + simp [Isize.smin] + cases System.Platform.numBits_eq <;> + unfold System.Platform.numBits at * <;> simp [*] ⟩ + +def Isize.refined_max : { n:Int // n = I32.max ∨ n = I64.max } := + ⟨ Isize.smax, by + simp [Isize.smax] + cases System.Platform.numBits_eq <;> + unfold System.Platform.numBits at * <;> simp [*] ⟩ + +def Usize.refined_max : { n:Int // n = U32.max ∨ n = U64.max } := + ⟨ Usize.smax, by + simp [Usize.smax] + cases System.Platform.numBits_eq <;> + unfold System.Platform.numBits at * <;> simp [*] ⟩ + +def Isize.min := Isize.refined_min.val +def Isize.max := Isize.refined_max.val +def Usize.max := Usize.refined_max.val + +inductive ScalarTy := +| Isize +| I8 +| I16 +| I32 +| I64 +| I128 +| Usize +| U8 +| U16 +| U32 +| U64 +| U128 + +def Scalar.smin (ty : ScalarTy) : Int := + match ty with + | .Isize => Isize.smin + | .I8 => I8.smin + | .I16 => I16.smin + | .I32 => I32.smin + | .I64 => I64.smin + | .I128 => I128.smin + | .Usize => Usize.smin + | .U8 => U8.smin + | .U16 => U16.smin + | .U32 => U32.smin + | .U64 => U64.smin + | .U128 => U128.smin + +def Scalar.smax (ty : ScalarTy) : Int := + match ty with + | .Isize => Isize.smax + | .I8 => I8.smax + | .I16 => I16.smax + | .I32 => I32.smax + | .I64 => I64.smax + | .I128 => I128.smax + | .Usize => Usize.smax + | .U8 => U8.smax + | .U16 => U16.smax + | .U32 => U32.smax + | .U64 => U64.smax + | .U128 => U128.smax + +def Scalar.min (ty : ScalarTy) : Int := + match ty with + | .Isize => Isize.min + | .I8 => I8.min + | .I16 => I16.min + | .I32 => I32.min + | .I64 => I64.min + | .I128 => I128.min + | .Usize => Usize.min + | .U8 => U8.min + | .U16 => U16.min + | .U32 => U32.min + | .U64 => U64.min + | .U128 => U128.min + +def Scalar.max (ty : ScalarTy) : Int := + match ty with + | .Isize => Isize.max + | .I8 => I8.max + | .I16 => I16.max + | .I32 => I32.max + | .I64 => I64.max + | .I128 => I128.max + | .Usize => Usize.max + | .U8 => U8.max + | .U16 => U16.max + | .U32 => U32.max + | .U64 => U64.max + | .U128 => U128.max + +def Scalar.smin_eq (ty : ScalarTy) : Scalar.min ty = Scalar.smin ty := by + cases ty <;> rfl + +def Scalar.smax_eq (ty : ScalarTy) : Scalar.max ty = Scalar.smax ty := by + cases ty <;> rfl + +-- "Conservative" bounds +-- We use those because we can't compare to the isize bounds (which can't +-- reduce at compile-time). Whenever we perform an arithmetic operation like +-- addition we need to check that the result is in bounds: we first compare +-- to the conservative bounds, which reduce, then compare to the real bounds. +-- This is useful for the various #asserts that we want to reduce at +-- type-checking time. +def Scalar.cMin (ty : ScalarTy) : Int := + match ty with + | .Isize => Scalar.min .I32 + | _ => Scalar.min ty + +def Scalar.cMax (ty : ScalarTy) : Int := + match ty with + | .Isize => Scalar.max .I32 + | .Usize => Scalar.max .U32 + | _ => Scalar.max ty + +theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by + cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at * + have h := Isize.refined_min.property + cases h <;> simp [*, Isize.min] + +theorem Scalar.cMax_bound ty : Scalar.cMax ty ≤ Scalar.max ty := by + cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at * + . have h := Isize.refined_max.property + cases h <;> simp [*, Isize.max] + . have h := Usize.refined_max.property + cases h <;> simp [*, Usize.max] + +theorem Scalar.cMin_suffices ty (h : Scalar.cMin ty ≤ x) : Scalar.min ty ≤ x := by + have := Scalar.cMin_bound ty + linarith + +theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty := by + have := Scalar.cMax_bound ty + linarith + +structure Scalar (ty : ScalarTy) where + val : Int + hmin : Scalar.min ty ≤ val + hmax : val ≤ Scalar.max ty +deriving Repr + +theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) : + Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty -> + Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty + := + λ h => by + apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith + +def Scalar.ofIntCore {ty : ScalarTy} (x : Int) + (hmin : Scalar.min ty ≤ x) (hmax : x ≤ Scalar.max ty) : Scalar ty := + { val := x, hmin := hmin, hmax := hmax } + +-- Tactic to prove that integers are in bounds +-- TODO: use this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam +syntax "intlit" : tactic +macro_rules + | `(tactic| intlit) => `(tactic| apply Scalar.bound_suffices; decide) + +def Scalar.ofInt {ty : ScalarTy} (x : Int) + (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by intlit) : Scalar ty := + -- Remark: we initially wrote: + -- let ⟨ hmin, hmax ⟩ := h + -- Scalar.ofIntCore x hmin hmax + -- We updated to the line below because a similar pattern in `Scalar.tryMk` + -- made reduction block. Both versions seem to work for `Scalar.ofInt`, though. + -- TODO: investigate + Scalar.ofIntCore x h.left h.right + +@[simp] def Scalar.check_bounds (ty : ScalarTy) (x : Int) : Bool := + (Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) ∧ (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty) + +theorem Scalar.check_bounds_prop {ty : ScalarTy} {x : Int} (h: Scalar.check_bounds ty x) : + Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by + simp at * + have ⟨ hmin, hmax ⟩ := h + have hbmin := Scalar.cMin_bound ty + have hbmax := Scalar.cMax_bound ty + cases hmin <;> cases hmax <;> apply And.intro <;> linarith + +-- Further thoughts: look at what has been done here: +-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean +-- and +-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean +-- which both contain a fair amount of reasoning already! +def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) := + if h:Scalar.check_bounds ty x then + -- If we do: + -- ``` + -- let ⟨ hmin, hmax ⟩ := (Scalar.check_bounds_prop h) + -- Scalar.ofIntCore x hmin hmax + -- ``` + -- then normalization blocks (for instance, some proofs which use reflexivity fail). + -- However, the version below doesn't block reduction (TODO: investigate): + return Scalar.ofInt x (Scalar.check_bounds_prop h) + else fail integerOverflow + +def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val) + +def Scalar.div {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := + if y.val != 0 then Scalar.tryMk ty (x.val / y.val) else fail divisionByZero + +-- Our custom remainder operation, which satisfies the semantics of Rust +-- TODO: is there a better way? +def scalar_rem (x y : Int) : Int := + if 0 ≤ x then |x| % |y| + else - (|x| % |y|) + +-- Our custom division operation, which satisfies the semantics of Rust +-- TODO: is there a better way? +def scalar_div (x y : Int) : Int := + if 0 ≤ x && 0 ≤ y then |x| / |y| + else if 0 ≤ x && y < 0 then - (|x| / |y|) + else if x < 0 && 0 ≤ y then - (|x| / |y|) + else |x| / |y| + +-- Checking that the remainder operation is correct +#assert scalar_rem 1 2 = 1 +#assert scalar_rem (-1) 2 = -1 +#assert scalar_rem 1 (-2) = 1 +#assert scalar_rem (-1) (-2) = -1 +#assert scalar_rem 7 3 = (1:Int) +#assert scalar_rem (-7) 3 = -1 +#assert scalar_rem 7 (-3) = 1 +#assert scalar_rem (-7) (-3) = -1 + +-- Checking that the division operation is correct +#assert scalar_div 3 2 = 1 +#assert scalar_div (-3) 2 = -1 +#assert scalar_div 3 (-2) = -1 +#assert scalar_div (-3) (-2) = 1 +#assert scalar_div 7 3 = 2 +#assert scalar_div (-7) 3 = -2 +#assert scalar_div 7 (-3) = -2 +#assert scalar_div (-7) (-3) = 2 + +def Scalar.rem {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := + if y.val != 0 then Scalar.tryMk ty (x.val % y.val) else fail divisionByZero + +def Scalar.add {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := + Scalar.tryMk ty (x.val + y.val) + +def Scalar.sub {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := + Scalar.tryMk ty (x.val - y.val) + +def Scalar.mul {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) := + Scalar.tryMk ty (x.val * y.val) + +-- TODO: instances of +, -, * etc. for scalars + +-- Cast an integer from a [src_ty] to a [tgt_ty] +-- TODO: check the semantics of casts in Rust +def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Result (Scalar tgt_ty) := + Scalar.tryMk tgt_ty x.val + +-- The scalar types +-- We declare the definitions as reducible so that Lean can unfold them (useful +-- for type class resolution for instance). +@[reducible] def Isize := Scalar .Isize +@[reducible] def I8 := Scalar .I8 +@[reducible] def I16 := Scalar .I16 +@[reducible] def I32 := Scalar .I32 +@[reducible] def I64 := Scalar .I64 +@[reducible] def I128 := Scalar .I128 +@[reducible] def Usize := Scalar .Usize +@[reducible] def U8 := Scalar .U8 +@[reducible] def U16 := Scalar .U16 +@[reducible] def U32 := Scalar .U32 +@[reducible] def U64 := Scalar .U64 +@[reducible] def U128 := Scalar .U128 + +-- TODO: below: not sure this is the best way. +-- Should we rather overload operations like +, -, etc.? +-- Also, it is possible to automate the generation of those definitions +-- with macros (but would it be a good idea? It would be less easy to +-- read the file, which is not supposed to change a lot) + +-- Negation + +/-- +Remark: there is no heterogeneous negation in the Lean prelude: we thus introduce +one here. + +The notation typeclass for heterogeneous addition. +This enables the notation `- a : β` where `a : α`. +-/ +class HNeg (α : Type u) (β : outParam (Type v)) where + /-- `- a` computes the negation of `a`. + The meaning of this notation is type-dependent. -/ + hNeg : α → β + +prefix:75 "-" => HNeg.hNeg + +instance : HNeg Isize (Result Isize) where hNeg x := Scalar.neg x +instance : HNeg I8 (Result I8) where hNeg x := Scalar.neg x +instance : HNeg I16 (Result I16) where hNeg x := Scalar.neg x +instance : HNeg I32 (Result I32) where hNeg x := Scalar.neg x +instance : HNeg I64 (Result I64) where hNeg x := Scalar.neg x +instance : HNeg I128 (Result I128) where hNeg x := Scalar.neg x + +-- Addition +instance {ty} : HAdd (Scalar ty) (Scalar ty) (Result (Scalar ty)) where + hAdd x y := Scalar.add x y + +-- Substraction +instance {ty} : HSub (Scalar ty) (Scalar ty) (Result (Scalar ty)) where + hSub x y := Scalar.sub x y + +-- Multiplication +instance {ty} : HMul (Scalar ty) (Scalar ty) (Result (Scalar ty)) where + hMul x y := Scalar.mul x y + +-- Division +instance {ty} : HDiv (Scalar ty) (Scalar ty) (Result (Scalar ty)) where + hDiv x y := Scalar.div x y + +-- Remainder +instance {ty} : HMod (Scalar ty) (Scalar ty) (Result (Scalar ty)) where + hMod x y := Scalar.rem x y + +-- ofIntCore +-- TODO: typeclass? +def Isize.ofIntCore := @Scalar.ofIntCore .Isize +def I8.ofIntCore := @Scalar.ofIntCore .I8 +def I16.ofIntCore := @Scalar.ofIntCore .I16 +def I32.ofIntCore := @Scalar.ofIntCore .I32 +def I64.ofIntCore := @Scalar.ofIntCore .I64 +def I128.ofIntCore := @Scalar.ofIntCore .I128 +def Usize.ofIntCore := @Scalar.ofIntCore .Usize +def U8.ofIntCore := @Scalar.ofIntCore .U8 +def U16.ofIntCore := @Scalar.ofIntCore .U16 +def U32.ofIntCore := @Scalar.ofIntCore .U32 +def U64.ofIntCore := @Scalar.ofIntCore .U64 +def U128.ofIntCore := @Scalar.ofIntCore .U128 + +-- ofInt +-- TODO: typeclass? +def Isize.ofInt := @Scalar.ofInt .Isize +def I8.ofInt := @Scalar.ofInt .I8 +def I16.ofInt := @Scalar.ofInt .I16 +def I32.ofInt := @Scalar.ofInt .I32 +def I64.ofInt := @Scalar.ofInt .I64 +def I128.ofInt := @Scalar.ofInt .I128 +def Usize.ofInt := @Scalar.ofInt .Usize +def U8.ofInt := @Scalar.ofInt .U8 +def U16.ofInt := @Scalar.ofInt .U16 +def U32.ofInt := @Scalar.ofInt .U32 +def U64.ofInt := @Scalar.ofInt .U64 +def U128.ofInt := @Scalar.ofInt .U128 + +-- Comparisons +instance {ty} : LT (Scalar ty) where + lt a b := LT.lt a.val b.val + +instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val + +instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt .. +instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe .. + +theorem Scalar.eq_of_val_eq {ty} : ∀ {i j : Scalar ty}, Eq i.val j.val → Eq i j + | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl + +theorem Scalar.val_eq_of_eq {ty} {i j : Scalar ty} (h : Eq i j) : Eq i.val j.val := + h ▸ rfl + +theorem Scalar.ne_of_val_ne {ty} {i j : Scalar ty} (h : Not (Eq i.val j.val)) : Not (Eq i j) := + fun h' => absurd (val_eq_of_eq h') h + +instance (ty : ScalarTy) : DecidableEq (Scalar ty) := + fun i j => + match decEq i.val j.val with + | isTrue h => isTrue (Scalar.eq_of_val_eq h) + | isFalse h => isFalse (Scalar.ne_of_val_ne h) + +/- Remark: we can't write the following instance because of restrictions about + the type class parameters (`ty` doesn't appear in the return type, which is + forbidden): + + ``` + instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val + ``` + -/ +def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val + +-- -- We now define a type class that subsumes the various machine integer types, so +-- -- as to write a concise definition for scalar_cast, rather than exhaustively +-- -- enumerating all of the possible pairs. We remark that Rust has sane semantics +-- -- and fails if a cast operation would involve a truncation or modulo. + +-- class MachineInteger (t: Type) where +-- size: Nat +-- val: t -> Fin size +-- ofNatCore: (n:Nat) -> LT.lt n size -> t + +-- set_option hygiene false in +-- run_cmd +-- for typeName in [`UInt8, `UInt16, `UInt32, `UInt64, `USize].map Lean.mkIdent do +-- Lean.Elab.Command.elabCommand (← `( +-- namespace $typeName +-- instance: MachineInteger $typeName where +-- size := size +-- val := val +-- ofNatCore := ofNatCore +-- end $typeName +-- )) + +-- -- Aeneas only instantiates the destination type (`src` is implicit). We rely on +-- -- Lean to infer `src`. + +-- def scalar_cast { src: Type } (dst: Type) [ MachineInteger src ] [ MachineInteger dst ] (x: src): Result dst := +-- if h: MachineInteger.val x < MachineInteger.size dst then +-- .ret (MachineInteger.ofNatCore (MachineInteger.val x).val h) +-- else +-- .fail integerOverflow + +end Primitives diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean new file mode 100644 index 00000000..7851a232 --- /dev/null +++ b/backends/lean/Base/Primitives/Vec.lean @@ -0,0 +1,113 @@ +import Lean +import Lean.Meta.Tactic.Simp +import Init.Data.List.Basic +import Mathlib.Tactic.RunCmd +import Mathlib.Tactic.Linarith +import Base.IList +import Base.Primitives.Scalar +import Base.Arith + +namespace Primitives + +open Result Error + +------------- +-- VECTORS -- +------------- + +def Vec (α : Type u) := { l : List α // List.length l ≤ Usize.max } + +-- TODO: do we really need it? It should be with Subtype by default +instance Vec.cast (a : Type): Coe (Vec a) (List a) where coe := λ v => v.val + +instance (a : Type) : Arith.HasIntProp (Vec a) where + prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize + prop := λ ⟨ _, l ⟩ => l + +example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by + intro_has_int_prop_instances + simp_all [Scalar.max, Scalar.min] + +example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by + scalar_tac + +def Vec.new (α : Type u): Vec α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩ + +def Vec.len (α : Type u) (v : Vec α) : Usize := + let ⟨ v, l ⟩ := v + Usize.ofIntCore (List.length v) (by simp [Scalar.min, Usize.min]) l + +def Vec.length {α : Type u} (v : Vec α) : Int := v.val.len + +-- This shouldn't be used +def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := () + +-- This is actually the backward function +def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α) + := + let nlen := List.length v.val + 1 + if h : nlen ≤ U32.max || nlen ≤ Usize.max then + have h : nlen ≤ Usize.max := by + simp [Usize.max] at * + have hm := Usize.refined_max.property + cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith + return ⟨ List.concat v.val x, by simp at *; assumption ⟩ + else + fail maximumSizeExceeded + +-- This shouldn't be used +def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit := + if i.val < List.length v.val then + .ret () + else + .fail arrayOutOfBounds + +-- This is actually the backward function +def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) := + if i.val < List.length v.val then + -- TODO: maybe we should redefine a list library which uses integers + -- (instead of natural numbers) + .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ + else + .fail arrayOutOfBounds + +-- TODO: remove +def Vec.index_to_fin {α : Type u} {v: Vec α} {i: Usize} (h : i.val < List.length v.val) : + Fin (List.length v.val) := + let j := i.val.toNat + let h: j < List.length v.val := by + have heq := @Int.toNat_lt (List.length v.val) i.val i.hmin + apply heq.mpr + assumption + ⟨j, h⟩ + +def Vec.index (α : Type u) (v: Vec α) (i: Usize): Result α := + match v.val.indexOpt i.val with + | none => fail .arrayOutOfBounds + | some x => ret x + +-- This shouldn't be used +def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit := + if i.val < List.length v.val then + .ret () + else + .fail arrayOutOfBounds + +def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize): Result α := + if h: i.val < List.length v.val then + let i := Vec.index_to_fin h + .ret (List.get v.val i) + else + .fail arrayOutOfBounds + +def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) := + if h: i.val < List.length v.val then + let i := Vec.index_to_fin h + .ret ⟨ List.set v.val i x, by + have h: List.length v.val ≤ Usize.max := v.property + simp [*] at * + ⟩ + else + .fail arrayOutOfBounds + +end Primitives diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 35a3c25a..af7b426a 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -7,6 +7,7 @@ namespace Progress open Lean Elab Term Meta Tactic open Utils +-- TODO: remove namespace Test open Primitives @@ -199,6 +200,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do elab "progress" args:progressArgs : tactic => evalProgress args +-- TODO: remove namespace Test open Primitives -- cgit v1.3.1