max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: unfolding functional induction principles (#8088)

Browse source 
This PR adds the “unfolding” variant of the functional induction and
functional cases principles, under the name `foo.induct_unfolding` resp.
`foo.fun_cases_unfolding`. These theorems combine induction over the
structure of a recursive function with the unfolding of that function,
and should be more reliable, easier to use and more efficient than just
case-splitting and then rewriting with equational theorems.

For example  instead of
```
ackermann.induct
  (motive : Nat → Nat → Prop)
  (case1 : ∀ (m : Nat), motive 0 m)
  (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
  (x x : Nat) : motive x x
```
one gets
```
ackermann.fun_cases_unfolding
  (motive : Nat → Nat → Nat → Prop)
  (case1 : ∀ (m : Nat), motive 0 m (m + 1))
  (case2 : ∀ (n : Nat), motive n.succ 0 (ackermann n 1))
  (case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m)))
  (x✝ x✝¹ : Nat) : motive x✝ x✝¹ (ackermann x✝ x✝¹)
```
This commit is contained in:
Joachim Breitner 2025-04-29 18:43:06 +02:00 • committed by GitHub
parent b5cfd86a89
commit 3d1d8fc1de
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 880 additions and 158 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Lean/Elab/PreDefinition/Eqns.lean
View file

@ -469,31 +469,6 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
throwError "failed to generate unfold theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
go mvarId
/-- Generate the "unfold" lemma for `declName`. -/
def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := do
let name := Name.str declName unfoldThmSuffix
realizeConst declName name (doRealize name)
return name
where
doRealize name := withOptions (tactic.hygienic.set · false) do
lambdaTelescope info.value fun xs body => do
let us := info.levelParams.map mkLevelParam
let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
let goal ← mkFreshExprSyntheticOpaqueMVar type
mkUnfoldProof declName goal.mvarId!
let type ← mkForallFVars xs type
let value ← mkLambdaFVars xs (← instantiateMVars goal)
addDecl <| Declaration.thmDecl {
name, type, value
levelParams := info.levelParams
}
def getUnfoldFor? (declName : Name) (getInfo? : Unit → Option EqnInfoCore) : MetaM (Option Name) := do
if let some info := getInfo? () then
return some (← mkUnfoldEq declName info)
else
return none
builtin_initialize
registerTraceClass `Elab.definition.unfoldEqn
registerTraceClass `Elab.definition.eqns

4
src/Lean/Elab/PreDefinition/Mutual.lean
View file

@ -63,8 +63,12 @@ Assign final attributes to the definitions. Assumes the EqnInfos to be already p
def addPreDefAttributes (preDefs : Array PreDefinition) : TermElabM Unit := do
for preDef in preDefs do
markAsRecursive preDef.declName
for preDef in preDefs.reverse do
-- must happen before `generateEagerEqns`
-- must happen in reverse order so that constants realized as part of the first decl
-- have realizations for the other ones enabled
enableRealizationsForConst preDef.declName
for preDef in preDefs do
generateEagerEqns preDef.declName
applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
-- Unless the user asks for something else, mark the definition as irreducible

27
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View file

@ -77,7 +77,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
thmNames := thmNames.push name
-- determinism: `type` should be independent of the environment changes since `baseName` was
-- added
realizeConst baseName name (doRealize name type)
realizeConst info.declNames[0]! name (doRealize name type)
return thmNames
where
doRealize name type := withOptions (tactic.hygienic.set · false) do
@ -102,9 +102,30 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
else
return none
/-- Generate the "unfold" lemma for `declName`. -/
def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
let name := Name.str declName unfoldThmSuffix
realizeConst info.declNames[0]! name (doRealize name)
return name
where
doRealize name := withOptions (tactic.hygienic.set · false) do
lambdaTelescope info.value fun xs body => do
let us := info.levelParams.map mkLevelParam
let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
let goal ← mkFreshExprSyntheticOpaqueMVar type
mkUnfoldProof declName goal.mvarId!
let type ← mkForallFVars xs type
let value ← mkLambdaFVars xs (← instantiateMVars goal)
addDecl <| Declaration.thmDecl {
name, type, value
levelParams := info.levelParams
}
def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
let env ← getEnv
Eqns.getUnfoldFor? declName fun _ => eqnInfoExt.find? env declName |>.map (·.toEqnInfoCore)
if let some info := eqnInfoExt.find? (← getEnv) declName then
return some (← mkUnfoldEq declName info)
else
return none
@[export lean_get_structural_rec_arg_pos]
def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do

55
src/Lean/Meta/ArgsPacker.lean
View file

@ -176,22 +176,32 @@ def uncurry (varNames : Array Name) (e : Expr) : MetaM Expr := do
let value ← casesOn varNames.toList x u codomain e
mkLambdaFVars #[x] value
/-- Given `(A ⊗' B ⊗' … ⊗' D) → R` (non-dependent) `R`, return `A → B → … → D → R` -/
/--
Given type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]`
return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]`
-/
private def curryType (varNames : Array Name) (type : Expr) : MetaM Expr := do
let some (domain, codomain) := type.arrow? |
throwError "curryType: Expected arrow type, got {type}"
go codomain varNames.toList domain
unless type.isForall do
throwError "curryType: Expected forall type, got {type}"
let packedDomain := type.bindingDomain!
go packedDomain packedDomain #[] varNames.toList
where
go (codomain : Expr) : List Name → Expr → MetaM Expr
| [], _ => pure codomain
| [_], domain => mkArrow domain codomain
| n::ns, domain =>
go (packedDomain domain : Expr) args : List Name → MetaM Expr
| [] => do
let packedArg := Unary.pack packedDomain args
instantiateForall type #[packedArg]
| [n] => do
withLocalDeclD n domain fun x => do
let dummy := Expr.const ``Unit []
mkForallFVars #[x] (← go packedDomain dummy (args.push x) [])
| n :: ns =>
match_expr domain with
| PSigma a b =>
withLocalDecl n .default a fun x => do
mkForallFVars #[x] (← go codomain ns (b.beta #[x]))
withLocalDeclD n a fun x => do
mkForallFVars #[x] (← go packedDomain (b.beta #[x]) (args.push x) ns)
| _ => throwError "curryType: Expected PSigma type, got {domain}"
/--
Given expression `e` of type `(x : A ⊗' B ⊗' … ⊗' D) → R[x]`
return expression of type `(x : A) → (y : B) → … → (z : D) → R[(x,y,z)]`
@ -420,16 +430,19 @@ def uncurryND (es : Array Expr) : MetaM Expr := do
mkLambdaFVars #[x] value
/-
Given type `(A ⊕' C) → R` (non-depenent), return types
Given type `(A ⊕' C) → R` (possibly depenent), return types
```
#[A → R, B → R]
```
-/
def curryType (n : Nat) (type : Expr) : MetaM (Array Expr) := do
let some (domain, codomain) := type.arrow? |
throwError "curryType: Expected arrow type, got {type}"
unless type.isForall do
throwError "curryType: Expected forall type, got {type}"
let domain := type.bindingDomain!
let ds ← unpackType n domain
ds.toArray.mapM (fun d => mkArrow d codomain)
ds.toArray.mapIdxM fun i d =>
withLocalDeclD `x d fun x => do
mkForallFVars #[x] (← instantiateForall type #[← pack ds.length domain i x])
end Mutual
@ -528,7 +541,7 @@ def curryProj (argsPacker : ArgsPacker) (e : Expr) (i : Nat) : MetaM Expr := do
/--
Given type `(x : a ⊗' b ⊕' c ⊗' d) → R` (non-dependent), return types
Given type `(x : a ⊗' b ⊕' c ⊗' d) → R` (dependent), return types
```
#[(x: a) → (y : b) → R, (x : c) → (y : d) → R]
```
@ -569,9 +582,9 @@ where
/--
Given `value : type` where `type` is
```
(m : a ⊗' b ⊕' c ⊗' d → s) → r[m]
(m : (x : a ⊗' b ⊕' c ⊗' d) → s[x]) → r[m]
```
brings `m1 : a → b → s` and `m2 : c → d → s` into scope. The continuation receives
brings `m1 : (x : a) → (y : b) → s[.inl ⟨x,y⟩]` and `m2 : (x : c) → (y : d) → s[.inr ⟨x,y⟩]` into scope. The continuation receives
* FVars for `m1`…
* `e[m]`
@ -585,14 +598,14 @@ unless `numFuns = 1`
def curryParam {α} (argsPacker : ArgsPacker) (value : Expr) (type : Expr)
(k : Array Expr → Expr → Expr → MetaM α) : MetaM α := do
unless type.isForall do
throwError "uncurryParam: expected forall, got {type}"
throwError "curryParam: expected forall, got {type}"
let packedMotiveType := type.bindingDomain!
unless packedMotiveType.isArrow do
throwError "uncurryParam: unexpected packed motive {packedMotiveType}"
unless packedMotiveType.isForall do
throwError "curryParam: unexpected packed motive, not a forall{indentExpr packedMotiveType}"
-- Bring unpacked motives (motive1 : a → b → Prop and motive2 : c → d → Prop) into scope
withCurriedDecl argsPacker type.bindingName! packedMotiveType fun motives => do
-- Combine them into a packed motive (motive : a ⊗' b ⊕' c ⊗' d → Prop), and use that
let motive ← argsPacker.uncurryND motives
let motive ← argsPacker.uncurryWithType packedMotiveType motives
let type ← instantiateForall type #[motive]
let value := mkApp value motive
k motives value type

348
src/Lean/Meta/Tactic/FunInd.lean
View file

@ -175,6 +175,32 @@ differences:
* The elaboration of structurally recursive function can handle extra arguments. We keep the
`motive` parameters in the original order.
## Unfolding principles
The code can also create a variant of the induction/cases principles that automatially unfolds
the function application. It's motive abstracts over the function call, so for the ackermann
function one gets
```
ackermann.fun_cases_unfolding
(motive : Nat → Nat → Nat → Prop)
(case1 : ∀ (m : Nat), motive 0 m (m + 1))
(case2 : ∀ (n : Nat), motive n.succ 0 (ackermann n 1))
(case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m)))
(x✝ x✝¹ : Nat) : motive x✝ x✝¹ (ackermann x✝ x✝¹)
```
To implement this, in the inital goal `motive x (ackermann x)` of `buildInductionBody` we unfold the
function definition, and then reduce is as we go into match, ite or let expressions, using the
`withRewrittenMotive` function.
This gives us great control over the reduction, for example to move `let` expressions to the context
simultaneously.
The combinators passed to `withRewrittenMotive` are forgiving, so when `unfolding := false`, or when
something goes wrong, one still gets a useful induction principle, just maybe with the function
not fully simplified.
-/
set_option autoImplicit false
@ -382,7 +408,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
assert! fvar == oldIH
pure <| mkFVar newIH
-- Now see if the type o/--f the expression we are building is a motive application.
-- Now see if the type of the expression we are building is a motive application.
-- If it is we want to replace it with the corresponding function application,
-- and remember the expression as a IH to be used in an inductive case.
@ -528,6 +554,120 @@ def maskArray {α} (mask : Array Bool) (xs : Array α) : Array α := Id.run do
return ys
/--
Applies `rw` to `goal`, passes the rewritten `goal'` to `k` (which should return an expression of
type `goal'`), and wraps that using the proof from `rw`.
-/
def withRewrittenMotive (goal : Expr) (rw : Expr → MetaM Simp.Result) (k : Expr → M2 Expr) : M2 Expr := do
let r ← rw goal
let e ← k r.expr
r.mkEqMPR e
def inLastArg (rw : Expr → MetaM Simp.Result) (goal : Expr) : MetaM Simp.Result := do
match goal with
| .app goalFn arg =>
let r ← rw arg
Simp.mkCongrArg goalFn r
| _ =>
return { expr := goal }
/--
If `goal` is of the form `motive a b e`, applies `rw` to `e`, passes the simplified
`goal'` to `k` (which should return an expression of type `goal'`), and rewrites that term
accordingly.
-/
def withRewrittenMotiveArg (goal : Expr) (rw : Expr → MetaM Simp.Result) (k : Expr → M2 Expr) : M2 Expr := do
withRewrittenMotive goal (inLastArg rw) k
/--
Use to write inside the packed motives used for mutual structural recursion.
-/
partial def inProdLambdaLastArg (rw : Expr → MetaM Simp.Result) (goal : Expr) : MetaM Simp.Result := do
match_expr goal with
| PProd.mk _ _ goal1 goal2 =>
let r1 ← inProdLambdaLastArg rw goal1
let r2 ← inProdLambdaLastArg rw goal2
let f := goal.appFn!.appFn!
Simp.mkCongr (← Simp.mkCongrArg f r1) r2
| _ =>
lambdaTelescope goal fun xs goal => do
let r ← inLastArg rw goal
r.addLambdas xs
def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
match_expr e with
| ite@ite α c h t f =>
let us := ite.constLevels!
if (← isDefEq c (← inferType hc)) then
return {
expr := t
proof? := (mkAppN (mkConst ``if_pos us) #[c, h, hc, α, t, f])
}
if (← isDefEq (mkNot c) (← inferType hc)) then
return {
expr := f
proof? := (mkAppN (mkConst ``if_neg us) #[c, h, hc, α, t, f])
}
else
return { expr := e}
| dite@dite α c h t f =>
let us := dite.constLevels!
if (← isDefEq c (← inferType hc)) then
return {
expr := t.beta #[hc]
proof? := (mkAppN (mkConst ``dif_pos us) #[c, h, hc, α, t, f])
}
if (← isDefEq (mkNot c) (← inferType hc)) then
return {
expr := f.beta #[hc]
proof? := (mkAppN (mkConst ``dif_neg us) #[c, h, hc, α, t, f])
}
else
return { expr := e }
| _ =>
return { expr := e }
def rwLetWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
if e.isLet then
if (← isDefEq e.letValue! h) then
return { expr := e.letBody!.instantiate1 h }
return { expr := e }
def rwHaveWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
if let some (_n, t, _v, b) := e.letFun? then
if (← isDefEq t (← inferType h)) then
return { expr := b.instantiate1 h }
return { expr := e }
def rwFun (names : Array Name) (e : Expr) : MetaM Simp.Result := do
e.withApp fun f xs => do
if let some name := names.find? f.isConstOf then
let some unfoldThm ← getUnfoldEqnFor? name (nonRec := true)
| return { expr := e }
let h := mkAppN (mkConst unfoldThm f.constLevels!) xs
let some (_, _, rhs) := (← inferType h).eq?
| throwError "Not an equality: {h}"
return { expr := rhs, proof? := h }
else
return { expr := e }
def rwMatcher (e : Expr) : MetaM Simp.Result := do
if e.isAppOf ``PSum.casesOn || e.isAppOf ``PSigma.casesOn then
let mut e := e
while true do
if let some e' ← reduceRecMatcher? e then
e := e'.headBeta
else
let e' := e.headBeta
if e != e' then
e := e'
else
break
return { expr := e }
else
Split.simpMatch e
/--
Builds an expression of type `goal` by replicating the expression `e` into its tail-call-positions,
where it calls `buildInductionCase`. Collects the cases of the final induction hypothesis
as `MVars` as it goes.
@ -543,10 +683,12 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
let c' ← foldAndCollect oldIH newIH isRecCall c
let h' ← foldAndCollect oldIH newIH isRecCall h
let t' ← withLocalDecl `h .default c' fun h => M2.branch do
let t' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall t
let t' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
buildInductionBody toErase toClear goal' oldIH newIH isRecCall t
mkLambdaFVars #[h] t'
let f' ← withLocalDecl `h .default (mkNot c') fun h => M2.branch do
let f' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall f
let f' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
buildInductionBody toErase toClear goal' oldIH newIH isRecCall f
mkLambdaFVars #[h] f'
let u ← getLevel goal
return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@ -555,11 +697,13 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
let h' ← foldAndCollect oldIH newIH isRecCall h
let t' ← withLocalDecl `h .default c' fun h => M2.branch do
let t ← instantiateLambda t #[h]
let t' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall t
let t' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
buildInductionBody toErase toClear goal' oldIH newIH isRecCall t
mkLambdaFVars #[h] t'
let f' ← withLocalDecl `h .default (mkNot c') fun h => M2.branch do
let f ← instantiateLambda f #[h]
let f' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall f
let f' ← withRewrittenMotiveArg goal (rwIfWith h) fun goal' =>
buildInductionBody toErase toClear goal' oldIH newIH isRecCall f
mkLambdaFVars #[h] f'
let u ← getLevel goal
return mkApp5 (mkConst ``dite [u]) goal c' h' t' f'
@ -608,7 +752,9 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
let #[newIH'] := newIH' | unreachable!
let toErase' := toErase ++ #[oldIH', newIH'.fvarId!]
let toClear' := toClear ++ matcherApp.discrs.filterMap (·.fvarId?)
let alt' ← buildInductionBody toErase' toClear' goal' oldIH' newIH'.fvarId! isRecCall alt
let alt' ← withRewrittenMotiveArg goal' rwMatcher fun goal'' => do
-- logInfo m!"rwMatcher after {matcherApp.matcherName} on{indentExpr goal'}\nyields{indentExpr goal''}"
buildInductionBody toErase' toClear' goal'' oldIH' newIH'.fvarId! isRecCall alt
mkLambdaFVars #[newIH'] alt')
(onRemaining := fun _ => pure #[.fvar newIH])
return matcherApp'.toExpr
@ -624,7 +770,8 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
(onParams := (foldAndCollect oldIH newIH isRecCall ·))
(onMotive := fun xs _body => pure (absMotiveBody.beta (maskArray mask xs)))
(onAlt := fun expAltType alt => M2.branch do
buildInductionBody toErase toClear expAltType oldIH newIH isRecCall alt)
withRewrittenMotiveArg expAltType Split.simpMatch fun expAltType' =>
buildInductionBody toErase toClear expAltType' oldIH newIH isRecCall alt)
return matcherApp'.toExpr
-- we look through mdata
@ -636,14 +783,16 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
let t' ← foldAndCollect oldIH newIH isRecCall t
let v' ← foldAndCollect oldIH newIH isRecCall v
return ← withLetDecl n t' v' fun x => M2.branch do
let b' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall (b.instantiate1 x)
let b' ← withRewrittenMotiveArg goal (rwLetWith x) fun goal' =>
buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
mkLetFVars #[x] b'
if let some (n, t, v, b) := e.letFun? then
let t' ← foldAndCollect oldIH newIH isRecCall t
let v' ← foldAndCollect oldIH newIH isRecCall v
return ← withLocalDeclD n t' fun x => M2.branch do
let b' ← buildInductionBody toErase toClear goal oldIH newIH isRecCall (b.instantiate1 x)
let b' ← withRewrittenMotiveArg goal (rwHaveWith x) fun goal' =>
buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
mkLetFun x v' b'
-- Special case for traversing the PProd’ed bodies in our encoding of structural mutual recursion
@ -696,8 +845,8 @@ def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : M
Given a unary definition `foo` defined via `WellFounded.fixF`, derive a suitable induction principle
`foo.induct` for it. See module doc for details.
-/
def deriveUnaryInduction (name : Name) : MetaM Name := do
let inductName := getFunInductName name
def deriveUnaryInduction (unfolding : Bool) (name : Name) : MetaM Name := do
let inductName := getFunInductName (unfolding := unfolding) name
realizeConst name inductName (doRealize inductName)
return inductName
where doRealize (inductName : Name) := do
@ -721,17 +870,29 @@ where doRealize (inductName : Name) := do
unless params.back! == target do
throwError "functional induction: expected the target as last parameter{indentExpr e}"
let fixedParamPerms := params.pop
let motiveType ← mkForallFVars #[target] (.sort levelZero)
let motiveType ←
if unfolding then
withLocalDeclD `r (← instantiateForall info.type params) fun r =>
mkForallFVars #[target, r] (.sort 0)
else
mkForallFVars #[target] (.sort 0)
withLocalDeclD `motive motiveType fun motive => do
let fn := mkAppN (← mkConstWithLevelParams name) fixedParamPerms
let isRecCall : Expr → Option Expr := fun e =>
if e.isApp && e.appFn!.isFVarOf motive.fvarId! then
mkApp fn e.appArg!
e.withApp fun f xs =>
if f.isFVarOf motive.fvarId! && xs.size > 0 then
mkApp fn xs[0]!
else
none
let motiveArg ←
if unfolding then
let motiveArg := mkApp2 motive target (mkAppN (← mkConstWithLevelParams name) params)
mkLambdaFVars #[target] motiveArg
else
pure motive
let e' := .const ``WellFounded.fix [fix.constLevels![0]!, levelZero]
let e' := mkApp4 e' α motive rel wf
let e' := mkApp4 e' α motiveArg rel wf
check e'
let (body', mvars) ← M2.run do
forallTelescope (← inferType e').bindingDomain! fun xs goal => do
@ -744,7 +905,8 @@ where doRealize (inductName : Name) := do
let body ← instantiateLambda body targets
lambdaTelescope1 body fun oldIH body => do
let body ← instantiateLambda body extraParams
let body' ← buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
let body' ← withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
buildInductionBody #[oldIH, 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')
@ -792,10 +954,10 @@ where doRealize (inductName : Name) := do
Given a realizer for `foo.mutual_induct`, defines `foo.induct`, `bar.induct` etc.
Used for well-founded and structural recursion.
-/
def projectMutualInduct (names : Array Name) (mutualInduct : MetaM Name) (finalizeFirstInd : MetaM Unit) : MetaM Unit := do
def projectMutualInduct (unfolding : Bool) (names : Array Name) (mutualInduct : MetaM Name) (finalizeFirstInd : MetaM Unit) : MetaM Unit := do
for name in names, idx in [:names.size] do
let inductName := getFunInductName name
realizeConst name inductName do
let inductName := getFunInductName (unfolding := unfolding) name
realizeConst names[0]! inductName do
let ci ← getConstInfo (← mutualInduct)
let levelParams := ci.levelParams
let value ← forallTelescope ci.type fun xs _body => do
@ -812,9 +974,9 @@ def projectMutualInduct (names : Array Name) (mutualInduct : MetaM Name) (finali
For a (non-mutual!) definition of `name`, uses the `FunIndInfo` associated with the `unaryInduct` and
derives the one for the n-ary function.
-/
def setNaryFunIndInfo (fixedParamPerms : FixedParamPerms) (name : Name) (unaryInduct : Name) : MetaM Unit := do
def setNaryFunIndInfo (unfolding : Bool) (fixedParamPerms : FixedParamPerms) (name : Name) (unaryInduct : Name) : MetaM Unit := do
assert! fixedParamPerms.perms.size = 1 -- only non-mutual for now
let funIndName := getFunInductName name
let funIndName := getFunInductName (unfolding := unfolding) name
unless funIndName = unaryInduct do
let some unaryFunIndInfo ← getFunIndInfoForInduct? unaryInduct
| throwError "Expected {unaryInduct} to have FunIndInfo"
@ -894,22 +1056,22 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
Retrieves `foo._unary.induct`, where the motive is a `PSigma`/`PSum` type, and
unpacks it into a n-ary and (possibly) joint induction principle.
-/
def unpackMutualInduction (eqnInfo : WF.EqnInfo) : MetaM Name := do
def unpackMutualInduction (unfolding : Bool) (eqnInfo : WF.EqnInfo) : MetaM Name := do
let inductName := if eqnInfo.declNames.size > 1 then
getMutualInductName eqnInfo.declNames[0]!
getMutualInductName (unfolding := unfolding) eqnInfo.declNames[0]!
else
-- If there is no mutual recursion, we generate the `foo.induct` directly.
getFunInductName eqnInfo.declNames[0]!
getFunInductName (unfolding := unfolding) eqnInfo.declNames[0]!
realizeConst eqnInfo.declNames[0]! inductName (doRealize inductName)
return inductName
where doRealize inductName := do
let unaryInductName ← deriveUnaryInduction eqnInfo.declNameNonRec
let unaryInductName ← deriveUnaryInduction (unfolding := unfolding) eqnInfo.declNameNonRec
mapError (f := (m!"Cannot unpack functional cases principle {.ofConstName unaryInductName} (please report this issue)\n{indentD ·}")) do
let ci ← getConstInfo unaryInductName
let us := ci.levelParams
let value := .const ci.name (us.map mkLevelParam)
let motivePos ← forallTelescope ci.type fun xs concl => concl.withApp fun motive targets => do
unless motive.isFVar && targets.size = 1 && targets.all (·.isFVar) do
unless motive.isFVar && targets.size = (if unfolding then 2 else 1) && targets[0]!.isFVar do
throwError "conclusion {concl} does not look like a packed motive application"
let packedTarget := targets[0]!
unless xs.back! == packedTarget do
@ -942,7 +1104,7 @@ where doRealize inductName := do
{ name := inductName, levelParams := ci.levelParams, type, value }
if eqnInfo.argsPacker.numFuncs = 1 then
setNaryFunIndInfo eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
setNaryFunIndInfo (unfolding := unfolding) eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
def withLetDecls {α} (name : Name) (ts : Array Expr) (es : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do
assert! es.size = ts.size
@ -960,12 +1122,12 @@ Given a recursive definition `foo` defined via structural recursion, derive `foo
if needed, and `foo.induct` for all functions in the group.
See module doc for details.
-/
def deriveInductionStructural (names : Array Name) (fixedParamPerms : FixedParamPerms) : MetaM Name := do
def deriveInductionStructural (unfolding : Bool) (names : Array Name) (fixedParamPerms : FixedParamPerms) : MetaM Name := do
let inductName :=
if names.size = 1 then
getFunInductName names[0]!
getFunInductName (unfolding := unfolding) names[0]!
else
getMutualInductName names[0]!
getMutualInductName (unfolding := unfolding) names[0]!
realizeConst names[0]! inductName (doRealize inductName)
return inductName
where doRealize inductName := do
@ -1050,11 +1212,16 @@ where doRealize inductName := do
-- Calculate the types of the induction motives (natural argument order) for each function
let motiveTypes ← infos.mapIdxM fun funIdx info => do
lambdaTelescope (← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs) fun ys _ =>
mkForallFVars ys (.sort levelZero)
let motiveArities ← infos.mapIdxM fun funIdx info => do
lambdaTelescope (← fixedParamPerms.perms[funIdx]!.instantiateLambda info.value xs) fun ys _ =>
pure ys.size
let funType ← fixedParamPerms.perms[funIdx]!.instantiateForall info.type xs
forallBoundedTelescope funType (some (fixedParamPerms.perms[funIdx]!.size - xs.size)) fun ys rType => do
if unfolding then
withLocalDeclD `r rType fun r =>
mkForallFVars (ys.push r) (.sort 0)
else
mkForallFVars ys (.sort 0)
trace[Meta.FunInd] m!"motiveTypes: {motiveTypes}"
let motiveArities ← motiveTypes.mapM fun motiveType =>
forallTelescope motiveType fun ys _ => pure ys.size
let motiveNames := Array.ofFn (n := infos.size) fun ⟨i, _⟩ =>
if infos.size = 1 then .mkSimple "motive" else .mkSimple s!"motive_{i+1}"
@ -1065,15 +1232,27 @@ where doRealize inductName := do
if let .some funIdx := motives.idxOf? e.getAppFn then
if e.getAppNumArgs = motiveArities[funIdx]! then
let info := infos[funIdx]!
let args := fixedParamPerms.perms[funIdx]!.buildArgs xs e.getAppArgs
let args := if unfolding then e.getAppArgs.pop else e.getAppArgs
let args := fixedParamPerms.perms[funIdx]!.buildArgs xs args
return mkAppN (.const info.name (info.levelParams.map mkLevelParam)) args
.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
-- Motives with parameters reordered, to put indices and major first,
-- and (when unfolding) the result field instantiated
let mut brecMotives := #[]
for motive in motives, recArgInfo in recArgInfos, info in infos, funIdx in [:motives.size] do
let brecMotive ← forallTelescope (← inferType motive) fun ys _ => do
let ys := if unfolding then ys.pop else ys
let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys
mkLambdaFVars indicesMajor (← mkForallFVars rest (mkAppN motive ys))
let motiveArg := mkAppN motive ys
let motiveArg ← if unfolding then
let args := fixedParamPerms.perms[funIdx]!.buildArgs xs ys
let fnCall := mkAppN (.const info.name (info.levelParams.map mkLevelParam)) args
pure <| mkApp motiveArg fnCall
else
pure motiveArg
mkLambdaFVars indicesMajor (← mkForallFVars rest motiveArg)
brecMotives := brecMotives.push brecMotive
-- We need to pack these motives according to the `positions` assignment.
let packedMotives ← positions.mapMwith PProdN.packLambdas brecMotiveTypes brecMotives
@ -1098,7 +1277,9 @@ where doRealize inductName := do
lambdaTelescope1 body fun oldIH body => do
trace[Meta.FunInd] "replacing {Expr.fvar oldIH} with {genIH}"
let body ← instantiateLambda body extraParams
let body' ← buildInductionBody #[oldIH, genIH.fvarId!] #[] goal oldIH genIH.fvarId! isRecCall body
let body' ←
withRewrittenMotive goal (inProdLambdaLastArg (rwFun names)) fun goal' =>
buildInductionBody #[oldIH, 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')
@ -1188,39 +1369,44 @@ In the future, we might post-process the theorem (or run the code below iterativ
targets that are unchanged in each case, so simplify applying the lemma when these “fixed” parameters
are not variables, to avoid having to generalize them.
-/
def deriveCases (name : Name) : MetaM Unit := do
let casesName := getFunCasesName name
def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do
let casesName := getFunCasesName (unfolding := unfolding) name
realizeConst name casesName do
mapError (f := (m!"Cannot derive functional cases principle (please report this issue)\n{indentD ·}")) do
let info ← getConstInfo name
let value ←
if let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := false) name then
let eqInfo ← getConstInfo unfoldEqnName
forallTelescope eqInfo.type fun xs body => do
let some (_, _, rhs) := body.eq?
| throwError "Type of {unfoldEqnName} not an equality: {body}"
mkLambdaFVars xs rhs
else if let some value := info.value? then
pure value
else
throwError "'{name}' does not have an unfold theorem nor a value"
let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) name
| throwError "'{name}' does not have an unfold theorem nor a value"
let value ← do
let eqInfo ← getConstInfo unfoldEqnName
forallTelescope eqInfo.type fun xs body => do
let some (_, _, rhs) := body.eq?
| throwError "Type of {unfoldEqnName} not an equality: {body}"
mkLambdaFVars xs rhs
let motiveType ← lambdaTelescope value fun xs _body => do
mkForallFVars xs (.sort 0)
if unfolding then
withLocalDeclD `r (← instantiateForall info.type xs) fun r =>
mkForallFVars (xs.push r) (.sort 0)
else
mkForallFVars xs (.sort 0)
let motiveArity ← lambdaTelescope value fun xs _body => do
pure xs.size
let e' ← withLocalDeclD `motive motiveType fun motive => do
lambdaTelescope value fun xs body => do
let (e',mvars) ← M2.run do
let (e', mvars) ← M2.run do
let goal := mkAppN motive xs
-- We bring an unused FVars into scope to pass as `oldIH` and `newIH`. These do not appear anywhere
-- so `buildInductionBody` should just do the right thing
withLocalDeclD `fakeIH (mkConst ``Unit) fun fakeIH =>
let isRecCall := fun _ => none
buildInductionBody #[fakeIH.fvarId!] #[] goal fakeIH.fvarId! fakeIH.fvarId! isRecCall body
let goal ← if unfolding then
pure <| mkApp goal (mkAppN (← mkConstWithLevelParams name) xs)
else
pure goal
withRewrittenMotiveArg goal (rwFun #[name]) fun goal => do
-- We bring an unused FVars into scope to pass as `oldIH` and `newIH`. These do not appear anywhere
-- so `buildInductionBody` should just do the right thing
withLocalDeclD `fakeIH (mkConst ``Unit) fun fakeIH =>
let isRecCall := fun _ => none
buildInductionBody #[fakeIH.fvarId!] #[] goal fakeIH.fvarId! fakeIH.fvarId! isRecCall body
let e' ← mkLambdaFVars xs e'
let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
let e' ← mkLambdaFVars #[motive] e'
pure e'
mkLambdaFVars #[motive] e'
unless (← isTypeCorrect e') do
logError m!"constructed functional cases principle is not type correct:{indentExpr e'}"
@ -1244,40 +1430,41 @@ def deriveCases (name : Name) : MetaM Unit := do
params := .replicate motiveArity .target
}
/--
Given a recursively defined function `foo`, derives `foo.induct`. See the module doc for details.
-/
def deriveInduction (name : Name) : MetaM Unit := do
def deriveInduction (unfolding : Bool) (name : Name) : MetaM Unit := do
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
let unaryInductName ← deriveUnaryInduction unfolding eqnInfo.declNameNonRec
if eqnInfo.declNames.size > 1 then
projectMutualInduct eqnInfo.declNames (unpackMutualInduction eqnInfo) do
projectMutualInduct unfolding eqnInfo.declNames (unpackMutualInduction unfolding eqnInfo) do
-- We set the FunIndInfo on the first induction principle, which must happen inside its
-- realization.
if eqnInfo.argsPacker.numFuncs = 1 then
setNaryFunIndInfo eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
setNaryFunIndInfo (unfolding := unfolding) eqnInfo.fixedParamPerms eqnInfo.declNames[0]! unaryInductName
else
-- (in this case, `unpackMutualInduction` already does `setNaryFunIndInfo`)
let _ ← unpackMutualInduction eqnInfo
let _ ← unpackMutualInduction unfolding eqnInfo
else if let some eqnInfo := Structural.eqnInfoExt.find? (← getEnv) name then
if eqnInfo.declNames.size > 1 then
projectMutualInduct eqnInfo.declNames (deriveInductionStructural eqnInfo.declNames eqnInfo.fixedParamPerms) (pure ())
projectMutualInduct unfolding eqnInfo.declNames (deriveInductionStructural unfolding eqnInfo.declNames eqnInfo.fixedParamPerms) (pure ())
else
let _ ← deriveInductionStructural eqnInfo.declNames eqnInfo.fixedParamPerms
let _ ← deriveInductionStructural unfolding eqnInfo.declNames eqnInfo.fixedParamPerms
else
throwError "constant '{name}' is not structurally or well-founded recursive"
def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
let .str p s := name | return false
match s with
| "induct" =>
| "induct"
| "induct_unfolding" =>
if let some eqnInfo := WF.eqnInfoExt.find? env p then
return true
if (Structural.eqnInfoExt.find? env p).isSome then return true
return false
| "mutual_induct" =>
| "mutual_induct"
| "mutual_induct_unfolding" =>
if let some eqnInfo := WF.eqnInfoExt.find? env p then
if h : eqnInfo.declNames.size > 1 then
return eqnInfo.declNames[0] = p
@ -1291,7 +1478,8 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
def isFunCasesName (env : Environment) (name : Name) : Bool := Id.run do
let .str p s := name | return false
match s with
| "fun_cases" =>
| "fun_cases"
| "fun_cases_unfolding" =>
if (WF.eqnInfoExt.find? env p).isSome then return true
if (Structural.eqnInfoExt.find? env p).isSome then return true
if let some ci := env.find? p then
@ -1306,16 +1494,18 @@ builtin_initialize
registerReservedNameAction fun name => do
if isFunInductName (← getEnv) name then
let .str p _ := name | return false
MetaM.run' <| deriveInduction p
let .str p s := name | return false
let unfolding := s.endsWith "_unfolding"
MetaM.run' <| deriveInduction unfolding p
return true
if isFunCasesName (← getEnv) name then
let .str p _ := name | return false
MetaM.run' <| deriveCases p
let .str p s := name | return false
let unfolding := s == "fun_cases_unfolding"
MetaM.run' <| deriveCases unfolding p
return true
return false
end Lean.Tactic.FunInd
builtin_initialize
builtin_initialize
Lean.registerTraceClass `Meta.FunInd

21
src/Lean/Meta/Tactic/FunIndInfo.lean
View file

@ -41,14 +41,23 @@ deriving Inhabited, Repr
builtin_initialize funIndInfoExt : MapDeclarationExtension FunIndInfo ← mkMapDeclarationExtension
def getFunInductName (declName : Name) : Name :=
declName ++ `induct
def getFunInductName (declName : Name) (unfolding : Bool := false) : Name :=
if unfolding then
declName ++ `induct_unfolding
else
declName ++ `induct
def getFunCasesName (declName : Name) : Name :=
declName ++ `fun_cases
def getFunCasesName (declName : Name) (unfolding : Bool := false) : Name :=
if unfolding then
declName ++ `fun_cases_unfolding
else
declName ++ `fun_cases
def getMutualInductName (declName : Name) : Name :=
declName ++ `mutual_induct
def getMutualInductName (declName : Name) (unfolding : Bool := false) : Name :=
if unfolding then
declName ++ `mutual_induct_unfolding
else
declName ++ `mutual_induct
def getFunInduct? (cases : Bool) (declName : Name) : CoreM (Option Name) := do
let .defnInfo _ ← getConstInfo declName | return none

23
src/Lean/Meta/Tactic/Simp/Types.lean
View file

@ -534,11 +534,23 @@ def Result.getProof' (source : Expr) (r : Result) : MetaM Expr := do
def Result.mkCast (r : Simp.Result) (e : Expr) : MetaM Expr := do
mkAppM ``cast #[← r.getProof, e]
/-- Construct the `Expr` `h.mpr e`, from a `Simp.Result` with proof `h`. -/
def Result.mkEqMPR (r : Simp.Result) (e : Expr) : MetaM Expr := do
if r.proof?.isNone && r.expr == e then
pure e
else
Meta.mkEqMPR (← r.getProof) e
def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
match r.proof? with
| none => return { expr := mkApp r.expr a, proof? := none }
| some h => return { expr := mkApp r.expr a, proof? := (← Meta.mkCongrFun h a) }
def mkCongrArg (f : Expr) (r : Result) : MetaM Result :=
match r.proof? with
| none => return { expr := mkApp f r.expr, proof? := none }
| some h => return { expr := mkApp f r.expr, proof? := (← Meta.mkCongrArg f h) }
def mkCongr (r₁ r₂ : Result) : MetaM Result :=
let e := mkApp r₁.expr r₂.expr
match r₁.proof?, r₂.proof? with
@ -773,6 +785,7 @@ def DStep.addExtraArgs (s : DStep) (extraArgs : Array Expr) : DStep :=
| .continue (some eNew) => .continue (mkAppN eNew extraArgs)
def Result.addLambdas (r : Result) (xs : Array Expr) : MetaM Result := do
if xs.isEmpty then return r
let eNew ← mkLambdaFVars xs r.expr
match r.proof? with
| none => return { expr := eNew }
@ -781,6 +794,16 @@ def Result.addLambdas (r : Result) (xs : Array Expr) : MetaM Result := do
mkFunExt (← mkLambdaFVars #[x] h)
return { expr := eNew, proof? := p }
def Result.addForalls (r : Result) (xs : Array Expr) : MetaM Result := do
if xs.isEmpty then return r
let eNew ← mkForallFVars xs r.expr
match r.proof? with
| none => return { expr := eNew }
| some h =>
let p ← xs.foldrM (init := h) fun x h => do
mkForallCongr (← mkLambdaFVars #[x] h)
return { expr := eNew, proof? := p }
end Simp
export Simp (SimpM Simprocs)

4
tests/lean/run/funind_structural.lean
View file

@ -89,8 +89,8 @@ termination_by structural n
/--
info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n → Prop)
(case1 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), motive x m Finn.fzero x_1)
(case2 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), (x_1 = Finn.fzero → False) → motive x m x_1 Finn.fzero)
(case1 : ∀ (x : Bool) (m n : Nat) (f : Finn n), motive x m Finn.fzero f)
(case2 : ∀ (x : Bool) (m n : Nat) (a : Finn n), (a = Finn.fzero → False) → motive x m a Finn.fzero)
(case3 : ∀ (x : Bool) (m n : Nat) (i j : Finn n), motive (!x) (m + 1) i j → motive x m i.fsucc j.fsucc) (x : Bool)
{n : Nat} (m : Nat) (a✝ f : Finn n) : motive x m a✝ f
-/

487
tests/lean/run/funind_unfolding.lean Normal file
View file

@ -0,0 +1,487 @@
axiom testSorry : α
def fib : Nat → Nat
| 0 => 0
| 1 => 1
| n+2 => fib n + fib (n+1)
termination_by x => x
/--
info: fib.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0 0) (case2 : motive 1 1)
(case3 : ∀ (n : Nat), motive n.succ.succ (fib n + fib (n + 1))) (x✝ : Nat) : motive x✝ (fib x✝)
-/
#guard_msgs in
#check fib.fun_cases_unfolding
def ackermann : Nat → Nat → Nat
| 0, m => m + 1
| n+1, 0 => ackermann n 1
| n+1, m+1 => ackermann n (ackermann (n + 1) m)
termination_by n m => (n, m)
/--
info: ackermann.fun_cases_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m (m + 1))
(case2 : ∀ (n : Nat), motive n.succ 0 (ackermann n 1))
(case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m))) (x✝ x✝¹ : Nat) :
motive x✝ x✝¹ (ackermann x✝ x✝¹)
-/
#guard_msgs in
#check ackermann.fun_cases_unfolding
def fib' : Nat → Nat
| 0 => 0
| 1 => 1
| n => fib' (n-1) + fib' (n-2)
decreasing_by all_goals exact testSorry
/--
info: fib'.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : motive 0 0) (case2 : motive 1 1)
(case3 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → motive n (fib' (n - 1) + fib' (n - 2))) (x✝ : Nat) :
motive x✝ (fib' x✝)
-/
#guard_msgs in
#check fib'.fun_cases_unfolding
def fib'' (n : Nat) : Nat :=
if _h : n < 2 then
n
else
let foo := n - 2
if foo < 100 then
fib'' (n - 1) + fib'' foo
else
0
/--
info: fib''.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), n < 2 → motive n n)
(case2 :
∀ (n : Nat),
¬n < 2 →
let foo := n - 2;
foo < 100 → motive n (fib'' (n - 1) + fib'' foo))
(case3 :
∀ (n : Nat),
¬n < 2 →
let foo := n - 2;
¬foo < 100 → motive n 0)
(n : Nat) : motive n (fib'' n)
-/
#guard_msgs in
#check fib''.fun_cases_unfolding
-- set_option trace.Meta.FunInd true in
def filter (p : Nat → Bool) : List Nat → List Nat
| [] => []
| x::xs => if p x then x::filter p xs else filter p xs
/--
info: filter.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 : ∀ (p : Nat → Bool), motive p [])
(case2 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), p x = true → motive p (x :: xs))
(case3 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), ¬p x = true → motive p (x :: xs)) (p : Nat → Bool)
(x✝ : List Nat) : motive p x✝
-/
#guard_msgs in
#check filter.fun_cases
/--
info: filter.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List Nat → Prop)
(case1 : ∀ (p : Nat → Bool), motive p [] [])
(case2 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), p x = true → motive p (x :: xs) (x :: filter p xs))
(case3 : ∀ (p : Nat → Bool) (x : Nat) (xs : List Nat), ¬p x = true → motive p (x :: xs) (filter p xs))
(p : Nat → Bool) (x✝ : List Nat) : motive p x✝ (filter p x✝)
-/
#guard_msgs in
#check filter.fun_cases_unfolding
/--
info: filter.induct (p : Nat → Bool) (motive : List Nat → Prop) (case1 : motive [])
(case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive xs → motive (x :: xs))
(case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive xs → motive (x :: xs)) (a✝ : List Nat) : motive a✝
-/
#guard_msgs in
#check filter.induct
/--
info: filter.induct_unfolding (p : Nat → Bool) (motive : List Nat → List Nat → Prop) (case1 : motive [] [])
(case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive xs (filter p xs) → motive (x :: xs) (x :: filter p xs))
(case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive xs (filter p xs) → motive (x :: xs) (filter p xs))
(a✝ : List Nat) : motive a✝ (filter p a✝)
-/
#guard_msgs in
#check filter.induct_unfolding
theorem filter_const_false_is_nil :
filter (fun _ => false) xs = [] := by
refine filter.induct_unfolding (fun _ => false) (motive := fun xs r => r = []) ?case1 ?case2 ?case3 xs
case case1 => rfl
case case2 => intros; contradiction
case case3 => intros; assumption
theorem filter_filter :
filter q (filter p xs) = filter (fun x => p x && q x) xs := by
refine filter.induct_unfolding p (motive := fun xs r => filter q r = filter (fun x => p x && q x) xs) ?case1 ?case2 ?case3 xs
case case1 => rfl
case case2 =>
intros x xs hp ih
by_cases hq : q x
case pos => simp [*, filter]
case neg => simp [*, filter]
case case3 =>
intros
simp [*, filter]
def map (f : Nat → Bool) : List Nat → List Bool
| [] => []
| x::xs => f x::map f xs
termination_by x => x
/--
info: map.fun_cases (motive : (Nat → Bool) → List Nat → Prop) (case1 : ∀ (f : Nat → Bool), motive f [])
(case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs)) (f : Nat → Bool) (x✝ : List Nat) :
motive f x✝
-/
#guard_msgs in
#check map.fun_cases
/--
info: map.fun_cases_unfolding (motive : (Nat → Bool) → List Nat → List Bool → Prop)
(case1 : ∀ (f : Nat → Bool), motive f [] [])
(case2 : ∀ (f : Nat → Bool) (x : Nat) (xs : List Nat), motive f (x :: xs) (f x :: map f xs)) (f : Nat → Bool)
(x✝ : List Nat) : motive f x✝ (map f x✝)
-/
#guard_msgs in
#check map.fun_cases_unfolding
/--
info: map.induct (motive : List Nat → Prop) (case1 : motive [])
(case2 : ∀ (x : Nat) (xs : List Nat), motive xs → motive (x :: xs)) (a✝ : List Nat) : motive a✝
-/
#guard_msgs in
#check map.induct
/--
info: map.induct_unfolding (f : Nat → Bool) (motive : List Nat → List Bool → Prop) (case1 : motive [] [])
(case2 : ∀ (x : Nat) (xs : List Nat), motive xs (map f xs) → motive (x :: xs) (f x :: map f xs)) (a✝ : List Nat) :
motive a✝ (map f a✝)
-/
#guard_msgs in
#check map.induct_unfolding
namespace BinaryWF
def map2 (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
| x::xs, y::ys => f x y::map2 f xs ys
| _, _ => []
termination_by x => x
/--
info: BinaryWF.map2.induct_unfolding (f : Nat → Nat → Bool) (motive : List Nat → List Nat → List Bool → Prop)
(case1 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive xs ys (map2 f xs ys) → motive (x :: xs) (y :: ys) (f x y :: map2 f xs ys))
(case2 :
∀ (x x_1 : List Nat),
(∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
motive x x_1 [])
(a✝ a✝¹ : List Nat) : motive a✝ a✝¹ (map2 f a✝ a✝¹)
-/
#guard_msgs in
#check map2.induct_unfolding
end BinaryWF
namespace BinaryStructural
def map2 (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
| x::xs, y::ys => f x y::map2 f xs ys
| _, _ => []
termination_by structural x => x
/--
info: BinaryStructural.map2.induct_unfolding (f : Nat → Nat → Bool) (motive : List Nat → List Nat → List Bool → Prop)
(case1 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive xs ys (map2 f xs ys) → motive (x :: xs) (y :: ys) (f x y :: map2 f xs ys))
(case2 :
∀ (t x : List Nat),
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive t x [])
(a✝ a✝¹ : List Nat) : motive a✝ a✝¹ (map2 f a✝ a✝¹)
-/
#guard_msgs in
#check map2.induct_unfolding
end BinaryStructural
namespace MutualWF
mutual
def map2a (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
| x::xs, y::ys => f x y::map2b f xs ys
| _, _ => []
termination_by x => x
def map2b (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
| x::xs, y::ys => f x y::map2a f xs ys
| _, _ => []
termination_by x => x
end
/--
info: MutualWF.map2a.mutual_induct_unfolding (f : Nat → Nat → Bool) (motive1 motive2 : List Nat → List Nat → List Bool → Prop)
(case1 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive2 xs ys (map2b f xs ys) → motive1 (x :: xs) (y :: ys) (f x y :: map2b f xs ys))
(case2 :
∀ (x x_1 : List Nat),
(∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
motive1 x x_1 [])
(case3 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive1 xs ys (map2a f xs ys) → motive2 (x :: xs) (y :: ys) (f x y :: map2a f xs ys))
(case4 :
∀ (x x_1 : List Nat),
(∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
motive2 x x_1 []) :
(∀ (a a_1 : List Nat), motive1 a a_1 (map2a f a a_1)) ∧ ∀ (a a_1 : List Nat), motive2 a a_1 (map2b f a a_1)
-/
#guard_msgs in
#check map2a.mutual_induct_unfolding
/--
info: MutualWF.map2a.induct_unfolding (f : Nat → Nat → Bool) (motive1 motive2 : List Nat → List Nat → List Bool → Prop)
(case1 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive2 xs ys (map2b f xs ys) → motive1 (x :: xs) (y :: ys) (f x y :: map2b f xs ys))
(case2 :
∀ (x x_1 : List Nat),
(∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
motive1 x x_1 [])
(case3 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive1 xs ys (map2a f xs ys) → motive2 (x :: xs) (y :: ys) (f x y :: map2a f xs ys))
(case4 :
∀ (x x_1 : List Nat),
(∀ (x_2 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), x = x_2 :: xs → x_1 = y :: ys → False) →
motive2 x x_1 [])
(a✝ a✝¹ : List Nat) : motive1 a✝ a✝¹ (map2a f a✝ a✝¹)
-/
#guard_msgs in
#check map2a.induct_unfolding
end MutualWF
namespace MutualStructural
-- set_option trace.Meta.FunInd true in
mutual
def map2a (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
| x::xs, y::ys => f x y::map2b f xs ys
| _, _ => []
termination_by structural x => x
def map2b (f : Nat → Nat → Bool) : List Nat → List Nat → List Bool
| x::xs, y::ys => f x y::map2a f xs ys
| _, _ => []
termination_by structural x => x
end
/--
info: MutualStructural.map2a.induct (motive_1 motive_2 : List Nat → List Nat → Prop)
(case1 : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), motive_2 xs ys → motive_1 (x :: xs) (y :: ys))
(case2 :
∀ (t x : List Nat),
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive_1 t x)
(case3 : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), motive_1 xs ys → motive_2 (x :: xs) (y :: ys))
(case4 :
∀ (t x : List Nat),
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) → motive_2 t x)
(a✝ a✝¹ : List Nat) : motive_1 a✝ a✝¹
-/
#guard_msgs in
#check map2a.induct
/--
info: MutualStructural.map2a.mutual_induct_unfolding (f : Nat → Nat → Bool)
(motive_1 motive_2 : List Nat → List Nat → List Bool → Prop)
(case1 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive_2 xs ys (map2b f xs ys) → motive_1 (x :: xs) (y :: ys) (map2a f (x :: xs) (y :: ys)))
(case2 :
∀ (t x : List Nat),
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) →
motive_1 t x (map2a f t x))
(case3 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive_1 xs ys (map2a f xs ys) → motive_2 (x :: xs) (y :: ys) (map2b f (x :: xs) (y :: ys)))
(case4 :
∀ (t x : List Nat),
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) →
motive_2 t x (map2b f t x)) :
(∀ (a a_1 : List Nat), motive_1 a a_1 (map2a f a a_1)) ∧ ∀ (a a_1 : List Nat), motive_2 a a_1 (map2b f a a_1)
-/
#guard_msgs in
#check map2a.mutual_induct_unfolding
/--
info: MutualStructural.map2a.induct_unfolding (f : Nat → Nat → Bool)
(motive_1 motive_2 : List Nat → List Nat → List Bool → Prop)
(case1 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive_2 xs ys (map2b f xs ys) → motive_1 (x :: xs) (y :: ys) (map2a f (x :: xs) (y :: ys)))
(case2 :
∀ (t x : List Nat),
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) →
motive_1 t x (map2a f t x))
(case3 :
∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat),
motive_1 xs ys (map2a f xs ys) → motive_2 (x :: xs) (y :: ys) (map2b f (x :: xs) (y :: ys)))
(case4 :
∀ (t x : List Nat),
(∀ (x_1 : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t = x_1 :: xs → x = y :: ys → False) →
motive_2 t x (map2b f t x))
(a✝ a✝¹ : List Nat) : motive_1 a✝ a✝¹ (map2a f a✝ a✝¹)
-/
#guard_msgs in
#check map2a.induct_unfolding
end MutualStructural
abbrev leftChild (i : Nat) := 2*i + 1
abbrev parent (i : Nat) := (i - 1) / 2
def siftDown (a : Array Int) (root : Nat) (e : Nat) (h : e ≤ a.size := by omega) : Array Int :=
if _ : leftChild root < e then
let child := leftChild root
let child := if _ : child+1 < e then
if a[child] < a[child + 1] then
child + 1
else
child
else
child
if a[root]! < a[child]! then
let a := a.swapIfInBounds root child
siftDown a child e testSorry
else
a
else
a
termination_by e - root
decreasing_by exact testSorry
/--
info: siftDown.induct_unfolding (e : Nat) (motive : (a : Array Int) → Nat → e ≤ a.size → Array Int → Prop)
(case1 :
∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
leftChild root < e →
let child := leftChild root;
let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
a[root]! < a[child]! →
let a_1 := a.swapIfInBounds root child;
motive a_1 child ⋯ (siftDown a_1 child e ⋯) → motive a root h (siftDown a_1 child e ⋯))
(case2 :
∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
leftChild root < e →
let child := leftChild root;
let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
¬a[root]! < a[child]! → motive a root h a)
(case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h a) (a : Array Int)
(root : Nat) (h : e ≤ a.size) : motive a root h (siftDown a root e h)
-/
#guard_msgs in
#check siftDown.induct_unfolding
/--
info: siftDown.induct (e : Nat) (motive : (a : Array Int) → Nat → e ≤ a.size → Prop)
(case1 :
∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
leftChild root < e →
let child := leftChild root;
let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
a[root]! < a[child]! →
let a_1 := a.swapIfInBounds root child;
motive a_1 child ⋯ → motive a root h)
(case2 :
∀ (a : Array Int) (root : Nat) (h : e ≤ a.size),
leftChild root < e →
let child := leftChild root;
let child := if x : child + 1 < e then if h : a[child] < a[child + 1] then child + 1 else child else child;
¬a[root]! < a[child]! → motive a root h)
(case3 : ∀ (a : Array Int) (root : Nat) (h : e ≤ a.size), ¬leftChild root < e → motive a root h) (a : Array Int)
(root : Nat) (h : e ≤ a.size) : motive a root h
-/
#guard_msgs in
#check siftDown.induct
-- Now something with have
def withHave (n : Nat): Bool :=
have : 0 < n := testSorry
if n = 42 then true else withHave (n - 1)
termination_by n
decreasing_by exact testSorry
/--
info: withHave.induct_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42 → motive 42 true)
(case2 : ∀ (x : Nat), 0 < x → ¬x = 42 → motive (x - 1) (withHave (x - 1)) → motive x (withHave (x - 1))) (n : Nat) :
motive n (withHave n)
-/
#guard_msgs in
#check withHave.induct_unfolding
/--
info: withHave.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42 → motive 42 true)
(case2 : ∀ (n : Nat), 0 < n → ¬n = 42 → motive n (withHave (n - 1))) (n : Nat) : motive n (withHave n)
-/
#guard_msgs in
#check withHave.fun_cases_unfolding
-- Structural Mutual recursion
inductive Tree (α : Type u) : Type u where
| node : α → (Bool → List (Tree α)) → Tree α
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_unfolding.{u_1} {α : Type u_1} (motive_1 : Tree α → Nat → Prop) (motive_2 : List (Tree α) → Nat → Prop)
(case1 :
∀ (a : α) (tsf : Bool → List (Tree α)),
motive_2 (tsf true) (Tree.size_aux (tsf true)) →
motive_2 (tsf false) (Tree.size_aux (tsf false)) →
motive_1 (Tree.node a tsf) (1 + Tree.size_aux (tsf true) + Tree.size_aux (tsf false)))
(case2 : motive_2 [] 0)
(case3 :
∀ (t : Tree α) (ts : List (Tree α)),
motive_1 t t.size → motive_2 ts (Tree.size_aux ts) → motive_2 (t :: ts) (t.size + Tree.size_aux ts))
(a✝ : Tree α) : motive_1 a✝ a✝.size
-/
#guard_msgs in
#check Tree.size.induct_unfolding
/--
info: Tree.size_aux.induct_unfolding.{u_1} {α : Type u_1} (motive_1 : Tree α → Nat → Prop)
(motive_2 : List (Tree α) → Nat → Prop)
(case1 :
∀ (a : α) (tsf : Bool → List (Tree α)),
motive_2 (tsf true) (Tree.size_aux (tsf true)) →
motive_2 (tsf false) (Tree.size_aux (tsf false)) →
motive_1 (Tree.node a tsf) (1 + Tree.size_aux (tsf true) + Tree.size_aux (tsf false)))
(case2 : motive_2 [] 0)
(case3 :
∀ (t : Tree α) (ts : List (Tree α)),
motive_1 t t.size → motive_2 ts (Tree.size_aux ts) → motive_2 (t :: ts) (t.size + Tree.size_aux ts))
(a✝ : List (Tree α)) : motive_2 a✝ (Tree.size_aux a✝)
-/
#guard_msgs in
#check Tree.size_aux.induct_unfolding

44
tests/lean/run/funinduction_generalize.lean
View file

@ -27,9 +27,9 @@ ih1✝ : P (xs✝.zip ys✝)
case case2
xs ys : List Nat
P : {α : Type} → List α → Prop
t✝ x✝¹ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
⊢ P (t✝.zip x✝¹)
t✝ ys✝ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
⊢ P (t✝.zip ys✝)
-/
#guard_msgs in
example : P (List.zip xs ys) := by
@ -52,10 +52,10 @@ h : (x✝ :: xs✝).isEmpty = true
case case2
xs ys : List Nat
P : {α : Type} → List α → Prop
t✝ x✝¹ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
t✝ ys✝ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
h : t✝.isEmpty = true
⊢ P (t✝.zip x✝¹)
⊢ P (t✝.zip ys✝)
-/
#guard_msgs in
example (h : xs.isEmpty) : P (List.zip xs ys) := by
@ -78,8 +78,8 @@ h : (x✝ :: xs✝).isEmpty = true
case case2
xs ys : List Nat
P : {α : Type} → List α → Prop
t✝ x✝¹ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
t✝ ys✝ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
h : t✝.isEmpty = true
⊢ P (t✝.zip ys)
-/
@ -103,8 +103,8 @@ h : (x✝ :: xs✝).isEmpty = true
case case2
xs ys : List Nat
P : {α : Type} → List α → Prop
t✝ x✝¹ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
t✝ ys✝ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
h : t✝.isEmpty = true
⊢ P (t✝.zip ys)
-/
@ -129,9 +129,9 @@ case case2
xs ys : List Nat
P : {α : Type} → List α → Prop
h : xs.isEmpty = true
t✝ x✝¹ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
⊢ P (xs.zip x✝¹)
t✝ ys✝ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
⊢ P (xs.zip ys✝)
-/
#guard_msgs in
example (h : xs.isEmpty) : P (List.zip xs ys) := by
@ -154,9 +154,9 @@ case case2
xs ys : List Nat
P : {α : Type} → List α → Prop
h : xs.isEmpty = true
t✝ x✝¹ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
⊢ P (xs.zip x✝¹)
t✝ ys✝ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
⊢ P (xs.zip ys✝)
-/
#guard_msgs in
example (h : xs.isEmpty) : P (List.zip xs ys) := by
@ -177,11 +177,11 @@ h : xs.isEmpty = true
case case2
P : {α : Type} → List α → Prop
t✝ x✝¹ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
t✝ ys✝ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
xs : List Nat
h : xs.isEmpty = true
⊢ P (xs.zip x✝¹)
⊢ P (xs.zip ys✝)
-/
#guard_msgs in
example (h : xs.isEmpty) : P (List.zip xs ys) := by
@ -202,11 +202,11 @@ h : xs.isEmpty = true
case case2
P : {α : Type} → List α → Prop
t✝ x✝¹ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → x✝¹ = y :: ys → False
t✝ ys✝ : List Nat
x✝ : ∀ (x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat), t✝ = x :: xs → ys✝ = y :: ys → False
xs : List Nat
h : xs.isEmpty = true
⊢ P (xs.zip x✝¹)
⊢ P (xs.zip ys✝)
-/
#guard_msgs in
example (h : xs.isEmpty) : P (List.zip xs ys) := by