From 3a4d2cded30beb3343ba0e13a3ddb2809703e26d Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 22 Jul 2024 13:56:50 +0200 Subject: [PATCH 1/6] refactor: Introduce PProdN module (#4807) code to create nested `PProd`s, and project out, and related functions were scattered in variuos places. This unifies them in `Lean.Meta.PProdN`. It also consistently avoids the terminal `True` or `PUnit`, for slightly easier to read constructions. --- .../Elab/PreDefinition/Structural/BRecOn.lean | 19 ++- .../PreDefinition/Structural/FunPacker.lean | 126 --------------- src/Lean/Meta/AppBuilder.lean | 21 --- src/Lean/Meta/ArgsPacker.lean | 5 +- src/Lean/Meta/Constructions/BRecOn.lean | 79 ++-------- src/Lean/Meta/PProdN.lean | 145 ++++++++++++++++++ src/Lean/Meta/Tactic/FunInd.lean | 30 +--- tests/lean/run/letrecInProofs.lean | 13 +- .../run/nestedInductiveConstructions.lean | 47 +++--- tests/lean/unusedLet.lean.expected.out | 2 +- 10 files changed, 201 insertions(+), 286 deletions(-) delete mode 100644 src/Lean/Elab/PreDefinition/Structural/FunPacker.lean create mode 100644 src/Lean/Meta/PProdN.lean diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 96f742b747cc..4bb591844fb7 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -5,11 +5,11 @@ Authors: Leonardo de Moura, Joachim Breitner -/ prelude import Lean.Util.HasConstCache +import Lean.Meta.PProdN import Lean.Meta.Match.MatcherApp.Transform import Lean.Elab.RecAppSyntax import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Structural.Basic -import Lean.Elab.PreDefinition.Structural.FunPacker import Lean.Elab.PreDefinition.Structural.RecArgInfo namespace Lean.Elab.Structural @@ -21,11 +21,11 @@ private def throwToBelowFailed : MetaM α := partial def searchPProd (e : Expr) (F : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do match (← whnf e) with | .app (.app (.const `PProd _) d1) d2 => - (do searchPProd d1 (← mkAppM ``PProd.fst #[F]) k) - <|> (do searchPProd d2 (← mkAppM `PProd.snd #[F]) k) + (do searchPProd d1 (.proj ``PProd 0 F) k) + <|> (do searchPProd d2 (.proj ``PProd 1 F) k) | .app (.app (.const `And _) d1) d2 => - (do searchPProd d1 (← mkAppM `And.left #[F]) k) - <|> (do searchPProd d2 (← mkAppM `And.right #[F]) k) + (do searchPProd d1 (.proj `And 0 F) k) + <|> (do searchPProd d2 (.proj `And 1 F) k) | .const `PUnit _ | .const `True _ => throwToBelowFailed | _ => k e F @@ -85,7 +85,7 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat) return ((← mkFreshUserName `C), fun _ => pure t) withLocalDeclsD CDecls fun Cs => do -- We have to pack these canary motives like we packed the real motives - let packedCs ← positions.mapMwith packMotives motiveTypes Cs + let packedCs ← positions.mapMwith PProdN.packLambdas motiveTypes Cs let belowDict := mkAppN pre packedCs let belowDict := mkAppN belowDict finalArgs trace[Elab.definition.structural] "initial belowDict for {Cs}:{indentExpr belowDict}" @@ -250,7 +250,7 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions) let brecOnAux := brecOnCons 0 -- Infer the type of the packed motive arguments let packedMotiveTypes ← inferArgumentTypesN indGroup.numMotives brecOnAux - let packedMotives ← positions.mapMwith packMotives packedMotiveTypes motives + let packedMotives ← positions.mapMwith PProdN.packLambdas packedMotiveTypes motives return fun n => mkAppN (brecOnCons n) packedMotives @@ -289,12 +289,11 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp let brecOn := brecOnConst recArgInfo.indIdx let brecOn := mkAppN brecOn indexMajorArgs let packedFTypes ← inferArgumentTypesN positions.size brecOn - let packedFArgs ← positions.mapMwith packFArgs packedFTypes FArgs + let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs let brecOn := mkAppN brecOn packedFArgs let some poss := positions.find? (·.contains fnIdx) | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}" - let brecOn ← if poss.size = 1 then pure brecOn else - mkPProdProjN (poss.getIdx? fnIdx).get! brecOn + let brecOn ← PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn mkLambdaFVars ys (mkAppN brecOn otherArgs) end Lean.Elab.Structural diff --git a/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean b/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean deleted file mode 100644 index 7ef1262313b0..000000000000 --- a/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean +++ /dev/null @@ -1,126 +0,0 @@ -/- -Copyright (c) 2024 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joachim Breitner --/ -prelude -import Lean.Meta.InferType - -/-! -This module contains the logic that packs the motives and FArgs of multiple functions into one, -to allow structural mutual recursion where the number of functions is not exactly the same -as the number of inductive data types in the mutual inductive group. - -The private helper functions related to `PProd` here should at some point be moved to their own -module, so that they can be used elsewhere (e.g. `FunInd`), and possibly unified with the similar -constructions for well-founded recursion (see `ArgsPacker` module). --/ - -namespace Lean.Elab.Structural -open Meta - -private def mkPUnit : Level → Expr - | .zero => .const ``True [] - | lvl => .const ``PUnit [lvl] - -private def mkPProd (e1 e2 : Expr) : MetaM Expr := do - let lvl1 ← getLevel e1 - let lvl2 ← getLevel e2 - if lvl1 matches .zero && lvl2 matches .zero then - return mkApp2 (.const `And []) e1 e2 - else - return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2 - -private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr := - es.foldrM (init := mkPUnit lvl) mkPProd - -private def mkPUnitMk : Level → Expr - | .zero => .const ``True.intro [] - | lvl => .const ``PUnit.unit [lvl] - -private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do - let t1 ← inferType e1 - let t2 ← inferType e2 - let lvl1 ← getLevel t1 - let lvl2 ← getLevel t2 - if lvl1 matches .zero && lvl2 matches .zero then - return mkApp4 (.const ``And.intro []) t1 t2 e1 e2 - else - return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2 - -private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr := - es.foldrM (init := mkPUnitMk lvl) mkPProdMk - -/-- `PProd.fst` or `And.left` (as projections) -/ -private def mkPProdFst (e : Expr) : MetaM Expr := do - let t ← whnf (← inferType e) - match_expr t with - | PProd _ _ => return .proj ``PProd 0 e - | And _ _ => return .proj ``And 0 e - | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}" - -/-- `PProd.snd` or `And.right` (as projections) -/ -private def mkPProdSnd (e : Expr) : MetaM Expr := do - let t ← whnf (← inferType e) - match_expr t with - | PProd _ _ => return .proj ``PProd 1 e - | And _ _ => return .proj ``And 1 e - | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}" - -/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ ∧ True`, return the proof of `Pᵢ` -/ -def mkPProdProjN (i : Nat) (e : Expr) : MetaM Expr := do - let mut value := e - for _ in [:i] do - value ← mkPProdSnd value - value ← mkPProdFst value - return value - -/-- -Combines motives from different functions that recurse on the same parameter type into a single -function returning a `PProd` type. - -For example -``` -packMotives (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )] -``` -will return -``` -fun (n : Nat) (PProd Nat (Fin n → Fin n)) -``` - -It is the identity if `motives.size = 1`. - -It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no motive is given. -(this is the reason we need the expected type in the `motiveType` parameter). - --/ -def packMotives (motiveType : Expr) (motives : Array Expr) : MetaM Expr := do - if motives.size = 1 then - return motives[0]! - trace[Elab.definition.structural] "packing Motives\nexpected: {motiveType}\nmotives: {motives}" - forallTelescope motiveType fun xs sort => do - unless sort.isSort do - throwError "packMotives: Unexpected motiveType {motiveType}" - -- NB: Use beta, not instantiateLambda; when constructing the belowDict below - -- we pass `C`, a plain FVar, here - let motives := motives.map (·.beta xs) - let packedMotives ← mkNProd sort.sortLevel! motives - mkLambdaFVars xs packedMotives - -/-- -Combines the F-args from different functions that recurse on the same parameter type into a single -function returning a `PProd` value. See `packMotives` - -It is the identity if `motives.size = 1`. --/ -def packFArgs (FArgType : Expr) (FArgs : Array Expr) : MetaM Expr := do - if FArgs.size = 1 then - return FArgs[0]! - forallTelescope FArgType fun xs body => do - let lvl ← getLevel body - let FArgs := FArgs.map (·.beta xs) - let packedFArgs ← mkNProdMk lvl FArgs - mkLambdaFVars xs packedFArgs - - -end Lean.Elab.Structural diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index 41a7ea2f1f1a..898b59abee51 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -665,27 +665,6 @@ def mkIffOfEq (h : Expr) : MetaM Expr := do else mkAppM ``Iff.of_eq #[h] -/-- -Given proofs of `P₁`, …, `Pₙ`, returns a proof of `P₁ ∧ … ∧ Pₙ`. -If `n = 0` returns a proof of `True`. -If `n = 1` returns the proof of `P₁`. --/ -def mkAndIntroN : Array Expr → MetaM Expr -| #[] => return mkConst ``True.intro [] -| #[e] => return e -| es => es.foldrM (start := es.size - 1) (fun a b => mkAppM ``And.intro #[a,b]) es.back - - -/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ`, return the proof of `Pᵢ` -/ -def mkProjAndN (n i : Nat) (e : Expr) : Expr := Id.run do - let mut value := e - for _ in [:i] do - value := mkProj ``And 1 value - if i + 1 < n then - value := mkProj ``And 0 value - return value - - builtin_initialize do registerTraceClass `Meta.appBuilder registerTraceClass `Meta.appBuilder.result (inherited := true) diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean index d871e97c972d..2b2b26d4711c 100644 --- a/src/Lean/Meta/ArgsPacker.lean +++ b/src/Lean/Meta/ArgsPacker.lean @@ -6,6 +6,7 @@ Authors: Joachim Breitner prelude import Lean.Meta.AppBuilder +import Lean.Meta.PProdN import Lean.Meta.ArgsPacker.Basic /-! @@ -518,7 +519,7 @@ def curry (argsPacker : ArgsPacker) (e : Expr) : MetaM Expr := do let mut es := #[] for i in [:argsPacker.numFuncs] do es := es.push (← argsPacker.curryProj e i) - mkAndIntroN es + PProdN.mk 0 es /-- Given type `(a ⊗' b ⊕' c ⊗' d) → e`, brings `a → b → e` and `c → d → e` @@ -533,7 +534,7 @@ where | [], acc => k acc | t::ts, acc => do let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size+1}" - withLocalDecl name .default t fun x => do + withLocalDeclD name t fun x => do go ts (acc.push x) /-- diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean index bee7244a54d3..52e4297d78fa 100644 --- a/src/Lean/Meta/Constructions/BRecOn.lean +++ b/src/Lean/Meta/Constructions/BRecOn.lean @@ -8,67 +8,18 @@ import Lean.Meta.InferType import Lean.AuxRecursor import Lean.AddDecl import Lean.Meta.CompletionName +import Lean.Meta.PProdN namespace Lean open Meta -section PProd - -/--! -Helpers to construct types and values of `PProd` and project out of them, set up to use `And` -instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful -elsewhere. --/ - -private def mkPUnit : Level → Expr - | .zero => .const ``True [] - | lvl => .const ``PUnit [lvl] - -private def mkPProd (e1 e2 : Expr) : MetaM Expr := do - let lvl1 ← getLevel e1 - let lvl2 ← getLevel e2 - if lvl1 matches .zero && lvl2 matches .zero then - return mkApp2 (.const `And []) e1 e2 - else - return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2 - -private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr := - es.foldrM (init := mkPUnit lvl) mkPProd - -private def mkPUnitMk : Level → Expr - | .zero => .const ``True.intro [] - | lvl => .const ``PUnit.unit [lvl] - -private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do - let t1 ← inferType e1 - let t2 ← inferType e2 - let lvl1 ← getLevel t1 - let lvl2 ← getLevel t2 - if lvl1 matches .zero && lvl2 matches .zero then - return mkApp4 (.const ``And.intro []) t1 t2 e1 e2 - else - return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2 - -private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr := - es.foldrM (init := mkPUnitMk lvl) mkPProdMk - -/-- `PProd.fst` or `And.left` (as projections) -/ -private def mkPProdFst (e : Expr) : MetaM Expr := do - let t ← whnf (← inferType e) - match_expr t with - | PProd _ _ => return .proj ``PProd 0 e - | And _ _ => return .proj ``And 0 e - | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}" - -/-- `PProd.snd` or `And.right` (as projections) -/ -private def mkPProdSnd (e : Expr) : MetaM Expr := do - let t ← whnf (← inferType e) - match_expr t with - | PProd _ _ => return .proj ``PProd 1 e - | And _ _ => return .proj ``And 1 e - | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}" - -end PProd +/-- Transforms `e : xᵢ → (t₁ ×' t₂)` into `(xᵢ → t₁) ×' (xᵢ → t₂) -/ +private def etaPProd (xs : Array Expr) (e : Expr) : MetaM Expr := do + if xs.isEmpty then return e + let r := mkAppN e xs + let r₁ ← mkLambdaFVars xs (← mkPProdFst r) + let r₂ ← mkLambdaFVars xs (← mkPProdSnd r) + mkPProdMk r₁ r₂ /-- If `minorType` is the type of a minor premies of a recursor, such as @@ -91,7 +42,7 @@ private def buildBelowMinorPremise (rlvl : Level) (motives : Array Expr) (minorT where ibelow := rlvl matches .zero go (prods : Array Expr) : List Expr → MetaM Expr - | [] => mkNProd rlvl prods + | [] => PProdN.pack rlvl prods | arg::args => do let argType ← inferType arg forallTelescope argType fun arg_args arg_type => do @@ -243,7 +194,7 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr) forallTelescope minorType fun minor_args minor_type => do let rec go (prods : Array Expr) : List Expr → MetaM Expr | [] => minor_type.withApp fun minor_type_fn minor_type_args => do - let b ← mkNProdMk rlvl prods + let b ← PProdN.mk rlvl prods let .some ⟨idx, _⟩ := motives.indexOf? minor_type_fn | throwError m!"Did not find {minor_type} in {motives}" mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b @@ -256,14 +207,8 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr) let type' ← mkForallFVars arg_args (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) ) withLocalDeclD name type' fun arg' => do - if arg_args.isEmpty then - mkLambdaFVars #[arg'] (← go (prods.push arg') args) - else - let r := mkAppN arg' arg_args - let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r) - let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r) - let r ← mkPProdMk r₁ r₂ - mkLambdaFVars #[arg'] (← go (prods.push r) args) + let r ← etaPProd arg_args arg' + mkLambdaFVars #[arg'] (← go (prods.push r) args) else mkLambdaFVars #[arg] (← go prods args) go #[] minor_args.toList diff --git a/src/Lean/Meta/PProdN.lean b/src/Lean/Meta/PProdN.lean new file mode 100644 index 000000000000..fcde4d4a46fb --- /dev/null +++ b/src/Lean/Meta/PProdN.lean @@ -0,0 +1,145 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joachim Breitner +-/ + +prelude +import Lean.Meta.InferType + +/-! +This module provides functios to pack and unpack values using nested `PProd` or `And`, +as used in the `.below` construction, in the `.brecOn` construction for mutual recursion and +and the `mutual_induct` construction. + +It uses `And` (equivalent to `PProd.{0}` when possible). + +The nesting is `t₁ ×' (t₂ ×' t₃)`, not `t₁ ×' (t₂ ×' (t₃ ×' PUnit))`. This is more readable, +slightly shorter, and means that the packing is the identity if `n=1`, which we rely on in some +places. It comes at the expense that hat projection needs to know `n`. + +Packing an empty list uses `True` or `PUnit` depending on the given `lvl`. + +Also see `Lean.Meta.ArgsPacker` for a similar module for `PSigma` and `PSum`, used by well-founded recursion. +-/ + + +namespace Lean.Meta + +/-- Given types `t₁` and `t₂`, produces `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow) -/ +def mkPProd (e1 e2 : Expr) : MetaM Expr := do + let lvl1 ← getLevel e1 + let lvl2 ← getLevel e2 + if lvl1 matches .zero && lvl2 matches .zero then + return mkApp2 (.const `And []) e1 e2 + else + return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2 + +/-- Given values of typs `t₁` and `t₂`, produces value of type `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow) -/ +def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do + let t1 ← inferType e1 + let t2 ← inferType e2 + let lvl1 ← getLevel t1 + let lvl2 ← getLevel t2 + if lvl1 matches .zero && lvl2 matches .zero then + return mkApp4 (.const ``And.intro []) t1 t2 e1 e2 + else + return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2 + +/-- `PProd.fst` or `And.left` (using `.proj`) -/ +def mkPProdFst (e : Expr) : MetaM Expr := do + let t ← whnf (← inferType e) + match_expr t with + | PProd _ _ => return .proj ``PProd 0 e + | And _ _ => return .proj ``And 0 e + | _ => panic! "mkPProdFst: cannot handle{indentExpr e}\nof type{indentExpr t}" + +/-- `PProd.snd` or `And.right` (using `.proj`) -/ +def mkPProdSnd (e : Expr) : MetaM Expr := do + let t ← whnf (← inferType e) + match_expr t with + | PProd _ _ => return .proj ``PProd 1 e + | And _ _ => return .proj ``And 1 e + | _ => panic! "mkPProdSnd: cannot handle{indentExpr e}\nof type{indentExpr t}" + + + +namespace PProdN + +/-- Given types `tᵢ`, produces `t₁ ×' t₂ ×' t₃` -/ +def pack (lvl : Level) (xs : Array Expr) : MetaM Expr := do + if xs.size = 0 then + if lvl matches .zero then return .const ``True [] + else return .const ``PUnit [lvl] + let xBack := xs.back + xs.pop.foldrM mkPProd xBack + +/-- Given values `xᵢ` of type `tᵢ`, produces value of type `t₁ ×' t₂ ×' t₃` -/ +def mk (lvl : Level) (xs : Array Expr) : MetaM Expr := do + if xs.size = 0 then + if lvl matches .zero then return .const ``True.intro [] + else return .const ``PUnit.unit [lvl] + let xBack := xs.back + xs.pop.foldrM mkPProdMk xBack + +/-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/ +def proj (n i : Nat) (e : Expr) : MetaM Expr := do + let mut value := e + for _ in [:i] do + value ← mkPProdSnd value + if i+1 < n then + mkPProdFst value + else + pure value + + + +/-- +Packs multiple type-forming lambda expressions taking the same parameters using `PProd`. + +The parameter `type` is the common type of the these expressions + +For example +``` +packLambdas (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )] +``` +will return +``` +fun (n : Nat) => (Nat ×' (Fin n → Fin n)) +``` + +It is the identity if `es.size = 1`. + +It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no expressions are given. +(this is the reason we need the expected type in the `type` parameter). + +-/ +def packLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do + if es.size = 1 then + return es[0]! + forallTelescope type fun xs sort => do + assert! sort.isSort + -- NB: Use beta, not instantiateLambda; when constructing the belowDict below + -- we pass `C`, a plain FVar, here + let es' := es.map (·.beta xs) + let packed ← PProdN.pack sort.sortLevel! es' + mkLambdaFVars xs packed + +/-- +The value analogue to `PProdN.packLambdas`. + +It is the identity if `es.size = 1`. +-/ +def mkLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do + if es.size = 1 then + return es[0]! + forallTelescope type fun xs body => do + let lvl ← getLevel body + let es' := es.map (·.beta xs) + let packed ← PProdN.mk lvl es' + mkLambdaFVars xs packed + + +end PProdN + +end Lean.Meta diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index e6eb1f96f52c..d5f1ce3d6640 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -12,6 +12,7 @@ import Lean.Meta.Tactic.Cleanup import Lean.Meta.Tactic.Subst import Lean.Meta.Injective -- for elimOptParam import Lean.Meta.ArgsPacker +import Lean.Meta.PProdN import Lean.Elab.PreDefinition.WF.Eqns import Lean.Elab.PreDefinition.Structural.Eqns import Lean.Elab.Command @@ -188,21 +189,6 @@ def removeLamda {n} [MonadLiftT MetaM n] [MonadError n] [MonadNameGenerator n] [ let b := b.instantiate1 (.fvar x) k x b -/-- `PProd.fst` or `And.left` -/ -def mkFst (e : Expr) : MetaM Expr := do - let t ← whnf (← inferType e) - match_expr t with - | PProd t₁ t₂ => return mkApp3 (.const ``PProd.fst t.getAppFn.constLevels!) t₁ t₂ e - | And t₁ t₂ => return mkApp3 (.const ``And.left []) t₁ t₂ e - | _ => throwError "Cannot project out of{indentExpr e}\nof type{indentExpr t}" - -/-- `PProd.snd` or `And.right` -/ -def mkSnd (e : Expr) : MetaM Expr := do - let t ← whnf (← inferType e) - match_expr t with - | PProd t₁ t₂ => return mkApp3 (.const ``PProd.snd t.getAppFn.constLevels!) t₁ t₂ e - | And t₁ t₂ => return mkApp3 (.const ``And.right []) t₁ t₂ e - | _ => throwError "Cannot project out of{indentExpr e}\nof type{indentExpr t}" /-- A monad to help collecting inductive hypothesis. @@ -310,7 +296,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E forallBoundedTelescope altType (some 1) fun newIH' _goal' => do let #[newIH'] := newIH' | unreachable! let altIHs ← M.exec <| foldAndCollect oldIH' newIH'.fvarId! isRecCall alt - let altIH ← mkAndIntroN altIHs + let altIH ← PProdN.mk 0 altIHs mkLambdaFVars #[newIH'] altIH) (onRemaining := fun _ => pure #[mkFVar newIH]) let ihMatcherApp'' ← ihMatcherApp'.inferMatchType @@ -328,11 +314,6 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E (onRemaining := fun _ => pure #[]) return matcherApp'.toExpr - -- These projections can be type changing, so re-infer their type arguments - match_expr e with - | PProd.fst _ _ e => mkFst (← foldAndCollect oldIH newIH isRecCall e) - | PProd.snd _ _ e => mkSnd (← foldAndCollect oldIH newIH isRecCall e) - | _ => if e.getAppArgs.any (·.isFVarOf oldIH) then -- Sometimes Fix.lean abstracts over oldIH in a proof definition. @@ -371,6 +352,10 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E | .mdata m b => pure <| .mdata m (← foldAndCollect oldIH newIH isRecCall b) + -- These projections can be type changing (to And), so re-infer their type arguments + | .proj ``PProd 0 e => mkPProdFst (← foldAndCollect oldIH newIH isRecCall e) + | .proj ``PProd 1 e => mkPProdSnd (← foldAndCollect oldIH newIH isRecCall e) + | .proj t i e => pure <| .proj t i (← foldAndCollect oldIH newIH isRecCall e) @@ -690,7 +675,6 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do { name := inductName, levelParams := us, type := eTyp, value := e' } return inductName - /-- In the type of `value`, reduces * Beta-redexes @@ -806,7 +790,7 @@ def deriveUnpackedInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name): Met let value ← forallTelescope ci.type fun xs _body => do let value := .const ci.name (levelParams.map mkLevelParam) let value := mkAppN value xs - let value := mkProjAndN eqnInfo.declNames.size idx value + let value ← PProdN.proj eqnInfo.declNames.size idx value mkLambdaFVars xs value let type ← inferType value addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value } diff --git a/tests/lean/run/letrecInProofs.lean b/tests/lean/run/letrecInProofs.lean index 853b9f821a0e..8f8c0aa92e94 100644 --- a/tests/lean/run/letrecInProofs.lean +++ b/tests/lean/run/letrecInProofs.lean @@ -19,7 +19,7 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by have ihl : x ≮ l → node s x ≠ l ∧ node s x ≮ l := right x s l have ihr : x ≮ r → node s x ≠ r ∧ node s x ≮ r := right x s r have hl : x ≠ l ∧ x ≮ l := h.1 - have hr : x ≠ r ∧ x ≮ r := h.2.1 + have hr : x ≠ r ∧ x ≮ r := h.2 have ihl : node s x ≠ l ∧ node s x ≮ l := ihl hl.2 have ihr : node s x ≠ r ∧ node s x ≮ r := ihr hr.2 apply And.intro @@ -31,7 +31,6 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by focus apply And.intro apply ihl - apply And.intro _ trivial apply ihr let rec left (x t : Tree) (b : Tree) (h : x ≮ b) : node x t ≠ b ∧ node x t ≮ b := by match b, h with @@ -42,7 +41,7 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by have ihl : x ≮ l → node x t ≠ l ∧ node x t ≮ l := left x t l have ihr : x ≮ r → node x t ≠ r ∧ node x t ≮ r := left x t r have hl : x ≠ l ∧ x ≮ l := h.1 - have hr : x ≠ r ∧ x ≮ r := h.2.1 + have hr : x ≠ r ∧ x ≮ r := h.2 have ihl : node x t ≠ l ∧ node x t ≮ l := ihl hl.2 have ihr : node x t ≠ r ∧ node x t ≮ r := ihr hr.2 apply And.intro @@ -54,19 +53,17 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by focus apply And.intro apply ihl - apply And.intro _ trivial apply ihr let rec aux : (x : Tree) → x ≮ x | leaf => trivial | node l r => by have ih₁ : l ≮ l := aux l have ih₂ : r ≮ r := aux r - show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r) ∧ True + show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r) apply And.intro focus apply left assumption - apply And.intro _ trivial focus apply right assumption @@ -78,7 +75,7 @@ open Tree theorem ex1 (x : Tree) : x ≠ node leaf (node x leaf) := by intro h - exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.2.1.1 + exact absurd rfl $ Tree.acyclic _ _ h |>.2.2.1.1 theorem ex2 (x : Tree) : x ≠ node x leaf := by intro h @@ -86,4 +83,4 @@ theorem ex2 (x : Tree) : x ≠ node x leaf := by theorem ex3 (x y : Tree) : x ≠ node y x := by intro h - exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.1 + exact absurd rfl $ Tree.acyclic _ _ h |>.2.1 diff --git a/tests/lean/run/nestedInductiveConstructions.lean b/tests/lean/run/nestedInductiveConstructions.lean index 6b51c1067ea3..e1d1ab8c4197 100644 --- a/tests/lean/run/nestedInductiveConstructions.lean +++ b/tests/lean/run/nestedInductiveConstructions.lean @@ -12,11 +12,10 @@ inductive Tree where | node : List Tree → Tree info: @[reducible] protected def Ex1.Tree.below.{u} : {motive_1 : Tree → Sort u} → {motive_2 : List.{0} Tree → Sort u} → Tree → Sort (max 1 u) := fun {motive_1} {motive_2} t => - Tree.rec.{(max 1 u) + 1} - (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u} + Tree.rec.{(max 1 u) + 1} (fun a a_ih => PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u} (fun head tail head_ih tail_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u})) + (PProd.{u, max 1 u} (motive_2 tail) tail_ih)) t -/ #guard_msgs in @@ -26,11 +25,10 @@ fun {motive_1} {motive_2} t => info: @[reducible] protected def Ex1.Tree.below_1.{u} : {motive_1 : Tree → Sort u} → {motive_2 : List.{0} Tree → Sort u} → List.{0} Tree → Sort (max 1 u) := fun {motive_1} {motive_2} t => - Tree.rec_1.{(max 1 u) + 1} - (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u} + Tree.rec_1.{(max 1 u) + 1} (fun a a_ih => PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u} (fun head tail head_ih tail_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u})) + (PProd.{u, max 1 u} (motive_2 tail) tail_ih)) t -/ #guard_msgs in @@ -40,8 +38,8 @@ fun {motive_1} {motive_2} t => info: @[reducible] protected def Ex1.Tree.ibelow_1 : {motive_1 : Tree → Prop} → {motive_2 : List.{0} Tree → Prop} → List.{0} Tree → Prop := fun {motive_1} {motive_2} t => - Tree.rec_1.{1} (fun a a_ih => And (And (motive_2 a) a_ih) True) True - (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (And (motive_2 tail) tail_ih) True)) t + Tree.rec_1.{1} (fun a a_ih => And (motive_2 a) a_ih) True + (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (motive_2 tail) tail_ih)) t -/ #guard_msgs in #print Tree.ibelow_1 @@ -82,16 +80,15 @@ info: @[reducible] protected def Ex2.Tree.below.{u} : {motive_1 : Tree → Sort fun {motive_1} {motive_2} {motive_3} t => Tree.rec.{(max 1 u) + 1} (fun a a_1 a_ih a_ih_1 => - PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u})) + PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1)) PUnit.{max 1 u} (fun head tail head_ih tail_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u})) + (PProd.{u, max 1 u} (motive_2 tail) tail_ih)) PUnit.{max 1 u} (fun head tail head_ih tail_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u})) + (PProd.{u, max 1 u} (motive_3 tail) tail_ih)) t -/ #guard_msgs in @@ -104,16 +101,15 @@ info: @[reducible] protected def Ex2.Tree.below_1.{u} : {motive_1 : Tree → Sor fun {motive_1} {motive_2} {motive_3} t => Tree.rec_1.{(max 1 u) + 1} (fun a a_1 a_ih a_ih_1 => - PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u})) + PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1)) PUnit.{max 1 u} (fun head tail head_ih tail_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u})) + (PProd.{u, max 1 u} (motive_2 tail) tail_ih)) PUnit.{max 1 u} (fun head tail head_ih tail_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u})) + (PProd.{u, max 1 u} (motive_3 tail) tail_ih)) t -/ #guard_msgs in @@ -126,16 +122,15 @@ info: @[reducible] protected def Ex2.Tree.below_2.{u} : {motive_1 : Tree → Sor fun {motive_1} {motive_2} {motive_3} t => Tree.rec_2.{(max 1 u) + 1} (fun a a_1 a_ih a_ih_1 => - PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u})) + PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1)) PUnit.{max 1 u} (fun head tail head_ih tail_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u})) + (PProd.{u, max 1 u} (motive_2 tail) tail_ih)) PUnit.{max 1 u} (fun head tail head_ih tail_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih) - (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u})) + (PProd.{u, max 1 u} (motive_3 tail) tail_ih)) t -/ #guard_msgs in @@ -169,12 +164,10 @@ inductive Tree : Type u where | node : List Tree → Tree info: @[reducible] protected def Ex3.Tree.below.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} → {motive_2 : List.{u} Tree.{u} → Sort u_1} → Tree.{u} → Sort (max 1 u_1) := fun {motive_1} {motive_2} t => - Tree.rec.{(max 1 u_1) + 1, u} - (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}) - PUnit.{max 1 u_1} + Tree.rec.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1} (fun head tail head_ih tail_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih) - (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1})) + (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih)) t -/ #guard_msgs in @@ -184,12 +177,10 @@ fun {motive_1} {motive_2} t => info: @[reducible] protected def Ex3.Tree.below_1.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} → {motive_2 : List.{u} Tree.{u} → Sort u_1} → List.{u} Tree.{u} → Sort (max 1 u_1) := fun {motive_1} {motive_2} t => - Tree.rec_1.{(max 1 u_1) + 1, u} - (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}) - PUnit.{max 1 u_1} + Tree.rec_1.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1} (fun head tail head_ih tail_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih) - (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1})) + (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih)) t -/ #guard_msgs in diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out index c33c68f746c4..7408d3dcc9a7 100644 --- a/tests/lean/unusedLet.lean.expected.out +++ b/tests/lean/unusedLet.lean.expected.out @@ -8,5 +8,5 @@ fun x => | 0 => fun x => 1 | n.succ => fun x => let y := 42; - 2 * x.fst.fst) + 2 * x.1.1) f From 92cca5ed1b577a7bc7f73c5f6cd9a97040c80f76 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 22 Jul 2024 15:39:00 +0100 Subject: [PATCH 2/6] chore: remove bif from hash map lemmas (#4791) The original idea was to use `bif` in computation contexts and `if` in propositional contexts, but this turned out to be really inconvenient in practice. --- .../DHashMap/Internal/List/Associative.lean | 116 +++++++++--------- src/Std/Data/DHashMap/Internal/RawLemmas.lean | 30 ++--- src/Std/Data/DHashMap/Internal/WF.lean | 3 +- src/Std/Data/DHashMap/Lemmas.lean | 39 +++--- src/Std/Data/DHashMap/RawLemmas.lean | 36 +++--- src/Std/Data/HashMap/Lemmas.lean | 24 ++-- src/Std/Data/HashMap/RawLemmas.lean | 24 ++-- src/Std/Data/HashSet/Lemmas.lean | 4 +- src/Std/Data/HashSet/RawLemmas.lean | 4 +- 9 files changed, 146 insertions(+), 134 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean index 4b6e4eb4479a..0f7b29d5cf55 100644 --- a/src/Std/Data/DHashMap/Internal/List/Associative.lean +++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean @@ -579,7 +579,7 @@ theorem getEntry?_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ( theorem getEntry?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} : - getEntry? a (replaceEntry k v l) = bif containsKey k l && k == a then some ⟨k, v⟩ else + getEntry? a (replaceEntry k v l) = if containsKey k l ∧ k == a then some ⟨k, v⟩ else getEntry? a l := by cases hl : containsKey k l · simp [getEntry?_replaceEntry_of_containsKey_eq_false hl] @@ -632,13 +632,11 @@ theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α) @[simp] theorem containsKey_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} : containsKey a (replaceEntry k v l) = containsKey a l := by - cases h : containsKey k l && k == a - · rw [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, cond_false, - containsKey_eq_isSome_getEntry?] - · rw [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, cond_true, Option.isSome_some, - Eq.comm] - rw [Bool.and_eq_true] at h - exact containsKey_of_beq h.1 h.2 + by_cases h : (getEntry? k l).isSome ∧ k == a + · simp only [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h, and_self, ↓reduceIte, + Option.isSome_some, Bool.true_eq] + rw [← getEntry?_congr h.2, h.1] + · simp [containsKey_eq_isSome_getEntry?, getEntry?_replaceEntry, h] /-- Internal implementation detail of the hash map -/ def eraseKey [BEq α] (k : α) : List ((a : α) × β a) → List ((a : α) × β a) @@ -681,7 +679,7 @@ theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} : · simpa using Sublist.cons_right Sublist.refl theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} : - (eraseKey k l).length = bif containsKey k l then l.length - 1 else l.length := by + (eraseKey k l).length = if containsKey k l then l.length - 1 else l.length := by induction l using assoc_induction · simp · next k' v' t ih => @@ -690,7 +688,7 @@ theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} : · rw [cond_false, Bool.false_or, List.length_cons, ih] cases h : containsKey k t · simp - · simp only [cond_true, Nat.succ_eq_add_one, List.length_cons, Nat.add_sub_cancel] + · simp only [Nat.succ_eq_add_one, List.length_cons, Nat.add_sub_cancel, if_true] rw [Nat.sub_add_cancel] cases t · simp at h @@ -855,7 +853,7 @@ theorem isEmpty_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : · rw [insertEntry_of_containsKey h, isEmpty_replaceEntry, isEmpty_eq_false_of_containsKey h] theorem length_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : - (insertEntry k v l).length = bif containsKey k l then l.length else l.length + 1 := by + (insertEntry k v l).length = if containsKey k l then l.length else l.length + 1 := by simp [insertEntry, Bool.apply_cond List.length] theorem length_le_length_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : @@ -886,23 +884,23 @@ theorem getValue?_insertEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ( · rw [insertEntry_of_containsKey h', getValue?_replaceEntry_of_false h] theorem getValue?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} - {v : β} : getValue? a (insertEntry k v l) = bif k == a then some v else getValue? a l := by + {v : β} : getValue? a (insertEntry k v l) = if k == a then some v else getValue? a l := by cases h : k == a · simp [getValue?_insertEntry_of_false h, h] · simp [getValue?_insertEntry_of_beq h, h] theorem getValue?_insertEntry_self [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β} : getValue? k (insertEntry k v l) = some v := by - rw [getValue?_insertEntry, Bool.cond_pos BEq.refl] + simp [getValue?_insertEntry] end theorem getEntry?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : - getEntry? a (insertEntry k v l) = bif k == a then some ⟨k, v⟩ else getEntry? a l := by + getEntry? a (insertEntry k v l) = if k == a then some ⟨k, v⟩ else getEntry? a l := by cases hl : containsKey k l - · rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons] - · rw [insertEntry_of_containsKey hl, getEntry?_replaceEntry, hl, Bool.true_and, BEq.comm] + · rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons, cond_eq_if] + · simp [insertEntry_of_containsKey hl, getEntry?_replaceEntry, hl] theorem getValueCast?_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : getValueCast? a (insertEntry k v l) = @@ -938,21 +936,21 @@ theorem getValueCastD_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : theorem getValue!_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} {v : β} : - getValue! a (insertEntry k v l) = bif k == a then v else getValue! a l := by - simp [getValue!_eq_getValue?, getValue?_insertEntry, Bool.apply_cond Option.get!] + getValue! a (insertEntry k v l) = if k == a then v else getValue! a l := by + simp [getValue!_eq_getValue?, getValue?_insertEntry, apply_ite Option.get!] theorem getValue!_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k : α} {v : β} : getValue! k (insertEntry k v l) = v := by - rw [getValue!_insertEntry, BEq.refl, cond_true] + simp [getValue!_insertEntry, BEq.refl] theorem getValueD_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback v : β} : getValueD a (insertEntry k v l) fallback = - bif k == a then v else getValueD a l fallback := by - simp [getValueD_eq_getValue?, getValue?_insertEntry, Bool.apply_cond (fun x => Option.getD x fallback)] + if k == a then v else getValueD a l fallback := by + simp [getValueD_eq_getValue?, getValue?_insertEntry, apply_ite (fun x => Option.getD x fallback)] theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback v : β} : getValueD k (insertEntry k v l) fallback = v := by - rw [getValueD_insertEntry, BEq.refl, cond_true] + simp [getValueD_insertEntry, BEq.refl] @[simp] theorem containsKey_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} @@ -991,7 +989,7 @@ theorem getValue_insertEntry {β : Type v} [BEq α] [PartialEquivBEq α] {l : Li if h' : k == a then v else getValue a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h')) := by rw [← Option.some_inj, ← getValue?_eq_some_getValue, apply_dite Option.some, - getValue?_insertEntry, cond_eq_if, ← dite_eq_ite] + getValue?_insertEntry, ← dite_eq_ite] simp only [← getValue?_eq_some_getValue] theorem getValue_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} @@ -1020,7 +1018,7 @@ theorem isEmpty_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} theorem getEntry?_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : getEntry? a (insertEntryIfNew k v l) = - bif k == a && !containsKey k l then some ⟨k, v⟩ else getEntry? a l := by + if k == a && !containsKey k l then some ⟨k, v⟩ else getEntry? a l := by cases h : containsKey k l · simp [insertEntryIfNew_of_containsKey_eq_false h, getEntry?_cons] · simp [insertEntryIfNew_of_containsKey h] @@ -1036,18 +1034,22 @@ theorem getValueCast?_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : theorem getValue?_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue? a (insertEntryIfNew k v l) = - bif k == a && !containsKey k l then some v else getValue? a l := by + if k == a ∧ containsKey k l = false then some v else getValue? a l := by simp [getValue?_eq_getEntry?, getEntry?_insertEntryIfNew, - Bool.apply_cond (Option.map (fun (y : ((_ : α) × β)) => y.2))] + apply_ite (Option.map (fun (y : ((_ : α) × β)) => y.2))] theorem containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : containsKey a (insertEntryIfNew k v l) = ((k == a) || containsKey a l) := by - simp only [containsKey_eq_isSome_getEntry?, getEntry?_insertEntryIfNew, Bool.apply_cond Option.isSome, - Option.isSome_some, Bool.cond_true_left] + simp only [containsKey_eq_isSome_getEntry?, getEntry?_insertEntryIfNew, apply_ite Option.isSome, + Option.isSome_some, if_true_left] + simp only [Bool.and_eq_true, Bool.not_eq_true', Option.not_isSome, Option.isNone_iff_eq_none, + getEntry?_eq_none, Bool.if_true_left, Bool.decide_and, Bool.decide_eq_true, + Bool.decide_eq_false] cases h : k == a · simp - · rw [Bool.true_and, Bool.true_or, getEntry?_congr h, Bool.not_or_self] + · rw [containsKey_eq_isSome_getEntry?, getEntry?_congr h] + simp theorem containsKey_insertEntryIfNew_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : containsKey k (insertEntryIfNew k v l) := by @@ -1085,7 +1087,7 @@ theorem getValue_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l if h' : k == a ∧ containsKey k l = false then v else getValue a l (containsKey_of_containsKey_insertEntryIfNew' h h') := by rw [← Option.some_inj, ← getValue?_eq_some_getValue, apply_dite Option.some, - getValue?_insertEntryIfNew, cond_eq_if, ← dite_eq_ite] + getValue?_insertEntryIfNew, ← dite_eq_ite] simp [← getValue?_eq_some_getValue] theorem getValueCast!_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} @@ -1096,8 +1098,8 @@ theorem getValueCast!_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : theorem getValue!_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} {v : β} : getValue! a (insertEntryIfNew k v l) = - bif k == a && !containsKey k l then v else getValue! a l := by - simp [getValue!_eq_getValue?, getValue?_insertEntryIfNew, Bool.apply_cond Option.get!] + if k == a ∧ containsKey k l = false then v else getValue! a l := by + simp [getValue!_eq_getValue?, getValue?_insertEntryIfNew, apply_ite Option.get!] theorem getValueCastD_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} {fallback : β a} : getValueCastD a (insertEntryIfNew k v l) fallback = @@ -1108,12 +1110,12 @@ theorem getValueCastD_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : theorem getValueD_insertEntryIfNew {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback v : β} : getValueD a (insertEntryIfNew k v l) fallback = - bif k == a && !containsKey k l then v else getValueD a l fallback := by + if k == a ∧ containsKey k l = false then v else getValueD a l fallback := by simp [getValueD_eq_getValue?, getValue?_insertEntryIfNew, - Bool.apply_cond (fun x => Option.getD x fallback)] + apply_ite (fun x => Option.getD x fallback)] theorem length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : - (insertEntryIfNew k v l).length = bif containsKey k l then l.length else l.length + 1 := by + (insertEntryIfNew k v l).length = if containsKey k l then l.length else l.length + 1 := by simp [insertEntryIfNew, Bool.apply_cond List.length] theorem length_le_length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : @@ -1169,7 +1171,7 @@ theorem getEntry?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((a theorem getEntry?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : - getEntry? a (eraseKey k l) = bif k == a then none else getEntry? a l := by + getEntry? a (eraseKey k l) = if k == a then none else getEntry? a l := by cases h : k == a · simp [getEntry?_eraseKey_of_false h, h] · simp [getEntry?_eraseKey_of_beq hl h, h] @@ -1222,8 +1224,8 @@ theorem getValue?_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ theorem getValue?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) : - getValue? a (eraseKey k l) = bif k == a then none else getValue? a l := by - simp [getValue?_eq_getEntry?, getEntry?_eraseKey hl, Bool.apply_cond (Option.map _)] + getValue? a (eraseKey k l) = if k == a then none else getValue? a l := by + simp [getValue?_eq_getEntry?, getEntry?_eraseKey hl, apply_ite (Option.map _)] end @@ -1241,25 +1243,25 @@ theorem containsKey_eraseKey_of_false [BEq α] [PartialEquivBEq α] {l : List (( theorem containsKey_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : containsKey a (eraseKey k l) = (!(k == a) && containsKey a l) := by - simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey hl, Bool.apply_cond] + simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey hl, apply_ite] theorem getValueCast?_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} (hl : DistinctKeys l) : - getValueCast? a (eraseKey k l) = bif k == a then none else getValueCast? a l := by + getValueCast? a (eraseKey k l) = if k == a then none else getValueCast? a l := by rw [getValueCast?_eq_getEntry?, Option.dmap_congr (getEntry?_eraseKey hl)] - rcases Bool.eq_false_or_eq_true (k == a) with h|h - · rw [Option.dmap_congr (Bool.cond_pos h), Option.dmap_none, Bool.cond_pos h] - · rw [Option.dmap_congr (Bool.cond_neg h), getValueCast?_eq_getEntry?] - exact (Bool.cond_neg h).symm + by_cases h : k == a + · rw [Option.dmap_congr (if_pos h), Option.dmap_none, if_pos h] + · rw [Option.dmap_congr (if_neg h), getValueCast?_eq_getEntry?] + exact (if_neg h).symm theorem getValueCast?_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) : getValueCast? k (eraseKey k l) = none := by - rw [getValueCast?_eraseKey hl, Bool.cond_pos BEq.refl] + rw [getValueCast?_eraseKey hl, if_pos BEq.refl] theorem getValueCast!_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} [Inhabited (β a)] (hl : DistinctKeys l) : - getValueCast! a (eraseKey k l) = bif k == a then default else getValueCast! a l := by - simp [getValueCast!_eq_getValueCast?, getValueCast?_eraseKey hl, Bool.apply_cond Option.get!] + getValueCast! a (eraseKey k l) = if k == a then default else getValueCast! a l := by + simp [getValueCast!_eq_getValueCast?, getValueCast?_eraseKey hl, apply_ite Option.get!] theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (hl : DistinctKeys l) : getValueCast! k (eraseKey k l) = default := by @@ -1267,9 +1269,9 @@ theorem getValueCast!_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) theorem getValueCastD_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {fallback : β a} (hl : DistinctKeys l) : getValueCastD a (eraseKey k l) fallback = - bif k == a then fallback else getValueCastD a l fallback := by + if k == a then fallback else getValueCastD a l fallback := by simp [getValueCastD_eq_getValueCast?, getValueCast?_eraseKey hl, - Bool.apply_cond (fun x => Option.getD x fallback)] + apply_ite (fun x => Option.getD x fallback)] theorem getValueCastD_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (hl : DistinctKeys l) : @@ -1278,8 +1280,8 @@ theorem getValueCastD_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) theorem getValue!_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) : - getValue! a (eraseKey k l) = bif k == a then default else getValue! a l := by - simp [getValue!_eq_getValue?, getValue?_eraseKey hl, Bool.apply_cond Option.get!] + getValue! a (eraseKey k l) = if k == a then default else getValue! a l := by + simp [getValue!_eq_getValue?, getValue?_eraseKey hl, apply_ite Option.get!] theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β] {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) : @@ -1288,8 +1290,8 @@ theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inh theorem getValueD_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback : β} (hl : DistinctKeys l) : getValueD a (eraseKey k l) fallback = - bif k == a then fallback else getValueD a l fallback := by - simp [getValueD_eq_getValue?, getValue?_eraseKey hl, Bool.apply_cond (fun x => Option.getD x fallback)] + if k == a then fallback else getValueD a l fallback := by + simp [getValueD_eq_getValue?, getValue?_eraseKey hl, apply_ite (fun x => Option.getD x fallback)] theorem getValueD_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback : β} (hl : DistinctKeys l) : @@ -1304,15 +1306,15 @@ theorem getValueCast_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β (hl : DistinctKeys l) : getValueCast a (eraseKey k l) h = getValueCast a l (containsKey_of_containsKey_eraseKey hl h) := by rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h - rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, getValueCast?_eraseKey hl, h.1, - cond_false, ← getValueCast?_eq_some_getValueCast] + rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, getValueCast?_eraseKey hl, h.1] + simp [← getValueCast?_eq_some_getValueCast] theorem getValue_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {h} (hl : DistinctKeys l) : getValue a (eraseKey k l) h = getValue a l (containsKey_of_containsKey_eraseKey hl h) := by rw [containsKey_eraseKey hl, Bool.and_eq_true, Bool.not_eq_true'] at h - rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_eraseKey hl, h.1, cond_false, - ← getValue?_eq_some_getValue] + rw [← Option.some_inj, ← getValue?_eq_some_getValue, getValue?_eraseKey hl, h.1] + simp [← getValue?_eq_some_getValue] theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} (hl : DistinctKeys l) (h : Perm l l') : getEntry? a l = getEntry? a l' := by diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index a6e2b90df1e5..585326596508 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -145,7 +145,7 @@ theorem isEmpty_eq_size_eq_zero : m.1.isEmpty = (m.1.size == 0) := by simp [Raw.isEmpty] theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : - (m.insert k v).1.size = bif m.contains k then m.1.size else m.1.size + 1 := by + (m.insert k v).1.size = if m.contains k then m.1.size else m.1.size + 1 := by simp_to_model using List.length_insertEntry theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : @@ -169,7 +169,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} simp_to_model using List.containsKey_of_containsKey_eraseKey theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} : - (m.erase k).1.size = bif m.contains k then m.1.size - 1 else m.1.size := by + (m.erase k).1.size = if m.contains k then m.1.size - 1 else m.1.size := by simp_to_model using List.length_eraseKey theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : @@ -215,7 +215,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : m.contains a = false → m.get? a simp_to_model using List.getValueCast?_eq_none theorem get?_erase [LawfulBEq α] {k a : α} : - (m.erase k).get? a = bif k == a then none else m.get? a := by + (m.erase k).get? a = if k == a then none else m.get? a := by simp_to_model using List.getValueCast?_eraseKey theorem get?_erase_self [LawfulBEq α] {k : α} : (m.erase k).get? k = none := by @@ -234,7 +234,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : simp_to_model; empty theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - get? (m.insert k v) a = bif k == a then some v else get? m a := by + get? (m.insert k v) a = if k == a then some v else get? m a := by simp_to_model using List.getValue?_insertEntry theorem get?_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : @@ -250,7 +250,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : simp_to_model using List.getValue?_eq_none.2 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : - Const.get? (m.erase k) a = bif k == a then none else get? m a := by + Const.get? (m.erase k) a = if k == a then none else get? m a := by simp_to_model using List.getValue?_eraseKey theorem get?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : @@ -340,7 +340,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] : simp_to_model using List.getValueCast!_eq_default theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] : - (m.erase k).get! a = bif k == a then default else m.get! a := by + (m.erase k).get! a = if k == a then default else m.get! a := by simp_to_model using List.getValueCast!_eraseKey theorem get!_erase_self [LawfulBEq α] {k : α} [Inhabited (β k)] : @@ -372,7 +372,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α simp_to_model; empty theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - get! (m.insert k v) a = bif k == a then v else get! m a := by + get! (m.insert k v) a = if k == a then v else get! m a := by simp_to_model using List.getValue!_insertEntry theorem get!_insert_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} {v : β} : @@ -384,7 +384,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α simp_to_model using List.getValue!_eq_default theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : - get! (m.erase k) a = bif k == a then default else get! m a := by + get! (m.erase k) a = if k == a then default else get! m a := by simp_to_model using List.getValue!_eraseKey theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} : @@ -435,7 +435,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} : simp_to_model using List.getValueCastD_eq_fallback theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} : - (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by + (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by simp_to_model using List.getValueCastD_eraseKey theorem getD_erase_self [LawfulBEq α] {k : α} {fallback : β k} : @@ -471,7 +471,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : simp_to_model; empty theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : - getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by + getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := by simp_to_model using List.getValueD_insertEntry theorem getD_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback v : β} : @@ -483,7 +483,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : simp_to_model using List.getValueD_eq_fallback theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : - getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by + getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by simp_to_model using List.getValueD_eraseKey theorem getD_erase_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : @@ -539,7 +539,7 @@ theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a simp_to_model using List.containsKey_of_containsKey_insertEntryIfNew' theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : - (m.insertIfNew k v).1.size = bif m.contains k then m.1.size else m.1.size + 1 := by + (m.insertIfNew k v).1.size = if m.contains k then m.1.size else m.1.size + 1 := by simp_to_model using List.length_insertEntryIfNew theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : @@ -575,7 +575,7 @@ namespace Const variable {β : Type v} (m : Raw₀ α (fun _ => β)) (h : m.1.WF) theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by + get? (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then some v else get? m a := by simp_to_model using List.getValue?_insertEntryIfNew theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} : @@ -585,12 +585,12 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h simp_to_model using List.getValue_insertEntryIfNew theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by + get! (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then v else get! m a := by simp_to_model using List.getValue!_insertEntryIfNew theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : getD (m.insertIfNew k v) a fallback = - bif k == a && !m.contains k then v else getD m a fallback := by + if k == a ∧ m.contains k = false then v else getD m a fallback := by simp_to_model using List.getValueD_insertEntryIfNew end Const diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 665871db313f..84e3dfac515c 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -472,7 +472,8 @@ theorem wfImp_eraseₘaux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable buckets_hash_self := isHashSelf_eraseₘaux m a h size_eq := by rw [(toListModel_eraseₘaux m a h).length_eq, eraseₘaux, length_eraseKey, - ← containsₘ_eq_containsKey h, h', cond_true, h.size_eq] + ← containsₘ_eq_containsKey h, h'] + simp [h.size_eq] distinct := h.distinct.eraseKey.perm (toListModel_eraseₘaux m a h) theorem toListModel_perm_eraseKey_of_containsₘ_eq_false [BEq α] [Hashable α] [EquivBEq α] diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index cf7661d8a083..f67c4c0e5ef3 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -102,7 +102,7 @@ theorem size_emptyc : (∅ : DHashMap α β).size = 0 := theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := rfl theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : - (m.insert k v).size = bif m.contains k then m.size else m.size + 1 := + (m.insert k v).size = if k ∈ m then m.size else m.size + 1 := Raw₀.size_insert ⟨m.1, _⟩ m.2 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : @@ -140,7 +140,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m. simp theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} : - (m.erase k).size = bif m.contains k then m.size - 1 else m.size := + (m.erase k).size = if k ∈ m then m.size - 1 else m.size := Raw₀.size_erase _ m.2 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := @@ -194,7 +194,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none := simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false theorem get?_erase [LawfulBEq α] {k a : α} : - (m.erase k).get? a = bif k == a then none else m.get? a := + (m.erase k).get? a = if k == a then none else m.get? a := Raw₀.get?_erase ⟨m.1, _⟩ m.2 @[simp] @@ -218,7 +218,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : Raw₀.Const.get?_of_isEmpty ⟨m.1, _⟩ m.2 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - get? (m.insert k v) a = bif k == a then some v else get? m a := + get? (m.insert k v) a = if k == a then some v else get? m a := Raw₀.Const.get?_insert ⟨m.1, _⟩ m.2 @[simp] @@ -238,7 +238,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α } : ¬a ∈ m → simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : - Const.get? (m.erase k) a = bif k == a then none else get? m a := + Const.get? (m.erase k) a = if k == a then none else get? m a := Raw₀.Const.get?_erase ⟨m.1, _⟩ m.2 @[simp] @@ -339,7 +339,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] : simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] : - (m.erase k).get! a = bif k == a then default else m.get! a := + (m.erase k).get! a = if k == a then default else m.get! a := Raw₀.get!_erase ⟨m.1, _⟩ m.2 @[simp] @@ -381,7 +381,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α Raw₀.Const.get!_of_isEmpty ⟨m.1, _⟩ m.2 theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - get! (m.insert k v) a = bif k == a then v else get! m a := + get! (m.insert k v) a = if k == a then v else get! m a := Raw₀.Const.get!_insert ⟨m.1, _⟩ m.2 @[simp] @@ -398,7 +398,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : - get! (m.erase k) a = bif k == a then default else get! m a := + get! (m.erase k) a = if k == a then default else get! m a := Raw₀.Const.get!_erase ⟨m.1, _⟩ m.2 @[simp] @@ -465,7 +465,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} : simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} : - (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := + (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := Raw₀.getD_erase ⟨m.1, _⟩ m.2 @[simp] @@ -512,7 +512,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : Raw₀.Const.getD_of_isEmpty ⟨m.1, _⟩ m.2 theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : - getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := + getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := Raw₀.Const.getD_insert ⟨m.1, _⟩ m.2 @[simp] @@ -529,7 +529,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : - getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := + getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := Raw₀.Const.getD_erase ⟨m.1, _⟩ m.2 @[simp] @@ -611,7 +611,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v simpa [mem_iff_contains, -contains_insertIfNew] using contains_of_contains_insertIfNew' theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : - (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 := + (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 := Raw₀.size_insertIfNew ⟨m.1, _⟩ m.2 theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : @@ -647,8 +647,9 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := - Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2 + get? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some v else get? m a := by + simp only [mem_iff_contains, Bool.not_eq_true] + exact Raw₀.Const.get?_insertIfNew ⟨m.1, _⟩ m.2 theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} : get (m.insertIfNew k v) a h₁ = @@ -657,13 +658,15 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h exact Raw₀.Const.get_insertIfNew ⟨m.1, _⟩ m.2 theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := - Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2 + get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a := by + simp only [mem_iff_contains, Bool.not_eq_true] + exact Raw₀.Const.get!_insertIfNew ⟨m.1, _⟩ m.2 theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : getD (m.insertIfNew k v) a fallback = - bif k == a && !m.contains k then v else getD m a fallback := - Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2 + if k == a ∧ ¬k ∈ m then v else getD m a fallback := by + simp only [mem_iff_contains, Bool.not_eq_true] + exact Raw₀.Const.getD_insertIfNew ⟨m.1, _⟩ m.2 end Const diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index ec60c166a93c..9487f4749c6f 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -150,7 +150,8 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by simp [isEmpty] theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : - (m.insert k v).size = bif m.contains k then m.size else m.size + 1 := by + (m.insert k v).size = if k ∈ m then m.size else m.size + 1 := by + simp only [mem_iff_contains] simp_to_raw using Raw₀.size_insert theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : @@ -189,7 +190,8 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m. simpa [mem_iff_contains] using contains_of_contains_erase h theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} : - (m.erase k).size = bif m.contains k then m.size - 1 else m.size := by + (m.erase k).size = if k ∈ m then m.size - 1 else m.size := by + simp only [mem_iff_contains] simp_to_raw using Raw₀.size_erase theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := by @@ -243,7 +245,7 @@ theorem get?_eq_none [LawfulBEq α] {a : α} : ¬a ∈ m → m.get? a = none := simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h theorem get?_erase [LawfulBEq α] {k a : α} : - (m.erase k).get? a = bif k == a then none else m.get? a := by + (m.erase k).get? a = if k == a then none else m.get? a := by simp_to_raw using Raw₀.get?_erase @[simp] @@ -267,7 +269,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : simp_to_raw using Raw₀.Const.get?_of_isEmpty ⟨m, _⟩ theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - get? (m.insert k v) a = bif k == a then some v else get? m a := by + get? (m.insert k v) a = if k == a then some v else get? m a := by simp_to_raw using Raw₀.Const.get?_insert @[simp] @@ -287,7 +289,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : - Const.get? (m.erase k) a = bif k == a then none else get? m a := by + Const.get? (m.erase k) a = if k == a then none else get? m a := by simp_to_raw using Raw₀.Const.get?_erase @[simp] @@ -388,7 +390,7 @@ theorem get!_eq_default [LawfulBEq α] {a : α} [Inhabited (β a)] : simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h theorem get!_erase [LawfulBEq α] {k a : α} [Inhabited (β a)] : - (m.erase k).get! a = bif k == a then default else m.get! a := by + (m.erase k).get! a = if k == a then default else m.get! a := by simp_to_raw using Raw₀.get!_erase @[simp] @@ -429,7 +431,7 @@ theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α simp_to_raw using Raw₀.Const.get!_of_isEmpty ⟨m, _⟩ theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - get! (m.insert k v) a = bif k == a then v else get! m a := by + get! (m.insert k v) a = if k == a then v else get! m a := by simp_to_raw using Raw₀.Const.get!_insert @[simp] @@ -446,7 +448,7 @@ theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h theorem get!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : - get! (m.erase k) a = bif k == a then default else get! m a := by + get! (m.erase k) a = if k == a then default else get! m a := by simp_to_raw using Raw₀.Const.get!_erase @[simp] @@ -513,7 +515,7 @@ theorem getD_eq_fallback [LawfulBEq α] {a : α} {fallback : β a} : simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h theorem getD_erase [LawfulBEq α] {k a : α} {fallback : β a} : - (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := by + (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := by simp_to_raw using Raw₀.getD_erase @[simp] @@ -559,7 +561,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : simp_to_raw using Raw₀.Const.getD_of_isEmpty ⟨m, _⟩ theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : - getD (m.insert k v) a fallback = bif k == a then v else getD m a fallback := by + getD (m.insert k v) a fallback = if k == a then v else getD m a fallback := by simp_to_raw using Raw₀.Const.getD_insert @[simp] @@ -576,7 +578,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : simpa [mem_iff_contains] using getD_eq_fallback_of_contains_eq_false h theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : - getD (m.erase k) a fallback = bif k == a then fallback else getD m a fallback := by + getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback := by simp_to_raw using Raw₀.Const.getD_erase @[simp] @@ -658,7 +660,8 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v simpa [mem_iff_contains] using contains_of_contains_insertIfNew' h theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : - (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 := by + (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 := by + simp only [mem_iff_contains] simp_to_raw using Raw₀.size_insertIfNew theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : @@ -697,7 +700,8 @@ namespace Const variable {β : Type v} {m : DHashMap.Raw α (fun _ => β)} (h : m.WF) theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - get? (m.insertIfNew k v) a = bif k == a && !m.contains k then some v else get? m a := by + get? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some v else get? m a := by + simp only [mem_iff_contains, Bool.not_eq_true] simp_to_raw using Raw₀.Const.get?_insertIfNew theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} : @@ -708,12 +712,14 @@ theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h simp_to_raw using Raw₀.Const.get_insertIfNew ⟨m, _⟩ theorem get!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - get! (m.insertIfNew k v) a = bif k == a && !m.contains k then v else get! m a := by + get! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then v else get! m a := by + simp only [mem_iff_contains, Bool.not_eq_true] simp_to_raw using Raw₀.Const.get!_insertIfNew theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : getD (m.insertIfNew k v) a fallback = - bif k == a && !m.contains k then v else getD m a fallback := by + if k == a ∧ ¬k ∈ m then v else getD m a fallback := by + simp only [mem_iff_contains, Bool.not_eq_true] simp_to_raw using Raw₀.Const.getD_insertIfNew end Const diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index b271c7926321..88bd978a199f 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -110,7 +110,7 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := DHashMap.isEmpty_eq_size_eq_zero theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : - (m.insert k v).size = bif m.contains k then m.size else m.size + 1 := + (m.insert k v).size = if k ∈ m then m.size else m.size + 1 := DHashMap.size_insert theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : @@ -148,7 +148,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m. DHashMap.mem_of_mem_erase theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} : - (m.erase k).size = bif m.contains k then m.size - 1 else m.size := + (m.erase k).size = if k ∈ m then m.size - 1 else m.size := DHashMap.size_erase theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := @@ -185,7 +185,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : DHashMap.Const.get?_of_isEmpty theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - (m.insert k v)[a]? = bif k == a then some v else m[a]? := + (m.insert k v)[a]? = if k == a then some v else m[a]? := DHashMap.Const.get?_insert @[simp] @@ -205,7 +205,7 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m DHashMap.Const.get?_eq_none theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : - (m.erase k)[a]? = bif k == a then none else m[a]? := + (m.erase k)[a]? = if k == a then none else m[a]? := DHashMap.Const.get?_erase @[simp] @@ -251,7 +251,7 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a DHashMap.Const.get!_of_isEmpty theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - (m.insert k v)[a]! = bif k == a then v else m[a]! := + (m.insert k v)[a]! = if k == a then v else m[a]! := DHashMap.Const.get!_insert @[simp] @@ -268,7 +268,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a DHashMap.Const.get!_eq_default theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : - (m.erase k)[a]! = bif k == a then default else m[a]! := + (m.erase k)[a]! = if k == a then default else m[a]! := DHashMap.Const.get!_erase @[simp] @@ -310,7 +310,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : DHashMap.Const.getD_of_isEmpty theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : - (m.insert k v).getD a fallback = bif k == a then v else m.getD a fallback := + (m.insert k v).getD a fallback = if k == a then v else m.getD a fallback := DHashMap.Const.getD_insert @[simp] @@ -327,7 +327,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : DHashMap.Const.getD_eq_fallback theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : - (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := + (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := DHashMap.Const.getD_erase @[simp] @@ -403,7 +403,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v DHashMap.mem_of_mem_insertIfNew' theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : - (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 := + (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 := DHashMap.size_insertIfNew theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : @@ -411,7 +411,7 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : DHashMap.size_le_size_insertIfNew theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - (m.insertIfNew k v)[a]? = bif k == a && !m.contains k then some v else m[a]? := + (m.insertIfNew k v)[a]? = if k == a ∧ ¬k ∈ m then some v else m[a]? := DHashMap.Const.get?_insertIfNew theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} : @@ -420,12 +420,12 @@ theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β DHashMap.Const.get_insertIfNew (h₁ := h₁) theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - (m.insertIfNew k v)[a]! = bif k == a && !m.contains k then v else m[a]! := + (m.insertIfNew k v)[a]! = if k == a ∧ ¬k ∈ m then v else m[a]! := DHashMap.Const.get!_insertIfNew theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : (m.insertIfNew k v).getD a fallback = - bif k == a && !m.contains k then v else m.getD a fallback := + if k == a ∧ ¬k ∈ m then v else m.getD a fallback := DHashMap.Const.getD_insertIfNew @[simp] diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 96fea3069c9d..76a7adabd2cf 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -109,7 +109,7 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := DHashMap.Raw.isEmpty_eq_size_eq_zero theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : - (m.insert k v).size = bif m.contains k then m.size else m.size + 1 := + (m.insert k v).size = if k ∈ m then m.size else m.size + 1 := DHashMap.Raw.size_insert h.out theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : @@ -147,7 +147,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m. DHashMap.Raw.mem_of_mem_erase h.out theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} : - (m.erase k).size = bif m.contains k then m.size - 1 else m.size := + (m.erase k).size = if k ∈ m then m.size - 1 else m.size := DHashMap.Raw.size_erase h.out theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := @@ -184,7 +184,7 @@ theorem getElem?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} : DHashMap.Raw.Const.get?_of_isEmpty h.out theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - (m.insert k v)[a]? = bif k == a then some v else m[a]? := + (m.insert k v)[a]? = if k == a then some v else m[a]? := DHashMap.Raw.Const.get?_insert h.out @[simp] @@ -204,7 +204,7 @@ theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m DHashMap.Raw.Const.get?_eq_none h.out theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} : - (m.erase k)[a]? = bif k == a then none else m[a]? := + (m.erase k)[a]? = if k == a then none else m[a]? := DHashMap.Raw.Const.get?_erase h.out @[simp] @@ -250,7 +250,7 @@ theorem getElem!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a DHashMap.Raw.Const.get!_of_isEmpty h.out theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - (m.insert k v)[a]! = bif k == a then v else m[a]! := + (m.insert k v)[a]! = if k == a then v else m[a]! := DHashMap.Raw.Const.get!_insert h.out @[simp] @@ -267,7 +267,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a DHashMap.Raw.Const.get!_eq_default h.out theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} : - (m.erase k)[a]! = bif k == a then default else m[a]! := + (m.erase k)[a]! = if k == a then default else m[a]! := DHashMap.Raw.Const.get!_erase h.out @[simp] @@ -308,7 +308,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : DHashMap.Raw.Const.getD_of_isEmpty h.out theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : - (m.insert k v).getD a fallback = bif k == a then v else m.getD a fallback := + (m.insert k v).getD a fallback = if k == a then v else m.getD a fallback := DHashMap.Raw.Const.getD_insert h.out @[simp] @@ -325,7 +325,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback : DHashMap.Raw.Const.getD_eq_fallback h.out theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} : - (m.erase k).getD a fallback = bif k == a then fallback else m.getD a fallback := + (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback := DHashMap.Raw.Const.getD_erase h.out @[simp] @@ -401,7 +401,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v DHashMap.Raw.mem_of_mem_insertIfNew' h.out theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : - (m.insertIfNew k v).size = bif m.contains k then m.size else m.size + 1 := + (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 := DHashMap.Raw.size_insertIfNew h.out theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : @@ -409,7 +409,7 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : DHashMap.Raw.size_le_size_insertIfNew h.out theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} : - (m.insertIfNew k v)[a]? = bif k == a && !m.contains k then some v else m[a]? := + (m.insertIfNew k v)[a]? = if k == a ∧ ¬k ∈ m then some v else m[a]? := DHashMap.Raw.Const.get?_insertIfNew h.out theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} : @@ -418,12 +418,12 @@ theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β DHashMap.Raw.Const.get_insertIfNew h.out (h₁ := h₁) theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} : - (m.insertIfNew k v)[a]! = bif k == a && !m.contains k then v else m[a]! := + (m.insertIfNew k v)[a]! = if k == a ∧ ¬k ∈ m then v else m[a]! := DHashMap.Raw.Const.get!_insertIfNew h.out theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} : (m.insertIfNew k v).getD a fallback = - bif k == a && !m.contains k then v else m.getD a fallback := + if k == a ∧ ¬k ∈ m then v else m.getD a fallback := DHashMap.Raw.Const.getD_insertIfNew h.out @[simp] diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 01f8356e2ab1..bee599c20d2d 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -102,7 +102,7 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := HashMap.isEmpty_eq_size_eq_zero theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} : - (m.insert k).size = bif m.contains k then m.size else m.size + 1 := + (m.insert k).size = if k ∈ m then m.size else m.size + 1 := HashMap.size_insertIfNew theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.insert k).size := @@ -139,7 +139,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m. HashMap.mem_of_mem_erase theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} : - (m.erase k).size = bif m.contains k then m.size - 1 else m.size := + (m.erase k).size = if k ∈ m then m.size - 1 else m.size := HashMap.size_erase theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index de06cfe8d4b5..40e3315c380b 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -102,7 +102,7 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := HashMap.Raw.isEmpty_eq_size_eq_zero theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} : - (m.insert k).size = bif m.contains k then m.size else m.size + 1 := + (m.insert k).size = if k ∈ m then m.size else m.size + 1 := HashMap.Raw.size_insertIfNew h.out theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.insert k).size := @@ -139,7 +139,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m. HashMap.Raw.mem_of_mem_erase h.out theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} : - (m.erase k).size = bif m.contains k then m.size - 1 else m.size := + (m.erase k).size = if k ∈ m then m.size - 1 else m.size := HashMap.Raw.size_erase h.out theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := From 9f1eb479b01d96b360b18ebf00bae5b929c096f9 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 22 Jul 2024 17:10:11 +0200 Subject: [PATCH 3/6] feat: functional induction for mutual structural recursion (#4772) --- src/Lean/Meta/Tactic/FunInd.lean | 381 +++++++++++++------ tests/lean/run/funind_structural_mutual.lean | 94 +++++ tests/lean/run/funind_tests.lean | 9 + tests/lean/run/structuralMutual.lean | 72 ++-- 4 files changed, 391 insertions(+), 165 deletions(-) create mode 100644 tests/lean/run/funind_structural_mutual.lean diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index d5f1ce3d6640..8cff7d5e0d41 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -15,6 +15,8 @@ import Lean.Meta.ArgsPacker import Lean.Meta.PProdN import Lean.Elab.PreDefinition.WF.Eqns import Lean.Elab.PreDefinition.Structural.Eqns +import Lean.Elab.PreDefinition.Structural.IndGroupInfo +import Lean.Elab.PreDefinition.Structural.FindRecArg import Lean.Elab.Command import Lean.Meta.Tactic.ElimInfo @@ -402,14 +404,13 @@ def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do /-- -Substitutes equations, but makes sure to only substitute variables introduced after the motive -as the motive could depend on anything before, and `substVar` would happily drop equations -about these fixed parameters. +Substitutes equations, but makes sure to only substitute variables introduced after the motives +(given by the index) as the motive could depend on anything before, and `substVar` would happily +drop equations about these fixed parameters. -/ -def substVarAfter (mvarId : MVarId) (x : FVarId) : MetaM MVarId := do +def substVarAfter (mvarId : MVarId) (index : Nat) : MetaM MVarId := do mvarId.withContext do let mut mvarId := mvarId - let index := (← x.getDecl).index for localDecl in (← getLCtx) do if localDecl.index > index then mvarId ← trySubstVar mvarId localDecl.fvarId @@ -513,6 +514,20 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr) mkLambdaFVars #[h] f' let u ← getLevel goal return mkApp5 (mkConst ``dite [u]) goal c' h' t' f' + + | _ => + + -- we look in to `PProd.mk`, as it occurs in the mutual structural recursion construction + match_expr goal with + | And goal₁ goal₂ => match_expr e with + | PProd.mk _α _β e₁ e₂ => + let e₁' ← buildInductionBody toClear toPreserve goal₁ oldIH newIH isRecCall e₁ + let e₂' ← buildInductionBody toClear toPreserve goal₂ oldIH newIH isRecCall e₂ + return mkApp4 (.const ``And.intro []) goal₁ goal₂ e₁' e₂' + | _ => + throwError "Goal is PProd, but expression is:{indentExpr e}" + | True => + return .const ``True.intro [] | _ => -- match and casesOn application cause case splitting @@ -571,7 +586,7 @@ partial def buildInductionBody (toClear toPreserve : Array FVarId) (goal : Expr) /-- Given an expression `e` with metavariables * collects all these meta-variables, -* lifts them to the current context by reverting all local declarations up to `x` +* lifts them to the current context by reverting all local declarations after index `index` * introducing a local variable for each of the meta variable * assigning that local variable to the mvar * and finally lambda-abstracting over these new local variables. @@ -585,14 +600,18 @@ be used anymore. We are not using `mkLambdaFVars` on mvars directly, nor `abstractMVars`, as these at the moment do not handle delayed assignemnts correctly. -/ -def abstractIndependentMVars (mvars : Array MVarId) (x : FVarId) (e : Expr) : MetaM Expr := do +def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : MetaM Expr := do + trace[Meta.FunInd] "abstractIndependentMVars, to revert after {index}, original mvars: {mvars}" let mvars ← mvars.mapM fun mvar => do - let mvar ← substVarAfter mvar x - let (_, mvar) ← mvar.revertAfter x - pure mvar + let mvar ← substVarAfter mvar index + mvar.withContext do + let fvarIds := (← getLCtx).foldl (init := #[]) (start := index+1) fun fvarIds decl => fvarIds.push decl.fvarId + let (_, mvar) ← mvar.revert fvarIds + pure mvar + trace[Meta.FunInd] "abstractIndependentMVars, reverted mvars: {mvars}" let decls := mvars.mapIdx fun i mvar => - (.mkSimple s!"case{i.val+1}", .default, (fun _ => mvar.getType)) - Meta.withLocalDecls decls fun xs => do + (.mkSimple s!"case{i.val+1}", (fun _ => mvar.getType)) + Meta.withLocalDeclsD decls fun xs => do for mvar in mvars, x in xs do mvar.assign x mkLambdaFVars xs (← instantiateMVars e) @@ -647,7 +666,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body') let e' := mkApp2 e' body' target let e' ← mkLambdaFVars #[target] e' - let e' ← abstractIndependentMVars mvars motive.fvarId! e' + let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e' let e' ← mkLambdaFVars #[motive] e' -- We could pass (usedOnly := true) below, and get nicer induction principles that @@ -675,6 +694,25 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do { name := inductName, levelParams := us, type := eTyp, value := e' } return inductName +/-- +Given `foo.mutual_induct`, defined `foo.induct`, `bar.induct` etc. +Used for well-founded and structural recursion. +-/ +def projectMutualInduct (names : Array Name) (mutualInduct : Name) : MetaM Unit := do + let ci ← getConstInfo mutualInduct + let levelParams := ci.levelParams + + for name in names, idx in [:names.size] do + let inductName := .append name `induct + unless ← hasConst inductName do + let value ← forallTelescope ci.type fun xs _body => do + let value := .const ci.name (levelParams.map mkLevelParam) + let value := mkAppN value xs + let value ← PProdN.proj names.size idx value + mkLambdaFVars xs value + let type ← inferType value + addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value } + /-- In the type of `value`, reduces * Beta-redexes @@ -778,22 +816,11 @@ def unpackMutualInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name) : Meta { name := inductName, levelParams := ci.levelParams, type, value } return inductName + /-- Given `foo._unary.induct`, define `foo.mutual_induct` and then `foo.induct`, `bar.induct`, … -/ def deriveUnpackedInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name): MetaM Unit := do let unpackedInductName ← unpackMutualInduction eqnInfo unaryInductName - let ci ← getConstInfo unpackedInductName - let levelParams := ci.levelParams - - for name in eqnInfo.declNames, idx in [:eqnInfo.declNames.size] do - let inductName := .append name `induct - unless ← hasConst inductName do - let value ← forallTelescope ci.type fun xs _body => do - let value := .const ci.name (levelParams.map mkLevelParam) - let value := mkAppN value xs - let value ← PProdN.proj eqnInfo.declNames.size idx value - mkLambdaFVars xs value - let type ← inferType value - addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value } + projectMutualInduct eqnInfo.declNames unpackedInductName def stripPProdProjs (e : Expr) : Expr := match e with @@ -801,93 +828,198 @@ def stripPProdProjs (e : Expr) : Expr := | .proj ``And _ e' => stripPProdProjs e' | e => e +def withLetDecls {α} (name : Name) (ts : Array Expr) (es : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do + assert! es.size = ts.size + go 0 #[] +where + go (i : Nat) (acc : Array Expr) := do + if h : i < es.size then + let n := if es.size = 1 then name else name.appendIndexAfter (i + 1) + withLetDecl n ts[i]! es[i] fun x => go (i+1) (acc.push x) + else + k acc + /-- -Given a recursive definition `foo` defined via structural recursion, derive `foo.induct` for it. See -module doc for details. +Given a recursive definition `foo` defined via structural recursion, derive `foo.mutual_induct`, +if needed, and `foo.induct` for all functions in the group. +See module doc for details. -/ -def deriveStructuralInduction (name : Name) : MetaM Unit := do - let inductName := .append name `induct - if ← hasConst inductName then return - - let info ← getConstInfoDefn name - - let varNames ← forallTelescope info.type fun xs _ => xs.mapM (·.fvarId!.getUserName) - - let e' ← lambdaTelescope info.value fun params body => (stripPProdProjs body).withApp fun f args => do - MatcherApp.withUserNames params varNames do - unless isBRecOnRecursor (← getEnv) f.constName! do - throwError "Body of strucually recursive function not as expected:{indentExpr body}" - -- Bail out on mutual or nested inductives - let .str indName _ := f.constName! | unreachable! +def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit := do + let infos ← names.mapM getConstInfoDefn + -- First open up the fixed parameters everywhere + let e' ← lambdaBoundedTelescope infos[0]!.value numFixed fun xs _ => do + -- Now look at the body of an arbitrary of the functions (they are essentially the same + -- up to the final projections) + let body ← instantiateLambda infos[0]!.value xs + + lambdaTelescope body fun ys body => do + -- The body is of the form (brecOn … ).2.2.1 extra1 extra2 etc; ignore the + -- projection here + let f' := body.getAppFn + let body' := stripPProdProjs f' + let f := body'.getAppFn + let args := body'.getAppArgs ++ body.getAppArgs + + let body := stripPProdProjs body + let .const brecOnName us := f | + throwError "{infos[0]!.name}: unexpected body:{indentExpr infos[0]!.value}" + unless isBRecOnRecursor (← getEnv) brecOnName do + throwError "{infos[0]!.name}: expected .brecOn application, found:{indentExpr body}" + + let .str indName _ := brecOnName | unreachable! let indInfo ← getConstInfoInduct indName - if indInfo.numTypeFormers > 1 then - throwError "functional induction: cannot handle mutual or nested inductives" - - let elimInfo ← getElimExprInfo f - let targets : Array Expr := elimInfo.targetsPos.map (args[·]!) - let body := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size]! - let extraArgs : Array Expr := args[elimInfo.motivePos + 1 + elimInfo.targetsPos.size + 1:] - - let fixedParams := params.filter fun x => !(targets.contains x || extraArgs.contains x) - let varyingParams := params.filter fun x => targets.contains x || extraArgs.contains x - unless params == fixedParams ++ varyingParams do - throwError "functional induction: unexpected order of fixed and varying parameters:{indentExpr body}" - unless 1 ≤ f.constLevels!.length do - throwError "functional induction: unexpected recursor: {f} has no universe parameters" - - let motiveType ← mkForallFVars varyingParams (.sort levelZero) - withLocalDecl `motive .default motiveType fun motive => do - - let fn := mkAppN (.const name (info.levelParams.map mkLevelParam)) fixedParams - let isRecCall : Expr → Option Expr := fun e => - if e.getAppNumArgs = varyingParams.size && e.getAppFn.isFVarOf motive.fvarId! then - mkAppN fn e.getAppArgs - else - none - - -- Sometimes `brecOn` only supports eliminating to `Type u`, not `Sort `u`. - -- So just use `binductionOn` instead - let us := f.constLevels!.drop 1 - let bInductionName := mkBInductionOnName indInfo.name - let value := mkAppN (.const bInductionName us) (args[:elimInfo.motivePos]) - -- We may have to reorder the parameters for motive before passing it to brec - let brecMotive ← mkLambdaFVars targets - (← mkForallFVars extraArgs (mkAppN motive varyingParams)) - let e' := mkAppN (mkApp value brecMotive) targets - check e' - let (body', mvars) ← M2.run do - forallTelescope (← inferType e').bindingDomain! fun xs goal => do - let arity := varyingParams.size + 1 - if xs.size ≠ arity then - throwError "expected recursor argument to take {arity} parameters, got {xs}" else - let targets : Array Expr := xs[:targets.size] - let genIH := xs[targets.size]! - let extraParams := xs[targets.size+1:] - -- open body with the same arg - let body ← instantiateLambda body targets - removeLamda body fun oldIH body => do - let body ← instantiateLambda body extraParams - let body' ← buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body - if body'.containsFVar oldIH then - throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}" - mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body') - let e' := mkApp e' body' - let e' := mkAppN e' extraArgs - let e' ← mkLambdaFVars varyingParams e' - let e' ← abstractIndependentMVars mvars motive.fvarId! e' - let e' ← mkLambdaFVars #[motive] e' - - -- We could pass (usedOnly := true) below, and get nicer induction principles that - -- do do not mention odd unused parameters. - -- But the downside is that automatic instantiation of the principle (e.g. in a tactic - -- that derives them from an function application in the goal) is harder, as - -- one would have to infer or keep track of which parameters to pass. - -- So for now lets just keep them around. - let e' ← mkLambdaFVars (binderInfoForMVars := .default) fixedParams e' - instantiateMVars e' + + -- we have a `.brecOn` application, so now figure out the length of the fixed prefix + -- we can use the recInfo for `.rec`, since `.brecOn` has a similar structure + let recInfo ← getConstInfoRec (mkRecName indName) + if args.size < recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 + recInfo.numMotives then + throwError "insufficient arguments to .brecOn:{indentExpr body}" + let brecOnArgs : Array Expr := args[:recInfo.numParams] + let _brecOnMotives : Array Expr := args[recInfo.numParams:recInfo.numParams + recInfo.numMotives] + let brecOnTargets : Array Expr := args[recInfo.numParams + recInfo.numMotives : + recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1] + let brecOnMinors : Array Expr := args[recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 : + recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 + recInfo.numMotives] + let brecOnExtras : Array Expr := args[ recInfo.numParams + recInfo.numMotives + recInfo.numIndices + 1 + + recInfo.numMotives:] + unless brecOnTargets.all (·.isFVar) do + throwError "the indices and major argument of the brecOn application are not variables:{indentExpr body}" + unless brecOnExtras.all (·.isFVar) do + throwError "the extra arguments to the the brecOn application are not variables:{indentExpr body}" + let lvl :: indLevels := us |throwError "Too few universe parameters in .brecOn application:{indentExpr body}" + + let group : Structural.IndGroupInst := { Structural.IndGroupInfo.ofInductiveVal indInfo with + levels := indLevels, params := brecOnArgs } + + -- We also need to know the number of indices of each type former, including the auxillary + -- type formers that do not have IndInfo. We can read it off the motives types of the recursor. + let numTargetss ← do + let aux := mkAppN (.const recInfo.name (0 :: group.levels)) group.params + let motives ← inferArgumentTypesN recInfo.numMotives aux + motives.mapM fun motive => + forallTelescopeReducing motive fun xs _ => pure xs.size + + let recArgInfos ← infos.mapM fun info => do + let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) info.name | throwError "{info.name} missing eqnInfo" + let value ← instantiateLambda info.value xs + let recArgInfo' ← lambdaTelescope value fun ys _ => + Structural.getRecArgInfo info.name numFixed (xs ++ ys) eqnInfo.recArgPos + let #[recArgInfo] ← Structural.argsInGroup group xs value #[recArgInfo'] + | throwError "Structural.argsInGroup did not return a recArgInfo" + pure recArgInfo + + let positions : Structural.Positions := .groupAndSort (·.indIdx) recArgInfos (Array.range indInfo.numTypeFormers) + + -- Below we'll need the types of the motive arguments (brecOn argument order) + let brecMotiveTypes ← inferArgumentTypesN recInfo.numMotives (group.brecOn true lvl 0) + trace[Meta.FunInd] m!"brecMotiveTypes: {brecMotiveTypes}" + assert! brecMotiveTypes.size = positions.size + + -- Remove the varying parameters from the environment + withErasedFVars (ys.map (·.fvarId!)) do + -- The brecOnArgs, brecOnMotives and brecOnMinor should still be valid in this + -- context, and are the parts relevant for every function in the mutual group + + -- Calculate the types of the induction motives (natural argument order) for each function + let motiveTypes ← infos.mapM fun info => do + lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => + mkForallFVars ys (.sort levelZero) + let motiveArities ← infos.mapM fun info => do + lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size + let motiveDecls ← motiveTypes.mapIdxM fun ⟨i,_⟩ motiveType => do + let n := if infos.size = 1 then .mkSimple "motive" + else .mkSimple s!"motive_{i+1}" + pure (n, fun _ => pure motiveType) + withLocalDeclsD motiveDecls fun motives => do + + -- Prepare the `isRecCall` that recognizes recursive calls + let fns := infos.map fun info => + mkAppN (.const info.name (info.levelParams.map mkLevelParam)) xs + let isRecCall : Expr → Option Expr := fun e => do + if let .some i := motives.indexOf? e.getAppFn then + if e.getAppNumArgs = motiveArities[i]! then + return mkAppN fns[i]! e.getAppArgs + .none + + -- Motives with parameters reordered, to put indices and major first + let brecMotives ← (Array.zip motives recArgInfos).mapM fun (motive, recArgInfo) => do + forallTelescope (← inferType motive) fun ys _ => do + let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys + mkLambdaFVars indicesMajor (← mkForallFVars rest (mkAppN motive ys)) + + -- We need to pack these motives according to the `positions` assignment. + let packedMotives ← positions.mapMwith PProdN.packLambdas brecMotiveTypes brecMotives + trace[Meta.FunInd] m!"packedMotives: {packedMotives}" + + -- Now we can calcualte the expected types of the minor arguments + let minorTypes ← inferArgumentTypesN recInfo.numMotives <| + mkAppN (group.brecOn true lvl 0) (packedMotives ++ brecOnTargets) + trace[Meta.FunInd] m!"minorTypes: {minorTypes}" + -- So that we can transform them + let (minors', mvars) ← M2.run do + let mut minors' := #[] + for brecOnMinor in brecOnMinors, goal in minorTypes, numTargets in numTargetss do + let minor' ← forallTelescope goal fun xs goal => do + unless xs.size ≥ numTargets do + throwError ".brecOn argument has too few parameters, expected at least {numTargets}: {xs}" + let targets : Array Expr := xs[:numTargets] + let genIH := xs[numTargets]! + let extraParams := xs[numTargets+1:] + -- open body with the same arg + let body ← instantiateLambda brecOnMinor targets + removeLamda body fun oldIH body => do + trace[Meta.FunInd] "replacing {Expr.fvar oldIH} with {genIH}" + let body ← instantiateLambda body extraParams + let body' ← buildInductionBody #[genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body + if body'.containsFVar oldIH then + throwError m!"Did not fully eliminate {mkFVar oldIH} from induction principle body:{indentExpr body}" + mkLambdaFVars (targets.push genIH) (← mkLambdaFVars extraParams body') + minors' := minors'.push minor' + pure minors' + trace[Meta.FunInd] "processed minors: {minors'}" + + -- Now assemble the mutual_induct theorem + -- Let-bind the transformed minors to avoid code duplication of possibly very large + -- terms when we have mutual induction. + let e' ← withLetDecls `minor minorTypes minors' fun minors' => do + let mut brecOnApps := #[] + for info in infos, recArgInfo in recArgInfos, idx in [:infos.size] do + -- Take care to pick the `ys` from the type, to get the variable names expected + -- by the user, but use the value arity + let arity ← lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size + let e ← forallBoundedTelescope (← instantiateForall info.type xs) arity fun ys _ => do + let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys + -- Find where in the function packing we are (TODO: abstract out) + let some indIdx := positions.findIdx? (·.contains idx) | panic! "invalid positions" + let some pos := positions.find? (·.contains idx) | panic! "invalid positions" + let some packIdx := pos.findIdx? (· == idx) | panic! "invalid positions" + let e := group.brecOn true lvl indIdx -- unconditionally using binduction here + let e := mkAppN e packedMotives + let e := mkAppN e indicesMajor + let e := mkAppN e minors' + let e ← PProdN.proj pos.size packIdx e + let e := mkAppN e rest + let e ← mkLambdaFVars ys e + trace[Meta.FunInd] "assembled call for {info.name}: {e}" + pure e + brecOnApps := brecOnApps.push e + mkLetFVars minors' (← PProdN.mk 0 brecOnApps) + let e' ← abstractIndependentMVars mvars (← motives.back.fvarId!.getDecl).index e' + let e' ← mkLambdaFVars motives e' + + -- We could pass (usedOnly := true) below, and get nicer induction principles that + -- do do not mention odd unused parameters. + -- But the downside is that automatic instantiation of the principle (e.g. in a tactic + -- that derives them from an function application in the goal) is harder, as + -- one would have to infer or keep track of which parameters to pass. + -- So for now lets just keep them around. + let e' ← mkLambdaFVars (binderInfoForMVars := .default) xs e' + let e' ← instantiateMVars e' + trace[Meta.FunInd] "complete body of mutual induction principle:{indentExpr e'}" + pure e' unless (← isTypeCorrect e') do - logError m!"failed to derive induction priciple:{indentExpr e'}" + logError m!"constructed induction principle is not type correct:{indentExpr e'}" check e' let eTyp ← inferType e' @@ -895,25 +1027,33 @@ def deriveStructuralInduction (name : Name) : MetaM Unit := do -- logInfo m!"eTyp: {eTyp}" let params := (collectLevelParams {} eTyp).params -- Prune unused level parameters, preserving the original order - let us := info.levelParams.filter (params.contains ·) + let us := infos[0]!.levelParams.filter (params.contains ·) + + let inductName := + if names.size = 1 then + names[0]! ++ `induct + else + names[0]! ++ `mutual_induct addDecl <| Declaration.thmDecl { name := inductName, levelParams := us, type := eTyp, value := e' } + if names.size > 1 then + projectMutualInduct names inductName + /-- Given a recursively defined function `foo`, derives `foo.induct`. See the module doc for details. -/ def deriveInduction (name : Name) : MetaM Unit := do - if let some eqnInfo := WF.eqnInfoExt.find? (← getEnv) name then - let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec - unless eqnInfo.declNameNonRec = name do - deriveUnpackedInduction eqnInfo unaryInductName - else if let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) name then - if eqnInfo.declNames.size > 1 then - throwError "Induction principles for mutually structurally recursive functions are not yet supported" - deriveStructuralInduction eqnInfo.declName - else - throwError "Cannot derive functional induction principle for {name}: Not defined by structural or well-founded recursion" + mapError (f := (m!"Cannot derive functional induction principle (please report this issue)\n{indentD ·}")) do + if let some eqnInfo := WF.eqnInfoExt.find? (← getEnv) name then + let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec + unless eqnInfo.declNameNonRec = name do + deriveUnpackedInduction eqnInfo unaryInductName + else if let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) name then + deriveInductionStructural eqnInfo.declNames eqnInfo.numFixed + else + throwError "{name} is not defined by structural or well-founded recursion" def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do let .str p s := name | return false @@ -926,6 +1066,9 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do if let some eqnInfo := WF.eqnInfoExt.find? env p then if h : eqnInfo.declNames.size > 1 then return eqnInfo.declNames[0] = p + if let some eqnInfo := Structural.eqnInfoExt.find? env p then + if h : eqnInfo.declNames.size > 1 then + return eqnInfo.declNames[0] = p return false | _ => return false diff --git a/tests/lean/run/funind_structural_mutual.lean b/tests/lean/run/funind_structural_mutual.lean new file mode 100644 index 000000000000..d364a4880787 --- /dev/null +++ b/tests/lean/run/funind_structural_mutual.lean @@ -0,0 +1,94 @@ +/-! +A few tests for functional induction theorems generated from mutual recursive inductives. + +Some more tests are in `structuralMutual.lean` and `funind_structural`. +-/ + +set_option guard_msgs.diff true + + +inductive Tree (α : Type u) : Type u where + | node : α → (Bool → List (Tree α)) → Tree α + +-- Recursion over nested inductive + +mutual +def Tree.size : Tree α → Nat + | .node _ tsf => 1 + size_aux (tsf true) + size_aux (tsf false) +termination_by structural t => t +def Tree.size_aux : List (Tree α) → Nat + | [] => 0 + | t :: ts => size t + size_aux ts +end + +/-- +info: Tree.size.induct.{u_1} {α : Type u_1} (motive_1 : Tree α → Prop) (motive_2 : List (Tree α) → Prop) + (case1 : + ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_2 (tsf false) → motive_1 (Tree.node a tsf)) + (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts)) : + ∀ (a : Tree α), motive_1 a +-/ +#guard_msgs in +#check Tree.size.induct + + +-- Recursion over nested inductive, functions in the “wrong” order (auxillary first) + +mutual +def Tree.size_aux' : List (Tree α) → Nat + | [] => 0 + | t :: ts => size' t + size_aux' ts +def Tree.size' : Tree α → Nat + | .node _ tsf => 1 + size_aux' (tsf true) + size_aux' (tsf false) +termination_by structural t => t +end + +/-- +info: Tree.size_aux'.mutual_induct.{u_1} {α : Type u_1} (motive_1 : List (Tree α) → Prop) (motive_2 : Tree α → Prop) + (case1 : + ∀ (a : α) (tsf : Bool → List (Tree α)), motive_1 (tsf true) → motive_1 (tsf false) → motive_2 (Tree.node a tsf)) + (case2 : motive_1 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_2 t → motive_1 ts → motive_1 (t :: ts)) : + (∀ (a : List (Tree α)), motive_1 a) ∧ ∀ (a : Tree α), motive_2 a +-/ +#guard_msgs in +#check Tree.size_aux'.mutual_induct + +-- Similar, but with many packed functions +mutual +def Tree.size_aux1 : List (Tree α) → Nat + | [] => 0 + | t :: ts => size2 t + size_aux2 ts +def Tree.size1 : Tree α → Nat + | .node _ tsf => 1 + size_aux2 (tsf true) + size_aux3 (tsf false) +termination_by structural t => t +def Tree.size_aux2 : List (Tree α) → Nat + | [] => 0 + | t :: ts => size3 t + size_aux3 ts +def Tree.size2 : Tree α → Nat + | .node _ tsf => 1 + size_aux3 (tsf true) + size_aux1 (tsf false) +def Tree.size_aux3 : List (Tree α) → Nat + | [] => 0 + | t :: ts => size1 t + size_aux1 ts +def Tree.size3 : Tree α → Nat + | .node _ tsf => 1 + size_aux1 (tsf true) + size_aux2 (tsf false) +end + +/-- +info: Tree.size_aux1.mutual_induct.{u_1} {α : Type u_1} (motive_1 motive_2 motive_3 : List (Tree α) → Prop) + (motive_4 motive_5 motive_6 : Tree α → Prop) + (case1 : + ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_3 (tsf false) → motive_4 (Tree.node a tsf)) + (case2 : + ∀ (a : α) (tsf : Bool → List (Tree α)), motive_1 (tsf true) → motive_2 (tsf false) → motive_5 (Tree.node a tsf)) + (case3 : + ∀ (a : α) (tsf : Bool → List (Tree α)), motive_3 (tsf true) → motive_1 (tsf false) → motive_6 (Tree.node a tsf)) + (case4 : motive_1 []) (case5 : ∀ (t : Tree α) (ts : List (Tree α)), motive_6 t → motive_2 ts → motive_1 (t :: ts)) + (case6 : motive_2 []) (case7 : ∀ (t : Tree α) (ts : List (Tree α)), motive_5 t → motive_3 ts → motive_2 (t :: ts)) + (case8 : motive_3 []) (case9 : ∀ (t : Tree α) (ts : List (Tree α)), motive_4 t → motive_1 ts → motive_3 (t :: ts)) : + (∀ (a : List (Tree α)), motive_1 a) ∧ + (∀ (a : List (Tree α)), motive_2 a) ∧ + (∀ (a : List (Tree α)), motive_3 a) ∧ + (∀ (a : Tree α), motive_4 a) ∧ (∀ (a : Tree α), motive_5 a) ∧ ∀ (a : Tree α), motive_6 a +-/ +#guard_msgs in +#check Tree.size_aux1.mutual_induct diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index 06c594c0a4b7..98e421448675 100644 --- a/tests/lean/run/funind_tests.lean +++ b/tests/lean/run/funind_tests.lean @@ -634,6 +634,15 @@ info: Tree.Tree.map_forest.induct (f : Tree → Tree) (motive1 : Tree → Prop) #guard_msgs in #check Tree.map_forest.induct +/-- +info: Tree.Tree.map.mutual_induct (f : Tree → Tree) (motive1 : Tree → Prop) (motive2 : List Tree → Prop) + (case1 : ∀ (ts : List Tree), motive2 ts → motive1 (Tree.node ts)) + (case2 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive1 t) → motive2 ts) : + (∀ (a : Tree), motive1 a) ∧ ∀ (ts : List Tree), motive2 ts +-/ +#guard_msgs in +#check Tree.map.mutual_induct + end Tree namespace DefaultArgument diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index abea5427e531..f3bdec673e17 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/tests/lean/run/structuralMutual.lean @@ -1,5 +1,3 @@ -import Lean.Elab.Command - set_option guard_msgs.diff true /-! @@ -527,13 +525,13 @@ Too many possible combinations of parameters of type Nattish (or please indicate Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) -Call from ManyCombinations.f to ManyCombinations.g at 559:15-29: +Call from ManyCombinations.f to ManyCombinations.g at 557:15-29: #1 #2 #3 #4 #5 ? ? ? ? #6 ? = ? ? #7 ? ? = ? #8 ? ? ? = -Call from ManyCombinations.g to ManyCombinations.f at 562:15-29: +Call from ManyCombinations.g to ManyCombinations.f at 560:15-29: #5 #6 #7 #8 #1 _ _ _ _ #2 _ = _ _ @@ -583,73 +581,55 @@ namespace FunIndTests -- out nicely /-- -error: Failed to realize constant A.size.induct: - Induction principles for mutually structurally recursive functions are not yet supported ---- -error: Failed to realize constant A.size.induct: - Induction principles for mutually structurally recursive functions are not yet supported ---- -error: unknown identifier 'A.size.induct' +info: A.size.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self) + (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty) + (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a)) + (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a -/ #guard_msgs in #check A.size.induct /-- -error: Failed to realize constant A.subs.induct: - Induction principles for mutually structurally recursive functions are not yet supported ---- -error: Failed to realize constant A.subs.induct: - Induction principles for mutually structurally recursive functions are not yet supported ---- -error: unknown identifier 'A.subs.induct' +info: A.subs.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self) + (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty) + (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a)) + (case6 : motive_2 B.empty) (a : A) : motive_1 a -/ #guard_msgs in #check A.subs.induct /-- -error: Failed to realize constant MutualIndNonMutualFun.A.self_size.induct: - functional induction: cannot handle mutual or nested inductives ---- -error: Failed to realize constant MutualIndNonMutualFun.A.self_size.induct: - functional induction: cannot handle mutual or nested inductives ---- -error: unknown identifier 'MutualIndNonMutualFun.A.self_size.induct' +info: MutualIndNonMutualFun.A.self_size.induct (motive : MutualIndNonMutualFun.A → Prop) + (case1 : ∀ (a : MutualIndNonMutualFun.A), motive a → motive a.self) + (case2 : ∀ (a : MutualIndNonMutualFun.B), motive (MutualIndNonMutualFun.A.other a)) + (case3 : motive MutualIndNonMutualFun.A.empty) : ∀ (a : MutualIndNonMutualFun.A), motive a -/ #guard_msgs in #check MutualIndNonMutualFun.A.self_size.induct /-- -error: Failed to realize constant MutualIndNonMutualFun.A.self_size_with_param.induct: - functional induction: cannot handle mutual or nested inductives ---- -error: Failed to realize constant MutualIndNonMutualFun.A.self_size_with_param.induct: - functional induction: cannot handle mutual or nested inductives ---- -error: unknown identifier 'MutualIndNonMutualFun.A.self_size_with_param.induct' +info: MutualIndNonMutualFun.A.self_size_with_param.induct (motive : Nat → MutualIndNonMutualFun.A → Prop) + (case1 : ∀ (n : Nat) (a : MutualIndNonMutualFun.A), motive n a → motive n a.self) + (case2 : ∀ (x : Nat) (a : MutualIndNonMutualFun.B), motive x (MutualIndNonMutualFun.A.other a)) + (case3 : ∀ (x : Nat), motive x MutualIndNonMutualFun.A.empty) : + ∀ (a : Nat) (a_1 : MutualIndNonMutualFun.A), motive a a_1 -/ #guard_msgs in #check MutualIndNonMutualFun.A.self_size_with_param.induct /-- -error: Failed to realize constant A.hasNoBEmpty.induct: - Induction principles for mutually structurally recursive functions are not yet supported ---- -error: Failed to realize constant A.hasNoBEmpty.induct: - Induction principles for mutually structurally recursive functions are not yet supported ---- -error: unknown identifier 'A.hasNoBEmpty.induct' +info: A.hasNoBEmpty.induct (motive_1 : A → Prop) (motive_2 : B → Prop) (case1 : ∀ (a : A), motive_1 a → motive_1 a.self) + (case2 : ∀ (b : B), motive_2 b → motive_1 (A.other b)) (case3 : motive_1 A.empty) + (case4 : ∀ (b : B), motive_2 b → motive_2 b.self) (case5 : ∀ (a : A), motive_1 a → motive_2 (B.other a)) + (case6 : motive_2 B.empty) : ∀ (a : A), motive_1 a -/ #guard_msgs in #check A.hasNoBEmpty.induct /-- -error: Failed to realize constant EvenOdd.isEven.induct: - Induction principles for mutually structurally recursive functions are not yet supported ---- -error: Failed to realize constant EvenOdd.isEven.induct: - Induction principles for mutually structurally recursive functions are not yet supported ---- -error: unknown identifier 'EvenOdd.isEven.induct' +info: EvenOdd.isEven.induct (motive_1 motive_2 : Nat → Prop) (case1 : motive_1 0) + (case2 : ∀ (n : Nat), motive_2 n → motive_1 n.succ) (case3 : motive_2 0) + (case4 : ∀ (n : Nat), motive_1 n → motive_2 n.succ) : ∀ (a : Nat), motive_1 a -/ #guard_msgs in #check EvenOdd.isEven.induct -- TODO: This error message can be improved From 20c857147c2496a806b3390012f99e08dfaa1741 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 22 Jul 2024 22:52:14 +0200 Subject: [PATCH 4/6] feat: unnecessary termination_by clauses cause warnings, not errors (#4809) fixes #4804 --- src/Lean/Elab/PreDefinition/Main.lean | 2 +- .../Elab/PreDefinition/TerminationHint.lean | 10 +++---- tests/lean/termination_by.lean.expected.out | 28 +++++++++---------- 3 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 55763c83804e..426b3c147315 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -114,7 +114,7 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do if !structural && !preDefsWithout.isEmpty then let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}")) let doOrDoes := if preDefsWithout.size = 1 then "does" else "do" - logErrorAt termBy.ref (m!"Incomplete set of `termination_by` annotations:\n"++ + logErrorAt termBy.ref (m!"incomplete set of `termination_by` annotations:\n"++ m!"This function is mutually with {m}, which {doOrDoes} not have " ++ m!"a `termination_by` clause.\n" ++ m!"The present clause is ignored.") diff --git a/src/Lean/Elab/PreDefinition/TerminationHint.lean b/src/Lean/Elab/PreDefinition/TerminationHint.lean index 7a4a94d11e57..757d388d55a0 100644 --- a/src/Lean/Elab/PreDefinition/TerminationHint.lean +++ b/src/Lean/Elab/PreDefinition/TerminationHint.lean @@ -57,18 +57,18 @@ structure TerminationHints where def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩ -/-- Logs warnings when the `TerminationHints` are present. -/ +/-- Logs warnings when the `TerminationHints` are unexpectedly present. -/ def TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : CoreM Unit := do match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with | .none, .none, .none => pure () | .none, .none, .some dec_by => - logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}" + logWarningAt dec_by.ref m!"unused `decreasing_by`, function is {reason}" | .some term_by?, .none, .none => - logErrorAt term_by? m!"unused `termination_by?`, function is {reason}" + logWarningAt term_by? m!"unused `termination_by?`, function is {reason}" | .none, .some term_by, .none => - logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}" + logWarningAt term_by.ref m!"unused `termination_by`, function is {reason}" | _, _, _ => - logErrorAt hints.ref m!"unused termination hints, function is {reason}" + logWarningAt hints.ref m!"unused termination hints, function is {reason}" /-- True if any form of termination hint is present. -/ def TerminationHints.isNotNone (hints : TerminationHints) : Bool := diff --git a/tests/lean/termination_by.lean.expected.out b/tests/lean/termination_by.lean.expected.out index 41b7308ab95b..b438c7f68249 100644 --- a/tests/lean/termination_by.lean.expected.out +++ b/tests/lean/termination_by.lean.expected.out @@ -1,20 +1,20 @@ -termination_by.lean:9:2-9:18: error: unused `termination_by`, function is not recursive -termination_by.lean:12:2-12:21: error: unused `decreasing_by`, function is not recursive -termination_by.lean:15:2-16:21: error: unused termination hints, function is not recursive -termination_by.lean:19:2-19:18: error: unused `termination_by`, function is partial -termination_by.lean:22:2-22:21: error: unused `decreasing_by`, function is partial -termination_by.lean:25:2-26:21: error: unused termination hints, function is partial -termination_by.lean:29:0-29:16: error: unused `termination_by`, function is unsafe -termination_by.lean:32:2-32:21: error: unused `decreasing_by`, function is unsafe -termination_by.lean:35:2-36:21: error: unused termination hints, function is unsafe -termination_by.lean:40:4-40:20: error: unused `termination_by`, function is not recursive -termination_by.lean:44:4-44:20: error: unused `termination_by`, function is not recursive -termination_by.lean:54:2-54:18: error: unused `termination_by`, function is not recursive -termination_by.lean:62:2-62:23: error: Incomplete set of `termination_by` annotations: +termination_by.lean:9:2-9:18: warning: unused `termination_by`, function is not recursive +termination_by.lean:12:2-12:21: warning: unused `decreasing_by`, function is not recursive +termination_by.lean:15:2-16:21: warning: unused termination hints, function is not recursive +termination_by.lean:19:2-19:18: warning: unused `termination_by`, function is partial +termination_by.lean:22:2-22:21: warning: unused `decreasing_by`, function is partial +termination_by.lean:25:2-26:21: warning: unused termination hints, function is partial +termination_by.lean:29:0-29:16: warning: unused `termination_by`, function is unsafe +termination_by.lean:32:2-32:21: warning: unused `decreasing_by`, function is unsafe +termination_by.lean:35:2-36:21: warning: unused termination hints, function is unsafe +termination_by.lean:40:4-40:20: warning: unused `termination_by`, function is not recursive +termination_by.lean:44:4-44:20: warning: unused `termination_by`, function is not recursive +termination_by.lean:54:2-54:18: warning: unused `termination_by`, function is not recursive +termination_by.lean:62:2-62:23: error: incomplete set of `termination_by` annotations: This function is mutually with isOdd, which does not have a `termination_by` clause. The present clause is ignored. Try this: termination_by x1 => x1 -termination_by.lean:79:2-79:27: error: Incomplete set of `termination_by` annotations: +termination_by.lean:79:2-79:27: error: incomplete set of `termination_by` annotations: This function is mutually with Test.f, Test.h and Test.i, which do not have a `termination_by` clause. The present clause is ignored. termination_by.lean:101:2-101:27: error: Invalid `termination_by`; this function is mutually recursive with Test2.f, which is marked as `termination_by structural` so this one also needs to be marked `structural`. From 852add3e55ed8c94bc496f35019674f046ab0d5e Mon Sep 17 00:00:00 2001 From: grunweg Date: Mon, 22 Jul 2024 23:55:37 +0200 Subject: [PATCH 5/6] doc: document `Command.Scope` (#4748) Also extends existing definition for `getScope`/`getScopes` and clarifies that the `end` command is optional at the end of a file. --------- Co-authored-by: Kyle Miller --- src/Lean/Elab/Command.lean | 57 ++++++++++++++++++++++++++++++++++-- src/Lean/Parser/Command.lean | 2 +- 2 files changed, 55 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 28acce42a624..2055eec7c745 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -12,17 +12,62 @@ import Lean.Language.Basic namespace Lean.Elab.Command +/-- +A `Scope` records the part of the `CommandElabM` state that respects scoping, +such as the data for `universe`, `open`, and `variable` declarations, the current namespace, +and currently enabled options. +The `CommandElabM` state contains a stack of scopes, and only the top `Scope` +on the stack is read from or modified. There is always at least one `Scope` on the stack, +even outside any `section` or `namespace`, and each new pushed `Scope` +starts as a modified copy of the previous top scope. +-/ structure Scope where + /-- + The component of the `namespace` or `section` that this scope is associated to. + For example, `section a.b.c` and `namespace a.b.c` each create three scopes with headers + named `a`, `b`, and `c`. + This is used for checking the `end` command. The "base scope" has `""` as its header. + -/ header : String + /-- + The current state of all set options at this point in the scope. Note that this is the + full current set of options and does *not* simply contain the options set + while this scope has been active. + -/ opts : Options := {} + /-- The current namespace. The top-level namespace is represented by `Name.anonymous`. -/ currNamespace : Name := Name.anonymous + /-- All currently `open`ed namespaces and names. -/ openDecls : List OpenDecl := [] + /-- The current list of names for universe level variables to use for new declarations. This is managed by the `universe` command. -/ levelNames : List Name := [] - /-- section variables -/ + /-- + The current list of binders to use for new declarations. + This is managed by the `variable` command. + Each binder is represented in `Syntax` form, and it is re-elaborated + within each command that uses this information. + + This is also used by commands, such as `#check`, to create an initial local context, + even if they do not work with binders per se. + -/ varDecls : Array (TSyntax ``Parser.Term.bracketedBinder) := #[] - /-- Globally unique internal identifiers for the `varDecls` -/ + /-- + Globally unique internal identifiers for the `varDecls`. + There is one identifier per variable introduced by the binders + (recall that a binder such as `(a b c : Ty)` can produce more than one variable), + and each identifier is the user-provided variable name with a macro scope. + This is used by `TermElabM` in `Lean.Elab.Term.Context` to help with processing macros + that capture these variables. + -/ varUIds : Array Name := #[] - /-- noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/ + /-- + If true (default: false), all declarations that fail to compile + automatically receive the `noncomputable` modifier. + A scope with this flag set is created by `noncomputable section`. + + Recall that a new scope inherits all values from its parent scope, + so all sections and namespaces nested within a `noncomputable` section also have this flag set. + -/ isNoncomputable : Bool := false deriving Inhabited @@ -230,6 +275,7 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M instance : MonadLiftT IO CommandElabM where monadLift := liftIO +/-- Return the current scope. -/ def getScope : CommandElabM Scope := do pure (← get).scopes.head! instance : MonadResolveName CommandElabM where @@ -612,6 +658,11 @@ Interrupt and abort exceptions are caught but not logged. private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do liftCoreM x +/-- +Return the stack of all currently active scopes: +the base scope always comes last; new scopes are prepended in the front. +In particular, the current scope is always the first element. +-/ def getScopes : CommandElabM (List Scope) := do pure (← get).scopes diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 8b11a0fb2c9e..9585a4fe028e 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -269,7 +269,7 @@ corresponding `end ` or the end of the file. "namespace " >> checkColGt >> ident /-- `end` closes a `section` or `namespace` scope. If the scope is named ``, it has to be closed -with `end `. +with `end `. The `end` command is optional at the end of a file. -/ @[builtin_command_parser] def «end» := leading_parser "end" >> optional (ppSpace >> checkColGt >> ident) From 5938dbbd14145c9b78f7645c4777f62a3fc8212c Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 22 Jul 2024 16:23:28 -0700 Subject: [PATCH 6/6] fix: make `elab_as_elim` eagerly elaborate arguments for parameters appearing in the types of targets (#4800) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `elab_as_elim` elaborator eagerly elaborates arguments that can help with elaborating the motive, however it does not include the transitive closure of parameters appearing in types of parameters appearing in ... types of targets. This leads to counter-intuitive behavior where arguments supplied to the eliminator may unexpectedly have postponed elaboration, causing motives to be type incorrect for under-applied eliminators such as the following: ```lean class IsEmpty (α : Sort u) : Prop where protected false : α → False @[elab_as_elim] def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := (IsEmpty.false a).elim example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α) ``` The issue is that when `isEmptyElim (α := α)` is computing its motive, the value of the postponed argument `α` is still an unassignable metavariable. With this PR, this argument is now among those that are eagerly elaborated since it appears as the type of the target `a`. This PR also contains some other fixes: * When underapplied, does unification when instantiating foralls in the expected type. * When overapplied, type checks the generalized-and-reverted expected type. * When collecting targets, collects them in the correct order. Adds trace class `trace.Elab.app.elab_as_elim`. This is a followup to #4722, which added motive type checking but exposed the eagerness issue. --- src/Lean/Elab/App.lean | 94 +++++++++---- tests/lean/elabAsElim.lean | 98 ------------- tests/lean/elabAsElim.lean.expected.out | 8 -- tests/lean/run/elabAsElim.lean | 177 ++++++++++++++++++++++++ 4 files changed, 243 insertions(+), 134 deletions(-) delete mode 100644 tests/lean/elabAsElim.lean delete mode 100644 tests/lean/elabAsElim.lean.expected.out create mode 100644 tests/lean/run/elabAsElim.lean diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 8be94e99ebc8..14c0ae70d636 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Lean.Util.FindMVar +import Lean.Util.CollectFVars import Lean.Parser.Term import Lean.Meta.KAbstract import Lean.Meta.Tactic.ElimInfo @@ -711,6 +712,12 @@ structure Context where ``` theorem Eq.subst' {α} {motive : α → Prop} {a b : α} (h : a = b) : motive a → motive b ``` + For another example, the term `isEmptyElim (α := α)` is an underapplied eliminator, and it needs + argument `α` to be elaborated eagerly to create a type-correct motive. + ``` + def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := ... + example {α : Type _} [IsEmpty α] : id (α → False) := isEmptyElim (α := α) + ``` -/ extraArgsPos : Array Nat @@ -724,8 +731,8 @@ structure State where namedArgs : List NamedArg /-- User-provided arguments that still have to be processed. -/ args : List Arg - /-- Discriminants processed so far. -/ - discrs : Array Expr := #[] + /-- Discriminants (targets) processed so far. -/ + discrs : Array (Option Expr) /-- Instance implicit arguments collected so far. -/ instMVars : Array MVarId := #[] /-- Position of the next argument to be processed. We use it to decide whether the argument is the motive or a discriminant. -/ @@ -742,10 +749,7 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do let motiveBody ← kabstract motive discr /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/ let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr)) - let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody - unless (← isTypeCorrect motive) do - throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}" - return motive + return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody /-- If the eliminator is over-applied, we "revert" the extra arguments. -/ def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) := @@ -761,7 +765,7 @@ def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (E return (mkApp f val, mkForall (← mkFreshBinderName) BinderInfo.default valType expectedTypeBody) /-- -Construct the resulting application after all discriminants have bee elaborated, and we have +Construct the resulting application after all discriminants have been elaborated, and we have consumed as many given arguments as possible. -/ def finalize : M Expr := do @@ -769,29 +773,50 @@ def finalize : M Expr := do throwError "failed to elaborate eliminator, unused named arguments: {(← get).namedArgs.map (·.name)}" let some motive := (← get).motive? | throwError "failed to elaborate eliminator, insufficient number of arguments" + trace[Elab.app.elab_as_elim] "motive: {motive}" forallTelescope (← get).fType fun xs _ => do + trace[Elab.app.elab_as_elim] "xs: {xs}" let mut expectedType := (← read).expectedType + trace[Elab.app.elab_as_elim] "expectedType:{indentD expectedType}" + let throwInsufficient := do + throwError "failed to elaborate eliminator, insufficient number of arguments, expected type:{indentExpr expectedType}" let mut f := (← get).f if xs.size > 0 then + -- under-application, specialize the expected type using `xs` assert! (← get).args.isEmpty - try - expectedType ← instantiateForall expectedType xs - catch _ => - throwError "failed to elaborate eliminator, insufficient number of arguments, expected type:{indentExpr expectedType}" + for x in xs do + let .forallE _ t b _ ← whnf expectedType | throwInsufficient + unless ← fullApproxDefEq <| isDefEq t (← inferType x) do + -- We can't assume that these binding domains were supposed to line up, so report insufficient arguments + throwInsufficient + expectedType := b.instantiate1 x + trace[Elab.app.elab_as_elim] "xs after specialization of expected type: {xs}" else - -- over-application, simulate `revert` + -- over-application, simulate `revert` while generalizing the values of these arguments in the expected type (f, expectedType) ← revertArgs (← get).args f expectedType + unless ← isTypeCorrect expectedType do + throwError "failed to elaborate eliminator, after generalizing over-applied arguments, expected type is type incorrect:{indentExpr expectedType}" + trace[Elab.app.elab_as_elim] "expectedType after processing:{indentD expectedType}" let result := mkAppN f xs + trace[Elab.app.elab_as_elim] "result:{indentD result}" let mut discrs := (← get).discrs let idx := (← get).idx - if (← get).discrs.size < (← read).elimInfo.targetsPos.size then + if discrs.any Option.isNone then for i in [idx:idx + xs.size], x in xs do - if (← read).elimInfo.targetsPos.contains i then - discrs := discrs.push x - let motiveVal ← mkMotive discrs expectedType + if let some tidx := (← read).elimInfo.targetsPos.indexOf? i then + discrs := discrs.set! tidx x + if let some idx := discrs.findIdx? Option.isNone then + -- This should not happen. + trace[Elab.app.elab_as_elim] "Internal error, missing target with index {idx}" + throwError "failed to elaborate eliminator, insufficient number of arguments" + trace[Elab.app.elab_as_elim] "discrs: {discrs.map Option.get!}" + let motiveVal ← mkMotive (discrs.map Option.get!) expectedType + unless (← isTypeCorrect motiveVal) do + throwError "failed to elaborate eliminator, motive is not type correct:{indentD motiveVal}" unless (← isDefEq motive motiveVal) do throwError "failed to elaborate eliminator, invalid motive{indentExpr motiveVal}" synthesizeAppInstMVars (← get).instMVars result + trace[Elab.app.elab_as_elim] "completed motive:{indentD motive}" let result ← mkLambdaFVars xs (← instantiateMVars result) return result @@ -819,9 +844,9 @@ def getNextArg? (binderName : Name) (binderInfo : BinderInfo) : M (LOption Arg) def setMotive (motive : Expr) : M Unit := modify fun s => { s with motive? := motive } -/-- Push the given expression into the `discrs` field in the state. -/ -def addDiscr (discr : Expr) : M Unit := - modify fun s => { s with discrs := s.discrs.push discr } +/-- Push the given expression into the `discrs` field in the state, where `i` is which target it is for. -/ +def addDiscr (i : Nat) (discr : Expr) : M Unit := + modify fun s => { s with discrs := s.discrs.set! i discr } /-- Elaborate the given argument with the given expected type. -/ private def elabArg (arg : Arg) (argExpectedType : Expr) : M Expr := do @@ -856,11 +881,11 @@ partial def main : M Expr := do let motive ← mkImplicitArg binderType binderInfo setMotive motive addArgAndContinue motive - else if (← read).elimInfo.targetsPos.contains idx then + else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then match (← getNextArg? binderName binderInfo) with - | .some arg => let discr ← elabArg arg binderType; addDiscr discr; addArgAndContinue discr + | .some arg => let discr ← elabArg arg binderType; addDiscr tidx discr; addArgAndContinue discr | .undef => finalize - | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr discr; addArgAndContinue discr + | .none => let discr ← mkImplicitArg binderType binderInfo; addDiscr tidx discr; addArgAndContinue discr else match (← getNextArg? binderName binderInfo) with | .some (.stx stx) => if (← read).extraArgsPos.contains idx then @@ -922,10 +947,12 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg) let expectedType ← instantiateMVars expectedType if expectedType.getAppFn.isMVar then throwError "failed to elaborate eliminator, expected type is not available" let extraArgsPos ← getElabAsElimExtraArgsPos elimInfo + trace[Elab.app.elab_as_elim] "extraArgsPos: {extraArgsPos}" ElabElim.main.run { elimInfo, expectedType, extraArgsPos } |>.run' { f, fType args := args.toList namedArgs := namedArgs.toList + discrs := mkArray elimInfo.targetsPos.size none } else ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport } |>.run' { @@ -955,19 +982,29 @@ where /-- Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`. - The idea is that the contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`. + The idea is that they contribute to motive inference. See comment at `ElamElim.Context.extraArgsPos`. -/ getElabAsElimExtraArgsPos (elimInfo : ElimInfo) : MetaM (Array Nat) := do forallTelescope elimInfo.elimType fun xs type => do - let resultArgs := type.getAppArgs + let targets := type.getAppArgs + /- Compute transitive closure of fvars appearing in the motive and the targets. -/ + let initMotiveFVars : CollectFVars.State := targets.foldl (init := {}) collectFVars + let motiveFVars ← xs.size.foldRevM (init := initMotiveFVars) fun i s => do + let x := xs[i]! + if elimInfo.motivePos == i || elimInfo.targetsPos.contains i || s.fvarSet.contains x.fvarId! then + return collectFVars s (← inferType x) + else + return s + /- Collect the extra argument positions -/ let mut extraArgsPos := #[] for i in [:xs.size] do let x := xs[i]! - unless elimInfo.targetsPos.contains i do - let xType ← inferType x + unless elimInfo.motivePos == i || elimInfo.targetsPos.contains i do + let xType ← x.fvarId!.getType /- We only consider "first-order" types because we can reliably "extract" information from them. -/ - if isFirstOrder xType - && Option.isSome (xType.find? fun e => e.isFVar && resultArgs.contains e) then + if motiveFVars.fvarSet.contains x.fvarId! + || (isFirstOrder xType + && Option.isSome (xType.find? fun e => e.isFVar && motiveFVars.fvarSet.contains e.fvarId!)) then extraArgsPos := extraArgsPos.push i return extraArgsPos @@ -1528,5 +1565,6 @@ builtin_initialize registerTraceClass `Elab.app.args (inherited := true) registerTraceClass `Elab.app.propagateExpectedType (inherited := true) registerTraceClass `Elab.app.finalize (inherited := true) + registerTraceClass `Elab.app.elab_as_elim (inherited := true) end Lean.Elab.Term diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean deleted file mode 100644 index da254e3a58ff..000000000000 --- a/tests/lean/elabAsElim.lean +++ /dev/null @@ -1,98 +0,0 @@ -inductive Vec (α : Type u) : Nat → Type u - | nil : Vec α 0 - | cons : α → Vec α n → Vec α (n+1) - -def f1 (xs : Vec α n) : Nat := - Vec.casesOn xs 0 fun _ _ => 1 - -def f2 (xs : Vec α n) : Nat := - xs.casesOn 0 -- Error insufficient number of arguments - -def f3 (x : Nat) : Nat → (Nat → Nat) → Nat := - x.casesOn - -def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 := - xs.casesOn (by intros; contradiction) (by intros; simp_arith) - -def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := - xs.casesOn (by intros; contradiction) (by intros; simp_arith) h - -def f6 (x : Nat) := - 2 * x.casesOn 0 id - -example : f6 (x+1) = 2*x := rfl - -def f7 (xs : Vec α n) : Nat := - xs.casesOn (a := 10) 0 -- Error unused named args - -def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 := - @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith) - -def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := - xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h - -example (h₁ : a = b) (h₂ : b = c) : a = c := - Eq.rec h₂ h₁.symm - -@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by - cases h₁ - assumption - -example (h₁ : a = b) (h₂ : b = c) : a = c := - subst h₁.symm h₂ - -theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ => - h.rec (λ h1 => h1 hp) (λ h2 => h2 hq) - -structure Point where - x : Nat - -theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q := - Point.recOn p <| - fun z1 q => Point.recOn q $ - fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA - -inductive pos_num : Type - | one : pos_num - | bit1 : pos_num → pos_num - | bit0 : pos_num → pos_num - -inductive num : Type - | zero : num - | pos : pos_num → num - -inductive znum : Type - | zero : znum - | pos : pos_num → znum - | neg : pos_num → znum - -def pos_num.pred' : pos_num → num - | one => .zero - | bit0 n => num.pos (num.casesOn (pred' n) one bit1) - | bit1 n => num.pos (bit0 n) - -protected def znum.bit1 : znum → znum - | zero => pos .one - | pos n => pos (pos_num.bit1 n) - | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1) - -example (h : False) : a = c := - h.rec - -example (h : False) : a = c := - h.elim - -noncomputable def f : Nat → Nat := - Nat.rec 0 (fun x _ => x) - -example : ∀ x, x ≥ 0 := - Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih) - -@[elab_as_elim] -def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry - -example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct - -example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct - -example {n : Type} : {T : n} → T = T := @(Foo.induction n) diff --git a/tests/lean/elabAsElim.lean.expected.out b/tests/lean/elabAsElim.lean.expected.out deleted file mode 100644 index 07450ee1193e..000000000000 --- a/tests/lean/elabAsElim.lean.expected.out +++ /dev/null @@ -1,8 +0,0 @@ -elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type: - Nat -elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a] -elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry' -elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct: - fun x => T = T -elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct: - fun x => T✝ = T✝ diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean new file mode 100644 index 000000000000..b76607fcf5d1 --- /dev/null +++ b/tests/lean/run/elabAsElim.lean @@ -0,0 +1,177 @@ +/-! +# Tests of elabAsElim elaborator and the `elab_as_elim` attribute +-/ + +-- For debugging: +-- set_option trace.Elab.app.elab_as_elim true + +inductive Vec (α : Type u) : Nat → Type u + | nil : Vec α 0 + | cons : α → Vec α n → Vec α (n+1) + +def f1 (xs : Vec α n) : Nat := + Vec.casesOn xs 0 fun _ _ => 1 + +/-! Under-applied eliminator, and expected type isn't a pi type. -/ +/-- +error: failed to elaborate eliminator, insufficient number of arguments, expected type: + Nat +-/ +#guard_msgs in +def f2 (xs : Vec α n) : Nat := + xs.casesOn 0 + +def f3 (x : Nat) : Nat → (Nat → Nat) → Nat := + x.casesOn + +/-! Under-applied eliminator, expected type's binders do not unify with remaining arguments. -/ +/-- +error: failed to elaborate eliminator, insufficient number of arguments, expected type: + (Nat → Nat) → Nat → Nat +-/ +#guard_msgs in +def f3' (x : Nat) : (Nat → Nat) → Nat → Nat := + x.casesOn + +def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 := + xs.casesOn (by intros; contradiction) (by intros; simp_arith) + +def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := + xs.casesOn (by intros; contradiction) (by intros; simp_arith) h + +def f6 (x : Nat) := + 2 * x.casesOn 0 id + +example : f6 (x+1) = 2*x := rfl + +/-- error: failed to elaborate eliminator, unused named arguments: [a] -/ +#guard_msgs in +def f7 (xs : Vec α n) : Nat := + xs.casesOn (a := 10) 0 + +def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 := + @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith) + +def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := + xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h + +example (h₁ : a = b) (h₂ : b = c) : a = c := + Eq.rec h₂ h₁.symm + +@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by + cases h₁ + assumption + +example (h₁ : a = b) (h₂ : b = c) : a = c := + subst h₁.symm h₂ + +theorem not_or_not : (¬p ∨ ¬q) → ¬(p ∧ q) := λ h ⟨hp, hq⟩ => + h.rec (λ h1 => h1 hp) (λ h2 => h2 hq) + +structure Point where + x : Nat + +theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q := + Point.recOn p <| + fun z1 q => Point.recOn q $ + fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA + +inductive pos_num : Type + | one : pos_num + | bit1 : pos_num → pos_num + | bit0 : pos_num → pos_num + +inductive num : Type + | zero : num + | pos : pos_num → num + +inductive znum : Type + | zero : znum + | pos : pos_num → znum + | neg : pos_num → znum + +def pos_num.pred' : pos_num → num + | one => .zero + | bit0 n => num.pos (num.casesOn (pred' n) one bit1) + | bit1 n => num.pos (bit0 n) + +protected def znum.bit1 : znum → znum + | zero => pos .one + | pos n => pos (pos_num.bit1 n) + | neg n => neg (num.casesOn (pos_num.pred' n) .one pos_num.bit1) + +example (h : False) : a = c := + h.rec + +example (h : False) : a = c := + h.elim + +noncomputable def f : Nat → Nat := + Nat.rec 0 (fun x _ => x) + +example : ∀ x, x ≥ 0 := + Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih) + +/-! +Tests of `@[elab_as_elim]` when the motive is not type correct. +-/ + +@[elab_as_elim] +def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry + +/-- +error: failed to elaborate eliminator, motive is not type correct: + fun x => T = T +-/ +#guard_msgs in +example {n : Type} {T : n} : T = T := Foo.induction n + +/-- +error: failed to elaborate eliminator, motive is not type correct: + fun x => T✝ = T✝ +-/ +#guard_msgs in +example {n : Type} : {T : n} → T = T := Foo.induction n + +example {n : Type} : (T : n) → T = T := Foo.induction n + +-- Disable implicit lambda +example {n : Type} : {T : n} → T = T := @(Foo.induction n) + +/-! +A "motive is not type correct" regression test. +The `isEmptyElim` was failing due to being under-applied and the named `(α := α)` argument +having postponed elaboration. This fix is that `α` now elaborates eagerly. +-/ + +class IsEmpty (α : Sort u) : Prop where + protected false : α → False + +@[elab_as_elim] +def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a := + (IsEmpty.false a).elim + +def Set (α : Type u) := α → Prop +def Set.univ {α : Type _} : Set α := fun _ => True +instance : Membership α (Set α) := ⟨fun x s => s x⟩ +def Set.pi {α : ι → Type _} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i) := fun f => ∀ i ∈ s, f i ∈ t i + +example {α : Type u} [IsEmpty α] {β : α → Type v} (x : (a : α) → β a) (s : (i : α) → Set (β i)) : + x ∈ Set.univ.pi s := isEmptyElim (α := α) + +-- Simplified version: +example {α : Type _} [IsEmpty α] : + id (α → False) := isEmptyElim (α := α) + +/-! +From mathlib, regression test. Need to eagerly elaborate the `n ≤ m` argument to deduce `m` +before computing the motive. +-/ + +@[elab_as_elim] +def leRecOn {C : Nat → Sort _} {n : Nat} : ∀ {m}, n ≤ m → (∀ {k}, C k → C (k + 1)) → C n → C m := + sorry + +theorem leRecOn_self {C : Nat → Sort _} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) : + (leRecOn n.le_refl next x : C n) = x := + sorry