lean2/tests/lean/run/div2.lean
Leonardo de Moura 064ecd3e3d refactor(library/data/nat): declare lt and le asap using inductive definitions, and make key theorems transparent for definitional package
We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.
2014-11-22 00:19:39 -08:00

120 lines
4.8 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import logic data.nat.sub algebra.relation data.prod
import tools.fake_simplifier
open nat relation relation.iff_ops prod
open fake_simplifier decidable
open eq.ops
namespace nat
-- A general recursion principle
-- -----------------------------
--
-- Data:
--
-- dom, codom : Type
-- default : codom
-- measure : dom →
-- rec_val : dom → (dom → codom) → codom
--
-- and a proof
--
-- rec_decreasing : ∀m, m ≥ measure x, rec_val x f = rec_val x (restrict f m)
--
-- ... which says that the recursive call only depends on f at values with measure less than x,
-- in the sense that changing other values to the default value doesn't change the result.
--
-- The result is a function f = rec_measure, satisfying
--
-- f x = rec_val x f
definition restrict {dom codom : Type} (default : codom) (measure : dom → ) (f : dom → codom)
(m : ) (x : dom) :=
if measure x < m then f x else default
theorem restrict_lt_eq {dom codom : Type} (default : codom) (measure : dom → ) (f : dom → codom)
(m : ) (x : dom) (H : measure x < m) :
restrict default measure f m x = f x :=
if_pos H
theorem restrict_not_lt_eq {dom codom : Type} (default : codom) (measure : dom → )
(f : dom → codom) (m : ) (x : dom) (H : ¬ measure x < m) :
restrict default measure f m x = default :=
if_neg H
definition rec_measure_aux {dom codom : Type} (default : codom) (measure : dom → )
(rec_val : dom → (dom → codom) → codom) : → dom → codom :=
rec (λx, default) (λm g x, if measure x < succ m then rec_val x g else default)
definition rec_measure {dom codom : Type} (default : codom) (measure : dom → )
(rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
rec_measure_aux default measure rec_val (succ (measure x)) x
theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → )
(rec_val : dom → (dom → codom) → codom)
(rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) →
rec_val x g1 = rec_val x g2)
(m : ) :
let f' := rec_measure_aux default measure rec_val in
let f := rec_measure default measure rec_val in
∀x, f' m x = restrict default measure f m x :=
let f' := rec_measure_aux default measure rec_val in
let f := rec_measure default measure rec_val in
case_strong_induction_on m
(take x,
have H1 : f' 0 x = default, from rfl,
have H2 : ¬ measure x < 0, from !not_lt_zero,
have H3 : restrict default measure f 0 x = default, from if_neg H2,
show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹)
(take m,
assume IH: ∀n, n ≤ m → ∀x, f' n x = restrict default measure f n x,
take x : dom,
show f' (succ m) x = restrict default measure f (succ m) x, from
by_cases -- (measure x < succ m)
(assume H1 : measure x < succ m,
have H2a : ∀z, measure z < measure x → f' m z = f z,
proof
take z,
assume Hzx : measure z < measure x,
calc
f' m z = restrict default measure f m z : IH m !le_refl z
... = f z : !restrict_lt_eq (lt_le.trans Hzx (lt_succ_imp_le H1))
∎,
have H2 : f' (succ m) x = rec_val x f,
proof
calc
f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
... = rec_val x (f' m) : if_pos H1
... = rec_val x f : rec_decreasing (f' m) f x H2a
∎,
let m' := measure x in
have H3a : ∀z, measure z < m' → f' m' z = f z,
proof
take z,
assume Hzx : measure z < measure x,
calc
f' m' z = restrict default measure f m' z : IH _ (lt_succ_imp_le H1) _
... = f z : !restrict_lt_eq Hzx
qed,
have H3 : restrict default measure f (succ m) x = rec_val x f,
proof
calc
restrict default measure f (succ m) x = f x : if_pos H1
... = f' (succ m') x : !eq.refl
... = if measure x < succ m' then rec_val x (f' m') else default : rfl
... = rec_val x (f' m') : if_pos !self_lt_succ
... = rec_val x f : rec_decreasing _ _ _ H3a
qed,
show f' (succ m) x = restrict default measure f (succ m) x,
from H2 ⬝ H3⁻¹)
(assume H1 : ¬ measure x < succ m,
have H2 : f' (succ m) x = default, from
calc
f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl
... = default : if_neg H1,
have H3 : restrict default measure f (succ m) x = default,
from if_neg H1,
show f' (succ m) x = restrict default measure f (succ m) x,
from H2 ⬝ H3⁻¹))
end nat