From e4060a5614fea07029de504c11cc5d5319352e03 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Mar 2015 12:06:51 -0800 Subject: [PATCH] feat(frontends/lean): do not force user to type the function name in the left-hand-side of recursive equations --- library/data/num.lean | 222 +++++++++++++++---------------- src/frontends/lean/decl_cmds.cpp | 51 +++++-- src/frontends/lean/tokens.cpp | 4 + src/frontends/lean/tokens.h | 1 + 4 files changed, 156 insertions(+), 122 deletions(-) diff --git a/library/data/num.lean b/library/data/num.lean index 30442d018..e7adab418 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -33,9 +33,9 @@ namespace pos_num rfl theorem pred_succ : ∀ (a : pos_num), pred (succ a) = a - | pred_succ one := rfl - | pred_succ (bit0 a) := by rewrite succ_bit0_eq_bit1 - | pred_succ (bit1 a) := + | one := rfl + | (bit0 a) := by rewrite succ_bit0_eq_bit1 + | (bit1 a) := calc pred (succ (bit1 a)) = cond (is_one (succ a)) one (bit1 (pred (succ a))) : rfl ... = cond ff one (bit1 (pred (succ a))) : succ_not_is_one @@ -88,19 +88,19 @@ namespace pos_num ... = bit0 n : iH) theorem decidable_eq [instance] : ∀ (a b : pos_num), decidable (a = b) - | decidable_eq one one := inl rfl - | decidable_eq one (bit0 b) := inr (λ H, pos_num.no_confusion H) - | decidable_eq one (bit1 b) := inr (λ H, pos_num.no_confusion H) - | decidable_eq (bit0 a) one := inr (λ H, pos_num.no_confusion H) - | decidable_eq (bit0 a) (bit0 b) := + | one one := inl rfl + | one (bit0 b) := inr (λ H, pos_num.no_confusion H) + | one (bit1 b) := inr (λ H, pos_num.no_confusion H) + | (bit0 a) one := inr (λ H, pos_num.no_confusion H) + | (bit0 a) (bit0 b) := match decidable_eq a b with | inl H₁ := inl (eq.rec_on H₁ rfl) | inr H₁ := inr (λ H, pos_num.no_confusion H (λ H₂, absurd H₂ H₁)) end - | decidable_eq (bit0 a) (bit1 b) := inr (λ H, pos_num.no_confusion H) - | decidable_eq (bit1 a) one := inr (λ H, pos_num.no_confusion H) - | decidable_eq (bit1 a) (bit0 b) := inr (λ H, pos_num.no_confusion H) - | decidable_eq (bit1 a) (bit1 b) := + | (bit0 a) (bit1 b) := inr (λ H, pos_num.no_confusion H) + | (bit1 a) one := inr (λ H, pos_num.no_confusion H) + | (bit1 a) (bit0 b) := inr (λ H, pos_num.no_confusion H) + | (bit1 a) (bit1 b) := match decidable_eq a b with | inl H₁ := inl (eq.rec_on H₁ rfl) | inr H₁ := inr (λ H, pos_num.no_confusion H (λ H₂, absurd H₂ H₁)) @@ -110,14 +110,14 @@ namespace pos_num local notation a `≮`:50 b:50 := (lt a b = ff) theorem lt_one_right_eq_ff : ∀ a : pos_num, a ≮ one - | lt_one_right_eq_ff one := rfl - | lt_one_right_eq_ff (bit0 a) := rfl - | lt_one_right_eq_ff (bit1 a) := rfl + | one := rfl + | (bit0 a) := rfl + | (bit1 a) := rfl theorem lt_one_succ_eq_tt : ∀ a : pos_num, one < succ a - | lt_one_succ_eq_tt one := rfl - | lt_one_succ_eq_tt (bit0 a) := rfl - | lt_one_succ_eq_tt (bit1 a) := rfl + | one := rfl + | (bit0 a) := rfl + | (bit1 a) := rfl theorem lt_of_lt_bit0_bit0 {a b : pos_num} (H : bit0 a < bit0 b) : a < b := H theorem lt_of_lt_bit0_bit1 {a b : pos_num} (H : bit1 a < bit0 b) : a < b := H @@ -137,197 +137,197 @@ namespace pos_num rfl theorem lt_irrefl : ∀ (a : pos_num), a ≮ a - | lt_irrefl one := rfl - | lt_irrefl (bit0 a) := + | one := rfl + | (bit0 a) := begin rewrite lt_bit0_bit0_eq_lt, apply lt_irrefl end - | lt_irrefl (bit1 a) := + | (bit1 a) := begin rewrite lt_bit1_bit1_eq_lt, apply lt_irrefl end theorem ne_of_lt_eq_tt : ∀ {a b : pos_num}, a < b → a = b → false - | @ne_of_lt_eq_tt one ⌞one⌟ H₁ (eq.refl one) := absurd H₁ ff_ne_tt - | @ne_of_lt_eq_tt (bit0 a) ⌞(bit0 a)⌟ H₁ (eq.refl (bit0 a)) := + | one ⌞one⌟ H₁ (eq.refl one) := absurd H₁ ff_ne_tt + | (bit0 a) ⌞(bit0 a)⌟ H₁ (eq.refl (bit0 a)) := begin rewrite lt_bit0_bit0_eq_lt at H₁, apply (ne_of_lt_eq_tt H₁ (eq.refl a)) end - | @ne_of_lt_eq_tt (bit1 a) ⌞(bit1 a)⌟ H₁ (eq.refl (bit1 a)) := + | (bit1 a) ⌞(bit1 a)⌟ H₁ (eq.refl (bit1 a)) := begin rewrite lt_bit1_bit1_eq_lt at H₁, apply (ne_of_lt_eq_tt H₁ (eq.refl a)) end theorem lt_base : ∀ a : pos_num, a < succ a - | lt_base one := rfl - | lt_base (bit0 a) := + | one := rfl + | (bit0 a) := begin rewrite [succ_bit0_eq_bit1, lt_bit0_bit1_eq_lt_succ], apply lt_base end - | lt_base (bit1 a) := + | (bit1 a) := begin rewrite [succ_bit1_eq_bit0_succ, lt_bit1_bit0_eq_lt], apply lt_base end theorem lt_step : ∀ {a b : pos_num}, a < b → a < succ b - | @lt_step one one H := rfl - | @lt_step one (bit0 b) H := rfl - | @lt_step one (bit1 b) H := rfl - | @lt_step (bit0 a) one H := absurd H ff_ne_tt - | @lt_step (bit0 a) (bit0 b) H := + | one one H := rfl + | one (bit0 b) H := rfl + | one (bit1 b) H := rfl + | (bit0 a) one H := absurd H ff_ne_tt + | (bit0 a) (bit0 b) H := begin rewrite [succ_bit0_eq_bit1, lt_bit0_bit1_eq_lt_succ, lt_bit0_bit0_eq_lt at H], apply (lt_step H) end - | @lt_step (bit0 a) (bit1 b) H := + | (bit0 a) (bit1 b) H := begin rewrite [succ_bit1_eq_bit0_succ, lt_bit0_bit0_eq_lt, lt_bit0_bit1_eq_lt_succ at H], exact H end - | @lt_step (bit1 a) one H := absurd H ff_ne_tt - | @lt_step (bit1 a) (bit0 b) H := + | (bit1 a) one H := absurd H ff_ne_tt + | (bit1 a) (bit0 b) H := begin rewrite [succ_bit0_eq_bit1, lt_bit1_bit1_eq_lt, lt_bit1_bit0_eq_lt at H], exact H end - | @lt_step (bit1 a) (bit1 b) H := + | (bit1 a) (bit1 b) H := begin rewrite [succ_bit1_eq_bit0_succ, lt_bit1_bit0_eq_lt, lt_bit1_bit1_eq_lt at H], apply (lt_step H) end theorem lt_of_lt_succ_succ : ∀ {a b : pos_num}, succ a < succ b → a < b - | @lt_of_lt_succ_succ one one H := absurd H ff_ne_tt - | @lt_of_lt_succ_succ one (bit0 b) H := rfl - | @lt_of_lt_succ_succ one (bit1 b) H := rfl - | @lt_of_lt_succ_succ (bit0 a) one H := + | one one H := absurd H ff_ne_tt + | one (bit0 b) H := rfl + | one (bit1 b) H := rfl + | (bit0 a) one H := begin rewrite [succ_bit0_eq_bit1 at H, succ_one_eq_bit0_one at H, lt_bit1_bit0_eq_lt at H], apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H) end - | @lt_of_lt_succ_succ (bit0 a) (bit0 b) H := by exact H - | @lt_of_lt_succ_succ (bit0 a) (bit1 b) H := by exact H - | @lt_of_lt_succ_succ (bit1 a) one H := + | (bit0 a) (bit0 b) H := by exact H + | (bit0 a) (bit1 b) H := by exact H + | (bit1 a) one H := begin rewrite [succ_bit1_eq_bit0_succ at H, succ_one_eq_bit0_one at H, lt_bit0_bit0_eq_lt at H], apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff (succ a)) H) end - | @lt_of_lt_succ_succ (bit1 a) (bit0 b) H := + | (bit1 a) (bit0 b) H := begin rewrite [succ_bit1_eq_bit0_succ at H, succ_bit0_eq_bit1 at H, lt_bit0_bit1_eq_lt_succ at H], rewrite lt_bit1_bit0_eq_lt, apply (lt_of_lt_succ_succ H) end - | @lt_of_lt_succ_succ (bit1 a) (bit1 b) H := + | (bit1 a) (bit1 b) H := begin rewrite [lt_bit1_bit1_eq_lt, *succ_bit1_eq_bit0_succ at H, lt_bit0_bit0_eq_lt at H], apply (lt_of_lt_succ_succ H) end theorem lt_succ_succ : ∀ {a b : pos_num}, a < b → succ a < succ b - | @lt_succ_succ one one H := absurd H ff_ne_tt - | @lt_succ_succ one (bit0 b) H := + | one one H := absurd H ff_ne_tt + | one (bit0 b) H := begin rewrite [succ_bit0_eq_bit1, succ_one_eq_bit0_one, lt_bit0_bit1_eq_lt_succ], apply lt_one_succ_eq_tt end - | @lt_succ_succ one (bit1 b) H := + | one (bit1 b) H := begin rewrite [succ_one_eq_bit0_one, succ_bit1_eq_bit0_succ, lt_bit0_bit0_eq_lt], apply lt_one_succ_eq_tt end - | @lt_succ_succ (bit0 a) one H := absurd H ff_ne_tt - | @lt_succ_succ (bit0 a) (bit0 b) H := by exact H - | @lt_succ_succ (bit0 a) (bit1 b) H := by exact H - | @lt_succ_succ (bit1 a) one H := absurd H ff_ne_tt - | @lt_succ_succ (bit1 a) (bit0 b) H := + | (bit0 a) one H := absurd H ff_ne_tt + | (bit0 a) (bit0 b) H := by exact H + | (bit0 a) (bit1 b) H := by exact H + | (bit1 a) one H := absurd H ff_ne_tt + | (bit1 a) (bit0 b) H := begin rewrite [succ_bit1_eq_bit0_succ, succ_bit0_eq_bit1, lt_bit0_bit1_eq_lt_succ, lt_bit1_bit0_eq_lt at H], apply (lt_succ_succ H) end - | @lt_succ_succ (bit1 a) (bit1 b) H := + | (bit1 a) (bit1 b) H := begin rewrite [lt_bit1_bit1_eq_lt at H, *succ_bit1_eq_bit0_succ, lt_bit0_bit0_eq_lt], apply (lt_succ_succ H) end theorem lt_of_lt_succ : ∀ {a b : pos_num}, succ a < b → a < b - | @lt_of_lt_succ one one H := absurd_of_eq_ff_of_eq_tt !lt_one_right_eq_ff H - | @lt_of_lt_succ one (bit0 b) H := rfl - | @lt_of_lt_succ one (bit1 b) H := rfl - | @lt_of_lt_succ (bit0 a) one H := absurd_of_eq_ff_of_eq_tt !lt_one_right_eq_ff H - | @lt_of_lt_succ (bit0 a) (bit0 b) H := by exact H - | @lt_of_lt_succ (bit0 a) (bit1 b) H := + | one one H := absurd_of_eq_ff_of_eq_tt !lt_one_right_eq_ff H + | one (bit0 b) H := rfl + | one (bit1 b) H := rfl + | (bit0 a) one H := absurd_of_eq_ff_of_eq_tt !lt_one_right_eq_ff H + | (bit0 a) (bit0 b) H := by exact H + | (bit0 a) (bit1 b) H := begin rewrite [succ_bit0_eq_bit1 at H, lt_bit1_bit1_eq_lt at H, lt_bit0_bit1_eq_lt_succ], apply (lt_step H) end - | @lt_of_lt_succ (bit1 a) one H := absurd_of_eq_ff_of_eq_tt !lt_one_right_eq_ff H - | @lt_of_lt_succ (bit1 a) (bit0 b) H := + | (bit1 a) one H := absurd_of_eq_ff_of_eq_tt !lt_one_right_eq_ff H + | (bit1 a) (bit0 b) H := begin rewrite [lt_bit1_bit0_eq_lt, succ_bit1_eq_bit0_succ at H, lt_bit0_bit0_eq_lt at H], apply (lt_of_lt_succ H) end - | @lt_of_lt_succ (bit1 a) (bit1 b) H := + | (bit1 a) (bit1 b) H := begin rewrite [succ_bit1_eq_bit0_succ at H, lt_bit0_bit1_eq_lt_succ at H, lt_bit1_bit1_eq_lt], apply (lt_of_lt_succ_succ H) end theorem lt_of_lt_succ_of_ne : ∀ {a b : pos_num}, a < succ b → a ≠ b → a < b - | @lt_of_lt_succ_of_ne one one H₁ H₂ := absurd rfl H₂ - | @lt_of_lt_succ_of_ne one (bit0 b) H₁ H₂ := rfl - | @lt_of_lt_succ_of_ne one (bit1 b) H₁ H₂ := rfl - | @lt_of_lt_succ_of_ne (bit0 a) one H₁ H₂ := + | one one H₁ H₂ := absurd rfl H₂ + | one (bit0 b) H₁ H₂ := rfl + | one (bit1 b) H₁ H₂ := rfl + | (bit0 a) one H₁ H₂ := begin rewrite [succ_one_eq_bit0_one at H₁, lt_bit0_bit0_eq_lt at H₁], apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁) end - | @lt_of_lt_succ_of_ne (bit0 a) (bit0 b) H₁ H₂ := + | (bit0 a) (bit0 b) H₁ H₂ := begin rewrite [lt_bit0_bit0_eq_lt, succ_bit0_eq_bit1 at H₁, lt_bit0_bit1_eq_lt_succ at H₁], apply (lt_of_lt_succ_of_ne H₁ (ne_of_bit0_ne_bit0 H₂)) end - | @lt_of_lt_succ_of_ne (bit0 a) (bit1 b) H₁ H₂ := + | (bit0 a) (bit1 b) H₁ H₂ := begin rewrite [succ_bit1_eq_bit0_succ at H₁, lt_bit0_bit0_eq_lt at H₁, lt_bit0_bit1_eq_lt_succ], exact H₁ end - | @lt_of_lt_succ_of_ne (bit1 a) one H₁ H₂ := + | (bit1 a) one H₁ H₂ := begin rewrite [succ_one_eq_bit0_one at H₁, lt_bit1_bit0_eq_lt at H₁], apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁) end - | @lt_of_lt_succ_of_ne (bit1 a) (bit0 b) H₁ H₂ := + | (bit1 a) (bit0 b) H₁ H₂ := begin rewrite [succ_bit0_eq_bit1 at H₁, lt_bit1_bit1_eq_lt at H₁, lt_bit1_bit0_eq_lt], exact H₁ end - | @lt_of_lt_succ_of_ne (bit1 a) (bit1 b) H₁ H₂ := + | (bit1 a) (bit1 b) H₁ H₂ := begin rewrite [succ_bit1_eq_bit0_succ at H₁, lt_bit1_bit0_eq_lt at H₁, lt_bit1_bit1_eq_lt], apply (lt_of_lt_succ_of_ne H₁ (ne_of_bit1_ne_bit1 H₂)) end theorem lt_trans : ∀ {a b c : pos_num}, a < b → b < c → a < c - | @lt_trans one b (bit0 c) H₁ H₂ := rfl - | @lt_trans one b (bit1 c) H₁ H₂ := rfl - | @lt_trans a (bit0 b) one H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ - | @lt_trans a (bit1 b) one H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ - | @lt_trans (bit0 a) (bit0 b) (bit0 c) H₁ H₂ := + | one b (bit0 c) H₁ H₂ := rfl + | one b (bit1 c) H₁ H₂ := rfl + | a (bit0 b) one H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ + | a (bit1 b) one H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ + | (bit0 a) (bit0 b) (bit0 c) H₁ H₂ := begin rewrite lt_bit0_bit0_eq_lt at *, apply (lt_trans H₁ H₂) end - | @lt_trans (bit0 a) (bit0 b) (bit1 c) H₁ H₂ := + | (bit0 a) (bit0 b) (bit1 c) H₁ H₂ := begin rewrite [lt_bit0_bit1_eq_lt_succ at *, lt_bit0_bit0_eq_lt at H₁], apply (lt_trans H₁ H₂) end - | @lt_trans (bit0 a) (bit1 b) (bit0 c) H₁ H₂ := + | (bit0 a) (bit1 b) (bit0 c) H₁ H₂ := begin rewrite [lt_bit0_bit1_eq_lt_succ at H₁, lt_bit1_bit0_eq_lt at H₂, lt_bit0_bit0_eq_lt], apply (@by_cases (a = b)), @@ -339,17 +339,17 @@ namespace pos_num apply (lt_trans (lt_of_lt_succ_of_ne H₁ H) H₂) end end - | @lt_trans (bit0 a) (bit1 b) (bit1 c) H₁ H₂ := + | (bit0 a) (bit1 b) (bit1 c) H₁ H₂ := begin rewrite [lt_bit0_bit1_eq_lt_succ at *, lt_bit1_bit1_eq_lt at H₂], apply (lt_trans H₁ (lt_succ_succ H₂)) end - | @lt_trans (bit1 a) (bit0 b) (bit0 c) H₁ H₂ := + | (bit1 a) (bit0 b) (bit0 c) H₁ H₂ := begin rewrite [lt_bit0_bit0_eq_lt at H₂, lt_bit1_bit0_eq_lt at *], apply (lt_trans H₁ H₂) end - | @lt_trans (bit1 a) (bit0 b) (bit1 c) H₁ H₂ := + | (bit1 a) (bit0 b) (bit1 c) H₁ H₂ := begin rewrite [lt_bit1_bit0_eq_lt at H₁, lt_bit0_bit1_eq_lt_succ at H₂, lt_bit1_bit1_eq_lt], apply (@by_cases (b = c)), @@ -361,28 +361,28 @@ namespace pos_num apply (lt_trans H₁ (lt_of_lt_succ_of_ne H₂ H)) end end - | @lt_trans (bit1 a) (bit1 b) (bit0 c) H₁ H₂ := + | (bit1 a) (bit1 b) (bit0 c) H₁ H₂ := begin rewrite [lt_bit1_bit1_eq_lt at H₁, lt_bit1_bit0_eq_lt at H₂, lt_bit1_bit0_eq_lt], apply (lt_trans H₁ H₂) end - | @lt_trans (bit1 a) (bit1 b) (bit1 c) H₁ H₂ := + | (bit1 a) (bit1 b) (bit1 c) H₁ H₂ := begin rewrite lt_bit1_bit1_eq_lt at *, apply (lt_trans H₁ H₂) end theorem lt_antisymm : ∀ {a b : pos_num}, a < b → b ≮ a - | @lt_antisymm one one H := rfl - | @lt_antisymm one (bit0 b) H := rfl - | @lt_antisymm one (bit1 b) H := rfl - | @lt_antisymm (bit0 a) one H := absurd H ff_ne_tt - | @lt_antisymm (bit0 a) (bit0 b) H := + | one one H := rfl + | one (bit0 b) H := rfl + | one (bit1 b) H := rfl + | (bit0 a) one H := absurd H ff_ne_tt + | (bit0 a) (bit0 b) H := begin rewrite lt_bit0_bit0_eq_lt at *, apply (lt_antisymm H) end - | @lt_antisymm (bit0 a) (bit1 b) H := + | (bit0 a) (bit1 b) H := begin rewrite lt_bit1_bit0_eq_lt, rewrite lt_bit0_bit1_eq_lt_succ at H, @@ -404,8 +404,8 @@ namespace pos_num apply (absurd_of_eq_ff_of_eq_tt H₁ H₄) end, end - | @lt_antisymm (bit1 a) one H := absurd H ff_ne_tt - | @lt_antisymm (bit1 a) (bit0 b) H := + | (bit1 a) one H := absurd H ff_ne_tt + | (bit1 a) (bit0 b) H := begin rewrite lt_bit0_bit1_eq_lt_succ, rewrite lt_bit1_bit0_eq_lt at H, @@ -426,7 +426,7 @@ namespace pos_num apply (absurd_of_eq_ff_of_eq_tt H₁ H₃) end, end - | @lt_antisymm (bit1 a) (bit1 b) H := + | (bit1 a) (bit1 b) H := begin rewrite lt_bit1_bit1_eq_lt at *, apply (lt_antisymm H) @@ -441,32 +441,32 @@ namespace pos_num rfl theorem not_lt_of_le : ∀ {a b : pos_num}, a ≤ b → b < a → false - | @not_lt_of_le one one H₁ H₂ := absurd H₂ ff_ne_tt - | @not_lt_of_le one (bit0 b) H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ - | @not_lt_of_le one (bit1 b) H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ - | @not_lt_of_le (bit0 a) one H₁ H₂ := + | one one H₁ H₂ := absurd H₂ ff_ne_tt + | one (bit0 b) H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ + | one (bit1 b) H₁ H₂ := absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₂ + | (bit0 a) one H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_one_eq_bit0_one at H₁, lt_bit0_bit0_eq_lt at H₁], apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁) end - | @not_lt_of_le (bit0 a) (bit0 b) H₁ H₂ := + | (bit0 a) (bit0 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_bit0_eq_bit1 at H₁, lt_bit0_bit1_eq_lt_succ at H₁], rewrite [lt_bit0_bit0_eq_lt at H₂], apply (not_lt_of_le H₁ H₂) end - | @not_lt_of_le (bit0 a) (bit1 b) H₁ H₂ := + | (bit0 a) (bit1 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_bit1_eq_bit0_succ at H₁, lt_bit0_bit0_eq_lt at H₁], rewrite [lt_bit1_bit0_eq_lt at H₂], apply (not_lt_of_le H₁ H₂) end - | @not_lt_of_le (bit1 a) one H₁ H₂ := + | (bit1 a) one H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_one_eq_bit0_one at H₁, lt_bit1_bit0_eq_lt at H₁], apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff _) H₁) end - | @not_lt_of_le (bit1 a) (bit0 b) H₁ H₂ := + | (bit1 a) (bit0 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_bit0_eq_bit1 at H₁, lt_bit1_bit1_eq_lt at H₁], rewrite lt_bit0_bit1_eq_lt_succ at H₂, @@ -482,7 +482,7 @@ namespace pos_num apply (not_lt_of_le H₃ H₄) end end - | @not_lt_of_le (bit1 a) (bit1 b) H₁ H₂ := + | (bit1 a) (bit1 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at H₁, succ_bit1_eq_bit0_succ at H₁, lt_bit1_bit0_eq_lt at H₁], rewrite [lt_bit1_bit1_eq_lt at H₂], @@ -490,34 +490,34 @@ namespace pos_num end theorem le_antisymm : ∀ {a b : pos_num}, a ≤ b → b ≤ a → a = b - | @le_antisymm one one H₁ H₂ := rfl - | @le_antisymm one (bit0 b) H₁ H₂ := + | one one H₁ H₂ := rfl + | one (bit0 b) H₁ H₂ := by apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff b) H₂) - | @le_antisymm one (bit1 b) H₁ H₂ := + | one (bit1 b) H₁ H₂ := by apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff b) H₂) - | @le_antisymm (bit0 a) one H₁ H₂ := + | (bit0 a) one H₁ H₂ := by apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H₁) - | @le_antisymm (bit0 a) (bit0 b) H₁ H₂ := + | (bit0 a) (bit0 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at *, succ_bit0_eq_bit1 at *, lt_bit0_bit1_eq_lt_succ at *], have H : a = b, from le_antisymm H₁ H₂, rewrite H end - | @le_antisymm (bit0 a) (bit1 b) H₁ H₂ := + | (bit0 a) (bit1 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at *, succ_bit1_eq_bit0_succ at H₁, succ_bit0_eq_bit1 at H₂], rewrite [lt_bit0_bit0_eq_lt at H₁, lt_bit1_bit1_eq_lt at H₂], apply (false.rec _ (not_lt_of_le H₁ H₂)) end - | @le_antisymm (bit1 a) one H₁ H₂ := + | (bit1 a) one H₁ H₂ := by apply (absurd_of_eq_ff_of_eq_tt (lt_one_right_eq_ff a) H₁) - | @le_antisymm (bit1 a) (bit0 b) H₁ H₂ := + | (bit1 a) (bit0 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at *, succ_bit0_eq_bit1 at H₁, succ_bit1_eq_bit0_succ at H₂], rewrite [lt_bit1_bit1_eq_lt at H₁, lt_bit0_bit0_eq_lt at H₂], apply (false.rec _ (not_lt_of_le H₂ H₁)) end - | @le_antisymm (bit1 a) (bit1 b) H₁ H₂ := + | (bit1 a) (bit1 b) H₁ H₂ := begin rewrite [le_eq_lt_succ at *, succ_bit1_eq_bit0_succ at *, lt_bit1_bit0_eq_lt at *], have H : a = b, from le_antisymm H₁ H₂, diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index d382935b6..5a4dc3b63 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -550,7 +550,7 @@ static expr merge_equation_lhs_vars(expr const & lhs, buffer & locals) { }); } -static void throw_invalid_equation_lhs(name const & n, pos_info const & p) { +[[ noreturn ]] static void throw_invalid_equation_lhs(name const & n, pos_info const & p) { throw parser_error(sstream() << "invalid recursive equation, head symbol '" << n << "' in the left-hand-side does not correspond to function(s) being defined", p); } @@ -565,6 +565,21 @@ static void check_eqn_prefix(parser & p) { p.next(); } +static optional is_equation_fn(buffer const & fns, name const & fn_name) { + for (expr const & fn : fns) { + if (local_pp_name(fn) == fn_name) + return some_expr(fn); + } + return none_expr(); +} + + +static expr get_equation_fn(buffer const & fns, name const & fn_name, pos_info const & lhs_pos) { + if (auto it = is_equation_fn(fns, fn_name)) + return *it; + throw_invalid_equation_lhs(fn_name, lhs_pos); +} + expr parse_equations(parser & p, name const & n, expr const & type, buffer & auxs, optional const & lenv, buffer const & ps, pos_info const & def_pos) { @@ -597,17 +612,31 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer buffer locals; { parser::undef_id_to_local_scope scope2(p); + buffer lhs_args; auto lhs_pos = p.pos(); - lhs = p.parse_expr(); - expr lhs_fn = get_app_fn(lhs); - if (is_explicit(lhs_fn)) - lhs_fn = get_explicit_arg(lhs_fn); - if (is_constant(lhs_fn)) - throw_invalid_equation_lhs(const_name(lhs_fn), lhs_pos); - if (is_local(lhs_fn) && std::all_of(fns.begin(), fns.end(), [&](expr const & fn) { return fn != lhs_fn; })) - throw_invalid_equation_lhs(local_pp_name(lhs_fn), lhs_pos); - if (!is_local(lhs_fn)) - throw parser_error("invalid recursive equation, head symbol in left-hand-side is not a constant", lhs_pos); + if (p.curr_is_token(get_explicit_tk())) { + p.next(); + name fn_name = p.check_id_next("invalid recursive equation, identifier expected"); + lhs_args.push_back(p.save_pos(mk_explicit(get_equation_fn(fns, fn_name, lhs_pos)), lhs_pos)); + } else { + expr first = p.parse_expr(get_max_prec()); + expr fn = first; + if (is_explicit(fn)) + fn = get_explicit_arg(fn); + if (is_local(fn) && is_equation_fn(fns, local_pp_name(fn))) { + lhs_args.push_back(first); + } else if (fns.size() == 1) { + lhs_args.push_back(p.save_pos(mk_explicit(fns[0]), lhs_pos)); + lhs_args.push_back(first); + } else { + throw parser_error("invalid recursive equation, head symbol in left-hand-side is not a constant", + lhs_pos); + } + } + while (!p.curr_is_token(get_assign_tk())) + lhs_args.push_back(p.parse_expr(get_max_prec())); + lhs = p.save_pos(mk_app(lhs_args.size(), lhs_args.data()), lhs_pos); + unsigned num_undef_ids = p.get_num_undef_ids(); for (unsigned i = prev_num_undef_ids; i < num_undef_ids; i++) { locals.push_back(p.get_undef_id(i)); diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 544e99fe5..e15e58a10 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -40,6 +40,7 @@ static name * g_slash = nullptr; static name * g_star = nullptr; static name * g_plus = nullptr; static name * g_turnstile = nullptr; +static name * g_explicit = nullptr; static name * g_max = nullptr; static name * g_imax = nullptr; static name * g_cup = nullptr; @@ -161,6 +162,7 @@ void initialize_tokens() { g_plus = new name("+"); g_star = new name("*"); g_turnstile = new name("⊢"); + g_explicit = new name("@"); g_max = new name("max"); g_imax = new name("imax"); g_cup = new name("\u2294"); @@ -346,6 +348,7 @@ void finalize_tokens() { delete g_plus; delete g_star; delete g_turnstile; + delete g_explicit; delete g_comma; delete g_bar; delete g_langle; @@ -405,6 +408,7 @@ name const & get_slash_tk() { return *g_slash; } name const & get_star_tk() { return *g_star; } name const & get_plus_tk() { return *g_plus; } name const & get_turnstile_tk() { return *g_turnstile; } +name const & get_explicit_tk() { return *g_explicit; } name const & get_max_tk() { return *g_max; } name const & get_imax_tk() { return *g_imax; } name const & get_cup_tk() { return *g_cup; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 66d4a0d6a..02a2c1876 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -42,6 +42,7 @@ name const & get_star_tk(); name const & get_plus_tk(); name const & get_greater_tk(); name const & get_turnstile_tk(); +name const & get_explicit_tk(); name const & get_max_tk(); name const & get_imax_tk(); name const & get_cup_tk();