summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith
diff options
context:
space:
mode:
authorSon HO2024-06-21 23:24:01 +0200
committerGitHub2024-06-21 23:24:01 +0200
commit4d30546c809cb2c512e0c3fd8ee540fff1330eab (patch)
treed83926c9aa30f7bfb2a1c6db0e776003bca63355 /backends/lean/Base/Arith
parentf264b9dcc6331eb9149d951f308cdc61c8c02801 (diff)
Add some proofs for the Lean backend (#255)
* Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local> Co-authored-by: Son Ho <sonho@Sons-MBP.lan>
Diffstat (limited to 'backends/lean/Base/Arith')
-rw-r--r--backends/lean/Base/Arith/Base.lean8
-rw-r--r--backends/lean/Base/Arith/Int.lean48
-rw-r--r--backends/lean/Base/Arith/Scalar.lean12
3 files changed, 54 insertions, 14 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index fb6b12e5..320b4b53 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -52,10 +52,6 @@ theorem int_pos_ind (p : Int → Prop) :
rename_i m
cases m <;> simp_all
--- We sometimes need this to make sure no natural numbers appear in the goals
--- TODO: there is probably something more general to do
-theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp
-
-- This is mostly used in termination proofs
theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) :
↑(x.toNat) < y := by
@@ -68,4 +64,8 @@ theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ)
have : 0 ≤ x := by omega
simp [Int.toNat_sub_of_le, *]
+-- WARNING: do not use this with `simp` as it might loop. The left-hand side indeed reduces to the
+-- righ-hand side, meaning the rewriting can be applied to `n` itself.
+theorem ofNat_instOfNatNat_eq (n : Nat) : @OfNat.ofNat Nat n (instOfNatNat n) = n := by rfl
+
end Arith
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 068d6f2f..b1927cfd 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -3,6 +3,7 @@
import Lean
import Lean.Meta.Tactic.Simp
import Init.Data.List.Basic
+import Mathlib.Tactic.Ring.RingNF
import Base.Utils
import Base.Arith.Base
@@ -111,7 +112,7 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
let hs := HashSet.empty
-- Explore the declarations
let decls ← ctx.getDecls
- let hs ← decls.foldlM (fun hs d => do
+ let hs ← decls.foldlM (fun hs d => do
-- Collect instances over all subexpressions in the context.
-- Note that we explore the *type* of the local declarations: if we have
-- for instance `h : A ∧ B` in the context, the expression itself is simply
@@ -154,7 +155,7 @@ def lookupHasIntPred (e : Expr) : MetaM (Option Expr) :=
lookupProp "lookupHasIntPred" ``HasIntPred e (fun term => pure #[term]) (fun _ => pure #[])
-- Collect the instances of `HasIntPred` for the subexpressions in the context
-def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
collectInstancesFromMainCtx lookupHasIntPred
-- Return an instance of `PropHasImp` for `e` if it has some
@@ -201,7 +202,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
-- 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 true {} #[] [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
+ Utils.simpAt true {} [] [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
-- Return the new value
pure nval
@@ -214,7 +215,7 @@ def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do
elab "intro_has_int_prop_instances" : tactic => do
let _ ← introHasIntPropInstances
-def introHasIntPredInstances : Tactic.TacticM (Array Expr) := do
+def introHasIntPredInstances : Tactic.TacticM (Array Expr) := do
trace[Arith] "Introducing the HasIntPred instances"
introInstances ``HasIntPred.concl lookupHasIntPred
@@ -230,6 +231,8 @@ def introPropHasImpInstances : Tactic.TacticM (Array Expr) := do
elab "intro_prop_has_imp_instances" : tactic => do
let _ ← introPropHasImpInstances
+def intTacSimpRocs : List Name := [``Int.reduceNegSucc, ``Int.reduceNeg]
+
/- Boosting a bit the `omega` tac.
-/
def intTacPreprocess (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
@@ -244,7 +247,33 @@ def intTacPreprocess (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM U
extraPreprocess
-- Reduce all the terms in the goal - note that the extra preprocessing step
-- might have proven the goal, hence the `Tactic.allGoals`
- Tactic.allGoals do tryTac (dsimpAt false {} #[] [] [] [] Tactic.Location.wildcard)
+ let dsimp :=
+ Tactic.allGoals do tryTac (
+ -- We set `simpOnly` at false on purpose
+ dsimpAt false {} intTacSimpRocs
+ -- Declarations to unfold
+ []
+ -- Theorems
+ []
+ [] Tactic.Location.wildcard)
+ dsimp
+ -- More preprocessing: apply norm_cast to the whole context
+ Tactic.allGoals (Utils.tryTac (Utils.normCastAtAll))
+ -- norm_cast does weird things with negative numbers so we reapply simp
+ dsimp
+ -- We also need this, in case the goal is: ¬ False
+ Tactic.allGoals do tryTac (
+ Utils.simpAt true {}
+ -- Simprocs
+ intTacSimpRocs
+ -- Unfoldings
+ []
+ -- Simp lemmas
+ [``not_false_eq_true]
+ -- Hypotheses
+ []
+ (.targets #[] true)
+ )
elab "int_tac_preprocess" : tactic =>
intTacPreprocess (do pure ())
@@ -260,8 +289,6 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess : Tactic
-- 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)
- -- More preprocessing
- Tactic.allGoals (Utils.tryTac (Utils.simpAt true {} #[] [] [``nat_zero_eq_int_zero] [] .wildcard))
-- Split the conjunctions in the goal
if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
-- Call omega
@@ -298,4 +325,11 @@ example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) :
example (a : Prop) (x : Int) (h0: 0 < x) (h1: x < 0) : a := by
int_tac
+-- Intermediate cast through natural numbers
+example (a : Prop) (x : Int) (h0: (0 : Nat) < x) (h1: x < 0) : a := by
+ int_tac
+
+example (x : Int) (h : x ≤ -3) : x ≤ -2 := by
+ int_tac
+
end Arith
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index ecc5acaf..31110b95 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -19,7 +19,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
-- Reveal the concrete bounds, simplify calls to [ofInt]
Utils.simpAt true {}
-- Simprocs
- #[]
+ intTacSimpRocs
-- Unfoldings
[``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
@@ -59,11 +59,11 @@ 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
+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
+example (x _y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
scalar_tac
-- Checking that we explore the goal *and* projectors correctly
@@ -92,4 +92,10 @@ example (x : U32) (h0 : ¬ x = U32.ofInt 0) : 0 < x.val := by
example {u: U64} (h1: (u : Int) < 2): (u : Int) = 0 ∨ (u : Int) = 1 := by
scalar_tac
+example (x : I32) : -100000000000 < x.val := by
+ scalar_tac
+
+example : (Usize.ofInt 2).val ≠ 0 := by
+ scalar_tac
+
end Arith