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`.
This commit is contained in:
Leonardo de Moura
parent
3e2e9ed98a
commit
5cef84709f
93 changed files with 432 additions and 464 deletions
|
|
@ -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 _)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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],
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 : ℕ}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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. -/
|
||||
|
|
|
|||
|
|
@ -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)} <|>
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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<expr> const & src, name const & S, name const & fname) {
|
||||
|
|
|
|||
|
|
@ -854,11 +854,11 @@ expr elaborator::visit_prenum(expr const & e, optional<expr> 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<expr> 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<expr> 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<expr> const & e
|
|||
expr empty_struct = copy_tag(e, mk_structure_instance(name(), buffer<name>(), buffer<expr>()));
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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)));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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]) {
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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<arith_app_info>({
|
||||
// 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)},
|
||||
});
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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<mpq> 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<mpq>(*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<mpq>(*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<mpq> arith_instance::eval(expr const & e) {
|
|||
else
|
||||
return optional<mpq>(*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<mpq> arith_instance::eval(expr const & e) {
|
|||
else
|
||||
return optional<mpq>(*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<mpq>(neg(*r1));
|
||||
} else if (auto r = to_num(e)) {
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -1448,7 +1448,7 @@ class add_nested_inductive_decl_fn {
|
|||
|
||||
expr prove_by_simp(local_context const & lctx, expr const & thm, list<expr> 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);
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<expr, expr> 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<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
|||
lhs_p.first, rhs_p.first, nval, lhs_p.second, rhs_p.second, prf});
|
||||
return pair<expr, expr>(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<expr, expr> 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<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
|||
args[2], nval, prf.second});
|
||||
return pair<expr, expr>(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<expr, expr> 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<expr, expr>(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<expr, expr> 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<expr, expr>(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<expr, expr>(e, mk_eq_refl(m_ctx, e));
|
||||
} else {
|
||||
|
|
|
|||
|
|
@ -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<expr> is_bit1(expr const & e) {
|
|||
}
|
||||
|
||||
optional<expr> 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<expr> 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<mpz> 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();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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<mpz> 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<mpz> eval_num(expr const & e) {
|
|||
return some(*r1 + 1);
|
||||
else
|
||||
return optional<mpz>();
|
||||
} 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<mpz>();
|
||||
auto r2 = eval_num(app_arg(e));
|
||||
if (!r2) return optional<mpz>();
|
||||
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<mpz>();
|
||||
auto r2 = eval_num(app_arg(e));
|
||||
|
|
@ -2748,9 +2748,9 @@ optional<unsigned> 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<unsigned> 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<unsigned> 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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<pair<expr, expr>> find_unsynth_metavar(expr const & e);
|
||||
bool mk_nested_instance(expr const & m, expr const & m_type);
|
||||
friend class unification_hint_fn;
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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() {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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}}]}
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
[nat.succ, nat.add, add]
|
||||
[nat.mul, mul]
|
||||
[has_mul.mul, nat.mul]
|
||||
[has_add.add, nat.succ, nat.add]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
[macro structure instance (const zero []) [macro prenum]]
|
||||
[macro structure instance (const has_zero.zero []) [macro prenum]]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
@add nat nat.has_add 10 3 : nat
|
||||
@has_add.add nat nat.has_add 10 3 : nat
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
#check @zero
|
||||
#check @zero nat
|
||||
#check @has_zero.zero
|
||||
#check @has_zero.zero nat
|
||||
|
|
|
|||
|
|
@ -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 ℕ], ℕ
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ open foo boo
|
|||
|
||||
open nat
|
||||
|
||||
#check ``add
|
||||
#check ``has_add.add
|
||||
|
||||
#check ``gcd
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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] :=
|
||||
|
|
|
|||
|
|
@ -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₂)) >>
|
||||
|
|
|
|||
|
|
@ -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],
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ constants (n : ℕ)
|
|||
{ pattern := m + 1 ≟ succ n,
|
||||
constraints := [m ≟ n] }
|
||||
|
||||
attribute [irreducible] add
|
||||
attribute [irreducible] has_add.add
|
||||
|
||||
open tactic
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 : ℕ
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue