feat: more parameters in .fun_cases theorem (#8359)
This PR improves the functional cases principles, by making a more educated guess which function parameters should be targets and which should remain parameters (or be dropped). This simplifies the principles, and increases the chance that `fun_cases` can unfold the function call. Fixes #8296 (at least for the common cases, I hope.)
This commit is contained in:
Joachim Breitner
GitHub
parent
af7eb01f29
commit
e7b61232c9
11 changed files with 204 additions and 113 deletions
|
|
@ -172,20 +172,19 @@ end FixedParams
|
|||
|
||||
open Lean Meta FixedParams
|
||||
|
||||
def getParamRevDeps (preDefs : Array PreDefinition) : MetaM (Array (Array (Array Nat))) := do
|
||||
preDefs.mapM fun preDef =>
|
||||
lambdaTelescope preDef.value (cleanupAnnotations := true) fun xs _ => do
|
||||
let mut revDeps := #[]
|
||||
for h : i in [:xs.size] do
|
||||
let mut deps := #[]
|
||||
for h : j in [i+1:xs.size] do
|
||||
if (← dependsOn (← inferType xs[j]) xs[i].fvarId!) then
|
||||
deps := deps.push j
|
||||
revDeps := revDeps.push deps
|
||||
pure revDeps
|
||||
def getParamRevDeps (value : Expr) : MetaM (Array (Array Nat)) := do
|
||||
lambdaTelescope value (cleanupAnnotations := true) fun xs _ => do
|
||||
let mut revDeps := #[]
|
||||
for h : i in [:xs.size] do
|
||||
let mut deps := #[]
|
||||
for h : j in [i+1:xs.size] do
|
||||
if (← dependsOn (← inferType xs[j]) xs[i].fvarId!) then
|
||||
deps := deps.push j
|
||||
revDeps := revDeps.push deps
|
||||
pure revDeps
|
||||
|
||||
def getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info := do
|
||||
let revDeps ← getParamRevDeps preDefs
|
||||
let revDeps ← preDefs.mapM (getParamRevDeps ·.value)
|
||||
let arities := revDeps.map (·.size)
|
||||
let ref ← IO.mkRef (Info.init revDeps)
|
||||
|
||||
|
|
|
|||
|
|
@ -551,6 +551,32 @@ def maskArray {α} (mask : Array Bool) (xs : Array α) : Array α := Id.run do
|
|||
if b then ys := ys.push x
|
||||
return ys
|
||||
|
||||
/--
|
||||
Inverse of `maskArray`:
|
||||
```
|
||||
zipMaskedArray mask (maskArray (mask.map not) xs) (maskArray mask xs) == xs
|
||||
```
|
||||
-/
|
||||
def zipMaskedArray {α} (mask : Array Bool) (xs ys : Array α) : Array α := Id.run do
|
||||
let mut i := 0
|
||||
let mut j := 0
|
||||
let mut zs := #[]
|
||||
for b in mask do
|
||||
if b then
|
||||
if h : j < ys.size then
|
||||
zs := zs.push ys[j]
|
||||
j := j + 1
|
||||
else
|
||||
panic! "zipMaskedArray: not enough elements in ys"
|
||||
else
|
||||
if h : i < xs.size then
|
||||
zs := zs.push xs[i]
|
||||
i := i + 1
|
||||
else
|
||||
panic! "zipMaskedArray: not enough elements in xs"
|
||||
return zs
|
||||
|
||||
|
||||
/--
|
||||
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`.
|
||||
|
|
@ -1478,6 +1504,55 @@ where doRealize inductName := do
|
|||
}
|
||||
|
||||
|
||||
/--
|
||||
Given an expression `fun x y z => body`, returns a bit mask of the functinon's arity length
|
||||
that has `true` whenver that parameter of the function appears as a scrutinee of a `match` in
|
||||
tail position. These are the parameters that are likely useful as targets of the motive
|
||||
of the functional cases theorem. All others become parameters or may be dropped.
|
||||
|
||||
-/
|
||||
partial def refinedArguments (e : Expr) : MetaM (Array Bool) := do
|
||||
let (_, mask) ← lambdaTelescope e fun xs body =>
|
||||
let mask0 := Array.replicate xs.size false
|
||||
go xs body |>.run mask0
|
||||
let mut mask := mask
|
||||
let revDeps ← getParamRevDeps e
|
||||
assert! revDeps.size = mask.size
|
||||
for i in [:mask.size] do
|
||||
if mask[i]! then
|
||||
for j in revDeps[i]! do
|
||||
mask := mask.set! j true
|
||||
pure mask
|
||||
where
|
||||
-- NB: we process open terms here.
|
||||
go (xs : Array Expr) (e : Expr) : StateT (Array Bool) MetaM Unit := do
|
||||
let e := e.consumeMData
|
||||
|
||||
if e.isLambda then
|
||||
-- Not strictly tail position, but simplifies the code below and should not make
|
||||
-- a difference in practice
|
||||
go xs e.bindingBody!
|
||||
else if e.isLet then
|
||||
go xs e.letBody!
|
||||
else
|
||||
e.withApp fun f args => do
|
||||
if f.isConst then
|
||||
if let some matchInfo ← getMatcherInfo? f.constName! then
|
||||
for scrut in args[matchInfo.getFirstDiscrPos:matchInfo.getFirstAltPos] do
|
||||
if let some i := xs.idxOf? scrut then
|
||||
modify (·.set! i true)
|
||||
for alt in args[matchInfo.getFirstAltPos:matchInfo.arity] do
|
||||
go xs alt
|
||||
if f.isConstOf ``letFun then
|
||||
for arg in args[3:4] do
|
||||
go xs arg
|
||||
if f.isConstOf ``ite || f.isConstOf ``dite then
|
||||
for arg in args[3:5] do
|
||||
go xs arg
|
||||
if f.isConstOf ``cond then
|
||||
for arg in args[2:4] do
|
||||
go xs arg
|
||||
|
||||
/--
|
||||
For non-recursive (and recursive functions) functions we derive a “functional case splitting theorem”. This is very similar
|
||||
than the functional induction theorem. It splits the goal, but does not give you inductive hyptheses.
|
||||
|
|
@ -1503,34 +1578,44 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := 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
|
||||
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 goal := mkAppN motive xs
|
||||
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'
|
||||
mkLambdaFVars #[motive] e'
|
||||
let targetMask ← refinedArguments value
|
||||
trace[Meta.FunInd] "targetMask: {targetMask}"
|
||||
|
||||
unless (← isTypeCorrect e') do
|
||||
logError m!"constructed functional cases principle is not type correct:{indentExpr e'}"
|
||||
let (paramsMask, e') ← lambdaTelescope value fun xs _ => do
|
||||
let params := maskArray (targetMask.map not) xs
|
||||
let targets := maskArray targetMask xs
|
||||
let motiveType ←
|
||||
if unfolding then
|
||||
withLocalDeclD `r (← instantiateForall info.type xs) fun r =>
|
||||
mkForallFVars (targets.push r) (.sort 0)
|
||||
else
|
||||
mkForallFVars targets (.sort 0)
|
||||
-- Remove targets from local context, we want to bring them into scope after the motive
|
||||
-- so that the index passed to `abstractIndependentMVars` works.
|
||||
withErasedFVars (targets.map (·.fvarId!)) do
|
||||
withLocalDeclD `motive motiveType fun motive => do
|
||||
-- Bring targets freshly into scope again
|
||||
forallBoundedTelescope motiveType targets.size fun targets _ => do
|
||||
let (e', mvars) ← M2.run do
|
||||
let args := zipMaskedArray targetMask params targets
|
||||
let body := value.beta args
|
||||
let goal := mkAppN motive targets
|
||||
let goal ← if unfolding then
|
||||
pure <| mkApp goal (mkAppN (← mkConstWithLevelParams name) args)
|
||||
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 targets e'
|
||||
let e' ← abstractIndependentMVars mvars (← motive.fvarId!.getDecl).index e'
|
||||
let e' ← mkLambdaFVars #[motive] e'
|
||||
mkLambdaFVarsMasked params e'
|
||||
|
||||
mapError (f := (m!"constructed functional cases principle is not type correct:{indentExpr e'}\n{indentD ·}")) do
|
||||
check e'
|
||||
|
||||
let eTyp ← inferType e'
|
||||
|
|
@ -1545,11 +1630,25 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do
|
|||
addDecl <| Declaration.thmDecl
|
||||
{ name := casesName, levelParams := us, type := eTyp, value := e' }
|
||||
|
||||
-- Calculate paramsKind from targetMask (length = arity) and paramsMask (length = params)
|
||||
let mut paramKinds := #[]
|
||||
let mut j := 0
|
||||
for isTarget in targetMask do
|
||||
if isTarget then
|
||||
paramKinds := paramKinds.push .target
|
||||
else
|
||||
assert! j < paramsMask.size
|
||||
if paramsMask[j]! then
|
||||
paramKinds := paramKinds.push .param
|
||||
else
|
||||
paramKinds := paramKinds.push .dropped
|
||||
j := j + 1
|
||||
|
||||
setFunIndInfo {
|
||||
funName := name
|
||||
funIndName := casesName
|
||||
levelMask := usMask
|
||||
params := .replicate motiveArity .target
|
||||
params := paramKinds
|
||||
}
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -529,7 +529,8 @@ attribute [Std.Internal.tree_tac] and_true true_and and_self heq_eq_eq inner.inj
|
|||
theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced)
|
||||
(hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size) :
|
||||
balance! k v l r = balanceₘ k v l r := by
|
||||
cases k, v, l, r using balance!.fun_cases
|
||||
set_option tactic.fun_induction.unfolding false in
|
||||
fun_cases balance!
|
||||
all_goals dsimp only [balance!, balanceₘ]
|
||||
· rfl
|
||||
· split <;> simp_all [Std.Internal.tree_tac]
|
||||
|
|
@ -582,15 +583,13 @@ theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb
|
|||
simp only [Std.Internal.tree_tac, Nat.add_right_cancel_iff] at *
|
||||
omega
|
||||
· exfalso
|
||||
rename_i ls rs h rls _ _ _ _ _ _ _ _ _ _
|
||||
simp only [balanced_inner_iff, size_inner, size_leaf, balancedAtRoot_zero_iff'] at hrb
|
||||
simp only [delta] at h
|
||||
simp only [delta] at ‹delta * _ < _›
|
||||
have := hlb.one_le
|
||||
omega
|
||||
· exfalso
|
||||
rename_i ls rs h _ _ _ _ _ _ _
|
||||
simp only [balanced_inner_iff, size_inner, size_leaf, balancedAtRoot_zero_iff] at hrb
|
||||
simp only [delta] at h
|
||||
simp only [delta] at ‹delta * _ < _›
|
||||
have := hlb.one_le
|
||||
omega
|
||||
· repeat simp_all only [Std.Internal.tree_tac, rotateR, dite_true, ite_true, dite_false]
|
||||
|
|
@ -602,15 +601,13 @@ theorem balance!_eq_balanceₘ {k v} {l r : Impl α β} (hlb : l.Balanced) (hrb
|
|||
simp only [Std.Internal.tree_tac, Nat.reduceMul] at *
|
||||
omega
|
||||
· exfalso
|
||||
rename_i ls rs h rls _ _ _ _ _ _ _ _ _ _
|
||||
simp only [balanced_inner_iff, size_inner, size_leaf, balancedAtRoot_zero_iff'] at hlb
|
||||
simp only [delta] at h
|
||||
simp only [delta] at ‹delta * _ < _›
|
||||
have := hrb.one_le
|
||||
omega
|
||||
· exfalso
|
||||
rename_i ls rs h _ _ _ _ _ _ _
|
||||
simp only [balanced_inner_iff, size_inner, size_leaf, balancedAtRoot_zero_iff] at hlb
|
||||
simp only [delta] at h
|
||||
simp only [delta] at ‹delta * _ < _›
|
||||
have := hrb.one_le
|
||||
omega
|
||||
· repeat simp only [Std.Internal.tree_tac, dite_true, dite_false, *] at *
|
||||
|
|
@ -654,6 +651,7 @@ theorem balanced_rotateL (k v l rs rk rv rl rr) (hl : l.Balanced)
|
|||
(hlr : BalanceLErasePrecond l.size rs ∨ BalanceLErasePrecond rs l.size)
|
||||
(hh : rs > delta * l.size) :
|
||||
(rotateL k v l rk rv rl rr : Impl α β).Balanced := by
|
||||
set_option tactic.fun_induction.unfolding false in
|
||||
fun_cases rotateL k v l rk rv rl rr <;> dsimp only [rotateL]
|
||||
· split
|
||||
· next h =>
|
||||
|
|
@ -668,6 +666,7 @@ theorem balanced_rotateR (k v ls lk lv ll lr r) (hl : (Impl.inner ls lk lv ll lr
|
|||
(hr : r.Balanced) (hlr : BalanceLErasePrecond ls r.size ∨ BalanceLErasePrecond r.size ls)
|
||||
(hh : ls > delta * r.size) :
|
||||
(rotateR k v lk lv ll lr r : Impl α β).Balanced := by
|
||||
set_option tactic.fun_induction.unfolding false in
|
||||
fun_cases rotateR k v lk lv ll lr r <;> dsimp only [rotateR]
|
||||
· split
|
||||
· next h =>
|
||||
|
|
@ -680,6 +679,7 @@ theorem balanced_rotateR (k v ls lk lv ll lr r) (hl : (Impl.inner ls lk lv ll lr
|
|||
|
||||
theorem balanceL_eq_balanceLErase {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
|
||||
balanceL k v l r hlb hrb hlr = balanceLErase k v l r hlb hrb hlr.erase := by
|
||||
set_option tactic.fun_induction.unfolding false in
|
||||
fun_cases balanceL k v l r hlb hrb hlr
|
||||
all_goals dsimp only [balanceL, balanceLErase]
|
||||
split
|
||||
|
|
@ -697,7 +697,7 @@ theorem balanceLErase_eq_balanceL! {k : α} {v : β k} {l r : Impl α β} {hlb h
|
|||
theorem balanceL!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced)
|
||||
(hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
|
||||
balanceL! k v l r = balance! k v l r := by
|
||||
cases k, v, l, r using balance!.fun_cases
|
||||
fun_cases balance!
|
||||
all_goals dsimp only [balanceL!, balance!]
|
||||
all_goals try simp only [*]
|
||||
all_goals try dsimp only [dreduceDIte, dreduceIte]
|
||||
|
|
@ -708,6 +708,7 @@ theorem balanceL!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Ba
|
|||
|
||||
theorem balanceR_eq_balanceRErase {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
|
||||
balanceR k v l r hlb hrb hlr = balanceRErase k v l r hlb hrb hlr.erase := by
|
||||
set_option tactic.fun_induction.unfolding false in
|
||||
fun_cases balanceR k v l r hlb hrb hlr
|
||||
all_goals dsimp only [balanceR, balanceRErase]
|
||||
split
|
||||
|
|
@ -725,7 +726,7 @@ theorem balanceRErase_eq_balanceR! {k : α} {v : β k} {l r : Impl α β} {hlb h
|
|||
theorem balanceR!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced)
|
||||
(hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
|
||||
balanceR! k v l r = balance! k v l r := by
|
||||
cases k, v, l, r using balance!.fun_cases
|
||||
fun_cases balance! k v l r
|
||||
all_goals dsimp only [balanceR!, balance!]
|
||||
all_goals try simp only [*]
|
||||
all_goals try dsimp only [dreduceDIte, dreduceIte]
|
||||
|
|
@ -736,6 +737,7 @@ theorem balanceR!_eq_balance! {k : α} {v : β k} {l r : Impl α β} (hlb : l.Ba
|
|||
|
||||
theorem balance_eq_balance! {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
|
||||
balance k v l r hlb hrb hlr = balance! k v l r := by
|
||||
set_option tactic.fun_induction.unfolding false in
|
||||
fun_cases balance! k v l r
|
||||
all_goals dsimp only [balance, balance!]
|
||||
all_goals simp only [*]
|
||||
|
|
|
|||
|
|
@ -674,19 +674,20 @@ theorem containsThenInsertIfNew!_snd_eq_insertIfNew! [Ord α] (t : Impl α β) (
|
|||
|
||||
theorem insertMin_eq_insertMin! [Ord α] {a b} {t : Impl α β} (htb) :
|
||||
(t.insertMin a b htb).impl = t.insertMin! a b := by
|
||||
cases a, b, t using insertMin!.fun_cases
|
||||
fun_cases insertMin!
|
||||
· rfl
|
||||
· simp only [insertMin!, insertMin, balanceL_eq_balanceL!, insertMin_eq_insertMin! htb.left]
|
||||
|
||||
theorem insertMax_eq_insertMax! [Ord α] {a b} {t : Impl α β} (htb) :
|
||||
(t.insertMax a b htb).impl = t.insertMax! a b := by
|
||||
cases a, b, t using insertMax!.fun_cases
|
||||
fun_cases insertMax!
|
||||
· rfl
|
||||
· simp only [insertMax!, insertMax, balanceR_eq_balanceR!, insertMax_eq_insertMax! htb.right]
|
||||
|
||||
theorem link_eq_link! [Ord α] {k v} {l r : Impl α β} (hlb hrb) :
|
||||
(link k v l r hlb hrb).impl = link! k v l r := by
|
||||
cases k, v, l, r using link!.fun_cases <;> rw [link, link!]
|
||||
set_option tactic.fun_induction.unfolding false in
|
||||
fun_cases link! <;> rw [link, link!]
|
||||
· rw [insertMin_eq_insertMin!]
|
||||
· rw [insertMax_eq_insertMax!]
|
||||
· split <;> simp only [balanceLErase_eq_balanceL!, link_eq_link! hlb hrb.left]
|
||||
|
|
@ -699,7 +700,8 @@ termination_by sizeOf l + sizeOf r
|
|||
|
||||
theorem link2_eq_link2! [Ord α] {l r : Impl α β} (hlb hrb) :
|
||||
(link2 l r hlb hrb).impl = link2! l r := by
|
||||
cases l, r using link2!.fun_cases <;> rw [link2!, link2]
|
||||
set_option tactic.fun_induction.unfolding false in
|
||||
fun_cases link2! <;> rw [link2!, link2]
|
||||
· split <;> simp only [balanceLErase_eq_balanceL!, link2_eq_link2! hlb hrb.left]
|
||||
· split <;> simp only [balanceRErase_eq_balanceR!, balanceLErase_eq_balanceL!,
|
||||
link2_eq_link2! hlb.right hrb, link2_eq_link2! hlb hrb.left]
|
||||
|
|
|
|||
|
|
@ -167,7 +167,7 @@ theorem toListModel_insertMax [Ord α] {k v} {t : Impl α β} {h} :
|
|||
@[simp]
|
||||
theorem toListModel_link [Ord α] {k v} {l r : Impl α β} {hl hr} :
|
||||
(l.link k v r hl hr).impl.toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel := by
|
||||
cases k, v, l, r, hl, hr using link.fun_cases <;> simp [link] <;> split <;> (try simp; done)
|
||||
fun_cases link <;> simp [link] <;> split <;> (try simp; done)
|
||||
all_goals
|
||||
simp only [toListModel_balanceLErase, toListModel_balanceRErase]
|
||||
rw [toListModel_link]
|
||||
|
|
|
|||
|
|
@ -1,5 +1,7 @@
|
|||
#include "util/options.h"
|
||||
|
||||
// please update stage0
|
||||
|
||||
namespace lean {
|
||||
options get_default_options() {
|
||||
options opts;
|
||||
|
|
|
|||
|
|
@ -1,32 +1,26 @@
|
|||
/--
|
||||
info: Option.map.fun_cases.{u_1, u_2} (motive : {α : Type u_1} → {β : Type u_2} → (α → β) → Option α → Prop)
|
||||
(case1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α), motive f (some x))
|
||||
(case2 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), motive f none) {α : Type u_1} {β : Type u_2} (f : α → β)
|
||||
(x✝ : Option α) : motive f x✝
|
||||
info: Option.map.fun_cases.{u_1} {α : Type u_1} (motive : Option α → Prop) (case1 : ∀ (x : α), motive (some x))
|
||||
(case2 : motive none) (x✝ : Option α) : motive x✝
|
||||
-/
|
||||
#guard_msgs in
|
||||
#guard_msgs(pass trace, all) in
|
||||
#check Option.map.fun_cases
|
||||
|
||||
example (x : Option Nat) (f : Nat → Nat) : (x.map f).isSome = x.isSome := by
|
||||
cases f, x using Option.map.fun_cases
|
||||
cases x using Option.map.fun_cases
|
||||
case case1 x => simp
|
||||
case case2 => simp
|
||||
|
||||
/--
|
||||
info: List.map.fun_cases.{u, v} (motive : {α : Type u} → {β : Type v} → (α → β) → List α → Prop)
|
||||
(case1 : ∀ {α : Type u} {β : Type v} (f : α → β), motive f [])
|
||||
(case2 : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (as : List α), motive f (a :: as)) {α : Type u} {β : Type v}
|
||||
(f : α → β) (x✝ : List α) : motive f x✝
|
||||
info: List.map.fun_cases.{u} {α : Type u} (motive : List α → Prop) (case1 : motive [])
|
||||
(case2 : ∀ (a : α) (as : List α), motive (a :: as)) (x✝ : List α) : motive x✝
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check List.map.fun_cases
|
||||
|
||||
/--
|
||||
info: List.find?.fun_cases.{u} (motive : {α : Type u} → (α → Bool) → List α → Prop)
|
||||
(case1 : ∀ {α : Type u} (p : α → Bool), motive p [])
|
||||
(case2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α), p a = true → motive p (a :: as))
|
||||
(case3 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α), p a = false → motive p (a :: as)) {α : Type u}
|
||||
(p : α → Bool) (x✝ : List α) : motive p x✝
|
||||
info: List.find?.fun_cases.{u} {α : Type u} (p : α → Bool) (motive : List α → Prop) (case1 : motive [])
|
||||
(case2 : ∀ (a : α) (as : List α), p a = true → motive (a :: as))
|
||||
(case3 : ∀ (a : α) (as : List α), p a = false → motive (a :: as)) (x✝ : List α) : motive x✝
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check List.find?.fun_cases
|
||||
|
|
@ -41,8 +35,8 @@ def areTheseTargetsUnchanged (x y : Nat) : Bool :=
|
|||
false
|
||||
|
||||
/--
|
||||
info: areTheseTargetsUnchanged.fun_cases (motive : Nat → Nat → Prop) (case1 : ∀ (y : Nat), motive y y)
|
||||
(case2 : ∀ (x y : Nat), ¬x = y → motive x y) (x y : Nat) : motive x y
|
||||
info: areTheseTargetsUnchanged.fun_cases (x y : Nat) (motive : Prop) (case1 : x = y → motive) (case2 : ¬x = y → motive) :
|
||||
motive
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check areTheseTargetsUnchanged.fun_cases
|
||||
|
|
|
|||
|
|
@ -54,18 +54,16 @@ def fib'' (n : Nat) : Nat :=
|
|||
0
|
||||
|
||||
/--
|
||||
info: fib''.fun_cases_unfolding (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), n < 2 → motive n n)
|
||||
info: fib''.fun_cases_unfolding (n : Nat) (motive : Nat → Prop) (case1 : n < 2 → motive n)
|
||||
(case2 :
|
||||
∀ (n : Nat),
|
||||
¬n < 2 →
|
||||
let foo := n - 2;
|
||||
foo < 100 → motive n (fib'' (n - 1) + fib'' foo))
|
||||
¬n < 2 →
|
||||
let foo := n - 2;
|
||||
foo < 100 → motive (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)
|
||||
¬n < 2 →
|
||||
let foo := n - 2;
|
||||
¬foo < 100 → motive 0) :
|
||||
motive (fib'' n)
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
#check fib''.fun_cases_unfolding
|
||||
|
|
@ -76,20 +74,18 @@ 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✝
|
||||
info: filter.fun_cases (p : Nat → Bool) (motive : List Nat → Prop) (case1 : motive [])
|
||||
(case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive (x :: xs))
|
||||
(case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive (x :: xs)) (x✝ : List Nat) : motive x✝
|
||||
-/
|
||||
#guard_msgs(pass trace, all) 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✝)
|
||||
info: filter.fun_cases_unfolding (p : Nat → Bool) (motive : List Nat → List Nat → Prop) (case1 : motive [] [])
|
||||
(case2 : ∀ (x : Nat) (xs : List Nat), p x = true → motive (x :: xs) (x :: filter p xs))
|
||||
(case3 : ∀ (x : Nat) (xs : List Nat), ¬p x = true → motive (x :: xs) (filter p xs)) (x✝ : List Nat) :
|
||||
motive x✝ (filter p x✝)
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
#check filter.fun_cases_unfolding
|
||||
|
|
@ -138,18 +134,15 @@ def map (f : Nat → Bool) : List Nat → List Bool
|
|||
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✝
|
||||
info: map.fun_cases (motive : List Nat → Prop) (case1 : motive []) (case2 : ∀ (x : Nat) (xs : List Nat), motive (x :: xs))
|
||||
(x✝ : List Nat) : motive x✝
|
||||
-/
|
||||
#guard_msgs(pass trace, all) 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✝)
|
||||
info: map.fun_cases_unfolding (f : Nat → Bool) (motive : List Nat → List Bool → Prop) (case1 : motive [] [])
|
||||
(case2 : ∀ (x : Nat) (xs : List Nat), motive (x :: xs) (f x :: map f xs)) (x✝ : List Nat) : motive x✝ (map f x✝)
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
#check map.fun_cases_unfolding
|
||||
|
|
@ -435,8 +428,8 @@ info: withHave.induct_unfolding (motive : Nat → Bool → Prop) (case1 : 0 < 42
|
|||
#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)
|
||||
info: withHave.fun_cases_unfolding (n : Nat) (motive : Bool → Prop) (case1 : 0 < n → n = 42 → motive true)
|
||||
(case2 : 0 < n → ¬n = 42 → motive (withHave (n - 1))) : motive (withHave n)
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
#check withHave.fun_cases_unfolding
|
||||
|
|
|
|||
|
|
@ -99,8 +99,8 @@ def testMe (n : Nat) : Bool :=
|
|||
| m => false
|
||||
|
||||
/--
|
||||
info: testMe.fun_cases_unfolding (motive : Nat → Bool → Prop) (case1 : ∀ (n : Nat), n - 2 = 0 → motive n true)
|
||||
(case2 : ∀ (n : Nat), (n - 2 = 0 → False) → motive n false) (n : Nat) : motive n (testMe n)
|
||||
info: testMe.fun_cases_unfolding (n : Nat) (motive : Bool → Prop) (case1 : n - 2 = 0 → motive true)
|
||||
(case2 : (n - 2 = 0 → False) → motive false) : motive (testMe n)
|
||||
-/
|
||||
#guard_msgs in
|
||||
#check testMe.fun_cases_unfolding
|
||||
|
|
|
|||
|
|
@ -15,10 +15,10 @@ error: Failed to realize constant myTest.fun_cases:
|
|||
Cannot derive functional cases principle (please report this issue)
|
||||
⏎
|
||||
failed to transform matcher, type error when constructing new pre-splitter motive:
|
||||
@myTest.match_1 _fvar.28 (fun x => @_fvar.27 _fvar.28 _fvar.29 x _fvar.31 _fvar.32) _fvar.30
|
||||
@myTest.match_1 _fvar.27 (fun x => @_fvar.32 x _fvar.34 _fvar.35) _fvar.33
|
||||
⏎
|
||||
Application type mismatch: In the application
|
||||
motive mmotive x✝ h_1
|
||||
motive x✝ h_1
|
||||
the argument
|
||||
h_1
|
||||
has type
|
||||
|
|
|
|||
|
|
@ -10,22 +10,22 @@ def test (f : Unit → MyVec α n) : Nat :=
|
|||
| .cons _ _ => 421
|
||||
|
||||
/--
|
||||
info: test.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
|
||||
info: test.fun_cases_unfolding.{u_1} {α : Type u_1} (motive : {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
|
||||
(case1 :
|
||||
∀ {α : Type u_1} (f : Unit → MyVec α 0),
|
||||
∀ (f : Unit → MyVec α 0),
|
||||
f () = MyVec.nil →
|
||||
motive f
|
||||
(match 0, f (), f with
|
||||
| .(0), MyVec.nil, f => 52
|
||||
| .(n + 1), MyVec.cons a a_1, f => 421))
|
||||
(case2 :
|
||||
∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
|
||||
∀ (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
|
||||
f () = MyVec.cons a a_1 →
|
||||
motive f
|
||||
(match n + 1, f (), f with
|
||||
| .(0), MyVec.nil, f => 52
|
||||
| .(n + 1), MyVec.cons a a_2, f => 421))
|
||||
{α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (test f)
|
||||
{n : Nat} (f : Unit → MyVec α n) : motive f (test f)
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
#check test.fun_cases_unfolding
|
||||
|
|
@ -36,22 +36,22 @@ def alsoTest (f : Unit → MyVec α n) : Nat :=
|
|||
| .cons _ _ => 421
|
||||
|
||||
/--
|
||||
info: alsoTest.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
|
||||
info: alsoTest.fun_cases_unfolding.{u_1} {α : Type u_1} (motive : {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
|
||||
(case1 :
|
||||
∀ {α : Type u_1} (f : Unit → MyVec α 0),
|
||||
∀ (f : Unit → MyVec α 0),
|
||||
f () = MyVec.nil →
|
||||
motive f
|
||||
(match h : 0, h : f (), f with
|
||||
| .(0), MyVec.nil, f_1 => 52
|
||||
| .(n + 1), MyVec.cons a a_1, f_1 => 421))
|
||||
(case2 :
|
||||
∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
|
||||
∀ (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
|
||||
f () = MyVec.cons a a_1 →
|
||||
motive f
|
||||
(match h : n + 1, h : f (), f with
|
||||
| .(0), MyVec.nil, f_1 => 52
|
||||
| .(n_1 + 1), MyVec.cons a a_2, f_1 => 421))
|
||||
{α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (alsoTest f)
|
||||
{n : Nat} (f : Unit → MyVec α n) : motive f (alsoTest f)
|
||||
-/
|
||||
#guard_msgs(pass trace, all) in
|
||||
#check alsoTest.fun_cases_unfolding
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue