From fa20b358dd6f383d35c91f66301cfe8c44763922 Mon Sep 17 00:00:00 2001 From: Son HO Date: Tue, 27 Aug 2024 11:02:08 +0200 Subject: [PATCH] Update the Lean library to 4.11.0-rc2 (#316) * Make minor updates * Start updating Lean to v4.11.0-rc2 * Fix Diverge/Elab.lean * Make minor modifications * Update the Lean tests and fix the proofs * Add a model for clone::clone::Clone::clone_from to the Lean library * Revert some modifications * Revert more modifications --- backends/lean/Base/Diverge/Elab.lean | 111 +++- backends/lean/Base/Primitives/Core.lean | 7 + backends/lean/Base/Utils.lean | 2 +- backends/lean/lake-manifest.json | 18 +- backends/lean/lean-toolchain | 2 +- compiler/ExtractBuiltin.ml | 1 + tests/lean/Avl/Properties.lean | 1 - .../lean/External/FunsExternal_Template.lean | 7 - tests/lean/Tutorial/Exercises.lean | 18 +- tests/lean/Tutorial/Solutions.lean | 481 +----------------- tests/lean/Tutorial/Tutorial.lean | 7 - tests/lean/lake-manifest.json | 18 +- tests/lean/lean-toolchain | 2 +- 13 files changed, 139 insertions(+), 536 deletions(-) diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean index 86de54b58..efd6c8e11 100644 --- a/backends/lean/Base/Diverge/Elab.lean +++ b/backends/lean/Base/Diverge/Elab.lean @@ -10,9 +10,6 @@ namespace Diverge /- Automating the generation of the encoding and the proofs so as to use nice syntactic sugar. -/ -syntax (name := divergentDef) - declModifiers "divergent" "def" declId ppIndent(optDeclSig) declVal : command - open Lean Elab Term Meta Primitives Lean.Meta open Utils @@ -1389,17 +1386,43 @@ def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLC else return () catch _ => s.restore --- The following two functions are copy-pasted from Lean.Elab.MutualDef - +-- The following three functions are copy-pasted from Lean.Elab.MutualDef.lean open private elabHeaders levelMVarToParamHeaders getAllUserLevelNames withFunLocalDecls elabFunValues instantiateMVarsAtHeader instantiateMVarsAtLetRecToLift checkLetRecsToLiftTypes withUsed from Lean.Elab.MutualDef +-- Copy/pasted from Lean.Elab.Term.withHeaderSecVars (because the definition is private) +private def Term.withHeaderSecVars {α} (vars : Array Expr) (includedVars : List Name) (headers : Array DefViewElabHeader) + (k : Array Expr → TermElabM α) : TermElabM α := do + let (_, used) ← collectUsed.run {} + let (lctx, localInsts, vars) ← removeUnused vars used + withLCtx lctx localInsts <| k vars +where + collectUsed : StateRefT CollectFVars.State MetaM Unit := do + -- directly referenced in headers + headers.forM (·.type.collectFVars) + -- included by `include` + vars.forM fun var => do + let ldecl ← getFVarLocalDecl var + if includedVars.contains ldecl.userName then + modify (·.add ldecl.fvarId) + -- transitively referenced + get >>= (·.addDependencies) >>= set + -- instances (`addDependencies` unnecessary as by definition they may only reference variables + -- already included) + vars.forM fun var => do + let ldecl ← getFVarLocalDecl var + let st ← get + if ldecl.binderInfo.isInstImplicit && (← getFVars ldecl.type).all st.fvarSet.contains then + modify (·.add ldecl.fvarId) + getFVars (e : Expr) : MetaM (Array FVarId) := + (·.2.fvarIds) <$> e.collectFVars.run {} + -- Comes from Term.isExample def isExample (views : Array DefView) : Bool := views.any (·.kind.isExample) open Language in -def Term.elabMutualDef (vars : Array Expr) (views : Array DefView) : TermElabM Unit := +def Term.elabMutualDef (vars : Array Expr) (includedVars : List Name) (views : Array DefView) : TermElabM Unit := if isExample views then withoutModifyingEnv do -- save correct environment in info tree @@ -1418,7 +1441,7 @@ where withFunLocalDecls headers fun funFVars => do for view in views, funFVar in funFVars do addLocalVarInfo view.declId funFVar - -- Modification 1: + -- MODIFICATION 1: -- Add fake use site to prevent "unused variable" warning (if the -- function is actually not recursive, Lean would print this warning). -- Remark: we could detect this case and encode the function without @@ -1428,7 +1451,7 @@ where addTermInfo' view.declId funFVar let values ← try - let values ← elabFunValues headers + let values ← elabFunValues headers vars includedVars Term.synthesizeSyntheticMVarsNoPostponing values.mapM (instantiateMVars ·) catch ex => @@ -1438,18 +1461,23 @@ where let letRecsToLift ← getLetRecsToLift let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift checkLetRecsToLiftTypes funFVars letRecsToLift - withUsed vars headers values letRecsToLift fun vars => do + (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars includedVars headers else withUsed vars headers values letRecsToLift) fun vars => do let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift for preDef in preDefs do trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}" let preDefs ← withLevelNames allUserLevelNames <| levelMVarToParamPreDecls preDefs let preDefs ← instantiateMVarsAtPreDecls preDefs + let preDefs ← shareCommonPreDefs preDefs let preDefs ← fixLevelParams preDefs scopeLevelNames allUserLevelNames for preDef in preDefs do trace[Elab.definition] "after eraseAuxDiscr, {preDef.declName} : {preDef.type} :=\n{preDef.value}" checkForHiddenUnivLevels allUserLevelNames preDefs - addPreDefinitions preDefs -- Modification 2: we use our custom function here + addPreDefinitions preDefs -- MODIFICATION 2: we use our custom function here processDeriving headers + for view in views, header in headers do + -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting + -- that depends only on a part of the ref + addDeclarationRanges header.declName view.ref processDeriving (headers : Array DefViewElabHeader) := do for header in headers, view in views do @@ -1460,22 +1488,61 @@ where unless (← processDefDeriving className header.declName) do throwError "failed to synthesize instance '{className}' for '{header.declName}'" +#check Command.elabMutualDef + +-- Copy/pasted from Lean.Elab.MutualDef open Command in +open Language in def Command.elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do - let views ← ds.mapM fun d => do - let `($mods:declModifiers divergent def $id:declId $sig:optDeclSig $val:declVal) := d - | throwUnsupportedSyntax - let modifiers ← elabModifiers mods - let (binders, type) := expandOptDeclSig sig - let deriving? := none - let headerRef := Syntax.missing -- Not sure what to put here - pure { ref := d, kind := DefKind.def, headerRef, modifiers, - declId := id, binders, type? := type, value := val, deriving? } - runTermElabM fun vars => Term.elabMutualDef vars views + let opts ← getOptions + withAlwaysResolvedPromises ds.size fun headerPromises => do + let snap? := (← read).snap? + let mut views := #[] + let mut defs := #[] + let mut reusedAllHeaders := true + for h : i in [0:ds.size], headerPromise in headerPromises do + let d := ds[i] + let modifiers ← elabModifiers d[0] + if ds.size > 1 && modifiers.isNonrec then + throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block" + let mut view ← mkDefView modifiers d[2] -- MODIFICATION: changed the index to 2 + let fullHeaderRef := mkNullNode #[d[0], view.headerRef] + if let some snap := snap? then + view := { view with headerSnap? := some { + old? := do + -- transitioning from `Context.snap?` to `DefView.headerSnap?` invariant: if the + -- elaboration context and state are unchanged, and the syntax of this as well as all + -- previous headers is unchanged, then the elaboration result for this header (which + -- includes state from elaboration of previous headers!) should be unchanged. + guard reusedAllHeaders + let old ← snap.old? + -- blocking wait, `HeadersParsedSnapshot` (and hopefully others) should be quick + let old ← old.val.get.toTyped? DefsParsedSnapshot + let oldParsed ← old.defs[i]? + guard <| fullHeaderRef.eqWithInfoAndTraceReuse opts oldParsed.fullHeaderRef + -- no syntax guard to store, we already did the necessary checks + return ⟨.missing, oldParsed.headerProcessedSnap⟩ + new := headerPromise + } } + defs := defs.push { + fullHeaderRef + headerProcessedSnap := { range? := d.getRange?, task := headerPromise.result } + } + reusedAllHeaders := reusedAllHeaders && view.headerSnap?.any (·.old?.isSome) + views := views.push view + if let some snap := snap? then + -- no non-fatal diagnostics at this point + snap.new.resolve <| .ofTyped { defs, diagnostics := .empty : DefsParsedSnapshot } + let includedVars := (← getScope).includedVars + runTermElabM fun vars => Term.elabMutualDef vars includedVars views + +syntax (name := divergentDef) + declModifiers "divergent" Lean.Parser.Command.definition : command -- Special command so that we don't fall back to the built-in mutual when we produce an error. local syntax "_divergent" Parser.Command.mutual : command -elab_rules : command | `(_divergent mutual $decls* end) => Command.elabMutualDef decls +elab_rules : command + | `(_divergent mutual $decls* end) => Command.elabMutualDef decls macro_rules | `(mutual $decls* end) => do @@ -1501,6 +1568,8 @@ namespace Tests /- Some examples of partial functions -/ + -- set_option trace.Diverge true + -- set_option pp.rawOnError true --set_option trace.Diverge.def true --set_option trace.Diverge.def.genBody true --set_option trace.Diverge.def.valid true diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean index 2c4c75550..275dc8108 100644 --- a/backends/lean/Base/Primitives/Core.lean +++ b/backends/lean/Base/Primitives/Core.lean @@ -74,3 +74,10 @@ end core /- [core::option::Option::is_none] -/ @[simp] def core.option.Option.is_none (T: Type) (self: Option T): Bool := self.isNone + +/- [core::clone::Clone::clone_from]: + Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 + Name pattern: core::clone::Clone::clone_from -/ +@[simp] def core.clone.Clone.clone_from + {Self : Type} (cloneInst : core.clone.Clone Self) (_self : Self) (source : Self) : Result Self := + cloneInst.clone source diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 65b8493bc..ab46e2c86 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -869,7 +869,7 @@ def evalAesopSaturate (options : Aesop.Options') (ruleSets : Array Name) : Tacti let rss ← Aesop.Frontend.getGlobalRuleSets ruleSets let rs ← Aesop.mkLocalRuleSet rss options |> Aesop.ElabM.runForwardElab (← getMainGoal) - tryLiftMetaTactic1 (Aesop.saturate rs · |>.run { options }) "Aesop.saturate failed" + tryLiftMetaTactic1 (Aesop.saturate rs · options) "Aesop.saturate failed" /-- Normalize the let-bindings by inlining them -/ def normalizeLetBindings (e : Expr) : MetaM Expr := diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json index cf7f10af5..859348233 100644 --- a/backends/lean/lake-manifest.json +++ b/backends/lean/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239", + "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cf30d04b6448dbb5a5b30a7d031e3949e74b9dd1", + "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,27 +35,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d1b33202c3a29a079f292de65ea438648123b635", + "rev": "a96aee5245720f588876021b6a0aa73efee49c76", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.39", + "inputRev": "v0.0.41", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", + "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e242f1edcacf917f40fae9b81f57f4bd0a4e45ac", + "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain index 6a4259fa5..e7a4f40b8 100644 --- a/backends/lean/lean-toolchain +++ b/backends/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0-rc2 +leanprover/lean4:v4.11.0-rc2 diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 3147c6814..1250e27de 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -508,6 +508,7 @@ let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list = ~extract_name: (Some (backend_choice "" "core::option::Option::is_none")) ~can_fail:false (); + mk_fun "core::clone::Clone::clone_from" (); ] @ List.map (fun ty -> diff --git a/tests/lean/Avl/Properties.lean b/tests/lean/Avl/Properties.lean index b26893f0d..c4e324f79 100644 --- a/tests/lean/Avl/Properties.lean +++ b/tests/lean/Avl/Properties.lean @@ -799,7 +799,6 @@ theorem Tree.insert_in_opt_node_spec split_conjs . simp [Node.invAux, Node.balanceFactor] . simp [Subtree.inv] - . apply Set.ext; simp . -- tree = some rename Node T => node have hNodeInv : Node.inv node := by simp_all (config := {maxDischargeDepth := 1}) diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean index 9b930662e..a8e7b90b2 100644 --- a/tests/lean/External/FunsExternal_Template.lean +++ b/tests/lean/External/FunsExternal_Template.lean @@ -24,10 +24,3 @@ axiom core.cell.Cell.get_mut core.cell.Cell T → State → Result (State × (T × (T → State → Result (State × (core.cell.Cell T))))) -/- [core::clone::Clone::clone_from]: - Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 - Name pattern: core::clone::Clone::clone_from -/ -axiom core.clone.Clone.clone_from - {Self : Type} (self_clause : core.clone.Clone Self) : - Self → Self → State → Result (State × Self) - diff --git a/tests/lean/Tutorial/Exercises.lean b/tests/lean/Tutorial/Exercises.lean index 4386c2ad3..8f0c5aaf5 100644 --- a/tests/lean/Tutorial/Exercises.lean +++ b/tests/lean/Tutorial/Exercises.lean @@ -165,7 +165,7 @@ theorem even_spec (n : U32) : . progress as ⟨ n' ⟩ progress as ⟨ b ⟩ simp [*] - simp [Int.even_sub] + simp [Int.odd_sub] termination_by n.toNat decreasing_by scalar_decr_tac @@ -437,10 +437,9 @@ divergent def add_no_overflow_loop - `scalar_eq_nf`: similar, but tuned to prove goals of the shape: `... = ...` You can try both tactics and see their effect. -/ --- Here, we're using ring_nf @[simp] -theorem toInt_aux_append (l0 l1 : List U32) : - toInt_aux (l0 ++ l1) = toInt_aux l0 + 2 ^ (32 * l0.length) * toInt_aux l1 := by +theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) : + toInt_aux (l.drop i) = l.index i + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by sorry /-- You will need this lemma for the proof of `add_no_overflow_loop_spec`. @@ -461,16 +460,11 @@ theorem toInt_aux_update (l : List U32) (i : Nat) (x : U32) (h0 : i < l.length) toInt_aux (l.update i x) = toInt_aux l + 2 ^ (32 * i) * (x - l.index i) := by sorry -/-- You will need this lemma for the proof of `add_no_overflow_loop_spec`. +/-- The proof about `add_no_overflow_loop`. - Advice: do the proof of `add_no_overflow_loop_spec` first, then come back to prove this lemma. + Hint: you will need to reason about non-linear arithmetic with `scalar_nf` and + `scalar_eq_nf`` (see above). -/ -@[simp] -theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) : - toInt_aux (l.drop i) = l.index i + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by - sorry - -/-- The proof about `add_no_overflow_loop` -/ @[pspec] theorem add_no_overflow_loop_spec (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize) diff --git a/tests/lean/Tutorial/Solutions.lean b/tests/lean/Tutorial/Solutions.lean index 92586508e..889a8b79c 100644 --- a/tests/lean/Tutorial/Solutions.lean +++ b/tests/lean/Tutorial/Solutions.lean @@ -1,251 +1,18 @@ import Base +import Tutorial.Tutorial open Primitives Result set_option maxHeartbeats 1000000 -namespace Primitives - -end Primitives - -namespace Tutorial.Exercises - -/- [tutorial::mul2_add1]: - Source: 'src/lib.rs', lines 11:0-11:31 -/ -def mul2_add1 (x : U32) : Result U32 := - do - let i ← x + x - i + 1#u32 - -#check U32.add_spec - -/-- Theorem about `mul2_add1`: without the `progress` tactic -/ --- @[pspec] -theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max) - : ∃ y, mul2_add1 x = ok y ∧ - ↑y = 2 * ↑x + (1 : Int) - := by - rw [mul2_add1] - have ⟨ x1, hEq1, hPost1 ⟩ := @U32.add_spec x x (by scalar_tac) - simp [hEq1] - have ⟨ x2, hEq2, hPost2 ⟩ := @U32.add_spec x1 1#u32 (by scalar_tac) - simp [hEq2] - scalar_tac - -/-- Theorem about `mul2_add1`: with the `progress` tactic -/ --- @[pspec] -theorem mul2_add1_spec' (x : U32) (h : 2 * ↑x + 1 ≤ U32.max) - : ∃ y, mul2_add1 x = ok y ∧ - ↑y = 2 * ↑x + (1 : Int) - := by - rw [mul2_add1] - progress with U32.add_spec as ⟨ x1 ⟩ - progress as ⟨ x2 ⟩ - scalar_tac - -/- [tutorial::mul2_add1_add]: - Source: 'src/lib.rs', lines 15:0-15:43 -/ -def mul2_add1_add (x : U32) (y : U32) : Result U32 := - do - let i ← mul2_add1 x - i + y - -/-- Theorem about `mul2_add1_add` -/ -theorem mul2_add1_add_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) : - ∃ z, mul2_add1_add x y = ok z ∧ - ↑z = 2 * ↑x + (1 : Int) + ↑y := by - rw [mul2_add1_add] - progress with mul2_add1_spec as ⟨ x1 ⟩ - progress as ⟨ x2 ⟩ - scalar_tac - -/- [tutorial::CList] - Source: 'src/lib.rs', lines 32:0-32:17 -/ -inductive CList (T : Type) := -| CCons : T → CList T → CList T -| CNil : CList T +namespace tutorial open CList -/-- Convert a "custom" list to a standard Lean list. - - By putting this definition in the namespace `CList`, we give the possibility of using the `.` - notation: if `x` has type `CList α` we can write `x.to_list` instead of `to_list x`. - -/ @[simp] def CList.to_list {α : Type} (x : CList α) : List α := match x with | CNil => [] | CCons hd tl => hd :: tl.to_list -/- [tutorial::list_nth]: - Source: 'src/lib.rs', lines 37:0-37:56 -/ -divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := - match l with - | CList.CCons x tl => - if i = 0#u32 - then Result.ok x - else do - let i1 ← i - 1#u32 - list_nth T tl i1 - | CList.CNil => Result.fail .panic - -/-- Theorem about `list_nth` -/ -theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) - (h : i.val < l.to_list.length) : - ∃ x, list_nth T l i = ok x ∧ - x = l.to_list.index i.toNat - := by - rw [list_nth] - split - . split - . simp_all - . simp_all - progress as ⟨ i1 ⟩ - progress as ⟨ x ⟩ - simp_all - . simp_all - scalar_tac - -/- [tutorial::i32_id]: - Source: 'src/lib.rs', lines 78:0-78:29 -/ -divergent def i32_id (i : I32) : Result I32 := - if i = 0#i32 - then Result.ok 0#i32 - else do - let i1 ← i - 1#i32 - let i2 ← i32_id i1 - i2 + 1#i32 - -/-- Theorem about `i32_id` -/ -theorem i32_id_spec (n : I32) (h : 0 ≤ n.val) : - i32_id n = ok n := by - rw [i32_id] - split - . simp [*] - . progress as ⟨ n1 ⟩ - progress - progress as ⟨ n2 ⟩ - scalar_tac -termination_by n.toNat -decreasing_by - simp_wf; scalar_tac - -- Remark: `scalar_decr_tac` does the same - -/- [tutorial::even]: - Source: 'src/lib.rs', lines 87:0-87:28 -/ -mutual divergent def even (i : U32) : Result Bool := - if i = 0#u32 - then Result.ok true - else do - let i1 ← i - 1#u32 - odd i1 - -/- [tutorial::odd]: - Source: 'src/lib.rs', lines 96:0-96:27 -/ -divergent def odd (i : U32) : Result Bool := - if i = 0#u32 - then Result.ok false - else do - let i1 ← i - 1#u32 - even i1 - -end - -mutual - -/-- The proof about `even` -/ -theorem even_spec (n : U32) : - ∃ b, even n = ok b ∧ (b ↔ Even n.val) := by - rw [even] - split - . simp [*] - . progress as ⟨ n' ⟩ - progress as ⟨ b ⟩ - simp [*] - simp [Int.even_sub] -termination_by n.toNat -decreasing_by scalar_decr_tac - -/-- The proof about `odd` -/ -theorem odd_spec (n : U32) : - ∃ b, odd n = ok b ∧ (b ↔ Odd n.val) := by - rw [odd] - split - . simp [*] - . progress as ⟨ n' ⟩ - progress as ⟨ b ⟩ - simp [*] - simp [Int.even_sub] -termination_by n.toNat -decreasing_by scalar_decr_tac - -end - -/- [tutorial::list_nth_mut1]: loop 0: - Source: 'src/lib.rs', lines 107:0-116:1 -/ -divergent def list_nth_mut1_loop - (T : Type) (l : CList T) (i : U32) : - Result (T × (T → Result (CList T))) - := - match l with - | CList.CCons x tl => - if i = 0#u32 - then - let back := fun ret => Result.ok (CList.CCons ret tl) - Result.ok (x, back) - else - do - let i1 ← i - 1#u32 - let (t, back) ← list_nth_mut1_loop T tl i1 - let back1 := - fun ret => do - let tl1 ← back ret - Result.ok (CList.CCons x tl1) - Result.ok (t, back1) - | CList.CNil => Result.fail .panic - -/- [tutorial::list_nth_mut1]: - Source: 'src/lib.rs', lines 107:0-107:77 -/ -@[reducible] -def list_nth_mut1 - (T : Type) (l : CList T) (i : U32) : - Result (T × (T → Result (CList T))) - := - list_nth_mut1_loop T l i - -/-- Theorem about `list_nth_mut1`: exercise! - - Hints: - - you can use `progress` to automatically apply a lemma, then refine it into `progress as ⟨ ... ⟩`` - to name the variables it introduces - - if there is a disjunction in the goal, use `split` - - if the goal is a conjunction, you can use `split_conjs` to introduce one subgoal per disjunct - - to simplify the context, use: - - `simp_all`: simplify the goal and the assumptions, and use the assumptions to simplify the goal - and the other assumption - - `simp`: simplify the goal - - `simp at *`: simplify the goal and the assumptions - - `simp [*]`: simplify the goal by using the assumptions - - `simp [a]`: simplify the goal by using the theorem `a`/the assumption `a`/unfolding the definition `a` - (also works with `simp_all`) - - `simp at h`: simplify a given hypothesis - - to prove a goal of the shape: `∀ x0 x1, ...`, use `intro y0 y1` to introduce the - quantified variables in the context and name them `y0`, `y1` - - if the goal is an arithmetic goal, use `scalar_tac` - - In order to type the special characters, you need to type the character '\' then a specific string: - - ↑ : \ + u ("up") - - → : \ + r ("right") - - ∧ : \ + and - - ∨ : \ + or - - ∀ : \ + forall - - ∃ : \ + exists - - Remarks: - - if `x` is a machine scalar, `↑x : Int` and `x.val` are the same - - if `v` is a vector (see exercises below) `↑v : List α` and `v.val` are the same - - If you don't know what a notation which appears in the goal is exactly, just put your mouse over it. - -/ theorem list_nth_mut1_spec {T: Type} [Inhabited T] (l : CList T) (i : U32) (h : i.val < l.to_list.length) : ∃ x back, list_nth_mut1 T l i = ok (x, back) ∧ @@ -272,40 +39,6 @@ theorem list_nth_mut1_spec {T: Type} [Inhabited T] (l : CList T) (i : U32) . simp_all scalar_tac -/- [tutorial::list_tail]: loop 0: - Source: 'src/lib.rs', lines 118:0-123:1 -/ -divergent def list_tail_loop - (T : Type) (l : CList T) : - Result ((CList T) × (CList T → Result (CList T))) - := - match l with - | CList.CCons t tl => - do - let (c, back) ← list_tail_loop T tl - let back1 := - fun ret => do - let tl1 ← back ret - Result.ok (CList.CCons t tl1) - Result.ok (c, back1) - | CList.CNil => Result.ok (CList.CNil, Result.ok) - -/- [tutorial::list_tail]: - Source: 'src/lib.rs', lines 118:0-118:68 -/ -@[reducible] -def list_tail - (T : Type) (l : CList T) : - Result ((CList T) × (CList T → Result (CList T))) - := - list_tail_loop T l - -/- [tutorial::append_in_place]: - Source: 'src/lib.rs', lines 125:0-125:67 -/ -def append_in_place - (T : Type) (l0 : CList T) (l1 : CList T) : Result (CList T) := - do - let (_, list_tail_back) ← list_tail T l0 - list_tail_back l1 - /-- Theorem about `list_tail` -/ @[pspec] theorem list_tail_spec {T : Type} (l : CList T) : @@ -335,23 +68,6 @@ theorem append_in_place_spec {T : Type} (l0 l1 : CList T) : /- Big numbers -/ -/- [tutorial::zero]: loop 0: - Source: 'src/lib.rs', lines 6:4-11:1 -/ -divergent def zero_loop - (x : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) := - let i1 := alloc.vec.Vec.len U32 x - if i < i1 - then - do - let (_, index_mut_back) ← - alloc.vec.Vec.index_mut U32 Usize - (core.slice.index.SliceIndexUsizeSliceTInst U32) x i - let i2 ← i + 1#usize - let x1 ← index_mut_back 0#u32 - zero_loop x1 i2 - else Result.ok x - - -- Auxiliary definitions to interpret a vector of u32 as a mathematical integer @[simp] def toInt_aux (l : List U32) : ℤ := @@ -393,15 +109,6 @@ theorem zero_loop_spec termination_by (x.length - i.val).toNat decreasing_by scalar_decr_tac -/- [tutorial::zero]: - Source: 'src/lib.rs', lines 5:0-5:28 -/ -def zero (x : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := - zero_loop x 0#usize - -/-- You will need this lemma for the proof of `zero_spec` - - Advice: do the proof of `zero_spec` first, then come back to prove this lemma. --/ theorem all_nil_impl_toInt_eq_zero (l : List U32) (h : ∀ (j : ℕ), j < l.length → l.index j = 0#u32) : toInt_aux l = 0 := by @@ -429,47 +136,20 @@ theorem zero_spec (x : alloc.vec.Vec U32) : apply all_nil_impl_toInt_eq_zero simp_all -/- [tutorial::add_no_overflow]: loop 0: - Source: 'src/lib.rs', lines 19:4-24:1 -/ -divergent def add_no_overflow_loop - (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (i : Usize) : - Result (alloc.vec.Vec U32) - := - let i1 := alloc.vec.Vec.len U32 x - if i < i1 - then - do - let i2 ← - alloc.vec.Vec.index U32 Usize (core.slice.index.SliceIndexUsizeSliceTInst - U32) y i - let (i3, index_mut_back) ← - alloc.vec.Vec.index_mut U32 Usize - (core.slice.index.SliceIndexUsizeSliceTInst U32) x i - let i4 ← i3 + i2 - let i5 ← i + 1#usize - let x1 ← index_mut_back i4 - add_no_overflow_loop x1 y i5 - else Result.ok x - -/-- You will need this lemma for the proof of `add_no_overflow_loop_spec`. - - Advice: do the proof of `add_no_overflow_loop_spec` first, then come back to prove this lemma. - -/ --- Here, we're using ring_nf @[simp] -theorem toInt_aux_append (l0 l1 : List U32) : - toInt_aux (l0 ++ l1) = toInt_aux l0 + 2 ^ (32 * l0.length) * toInt_aux l1 := by - match l0 with - | [] => simp - | hd :: tl => - have := toInt_aux_append tl l1 +theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) : + toInt_aux (l.drop i) = l.index i + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by + cases l with + | nil => simp at * + | cons hd tl => simp_all - scalar_eq_nf - -/-- You will need this lemma for the proof of `add_no_overflow_loop_spec`. + dcases i = 0 <;> simp_all + have := toInt_aux_drop tl (i - 1) (by scalar_tac) + simp_all + scalar_nf at * + have : 1 + (i - 1) = i := by scalar_tac + simp [*] - Advice: do the proof of `add_no_overflow_loop_spec` first, then come back to prove this lemma. - -/ @[simp] theorem toInt_aux_update (l : List U32) (i : Nat) (x : U32) (h0 : i < l.length) : toInt_aux (l.update i x) = toInt_aux l + 2 ^ (32 * i) * (x - l.index i) := by @@ -506,24 +186,6 @@ theorem toInt_aux_update (l : List U32) (i : Nat) (x : U32) (h0 : i < l.length) simp [mul_assoc, *] scalar_eq_nf -/-- You will need this lemma for the proof of `add_no_overflow_loop_spec`. - - Advice: do the proof of `add_no_overflow_loop_spec` first, then come back to prove this lemma. - -/ -@[simp] -theorem toInt_aux_drop (l : List U32) (i : Nat) (h0 : i < l.length) : - toInt_aux (l.drop i) = l.index i + 2 ^ 32 * toInt_aux (l.drop (i + 1)) := by - cases l with - | nil => simp at * - | cons hd tl => - simp_all - dcases i = 0 <;> simp_all - have := toInt_aux_drop tl (i - 1) (by scalar_tac) - simp_all - scalar_nf at * - have : 1 + (i - 1) = i := by scalar_tac - simp [*] - /-- The proof about `add_no_overflow_loop` -/ @[pspec] theorem add_no_overflow_loop_spec @@ -574,14 +236,6 @@ theorem add_no_overflow_loop_spec termination_by (x.length - i.val).toNat decreasing_by scalar_decr_tac -/- [tutorial::add_no_overflow]: - Source: 'src/lib.rs', lines 18:0-18:50 -/ -def add_no_overflow - (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) : - Result (alloc.vec.Vec U32) - := - add_no_overflow_loop x y 0#usize - /-- The proof about `add_no_overflow` -/ theorem add_no_overflow_spec (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (hLength : x.length = y.length) @@ -593,38 +247,6 @@ theorem add_no_overflow_spec (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) progress as ⟨ x' ⟩ <;> simp_all [toInt] -/- [tutorial::add_with_carry]: loop 0: - Source: 'src/lib.rs', lines 39:4-50:1 -/ -divergent def add_with_carry_loop - (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (c0 : U8) (i : Usize) : - Result (U8 × (alloc.vec.Vec U32)) - := - let i1 := alloc.vec.Vec.len U32 x - if i < i1 - then - do - let i2 ← - alloc.vec.Vec.index U32 Usize (core.slice.index.SliceIndexUsizeSliceTInst - U32) x i - let i3 ← Scalar.cast .U32 c0 - let p ← core.num.U32.overflowing_add i2 i3 - let (sum, c1) := p - let i4 ← - alloc.vec.Vec.index U32 Usize (core.slice.index.SliceIndexUsizeSliceTInst - U32) y i - let p1 ← core.num.U32.overflowing_add sum i4 - let (sum1, c2) := p1 - let i5 ← Scalar.cast_bool .U8 c1 - let i6 ← Scalar.cast_bool .U8 c2 - let c01 ← i5 + i6 - let (_, index_mut_back) ← - alloc.vec.Vec.index_mut U32 Usize - (core.slice.index.SliceIndexUsizeSliceTInst U32) x i - let i7 ← i + 1#usize - let x1 ← index_mut_back sum1 - add_with_carry_loop x1 y c01 i7 - else Result.ok (c0, x) - /-- The proof about `add_with_carry_loop` -/ @[pspec] theorem add_with_carry_loop_spec @@ -667,14 +289,6 @@ theorem add_with_carry_loop_spec termination_by (x.length - i.val).toNat decreasing_by scalar_decr_tac -/- [tutorial::add_with_carry]: - Source: 'src/lib.rs', lines 37:0-37:55 -/ -def add_with_carry - (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) : - Result (U8 × (alloc.vec.Vec U32)) - := - add_with_carry_loop x y 0#u8 0#usize - /-- The proof about `add_with_carry` -/ @[pspec] theorem add_with_carry_spec @@ -688,71 +302,4 @@ theorem add_with_carry_spec progress as ⟨ c, x' ⟩ simp_all -/- Bonus exercises -/ - -/- [tutorial::max]: - Source: 'src/lib.rs', lines 26:0-26:37 -/ -def max (x : Usize) (y : Usize) : Result Usize := - if x > y - then Result.ok x - else Result.ok y - -/- [tutorial::get_or_zero]: - Source: 'src/lib.rs', lines 30:0-30:45 -/ -def get_or_zero (y : alloc.vec.Vec U32) (i : Usize) : Result U32 := - let i1 := alloc.vec.Vec.len U32 y - if i < i1 - then - alloc.vec.Vec.index U32 Usize (core.slice.index.SliceIndexUsizeSliceTInst - U32) y i - else Result.ok 0#u32 - -/- [tutorial::add]: loop 0: - Source: 'src/lib.rs', lines 60:4-76:1 -/ -divergent def add_loop - (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (max1 : Usize) (c0 : U8) - (i : Usize) : - Result (alloc.vec.Vec U32) - := - if i < max1 - then - do - let yi ← get_or_zero y i - let i1 ← - alloc.vec.Vec.index U32 Usize (core.slice.index.SliceIndexUsizeSliceTInst - U32) x i - let i2 ← Scalar.cast .U32 c0 - let p ← core.num.U32.overflowing_add i1 i2 - let (sum, c1) := p - let p1 ← core.num.U32.overflowing_add sum yi - let (sum1, c2) := p1 - let i3 ← Scalar.cast_bool .U8 c1 - let i4 ← Scalar.cast_bool .U8 c2 - let c01 ← i3 + i4 - let (_, index_mut_back) ← - alloc.vec.Vec.index_mut U32 Usize - (core.slice.index.SliceIndexUsizeSliceTInst U32) x i - let i5 ← i + 1#usize - let x1 ← index_mut_back sum1 - add_loop x1 y max1 c01 i5 - else - if c0 != 0#u8 - then do - let i1 ← Scalar.cast .U32 c0 - alloc.vec.Vec.push U32 x i1 - else Result.ok x - -/- [tutorial::add]: - Source: 'src/lib.rs', lines 55:0-55:38 -/ -def add - (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) : - Result (alloc.vec.Vec U32) - := - do - let i := alloc.vec.Vec.len U32 x - let i1 := alloc.vec.Vec.len U32 y - let max1 ← max i i1 - let x1 ← alloc.vec.Vec.resize U32 core.clone.CloneU32 x max1 0#u32 - add_loop x1 y max1 0#u8 0#usize - -end Tutorial.Exercises +end tutorial diff --git a/tests/lean/Tutorial/Tutorial.lean b/tests/lean/Tutorial/Tutorial.lean index c35550665..153229f0f 100644 --- a/tests/lean/Tutorial/Tutorial.lean +++ b/tests/lean/Tutorial/Tutorial.lean @@ -385,11 +385,4 @@ def add let x1 ← alloc.vec.Vec.resize U32 core.clone.CloneU32 x max1 0#u32 add_loop x1 y max1 0#u8 0#usize -/- [core::clone::Clone::clone_from]: - Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43 - Name pattern: core::clone::Clone::clone_from -/ -axiom core.clone.Clone.clone_from - {Self : Type} (self_clause : core.clone.Clone Self) : - Self → Self → Result Self - end tutorial diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json index 958743b24..d6c3c7a09 100644 --- a/tests/lean/lake-manifest.json +++ b/tests/lean/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239", + "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cf30d04b6448dbb5a5b30a7d031e3949e74b9dd1", + "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,27 +35,27 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d1b33202c3a29a079f292de65ea438648123b635", + "rev": "a96aee5245720f588876021b6a0aa73efee49c76", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.39", + "inputRev": "v0.0.41", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", + "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c198452b2993c475770cdfa2801ad2a29fd35194", + "rev": "9d7806d77c33a5e19050de8fbdc106a28150ec71", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain index 6a4259fa5..e7a4f40b8 100644 --- a/tests/lean/lean-toolchain +++ b/tests/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0-rc2 +leanprover/lean4:v4.11.0-rc2