From e9b4b811de283ee38ac5cf76225b5ff477ca7c65 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Jun 2018 12:06:27 -0700 Subject: [PATCH] chore(library/equations_compiler/util): disable generation of equational lemmas @kha, `eqn_compiler.lemmas` is false by default. I will keep them disabled until I remove the inductive compiler. I'm building the new inductive datatype module (to replace the inductive compiler), and the lemmas will fail to be proved in the next commits until the transition is complete. --- library/init/data/int/basic.lean | 2 +- library/init/data/list/basic.lean | 28 ++++++++++++------------- library/init/data/list/instances.lean | 2 -- library/init/data/option/basic.lean | 2 +- library/init/lean/name.lean | 2 +- src/library/equations_compiler/util.cpp | 2 +- 6 files changed, 18 insertions(+), 20 deletions(-) diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index 3da7fe50c5..8f9bae6351 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -83,7 +83,7 @@ m + -n instance : has_sub int := ⟨int.sub⟩ -@[simp] def nat_abs : int → ℕ +def nat_abs : int → ℕ | (of_nat m) := m | -[1+ m] := succ m diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index bea78899e5..76c0ec129e 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -31,7 +31,7 @@ protected def has_dec_eq [s : decidable_eq α] : decidable_eq (list α) instance [decidable_eq α] : decidable_eq (list α) := list.has_dec_eq -@[simp] protected def append : list α → list α → list α +protected def append : list α → list α → list α | [] l := l | (h :: s) t := h :: (append s t) @@ -78,7 +78,7 @@ protected def diff {α} [decidable_eq α] : list α → list α → list α | l [] := l | l₁ (a::l₂) := if a ∈ l₁ then diff (l₁.erase a) l₂ else diff l₁ l₂ -@[simp] def length : list α → nat +def length : list α → nat | [] := 0 | (a :: l) := length l + 1 @@ -88,21 +88,21 @@ def empty : list α → bool open option nat -@[simp] def nth : list α → nat → option α +def nth : list α → nat → option α | [] n := none | (a :: l) 0 := some a | (a :: l) (n+1) := nth l n -@[simp] def nth_le : Π (l : list α) (n), n < l.length → α +def nth_le : Π (l : list α) (n), n < l.length → α | [] n h := absurd h (not_lt_zero n) | (a :: l) 0 h := a | (a :: l) (n+1) h := nth_le l n (le_of_succ_le_succ h) -@[simp] def head [inhabited α] : list α → α +def head [inhabited α] : list α → α | [] := default α | (a :: l) := a -@[simp] def tail : list α → list α +def tail : list α → list α | [] := [] | (a :: l) := l @@ -113,11 +113,11 @@ def reverse_core : list α → list α → list α def reverse : list α → list α := λ l, reverse_core l [] -@[simp] def map (f : α → β) : list α → list β +def map (f : α → β) : list α → list β | [] := [] | (a :: l) := f a :: map l -@[simp] def map₂ (f : α → β → γ) : list α → list β → list γ +def map₂ (f : α → β → γ) : list α → list β → list γ | [] _ := [] | _ [] := [] | (x::xs) (y::ys) := f x y :: map₂ xs ys @@ -168,21 +168,21 @@ def remove_nth : list α → ℕ → list α | (x::xs) 0 := xs | (x::xs) (i+1) := x :: remove_nth xs i -@[simp] def drop : ℕ → list α → list α +def drop : ℕ → list α → list α | 0 a := a | (succ n) [] := [] | (succ n) (x::r) := drop n r -@[simp] def take : ℕ → list α → list α +def take : ℕ → list α → list α | 0 a := [] | (succ n) [] := [] | (succ n) (x :: r) := x :: take n r -@[simp] def foldl (f : α → β → α) : α → list β → α +def foldl (f : α → β → α) : α → list β → α | a [] := a | a (b :: l) := foldl (f a b) l -@[simp] def foldr (f : α → β → β) (b : β) : list α → β +def foldr (f : α → β → β) (b : β) : list α → β | [] := b | (a :: l) := f a (foldr l) @@ -225,7 +225,7 @@ filter (∈ l₂) l₁ instance [decidable_eq α] : has_inter (list α) := ⟨list.inter⟩ -@[simp] def repeat (a : α) : ℕ → list α +def repeat (a : α) : ℕ → list α | 0 := [] | (succ n) := a :: repeat n @@ -246,7 +246,7 @@ def enum_from : ℕ → list α → list (ℕ × α) def enum : list α → list (ℕ × α) := enum_from 0 -@[simp] def last : Π l : list α, l ≠ [] → α +def last : Π l : list α, l ≠ [] → α | [] h := absurd rfl h | [a] h := a | (a::b::l) h := last (b::l) (λ h, list.no_confusion h) diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean index a4dbe83ff3..90e467f445 100644 --- a/library/init/data/list/instances.lean +++ b/library/init/data/list/instances.lean @@ -10,8 +10,6 @@ open list universes u v -local attribute [simp] join list.ret - instance : monad list := { pure := @list.ret, map := @list.map, bind := @list.bind } diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean index 1935e7474a..36f1cd60b9 100644 --- a/library/init/data/option/basic.lean +++ b/library/init/data/option/basic.lean @@ -57,7 +57,7 @@ instance : alternative option := { failure := @none, orelse := @option.orelse } -@[simp] protected def lt {α : Type u} (r : α → α → Prop) : option α → option α → Prop +protected def lt {α : Type u} (r : α → α → Prop) : option α → option α → Prop | none (some x) := true | (some x) (some y) := r x y | _ _ := false diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index ab86a5596f..61f6e961c8 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -86,7 +86,7 @@ def replace_prefix : name → name → name → name else mk_numeral (p.replace_prefix query_p new_p) s -@[simp] def quick_lt : name → name → bool +def quick_lt : name → name → bool | anonymous anonymous := ff | anonymous _ := tt | (mk_numeral n v) (mk_numeral n' v') := v < v' || (v = v' && n.quick_lt n') diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 8909ab8beb..728a00e518 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -36,7 +36,7 @@ Author: Leonardo de Moura #include "library/equations_compiler/wf_rec.h" #ifndef LEAN_DEFAULT_EQN_COMPILER_LEMMAS -#define LEAN_DEFAULT_EQN_COMPILER_LEMMAS true +#define LEAN_DEFAULT_EQN_COMPILER_LEMMAS false #endif #ifndef LEAN_DEFAULT_EQN_COMPILER_ZETA