4ee131981d
This modification is relevant for fixing regressions on recent changes to the auto implicit behavior for inductive families. The following declarations are now accepted: ```lean inductive HasType : Fin n → Vector Ty n → Ty → Type where | stop : HasType 0 (ty :: ctx) ty | pop : HasType k ctx ty → HasType k.succ (u :: ctx) ty inductive Sublist : List α → List α → Prop | slnil : Sublist [] [] | cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂) | cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂) inductive Lst : Type u → Type u | nil : Lst α | cons : α → Lst α → Lst α ``` TODO: universe inference for `inductive` should be improved. The current approach is not good enough when we have auto implicits. TODO: allow implicit fixed indices that do not depend on indices that cannot be moved to become parameters.
117 lines
3.8 KiB
Text
117 lines
3.8 KiB
Text
import Lean
|
||
open Lean
|
||
|
||
namespace Ex
|
||
inductive LE : Nat → Nat → Prop
|
||
| refl : LE n n
|
||
| succ : LE n m → LE n m.succ
|
||
|
||
|
||
def typeOf {α : Sort u} (a : α) := α
|
||
|
||
theorem LE.trans' : LE m n → LE n o → LE m o
|
||
| h1, refl => h1
|
||
| h1, succ h2 => succ (trans' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
|
||
|
||
inductive Even : Nat → Prop
|
||
| zero : Even 0
|
||
| ss : Even n → Even n.succ.succ
|
||
|
||
theorem Even_brecOn : typeOf @Even.brecOn = ∀ {motive : (a : Nat) → Even a → Prop} {a : Nat} (x : Even a),
|
||
(∀ (a : Nat) (x : Even a), @Even.below motive a x → motive a x) → motive a x := rfl
|
||
|
||
theorem Even.add : Even n → Even m → Even (n+m) := by
|
||
intro h1 h2
|
||
induction h2 with
|
||
| zero => exact h1
|
||
| ss h2 ih => exact ss ih
|
||
|
||
theorem Even.add' : Even n → Even m → Even (n+m)
|
||
| h1, zero => h1
|
||
| h1, ss h2 => ss (add' h1 h2) -- the structural recursion in being performed on the implicit `Nat` parameter
|
||
|
||
theorem mul_left_comm (n m o : Nat) : n * (m * o) = m * (n * o) := by
|
||
rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]
|
||
|
||
inductive Power2 : Nat → Prop
|
||
| base : Power2 1
|
||
| ind : Power2 n → Power2 (2*n) -- Note that index here is not a constructor
|
||
|
||
theorem Power2_brecOn : typeOf @Power2.brecOn = ∀ {motive : (a : Nat) → Power2 a → Prop} {a : Nat} (x : Power2 a),
|
||
(∀ (a : Nat) (x : Power2 a), @Power2.below motive a x → motive a x) → motive a x := rfl
|
||
|
||
theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
|
||
intro h1 h2
|
||
induction h2 with
|
||
| base => simp_all
|
||
| ind h2 ih => exact mul_left_comm .. ▸ ind ih
|
||
|
||
/- The following example fails because the structural recursion cannot be performed on the `Nat`s and
|
||
the `brecOn` construction doesn't work for inductive predicates -/
|
||
set_option trace.Elab.definition.structural true in
|
||
set_option trace.Meta.IndPredBelow.match true in
|
||
set_option pp.explicit true in
|
||
theorem Power2.mul' : Power2 n → Power2 m → Power2 (n*m)
|
||
| h1, base => by simp_all
|
||
| h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)
|
||
|
||
inductive tm : Type :=
|
||
| C : Nat → tm
|
||
| P : tm → tm → tm
|
||
|
||
open tm
|
||
|
||
set_option hygiene false in
|
||
infixl:40 " ==> " => step
|
||
inductive step : tm → tm → Prop :=
|
||
| ST_PlusConstConst : ∀ n1 n2,
|
||
P (C n1) (C n2) ==> C (n1 + n2)
|
||
| ST_Plus1 : ∀ t1 t1' t2,
|
||
t1 ==> t1' →
|
||
P t1 t2 ==> P t1' t2
|
||
| ST_Plus2 : ∀ n1 t2 t2',
|
||
t2 ==> t2' →
|
||
P (C n1) t2 ==> P (C n1) t2'
|
||
|
||
def deterministic {X : Type} (R : X → X → Prop) :=
|
||
∀ x y1 y2 : X, R x y1 → R x y2 → y1 = y2
|
||
|
||
theorem step_deterministic' : deterministic step := λ x y₁ y₂ hy₁ hy₂ =>
|
||
@step.brecOn (λ s t st => ∀ y₂, s ==> y₂ → t = y₂) _ _ hy₁ (λ s t st hy₁ y₂ hy₂ =>
|
||
match hy₁, hy₂ with
|
||
| step.below.ST_PlusConstConst _ _, step.ST_PlusConstConst _ _ => rfl
|
||
| step.below.ST_Plus1 _ _ _ hy₁ ih, step.ST_Plus1 _ t₁' _ _ => by rw [←ih t₁']; assumption
|
||
| step.below.ST_Plus1 _ _ _ hy₁ ih, step.ST_Plus2 _ _ _ _ => by cases hy₁
|
||
| step.below.ST_Plus2 _ _ _ _ ih, step.ST_Plus2 _ _ t₂ _ => by rw [←ih t₂]; assumption
|
||
| step.below.ST_Plus2 _ _ _ hy₁ _, step.ST_PlusConstConst _ _ => by cases hy₁
|
||
) y₂ hy₂
|
||
|
||
section NestedRecursion
|
||
|
||
axiom f : Nat → Nat
|
||
|
||
inductive is_nat : Nat -> Prop
|
||
| Z : is_nat 0
|
||
| S {n} : is_nat n → is_nat (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))
|
||
|
||
-- we would like to write this
|
||
theorem foo : ∀ {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 (foo h)
|
||
|
||
theorem foo' : ∀ {n}, is_nat n → P n := fun h =>
|
||
@is_nat.brecOn (fun n hn => P n) _ h fun n h ih =>
|
||
match ih with
|
||
| is_nat.below.Z => F0
|
||
| is_nat.below.S is_nat.below.Z _ => F1
|
||
| is_nat.below.S (is_nat.below.S b hx) h₂ => FS hx
|
||
|
||
end NestedRecursion
|
||
|
||
end Ex
|