lean2/tests/lean/run/occurs_check_bug1.lean

import logic data.nat data.prod

open nat prod
open decidable

constant modulo1 (x : ℕ) (y : ℕ) : ℕ
infixl `mod`:70 := modulo1

constant gcd_aux : ℕ × ℕ → ℕ

definition gcd (x y : ℕ) : ℕ := gcd_aux (pair x y)

theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.has_decidable_eq (pr2 (pair x y)) 0) nat x (gcd y (x mod y)) :=
sorry

theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=
eq.trans (gcd_def _ _) (if_neg !succ_ne_zero)
-												fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-21 17:56:18 -07:00
+								import logic data.nat data.prod
-												feat(frontends/lean): rename 'using' command to 'open'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-09-03 16:00:38 -07:00
+								open nat prod
 								open decidable
-												fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-21 17:56:18 -07:00
-												fix(tests/lean/run): adjust some tests to changes in the standard library

											
										
										
											2015-10-13 15:39:03 -07:00
+								constant modulo1 (x : ℕ) (y : ℕ) : ℕ
-												refactor(library/*): use type classes for div and mod

											
										
										
											2015-10-29 15:36:26 -04:00
+								infixl `mod`:70 := modulo1
-												fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-21 17:56:18 -07:00
-												refactor(frontends/lean): constant/axiom are top-level commands, parameter/variable/hypothesis/conjecture are section/context-level commands

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-10-02 16:20:52 -07:00
+								constant gcd_aux : ℕ × ℕ → ℕ
-												fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-21 17:56:18 -07:00
 								definition gcd (x y : ℕ) : ℕ := gcd_aux (pair x y)
-												feat(library): add 'decidable_eq' class

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-09-07 22:22:04 -07:00
+								theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.has_decidable_eq (pr2 (pair x y)) 0) nat x (gcd y (x mod y)) :=
-												fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

											
										
										
											2014-08-21 17:56:18 -07:00
+								sorry
 								theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=
-												feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type.

											
										
										
											2014-10-01 18:50:17 -07:00
+								eq.trans (gcd_def _ _) (if_neg !succ_ne_zero)