From 4d30546c809cb2c512e0c3fd8ee540fff1330eab Mon Sep 17 00:00:00 2001 From: Son HO Date: Fri, 21 Jun 2024 23:24:01 +0200 Subject: 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 Co-authored-by: Son Ho --- backends/lean/Base/Arith/Base.lean | 8 +++--- backends/lean/Base/Arith/Int.lean | 48 ++++++++++++++++++++++++++++++------ backends/lean/Base/Arith/Scalar.lean | 12 ++++++--- 3 files changed, 54 insertions(+), 14 deletions(-) (limited to 'backends/lean/Base/Arith') 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 -- cgit v1.2.3