michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): do not force user to type the function name in the left-hand-side of recursive equations

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-05 12:06:51 -08:00
parent 87c236613a
commit e4060a5614
4 changed files with 156 additions and 122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

222
library/data/num.lean
View file

@ -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₂,

51
src/frontends/lean/decl_cmds.cpp
View file

@ -550,7 +550,7 @@ static expr merge_equation_lhs_vars(expr const & lhs, buffer<expr> & 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<expr> is_equation_fn(buffer<expr> 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<expr> 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<name> & auxs,
optional<local_environment> const & lenv, buffer<expr> const & ps,
pos_info const & def_pos) {
@ -597,17 +612,31 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
buffer<expr> locals;
{
parser::undef_id_to_local_scope scope2(p);
buffer<expr> 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));

4
src/frontends/lean/tokens.cpp
View file

@ -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; }

1
src/frontends/lean/tokens.h
View file

@ -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();