5b9567b144
This PR almost completely rewrites the inductive predicate recursion
algorithm; in particular `IndPredBelow` to function more consistently.
Historically, the `brecOn` generation through `IndPredBelow` has been
very error-prone -- this should be fixed now since the new algorithm is
very direct and doesn't rely on tactics or meta-variables at all.
Additionally, the new structural recursion procedure for inductive
predicates shares more code with regular structural recursion and thus
allows for mutual and nested recursion in the same way it was possible
with regular structural recursion. For example, the following works now:
```lean-4
mutual
inductive Even : Nat → Prop where
| zero : Even 0
| succ (h : Odd n) : Even n.succ
inductive Odd : Nat → Prop where
| succ (h : Even n) : Odd n.succ
end
mutual
theorem Even.exists (h : Even n) : ∃ a, n = 2 * a :=
match h with
| .zero => ⟨0, rfl⟩
| .succ h =>
have ⟨a, ha⟩ := h.exists
⟨a + 1, congrArg Nat.succ ha⟩
termination_by structural h
theorem Odd.exists (h : Odd n) : ∃ a, n = 2 * a + 1 :=
match h with
| .succ h =>
have ⟨a, ha⟩ := h.exists
⟨a, congrArg Nat.succ ha⟩
termination_by structural h
end
```
Closes #1672
Closes #10004
229 lines
5.4 KiB
Text
229 lines
5.4 KiB
Text
set_option linter.unusedVariables false
|
||
|
||
inductive PList (α : Type) : Prop
|
||
| nil
|
||
| cons : α → PList α → PList α
|
||
|
||
infixr:67 " ::: " => PList.cons
|
||
|
||
def map {α β} (f : α → β) : List α → List β
|
||
| [] => []
|
||
| a::as => f a :: map f as
|
||
|
||
def pmap {α β} (f : α → β) : PList α → PList β
|
||
| PList.nil => PList.nil
|
||
| a:::as => f a ::: pmap f as
|
||
|
||
theorem ex1 : map Nat.succ [1] = [2] :=
|
||
rfl
|
||
|
||
theorem ex2 : map Nat.succ [] = [] :=
|
||
rfl
|
||
|
||
theorem ex3 (a : Nat) : map Nat.succ [a] = [Nat.succ a] :=
|
||
rfl
|
||
|
||
theorem ex4 {α β} (f : α → β) (a : α) (as : List α) : map f (a::as) = (f a) :: map f as :=
|
||
rfl
|
||
|
||
theorem ex5 {α β} (f : α → β) : map f [] = [] :=
|
||
rfl
|
||
|
||
def map2 {α β} (f : α → β) (as : List α) : List β :=
|
||
let rec loop : List α → List β
|
||
| [] => []
|
||
| a::as => f a :: loop as;
|
||
loop as
|
||
|
||
def pmap2 {α β} (f : α → β) (as : PList α) : PList β :=
|
||
let rec loop : PList α → PList β
|
||
| PList.nil => PList.nil
|
||
| a:::as => f a ::: loop as;
|
||
loop as
|
||
|
||
|
||
theorem ex6 {α β} (f : α → β) (a : α) (as : List α) : map2 f (a::as) = (f a) :: map2 f as :=
|
||
rfl
|
||
|
||
def foo (xs : List Nat) : List Nat :=
|
||
match xs with
|
||
| [] => []
|
||
| x::xs =>
|
||
let y := 2 * x;
|
||
match xs with
|
||
| [] => []
|
||
| x::xs => (y + x) :: foo xs
|
||
|
||
def pfoo (xs : PList Nat) : PList Nat :=
|
||
match xs with
|
||
| PList.nil => PList.nil
|
||
| x:::xs =>
|
||
let y := 2 * x;
|
||
match xs with
|
||
| PList.nil => PList.nil
|
||
| x:::xs => (y + x) ::: pfoo xs
|
||
|
||
#guard foo [1, 2, 3, 4] == [4, 10]
|
||
|
||
theorem fooEq (x y : Nat) (xs : List Nat) : foo (x::y::xs) = (2*x + y) :: foo xs :=
|
||
rfl
|
||
|
||
def bla (x : Nat) (ys : List Nat) : List Nat :=
|
||
if x % 2 == 0 then
|
||
match ys with
|
||
| [] => []
|
||
| y::ys => (y + x/2) :: bla (x/2) ys
|
||
else
|
||
match ys with
|
||
| [] => []
|
||
| y::ys => (y + x/2 + 1) :: bla (x/2) ys
|
||
|
||
def pbla (x : Nat) (ys : PList Nat) : PList Nat :=
|
||
if x % 2 == 0 then
|
||
match ys with
|
||
| PList.nil => PList.nil
|
||
| y:::ys => (y + x/2) ::: pbla (x/2) ys
|
||
else
|
||
match ys with
|
||
| PList.nil => PList.nil
|
||
| y:::ys => (y + x/2 + 1) ::: pbla (x/2) ys
|
||
termination_by structural ys
|
||
|
||
theorem blaEq (y : Nat) (ys : List Nat) : bla 4 (y::ys) = (y+2) :: bla 2 ys :=
|
||
rfl
|
||
|
||
inductive PNat : Prop
|
||
| zero
|
||
| succ : PNat → PNat
|
||
|
||
def f : Nat → Nat → Nat
|
||
| 0, y => y
|
||
| x+1, y =>
|
||
match f x y with
|
||
| 0 => f x y
|
||
| v => f x v + 1
|
||
|
||
def pf : PNat → PNat → PNat
|
||
| PNat.zero, y => y
|
||
| PNat.succ x, y =>
|
||
match pf x y with
|
||
| PNat.zero => pf x y
|
||
| v => PNat.succ $ pf x v
|
||
|
||
def g (xs : List Nat) : Nat :=
|
||
match xs with
|
||
| [] => 0
|
||
| y::ys =>
|
||
match ys with
|
||
| [] => 1
|
||
| _ => g ys + 1
|
||
|
||
def pg (xs : PList Nat) : True :=
|
||
match xs with
|
||
| PList.nil => True.intro
|
||
| y:::ys =>
|
||
match ys with
|
||
| PList.nil => True.intro
|
||
| _ => pg ys
|
||
|
||
def aux : Nat → Nat → Nat
|
||
| 0, y => y
|
||
| x+1, y =>
|
||
match f x y with
|
||
| 0 => f x y
|
||
| v => f x v + 1
|
||
|
||
def paux : PNat → PNat → PNat
|
||
| PNat.zero, y => y
|
||
| PNat.succ x, y =>
|
||
match pf x y with
|
||
| PNat.zero => pf x y
|
||
| v => PNat.succ (pf x v)
|
||
|
||
theorem ex (x y : Nat) : f x y = aux x y := by
|
||
cases x
|
||
rfl
|
||
rfl
|
||
|
||
axiom F : Nat → Nat
|
||
|
||
inductive is_nat : Nat -> Prop
|
||
| Z : is_nat 0
|
||
| S {n} : is_nat n → is_nat (F n)
|
||
|
||
inductive is_nat_T : Nat -> Type
|
||
| Z : is_nat_T 0
|
||
| S {n} : is_nat_T n → is_nat_T (F n)
|
||
|
||
axiom P : Nat → Prop
|
||
axiom F0 : P 0
|
||
axiom F1 : P (F 0)
|
||
axiom FS {n : Nat} : P n → P (F (F n))
|
||
|
||
axiom T : Nat → Prop
|
||
axiom TF0 : T 0
|
||
axiom TF1 : T (F 0)
|
||
axiom TFS {n : Nat} : T n → T (F (F n))
|
||
|
||
-- set_option trace.Elab.definition.structural true in
|
||
theorem «nested recursion» : ∀ {n}, is_nat n → P n
|
||
| _, is_nat.Z => F0
|
||
| _, is_nat.S is_nat.Z => F1
|
||
| _, is_nat.S (is_nat.S h) => FS («nested recursion» h)
|
||
|
||
/-- forbidding this, because it shouldn't exist in the first place.
|
||
We don't expect this kind of inconsistent inaccessible patterns. -/
|
||
-- theorem «nested recursion, inaccessible» : ∀ {n}, is_nat n → P n
|
||
-- | _, .(is_nat.Z) => F0
|
||
-- | _, is_nat.S .(is_nat.Z) => F1
|
||
-- | _, is_nat.S (is_nat.S h) => FS («nested recursion, inaccessible» h)
|
||
|
||
theorem «reordered discriminants, type» : ∀ n, is_nat_T n → Nat → T n := fun n hn m =>
|
||
match n, m, hn with
|
||
| _, _, is_nat_T.Z => TF0
|
||
| _, _, is_nat_T.S is_nat_T.Z => TF1
|
||
| _, m, is_nat_T.S (is_nat_T.S h) => TFS («reordered discriminants, type» _ h m)
|
||
|
||
|
||
theorem «reordered discriminants» : ∀ n, is_nat n → Nat → P n := fun n hn m =>
|
||
match n, m, hn with
|
||
| _, _, is_nat.Z => F0
|
||
| _, _, is_nat.S is_nat.Z => F1
|
||
| _, m, is_nat.S (is_nat.S h) => FS («reordered discriminants» _ h m)
|
||
termination_by structural _ n => n
|
||
|
||
/- known unsupported case for types, just here for reference. -/
|
||
-- def «unsupported nesting» (xs : List Nat) : True :=
|
||
-- match xs with
|
||
-- | List.nil => True.intro
|
||
-- | y::ys =>
|
||
-- match ys with
|
||
-- | List.nil => True.intro
|
||
-- | _::_::zs => «unsupported nesting» zs
|
||
-- | zs => «unsupported nesting» ys
|
||
|
||
def «unsupported nesting, predicate» (xs : PList Nat) : True :=
|
||
match xs with
|
||
| PList.nil => True.intro
|
||
| y:::ys =>
|
||
match ys with
|
||
| PList.nil => True.intro
|
||
| _:::_:::zs => «unsupported nesting, predicate» zs
|
||
| zs => «unsupported nesting, predicate» ys
|
||
|
||
|
||
def f1 (xs : List Nat) : Nat :=
|
||
match xs with
|
||
| [] => 0
|
||
| x::xs =>
|
||
match xs with
|
||
| [] => 0
|
||
| _ => f1 xs + 1
|
||
|
||
def pf1 (xs : PList Nat) : True :=
|
||
match xs with
|
||
| PList.nil => True.intro
|
||
| x:::xs =>
|
||
match xs with
|
||
| PList.nil => True.intro
|
||
| _ => pf1 xs
|