From 5cef84709f3389261a3b301bb84a7fd3262196ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 May 2017 08:52:19 -0700 Subject: [PATCH] refactor(library): avoid auxiliary definitions such as add/mul/le/etc See Section "Other goodies" at https://github.com/leanprover/lean/wiki/Refactoring-structures This commit also improves the support for projections in the unifier/matcher. Now, we consider the extra case-split for projections. Given a projection `proj`, and the constraint `proj s =?= proj t`, we need to try first `s =?= t` and if it fails, then try to reduce. This is needed in the standard library because we now have constraints such as: ``` @has_le.le ?A ?s ?a ?b =?= @has_le.le nat nat.has_add x y ``` If we reduce the right hand side, we get the unsolvable constraint ``` @has_le.le ?A ?s ?a ?b =?= nat.le x y ``` Before this change, the constraint was `@le ?A ?s ?a ?b =?= @le nat nat.has_add x y`, and we already perform a case-split in this case. Moreover, projections were eagerly reduced whenever possible. The extra case-split generates a performance problem in several tests. For example `fib 8 = 34` was timing out. I worked around this issue by performing the case-split only when the constraint contains meta-variables. There are also minor issues. Example. `<` is notation for `has_lt.lt`, but `>` is for `gt`. --- library/data/set/basic.lean | 10 +- library/init/algebra/group.lean | 12 +- library/init/algebra/norm_num.lean | 22 ++-- library/init/algebra/order.lean | 1 + library/init/core.lean | 108 +++++++--------- library/init/data/int/basic.lean | 6 +- library/init/data/list/basic.lean | 4 +- library/init/data/list/lemmas.lean | 6 +- library/init/data/nat/div.lean | 4 +- library/init/data/nat/lemmas.lean | 11 +- library/init/data/to_string.lean | 2 +- library/init/meta/expr.lean | 8 +- library/init/meta/smt/rsimp.lean | 10 +- library/init/meta/transfer.lean | 2 +- library/init/wf.lean | 2 +- src/frontends/lean/brackets.cpp | 4 +- src/frontends/lean/elaborator.cpp | 13 +- src/frontends/lean/parser.cpp | 2 +- src/frontends/lean/pp.cpp | 6 +- src/frontends/lean/structure_cmd.cpp | 1 - src/frontends/lean/tactic_notation.cpp | 2 +- src/frontends/smt2/elaborator.cpp | 18 +-- src/library/app_builder.cpp | 8 +- src/library/arith_instance.cpp | 30 ++--- src/library/constants.cpp | 116 ++++++++---------- src/library/constants.h | 29 ++--- src/library/constants.txt | 29 ++--- src/library/inductive_compiler/nested.cpp | 2 +- src/library/norm_num.cpp | 20 +-- src/library/num.cpp | 16 +-- src/library/tactic/smt/ematch.cpp | 3 - src/library/tactic/smt/smt_state.cpp | 3 +- src/library/type_context.cpp | 68 ++++++---- src/library/type_context.h | 2 +- src/library/unification_hint.h | 6 +- src/library/util.cpp | 6 +- tests/lean/coe4.lean.expected.out | 3 +- .../lean/concrete_instance.lean.expected.out | 8 +- tests/lean/defeq_simp1.lean | 4 +- tests/lean/defeq_simp1.lean.expected.out | 7 +- tests/lean/defeq_simp3.lean | 2 +- tests/lean/defeq_simp3.lean.expected.out | 2 +- tests/lean/defeq_simp4.lean | 2 +- tests/lean/defeq_simp4.lean.expected.out | 4 +- tests/lean/defeq_simp5.lean | 4 +- tests/lean/defeq_simp5.lean.expected.out | 4 +- tests/lean/elab1.lean | 6 +- tests/lean/elab1.lean.expected.out | 2 +- tests/lean/elab2.lean.expected.out | 4 +- tests/lean/elab7.lean.expected.out | 11 +- tests/lean/elab8.lean.expected.out | 16 +-- tests/lean/elab9.lean.expected.out | 12 +- tests/lean/eta_tac.lean | 10 +- tests/lean/eta_tac.lean.expected.out | 10 +- tests/lean/generalize1.lean | 2 +- tests/lean/hinst_lemmas1.lean.expected.out | 4 +- tests/lean/interactive/info.lean.expected.out | 2 +- tests/lean/key_eqv1.lean | 4 +- tests/lean/key_eqv1.lean.expected.out | 4 +- tests/lean/macro_args.lean | 2 +- tests/lean/macro_args.lean.expected.out | 2 +- tests/lean/notation7.lean.expected.out | 2 +- tests/lean/pp_all.lean.expected.out | 4 +- tests/lean/pp_all2.lean.expected.out | 2 +- tests/lean/pp_zero_bug.lean | 4 +- tests/lean/pp_zero_bug.lean.expected.out | 4 +- tests/lean/qexpr1.lean.expected.out | 4 +- tests/lean/qexpr2.lean.expected.out | 4 +- tests/lean/rquote.lean | 2 +- tests/lean/rquote.lean.expected.out | 2 +- tests/lean/run/1468.lean | 17 --- tests/lean/run/app_builder_tac1.lean | 6 +- tests/lean/run/at_at_bug.lean | 3 +- tests/lean/run/auto_param_in_structures.lean | 8 +- tests/lean/run/check_constants.lean | 29 ++--- tests/lean/run/cpdt3.lean | 8 +- tests/lean/run/decl_olean.lean | 1 - tests/lean/run/dep_coe_to_fn3.lean | 8 +- tests/lean/run/destruct.lean | 2 +- tests/lean/run/dunfold3.lean | 2 +- tests/lean/run/list_notation.lean | 2 +- tests/lean/run/listex.lean | 12 +- tests/lean/run/listex2.lean | 6 +- tests/lean/run/quote1.lean | 2 +- tests/lean/run/shadow1.lean | 4 +- tests/lean/run/super_examples.lean | 6 +- tests/lean/run/type_equations.lean | 2 +- tests/lean/run/u_eq_max_u_v.lean | 4 +- tests/lean/run/unification_hints.lean | 2 +- tests/lean/run/wfrec1.lean | 2 +- tests/lean/set_opt_tac.lean.expected.out | 2 +- tests/lean/type_class_bug.lean.expected.out | 13 +- .../lean/unification_hints1.lean.expected.out | 4 +- 93 files changed, 432 insertions(+), 464 deletions(-) delete mode 100644 tests/lean/run/1468.lean diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index d27b4c3271..fcdb5ebc40 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -51,10 +51,10 @@ ext (take x, or.comm) lemma union_assoc (a b c : set α) : (a ∪ b) ∪ c = a ∪ (b ∪ c) := ext (take x, or.assoc) -instance union_is_assoc : is_associative (set α) union := +instance union_is_assoc : is_associative (set α) (∪) := ⟨union_assoc⟩ -instance union_is_comm : is_commutative (set α) union := +instance union_is_comm : is_commutative (set α) (∪) := ⟨union_comm⟩ lemma union_self (a : set α) : a ∪ a = a := @@ -72,11 +72,11 @@ ext (take x, and.comm) lemma inter_assoc (a b c : set α) : (a ∩ b) ∩ c = a ∩ (b ∩ c) := ext (take x, and.assoc) -instance inter_is_assoc : is_associative (set α) inter := +instance inter_is_assoc : is_associative (set α) (∩) := ⟨inter_assoc⟩ -instance inter_is_comm : is_commutative (set α) union := -⟨union_comm⟩ +instance inter_is_comm : is_commutative (set α) (∩) := +⟨inter_comm⟩ lemma inter_self (a : set α) : a ∩ a = a := ext (take x, and_self _) diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean index 1222ab6b24..112bc77b7e 100644 --- a/library/init/algebra/group.lean +++ b/library/init/algebra/group.lean @@ -40,17 +40,17 @@ class comm_group (α : Type u) extends group α, comm_monoid α @[simp] lemma mul_assoc [semigroup α] : ∀ a b c : α, a * b * c = a * (b * c) := semigroup.mul_assoc -instance semigroup_to_is_associative [semigroup α] : is_associative α mul := +instance semigroup_to_is_associative [semigroup α] : is_associative α (*) := ⟨mul_assoc⟩ @[simp] lemma mul_comm [comm_semigroup α] : ∀ a b : α, a * b = b * a := comm_semigroup.mul_comm -instance comm_semigroup_to_is_commutative [comm_semigroup α] : is_commutative α mul := +instance comm_semigroup_to_is_commutative [comm_semigroup α] : is_commutative α (*) := ⟨mul_comm⟩ @[simp] lemma mul_left_comm [comm_semigroup α] : ∀ a b c : α, a * (b * c) = b * (a * c) := -left_comm mul mul_comm mul_assoc +left_comm has_mul.mul mul_comm mul_assoc lemma mul_left_cancel [left_cancel_semigroup α] {a b c : α} : a * b = a * c → b = c := left_cancel_semigroup.mul_left_cancel a b c @@ -210,7 +210,7 @@ copy_decl_using dict src tgt meta def multiplicative_to_additive_pairs : list (name × name) := [/- map operations -/ - (`mul, `add), (`one, `zero), (`inv, `neg), + (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg), (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg), /- map constructors -/ (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk), @@ -298,10 +298,10 @@ skip run_cmd transport_multiplicative_to_additive -instance add_semigroup_to_is_eq_associative [add_semigroup α] : is_associative α add := +instance add_semigroup_to_is_eq_associative [add_semigroup α] : is_associative α (+) := ⟨add_assoc⟩ -instance add_comm_semigroup_to_is_eq_commutative [add_comm_semigroup α] : is_commutative α add := +instance add_comm_semigroup_to_is_eq_commutative [add_comm_semigroup α] : is_commutative α (+) := ⟨add_comm⟩ def neg_add_self := @add_left_neg diff --git a/library/init/algebra/norm_num.lean b/library/init/algebra/norm_num.lean index 0ea8de1d7f..795ab73a74 100644 --- a/library/init/algebra/norm_num.lean +++ b/library/init/algebra/norm_num.lean @@ -178,30 +178,30 @@ lemma bit1_add_bit1_helper [add_comm_semigroup α] [has_one α] (a b t s : α) (h : (a + b) = t) (h2 : add1 t = s) : bit1 a + bit1 b = bit0 s := begin rw -h at h2, rw -h2, usimp end -lemma bin_add_zero [add_monoid α] (a : α) : a + zero = a := +lemma bin_add_zero [add_monoid α] (a : α) : a + 0 = a := by simp -lemma bin_zero_add [add_monoid α] (a : α) : zero + a = a := +lemma bin_zero_add [add_monoid α] (a : α) : 0 + a = a := by simp -lemma one_add_bit0 [add_comm_semigroup α] [has_one α] (a : α) : one + bit0 a = bit1 a := +lemma one_add_bit0 [add_comm_semigroup α] [has_one α] (a : α) : 1 + bit0 a = bit1 a := begin unfold bit0 bit1, simp end -lemma bit0_add_one [has_add α] [has_one α] (a : α) : bit0 a + one = bit1 a := +lemma bit0_add_one [has_add α] [has_one α] (a : α) : bit0 a + 1 = bit1 a := rfl -lemma bit1_add_one [has_add α] [has_one α] (a : α) : bit1 a + one = add1 (bit1 a) := +lemma bit1_add_one [has_add α] [has_one α] (a : α) : bit1 a + 1 = add1 (bit1 a) := rfl lemma bit1_add_one_helper [has_add α] [has_one α] (a t : α) (h : add1 (bit1 a) = t) : - bit1 a + one = t := + bit1 a + 1 = t := by rw -h -lemma one_add_bit1 [add_comm_semigroup α] [has_one α] (a : α) : one + bit1 a = add1 (bit1 a) := +lemma one_add_bit1 [add_comm_semigroup α] [has_one α] (a : α) : 1 + bit1 a = add1 (bit1 a) := begin unfold bit0 bit1 add1, simp end lemma one_add_bit1_helper [add_comm_semigroup α] [has_one α] (a t : α) - (h : add1 (bit1 a) = t) : one + bit1 a = t := + (h : add1 (bit1 a) = t) : 1 + bit1 a = t := begin rw -h, usimp end lemma add1_bit0 [has_add α] [has_one α] (a : α) : add1 (bit0 a) = bit1 a := @@ -215,13 +215,13 @@ lemma add1_bit1_helper [add_comm_semigroup α] [has_one α] (a t : α) (h : add1 add1 (bit1 a) = bit0 t := begin rw -h, usimp end -lemma add1_one [has_add α] [has_one α] : add1 (one : α) = bit0 one := +lemma add1_one [has_add α] [has_one α] : add1 (1 : α) = bit0 1 := rfl -lemma add1_zero [add_monoid α] [has_one α] : add1 (zero : α) = one := +lemma add1_zero [add_monoid α] [has_one α] : add1 (0 : α) = 1 := by usimp -lemma one_add_one [has_add α] [has_one α] : (one : α) + one = bit0 one := +lemma one_add_one [has_add α] [has_one α] : (1 : α) + 1 = bit0 1 := rfl lemma subst_into_sum [has_add α] (l r tl tr t : α) (prl : l = tl) (prr : r = tr) diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean index eabb7f6f81..5ed0a49f71 100644 --- a/library/init/algebra/order.lean +++ b/library/init/algebra/order.lean @@ -178,6 +178,7 @@ or.elim (le_total a b) (λ h : b < a, or.inr (or.inr h)) (λ h : b = a, or.inr (or.inl h.symm))) + lemma le_of_not_gt [linear_strong_order_pair α] {a b : α} (h : ¬ a > b) : a ≤ b := match lt_trichotomy a b with | or.inl hlt := le_of_lt hlt diff --git a/library/init/core.lean b/library/init/core.lean index 8b7ff90c84..c02cbab47e 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -323,53 +323,53 @@ class has_sep (α : out_param (Type u)) (γ : Type v) := /- Type class for set-like membership -/ class has_mem (α : out_param (Type u)) (γ : Type v) := (mem : α → γ → Prop) -def zero {α : Type u} [has_zero α] : α := has_zero.zero α -def one {α : Type u} [has_one α] : α := has_one.one α -def add {α : Type u} [has_add α] : α → α → α := has_add.add -def mul {α : Type u} [has_mul α] : α → α → α := has_mul.mul -def sub {α : Type u} [has_sub α] : α → α → α := has_sub.sub -def div {α : Type u} [has_div α] : α → α → α := has_div.div -def dvd {α : Type u} [has_dvd α] : α → α → Prop := has_dvd.dvd -def mod {α : Type u} [has_mod α] : α → α → α := has_mod.mod -def neg {α : Type u} [has_neg α] : α → α := has_neg.neg -def inv {α : Type u} [has_inv α] : α → α := has_inv.inv -def le {α : Type u} [has_le α] : α → α → Prop := has_le.le -def lt {α : Type u} [has_lt α] : α → α → Prop := has_lt.lt -def append {α : Type u} [has_append α] : α → α → α := has_append.append -def andthen {α : Type u} [has_andthen α] : α → α → α := has_andthen.andthen -def union {α : Type u} [has_union α] : α → α → α := has_union.union -def inter {α : Type u} [has_inter α] : α → α → α := has_inter.inter -def sdiff {α : Type u} [has_sdiff α] : α → α → α := has_sdiff.sdiff -def subset {α : Type u} [has_subset α] : α → α → Prop := has_subset.subset -def ssubset {α : Type u} [has_ssubset α] : α → α → Prop := has_ssubset.ssubset -@[reducible] -def ge {α : Type u} [has_le α] (a b : α) : Prop := le b a -@[reducible] -def gt {α : Type u} [has_lt α] (a b : α) : Prop := lt b a -@[reducible] -def superset {α : Type u} [has_subset α] (a b : α) : Prop := subset b a -@[reducible] -def ssuperset {α : Type u} [has_ssubset α] (a b : α) : Prop := ssubset b a -def bit0 {α : Type u} [s : has_add α] (a : α) : α := add a a -def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α := add (bit0 a) one +infix ∈ := has_mem.mem +notation a ∉ s := ¬ has_mem.mem a s +infix + := has_add.add +infix * := has_mul.mul +infix - := has_sub.sub +infix / := has_div.div +infix ∣ := has_dvd.dvd +infix % := has_mod.mod +prefix - := has_neg.neg +infix <= := has_le.le +infix ≤ := has_le.le +infix < := has_lt.lt +infix ++ := has_append.append +infix ; := has_andthen.andthen +notation `∅` := has_emptyc.emptyc _ +infix ∪ := has_union.union +infix ∩ := has_inter.inter +infix ⊆ := has_subset.subset +infix ⊂ := has_ssubset.ssubset +infix \ := has_sdiff.sdiff -attribute [pattern] zero one bit0 bit1 add neg +export has_append (append) + +@[reducible] def ge {α : Type u} [has_le α] (a b : α) : Prop := has_le.le b a +@[reducible] def gt {α : Type u} [has_lt α] (a b : α) : Prop := has_lt.lt b a + +infix >= := ge +infix ≥ := ge +infix > := gt + +@[reducible] def superset {α : Type u} [has_subset α] (a b : α) : Prop := has_subset.subset b a +@[reducible] def ssuperset {α : Type u} [has_ssubset α] (a b : α) : Prop := has_ssubset.ssubset b a + +infix ⊇ := superset +infix ⊃ := ssuperset + +def bit0 {α : Type u} [s : has_add α] (a : α) : α := a + a +def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α := (bit0 a) + 1 + +attribute [pattern] has_zero.zero has_one.one bit0 bit1 has_add.add has_neg.neg def insert {α : Type u} {γ : Type v} [has_insert α γ] : α → γ → γ := has_insert.insert /- The empty collection -/ -def emptyc {α : Type u} [has_emptyc α] : α := -has_emptyc.emptyc α - def singleton {α : Type u} {γ : Type v} [has_emptyc γ] [has_insert α γ] (a : α) : γ := -insert a emptyc - -def sep {α : Type u} {γ : Type v} [has_sep α γ] : (α → Prop) → γ → γ := -has_sep.sep - -def mem {α : Type u} {γ : Type v} [has_mem α γ] : α → γ → Prop := -has_mem.mem +has_insert.insert a ∅ /- num, pos_num instances -/ @@ -475,33 +475,7 @@ num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ ( (num.succ std.prec.max))))))))) reserve postfix `⁻¹`:std.prec.max_plus -- input with \sy or \-1 or \inv - -infix ∈ := mem -notation a ∉ s := ¬ mem a s -infix + := add -infix * := mul -infix - := sub -infix / := div -infix ∣ := dvd -infix % := mod -prefix - := neg -postfix ⁻¹ := inv -infix <= := le -infix >= := ge -infix ≤ := le -infix ≥ := ge -infix < := lt -infix > := gt -infix ++ := append -infix ; := andthen -notation `∅` := emptyc -infix ∪ := union -infix ∩ := inter -infix ⊆ := subset -infix ⊇ := superset -infix ⊂ := ssubset -infix ⊃ := ssuperset -infix \ := sdiff +postfix ⁻¹ := has_inv.inv notation α × β := prod α β -- notation for n-ary tuples diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index e3a2eef6b2..1ceffe87ec 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -230,12 +230,12 @@ rel_int_nat_nat.pos protected lemma rel_one : rel_int_nat_nat 1 (1, 0) := rel_int_nat_nat.pos -protected lemma rel_neg : (rel_int_nat_nat ⇒ rel_int_nat_nat) neg (λa, (a.2, a.1)) +protected lemma rel_neg : (rel_int_nat_nat ⇒ rel_int_nat_nat) has_neg.neg (λa, (a.2, a.1)) | ._ ._ (@rel_int_nat_nat.pos m p) := int.rel_neg_of_nat | ._ ._ (@rel_int_nat_nat.neg m n) := rel_int_nat_nat.pos protected lemma rel_add : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_nat)) - add (λa b, (a.1 + b.1, a.2 + b.2)) + has_add.add (λa b, (a.1 + b.1, a.2 + b.2)) | ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := have eq : m + p + (m' + p') = m + m' + (p + p'), by simp, @@ -268,7 +268,7 @@ protected lemma rel_add : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_ begin rw [eq], apply rel_int_nat_nat.neg end protected lemma rel_mul : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_nat)) - mul (λa b, (a.1 * b.1 + a.2 * b.2, a.1 * b.2 + a.2 * b.1)) + has_mul.mul (λa b, (a.1 * b.1 + a.2 * b.2, a.1 * b.2 + a.2 * b.1)) | ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := have e : (m + p) * (m' + p') + m * m' = (m + p) * m' + m * (m' + p') + p * p', by simp [mul_add, add_mul], diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index ec9763bbbd..1a05cd877c 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -123,7 +123,7 @@ def map₂ (f : α → β → γ) : list α → list β → list γ def join : list (list α) → list α | [] := [] -| (l :: ls) := append l (join ls) +| (l :: ls) := l ++ (join ls) def filter (p : α → Prop) [decidable_pred p] : list α → list α | [] := [] @@ -197,7 +197,7 @@ def enum_from : ℕ → list α → list (ℕ × α) def enum : list α → list (ℕ × α) := enum_from 0 def sum [has_add α] [has_zero α] : list α → α := -foldl add zero +foldl (+) 0 def last : Π l : list α, l ≠ [] → α | [] h := absurd rfl h diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index d577725f5b..a021ba22a2 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -63,10 +63,10 @@ rfl by induction s; simph lemma length_concat (a : α) (l : list α) : length (concat l a) = succ (length l) := -by simp +by simp [succ_eq_add_one] @[simp] lemma length_repeat (a : α) (n : ℕ) : length (repeat a n) = n := -by induction n; simph +by induction n; simph; refl lemma eq_nil_of_length_eq_zero {l : list α} : length l = 0 → l = [] := by {induction l; intros, refl, contradiction} @@ -78,7 +78,7 @@ by induction l; intros; contradiction @[simp] lemma length_taken : ∀ (i : ℕ) (l : list α), length (taken i l) = min i (length l) | 0 l := by simp | (succ n) [] := by simp -| (succ n) (a::l) := by simph [nat.min_succ_succ]; rw [-add_one_eq_succ]; simp +| (succ n) (a::l) := begin simph [nat.min_succ_succ, add_one_eq_succ] end -- TODO(Leo): cleanup proof after arith dec proc @[simp] lemma length_dropn : ∀ (i : ℕ) (l : list α), length (dropn i l) = length l - i diff --git a/library/init/data/nat/div.lean b/library/init/data/nat/div.lean index cc4cf74c23..fa8678d5be 100644 --- a/library/init/data/nat/div.lean +++ b/library/init/data/nat/div.lean @@ -18,7 +18,7 @@ protected def div := well_founded.fix lt_wf div.F instance : has_div nat := ⟨nat.div⟩ -lemma div_def_aux (x y : nat) : div x y = if h : 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := +lemma div_def_aux (x y : nat) : x / y = if h : 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := congr_fun (well_founded.fix_eq lt_wf div.F x) y private def mod.F (x : nat) (f : Π x₁, x₁ < x → nat → nat) (y : nat) : nat := @@ -29,7 +29,7 @@ protected def mod := well_founded.fix lt_wf mod.F instance : has_mod nat := ⟨nat.mod⟩ -lemma mod_def_aux (x y : nat) : mod x y = if h : 0 < y ∧ y ≤ x then mod (x - y) y else x := +lemma mod_def_aux (x y : nat) : x % y = if h : 0 < y ∧ y ≤ x then (x - y) % y else x := congr_fun (well_founded.fix_eq lt_wf mod.F x) y end nat diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index cc0a00dd25..61982643a7 100644 --- a/library/init/data/nat/lemmas.lean +++ b/library/init/data/nat/lemmas.lean @@ -26,6 +26,9 @@ protected lemma add_zero : ∀ n : ℕ, n + 0 = n := lemma add_one_eq_succ : ∀ n : ℕ, n + 1 = succ n := λ n, rfl +lemma succ_eq_add_one : ∀ n : ℕ, succ n = n + 1 := +λ n, rfl + protected lemma add_comm : ∀ n m : ℕ, n + m = m + n | n 0 := eq.symm (nat.zero_add n) | n (m+1) := @@ -818,7 +821,7 @@ nat.strong_induction_on a $ λ n, end /- mod -/ -lemma mod_def (x y : nat) : mod x y = if 0 < y ∧ y ≤ x then mod (x - y) y else x := +lemma mod_def (x y : nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by note h := mod_def_aux x y; rwa [dif_eq_if] at h lemma mod_zero (a : nat) : a % 0 = a := @@ -914,7 +917,7 @@ begin end /- div & mod -/ -lemma div_def (x y : nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 := +lemma div_def (x y : nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by note h := div_def_aux x y; rwa dif_eq_if at h lemma mod_add_div (m k : ℕ) @@ -1033,7 +1036,9 @@ begin rw [ -add_one_eq_succ , nat.add_le_add_iff_le_right , IH (y - k) Hlt x - , succ_mul,add_le_to_le_sub _ h] } } + , add_one_eq_succ + , succ_mul, add_le_to_le_sub _ h ] + } } end theorem div_lt_iff_lt_mul (x y : ℕ) {k : ℕ} diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean index 49df129bab..84e512f5f3 100644 --- a/library/init/data/to_string.lean +++ b/library/init/data/to_string.lean @@ -72,7 +72,7 @@ else "f" def char_to_hex (c : char) : string := let n := char.to_nat c, - d2 := div n 16, + d2 := n / 16, d1 := n % 16 in hex_digit_to_string d2 ++ hex_digit_to_string d1 diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index f627a6ec6b..0a6b4d5136 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -272,16 +272,16 @@ then some (app_arg (app_fn e), app_arg e) else none meta def is_lt (e : expr) : option (expr × expr) := -is_bin_arith_app e `lt +is_bin_arith_app e ``has_lt.lt meta def is_gt (e : expr) : option (expr × expr) := -is_bin_arith_app e `gt +is_bin_arith_app e ``gt meta def is_le (e : expr) : option (expr × expr) := -is_bin_arith_app e `le +is_bin_arith_app e ``has_le.le meta def is_ge (e : expr) : option (expr × expr) := -is_bin_arith_app e `ge +is_bin_arith_app e ``ge meta def is_heq : expr → option (expr × expr × expr × expr) | ```(@heq %%α %%a %%β %%b) := some (α, a, β, b) diff --git a/library/init/meta/smt/rsimp.lean b/library/init/meta/smt/rsimp.lean index c836d247e5..743477320f 100644 --- a/library/init/meta/smt/rsimp.lean +++ b/library/init/meta/smt/rsimp.lean @@ -65,11 +65,11 @@ meta def is_value_like : expr → bool if ¬ fn.is_constant then ff else let nargs := e.get_app_num_args, fname := fn.const_name in - if fname = `zero ∧ nargs = 2 then tt - else if fname = `one ∧ nargs = 2 then tt - else if fname = `bit0 ∧ nargs = 3 then is_value_like e.app_arg - else if fname = `bit1 ∧ nargs = 4 then is_value_like e.app_arg - else if fname = `char.of_nat ∧ nargs = 1 then is_value_like e.app_arg + if fname = ``has_zero.zero ∧ nargs = 2 then tt + else if fname = ``has_one.one ∧ nargs = 2 then tt + else if fname = ``bit0 ∧ nargs = 3 then is_value_like e.app_arg + else if fname = ``bit1 ∧ nargs = 4 then is_value_like e.app_arg + else if fname = ``char.of_nat ∧ nargs = 1 then is_value_like e.app_arg else ff /-- Return the size of term by considering only explicit arguments. -/ diff --git a/library/init/meta/transfer.lean b/library/init/meta/transfer.lean index 3d6ca447db..295aeca639 100644 --- a/library/init/meta/transfer.lean +++ b/library/init/meta/transfer.lean @@ -73,7 +73,7 @@ meta instance has_to_tactic_format_rule_data : has_to_tactic_format rule_data := private meta def get_lift_fun : expr → tactic (list rel_data × expr) | e := do { - guardb (is_constant_of (get_app_fn e) `relator.lift_fun), + guardb (is_constant_of (get_app_fn e) ``relator.lift_fun), [α, β, γ, δ, R, S] ← return $ get_app_args e, (ps, r) ← get_lift_fun S, return (rel_data.mk α β R :: ps, r)} <|> diff --git a/library/init/wf.lean b/library/init/wf.lean index 5a6aae1e4b..c9b69edb5b 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -131,7 +131,7 @@ def nat.lt_wf : well_founded nat.lt := (λ e, eq.substr e ih) (acc.inv ih)))⟩ def measure {α : Type u} : (α → ℕ) → α → α → Prop := -inv_image lt +inv_image (<) def measure_wf {α : Type u} (f : α → ℕ) : well_founded (measure f) := inv_image.wf f nat.lt_wf diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp index 608a1d7219..75a7c23cfd 100644 --- a/src/frontends/lean/brackets.cpp +++ b/src/frontends/lean/brackets.cpp @@ -50,7 +50,7 @@ static expr parse_fin_set(parser & p, pos_info const & pos, expr const & e) { auto ins_pos = p.pos(); p.next(); expr e2 = p.parse_expr(); - expr insert = p.save_pos(mk_constant(get_insert_name()), ins_pos); + expr insert = p.save_pos(mk_constant(get_has_insert_insert_name()), ins_pos); r = p.rec_save_pos(mk_app(insert, e2, r), ins_pos); } p.check_token_next(get_rcurly_tk(), "invalid explicit finite collection, '}' expected"); @@ -68,7 +68,7 @@ static expr parse_sep(parser & p, pos_info const & pos, name const & id) { p.check_token_next(get_rcurly_tk(), "invalid sep expression, '}' expected"); bool use_cache = false; pred = p.rec_save_pos(Fun(local, pred, use_cache), pos); - return p.rec_save_pos(mk_app(mk_constant(get_sep_name()), pred, s), pos); + return p.rec_save_pos(mk_app(mk_constant(get_has_sep_sep_name()), pred, s), pos); } static expr parse_structure_instance_core(parser & p, optional const & src, name const & S, name const & fname) { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index bfde549a4d..9944c513c4 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -854,11 +854,11 @@ expr elaborator::visit_prenum(expr const & e, optional const & expected_ty if (v.is_zero()) { expr has_zero_A = mk_app(mk_constant(get_has_zero_name(), ls), A, e_tag); expr S = mk_instance(has_zero_A, ref); - return mk_app(mk_app(mk_constant(get_zero_name(), ls), A, e_tag), S, e_tag); + return mk_app(mk_app(mk_constant(get_has_zero_zero_name(), ls), A, e_tag), S, e_tag); } else { expr has_one_A = mk_app(mk_constant(get_has_one_name(), ls), A, e_tag); expr S_one = mk_instance(has_one_A, ref); - expr one = mk_app(mk_app(mk_constant(get_one_name(), ls), A, e_tag), S_one, e_tag); + expr one = mk_app(mk_app(mk_constant(get_has_one_one_name(), ls), A, e_tag), S_one, e_tag); if (v == 1) { return one; } else { @@ -3111,9 +3111,14 @@ expr elaborator::visit_suffices_expr(expr const & e, optional const & expe return mk_suffices_annotation(mk_app(new_fn, new_rest)); } +static expr mk_emptyc(expr const & src) { + return copy_tag(src, mk_app(copy_tag(src, mk_constant(get_has_emptyc_emptyc_name())), + copy_tag(src, mk_expr_placeholder()))); +} + expr elaborator::visit_emptyc_or_emptys(expr const & e, optional const & expected_type) { if (!expected_type) { - return visit(copy_tag(e, mk_constant(get_emptyc_name())), expected_type); + return visit(mk_emptyc(e), expected_type); } else { synthesize_type_class_instances(); expr new_expected_type = instantiate_mvars(*expected_type); @@ -3124,7 +3129,7 @@ expr elaborator::visit_emptyc_or_emptys(expr const & e, optional const & e expr empty_struct = copy_tag(e, mk_structure_instance(name(), buffer(), buffer())); return visit(empty_struct, expected_type); } else { - return visit(copy_tag(e, mk_constant(get_emptyc_name())), expected_type); + return visit(mk_emptyc(e), expected_type); } } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index d5b5eaf2c1..aa02d48ac2 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1957,7 +1957,7 @@ expr parser::parse_decimal_expr() { return num; } else { expr den = save_pos(mk_prenum(val.get_denominator()), p); - expr div = save_pos(mk_constant(get_div_name()), p); + expr div = save_pos(mk_constant(get_has_div_div_name()), p); return save_pos(lean::mk_app(div, num, den), p); } } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index e0427c4a36..9b0f3e4cd2 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1591,7 +1591,7 @@ auto pretty_fn::pp_subtype(expr const & e) -> result { static bool is_emptyc(expr const & e) { return - is_constant(get_app_fn(e), get_emptyc_name()) && + is_constant(get_app_fn(e), get_has_emptyc_emptyc_name()) && get_app_num_args(e) == 2; } @@ -1603,7 +1603,7 @@ static bool is_singleton(expr const & e) { static bool is_insert(expr const & e) { return - is_constant(get_app_fn(e), get_insert_name()) && + is_constant(get_app_fn(e), get_has_insert_insert_name()) && get_app_num_args(e) == 5; } @@ -1658,7 +1658,7 @@ auto pretty_fn::pp_set_of(expr const & e) -> result { static bool is_sep(expr const & e) { return - is_constant(get_app_fn(e), get_sep_name()) && + is_constant(get_app_fn(e), get_has_sep_sep_name()) && get_app_num_args(e) == 5 && is_lambda(app_arg(app_fn(e))); } diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index f0b19f070d..045983ff98 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -1265,7 +1265,6 @@ struct structure_cmd_fn { declaration coercion_decl = mk_definition_inferring_trusted(m_env, coercion_name, lnames, coercion_type, coercion_value, use_conv_opt); m_env = module::add(m_env, check(m_env, coercion_decl)); - m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible, true); add_alias(coercion_name); m_env = vm_compile(m_env, m_env.get(coercion_name)); if (!m_private_parents[i]) { diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index a9b03a82f2..f8bc73fe4c 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -210,7 +210,7 @@ struct parse_tactic_fn { } expr andthen(expr const & tac1, expr const & tac2, pos_info const & pos) { - return m_p.save_pos(mk_app(mk_constant(get_andthen_name()), tac1, tac2), pos); + return m_p.save_pos(mk_app(mk_constant(get_has_andthen_andthen_name()), tac1, tac2), pos); } expr orelse(expr const & tac1, expr const & tac2, pos_info const & pos) { diff --git a/src/frontends/smt2/elaborator.cpp b/src/frontends/smt2/elaborator.cpp index ce5db13aaa..8e829fb134 100644 --- a/src/frontends/smt2/elaborator.cpp +++ b/src/frontends/smt2/elaborator.cpp @@ -258,7 +258,7 @@ private: // Special case // (the map stores "-" ==> sub) if (n == "-" && args.size() == 2) { - arith_app_info info(get_neg_name(), get_int_has_neg_name(), get_real_has_neg_name()); + arith_app_info info(get_has_neg_neg_name(), get_int_has_neg_name(), get_real_has_neg_name()); return elaborate_arith(args, info); } @@ -320,20 +320,20 @@ void initialize_elaborator() { g_arith_symbol_map = new name_hash_map({ // Int-specific - {"mod", arith_app_info(get_mod_name(), get_int_has_mod_name())}, + {"mod", arith_app_info(get_has_mod_mod_name(), get_int_has_mod_name())}, {"abs", arith_app_info(get_abs_name(), get_int_decidable_linear_ordered_comm_group_name())}, - {"div", arith_app_info(get_div_name(), get_int_has_div_name(), name(), fun_attr::LEFT_ASSOC)}, + {"div", arith_app_info(get_has_div_div_name(), get_int_has_div_name(), name(), fun_attr::LEFT_ASSOC)}, // Real-specific - {"/", arith_app_info(get_div_name(), name(), get_real_has_div_name(), fun_attr::LEFT_ASSOC)}, + {"/", arith_app_info(get_has_div_div_name(), name(), get_real_has_div_name(), fun_attr::LEFT_ASSOC)}, // Overloaded operators - {"+", arith_app_info(get_add_name(), get_int_has_add_name(), get_real_has_add_name(), fun_attr::LEFT_ASSOC)}, - {"*", arith_app_info(get_mul_name(), get_int_has_mul_name(), get_real_has_mul_name(), fun_attr::LEFT_ASSOC)}, - {"-", arith_app_info(get_sub_name(), get_int_has_sub_name(), get_real_has_sub_name(), fun_attr::LEFT_ASSOC)}, + {"+", arith_app_info(get_has_add_add_name(), get_int_has_add_name(), get_real_has_add_name(), fun_attr::LEFT_ASSOC)}, + {"*", arith_app_info(get_has_mul_mul_name(), get_int_has_mul_name(), get_real_has_mul_name(), fun_attr::LEFT_ASSOC)}, + {"-", arith_app_info(get_has_sub_sub_name(), get_int_has_sub_name(), get_real_has_sub_name(), fun_attr::LEFT_ASSOC)}, - {"<", arith_app_info(get_lt_name(), get_int_has_lt_name(), get_real_has_lt_name(), fun_attr::CHAINABLE)}, - {"<=", arith_app_info(get_le_name(), get_int_has_le_name(), get_real_has_le_name(), fun_attr::CHAINABLE)}, + {"<", arith_app_info(get_has_lt_lt_name(), get_int_has_lt_name(), get_real_has_lt_name(), fun_attr::CHAINABLE)}, + {"<=", arith_app_info(get_has_le_le_name(), get_int_has_le_name(), get_real_has_le_name(), fun_attr::CHAINABLE)}, {">", arith_app_info(get_gt_name(), get_int_has_lt_name(), get_real_has_lt_name(), fun_attr::CHAINABLE)}, {">=", arith_app_info(get_ge_name(), get_int_has_le_name(), get_real_has_le_name(), fun_attr::CHAINABLE)}, }); diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 5c5dae89d8..b876bb498f 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -700,7 +700,7 @@ public: trace_inst_failure(A, "has_add"); throw app_builder_exception(); } - return ::lean::mk_app(mk_constant(get_add_name(), {lvl}), A, *A_has_add); + return ::lean::mk_app(mk_constant(get_has_add_add_name(), {lvl}), A, *A_has_add); } expr mk_partial_mul(expr const & A) { @@ -710,7 +710,7 @@ public: trace_inst_failure(A, "has_mul"); throw app_builder_exception(); } - return ::lean::mk_app(mk_constant(get_mul_name(), {lvl}), A, *A_has_mul); + return ::lean::mk_app(mk_constant(get_has_mul_mul_name(), {lvl}), A, *A_has_mul); } expr mk_zero(expr const & A) { @@ -720,7 +720,7 @@ public: trace_inst_failure(A, "has_zero"); throw app_builder_exception(); } - return ::lean::mk_app(mk_constant(get_zero_name(), {lvl}), A, *A_has_zero); + return ::lean::mk_app(mk_constant(get_has_zero_zero_name(), {lvl}), A, *A_has_zero); } expr mk_one(expr const & A) { @@ -730,7 +730,7 @@ public: trace_inst_failure(A, "has_one"); throw app_builder_exception(); } - return ::lean::mk_app(mk_constant(get_one_name(), {lvl}), A, *A_has_one); + return ::lean::mk_app(mk_constant(get_has_one_one_name(), {lvl}), A, *A_has_one); } expr mk_partial_left_distrib(expr const & A) { diff --git a/src/library/arith_instance.cpp b/src/library/arith_instance.cpp index 3b343f147d..eaff0b026d 100644 --- a/src/library/arith_instance.cpp +++ b/src/library/arith_instance.cpp @@ -62,16 +62,16 @@ expr arith_instance::mk_bit1() { return *m_info->m_bit1; } -expr arith_instance::mk_zero() { return mk_op(get_zero_name(), get_has_zero_name(), m_info->m_zero); } -expr arith_instance::mk_one() { return mk_op(get_one_name(), get_has_one_name(), m_info->m_one); } -expr arith_instance::mk_add() { return mk_op(get_add_name(), get_has_add_name(), m_info->m_add); } -expr arith_instance::mk_sub() { return mk_op(get_sub_name(), get_has_sub_name(), m_info->m_sub); } -expr arith_instance::mk_neg() { return mk_op(get_neg_name(), get_has_neg_name(), m_info->m_neg); } -expr arith_instance::mk_mul() { return mk_op(get_mul_name(), get_has_mul_name(), m_info->m_mul); } -expr arith_instance::mk_div() { return mk_op(get_div_name(), get_has_div_name(), m_info->m_div); } -expr arith_instance::mk_inv() { return mk_op(get_inv_name(), get_has_inv_name(), m_info->m_inv); } -expr arith_instance::mk_lt() { return mk_op(get_lt_name(), get_has_lt_name(), m_info->m_lt); } -expr arith_instance::mk_le() { return mk_op(get_le_name(), get_has_le_name(), m_info->m_le); } +expr arith_instance::mk_zero() { return mk_op(get_has_zero_zero_name(), get_has_zero_name(), m_info->m_zero); } +expr arith_instance::mk_one() { return mk_op(get_has_one_one_name(), get_has_one_name(), m_info->m_one); } +expr arith_instance::mk_add() { return mk_op(get_has_add_add_name(), get_has_add_name(), m_info->m_add); } +expr arith_instance::mk_sub() { return mk_op(get_has_sub_sub_name(), get_has_sub_name(), m_info->m_sub); } +expr arith_instance::mk_neg() { return mk_op(get_has_neg_neg_name(), get_has_neg_name(), m_info->m_neg); } +expr arith_instance::mk_mul() { return mk_op(get_has_mul_mul_name(), get_has_mul_name(), m_info->m_mul); } +expr arith_instance::mk_div() { return mk_op(get_has_div_div_name(), get_has_div_name(), m_info->m_div); } +expr arith_instance::mk_inv() { return mk_op(get_has_inv_inv_name(), get_has_inv_name(), m_info->m_inv); } +expr arith_instance::mk_lt() { return mk_op(get_has_lt_lt_name(), get_has_lt_name(), m_info->m_lt); } +expr arith_instance::mk_le() { return mk_op(get_has_le_le_name(), get_has_le_name(), m_info->m_le); } expr arith_instance::mk_bit0() { return mk_op(get_bit0_name(), get_has_add_name(), m_info->m_bit0); } @@ -131,15 +131,15 @@ optional arith_instance::eval(expr const & e) { expr f = get_app_args(e, args); if (!is_constant(f)) { throw exception("cannot find num of nonconstant"); - } else if (const_name(f) == get_add_name() && args.size() == 4) { + } else if (const_name(f) == get_has_add_add_name() && args.size() == 4) { if (auto r1 = eval(args[2])) if (auto r2 = eval(args[3])) return optional(*r1 + *r2); - } else if (const_name(f) == get_mul_name() && args.size() == 4) { + } else if (const_name(f) == get_has_mul_mul_name() && args.size() == 4) { if (auto r1 = eval(args[2])) if (auto r2 = eval(args[3])) return optional(*r1 * *r2); - } else if (const_name(f) == get_sub_name() && args.size() == 4) { + } else if (const_name(f) == get_has_sub_sub_name() && args.size() == 4) { if (auto r1 = eval(args[2])) if (auto r2 = eval(args[3])) { if (is_nat() && *r2 > *r1) @@ -147,7 +147,7 @@ optional arith_instance::eval(expr const & e) { else return optional(*r1 - *r2); } - } else if (const_name(f) == get_div_name() && args.size() == 4) { + } else if (const_name(f) == get_has_div_div_name() && args.size() == 4) { if (auto r1 = eval(args[2])) if (auto r2 = eval(args[3])) { if (is_nat()) @@ -157,7 +157,7 @@ optional arith_instance::eval(expr const & e) { else return optional(*r1 / *r2); } - } else if (const_name(f) == get_neg_name() && args.size() == 3) { + } else if (const_name(f) == get_has_neg_neg_name() && args.size() == 3) { if (auto r1 = eval(args[2])) return optional(neg(*r1)); } else if (auto r = to_num(e)) { diff --git a/src/library/constants.cpp b/src/library/constants.cpp index a59c5110d2..ba11c9549f 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -6,7 +6,6 @@ namespace lean{ name const * g_abs = nullptr; name const * g_absurd = nullptr; name const * g_acc_cases_on = nullptr; -name const * g_add = nullptr; name const * g_add_comm_group = nullptr; name const * g_add_comm_semigroup = nullptr; name const * g_add_group = nullptr; @@ -17,7 +16,6 @@ name const * g_and_elim_right = nullptr; name const * g_and_intro = nullptr; name const * g_and_rec = nullptr; name const * g_and_cases_on = nullptr; -name const * g_andthen = nullptr; name const * g_auto_param = nullptr; name const * g_bit0 = nullptr; name const * g_bit1 = nullptr; @@ -44,10 +42,8 @@ name const * g_decidable = nullptr; name const * g_decidable_to_bool = nullptr; name const * g_distrib = nullptr; name const * g_dite = nullptr; -name const * g_div = nullptr; name const * g_id = nullptr; name const * g_empty = nullptr; -name const * g_emptyc = nullptr; name const * g_Exists = nullptr; name const * g_eq = nullptr; name const * g_eq_cases_on = nullptr; @@ -82,20 +78,33 @@ name const * g_funext = nullptr; name const * g_ge = nullptr; name const * g_gt = nullptr; name const * g_has_add = nullptr; +name const * g_has_add_add = nullptr; +name const * g_has_andthen_andthen = nullptr; name const * g_has_bind_and_then = nullptr; name const * g_has_bind_bind = nullptr; name const * g_has_bind_seq = nullptr; name const * g_has_div = nullptr; +name const * g_has_div_div = nullptr; +name const * g_has_emptyc_emptyc = nullptr; +name const * g_has_mod_mod = nullptr; name const * g_has_mul = nullptr; +name const * g_has_mul_mul = nullptr; +name const * g_has_insert_insert = nullptr; name const * g_has_inv = nullptr; +name const * g_has_inv_inv = nullptr; name const * g_has_le = nullptr; +name const * g_has_le_le = nullptr; name const * g_has_lt = nullptr; +name const * g_has_lt_lt = nullptr; name const * g_has_neg = nullptr; +name const * g_has_neg_neg = nullptr; name const * g_has_one = nullptr; name const * g_has_one_one = nullptr; +name const * g_has_sep_sep = nullptr; name const * g_has_sizeof = nullptr; name const * g_has_sizeof_mk = nullptr; name const * g_has_sub = nullptr; +name const * g_has_sub_sub = nullptr; name const * g_has_to_format = nullptr; name const * g_has_to_string = nullptr; name const * g_has_zero = nullptr; @@ -127,7 +136,6 @@ name const * g_implies_of_if_neg = nullptr; name const * g_implies_of_if_pos = nullptr; name const * g_inductive_compiler_tactic_prove_nested_inj = nullptr; name const * g_inductive_compiler_tactic_prove_pack_inj = nullptr; -name const * g_insert = nullptr; name const * g_int = nullptr; name const * g_int_has_add = nullptr; name const * g_int_has_mul = nullptr; @@ -157,7 +165,6 @@ name const * g_int_zero_ne_neg_of_ne = nullptr; name const * g_int_decidable_linear_ordered_comm_group = nullptr; name const * g_interactive_param_desc = nullptr; name const * g_interactive_parse = nullptr; -name const * g_inv = nullptr; name const * g_io = nullptr; name const * g_io_interface = nullptr; name const * g_is_associative = nullptr; @@ -167,20 +174,16 @@ name const * g_is_commutative_comm = nullptr; name const * g_ite = nullptr; name const * g_left_distrib = nullptr; name const * g_left_comm = nullptr; -name const * g_le = nullptr; name const * g_le_refl = nullptr; name const * g_linear_ordered_ring = nullptr; name const * g_linear_ordered_semiring = nullptr; name const * g_list = nullptr; name const * g_list_nil = nullptr; name const * g_list_cons = nullptr; -name const * g_lt = nullptr; name const * g_match_failed = nullptr; -name const * g_mod = nullptr; name const * g_monad = nullptr; name const * g_monad_fail = nullptr; name const * g_monoid = nullptr; -name const * g_mul = nullptr; name const * g_mul_one = nullptr; name const * g_mul_zero = nullptr; name const * g_mul_zero_class = nullptr; @@ -222,7 +225,6 @@ name const * g_nat_one_lt_bit1 = nullptr; name const * g_nat_le_of_lt = nullptr; name const * g_nat_le_refl = nullptr; name const * g_ne = nullptr; -name const * g_neg = nullptr; name const * g_neq_of_not_iff = nullptr; name const * g_norm_num_add1 = nullptr; name const * g_norm_num_add1_bit0 = nullptr; @@ -279,7 +281,6 @@ name const * g_num_pos = nullptr; name const * g_num_zero = nullptr; name const * g_of_eq_true = nullptr; name const * g_of_iff_true = nullptr; -name const * g_one = nullptr; name const * g_opt_param = nullptr; name const * g_or = nullptr; name const * g_orelse = nullptr; @@ -316,7 +317,6 @@ name const * g_right_distrib = nullptr; name const * g_ring = nullptr; name const * g_scope_trace = nullptr; name const * g_set_of = nullptr; -name const * g_sep = nullptr; name const * g_semiring = nullptr; name const * g_sigma = nullptr; name const * g_sigma_mk = nullptr; @@ -338,7 +338,6 @@ name const * g_string_empty_ne_str = nullptr; name const * g_string_str_ne_empty = nullptr; name const * g_string_str_ne_str_left = nullptr; name const * g_string_str_ne_str_right = nullptr; -name const * g_sub = nullptr; name const * g_subsingleton = nullptr; name const * g_subsingleton_elim = nullptr; name const * g_subsingleton_helim = nullptr; @@ -351,7 +350,6 @@ name const * g_psum_cases_on = nullptr; name const * g_psum_inl = nullptr; name const * g_psum_inr = nullptr; name const * g_tactic = nullptr; -name const * g_tactic_eval_expr = nullptr; name const * g_tactic_try = nullptr; name const * g_tactic_triv = nullptr; name const * g_thunk = nullptr; @@ -372,7 +370,6 @@ name const * g_vm_monitor = nullptr; name const * g_weak_order = nullptr; name const * g_well_founded = nullptr; name const * g_xor = nullptr; -name const * g_zero = nullptr; name const * g_zero_le_one = nullptr; name const * g_zero_lt_one = nullptr; name const * g_zero_mul = nullptr; @@ -380,7 +377,6 @@ void initialize_constants() { g_abs = new name{"abs"}; g_absurd = new name{"absurd"}; g_acc_cases_on = new name{"acc", "cases_on"}; - g_add = new name{"add"}; g_add_comm_group = new name{"add_comm_group"}; g_add_comm_semigroup = new name{"add_comm_semigroup"}; g_add_group = new name{"add_group"}; @@ -391,7 +387,6 @@ void initialize_constants() { g_and_intro = new name{"and", "intro"}; g_and_rec = new name{"and", "rec"}; g_and_cases_on = new name{"and", "cases_on"}; - g_andthen = new name{"andthen"}; g_auto_param = new name{"auto_param"}; g_bit0 = new name{"bit0"}; g_bit1 = new name{"bit1"}; @@ -418,10 +413,8 @@ void initialize_constants() { g_decidable_to_bool = new name{"decidable", "to_bool"}; g_distrib = new name{"distrib"}; g_dite = new name{"dite"}; - g_div = new name{"div"}; g_id = new name{"id"}; g_empty = new name{"empty"}; - g_emptyc = new name{"emptyc"}; g_Exists = new name{"Exists"}; g_eq = new name{"eq"}; g_eq_cases_on = new name{"eq", "cases_on"}; @@ -456,20 +449,33 @@ void initialize_constants() { g_ge = new name{"ge"}; g_gt = new name{"gt"}; g_has_add = new name{"has_add"}; + g_has_add_add = new name{"has_add", "add"}; + g_has_andthen_andthen = new name{"has_andthen", "andthen"}; g_has_bind_and_then = new name{"has_bind", "and_then"}; g_has_bind_bind = new name{"has_bind", "bind"}; g_has_bind_seq = new name{"has_bind", "seq"}; g_has_div = new name{"has_div"}; + g_has_div_div = new name{"has_div", "div"}; + g_has_emptyc_emptyc = new name{"has_emptyc", "emptyc"}; + g_has_mod_mod = new name{"has_mod", "mod"}; g_has_mul = new name{"has_mul"}; + g_has_mul_mul = new name{"has_mul", "mul"}; + g_has_insert_insert = new name{"has_insert", "insert"}; g_has_inv = new name{"has_inv"}; + g_has_inv_inv = new name{"has_inv", "inv"}; g_has_le = new name{"has_le"}; + g_has_le_le = new name{"has_le", "le"}; g_has_lt = new name{"has_lt"}; + g_has_lt_lt = new name{"has_lt", "lt"}; g_has_neg = new name{"has_neg"}; + g_has_neg_neg = new name{"has_neg", "neg"}; g_has_one = new name{"has_one"}; g_has_one_one = new name{"has_one", "one"}; + g_has_sep_sep = new name{"has_sep", "sep"}; g_has_sizeof = new name{"has_sizeof"}; g_has_sizeof_mk = new name{"has_sizeof", "mk"}; g_has_sub = new name{"has_sub"}; + g_has_sub_sub = new name{"has_sub", "sub"}; g_has_to_format = new name{"has_to_format"}; g_has_to_string = new name{"has_to_string"}; g_has_zero = new name{"has_zero"}; @@ -501,7 +507,6 @@ void initialize_constants() { g_implies_of_if_pos = new name{"implies_of_if_pos"}; g_inductive_compiler_tactic_prove_nested_inj = new name{"inductive_compiler", "tactic", "prove_nested_inj"}; g_inductive_compiler_tactic_prove_pack_inj = new name{"inductive_compiler", "tactic", "prove_pack_inj"}; - g_insert = new name{"insert"}; g_int = new name{"int"}; g_int_has_add = new name{"int", "has_add"}; g_int_has_mul = new name{"int", "has_mul"}; @@ -531,7 +536,6 @@ void initialize_constants() { g_int_decidable_linear_ordered_comm_group = new name{"int", "decidable_linear_ordered_comm_group"}; g_interactive_param_desc = new name{"interactive", "param_desc"}; g_interactive_parse = new name{"interactive", "parse"}; - g_inv = new name{"inv"}; g_io = new name{"io"}; g_io_interface = new name{"io", "interface"}; g_is_associative = new name{"is_associative"}; @@ -541,20 +545,16 @@ void initialize_constants() { g_ite = new name{"ite"}; g_left_distrib = new name{"left_distrib"}; g_left_comm = new name{"left_comm"}; - g_le = new name{"le"}; g_le_refl = new name{"le_refl"}; g_linear_ordered_ring = new name{"linear_ordered_ring"}; g_linear_ordered_semiring = new name{"linear_ordered_semiring"}; g_list = new name{"list"}; g_list_nil = new name{"list", "nil"}; g_list_cons = new name{"list", "cons"}; - g_lt = new name{"lt"}; g_match_failed = new name{"match_failed"}; - g_mod = new name{"mod"}; g_monad = new name{"monad"}; g_monad_fail = new name{"monad_fail"}; g_monoid = new name{"monoid"}; - g_mul = new name{"mul"}; g_mul_one = new name{"mul_one"}; g_mul_zero = new name{"mul_zero"}; g_mul_zero_class = new name{"mul_zero_class"}; @@ -596,7 +596,6 @@ void initialize_constants() { g_nat_le_of_lt = new name{"nat", "le_of_lt"}; g_nat_le_refl = new name{"nat", "le_refl"}; g_ne = new name{"ne"}; - g_neg = new name{"neg"}; g_neq_of_not_iff = new name{"neq_of_not_iff"}; g_norm_num_add1 = new name{"norm_num", "add1"}; g_norm_num_add1_bit0 = new name{"norm_num", "add1_bit0"}; @@ -653,7 +652,6 @@ void initialize_constants() { g_num_zero = new name{"num", "zero"}; g_of_eq_true = new name{"of_eq_true"}; g_of_iff_true = new name{"of_iff_true"}; - g_one = new name{"one"}; g_opt_param = new name{"opt_param"}; g_or = new name{"or"}; g_orelse = new name{"orelse"}; @@ -690,7 +688,6 @@ void initialize_constants() { g_ring = new name{"ring"}; g_scope_trace = new name{"scope_trace"}; g_set_of = new name{"set_of"}; - g_sep = new name{"sep"}; g_semiring = new name{"semiring"}; g_sigma = new name{"sigma"}; g_sigma_mk = new name{"sigma", "mk"}; @@ -712,7 +709,6 @@ void initialize_constants() { g_string_str_ne_empty = new name{"string", "str_ne_empty"}; g_string_str_ne_str_left = new name{"string", "str_ne_str_left"}; g_string_str_ne_str_right = new name{"string", "str_ne_str_right"}; - g_sub = new name{"sub"}; g_subsingleton = new name{"subsingleton"}; g_subsingleton_elim = new name{"subsingleton", "elim"}; g_subsingleton_helim = new name{"subsingleton", "helim"}; @@ -725,7 +721,6 @@ void initialize_constants() { g_psum_inl = new name{"psum", "inl"}; g_psum_inr = new name{"psum", "inr"}; g_tactic = new name{"tactic"}; - g_tactic_eval_expr = new name{"tactic", "eval_expr"}; g_tactic_try = new name{"tactic", "try"}; g_tactic_triv = new name{"tactic", "triv"}; g_thunk = new name{"thunk"}; @@ -746,7 +741,6 @@ void initialize_constants() { g_weak_order = new name{"weak_order"}; g_well_founded = new name{"well_founded"}; g_xor = new name{"xor"}; - g_zero = new name{"zero"}; g_zero_le_one = new name{"zero_le_one"}; g_zero_lt_one = new name{"zero_lt_one"}; g_zero_mul = new name{"zero_mul"}; @@ -755,7 +749,6 @@ void finalize_constants() { delete g_abs; delete g_absurd; delete g_acc_cases_on; - delete g_add; delete g_add_comm_group; delete g_add_comm_semigroup; delete g_add_group; @@ -766,7 +759,6 @@ void finalize_constants() { delete g_and_intro; delete g_and_rec; delete g_and_cases_on; - delete g_andthen; delete g_auto_param; delete g_bit0; delete g_bit1; @@ -793,10 +785,8 @@ void finalize_constants() { delete g_decidable_to_bool; delete g_distrib; delete g_dite; - delete g_div; delete g_id; delete g_empty; - delete g_emptyc; delete g_Exists; delete g_eq; delete g_eq_cases_on; @@ -831,20 +821,33 @@ void finalize_constants() { delete g_ge; delete g_gt; delete g_has_add; + delete g_has_add_add; + delete g_has_andthen_andthen; delete g_has_bind_and_then; delete g_has_bind_bind; delete g_has_bind_seq; delete g_has_div; + delete g_has_div_div; + delete g_has_emptyc_emptyc; + delete g_has_mod_mod; delete g_has_mul; + delete g_has_mul_mul; + delete g_has_insert_insert; delete g_has_inv; + delete g_has_inv_inv; delete g_has_le; + delete g_has_le_le; delete g_has_lt; + delete g_has_lt_lt; delete g_has_neg; + delete g_has_neg_neg; delete g_has_one; delete g_has_one_one; + delete g_has_sep_sep; delete g_has_sizeof; delete g_has_sizeof_mk; delete g_has_sub; + delete g_has_sub_sub; delete g_has_to_format; delete g_has_to_string; delete g_has_zero; @@ -876,7 +879,6 @@ void finalize_constants() { delete g_implies_of_if_pos; delete g_inductive_compiler_tactic_prove_nested_inj; delete g_inductive_compiler_tactic_prove_pack_inj; - delete g_insert; delete g_int; delete g_int_has_add; delete g_int_has_mul; @@ -906,7 +908,6 @@ void finalize_constants() { delete g_int_decidable_linear_ordered_comm_group; delete g_interactive_param_desc; delete g_interactive_parse; - delete g_inv; delete g_io; delete g_io_interface; delete g_is_associative; @@ -916,20 +917,16 @@ void finalize_constants() { delete g_ite; delete g_left_distrib; delete g_left_comm; - delete g_le; delete g_le_refl; delete g_linear_ordered_ring; delete g_linear_ordered_semiring; delete g_list; delete g_list_nil; delete g_list_cons; - delete g_lt; delete g_match_failed; - delete g_mod; delete g_monad; delete g_monad_fail; delete g_monoid; - delete g_mul; delete g_mul_one; delete g_mul_zero; delete g_mul_zero_class; @@ -971,7 +968,6 @@ void finalize_constants() { delete g_nat_le_of_lt; delete g_nat_le_refl; delete g_ne; - delete g_neg; delete g_neq_of_not_iff; delete g_norm_num_add1; delete g_norm_num_add1_bit0; @@ -1028,7 +1024,6 @@ void finalize_constants() { delete g_num_zero; delete g_of_eq_true; delete g_of_iff_true; - delete g_one; delete g_opt_param; delete g_or; delete g_orelse; @@ -1065,7 +1060,6 @@ void finalize_constants() { delete g_ring; delete g_scope_trace; delete g_set_of; - delete g_sep; delete g_semiring; delete g_sigma; delete g_sigma_mk; @@ -1087,7 +1081,6 @@ void finalize_constants() { delete g_string_str_ne_empty; delete g_string_str_ne_str_left; delete g_string_str_ne_str_right; - delete g_sub; delete g_subsingleton; delete g_subsingleton_elim; delete g_subsingleton_helim; @@ -1100,7 +1093,6 @@ void finalize_constants() { delete g_psum_inl; delete g_psum_inr; delete g_tactic; - delete g_tactic_eval_expr; delete g_tactic_try; delete g_tactic_triv; delete g_thunk; @@ -1121,7 +1113,6 @@ void finalize_constants() { delete g_weak_order; delete g_well_founded; delete g_xor; - delete g_zero; delete g_zero_le_one; delete g_zero_lt_one; delete g_zero_mul; @@ -1129,7 +1120,6 @@ void finalize_constants() { name const & get_abs_name() { return *g_abs; } name const & get_absurd_name() { return *g_absurd; } name const & get_acc_cases_on_name() { return *g_acc_cases_on; } -name const & get_add_name() { return *g_add; } name const & get_add_comm_group_name() { return *g_add_comm_group; } name const & get_add_comm_semigroup_name() { return *g_add_comm_semigroup; } name const & get_add_group_name() { return *g_add_group; } @@ -1140,7 +1130,6 @@ name const & get_and_elim_right_name() { return *g_and_elim_right; } name const & get_and_intro_name() { return *g_and_intro; } name const & get_and_rec_name() { return *g_and_rec; } name const & get_and_cases_on_name() { return *g_and_cases_on; } -name const & get_andthen_name() { return *g_andthen; } name const & get_auto_param_name() { return *g_auto_param; } name const & get_bit0_name() { return *g_bit0; } name const & get_bit1_name() { return *g_bit1; } @@ -1167,10 +1156,8 @@ name const & get_decidable_name() { return *g_decidable; } name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; } name const & get_distrib_name() { return *g_distrib; } name const & get_dite_name() { return *g_dite; } -name const & get_div_name() { return *g_div; } name const & get_id_name() { return *g_id; } name const & get_empty_name() { return *g_empty; } -name const & get_emptyc_name() { return *g_emptyc; } name const & get_Exists_name() { return *g_Exists; } name const & get_eq_name() { return *g_eq; } name const & get_eq_cases_on_name() { return *g_eq_cases_on; } @@ -1205,20 +1192,33 @@ name const & get_funext_name() { return *g_funext; } name const & get_ge_name() { return *g_ge; } name const & get_gt_name() { return *g_gt; } name const & get_has_add_name() { return *g_has_add; } +name const & get_has_add_add_name() { return *g_has_add_add; } +name const & get_has_andthen_andthen_name() { return *g_has_andthen_andthen; } name const & get_has_bind_and_then_name() { return *g_has_bind_and_then; } name const & get_has_bind_bind_name() { return *g_has_bind_bind; } name const & get_has_bind_seq_name() { return *g_has_bind_seq; } name const & get_has_div_name() { return *g_has_div; } +name const & get_has_div_div_name() { return *g_has_div_div; } +name const & get_has_emptyc_emptyc_name() { return *g_has_emptyc_emptyc; } +name const & get_has_mod_mod_name() { return *g_has_mod_mod; } name const & get_has_mul_name() { return *g_has_mul; } +name const & get_has_mul_mul_name() { return *g_has_mul_mul; } +name const & get_has_insert_insert_name() { return *g_has_insert_insert; } name const & get_has_inv_name() { return *g_has_inv; } +name const & get_has_inv_inv_name() { return *g_has_inv_inv; } name const & get_has_le_name() { return *g_has_le; } +name const & get_has_le_le_name() { return *g_has_le_le; } name const & get_has_lt_name() { return *g_has_lt; } +name const & get_has_lt_lt_name() { return *g_has_lt_lt; } name const & get_has_neg_name() { return *g_has_neg; } +name const & get_has_neg_neg_name() { return *g_has_neg_neg; } name const & get_has_one_name() { return *g_has_one; } name const & get_has_one_one_name() { return *g_has_one_one; } +name const & get_has_sep_sep_name() { return *g_has_sep_sep; } name const & get_has_sizeof_name() { return *g_has_sizeof; } name const & get_has_sizeof_mk_name() { return *g_has_sizeof_mk; } name const & get_has_sub_name() { return *g_has_sub; } +name const & get_has_sub_sub_name() { return *g_has_sub_sub; } name const & get_has_to_format_name() { return *g_has_to_format; } name const & get_has_to_string_name() { return *g_has_to_string; } name const & get_has_zero_name() { return *g_has_zero; } @@ -1250,7 +1250,6 @@ name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } name const & get_inductive_compiler_tactic_prove_nested_inj_name() { return *g_inductive_compiler_tactic_prove_nested_inj; } name const & get_inductive_compiler_tactic_prove_pack_inj_name() { return *g_inductive_compiler_tactic_prove_pack_inj; } -name const & get_insert_name() { return *g_insert; } name const & get_int_name() { return *g_int; } name const & get_int_has_add_name() { return *g_int_has_add; } name const & get_int_has_mul_name() { return *g_int_has_mul; } @@ -1280,7 +1279,6 @@ name const & get_int_zero_ne_neg_of_ne_name() { return *g_int_zero_ne_neg_of_ne; name const & get_int_decidable_linear_ordered_comm_group_name() { return *g_int_decidable_linear_ordered_comm_group; } name const & get_interactive_param_desc_name() { return *g_interactive_param_desc; } name const & get_interactive_parse_name() { return *g_interactive_parse; } -name const & get_inv_name() { return *g_inv; } name const & get_io_name() { return *g_io; } name const & get_io_interface_name() { return *g_io_interface; } name const & get_is_associative_name() { return *g_is_associative; } @@ -1290,20 +1288,16 @@ name const & get_is_commutative_comm_name() { return *g_is_commutative_comm; } name const & get_ite_name() { return *g_ite; } name const & get_left_distrib_name() { return *g_left_distrib; } name const & get_left_comm_name() { return *g_left_comm; } -name const & get_le_name() { return *g_le; } name const & get_le_refl_name() { return *g_le_refl; } name const & get_linear_ordered_ring_name() { return *g_linear_ordered_ring; } name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semiring; } name const & get_list_name() { return *g_list; } name const & get_list_nil_name() { return *g_list_nil; } name const & get_list_cons_name() { return *g_list_cons; } -name const & get_lt_name() { return *g_lt; } name const & get_match_failed_name() { return *g_match_failed; } -name const & get_mod_name() { return *g_mod; } name const & get_monad_name() { return *g_monad; } name const & get_monad_fail_name() { return *g_monad_fail; } name const & get_monoid_name() { return *g_monoid; } -name const & get_mul_name() { return *g_mul; } name const & get_mul_one_name() { return *g_mul_one; } name const & get_mul_zero_name() { return *g_mul_zero; } name const & get_mul_zero_class_name() { return *g_mul_zero_class; } @@ -1345,7 +1339,6 @@ name const & get_nat_one_lt_bit1_name() { return *g_nat_one_lt_bit1; } name const & get_nat_le_of_lt_name() { return *g_nat_le_of_lt; } name const & get_nat_le_refl_name() { return *g_nat_le_refl; } name const & get_ne_name() { return *g_ne; } -name const & get_neg_name() { return *g_neg; } name const & get_neq_of_not_iff_name() { return *g_neq_of_not_iff; } name const & get_norm_num_add1_name() { return *g_norm_num_add1; } name const & get_norm_num_add1_bit0_name() { return *g_norm_num_add1_bit0; } @@ -1402,7 +1395,6 @@ name const & get_num_pos_name() { return *g_num_pos; } name const & get_num_zero_name() { return *g_num_zero; } name const & get_of_eq_true_name() { return *g_of_eq_true; } name const & get_of_iff_true_name() { return *g_of_iff_true; } -name const & get_one_name() { return *g_one; } name const & get_opt_param_name() { return *g_opt_param; } name const & get_or_name() { return *g_or; } name const & get_orelse_name() { return *g_orelse; } @@ -1439,7 +1431,6 @@ name const & get_right_distrib_name() { return *g_right_distrib; } name const & get_ring_name() { return *g_ring; } name const & get_scope_trace_name() { return *g_scope_trace; } name const & get_set_of_name() { return *g_set_of; } -name const & get_sep_name() { return *g_sep; } name const & get_semiring_name() { return *g_semiring; } name const & get_sigma_name() { return *g_sigma; } name const & get_sigma_mk_name() { return *g_sigma_mk; } @@ -1461,7 +1452,6 @@ name const & get_string_empty_ne_str_name() { return *g_string_empty_ne_str; } name const & get_string_str_ne_empty_name() { return *g_string_str_ne_empty; } name const & get_string_str_ne_str_left_name() { return *g_string_str_ne_str_left; } name const & get_string_str_ne_str_right_name() { return *g_string_str_ne_str_right; } -name const & get_sub_name() { return *g_sub; } name const & get_subsingleton_name() { return *g_subsingleton; } name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; } name const & get_subsingleton_helim_name() { return *g_subsingleton_helim; } @@ -1474,7 +1464,6 @@ name const & get_psum_cases_on_name() { return *g_psum_cases_on; } name const & get_psum_inl_name() { return *g_psum_inl; } name const & get_psum_inr_name() { return *g_psum_inr; } name const & get_tactic_name() { return *g_tactic; } -name const & get_tactic_eval_expr_name() { return *g_tactic_eval_expr; } name const & get_tactic_try_name() { return *g_tactic_try; } name const & get_tactic_triv_name() { return *g_tactic_triv; } name const & get_thunk_name() { return *g_thunk; } @@ -1495,7 +1484,6 @@ name const & get_vm_monitor_name() { return *g_vm_monitor; } name const & get_weak_order_name() { return *g_weak_order; } name const & get_well_founded_name() { return *g_well_founded; } name const & get_xor_name() { return *g_xor; } -name const & get_zero_name() { return *g_zero; } name const & get_zero_le_one_name() { return *g_zero_le_one; } name const & get_zero_lt_one_name() { return *g_zero_lt_one; } name const & get_zero_mul_name() { return *g_zero_mul; } diff --git a/src/library/constants.h b/src/library/constants.h index dcc45bc2d9..bb131f3c54 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -8,7 +8,6 @@ void finalize_constants(); name const & get_abs_name(); name const & get_absurd_name(); name const & get_acc_cases_on_name(); -name const & get_add_name(); name const & get_add_comm_group_name(); name const & get_add_comm_semigroup_name(); name const & get_add_group_name(); @@ -19,7 +18,6 @@ name const & get_and_elim_right_name(); name const & get_and_intro_name(); name const & get_and_rec_name(); name const & get_and_cases_on_name(); -name const & get_andthen_name(); name const & get_auto_param_name(); name const & get_bit0_name(); name const & get_bit1_name(); @@ -46,10 +44,8 @@ name const & get_decidable_name(); name const & get_decidable_to_bool_name(); name const & get_distrib_name(); name const & get_dite_name(); -name const & get_div_name(); name const & get_id_name(); name const & get_empty_name(); -name const & get_emptyc_name(); name const & get_Exists_name(); name const & get_eq_name(); name const & get_eq_cases_on_name(); @@ -84,20 +80,33 @@ name const & get_funext_name(); name const & get_ge_name(); name const & get_gt_name(); name const & get_has_add_name(); +name const & get_has_add_add_name(); +name const & get_has_andthen_andthen_name(); name const & get_has_bind_and_then_name(); name const & get_has_bind_bind_name(); name const & get_has_bind_seq_name(); name const & get_has_div_name(); +name const & get_has_div_div_name(); +name const & get_has_emptyc_emptyc_name(); +name const & get_has_mod_mod_name(); name const & get_has_mul_name(); +name const & get_has_mul_mul_name(); +name const & get_has_insert_insert_name(); name const & get_has_inv_name(); +name const & get_has_inv_inv_name(); name const & get_has_le_name(); +name const & get_has_le_le_name(); name const & get_has_lt_name(); +name const & get_has_lt_lt_name(); name const & get_has_neg_name(); +name const & get_has_neg_neg_name(); name const & get_has_one_name(); name const & get_has_one_one_name(); +name const & get_has_sep_sep_name(); name const & get_has_sizeof_name(); name const & get_has_sizeof_mk_name(); name const & get_has_sub_name(); +name const & get_has_sub_sub_name(); name const & get_has_to_format_name(); name const & get_has_to_string_name(); name const & get_has_zero_name(); @@ -129,7 +138,6 @@ name const & get_implies_of_if_neg_name(); name const & get_implies_of_if_pos_name(); name const & get_inductive_compiler_tactic_prove_nested_inj_name(); name const & get_inductive_compiler_tactic_prove_pack_inj_name(); -name const & get_insert_name(); name const & get_int_name(); name const & get_int_has_add_name(); name const & get_int_has_mul_name(); @@ -159,7 +167,6 @@ name const & get_int_zero_ne_neg_of_ne_name(); name const & get_int_decidable_linear_ordered_comm_group_name(); name const & get_interactive_param_desc_name(); name const & get_interactive_parse_name(); -name const & get_inv_name(); name const & get_io_name(); name const & get_io_interface_name(); name const & get_is_associative_name(); @@ -169,20 +176,16 @@ name const & get_is_commutative_comm_name(); name const & get_ite_name(); name const & get_left_distrib_name(); name const & get_left_comm_name(); -name const & get_le_name(); name const & get_le_refl_name(); name const & get_linear_ordered_ring_name(); name const & get_linear_ordered_semiring_name(); name const & get_list_name(); name const & get_list_nil_name(); name const & get_list_cons_name(); -name const & get_lt_name(); name const & get_match_failed_name(); -name const & get_mod_name(); name const & get_monad_name(); name const & get_monad_fail_name(); name const & get_monoid_name(); -name const & get_mul_name(); name const & get_mul_one_name(); name const & get_mul_zero_name(); name const & get_mul_zero_class_name(); @@ -224,7 +227,6 @@ name const & get_nat_one_lt_bit1_name(); name const & get_nat_le_of_lt_name(); name const & get_nat_le_refl_name(); name const & get_ne_name(); -name const & get_neg_name(); name const & get_neq_of_not_iff_name(); name const & get_norm_num_add1_name(); name const & get_norm_num_add1_bit0_name(); @@ -281,7 +283,6 @@ name const & get_num_pos_name(); name const & get_num_zero_name(); name const & get_of_eq_true_name(); name const & get_of_iff_true_name(); -name const & get_one_name(); name const & get_opt_param_name(); name const & get_or_name(); name const & get_orelse_name(); @@ -318,7 +319,6 @@ name const & get_right_distrib_name(); name const & get_ring_name(); name const & get_scope_trace_name(); name const & get_set_of_name(); -name const & get_sep_name(); name const & get_semiring_name(); name const & get_sigma_name(); name const & get_sigma_mk_name(); @@ -340,7 +340,6 @@ name const & get_string_empty_ne_str_name(); name const & get_string_str_ne_empty_name(); name const & get_string_str_ne_str_left_name(); name const & get_string_str_ne_str_right_name(); -name const & get_sub_name(); name const & get_subsingleton_name(); name const & get_subsingleton_elim_name(); name const & get_subsingleton_helim_name(); @@ -353,7 +352,6 @@ name const & get_psum_cases_on_name(); name const & get_psum_inl_name(); name const & get_psum_inr_name(); name const & get_tactic_name(); -name const & get_tactic_eval_expr_name(); name const & get_tactic_try_name(); name const & get_tactic_triv_name(); name const & get_thunk_name(); @@ -374,7 +372,6 @@ name const & get_vm_monitor_name(); name const & get_weak_order_name(); name const & get_well_founded_name(); name const & get_xor_name(); -name const & get_zero_name(); name const & get_zero_le_one_name(); name const & get_zero_lt_one_name(); name const & get_zero_mul_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index f146ce2fa7..b38c3b373e 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -1,7 +1,6 @@ abs absurd acc.cases_on -add add_comm_group add_comm_semigroup add_group @@ -12,7 +11,6 @@ and.elim_right and.intro and.rec and.cases_on -andthen auto_param bit0 bit1 @@ -39,10 +37,8 @@ decidable decidable.to_bool distrib dite -div id empty -emptyc Exists eq eq.cases_on @@ -77,20 +73,33 @@ funext ge gt has_add +has_add.add +has_andthen.andthen has_bind.and_then has_bind.bind has_bind.seq has_div +has_div.div +has_emptyc.emptyc +has_mod.mod has_mul +has_mul.mul +has_insert.insert has_inv +has_inv.inv has_le +has_le.le has_lt +has_lt.lt has_neg +has_neg.neg has_one has_one.one +has_sep.sep has_sizeof has_sizeof.mk has_sub +has_sub.sub has_to_format has_to_string has_zero @@ -122,7 +131,6 @@ implies_of_if_neg implies_of_if_pos inductive_compiler.tactic.prove_nested_inj inductive_compiler.tactic.prove_pack_inj -insert int int.has_add int.has_mul @@ -152,7 +160,6 @@ int.zero_ne_neg_of_ne int.decidable_linear_ordered_comm_group interactive.param_desc interactive.parse -inv io io.interface is_associative @@ -162,20 +169,16 @@ is_commutative.comm ite left_distrib left_comm -le le_refl linear_ordered_ring linear_ordered_semiring list list.nil list.cons -lt match_failed -mod monad monad_fail monoid -mul mul_one mul_zero mul_zero_class @@ -217,7 +220,6 @@ nat.one_lt_bit1 nat.le_of_lt nat.le_refl ne -neg neq_of_not_iff norm_num.add1 norm_num.add1_bit0 @@ -274,7 +276,6 @@ num.pos num.zero of_eq_true of_iff_true -one opt_param or orelse @@ -311,7 +312,6 @@ right_distrib ring scope_trace set_of -sep semiring sigma sigma.mk @@ -333,7 +333,6 @@ string.empty_ne_str string.str_ne_empty string.str_ne_str_left string.str_ne_str_right -sub subsingleton subsingleton.elim subsingleton.helim @@ -346,7 +345,6 @@ psum.cases_on psum.inl psum.inr tactic -tactic.eval_expr tactic.try tactic.triv thunk @@ -367,7 +365,6 @@ vm_monitor weak_order well_founded xor -zero zero_le_one zero_lt_one zero_mul diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 513727d55f..42e49de0ae 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -1448,7 +1448,7 @@ class add_nested_inductive_decl_fn { expr prove_by_simp(local_context const & lctx, expr const & thm, list Hs, bool use_sizeof) { environment env = set_reducible(m_env, get_sizeof_name(), reducible_status::Irreducible, false); - env = set_reducible(env, get_add_name(), reducible_status::Irreducible, false); + env = set_reducible(env, get_has_add_add_name(), reducible_status::Irreducible, false); type_context tctx(env, m_tctx.get_options(), lctx, transparency_mode::Semireducible); type_context tctx_whnf(env, m_tctx.get_options(), lctx, transparency_mode::None); diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp index cd42104a98..3fedbf9502 100644 --- a/src/library/norm_num.cpp +++ b/src/library/norm_num.cpp @@ -19,11 +19,11 @@ bool norm_num_context::is_nat_const(expr const & e) const { } bool norm_num_context::is_neg_app(expr const & e) const { - return is_const_app(e, get_neg_name(), 3); + return is_const_app(e, get_has_neg_neg_name(), 3); } bool norm_num_context::is_div(expr const & e) const { - return is_const_app(e, get_div_name(), 4); + return is_const_app(e, get_has_div_div_name(), 4); } expr norm_num_context::mk_const(name const & n) { @@ -325,10 +325,10 @@ expr norm_num_context::mk_norm_add_div(expr const & s_lhs, expr const & s_rhs, e expr norm_num_context::mk_nonzero_prf(expr const & e) { buffer args; expr f = get_app_args(e, args); - if (const_name(f) == get_neg_name()) { + if (const_name(f) == get_has_neg_neg_name()) { return mk_app({mk_const(get_norm_num_nonzero_of_neg_helper_name()), args[0], mk_lin_ord_ring(), args[2], mk_nonzero_prf(args[2])}); - } else if (const_name(f) == get_div_name()) { + } else if (const_name(f) == get_has_div_div_name()) { expr num_pr = mk_nonzero_prf(args[2]), den_pr = mk_nonzero_prf(args[3]); return mk_app({mk_const(get_norm_num_nonzero_of_div_helper_name()), args[0], mk_field(), args[2], args[3], num_pr, den_pr}); @@ -439,7 +439,7 @@ pair norm_num_context::mk_norm(expr const & e) { mpq val = mpq_of_expr(e); expr nval = mk_num(val); - if (const_name(f) == get_add_name() && args.size() == 4) { + if (const_name(f) == get_has_add_add_name() && args.size() == 4) { expr prf; auto lhs_p = mk_norm(args[2]); auto rhs_p = mk_norm(args[3]); @@ -466,7 +466,7 @@ pair norm_num_context::mk_norm(expr const & e) { lhs_p.first, rhs_p.first, nval, lhs_p.second, rhs_p.second, prf}); return pair(nval, rprf); - } else if (const_name(f) == get_sub_name() && args.size() == 4) { + } else if (const_name(f) == get_has_sub_sub_name() && args.size() == 4) { if (is_nat_const(args[0])) { return mk_norm_nat_sub(args[2], args[3]); } @@ -475,7 +475,7 @@ pair norm_num_context::mk_norm(expr const & e) { expr rprf = mk_app({mk_const(get_norm_num_subst_into_subtr_name()), type, mk_add_group(), args[2], args[3], anprf.first, anprf.second}); return expr_pair(nval, rprf); - } else if (const_name(f) == get_neg_name() && args.size() == 3) { + } else if (const_name(f) == get_has_neg_neg_name() && args.size() == 3) { auto prf = mk_norm(args[2]); lean_assert(mpq_of_expr(prf.first) == neg(val)); if (is_zero(prf.first)) { @@ -495,7 +495,7 @@ pair norm_num_context::mk_norm(expr const & e) { args[2], nval, prf.second}); return pair(nval, rprf); } - } else if (const_name(f) == get_mul_name() && args.size() == 4) { + } else if (const_name(f) == get_has_mul_mul_name() && args.size() == 4) { auto lhs_p = mk_norm(args[2]); auto rhs_p = mk_norm(args[3]); expr prf; @@ -521,7 +521,7 @@ pair norm_num_context::mk_norm(expr const & e) { expr rprf = mk_app({mk_const(get_norm_num_subst_into_prod_name()), type, mk_has_mul(), args[2], args[3], lhs_p.first, rhs_p.first, nval, lhs_p.second, rhs_p.second, prf}); return pair(nval, rprf); - } else if (const_name(f) == get_div_name() && args.size() == 4) { + } else if (const_name(f) == get_has_div_div_name() && args.size() == 4) { auto lhs_p = mk_norm(args[2]); auto rhs_p = mk_norm(args[3]); expr prf; @@ -565,7 +565,7 @@ pair norm_num_context::mk_norm(expr const & e) { auto rprf = mk_cong(mk_app(f, args[0], args[1], args[2]), type, args[3], nval_args[3], prf.second); return pair(nval, rprf); - } else if ((const_name(f) == get_zero_name() || const_name(f) == get_one_name()) + } else if ((const_name(f) == get_has_zero_zero_name() || const_name(f) == get_has_one_one_name()) && args.size() == 2) { return pair(e, mk_eq_refl(m_ctx, e)); } else { diff --git a/src/library/num.cpp b/src/library/num.cpp index f8443fea09..4be91bad6e 100644 --- a/src/library/num.cpp +++ b/src/library/num.cpp @@ -16,13 +16,13 @@ bool is_const_app(expr const & e, name const & n, unsigned nargs) { bool is_zero(expr const & e) { return - is_const_app(e, get_zero_name(), 2) || + is_const_app(e, get_has_zero_zero_name(), 2) || is_constant(e, get_nat_zero_name()); } bool is_one(expr const & e) { return - is_const_app(e, get_one_name(), 2) || + is_const_app(e, get_has_one_one_name(), 2) || (is_const_app(e, get_nat_succ_name(), 1) && is_zero(app_arg(e))); } @@ -39,7 +39,7 @@ optional is_bit1(expr const & e) { } optional is_neg(expr const & e) { - if (!is_const_app(e, get_neg_name(), 3)) + if (!is_const_app(e, get_has_neg_neg_name(), 3)) return none_expr(); return some_expr(app_arg(e)); } @@ -53,7 +53,7 @@ optional unfold_num_app(environment const & env, expr const & e) { } bool is_numeral_const_name(name const & n) { - return n == get_zero_name() || n == get_one_name() || n == get_bit0_name() || n == get_bit1_name(); + return n == get_has_zero_zero_name() || n == get_has_one_one_name() || n == get_bit0_name() || n == get_bit1_name(); } static bool is_num(expr const & e, bool first) { @@ -61,10 +61,12 @@ static bool is_num(expr const & e, bool first) { expr const & f = get_app_args(e, args); if (!is_constant(f)) return false; - if (const_name(f) == get_one_name()) + if (const_name(f) == get_has_one_one_name()) return args.size() == 2; - else if (const_name(f) == get_zero_name()) + else if (const_name(f) == get_has_zero_zero_name()) return first && args.size() == 2; + else if (const_name(f) == get_nat_zero_name()) + return first && args.size() == 0; else if (const_name(f) == get_bit0_name()) return args.size() == 3 && is_num(args[2], false); else if (const_name(f) == get_bit1_name()) @@ -131,8 +133,6 @@ optional to_num_core(expr const & e) { bool is_num_leaf_constant(name const & n) { return - n == get_zero_name() || - n == get_one_name() || n == get_has_zero_zero_name() || n == get_has_one_one_name(); } diff --git a/src/library/tactic/smt/ematch.cpp b/src/library/tactic/smt/ematch.cpp index 7371b7cc03..19cd23c6b0 100644 --- a/src/library/tactic/smt/ematch.cpp +++ b/src/library/tactic/smt/ematch.cpp @@ -1023,7 +1023,6 @@ public: void ematch_term(hinst_lemma const & lemma, expr const & t) { /* The following scope is a temporary workaround, we need to refactor this module and adapt all improvements added to type_context::is_def_eq. */ - type_context::transparency_scope scope(m_ctx, ensure_instances_mode(m_ctx.mode())); for (multi_pattern const & mp : lemma.m_multi_patterns) { ematch_term(lemma, mp, t); } @@ -1033,7 +1032,6 @@ public: void ematch_terms(hinst_lemma const & lemma, bool filter) { /* The following scope is a temporary workaround, we need to refactor this module and adapt all improvements added to type_context::is_def_eq. */ - type_context::transparency_scope scope(m_ctx, ensure_instances_mode(m_ctx.mode())); for (multi_pattern const & mp : lemma.m_multi_patterns) { ematch_terms(lemma, mp, filter); } @@ -1044,7 +1042,6 @@ public: return; /* The following scope is a temporary workaround, we need to refactor this module and adapt all improvements added to type_context::is_def_eq. */ - type_context::transparency_scope scope(m_ctx, ensure_instances_mode(m_ctx.mode())); ematch_using_lemmas(m_em_state.get_new_lemmas(), false); ematch_using_lemmas(m_em_state.get_lemmas(), true); m_em_state.m_lemmas.merge(m_em_state.m_new_lemmas); diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index 9438b41dca..fb1945983b 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -222,7 +222,8 @@ static simplify_fn mk_simp(type_context & ctx, defeq_can_state & dcs, smt_pre_co } static simp_result preprocess(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg, expr const & e) { - type_context::zeta_scope _1(ctx, cfg.m_zeta); + type_context::zeta_scope scope1(ctx, cfg.m_zeta); + type_context::transparency_scope scope2(ctx, transparency_mode::Reducible); dsimplify_fn dsimp = mk_dsimp(ctx, dcs, cfg); expr new_e = dsimp(e); simplify_fn simp = mk_simp(ctx, dcs, cfg); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 8b33c4922d..7e5f00dd74 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -2678,7 +2678,7 @@ bool type_context::on_is_def_eq_failure(expr const & e1, expr const & e2) { if (is_stuck(e1)) { expr new_e1 = try_to_unstuck_using_complete_instance(e1); if (new_e1 != e1) { - lean_trace(name({"type_context", "is_def_eq_detail"}), tout() << "synthesized instances on right\n";); + lean_trace(name({"type_context", "is_def_eq_detail"}), tout() << "synthesized instances on left\n";); return is_def_eq_core(new_e1, e2); } } @@ -2686,7 +2686,7 @@ bool type_context::on_is_def_eq_failure(expr const & e1, expr const & e2) { if (is_stuck(e2)) { expr new_e2 = try_to_unstuck_using_complete_instance(e2); if (new_e2 != e2) { - lean_trace(name({"type_context", "is_def_eq_detail"}), tout() << "synthesized instances on left\n";); + lean_trace(name({"type_context", "is_def_eq_detail"}), tout() << "synthesized instances on right\n";); return is_def_eq_core(e1, new_e2); } } @@ -2698,9 +2698,9 @@ bool type_context::on_is_def_eq_failure(expr const & e1, expr const & e2) { static optional eval_num(expr const & e) { if (is_constant(e, get_nat_zero_name())) { return some(mpz(0)); - } else if (is_app_of(e, get_zero_name(), 2)) { + } else if (is_app_of(e, get_has_zero_zero_name(), 2)) { return some(mpz(0)); - } else if (is_app_of(e, get_one_name(), 2)) { + } else if (is_app_of(e, get_has_one_one_name(), 2)) { return some(mpz(1)); } else if (auto a = is_bit0(e)) { if (auto r1 = eval_num(*a)) @@ -2717,13 +2717,13 @@ static optional eval_num(expr const & e) { return some(*r1 + 1); else return optional(); - } else if (is_app_of(e, get_add_name(), 4)) { + } else if (is_app_of(e, get_has_add_add_name(), 4)) { auto r1 = eval_num(app_arg(app_fn(e))); if (!r1) return optional(); auto r2 = eval_num(app_arg(e)); if (!r2) return optional(); return some(*r1 + *r2); - } else if (is_app_of(e, get_sub_name(), 4)) { + } else if (is_app_of(e, get_has_sub_sub_name(), 4)) { auto r1 = eval_num(app_arg(app_fn(e))); if (!r1) return optional(); auto r2 = eval_num(app_arg(e)); @@ -2748,9 +2748,9 @@ optional type_context::to_small_num(expr const & e) { /* If \c t is of the form (s + k) where k is a numeral, then return k. Otherwise, return none. */ optional type_context::is_offset_term (expr const & t) { - if (is_app_of(t, get_add_name(), 4) && - /* We do not consider (s + k) to be an offset term when add is marked as irreducible */ - m_cache->is_transparent(transparency_mode::Semireducible, get_add_name())) { + if (is_app_of(t, get_has_add_add_name(), 4) && + /* We do not consider (s + k) to be an offset term when has_add.add is marked as irreducible */ + get_reducible_status(env(), get_has_add_add_name()) != reducible_status::Irreducible) { expr const & k = app_arg(t); return to_small_num(k); } else { @@ -2769,7 +2769,7 @@ optional type_context::is_offset_term (expr const & t) { /* Return true iff t is of the form (t' + k) where k is a numeral */ static expr get_offset_term(expr const & t) { - if (is_app_of(t, get_add_name(), 4)) { + if (is_app_of(t, get_has_add_add_name(), 4)) { return app_arg(app_fn(t)); } else { lean_assert(is_app_of(t, get_nat_succ_name(), 1)); @@ -2786,7 +2786,7 @@ static expr get_offset_term(expr const & t) { static bool uses_nat_has_add_instance_or_succ(type_context & ctx, expr const & t) { if (is_app_of(t, get_nat_succ_name(), 1)) { return true; - } else if (is_app_of(t, get_add_name(), 4)) { + } else if (is_app_of(t, get_has_add_add_name(), 4)) { expr inst = app_arg(app_fn(app_fn(t))); if (is_constant(inst, get_nat_has_add_name())) return true; @@ -2813,7 +2813,7 @@ static expr update_offset(expr const & t, unsigned k) { r = mk_app(succ, r); return r; } else { - lean_assert(is_app_of(t, get_add_name(), 4)); + lean_assert(is_app_of(t, get_has_add_add_name(), 4)); return mk_app(app_fn(app_fn(t)), get_offset_term(t), to_nat_expr(mpz(k))); } } @@ -3004,7 +3004,7 @@ lbool type_context::is_def_eq_delta(expr const & t, expr const & s) { return l_undef; } -lbool type_context::is_def_eq_proj(expr const & t, expr const & s) { +lbool type_context::is_def_eq_proj(expr t, expr s) { projection_info const * t_proj = is_projection(t); projection_info const * s_proj = is_projection(s); if (t_proj && !s_proj) { @@ -3015,27 +3015,41 @@ lbool type_context::is_def_eq_proj(expr const & t, expr const & s) { if (auto s_n = reduce_projection_core(s_proj, s)) return to_lbool(is_def_eq_core_core(t, *s_n)); } else if (t_proj && s_proj) { + if (t_proj == s_proj) { + t = instantiate_mvars(t); + s = instantiate_mvars(s); + if (has_expr_metavar(t) || has_expr_metavar(s)) { + /* If is the same projection, and at least one of them contain unassigned metavariables, + then we try to unify arguments. + + Remark: this case is usually a bad idea if both + projections can be reduced. However, some + lemmas at init/algebra/order.lean cannot + be elaborated without it. + + A potential workaround (hack): if both structures + can be reduced, then we do it only if the structure + has only one field. + */ + scope S(*this); + if (is_def_eq_core(get_app_fn(t), get_app_fn(s)) && + is_def_eq_args(t, s) && + process_postponed(S)) { + S.commit(); + return l_true; + } + } + } auto t_n = reduce_projection_core(t_proj, t); auto s_n = reduce_projection_core(s_proj, s); if (t_n && s_n) { /* Both projections can be reduced */ return to_lbool(is_def_eq_core_core(*t_n, *s_n)); - } else if (t_proj == s_proj) { - /* If is the same projection and both cannot - be reduced, then we try to unify arguments */ - scope S(*this); - if (is_def_eq_core(get_app_fn(t), get_app_fn(s)) && - is_def_eq_args(t, s) && - process_postponed(S)) { - S.commit(); - return l_true; - } - } - /* If one of them could be reduced */ - if (t_n) + } else if (t_n) { return to_lbool(is_def_eq_core_core(*t_n, s)); - if (s_n) + } else if (s_n) { return to_lbool(is_def_eq_core_core(t, *s_n)); + } } return l_undef; } diff --git a/src/library/type_context.h b/src/library/type_context.h index 2e77adfb08..eb10ab327e 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -673,7 +673,7 @@ private: bool is_productive(expr const & e); expr reduce_if_productive(expr const & t); lbool is_def_eq_delta(expr const & t, expr const & s); - lbool is_def_eq_proj(expr const & t, expr const & s); + lbool is_def_eq_proj(expr t, expr s); optional> find_unsynth_metavar(expr const & e); bool mk_nested_instance(expr const & m, expr const & m_type); friend class unification_hint_fn; diff --git a/src/library/unification_hint.h b/src/library/unification_hint.h index fd5f33c155..2509e368db 100644 --- a/src/library/unification_hint.h +++ b/src/library/unification_hint.h @@ -21,9 +21,9 @@ structure unification_hint := (pattern : unification_constraint) (constraints : Example: definition both_zero_of_add_eq_zero [unify] (n₁ n₂ : ℕ) (s₁ : has_add ℕ) (s₂ : has_zero ℕ) : unification_hint := - unification_hint.mk (unification_constraint.mk (@add ℕ s₁ n₁ n₂) (@zero ℕ s₂)) - [unification_constraint.mk n₁ (@zero ℕ s₂), - unification_constraint.mk n₂ (@zero ℕ s₂)] + unification_hint.mk (unification_constraint.mk (@has_add.add ℕ s₁ n₁ n₂) (@has_zero.zero ℕ s₂)) + [unification_constraint.mk n₁ (@has_zero.zero ℕ s₂), + unification_constraint.mk n₂ (@has_zero.zero ℕ s₂)] creates the following unification hint: m_lhs: add nat #1 #3 #2 diff --git a/src/library/util.cpp b/src/library/util.cpp index 0cc2e275a5..c3336ebec7 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -514,11 +514,11 @@ static expr * g_nat_add_fn = nullptr; static void initialize_nat() { g_nat = new expr(mk_constant(get_nat_name())); - g_nat_zero = new expr(mk_app(mk_constant(get_zero_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_zero_name())})); - g_nat_one = new expr(mk_app(mk_constant(get_one_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_one_name())})); + g_nat_zero = new expr(mk_app(mk_constant(get_has_zero_zero_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_zero_name())})); + g_nat_one = new expr(mk_app(mk_constant(get_has_one_one_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_one_name())})); g_nat_bit0_fn = new expr(mk_app(mk_constant(get_bit0_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_add_name())})); g_nat_bit1_fn = new expr(mk_app(mk_constant(get_bit1_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_one_name()), mk_constant(get_nat_has_add_name())})); - g_nat_add_fn = new expr(mk_app(mk_constant(get_add_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_add_name())})); + g_nat_add_fn = new expr(mk_app(mk_constant(get_has_add_add_name(), {mk_level_zero()}), {*g_nat, mk_constant(get_nat_has_add_name())})); } static void finalize_nat() { diff --git a/tests/lean/coe4.lean.expected.out b/tests/lean/coe4.lean.expected.out index 67e5acf108..17b20e9476 100644 --- a/tests/lean/coe4.lean.expected.out +++ b/tests/lean/coe4.lean.expected.out @@ -1,5 +1,6 @@ ⇑f 0 1 : ℕ f 0 1 : ℕ ⇑f 0 1 : ℕ -@coe_fn.{1 1} (Functor.{0} nat) (coe_functor_to_fn.{0} nat) f (@zero.{0} nat nat.has_zero) (@one.{0} nat nat.has_one) : +@coe_fn.{1 1} (Functor.{0} nat) (coe_functor_to_fn.{0} nat) f (@has_zero.zero.{0} nat nat.has_zero) + (@has_one.one.{0} nat nat.has_one) : nat diff --git a/tests/lean/concrete_instance.lean.expected.out b/tests/lean/concrete_instance.lean.expected.out index f6e40c8e85..b0f7c8f2d4 100644 --- a/tests/lean/concrete_instance.lean.expected.out +++ b/tests/lean/concrete_instance.lean.expected.out @@ -1,4 +1,4 @@ -@mul.{0} nat nat.has_mul a b : nat -@add.{0} nat nat.has_add a b : nat -@mul.{0} nat nat.has_mul a b : nat -@add.{0} nat nat.has_add a b : nat +@has_mul.mul.{0} nat nat.has_mul a b : nat +@has_add.add.{0} nat nat.has_add a b : nat +@has_mul.mul.{0} nat nat.has_mul a b : nat +@has_add.add.{0} nat nat.has_add a b : nat diff --git a/tests/lean/defeq_simp1.lean b/tests/lean/defeq_simp1.lean index 8542b9ff63..9f921819c1 100644 --- a/tests/lean/defeq_simp1.lean +++ b/tests/lean/defeq_simp1.lean @@ -6,14 +6,14 @@ set_option pp.all true open tactic -example (a b : nat) (H : @add nat (id (id nat.has_add)) a b = @add nat nat_has_add2 a b) : true := +example (a b : nat) (H : @has_add.add nat (id (id nat.has_add)) a b = @has_add.add nat nat_has_add2 a b) : true := by do s ← simp_lemmas.mk_default, get_local `H >>= infer_type >>= s^.dsimplify >>= trace, constructor -example (a b : nat) (H : (λ x : nat, @add nat (id (id nat.has_add)) a b) = (λ x : nat, @add nat nat_has_add2 a x)) : true := +example (a b : nat) (H : (λ x : nat, @has_add.add nat (id (id nat.has_add)) a b) = (λ x : nat, @has_add.add nat nat_has_add2 a x)) : true := by do s ← simp_lemmas.mk_default, get_local `H >>= infer_type >>= s^.dsimplify >>= trace, diff --git a/tests/lean/defeq_simp1.lean.expected.out b/tests/lean/defeq_simp1.lean.expected.out index 97ddfa62d2..3b6864c668 100644 --- a/tests/lean/defeq_simp1.lean.expected.out +++ b/tests/lean/defeq_simp1.lean.expected.out @@ -1,5 +1,4 @@ -@eq.{1} nat (@add.{0} nat (@id.{1} (has_add.{0} nat) (@id.{1} (has_add.{0} nat) nat.has_add)) a b) - (@add.{0} nat nat_has_add2 a b) +@eq.{1} nat (@has_add.add.{0} nat (@id.{1} (has_add.{0} nat) (@id.{1} (has_add.{0} nat) nat.has_add)) a b) (nat.add a b) @eq.{1} (nat → nat) - (λ (x : nat), @add.{0} nat (@id.{1} (has_add.{0} nat) (@id.{1} (has_add.{0} nat) nat.has_add)) a b) - (@add.{0} nat nat_has_add2 a) + (λ (x : nat), @has_add.add.{0} nat (@id.{1} (has_add.{0} nat) (@id.{1} (has_add.{0} nat) nat.has_add)) a b) + (nat.add a) diff --git a/tests/lean/defeq_simp3.lean b/tests/lean/defeq_simp3.lean index 188622f426..9768789142 100644 --- a/tests/lean/defeq_simp3.lean +++ b/tests/lean/defeq_simp3.lean @@ -9,7 +9,7 @@ definition nat_has_add3 : nat → has_add nat := open tactic set_option pp.all true -example (a b : nat) (H : (λ x : nat, @add nat nat_has_add2 a x) = (λ x : nat, @add nat (nat_has_add3 x) a b)) : true := +example (a b : nat) (H : (λ x : nat, @has_add.add nat nat_has_add2 a x) = (λ x : nat, @has_add.add nat (nat_has_add3 x) a b)) : true := by do s ← simp_lemmas.mk_default, get_local `H >>= infer_type >>= s^.dsimplify >>= trace, diff --git a/tests/lean/defeq_simp3.lean.expected.out b/tests/lean/defeq_simp3.lean.expected.out index 49b8955d8f..b2c1d2fe82 100644 --- a/tests/lean/defeq_simp3.lean.expected.out +++ b/tests/lean/defeq_simp3.lean.expected.out @@ -1 +1 @@ -@eq.{1} (nat → nat) (@add.{0} nat nat_has_add2 a) (λ (x : nat), @add.{0} nat nat_has_add2 a b) +@eq.{1} (nat → nat) (@has_add.add.{0} nat nat.has_add a) (λ (x : nat), @has_add.add.{0} nat nat.has_add a b) diff --git a/tests/lean/defeq_simp4.lean b/tests/lean/defeq_simp4.lean index 948ac4bb46..59455d1a63 100644 --- a/tests/lean/defeq_simp4.lean +++ b/tests/lean/defeq_simp4.lean @@ -13,7 +13,7 @@ set_option pp.all true -- Remark: we can "fix" it by re-running defeq_simp until there is no change. -- However, this is too expensive. Well, if users want they can define their own defeq_simp that implements this -- behavior. -example (a b : nat) (H : (λ x : nat, @add nat (nat_has_add3 x) a b) = (λ x : nat, @add nat nat_has_add2 a x)) : true := +example (a b : nat) (H : (λ x : nat, @has_add.add nat (nat_has_add3 x) a b) = (λ x : nat, @has_add.add nat nat_has_add2 a x)) : true := by do s ← simp_lemmas.mk_default, get_local `H >>= infer_type >>= s^.dsimplify >>= trace, diff --git a/tests/lean/defeq_simp4.lean.expected.out b/tests/lean/defeq_simp4.lean.expected.out index 1bbe2832eb..dc01e3458a 100644 --- a/tests/lean/defeq_simp4.lean.expected.out +++ b/tests/lean/defeq_simp4.lean.expected.out @@ -1,3 +1,3 @@ -@eq.{1} (nat → nat) (λ (x : nat), @add.{0} nat (nat_has_add3 x) a b) (@add.{0} nat nat_has_add2 a) +@eq.{1} (nat → nat) (λ (x : nat), @has_add.add.{0} nat nat.has_add a b) (@has_add.add.{0} nat nat.has_add a) --------- -@eq.{1} (nat → nat) (λ (x : nat), @add.{0} nat nat_has_add2 a b) (@add.{0} nat nat_has_add2 a) +@eq.{1} (nat → nat) (λ (x : nat), @has_add.add.{0} nat nat.has_add a b) (@has_add.add.{0} nat nat.has_add a) diff --git a/tests/lean/defeq_simp5.lean b/tests/lean/defeq_simp5.lean index 5018144a5b..efde3736a1 100644 --- a/tests/lean/defeq_simp5.lean +++ b/tests/lean/defeq_simp5.lean @@ -13,8 +13,8 @@ set_option pp.all true -- This is a different issue. We can only make them work if we normalize (nat_has_add3 x) and (nat_has_add3 y). -- Again, the user can workaround it by manually normalizing these instances before invoking defeq_simp. example (a b : nat) - (H : (λ x y : nat, @add nat (nat_has_add3 x) a b) = - (λ x y : nat, @add nat (nat_has_add3 y) a x)) : true := + (H : (λ x y : nat, @has_add.add nat (nat_has_add3 x) a b) = + (λ x y : nat, @has_add.add nat (nat_has_add3 y) a x)) : true := by do s ← simp_lemmas.mk_default, get_local `H >>= infer_type >>= s^.dsimplify >>= trace, diff --git a/tests/lean/defeq_simp5.lean.expected.out b/tests/lean/defeq_simp5.lean.expected.out index 4e5b97244d..92d6111f52 100644 --- a/tests/lean/defeq_simp5.lean.expected.out +++ b/tests/lean/defeq_simp5.lean.expected.out @@ -1,2 +1,2 @@ -@eq.{1} (nat → nat → nat) (λ (x y : nat), @add.{0} nat (nat_has_add3 x) a b) - (λ (x y : nat), @add.{0} nat (nat_has_add3 y) a x) +@eq.{1} (nat → nat → nat) (λ (x y : nat), @has_add.add.{0} nat nat.has_add a b) + (λ (x y : nat), @has_add.add.{0} nat nat.has_add a x) diff --git a/tests/lean/elab1.lean b/tests/lean/elab1.lean index 1649dc47a6..5d356af7d5 100644 --- a/tests/lean/elab1.lean +++ b/tests/lean/elab1.lean @@ -1,12 +1,12 @@ definition foo.subst := @eq.subst definition boo.subst := @eq.subst -definition foo.add := @add -definition boo.add := @add +definition foo.add := @has_add.add +definition boo.add := @has_add.add set_option pp.all true -open foo boo +open foo boo has_add #print raw subst -- subst is overloaded #print raw add -- add is overloaded diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index 6cf6446eb4..ec6956041f 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -1,5 +1,5 @@ [choice boo.subst foo.subst] -[choice add boo.add foo.add] +[choice has_add.add boo.add foo.add] elab1.lean:13:7: error: invalid '@', function is overloaded, use fully qualified names (overloads: boo.subst, foo.subst) elab1.lean:15:7: error: invalid '@@', function is overloaded, use fully qualified names (overloads: boo.subst, foo.subst) elab1.lean:19:7: error: invalid overloaded application, elaborator has special support for 'eq.subst' (it is handled as an "eliminator"), but this kind of constant cannot be overloaded (solution: use fully qualified names) (overloads: eq.subst, boo.subst, foo.subst) diff --git a/tests/lean/elab2.lean.expected.out b/tests/lean/elab2.lean.expected.out index 22b1a70570..22431f4f8d 100644 --- a/tests/lean/elab2.lean.expected.out +++ b/tests/lean/elab2.lean.expected.out @@ -1,4 +1,4 @@ -@foo.{0 0} nat nat nat.has_add (@zero.{0} nat nat.has_zero) (@one.{0} nat nat.has_one) : nat +@foo.{0 0} nat nat nat.has_add (@has_zero.zero.{0} nat nat.has_zero) (@has_one.one.{0} nat nat.has_one) : nat elab2.lean:13:7: error: type mismatch at application @bla.{0 ?l_1} nat ?m_2 nat.zero bool.tt term @@ -7,4 +7,4 @@ has type bool but is expected to have type nat -@bla.{0 0} nat bool (@zero.{0} nat nat.has_zero) (@zero.{0} nat nat.has_zero) bool.tt : nat +@bla.{0 0} nat bool (@has_zero.zero.{0} nat nat.has_zero) (@has_zero.zero.{0} nat nat.has_zero) bool.tt : nat diff --git a/tests/lean/elab7.lean.expected.out b/tests/lean/elab7.lean.expected.out index 3fa85553fd..3d6bca78e1 100644 --- a/tests/lean/elab7.lean.expected.out +++ b/tests/lean/elab7.lean.expected.out @@ -1,5 +1,8 @@ -λ (x : nat), @add.{0} nat nat.has_add x (@one.{0} nat nat.has_one) : nat → nat -λ (x y : nat), @add.{0} nat nat.has_add x y : nat → nat → nat -λ (x y : nat), @add.{0} nat nat.has_add (@add.{0} nat nat.has_add x y) (@one.{0} nat nat.has_one) : nat → nat → nat -λ (x : nat), @list.cons.{0} nat (@add.{0} nat nat.has_add x (@one.{0} nat nat.has_one)) (@list.nil.{0} nat) : +λ (x : nat), @has_add.add.{0} nat nat.has_add x (@has_one.one.{0} nat nat.has_one) : nat → nat +λ (x y : nat), @has_add.add.{0} nat nat.has_add x y : nat → nat → nat +λ (x y : nat), + @has_add.add.{0} nat nat.has_add (@has_add.add.{0} nat nat.has_add x y) (@has_one.one.{0} nat nat.has_one) : + nat → nat → nat +λ (x : nat), + @list.cons.{0} nat (@has_add.add.{0} nat nat.has_add x (@has_one.one.{0} nat nat.has_one)) (@list.nil.{0} nat) : nat → list.{0} nat diff --git a/tests/lean/elab8.lean.expected.out b/tests/lean/elab8.lean.expected.out index 28b47a544f..f1c713835d 100644 --- a/tests/lean/elab8.lean.expected.out +++ b/tests/lean/elab8.lean.expected.out @@ -1,14 +1,14 @@ λ (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A] (a : A), - @add A _inst_1 a (@one A _inst_2) : + @has_add.add A _inst_1 a (@has_one.one A _inst_2) : Π (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A], A → A λ (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A] (a : A) -(H : @gt A _inst_3 a (@one A _inst_2)), @add A _inst_1 a (@one A _inst_2) : +(H : @gt A _inst_3 a (@has_one.one A _inst_2)), @has_add.add A _inst_1 a (@has_one.one A _inst_2) : Π (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A] (a : A), - @gt A _inst_3 a (@one A _inst_2) → A + @gt A _inst_3 a (@has_one.one A _inst_2) → A λ (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A] (a : A) -(H₁ : @gt A _inst_3 a (@one A _inst_2)) -(H₂ : @lt A _inst_3 a (@bit1 A _inst_2 _inst_1 (@bit0 A _inst_1 (@one A _inst_2)))), - @add A _inst_1 a (@one A _inst_2) : +(H₁ : @gt A _inst_3 a (@has_one.one A _inst_2)) +(H₂ : @has_lt.lt A _inst_3 a (@bit1 A _inst_2 _inst_1 (@bit0 A _inst_1 (@has_one.one A _inst_2)))), + @has_add.add A _inst_1 a (@has_one.one A _inst_2) : Π (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_one A] [_inst_3 : has_lt A] (a : A), - @gt A _inst_3 a (@one A _inst_2) → - @lt A _inst_3 a (@bit1 A _inst_2 _inst_1 (@bit0 A _inst_1 (@one A _inst_2))) → A + @gt A _inst_3 a (@has_one.one A _inst_2) → + @has_lt.lt A _inst_3 a (@bit1 A _inst_2 _inst_1 (@bit0 A _inst_1 (@has_one.one A _inst_2))) → A diff --git a/tests/lean/elab9.lean.expected.out b/tests/lean/elab9.lean.expected.out index 2135696e95..5a4b0acd8a 100644 --- a/tests/lean/elab9.lean.expected.out +++ b/tests/lean/elab9.lean.expected.out @@ -1,8 +1,10 @@ λ (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_zero A] (a : A) -(H : @eq A (@add A _inst_1 a (@zero A _inst_2)) a) [_inst_3 : has_add A] -(H : @eq A a (@add A _inst_3 (@zero A _inst_2) (@zero A _inst_2))), @add A _inst_3 a a : +(H : @eq A (@has_add.add A _inst_1 a (@has_zero.zero A _inst_2)) a) [_inst_3 : has_add A] +(H : @eq A a (@has_add.add A _inst_3 (@has_zero.zero A _inst_2) (@has_zero.zero A _inst_2))), + @has_add.add A _inst_3 a a : Π (A : Type u_1) [_inst_1 : has_add A] [_inst_2 : has_zero A] (a : A), - @eq A (@add A _inst_1 a (@zero A _inst_2)) a → - Π [_inst_3 : has_add A], @eq A a (@add A _inst_3 (@zero A _inst_2) (@zero A _inst_2)) → A -λ (a b : nat) (H : @gt nat nat.has_lt a b) [_inst_1 : has_lt nat], @lt nat _inst_1 a b : + @eq A (@has_add.add A _inst_1 a (@has_zero.zero A _inst_2)) a → + Π [_inst_3 : has_add A], + @eq A a (@has_add.add A _inst_3 (@has_zero.zero A _inst_2) (@has_zero.zero A _inst_2)) → A +λ (a b : nat) (H : @gt nat nat.has_lt a b) [_inst_1 : has_lt nat], @has_lt.lt nat _inst_1 a b : Π (a b : nat), @gt nat nat.has_lt a b → Π [_inst_1 : has_lt nat], Prop diff --git a/tests/lean/eta_tac.lean b/tests/lean/eta_tac.lean index 18dbc48d27..f603768d76 100644 --- a/tests/lean/eta_tac.lean +++ b/tests/lean/eta_tac.lean @@ -6,10 +6,10 @@ set_option pp.notation false example (a : nat) : true := by do - mk_const `add >>= head_eta_expand >>= trace, + mk_const `has_add.add >>= head_eta_expand >>= trace, mk_const `nat.succ >>= head_eta_expand >>= trace, - to_expr `(add a) >>= head_eta_expand >>= trace, - to_expr `(λ x : nat, add x) >>= head_eta_expand >>= trace, - to_expr `(λ x : nat, add x) >>= head_eta >>= trace, - to_expr `(add a) >>= head_eta_expand >>= head_eta >>= trace, + to_expr `(has_add.add a) >>= head_eta_expand >>= trace, + to_expr `(λ x : nat, has_add.add x) >>= head_eta_expand >>= trace, + to_expr `(λ x : nat, has_add.add x) >>= head_eta >>= trace, + to_expr `(has_add.add a) >>= head_eta_expand >>= head_eta >>= trace, constructor diff --git a/tests/lean/eta_tac.lean.expected.out b/tests/lean/eta_tac.lean.expected.out index 5f7a62fddb..bcffd2ac85 100644 --- a/tests/lean/eta_tac.lean.expected.out +++ b/tests/lean/eta_tac.lean.expected.out @@ -1,6 +1,6 @@ -λ {α : Type ?} [_inst_1 : has_add α] (a a_1 : α), @add α _inst_1 a a_1 +λ {α : Type ?} [c : has_add α] (a a_1 : α), @has_add.add α c a a_1 λ (a : nat), nat.succ a -λ (a_1 : nat), @add nat nat.has_add a a_1 -λ (x a : nat), @add nat nat.has_add x a -@add nat nat.has_add -@add nat nat.has_add a +λ (a_1 : nat), @has_add.add nat nat.has_add a a_1 +λ (x a : nat), @has_add.add nat nat.has_add x a +@has_add.add nat nat.has_add +@has_add.add nat nat.has_add a diff --git a/tests/lean/generalize1.lean b/tests/lean/generalize1.lean index d615af2c19..98b189ca50 100644 --- a/tests/lean/generalize1.lean +++ b/tests/lean/generalize1.lean @@ -1,6 +1,6 @@ open tactic -add_key_equivalence add nat.succ +add_key_equivalence has_add.add nat.succ set_option pp.binder_types true diff --git a/tests/lean/hinst_lemmas1.lean.expected.out b/tests/lean/hinst_lemmas1.lean.expected.out index 99b51bef21..150c1bd7bc 100644 --- a/tests/lean/hinst_lemmas1.lean.expected.out +++ b/tests/lean/hinst_lemmas1.lean.expected.out @@ -1,3 +1,3 @@ -{[foo1, patterns: {{?x_0 < ?x_1, ?x_1 < ?x_2}}], - [foo2, patterns: {{?x_1 > ?x_0, ?x_1 < ?x_2}}], +{[foo2, patterns: {{?x_1 < ?x_2, ?x_1 > ?x_0}}], + [foo1, patterns: {{?x_1 < ?x_2, ?x_0 < ?x_1}}], [foo3, patterns: {{?x_0 < ?x_1, ?x_1 < ?x_2 + ?x_2}}]} diff --git a/tests/lean/interactive/info.lean.expected.out b/tests/lean/interactive/info.lean.expected.out index 25037c8633..a280a6d661 100644 --- a/tests/lean/interactive/info.lean.expected.out +++ b/tests/lean/interactive/info.lean.expected.out @@ -5,5 +5,5 @@ {"record":{"full-id":"bool.tt","source":,"type":"bool"},"response":"ok","seq_num":7} {"record":{"doc":"(trace) enable/disable tracing for the given module and submodules"},"response":"ok","seq_num":10} {"record":{"full-id":"list.cons","source":,"type":"Π {T : Type}, T → list T → list T"},"response":"ok","seq_num":13} -{"record":{"full-id":"append","source":,"type":"Π {α : Type} [_inst_1 : has_append α], α → α → α"},"response":"ok","seq_num":16} +{"record":{"full-id":"has_append.append","source":,"type":"Π {α : Type} [c : has_append α], α → α → α"},"response":"ok","seq_num":16} {"record":{"full-id":"id","source":,"type":"Π {α : Sort u}, α → α"},"response":"ok","seq_num":19} diff --git a/tests/lean/key_eqv1.lean b/tests/lean/key_eqv1.lean index f46d0607d3..8c60664b69 100644 --- a/tests/lean/key_eqv1.lean +++ b/tests/lean/key_eqv1.lean @@ -1,4 +1,4 @@ -add_key_equivalence add nat.add +add_key_equivalence has_add.add nat.add add_key_equivalence nat.add nat.succ -add_key_equivalence mul nat.mul +add_key_equivalence has_mul.mul nat.mul #print key_equivalences diff --git a/tests/lean/key_eqv1.lean.expected.out b/tests/lean/key_eqv1.lean.expected.out index 0ecffff206..38622d442a 100644 --- a/tests/lean/key_eqv1.lean.expected.out +++ b/tests/lean/key_eqv1.lean.expected.out @@ -1,2 +1,2 @@ -[nat.succ, nat.add, add] -[nat.mul, mul] +[has_mul.mul, nat.mul] +[has_add.add, nat.succ, nat.add] diff --git a/tests/lean/macro_args.lean b/tests/lean/macro_args.lean index 7532724c6c..6122111b04 100644 --- a/tests/lean/macro_args.lean +++ b/tests/lean/macro_args.lean @@ -1 +1 @@ -#eval ``({pos . line := zero, col := 1}).to_raw_expr.to_raw_fmt +#eval ``({pos . line := has_zero.zero, col := 1}).to_raw_expr.to_raw_fmt diff --git a/tests/lean/macro_args.lean.expected.out b/tests/lean/macro_args.lean.expected.out index 10bbc77be7..24a5051531 100644 --- a/tests/lean/macro_args.lean.expected.out +++ b/tests/lean/macro_args.lean.expected.out @@ -1 +1 @@ -[macro structure instance (const zero []) [macro prenum]] +[macro structure instance (const has_zero.zero []) [macro prenum]] diff --git a/tests/lean/notation7.lean.expected.out b/tests/lean/notation7.lean.expected.out index 1e7601c26f..1f9c26bed0 100644 --- a/tests/lean/notation7.lean.expected.out +++ b/tests/lean/notation7.lean.expected.out @@ -1,2 +1,2 @@ g 0:+1:+1 (1:+1 + 2:+1):+1 : num -g (f (f 0)) (f (add (f 1) (f 2))) : num +g (f (f 0)) (f (has_add.add (f 1) (f 2))) : num diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out index a5f0858fb0..588ab71b51 100644 --- a/tests/lean/pp_all.lean.expected.out +++ b/tests/lean/pp_all.lean.expected.out @@ -1,5 +1,5 @@ (λ (x : ℕ), x) a + of_num b = 10 : Prop -@eq.{1} nat (@add.{0} nat nat.has_add ((λ (x : nat), x) a) (nat.of_num b)) +@eq.{1} nat (@has_add.add.{0} nat nat.has_add ((λ (x : nat), x) a) (nat.of_num b)) (@bit0.{0} nat nat.has_add - (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@one.{0} nat nat.has_one)))) : + (@bit1.{0} nat nat.has_one nat.has_add (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)))) : Prop diff --git a/tests/lean/pp_all2.lean.expected.out b/tests/lean/pp_all2.lean.expected.out index 510a3c261f..faf01ba0e8 100644 --- a/tests/lean/pp_all2.lean.expected.out +++ b/tests/lean/pp_all2.lean.expected.out @@ -1 +1 @@ -@add nat nat.has_add 10 3 : nat +@has_add.add nat nat.has_add 10 3 : nat diff --git a/tests/lean/pp_zero_bug.lean b/tests/lean/pp_zero_bug.lean index 66ecd1b97e..11803d963a 100644 --- a/tests/lean/pp_zero_bug.lean +++ b/tests/lean/pp_zero_bug.lean @@ -1,2 +1,2 @@ -#check @zero -#check @zero nat +#check @has_zero.zero +#check @has_zero.zero nat diff --git a/tests/lean/pp_zero_bug.lean.expected.out b/tests/lean/pp_zero_bug.lean.expected.out index 6465f44887..276583b1b2 100644 --- a/tests/lean/pp_zero_bug.lean.expected.out +++ b/tests/lean/pp_zero_bug.lean.expected.out @@ -1,2 +1,2 @@ -zero : Π {α : Type u_1} [_inst_1 : has_zero α], α -zero : Π [_inst_1 : has_zero ℕ], ℕ +has_zero.zero : Π (α : Type u_1) [c : has_zero α], α +has_zero.zero ℕ : Π [c : has_zero ℕ], ℕ diff --git a/tests/lean/qexpr1.lean.expected.out b/tests/lean/qexpr1.lean.expected.out index 511f1dce56..b2ff64940c 100644 --- a/tests/lean/qexpr1.lean.expected.out +++ b/tests/lean/qexpr1.lean.expected.out @@ -1,4 +1,4 @@ -@add.{0} nat nat.has_add a b +@has_add.add.{0} nat nat.has_add a b nat -@add.{0} nat nat.has_add (nat.succ a) b +@has_add.add.{0} nat nat.has_add (nat.succ a) b nat diff --git a/tests/lean/qexpr2.lean.expected.out b/tests/lean/qexpr2.lean.expected.out index 35daf4eb99..f2e3070268 100644 --- a/tests/lean/qexpr2.lean.expected.out +++ b/tests/lean/qexpr2.lean.expected.out @@ -1,4 +1,4 @@ -@add.{0} nat nat.has_add ?m_1 b +@has_add.add.{0} nat nat.has_add ?m_1 b nat ------ after instantiate_mvars -@add.{0} nat nat.has_add c b +@has_add.add.{0} nat nat.has_add c b diff --git a/tests/lean/rquote.lean b/tests/lean/rquote.lean index caa0dc41ed..813d20fcdc 100644 --- a/tests/lean/rquote.lean +++ b/tests/lean/rquote.lean @@ -17,7 +17,7 @@ open foo boo open nat -#check ``add +#check ``has_add.add #check ``gcd diff --git a/tests/lean/rquote.lean.expected.out b/tests/lean/rquote.lean.expected.out index 948ebe9b2c..054041658f 100644 --- a/tests/lean/rquote.lean.expected.out +++ b/tests/lean/rquote.lean.expected.out @@ -1,6 +1,6 @@ rquote.lean:14: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.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 diff --git a/tests/lean/run/1468.lean b/tests/lean/run/1468.lean deleted file mode 100644 index a824a40cb1..0000000000 --- a/tests/lean/run/1468.lean +++ /dev/null @@ -1,17 +0,0 @@ -local infix * := _root_.mul - -namespace Y -def mul : bool → bool := λ b, b - -example (m n : ℕ) : true := -begin -definev k : ℕ := m * n, -definev a : bool := mul tt, -trivial -end -end Y - - -meta def is_mul : expr → option (expr × expr) -| ```(%%a * %%b) := some (a, b) -| _ := none diff --git a/tests/lean/run/app_builder_tac1.lean b/tests/lean/run/app_builder_tac1.lean index dc411567b0..9e54fbc0d1 100644 --- a/tests/lean/run/app_builder_tac1.lean +++ b/tests/lean/run/app_builder_tac1.lean @@ -9,9 +9,9 @@ mk_mapp `ite [some c, none, none, some a, some b] example (a b : nat) : nat := by do a ← get_local `a, b ← get_local `b, - mk_app `add [a, b] >>= trace, - mk_app `mul [a, b] >>= trace, - mk_app `sub [a, b] >>= trace, + mk_app `has_add.add [a, b] >>= trace, + mk_app `has_mul.mul [a, b] >>= trace, + mk_app `has_sub.sub [a, b] >>= trace, c ← mk_app `eq [a, b], trace c, mk_ite c a b >>= trace, diff --git a/tests/lean/run/at_at_bug.lean b/tests/lean/run/at_at_bug.lean index f27860ec1c..4ef55d5bc6 100644 --- a/tests/lean/run/at_at_bug.lean +++ b/tests/lean/run/at_at_bug.lean @@ -1,11 +1,10 @@ - example (a b : nat) (p : nat → nat → Prop) (h₁ : p a b) (h₂ : a = b) : p b b := @@eq.subst (λ x, p x b) h₂ h₁ set_option pp.all true variable my_has_add : has_add nat -#check @@add my_has_add 0 1 +#check @@has_add.add my_has_add 0 1 local notation h1 `▸[` m `]` h2 := @@eq.subst m h1 h2 diff --git a/tests/lean/run/auto_param_in_structures.lean b/tests/lean/run/auto_param_in_structures.lean index 18ad7c664c..cfd9298129 100644 --- a/tests/lean/run/auto_param_in_structures.lean +++ b/tests/lean/run/auto_param_in_structures.lean @@ -7,19 +7,19 @@ structure monoid (α : Type) := (assoc : ∀ a b c, op (op a b) c = op a (op b c) . my_tac) def m1 : monoid nat := -monoid.mk add +monoid.mk (+) def m2 : monoid nat := -monoid.mk mul +monoid.mk (*) #print m1 #print m2 def m3 : monoid nat := -{op := add} +{op := (+)} def m4 : monoid nat := -{op := mul} +{op := (*)} #print m3 #print m4 diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index e80d165dda..e547f1c9d9 100644 --- a/tests/lean/run/check_constants.lean +++ b/tests/lean/run/check_constants.lean @@ -6,7 +6,6 @@ do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) run_cmd script_check_id `abs run_cmd script_check_id `absurd run_cmd script_check_id `acc.cases_on -run_cmd script_check_id `add run_cmd script_check_id `add_comm_group run_cmd script_check_id `add_comm_semigroup run_cmd script_check_id `add_group @@ -17,7 +16,6 @@ run_cmd script_check_id `and.elim_right run_cmd script_check_id `and.intro run_cmd script_check_id `and.rec run_cmd script_check_id `and.cases_on -run_cmd script_check_id `andthen run_cmd script_check_id `auto_param run_cmd script_check_id `bit0 run_cmd script_check_id `bit1 @@ -44,10 +42,8 @@ run_cmd script_check_id `decidable run_cmd script_check_id `decidable.to_bool run_cmd script_check_id `distrib run_cmd script_check_id `dite -run_cmd script_check_id `div run_cmd script_check_id `id run_cmd script_check_id `empty -run_cmd script_check_id `emptyc run_cmd script_check_id `Exists run_cmd script_check_id `eq run_cmd script_check_id `eq.cases_on @@ -82,20 +78,33 @@ run_cmd script_check_id `funext run_cmd script_check_id `ge run_cmd script_check_id `gt run_cmd script_check_id `has_add +run_cmd script_check_id `has_add.add +run_cmd script_check_id `has_andthen.andthen run_cmd script_check_id `has_bind.and_then run_cmd script_check_id `has_bind.bind run_cmd script_check_id `has_bind.seq run_cmd script_check_id `has_div +run_cmd script_check_id `has_div.div +run_cmd script_check_id `has_emptyc.emptyc +run_cmd script_check_id `has_mod.mod run_cmd script_check_id `has_mul +run_cmd script_check_id `has_mul.mul +run_cmd script_check_id `has_insert.insert run_cmd script_check_id `has_inv +run_cmd script_check_id `has_inv.inv run_cmd script_check_id `has_le +run_cmd script_check_id `has_le.le run_cmd script_check_id `has_lt +run_cmd script_check_id `has_lt.lt run_cmd script_check_id `has_neg +run_cmd script_check_id `has_neg.neg run_cmd script_check_id `has_one run_cmd script_check_id `has_one.one +run_cmd script_check_id `has_sep.sep run_cmd script_check_id `has_sizeof run_cmd script_check_id `has_sizeof.mk run_cmd script_check_id `has_sub +run_cmd script_check_id `has_sub.sub run_cmd script_check_id `has_to_format run_cmd script_check_id `has_to_string run_cmd script_check_id `has_zero @@ -127,7 +136,6 @@ run_cmd script_check_id `implies_of_if_neg run_cmd script_check_id `implies_of_if_pos run_cmd script_check_id `inductive_compiler.tactic.prove_nested_inj run_cmd script_check_id `inductive_compiler.tactic.prove_pack_inj -run_cmd script_check_id `insert run_cmd script_check_id `int run_cmd script_check_id `int.has_add run_cmd script_check_id `int.has_mul @@ -157,7 +165,6 @@ run_cmd script_check_id `int.zero_ne_neg_of_ne run_cmd script_check_id `int.decidable_linear_ordered_comm_group run_cmd script_check_id `interactive.param_desc run_cmd script_check_id `interactive.parse -run_cmd script_check_id `inv run_cmd script_check_id `io run_cmd script_check_id `io.interface run_cmd script_check_id `is_associative @@ -167,20 +174,16 @@ run_cmd script_check_id `is_commutative.comm run_cmd script_check_id `ite run_cmd script_check_id `left_distrib run_cmd script_check_id `left_comm -run_cmd script_check_id `le run_cmd script_check_id `le_refl run_cmd script_check_id `linear_ordered_ring run_cmd script_check_id `linear_ordered_semiring run_cmd script_check_id `list run_cmd script_check_id `list.nil run_cmd script_check_id `list.cons -run_cmd script_check_id `lt run_cmd script_check_id `match_failed -run_cmd script_check_id `mod run_cmd script_check_id `monad run_cmd script_check_id `monad_fail run_cmd script_check_id `monoid -run_cmd script_check_id `mul run_cmd script_check_id `mul_one run_cmd script_check_id `mul_zero run_cmd script_check_id `mul_zero_class @@ -222,7 +225,6 @@ run_cmd script_check_id `nat.one_lt_bit1 run_cmd script_check_id `nat.le_of_lt run_cmd script_check_id `nat.le_refl run_cmd script_check_id `ne -run_cmd script_check_id `neg run_cmd script_check_id `neq_of_not_iff run_cmd script_check_id `norm_num.add1 run_cmd script_check_id `norm_num.add1_bit0 @@ -279,7 +281,6 @@ run_cmd script_check_id `num.pos run_cmd script_check_id `num.zero run_cmd script_check_id `of_eq_true run_cmd script_check_id `of_iff_true -run_cmd script_check_id `one run_cmd script_check_id `opt_param run_cmd script_check_id `or run_cmd script_check_id `orelse @@ -316,7 +317,6 @@ run_cmd script_check_id `right_distrib run_cmd script_check_id `ring run_cmd script_check_id `scope_trace run_cmd script_check_id `set_of -run_cmd script_check_id `sep run_cmd script_check_id `semiring run_cmd script_check_id `sigma run_cmd script_check_id `sigma.mk @@ -338,7 +338,6 @@ run_cmd script_check_id `string.empty_ne_str run_cmd script_check_id `string.str_ne_empty run_cmd script_check_id `string.str_ne_str_left run_cmd script_check_id `string.str_ne_str_right -run_cmd script_check_id `sub run_cmd script_check_id `subsingleton run_cmd script_check_id `subsingleton.elim run_cmd script_check_id `subsingleton.helim @@ -351,7 +350,6 @@ run_cmd script_check_id `psum.cases_on run_cmd script_check_id `psum.inl run_cmd script_check_id `psum.inr run_cmd script_check_id `tactic -run_cmd script_check_id `tactic.eval_expr run_cmd script_check_id `tactic.try run_cmd script_check_id `tactic.triv run_cmd script_check_id `thunk @@ -372,7 +370,6 @@ run_cmd script_check_id `vm_monitor run_cmd script_check_id `weak_order run_cmd script_check_id `well_founded run_cmd script_check_id `xor -run_cmd script_check_id `zero run_cmd script_check_id `zero_le_one run_cmd script_check_id `zero_lt_one run_cmd script_check_id `zero_mul diff --git a/tests/lean/run/cpdt3.lean b/tests/lean/run/cpdt3.lean index acc9e95afe..2194a17581 100644 --- a/tests/lean/run/cpdt3.lean +++ b/tests/lean/run/cpdt3.lean @@ -17,8 +17,8 @@ inductive exp : Type open exp def binop_denote : binop → nat → nat → nat -| Plus := add -| Times := mul +| Plus := (+) +| Times := (*) def exp_denote : exp → nat | (Const n) := n @@ -98,8 +98,8 @@ def leb (m n : ℕ) : bool := if m < n then tt else ff def tbinop_denote : Π {arg1 arg2 res : type}, tbinop arg1 arg2 res → type_denote arg1 → type_denote arg2 → type_denote res -| ._ ._ ._ TPlus := (add : ℕ → ℕ → ℕ) -| ._ ._ ._ TTimes := (mul : ℕ → ℕ → ℕ) +| ._ ._ ._ TPlus := ((+) : ℕ → ℕ → ℕ) +| ._ ._ ._ TTimes := ((*) : ℕ → ℕ → ℕ) | ._ ._ ._ (TEq Nat) := beq_nat | ._ ._ ._ (TEq Bool) := eqb | ._ ._ ._ TLt := leb diff --git a/tests/lean/run/decl_olean.lean b/tests/lean/run/decl_olean.lean index b26c2c3b18..a9de718650 100644 --- a/tests/lean/run/decl_olean.lean +++ b/tests/lean/run/decl_olean.lean @@ -9,7 +9,6 @@ do env ← get_env, olean ← returnopt (env^.decl_olean n) <|> return "current file", trace $ to_string n ++ " was defined at " ++ olean ++ " : " ++ to_string pos.1 ++ ":" ++ to_string pos.2 -run_cmd show_pos `add run_cmd show_pos `nat.succ run_cmd show_pos `subsingleton.intro run_cmd show_pos `subsingleton.rec diff --git a/tests/lean/run/dep_coe_to_fn3.lean b/tests/lean/run/dep_coe_to_fn3.lean index 0b2b320eab..46c39be0e3 100644 --- a/tests/lean/run/dep_coe_to_fn3.lean +++ b/tests/lean/run/dep_coe_to_fn3.lean @@ -13,7 +13,9 @@ variables (f : Func) (a : f^.A) (b : f^.B a) def f1 : Func := { A := nat, B := λ a, nat, - fn := add } + fn := (+) } + +-- set_option trace.type_context.is_def_eq_detail true /- We need to mark 10 as a nat. Reason: f1 is not reducible, then type class resolution @@ -21,6 +23,9 @@ def f1 : Func := example : f1 (10:nat) (30:nat) = (50:nat) := rfl +/- +#exit + attribute [reducible] f1 example : f1 10 30 = 50 := @@ -28,3 +33,4 @@ rfl example (n m : nat) : f1 n m = n + (n + m) := rfl +-/ diff --git a/tests/lean/run/destruct.lean b/tests/lean/run/destruct.lean index 0448a9cca3..1763337ec3 100644 --- a/tests/lean/run/destruct.lean +++ b/tests/lean/run/destruct.lean @@ -16,7 +16,7 @@ axiom fax2 {α : Type u} {n : nat} (v : Vec α (nat.succ n)) : f v = 1 example {α : Type u} {n : nat} (v : Vec α n) : f v ≠ 2 := begin destruct v, - intros, intro, note h := fax1 α, cc, + {intros, intro, note h := fax1 α, cc}, intros n1 h t, intros, intro, note h := fax2 (Vec.cons h t), cc end diff --git a/tests/lean/run/dunfold3.lean b/tests/lean/run/dunfold3.lean index c7699e2700..3684d94daa 100644 --- a/tests/lean/run/dunfold3.lean +++ b/tests/lean/run/dunfold3.lean @@ -6,7 +6,7 @@ example (a b : nat) (p : nat → Prop) (h : p (g (nat.succ (nat.succ a)))) : p ( begin unfold g at h, do { h ← get_local `h >>= infer_type, t ← to_expr `(p (nat.succ (nat.succ a) + 5)), guard (h = t) }, - unfold add has_add.add bit0 one nat.add, + unfold has_add.add bit0 has_one.one nat.add, unfold g, do { t ← target, h ← get_local `h >>= infer_type, guard (t = h) }, assumption diff --git a/tests/lean/run/list_notation.lean b/tests/lean/run/list_notation.lean index f8447b0794..6917236d74 100644 --- a/tests/lean/run/list_notation.lean +++ b/tests/lean/run/list_notation.lean @@ -20,7 +20,7 @@ open nat #eval [1, 2, 3] ∩ [3, 4, 1, 5] -#eval (mul 10) <$> [1, 2, 3] +#eval (*10) <$> [1, 2, 3] #check ({1, 2, 3} : list nat) diff --git a/tests/lean/run/listex.lean b/tests/lean/run/listex.lean index c1d84de8c6..53cd5f4fae 100644 --- a/tests/lean/run/listex.lean +++ b/tests/lean/run/listex.lean @@ -9,19 +9,19 @@ open expr tactic meta def search_mem_list : expr → expr → tactic expr | a e := -(do m ← mk_app `mem [a, e], find_assumption m) +(do m ← mk_app ``has_mem.mem [a, e], find_assumption m) <|> -(do [_, _, l, r] ← match_app_of e `append | failed, h ← search_mem_list a l, mk_app `in_left [l, r, h]) +(do [_, _, l, r] ← match_app_of e ``has_append.append | failed, h ← search_mem_list a l, mk_app `in_left [l, r, h]) <|> -(do [_, _, l, r] ← match_app_of e `append | failed, h ← search_mem_list a r, mk_app `in_right [l, r, h]) +(do [_, _, l, r] ← match_app_of e ``has_append.append | failed, h ← search_mem_list a r, mk_app `in_right [l, r, h]) <|> -(do [_, b, t] ← match_app_of e `list.cons | failed, is_def_eq a b, mk_app `in_head [b, t]) +(do [_, b, t] ← match_app_of e ``list.cons | failed, is_def_eq a b, mk_app `in_head [b, t]) <|> -(do [_, b, t] ← match_app_of e `list.cons | failed, h ← search_mem_list a t, mk_app `in_tail [a, b, t, h]) +(do [_, b, t] ← match_app_of e ``list.cons | failed, h ← search_mem_list a t, mk_app `in_tail [a, b, t, h]) meta def mk_mem_list : tactic unit := do t ← target, - [_, _, _, a, e] ← match_app_of t `mem | failed, + [_, _, _, a, e] ← match_app_of t ``has_mem.mem | failed, search_mem_list a e >>= exact example (a b c : nat) : a ∈ [b, c] ++ [b, a, b] := diff --git a/tests/lean/run/listex2.lean b/tests/lean/run/listex2.lean index 6782457ea8..e8b7e38be8 100644 --- a/tests/lean/run/listex2.lean +++ b/tests/lean/run/listex2.lean @@ -12,13 +12,13 @@ open expr tactic declare_trace search_mem_list meta def match_append (e : expr) : tactic (expr × expr) := -do [_, _, l, r] ← match_app_of e `append | failed, return (l, r) +do [_, _, l, r] ← match_app_of e ``has_append.append | failed, return (l, r) meta def match_cons (e : expr) : tactic (expr × expr) := -do [_, a, t] ← match_app_of e `list.cons | failed, return (a, t) +do [_, a, t] ← match_app_of e ``list.cons | failed, return (a, t) meta def match_mem (e : expr) : tactic (expr × expr) := -do [_, _, _, a, t] ← match_app_of e `mem | failed, return (a, t) +do [_, _, _, a, t] ← match_app_of e ``has_mem.mem | failed, return (a, t) meta def search_mem_list : expr → expr → tactic expr | a e := when_tracing `search_mem_list (do f₁ ← pp a, f₂ ← pp e, trace (to_fmt "search " ++ f₁ ++ to_fmt " in " ++ f₂)) >> diff --git a/tests/lean/run/quote1.lean b/tests/lean/run/quote1.lean index d13b11bf40..655606efbb 100644 --- a/tests/lean/run/quote1.lean +++ b/tests/lean/run/quote1.lean @@ -6,7 +6,7 @@ meta definition foo (a : pexpr) : pexpr := example (a b : nat) : a = a := by do a ← get_local `a, - t1 ← mk_app `add [a, a], + t1 ← mk_app ``has_add.add [a, a], t2 ← to_expr (foo (to_pexpr t1)), trace t2, r ← mk_app (`eq.refl) [a], diff --git a/tests/lean/run/shadow1.lean b/tests/lean/run/shadow1.lean index c38fba1b77..1afec52a8a 100644 --- a/tests/lean/run/shadow1.lean +++ b/tests/lean/run/shadow1.lean @@ -19,7 +19,7 @@ definition h (a : nat) : nat → nat example (a b : nat) : h a b = b := rfl -definition o : nat := zero +definition o : nat := 0 definition f2 : nat → nat | o := 0 @@ -27,7 +27,7 @@ definition f2 : nat → nat example (a : nat) : f2 a = 0 := rfl definition f3 : nat → nat -| (add a 1) := a +| (a+1) := a | nat.zero := nat.zero example : f3 10 = 9 := rfl diff --git a/tests/lean/run/super_examples.lean b/tests/lean/run/super_examples.lean index 28e224381a..130446d8a3 100644 --- a/tests/lean/run/super_examples.lean +++ b/tests/lean/run/super_examples.lean @@ -4,9 +4,9 @@ open tactic constant nat_has_dvd : has_dvd nat attribute [instance] nat_has_dvd -noncomputable def prime (n : ℕ) := ∀d, dvd d n → d = 1 ∨ d = n -axiom dvd_refl (m : ℕ) : dvd m m -axiom dvd_mul (m n k : ℕ) : dvd m n → dvd m (n*k) +noncomputable def prime (n : ℕ) := ∀d, d ∣ n → d = 1 ∨ d = n +axiom dvd_refl (m : ℕ) : m ∣ m +axiom dvd_mul (m n k : ℕ) : m ∣ n → m ∣ (n*k) axiom nat_mul_cancel_one (m n : ℕ) : m = m * n → n = 1 diff --git a/tests/lean/run/type_equations.lean b/tests/lean/run/type_equations.lean index 6e3e0b80b8..df88a94762 100644 --- a/tests/lean/run/type_equations.lean +++ b/tests/lean/run/type_equations.lean @@ -32,7 +32,7 @@ set_option pp.notation false definition ev : Expr → nat | zero := 0 | one := 1 -| ((a : Expr) + b) := _root_.add (ev a) (ev b) +| ((a : Expr) + b) := has_add.add (ev a) (ev b) definition foo : Expr := add zero (add one one) diff --git a/tests/lean/run/u_eq_max_u_v.lean b/tests/lean/run/u_eq_max_u_v.lean index 52b541bf60..80bf5e1ca4 100644 --- a/tests/lean/run/u_eq_max_u_v.lean +++ b/tests/lean/run/u_eq_max_u_v.lean @@ -30,7 +30,7 @@ attribute [simp] semigroup_morphism.multiplicative mul := λ p q, (p^.fst * q^.fst, p^.snd * q^.snd), mul_assoc := begin intros, - simp [@mul.equations._eqn_1 (α × β)] + simp [@has_mul.mul (α × β)] end } @@ -44,7 +44,7 @@ definition semigroup_morphism_product begin -- cf https://groups.google.com/d/msg/lean-user/bVs5FdjClp4/tfHiVjLIBAAJ intros, - unfold mul has_mul.mul, + unfold has_mul.mul, dsimp, simp end diff --git a/tests/lean/run/unification_hints.lean b/tests/lean/run/unification_hints.lean index bbf15fb894..43e596e3b2 100644 --- a/tests/lean/run/unification_hints.lean +++ b/tests/lean/run/unification_hints.lean @@ -26,7 +26,7 @@ constants (n : ℕ) { pattern := m + 1 ≟ succ n, constraints := [m ≟ n] } -attribute [irreducible] add +attribute [irreducible] has_add.add open tactic diff --git a/tests/lean/run/wfrec1.lean b/tests/lean/run/wfrec1.lean index 232164a316..4f12d82a67 100644 --- a/tests/lean/run/wfrec1.lean +++ b/tests/lean/run/wfrec1.lean @@ -1,5 +1,5 @@ private definition S := Σ a : nat, nat -private definition R : S → S → Prop := sigma.skip_left nat lt +private definition R : S → S → Prop := sigma.skip_left nat (<) private definition Rwf : well_founded R := sigma.skip_left_wf nat nat.lt_wf private definition f_aux : ∀ (p₁ : S), (∀ p₂ : S, R p₂ p₁ → nat) → nat diff --git a/tests/lean/set_opt_tac.lean.expected.out b/tests/lean/set_opt_tac.lean.expected.out index d27a1d2d2c..0ad38d56d1 100644 --- a/tests/lean/set_opt_tac.lean.expected.out +++ b/tests/lean/set_opt_tac.lean.expected.out @@ -1,5 +1,5 @@ a + b = 0 after pp.all true -@eq.{1} nat (@add.{0} nat nat.has_add a b) (@zero.{0} nat nat.has_zero) +@eq.{1} nat (@has_add.add.{0} nat nat.has_add a b) (@has_zero.zero.{0} nat nat.has_zero) set_bool_option tactic does not affect other commands 0 + 1 : ℕ diff --git a/tests/lean/type_class_bug.lean.expected.out b/tests/lean/type_class_bug.lean.expected.out index 99f2da45ef..eb0c05e047 100644 --- a/tests/lean/type_class_bug.lean.expected.out +++ b/tests/lean/type_class_bug.lean.expected.out @@ -1,15 +1,16 @@ @has_bind.bind.{0 0} list.{0} (@monad.to_has_bind.{0 0} list.{0} list.monad.{0}) nat nat - (@list.cons.{0} nat (@one.{0} nat nat.has_one) (@list.nil.{0} nat)) + (@list.cons.{0} nat (@has_one.one.{0} nat nat.has_one) (@list.nil.{0} nat)) (λ (a : nat), @return.{0 0} list.{0} list.monad.{0} nat a) : list.{0} nat @has_bind.bind.{0 0} list.{0} (@monad.to_has_bind.{0 0} list.{0} list.monad.{0}) nat (prod.{0 0} nat nat) - (@list.cons.{0} nat (@one.{0} nat nat.has_one) - (@list.cons.{0} nat (@bit0.{0} nat nat.has_add (@one.{0} nat nat.has_one)) - (@list.cons.{0} nat (@bit1.{0} nat nat.has_one nat.has_add (@one.{0} nat nat.has_one)) (@list.nil.{0} nat)))) + (@list.cons.{0} nat (@has_one.one.{0} nat nat.has_one) + (@list.cons.{0} nat (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one)) + (@list.cons.{0} nat (@bit1.{0} nat nat.has_one nat.has_add (@has_one.one.{0} nat nat.has_one)) + (@list.nil.{0} nat)))) (λ (a : nat), @has_bind.bind.{0 0} list.{0} (@monad.to_has_bind.{0 0} list.{0} list.monad.{0}) nat (prod.{0 0} nat nat) - (@list.cons.{0} nat (@bit1.{0} nat nat.has_one nat.has_add (@one.{0} nat nat.has_one)) - (@list.cons.{0} nat (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@one.{0} nat nat.has_one))) + (@list.cons.{0} nat (@bit1.{0} nat nat.has_one nat.has_add (@has_one.one.{0} nat nat.has_one)) + (@list.cons.{0} nat (@bit0.{0} nat nat.has_add (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one))) (@list.nil.{0} nat))) (λ (b : nat), @return.{0 0} list.{0} list.monad.{0} (prod.{0 0} nat nat) (@prod.mk.{0 0} nat nat a b))) : list.{0} (prod.{0 0} nat nat) diff --git a/tests/lean/unification_hints1.lean.expected.out b/tests/lean/unification_hints1.lean.expected.out index 4778e2372d..a5e531cd33 100644 --- a/tests/lean/unification_hints1.lean.expected.out +++ b/tests/lean/unification_hints1.lean.expected.out @@ -4,7 +4,7 @@ g x y =?= f z g x y =?= f z unification successful unification hints: -(nat.succ, add) succ #0 =?= #2 + succ #1 {#0 =?= #2 + #1} +(has_add.add, nat.succ) #2 + succ #1 =?= succ #0 {#0 =?= #2 + #1} (toy.f, toy.g) f z =?= g #1 #0 {} Canonical.carrier A_canonical =?= A unification failed @@ -12,6 +12,6 @@ Canonical.carrier A_canonical =?= A Canonical.carrier A_canonical =?= A unification successful unification hints: -(nat.succ, add) succ #0 =?= #2 + succ #1 {#0 =?= #2 + #1} +(has_add.add, nat.succ) #2 + succ #1 =?= succ #0 {#0 =?= #2 + #1} (toy.f, toy.g) toy.f toy.z =?= toy.g #1 #0 {} (canonical.A, canonical.Canonical.carrier) A =?= Canonical.carrier #0 {#0 =?= A_canonical}