feat(frontends/lean): 'let [inline]' is the default
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
0df87bae24
commit
07bc0727e2
9 changed files with 107 additions and 147 deletions
|
|
@ -62,7 +62,7 @@ calc_subst subst
|
|||
theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
|
||||
assume H : succ n = 0,
|
||||
have H2 : true = false, from
|
||||
let f [inline] := (nat_rec false (fun a b, true)) in
|
||||
let f := (nat_rec false (fun a b, true)) in
|
||||
calc
|
||||
true = f (succ n) : rfl
|
||||
... = f 0 : {H}
|
||||
|
|
@ -115,19 +115,19 @@ have general : ∀n, decidable (n = m), from
|
|||
rec_on m
|
||||
(take n,
|
||||
rec_on n
|
||||
(inl (refl 0))
|
||||
(λ m iH, inr (succ_ne_zero m)))
|
||||
(inl (refl 0))
|
||||
(λ m iH, inr (succ_ne_zero m)))
|
||||
(λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')),
|
||||
take n, rec_on n
|
||||
(inr (ne_symm (succ_ne_zero m')))
|
||||
(λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
|
||||
have d1 : decidable (n' = m'), from iH1 n',
|
||||
decidable.rec_on d1
|
||||
(assume Heq : n' = m', inl (congr_arg succ Heq))
|
||||
(assume Hne : n' ≠ m',
|
||||
have H1 : succ n' ≠ succ m', from
|
||||
assume Heq, absurd (succ_inj Heq) Hne,
|
||||
inr H1))),
|
||||
(inr (ne_symm (succ_ne_zero m')))
|
||||
(λ (n' : ℕ) (iH2 : decidable (n' = succ m')),
|
||||
have d1 : decidable (n' = m'), from iH1 n',
|
||||
decidable.rec_on d1
|
||||
(assume Heq : n' = m', inl (congr_arg succ Heq))
|
||||
(assume Hne : n' ≠ m',
|
||||
have H1 : succ n' ≠ succ m', from
|
||||
assume Heq, absurd (succ_inj Heq) Hne,
|
||||
inr H1))),
|
||||
general n
|
||||
|
||||
theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1)
|
||||
|
|
@ -138,7 +138,7 @@ have stronger : P a ∧ P (succ a), from
|
|||
(take k IH,
|
||||
have IH1 : P k, from and_elim_left IH,
|
||||
have IH2 : P (succ k), from and_elim_right IH,
|
||||
and_intro IH2 (H3 k IH1 IH2)),
|
||||
and_intro IH2 (H3 k IH1 IH2)),
|
||||
and_elim_left stronger
|
||||
|
||||
theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
|
||||
|
|
@ -150,10 +150,10 @@ have general : ∀m, P n m, from induction_on n
|
|||
take m : ℕ,
|
||||
discriminate
|
||||
(assume Hm : m = 0,
|
||||
Hm⁻¹ ▸ (H2 k))
|
||||
Hm⁻¹ ▸ (H2 k))
|
||||
(take l : ℕ,
|
||||
assume Hm : m = succ l,
|
||||
Hm⁻¹ ▸ (H3 k l (IH l)))),
|
||||
assume Hm : m = succ l,
|
||||
Hm⁻¹ ▸ (H3 k l (IH l)))),
|
||||
general m
|
||||
|
||||
|
||||
|
|
@ -237,14 +237,14 @@ induction_on n
|
|||
(take H : 0 + m = 0 + k,
|
||||
calc
|
||||
m = 0 + m : symm (add_zero_left m)
|
||||
... = 0 + k : H
|
||||
... = k : add_zero_left k)
|
||||
... = 0 + k : H
|
||||
... = k : add_zero_left k)
|
||||
(take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
|
||||
have H2 : succ (n + m) = succ (n + k),
|
||||
from calc
|
||||
succ (n + m) = succ n + m : symm (add_succ_left n m)
|
||||
... = succ n + k : H
|
||||
... = succ (n + k) : add_succ_left n k,
|
||||
... = succ n + k : H
|
||||
... = succ (n + k) : add_succ_left n k,
|
||||
have H3 : n + m = n + k, from succ_inj H2,
|
||||
IH H3)
|
||||
|
||||
|
|
@ -263,9 +263,9 @@ induction_on n
|
|||
assume (H : succ k + m = 0),
|
||||
absurd_elim (succ k = 0)
|
||||
(show succ (k + m) = 0, from
|
||||
calc
|
||||
succ (k + m) = succ k + m : symm (add_succ_left k m)
|
||||
... = 0 : H)
|
||||
calc
|
||||
succ (k + m) = succ k + m : symm (add_succ_left k m)
|
||||
... = 0 : H)
|
||||
(succ_ne_zero (k + m)))
|
||||
|
||||
theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 :=
|
||||
|
|
@ -313,8 +313,8 @@ induction_on n
|
|||
(take m IH,
|
||||
calc
|
||||
0 * succ m = 0 * m + 0 : mul_succ_right _ _
|
||||
... = 0 * m : add_zero_right _
|
||||
... = 0 : IH)
|
||||
... = 0 * m : add_zero_right _
|
||||
... = 0 : IH)
|
||||
|
||||
theorem mul_succ_left (n m:ℕ) : (succ n) * m = (n * m) + m :=
|
||||
induction_on m
|
||||
|
|
@ -325,11 +325,11 @@ induction_on m
|
|||
(take k IH,
|
||||
calc
|
||||
succ n * succ k = (succ n * k) + succ n : mul_succ_right _ _
|
||||
... = (n * k) + k + succ n : { IH }
|
||||
... = (n * k) + (k + succ n) : add_assoc _ _ _
|
||||
... = (n * k) + (n + succ k) : {add_comm_succ _ _}
|
||||
... = (n * k) + n + succ k : symm (add_assoc _ _ _)
|
||||
... = (n * succ k) + succ k : {symm (mul_succ_right n k)})
|
||||
... = (n * k) + k + succ n : { IH }
|
||||
... = (n * k) + (k + succ n) : add_assoc _ _ _
|
||||
... = (n * k) + (n + succ k) : {add_comm_succ _ _}
|
||||
... = (n * k) + n + succ k : symm (add_assoc _ _ _)
|
||||
... = (n * succ k) + succ k : {symm (mul_succ_right n k)})
|
||||
|
||||
theorem mul_comm (n m:ℕ) : n * m = m * n :=
|
||||
induction_on m
|
||||
|
|
@ -337,8 +337,8 @@ induction_on m
|
|||
(take k IH,
|
||||
calc
|
||||
n * succ k = n * k + n : mul_succ_right _ _
|
||||
... = k * n + n : {IH}
|
||||
... = (succ k) * n : symm (mul_succ_left _ _))
|
||||
... = k * n + n : {IH}
|
||||
... = (succ k) * n : symm (mul_succ_left _ _))
|
||||
|
||||
theorem mul_distr_right (n m k : ℕ) : (n + m) * k = n * k + m * k :=
|
||||
induction_on k
|
||||
|
|
@ -349,12 +349,12 @@ induction_on k
|
|||
... = n * 0 + m * 0 : {symm (mul_zero_right _)})
|
||||
(take l IH, calc
|
||||
(n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right _ _
|
||||
... = n * l + m * l + (n + m) : {IH}
|
||||
... = n * l + m * l + n + m : symm (add_assoc _ _ _)
|
||||
... = n * l + n + m * l + m : {add_right_comm _ _ _}
|
||||
... = n * l + n + (m * l + m) : add_assoc _ _ _
|
||||
... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
|
||||
... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
|
||||
... = n * l + m * l + (n + m) : {IH}
|
||||
... = n * l + m * l + n + m : symm (add_assoc _ _ _)
|
||||
... = n * l + n + m * l + m : {add_right_comm _ _ _}
|
||||
... = n * l + n + (m * l + m) : add_assoc _ _ _
|
||||
... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
|
||||
... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
|
||||
|
||||
theorem mul_distr_left (n m k : ℕ) : n * (m + k) = n * m + n * k :=
|
||||
calc
|
||||
|
|
@ -372,9 +372,9 @@ induction_on k
|
|||
(take l IH,
|
||||
calc
|
||||
(n * m) * succ l = (n * m) * l + n * m : mul_succ_right _ _
|
||||
... = n * (m * l) + n * m : {IH}
|
||||
... = n * (m * l + m) : symm (mul_distr_left _ _ _)
|
||||
... = n * (m * succ l) : {symm (mul_succ_right _ _)})
|
||||
... = n * (m * l) + n * m : {IH}
|
||||
... = n * (m * l + m) : symm (mul_distr_left _ _ _)
|
||||
... = n * (m * succ l) : {symm (mul_succ_right _ _)})
|
||||
|
||||
theorem mul_left_comm (n m k : ℕ) : n * (m * k) = m * (n * k) :=
|
||||
left_comm mul_comm mul_assoc n m k
|
||||
|
|
@ -401,14 +401,14 @@ discriminate
|
|||
discriminate
|
||||
(take (Hm : m = 0), or_intro_right _ Hm)
|
||||
(take (l : ℕ),
|
||||
assume (Hl : m = succ l),
|
||||
have Heq : succ (k * succ l + l) = n * m, from
|
||||
symm (calc
|
||||
n * m = n * succ l : {Hl}
|
||||
... = succ k * succ l : {Hk}
|
||||
... = k * succ l + succ l : mul_succ_left _ _
|
||||
... = succ (k * succ l + l) : add_succ_right _ _),
|
||||
absurd_elim _ (trans Heq H) (succ_ne_zero _)))
|
||||
assume (Hl : m = succ l),
|
||||
have Heq : succ (k * succ l + l) = n * m, from
|
||||
symm (calc
|
||||
n * m = n * succ l : {Hl}
|
||||
... = succ k * succ l : {Hk}
|
||||
... = k * succ l + succ l : mul_succ_left _ _
|
||||
... = succ (k * succ l + l) : add_succ_right _ _),
|
||||
absurd_elim _ (trans Heq H) (succ_ne_zero _)))
|
||||
|
||||
---other inversion theorems appear below
|
||||
|
||||
|
|
|
|||
|
|
@ -87,8 +87,8 @@ theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom
|
|||
let f := rec_measure default measure rec_val in
|
||||
f' m = restrict default measure f m :=
|
||||
-- TODO: note the use of (need for) inline here
|
||||
let f' [inline] := rec_measure_aux default measure rec_val in
|
||||
let f [inline] := rec_measure default measure rec_val in
|
||||
let f' := rec_measure_aux default measure rec_val in
|
||||
let f := rec_measure default measure rec_val in
|
||||
case_strong_induction_on m
|
||||
(have H1 : f' 0 = (λx, default), from rfl,
|
||||
have H2 : restrict default measure f 0 = (λx, default), from
|
||||
|
|
@ -111,7 +111,7 @@ case_strong_induction_on m
|
|||
... = rec_val x (restrict default measure f m) : {IH m (le_refl m)}
|
||||
... = rec_val x f : symm (rec_decreasing _ _ _ (lt_succ_imp_le H1)),
|
||||
have H3 : restrict default measure f (succ m) x = rec_val x f, from
|
||||
let m' [inline] := measure x in
|
||||
let m' := measure x in
|
||||
calc
|
||||
restrict default measure f (succ m) x = f x : if_pos H1 _ _
|
||||
... = f' (succ m') x : refl _
|
||||
|
|
@ -138,9 +138,9 @@ theorem rec_measure_spec {dom codom : Type} {default : codom} {measure : dom →
|
|||
(x : dom):
|
||||
let f := rec_measure default measure rec_val in
|
||||
f x = rec_val x f :=
|
||||
let f' [inline] := rec_measure_aux default measure rec_val in
|
||||
let f [inline] := rec_measure default measure rec_val in
|
||||
let m [inline] := measure x in
|
||||
let f' := rec_measure_aux default measure rec_val in
|
||||
let f := rec_measure default measure rec_val in
|
||||
let m := measure x in
|
||||
calc
|
||||
f x = f' (succ m) x : refl _
|
||||
... = if measure x < succ m then rec_val x (f' m) else default : rfl
|
||||
|
|
@ -162,8 +162,8 @@ definition div_aux (y : ℕ) : ℕ → ℕ := rec_measure 0 (fun x, x) (div_aux_
|
|||
|
||||
theorem div_aux_decreasing (y : ℕ) (g : ℕ → ℕ) (m : ℕ) (x : ℕ) (H : m ≥ x) :
|
||||
div_aux_rec y x g = div_aux_rec y x (restrict 0 (fun x, x) g m) :=
|
||||
let lhs [inline] := div_aux_rec y x g in
|
||||
let rhs [inline] := div_aux_rec y x (restrict 0 (fun x, x) g m) in
|
||||
let lhs := div_aux_rec y x g in
|
||||
let rhs := div_aux_rec y x (restrict 0 (fun x, x) g m) in
|
||||
show lhs = rhs, from
|
||||
by_cases (y = 0 ∨ x < y)
|
||||
(assume H1 : y = 0 ∨ x < y,
|
||||
|
|
@ -238,8 +238,8 @@ definition mod_aux (y : ℕ) : ℕ → ℕ := rec_measure 0 (fun x, x) (mod_aux_
|
|||
|
||||
theorem mod_aux_decreasing (y : ℕ) (g : ℕ → ℕ) (m : ℕ) (x : ℕ) (H : m ≥ x) :
|
||||
mod_aux_rec y x g = mod_aux_rec y x (restrict 0 (fun x, x) g m) :=
|
||||
let lhs [inline] := mod_aux_rec y x g in
|
||||
let rhs [inline] := mod_aux_rec y x (restrict 0 (fun x, x) g m) in
|
||||
let lhs := mod_aux_rec y x g in
|
||||
let rhs := mod_aux_rec y x (restrict 0 (fun x, x) g m) in
|
||||
show lhs = rhs, from
|
||||
by_cases (y = 0 ∨ x < y)
|
||||
(assume H1 : y = 0 ∨ x < y,
|
||||
|
|
@ -596,17 +596,17 @@ definition gcd_aux_measure (p : ℕ × ℕ) : ℕ :=
|
|||
pr2 p
|
||||
|
||||
definition gcd_aux_rec (p : ℕ × ℕ) (gcd_aux' : ℕ × ℕ → ℕ) : ℕ :=
|
||||
let x [inline] := pr1 p, y [inline] := pr2 p in
|
||||
let x := pr1 p, y := pr2 p in
|
||||
if y = 0 then x else gcd_aux' (pair y (x mod y))
|
||||
|
||||
definition gcd_aux : ℕ × ℕ → ℕ := rec_measure 0 gcd_aux_measure gcd_aux_rec
|
||||
|
||||
theorem gcd_aux_decreasing (g : ℕ × ℕ → ℕ) (m : ℕ) (p : ℕ × ℕ) (H : m ≥ gcd_aux_measure p) :
|
||||
gcd_aux_rec p g = gcd_aux_rec p (restrict 0 gcd_aux_measure g m) :=
|
||||
let x [inline] := pr1 p, y [inline] := pr2 p in
|
||||
let p' [inline] := pair y (x mod y) in
|
||||
let lhs [inline] := gcd_aux_rec p g in
|
||||
let rhs [inline] := gcd_aux_rec p (restrict 0 gcd_aux_measure g m) in
|
||||
let x := pr1 p, y := pr2 p in
|
||||
let p' := pair y (x mod y) in
|
||||
let lhs := gcd_aux_rec p g in
|
||||
let rhs := gcd_aux_rec p (restrict 0 gcd_aux_measure g m) in
|
||||
show lhs = rhs, from
|
||||
by_cases (y = 0)
|
||||
(assume H1 : y = 0,
|
||||
|
|
@ -624,14 +624,14 @@ show lhs = rhs, from
|
|||
... = lhs : symm (if_neg H1 _ _)))
|
||||
|
||||
theorem gcd_aux_spec (p : ℕ × ℕ) : gcd_aux p =
|
||||
let x [inline] := pr1 p, y [inline] := pr2 p in
|
||||
let x := pr1 p, y := pr2 p in
|
||||
if y = 0 then x else gcd_aux (pair y (x mod y)) :=
|
||||
rec_measure_spec gcd_aux_rec gcd_aux_decreasing p
|
||||
|
||||
definition gcd (x y : ℕ) : ℕ := gcd_aux (pair x y)
|
||||
|
||||
theorem gcd_def (x y : ℕ) : gcd x y = if y = 0 then x else gcd y (x mod y) :=
|
||||
let x' [inline] := pr1 (pair x y), y' [inline] := pr2 (pair x y) in
|
||||
let x' := pr1 (pair x y), y' := pr2 (pair x y) in
|
||||
calc
|
||||
gcd x y = if y' = 0 then x' else gcd_aux (pair y' (x' mod y'))
|
||||
: gcd_aux_spec (pair x y)
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ abbreviation is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (re
|
|||
|
||||
theorem intro {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(H1 : ∀b, abs (rep b) = b) (H2 : ∀b, R (rep b) (rep b))
|
||||
(H3 : ∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s)) : is_quotient R abs rep :=
|
||||
(H3 : ∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s)) : is_quotient R abs rep :=
|
||||
and_intro H1 (and_intro H2 H3)
|
||||
|
||||
theorem and_absorb_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
|
||||
|
|
@ -41,16 +41,16 @@ intro
|
|||
(take b, H1 (rep b))
|
||||
(take r s,
|
||||
have H4 : R r s ↔ R s s ∧ abs r = abs s,
|
||||
from
|
||||
from
|
||||
subst (symm (and_absorb_left _ (H1 s))) (H3 r s),
|
||||
subst (symm (and_absorb_left _ (H1 r))) H4)
|
||||
|
||||
theorem abs_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) (b : B) : abs (rep b) = b :=
|
||||
(Q : is_quotient R abs rep) (b : B) : abs (rep b) = b :=
|
||||
and_elim_left Q b
|
||||
|
||||
theorem refl_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) (b : B) : R (rep b) (rep b) :=
|
||||
(Q : is_quotient R abs rep) (b : B) : R (rep b) (rep b) :=
|
||||
and_elim_left (and_elim_right Q) b
|
||||
|
||||
theorem R_iff {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
|
|
@ -124,7 +124,7 @@ theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
|||
{a : A} (Ha : R a a) : rec Q f (abs a) = f a :=
|
||||
have H2 [fact] : R a (rep (abs a)), from R_rep_abs Q Ha,
|
||||
calc
|
||||
rec Q f (abs a) = eq_rec_on _ (f (rep (abs a))) : rfl
|
||||
rec Q f (abs a) = eq_rec_on _ (f (rep (abs a))) : rfl
|
||||
... = eq_rec_on _ (eq_rec_on _ (f a)) : {symm (H _ _ H2)}
|
||||
... = eq_rec_on _ (f a) : eq_rec_on_compose _ _ _
|
||||
... = f a : eq_rec_on_id _ _
|
||||
|
|
@ -213,7 +213,7 @@ image_inhabited f (inhabited_mk a)
|
|||
definition fun_image {A B : Type} (f : A → B) (a : A) : image f :=
|
||||
tag (f a) (exists_intro a rfl)
|
||||
|
||||
theorem fun_image_def {A B : Type} (f : A → B) (a : A) :
|
||||
theorem fun_image_def {A B : Type} (f : A → B) (a : A) :
|
||||
fun_image f a = tag (f a) (exists_intro a rfl) := rfl
|
||||
|
||||
theorem elt_of_fun_image {A B : Type} (f : A → B) (a : A) : elt_of (fun_image f a) = f a :=
|
||||
|
|
@ -223,7 +223,7 @@ theorem image_elt_of {A B : Type} {f : A → B} (u : image f) : ∃a, f a = elt_
|
|||
has_property u
|
||||
|
||||
theorem fun_image_surj {A B : Type} {f : A → B} (u : image f) : ∃a, fun_image f a = u :=
|
||||
subtype_destruct u
|
||||
subtype_destruct u
|
||||
(take (b : B) (H : ∃a, f a = b),
|
||||
obtain a (H': f a = b), from H,
|
||||
(exists_intro a (tag_eq H')))
|
||||
|
|
@ -273,7 +273,7 @@ symm (H2 a (f a) (H1 a))
|
|||
theorem representative_map_refl_rep {A : Type} {R : A → A → Prop} {f : A → A}
|
||||
(H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b ↔ R a a ∧ R b b ∧ f a = f b) (a : A) :
|
||||
R (f a) (f a) :=
|
||||
subst (representative_map_idempotent H1 H2 a) (H1 (f a))
|
||||
subst (representative_map_idempotent H1 H2 a) (H1 (f a))
|
||||
|
||||
theorem representative_map_image_fix {A : Type} {R : A → A → Prop} {f : A → A}
|
||||
(H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') (b : image f) :
|
||||
|
|
@ -283,7 +283,7 @@ idempotent_image_fix (representative_map_idempotent H1 H2) b
|
|||
theorem representative_map_to_quotient {A : Type} {R : A → A → Prop} {f : A → A}
|
||||
(H1 : ∀a, R a (f a)) (H2 : ∀a a', R a a' ↔ R a a ∧ R a' a' ∧ f a = f a') :
|
||||
is_quotient _ (fun_image f) elt_of :=
|
||||
let abs [inline] := fun_image f in
|
||||
let abs := fun_image f in
|
||||
intro
|
||||
(take u : image f,
|
||||
obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u,
|
||||
|
|
@ -298,12 +298,12 @@ intro
|
|||
show R (elt_of u) (elt_of u), from
|
||||
obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u,
|
||||
subst Ha (@representative_map_refl_rep A R f H1 H2 a))
|
||||
(take a a',
|
||||
(take a a',
|
||||
subst (fun_image_eq f a a') (H2 a a'))
|
||||
|
||||
theorem representative_map_equiv_inj {A : Type} {R : A → A → Prop}
|
||||
(equiv : is_equivalence R) {f : A → A}
|
||||
(H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) {a b : A} (H3 : f a = f b) :
|
||||
(equiv : is_equivalence R) {f : A → A}
|
||||
(H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) {a b : A} (H3 : f a = f b) :
|
||||
R a b :=
|
||||
have symmR : symmetric R, from rel_symm R,
|
||||
have transR : transitive R, from rel_trans R,
|
||||
|
|
|
|||
|
|
@ -58,8 +58,8 @@ epsilon_spec (exists_intro a (refl a))
|
|||
|
||||
theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H : ∀x, ∃y, R x y) :
|
||||
∃f, ∀x, R x (f x) :=
|
||||
let f [inline] := λx, @epsilon _ (exists_imp_nonempty (H x)) (λy, R x y),
|
||||
H [inline] := take x, epsilon_spec (H x)
|
||||
let f := λx, @epsilon _ (exists_imp_nonempty (H x)) (λy, R x y),
|
||||
H := take x, epsilon_spec (H x)
|
||||
in exists_intro f H
|
||||
|
||||
theorem skolem {A : Type} {B : A → Type} {P : Πx, B x → Prop} :
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ by_contradiction (assume N : ¬∀x, P x,
|
|||
obtain (w : A) (Hw : ¬P w), from not_forall_exists N,
|
||||
-- The main "trick" is to define Q x as ¬P x.
|
||||
-- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬P r)
|
||||
let Q [inline] x := ¬P x in
|
||||
let Q x := ¬P x in
|
||||
have Qw : ∃w, Q w, from exists_intro w Hw,
|
||||
have Qwf : ∃min, Q min ∧ ∀b, R b min → ¬Q b, from Hwf Q Qw,
|
||||
obtain (r : A) (Hr : Q r ∧ ∀b, R b r → ¬Q b), from Qwf,
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ Author: Leonardo de Moura
|
|||
namespace lean {
|
||||
namespace notation {
|
||||
static name g_llevel_curly(".{"), g_rcurly("}"), g_in("in"), g_colon(":"), g_assign(":=");
|
||||
static name g_comma(","), g_fact("[fact]"), g_inline("[inline]"), g_from("from"), g_using("using");
|
||||
static name g_comma(","), g_fact("[fact]"), g_from("from"), g_using("using");
|
||||
static name g_then("then"), g_have("have"), g_by("by"), g_qed("qed"), g_end("end");
|
||||
static name g_take("take"), g_assume("assume"), g_show("show"), g_fun("fun");
|
||||
|
||||
|
|
@ -58,14 +58,11 @@ static expr mk_let(parser & p, name const & id, expr const & t, expr const & v,
|
|||
return p.mk_app(l, v, pos);
|
||||
}
|
||||
|
||||
static void parse_let_modifiers(parser & p, bool & is_fact, bool & is_opaque) {
|
||||
static void parse_let_modifiers(parser & p, bool & is_fact) {
|
||||
while (true) {
|
||||
if (p.curr_is_token(g_fact)) {
|
||||
is_fact = true;
|
||||
p.next();
|
||||
} else if (p.curr_is_token(g_inline)) {
|
||||
is_opaque = false;
|
||||
p.next();
|
||||
} else {
|
||||
break;
|
||||
}
|
||||
|
|
@ -79,18 +76,14 @@ static expr parse_let(parser & p, pos_info const & pos) {
|
|||
} else {
|
||||
auto pos = p.pos();
|
||||
name id = p.check_atomic_id_next("invalid let declaration, identifier expected");
|
||||
bool is_opaque = true;
|
||||
bool is_fact = false;
|
||||
expr type, value;
|
||||
parse_let_modifiers(p, is_fact, is_opaque);
|
||||
parse_let_modifiers(p, is_fact);
|
||||
if (p.curr_is_token(g_assign)) {
|
||||
p.next();
|
||||
if (is_opaque)
|
||||
type = p.save_pos(mk_expr_placeholder(), pos);
|
||||
type = p.save_pos(mk_expr_placeholder(), pos);
|
||||
value = p.parse_expr();
|
||||
} else if (p.curr_is_token(g_colon)) {
|
||||
if (!is_opaque)
|
||||
throw parser_error("invalid let 'inline' declaration, explicit type must not be provided", p.pos());
|
||||
p.next();
|
||||
type = p.parse_expr();
|
||||
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
|
||||
|
|
@ -100,28 +93,24 @@ static expr parse_let(parser & p, pos_info const & pos) {
|
|||
buffer<expr> ps;
|
||||
auto lenv = p.parse_binders(ps);
|
||||
if (p.curr_is_token(g_colon)) {
|
||||
if (!is_opaque)
|
||||
throw parser_error("invalid let 'inline' declaration, explicit type must not be provided", p.pos());
|
||||
p.next();
|
||||
type = p.parse_scoped_expr(ps, lenv);
|
||||
} else if (is_opaque) {
|
||||
} else {
|
||||
type = p.save_pos(mk_expr_placeholder(), pos);
|
||||
}
|
||||
p.check_token_next(g_assign, "invalid let declaration, ':=' expected");
|
||||
value = p.parse_scoped_expr(ps, lenv);
|
||||
if (is_opaque)
|
||||
type = Pi(ps, type, p);
|
||||
type = Pi(ps, type, p);
|
||||
value = Fun(ps, value, p);
|
||||
}
|
||||
if (is_opaque) {
|
||||
expr l = p.save_pos(mk_local(id, type), pos);
|
||||
p.add_local(l);
|
||||
expr body = abstract(parse_let_body(p, pos), l);
|
||||
return mk_let(p, id, type, value, body, pos, mk_contextual_info(is_fact));
|
||||
} else {
|
||||
p.add_local_expr(id, value);
|
||||
return parse_let_body(p, pos);
|
||||
}
|
||||
// expr l = p.save_pos(mk_local(id, type), pos);
|
||||
// p.add_local(l);
|
||||
// expr body = abstract(parse_let_body(p, pos), l);
|
||||
// return mk_let(p, id, type, value, body, pos, mk_contextual_info(is_fact));
|
||||
// } else {
|
||||
p.add_local_expr(id, value);
|
||||
return parse_let_body(p, pos);
|
||||
// }
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
-- Correct version
|
||||
check let bool [inline] := Type.{0},
|
||||
and [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c,
|
||||
check let bool := Type.{0},
|
||||
and (p q : bool) := ∀ c : bool, (p → q → c) → c,
|
||||
infixl `∧`:25 := and,
|
||||
and_intro (p q : bool) (H1 : p) (H2 : q) : p ∧ q
|
||||
:= λ (c : bool) (H : p → q → c), H H1 H2,
|
||||
|
|
@ -10,8 +10,10 @@ check let bool [inline] := Type.{0},
|
|||
:= H q (λ (H1 : p) (H2 : q), H2)
|
||||
in and_intro
|
||||
|
||||
check let bool [inline] := Type.{0},
|
||||
and [inline] (p q : bool) := ∀ c : bool, (p → q → c) → c,
|
||||
-- TODO(Leo): fix expected output as soon as elaborator starts checking let-expression type again
|
||||
|
||||
check let bool := Type.{0},
|
||||
and (p q : bool) := ∀ c : bool, (p → q → c) → c,
|
||||
infixl `∧`:25 := and,
|
||||
and_intro [fact] (p q : bool) (H1 : p) (H2 : q) : q ∧ p
|
||||
:= λ (c : bool) (H : p → q → c), H H1 H2,
|
||||
|
|
@ -20,4 +22,3 @@ check let bool [inline] := Type.{0},
|
|||
and_elim_right (p q : bool) (H : p ∧ q) : q
|
||||
:= H q (λ (H1 : p) (H2 : q), H2)
|
||||
in and_intro
|
||||
|
||||
|
|
|
|||
|
|
@ -1,38 +1,8 @@
|
|||
let and_intro : ∀ (p q : Prop),
|
||||
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q :=
|
||||
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
|
||||
H H1 H2,
|
||||
and_elim_left : ∀ (p q : Prop),
|
||||
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
|
||||
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
|
||||
H p (λ (H1 : p) (H2 : q), H1),
|
||||
and_elim_right : ∀ (p q : Prop),
|
||||
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
|
||||
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
|
||||
H q (λ (H1 : p) (H2 : q), H2)
|
||||
in and_intro :
|
||||
∀ (p q : Prop),
|
||||
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q
|
||||
let1.lean:16:10: error: type mismatch at application
|
||||
let and_intro : ∀ (p q : Prop),
|
||||
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p :=
|
||||
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
|
||||
H H1 H2,
|
||||
and_elim_left : ∀ (p q : Prop),
|
||||
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
|
||||
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
|
||||
H p (λ (H1 : p) (H2 : q), H1),
|
||||
and_elim_right : ∀ (p q : Prop),
|
||||
(λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → q :=
|
||||
λ (p q : Prop) (H : (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q),
|
||||
H q (λ (H1 : p) (H2 : q), H2)
|
||||
in and_intro
|
||||
term
|
||||
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
|
||||
H H1 H2
|
||||
has type
|
||||
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
|
||||
H H1 H2 :
|
||||
∀ (p q : Prop),
|
||||
p → q → (∀ (c : Prop), (p → q → c) → c)
|
||||
but is expected to have type
|
||||
λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
|
||||
H H1 H2 :
|
||||
∀ (p q : Prop),
|
||||
p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p
|
||||
p → q → (∀ (c : Prop), (p → q → c) → c)
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@ definition rec_on {P : ℕ → Type} (n : ℕ) (H1 : P 0) (H2 : ∀m, P m → P
|
|||
theorem succ_ne_zero (n : ℕ) : succ n ≠ 0
|
||||
:= assume H : succ n = 0,
|
||||
have H2 : true = false, from
|
||||
let f [inline] := (nat_rec false (fun a b, true)) in
|
||||
let f := (nat_rec false (fun a b, true)) in
|
||||
calc true = f (succ n) : _
|
||||
... = f 0 : {H}
|
||||
... = false : _,
|
||||
|
|
|
|||
Loading…
Reference in a new issue