08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
226 lines
9.6 KiB
Text
226 lines
9.6 KiB
Text
def loop (x : Nat) : Unit := loop (x + 1)
|
||
partial_fixpoint
|
||
|
||
/--
|
||
info: loop.fixpoint_induct (motive : (Nat → Unit) → Prop) (adm : Lean.Order.admissible motive)
|
||
(h : ∀ (loop : Nat → Unit), motive loop → motive fun x => loop (x + 1)) : motive loop
|
||
-/
|
||
#guard_msgs in #check loop.fixpoint_induct
|
||
|
||
|
||
/-- error: Unknown constant `loop.partial_correctness` -/
|
||
#guard_msgs in #check loop.partial_correctness
|
||
|
||
|
||
def find (P : Nat → Bool) (x : Nat) : Option Nat :=
|
||
if P x then
|
||
some x
|
||
else
|
||
find P (x +1)
|
||
partial_fixpoint
|
||
|
||
/--
|
||
info: find.fixpoint_induct (P : Nat → Bool) (motive : (Nat → Option Nat) → Prop) (adm : Lean.Order.admissible motive)
|
||
(h : ∀ (find : Nat → Option Nat), motive find → motive fun x => if P x = true then some x else find (x + 1)) :
|
||
motive (find P)
|
||
-/
|
||
#guard_msgs in #check find.fixpoint_induct
|
||
|
||
/--
|
||
info: find.partial_correctness (P : Nat → Bool) (motive : Nat → Nat → Prop)
|
||
(h :
|
||
∀ (find : Nat → Option Nat),
|
||
(∀ (x r : Nat), find x = some r → motive x r) →
|
||
∀ (x r : Nat), (if P x = true then some x else find (x + 1)) = some r → motive x r)
|
||
(x r✝ : Nat) : find P x = some r✝ → motive x r✝
|
||
-/
|
||
#guard_msgs in #check find.partial_correctness
|
||
|
||
def fib (n : Nat) := go 0 0 1
|
||
where
|
||
go i fip fi :=
|
||
if i = n then
|
||
fi
|
||
else
|
||
go (i + 1) fi (fi + fip)
|
||
partial_fixpoint
|
||
|
||
/--
|
||
info: fib.go.fixpoint_induct (n : Nat) (motive : (Nat → Nat → Nat → Nat) → Prop) (adm : Lean.Order.admissible motive)
|
||
(h :
|
||
∀ (go : Nat → Nat → Nat → Nat), motive go → motive fun i fip fi => if i = n then fi else go (i + 1) fi (fi + fip)) :
|
||
motive (fib.go n)
|
||
-/
|
||
#guard_msgs in #check fib.go.fixpoint_induct
|
||
|
||
|
||
local instance (b : Bool) [Nonempty α] [Nonempty β] : Nonempty (cond b α β) := by
|
||
cases b <;> assumption
|
||
local instance (b : Bool) [Nonempty α] [Nonempty β] : Nonempty (if b then α else β) := by
|
||
split <;> assumption
|
||
|
||
mutual
|
||
def dependent2''a (m n : Nat) (b : Bool) : if b then Nat else Bool :=
|
||
if _ : b then dependent2''a m (n + 1) b else dependent2''b m m (n + m) b
|
||
partial_fixpoint
|
||
def dependent2''b (m k n : Nat) (b : Bool) : if b then Nat else Bool :=
|
||
if b then dependent2''b m k n b else dependent2''c m (.last _) (n + m) b
|
||
partial_fixpoint
|
||
def dependent2''c (m : Nat) (i : Fin (m+1)) (n : Nat) (b : Bool) : if b then Nat else Bool :=
|
||
if b then dependent2''c m i n b else dependent2''a m i b
|
||
partial_fixpoint
|
||
end
|
||
|
||
/--
|
||
info: dependent2''a.mutual_fixpoint_induct (m : Nat) (b : Bool) (motive_1 : (Nat → if b = true then Nat else Bool) → Prop)
|
||
(motive_2 : (Nat → Nat → if b = true then Nat else Bool) → Prop)
|
||
(motive_3 : (Fin (m + 1) → Nat → if b = true then Nat else Bool) → Prop) (adm_1 : Lean.Order.admissible motive_1)
|
||
(adm_2 : Lean.Order.admissible motive_2) (adm_3 : Lean.Order.admissible motive_3)
|
||
(h_1 :
|
||
∀ (dependent2''a : Nat → if b = true then Nat else Bool)
|
||
(dependent2''b : Nat → Nat → if b = true then Nat else Bool),
|
||
motive_1 dependent2''a →
|
||
motive_2 dependent2''b →
|
||
motive_1 fun n => if x : b = true then dependent2''a (n + 1) else dependent2''b m (n + m))
|
||
(h_2 :
|
||
∀ (dependent2''b : Nat → Nat → if b = true then Nat else Bool)
|
||
(dependent2''c : Fin (m + 1) → Nat → if b = true then Nat else Bool),
|
||
motive_2 dependent2''b →
|
||
motive_3 dependent2''c →
|
||
motive_2 fun k n => if b = true then dependent2''b k n else dependent2''c (Fin.last m) (n + m))
|
||
(h_3 :
|
||
∀ (dependent2''a : Nat → if b = true then Nat else Bool)
|
||
(dependent2''c : Fin (m + 1) → Nat → if b = true then Nat else Bool),
|
||
motive_1 dependent2''a →
|
||
motive_3 dependent2''c → motive_3 fun i n => if b = true then dependent2''c i n else dependent2''a ↑i) :
|
||
(motive_1 fun n => dependent2''a m n b) ∧
|
||
(motive_2 fun k n => dependent2''b m k n b) ∧ motive_3 fun i n => dependent2''c m i n b
|
||
-/
|
||
#guard_msgs in #check dependent2''a.mutual_fixpoint_induct
|
||
|
||
mutual
|
||
def dependent3''a (m n : Nat) (b : Bool) : Option (if b then Nat else Bool) :=
|
||
if _ : b then dependent3''a m (n + 1) b else dependent3''b m m (n + m) b
|
||
partial_fixpoint
|
||
def dependent3''b (m k n : Nat) (b : Bool) : Option (if b then Nat else Bool) :=
|
||
if b then dependent3''b m k n b else dependent3''c m (.last _) (n + m) b
|
||
partial_fixpoint
|
||
def dependent3''c (m : Nat) (i : Fin (m+1)) (n : Nat) (b : Bool) : Option (if b then Nat else Bool) :=
|
||
if b then dependent3''c m i n b else dependent3''a m i b
|
||
partial_fixpoint
|
||
end
|
||
|
||
/--
|
||
info: dependent3''a.mutual_partial_correctness (m : Nat) (b : Bool) (motive_1 : Nat → (if b = true then Nat else Bool) → Prop)
|
||
(motive_2 : Nat → Nat → (if b = true then Nat else Bool) → Prop)
|
||
(motive_3 : Fin (m + 1) → Nat → (if b = true then Nat else Bool) → Prop)
|
||
(h_1 :
|
||
∀ (dependent3''a : Nat → Option (if b = true then Nat else Bool))
|
||
(dependent3''b : Nat → Nat → Option (if b = true then Nat else Bool)),
|
||
(∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a n = some r → motive_1 n r) →
|
||
(∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b k n = some r → motive_2 k n r) →
|
||
∀ (n : Nat) (r : if b = true then Nat else Bool),
|
||
(if x : b = true then dependent3''a (n + 1) else dependent3''b m (n + m)) = some r → motive_1 n r)
|
||
(h_2 :
|
||
∀ (dependent3''b : Nat → Nat → Option (if b = true then Nat else Bool))
|
||
(dependent3''c : Fin (m + 1) → Nat → Option (if b = true then Nat else Bool)),
|
||
(∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b k n = some r → motive_2 k n r) →
|
||
(∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool),
|
||
dependent3''c i n = some r → motive_3 i n r) →
|
||
∀ (k n : Nat) (r : if b = true then Nat else Bool),
|
||
(if b = true then dependent3''b k n else dependent3''c (Fin.last m) (n + m)) = some r → motive_2 k n r)
|
||
(h_3 :
|
||
∀ (dependent3''a : Nat → Option (if b = true then Nat else Bool))
|
||
(dependent3''c : Fin (m + 1) → Nat → Option (if b = true then Nat else Bool)),
|
||
(∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a n = some r → motive_1 n r) →
|
||
(∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool),
|
||
dependent3''c i n = some r → motive_3 i n r) →
|
||
∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool),
|
||
(if b = true then dependent3''c i n else dependent3''a ↑i) = some r → motive_3 i n r) :
|
||
(∀ (n : Nat) (r : if b = true then Nat else Bool), dependent3''a m n b = some r → motive_1 n r) ∧
|
||
(∀ (k n : Nat) (r : if b = true then Nat else Bool), dependent3''b m k n b = some r → motive_2 k n r) ∧
|
||
∀ (i : Fin (m + 1)) (n : Nat) (r : if b = true then Nat else Bool),
|
||
dependent3''c m i n b = some r → motive_3 i n r
|
||
-/
|
||
#guard_msgs in #check dependent3''a.mutual_partial_correctness
|
||
|
||
-- The following example appears in the manual; having it here alerts us early of breakage
|
||
|
||
def List.findIndex (xs : List α) (p : α → Bool) : Option Nat := match xs with
|
||
| [] => none
|
||
| x::ys =>
|
||
if p x then
|
||
some 0
|
||
else
|
||
(· + 1) <$> List.findIndex ys p
|
||
partial_fixpoint
|
||
|
||
/--
|
||
info: List.findIndex.partial_correctness.{u_1} {α : Type u_1} (p : α → Bool) (motive : List α → Nat → Prop)
|
||
(h :
|
||
∀ (findIndex : List α → Option Nat),
|
||
(∀ (xs : List α) (r : Nat), findIndex xs = some r → motive xs r) →
|
||
∀ (xs : List α) (r : Nat),
|
||
(match xs with
|
||
| [] => none
|
||
| x :: ys => if p x = true then some 0 else (fun x => x + 1) <$> findIndex ys) =
|
||
some r →
|
||
motive xs r)
|
||
(xs : List α) (r✝ : Nat) : xs.findIndex p = some r✝ → motive xs r✝
|
||
-/
|
||
#guard_msgs in
|
||
#check List.findIndex.partial_correctness
|
||
|
||
theorem List.findIndex_implies_pred (xs : List α) (p : α → Bool) :
|
||
xs.findIndex p = some i → xs[i]?.any p := by
|
||
apply List.findIndex.partial_correctness (motive := fun xs i => xs[i]?.any p)
|
||
intro findIndex ih xs r hsome
|
||
split at hsome
|
||
next => contradiction
|
||
next x ys =>
|
||
split at hsome
|
||
next =>
|
||
have : r = 0 := by simp_all
|
||
simp_all
|
||
next =>
|
||
simp only [Option.map_eq_map, Option.map_eq_some_iff] at hsome
|
||
obtain ⟨r', hr, rfl⟩ := hsome
|
||
specialize ih _ _ hr
|
||
simpa
|
||
|
||
mutual
|
||
def f (n : Nat) : Option Nat :=
|
||
g (n + 1)
|
||
partial_fixpoint
|
||
|
||
def g (n : Nat) : Option Nat :=
|
||
if n = 0 then .none else f (n + 1)
|
||
partial_fixpoint
|
||
end
|
||
/--
|
||
info: f.mutual_partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
|
||
(h_1 :
|
||
∀ (g : Nat → Option Nat),
|
||
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
|
||
(h_2 :
|
||
∀ (f : Nat → Option Nat),
|
||
(∀ (n r : Nat), f n = some r → motive_1 n r) →
|
||
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r) :
|
||
(∀ (n r : Nat), f n = some r → motive_1 n r) ∧ ∀ (n r : Nat), g n = some r → motive_2 n r
|
||
-/
|
||
#guard_msgs in
|
||
#check f.mutual_partial_correctness
|
||
|
||
/--
|
||
info: f.partial_correctness (motive_1 motive_2 : Nat → Nat → Prop)
|
||
(h_1 :
|
||
∀ (g : Nat → Option Nat),
|
||
(∀ (n r : Nat), g n = some r → motive_2 n r) → ∀ (n r : Nat), g (n + 1) = some r → motive_1 n r)
|
||
(h_2 :
|
||
∀ (f : Nat → Option Nat),
|
||
(∀ (n r : Nat), f n = some r → motive_1 n r) →
|
||
∀ (n r : Nat), (if n = 0 then none else f (n + 1)) = some r → motive_2 n r)
|
||
(n r✝ : Nat) : f n = some r✝ → motive_1 n r✝
|
||
-/
|
||
#guard_msgs in
|
||
#check f.partial_correctness
|