From bae50f8ce67880cfaf367bc3a3c4dec4ecdf741e Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 22 Jun 2017 19:50:27 -0400 Subject: [PATCH] fix(tests/lean): fix tests --- tests/lean/rquote.lean | 1 - tests/lean/rquote.lean.expected.out | 4 ++-- tests/lean/run/occurs_check_bug1.lean | 12 +++++------- tests/lean/run/rw_eqn_lemmas.lean | 12 ++++++------ tests/lean/run/simp_single_pass.lean | 8 ++++---- tests/lean/run/unfold_lemmas.lean | 6 +++--- 6 files changed, 20 insertions(+), 23 deletions(-) diff --git a/tests/lean/rquote.lean b/tests/lean/rquote.lean index 813d20fcdc..c419edc653 100644 --- a/tests/lean/rquote.lean +++ b/tests/lean/rquote.lean @@ -1,5 +1,4 @@ -- -constant nat.gcd : nat → nat → nat namespace foo constant f : nat → nat constant g : nat → nat diff --git a/tests/lean/rquote.lean.expected.out b/tests/lean/rquote.lean.expected.out index 054041658f..a6c428db7a 100644 --- a/tests/lean/rquote.lean.expected.out +++ b/tests/lean/rquote.lean.expected.out @@ -1,7 +1,7 @@ -rquote.lean:14:7: error: invalid resolved quoted symbol, it is ambiguous, possible interpretations: boo.f foo.f (solution: use fully qualified names) +rquote.lean:13:7: error: invalid resolved quoted symbol, it is ambiguous, possible interpretations: boo.f foo.f (solution: use fully qualified names) name.mk_string "g" (name.mk_string "foo" name.anonymous) : name name.mk_string "add" (name.mk_string "has_add" name.anonymous) : name name.mk_string "gcd" (name.mk_string "nat" name.anonymous) : name name.mk_string "f" name.anonymous : name name.mk_string "f" (name.mk_string "foo" name.anonymous) : name -rquote.lean:32:9: error: invalid quoted symbol, failed to resolve it (solution: use ` to bypass name resolution) +rquote.lean:31:9: error: invalid quoted symbol, failed to resolve it (solution: use ` to bypass name resolution) diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean index 5479cea8eb..cd9cfc4584 100644 --- a/tests/lean/run/occurs_check_bug1.lean +++ b/tests/lean/run/occurs_check_bug1.lean @@ -1,17 +1,15 @@ open nat prod open decidable -constant modulo1 (x : ℕ) (y : ℕ) : ℕ -infixl `mod`:70 := modulo1 +constant modulo' (x : ℕ) (y : ℕ) : ℕ +infixl `mod`:70 := modulo' constant gcd_aux : ℕ × ℕ → ℕ -noncomputable definition gcd (x y : ℕ) : ℕ := gcd_aux (x, y) +noncomputable definition gcd' (x y : ℕ) : ℕ := gcd_aux (x, y) -theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.decidable_eq (snd (x, y)) 0) nat x (gcd y (x mod y)) := +theorem gcd_def (x y : ℕ) : gcd' x y = @ite (y = 0) (nat.decidable_eq (snd (x, y)) 0) nat x (gcd' y (x mod y)) := sorry -constant succ_ne_zero (a : nat) : succ a ≠ 0 - -theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) := +theorem gcd_succ (m n : ℕ) : gcd' m (succ n) = gcd' (succ n) (m mod succ n) := eq.trans (gcd_def _ _) (if_neg (nat.succ_ne_zero _)) diff --git a/tests/lean/run/rw_eqn_lemmas.lean b/tests/lean/run/rw_eqn_lemmas.lean index 624aa8e18d..44827f740d 100644 --- a/tests/lean/run/rw_eqn_lemmas.lean +++ b/tests/lean/run/rw_eqn_lemmas.lean @@ -1,21 +1,21 @@ open nat well_founded -def gcd : ℕ → ℕ → ℕ | y := λ x, +def gcd' : ℕ → ℕ → ℕ | y := λ x, if h : y = 0 then x else have x % y < y, by { apply mod_lt, cases y, contradiction, apply succ_pos }, - gcd (x % y) y + gcd' (x % y) y -lemma gcd_zero_right (x : nat) : gcd 0 x = x := +lemma gcd_zero_right (x : nat) : gcd' 0 x = x := begin - rw [gcd], + rw [gcd'], simp end -lemma ex (x : nat) (h : gcd 0 x = 0) : x + x = 0 := +lemma ex (x : nat) (h : gcd' 0 x = 0) : x + x = 0 := begin - rw [gcd] at h, + rw [gcd'] at h, simp at h, simp [h] end diff --git a/tests/lean/run/simp_single_pass.lean b/tests/lean/run/simp_single_pass.lean index 8226a1c2d1..7566ca893f 100644 --- a/tests/lean/run/simp_single_pass.lean +++ b/tests/lean/run/simp_single_pass.lean @@ -1,14 +1,14 @@ open nat well_founded -def gcd : ℕ → ℕ → ℕ | y := λ x, +def gcd' : ℕ → ℕ → ℕ | y := λ x, if h : y = 0 then x else have x % y < y, by { apply mod_lt, cases y, contradiction, apply succ_pos }, - gcd (x % y) y + gcd' (x % y) y -lemma gcd_zero_right (x : nat) : gcd 0 x = x := +lemma gcd'_zero_right (x : nat) : gcd' 0 x = x := begin - simp [gcd] {single_pass := tt}, + simp [gcd'] {single_pass := tt}, simp end diff --git a/tests/lean/run/unfold_lemmas.lean b/tests/lean/run/unfold_lemmas.lean index ea61ae1a27..0b304f79ea 100644 --- a/tests/lean/run/unfold_lemmas.lean +++ b/tests/lean/run/unfold_lemmas.lean @@ -1,10 +1,10 @@ open nat well_founded -def gcd : ℕ → ℕ → ℕ | y := λ x, +def gcd' : ℕ → ℕ → ℕ | y := λ x, if h : y = 0 then x else have x % y < y, by { apply mod_lt, cases y, contradiction, apply succ_pos }, - gcd (x % y) y + gcd' (x % y) y -@[simp] lemma gcd_zero_right (x : nat) : gcd 0 x = x := rfl +@[simp] lemma gcd_zero_right (x : nat) : gcd' 0 x = x := rfl