From a7d08d2f3dd608a70d41c92ca5559c2528e21ee5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Jun 2018 12:33:21 -0700 Subject: [PATCH] feat(kernel/inductive/inductive): dependent elimination for inductive predicates In Lean4, we will not generate non dependent recursors for inductive predicates. The main goal is to make the shape of the automatically generated recursors more uniform. The non uniform representation is leftover from Lean2. In Lean2, we wanted to support different kernels with different features. For example: we could create proof relevant kernels, no impredicative universe, etc. Recall that, in a kernel with an impredicative Prop and no proof irrelevance, inductive predicates without dependent elimination are weaker that inductive predicates with dependent elimination. When proof irrelevance is enabled, we can generate the dependent recursor from the non dependent one. Actually, the module drec.cpp generates the dependent recursor. Now, we only support one kind of kernel, and it doesn't make sense anymore to generate non dependent recursors for inductive predicates. This would only produce an unnecessary asymmetry on the inductive datatype module. Remark: we had to create non dependent recursors to help the elaborator. This can be avoid if we improve the elaborator. I will do that in the new elaborator implemented in Lean. Remark: equation lemmas are broken for definitions that pattern match on nested inductive datatypes. The problem is the super messy `prove_eq_rec_invertible_aux` function. This function will not be needed after I finish the new inductive datatype support in the kernel. cc @kha --- library/init/core.lean | 87 +++++++++++++------ library/init/data/nat/basic.lean | 14 ++- library/init/wf.lean | 39 ++++++--- src/frontends/lean/elaborator.cpp | 1 + src/frontends/lean/structure_cmd.cpp | 2 - src/kernel/inductive/inductive.cpp | 6 +- src/library/app_builder.cpp | 16 ++-- src/library/app_builder.h | 4 +- src/library/congr_lemma.cpp | 8 +- src/library/constants.cpp | 16 ++-- src/library/constants.h | 4 +- src/library/constants.txt | 4 +- src/library/constructions/no_confusion.cpp | 4 +- src/library/equations_compiler/elim_match.cpp | 2 +- src/library/equations_compiler/util.cpp | 10 ++- src/library/inductive_compiler/basic.cpp | 16 ++-- src/library/inductive_compiler/nested.cpp | 12 +-- src/library/tactic/rewrite_tactic.cpp | 2 +- src/library/tactic/simplify.cpp | 2 +- src/library/tactic/subst_tactic.cpp | 2 +- src/library/user_recursors.cpp | 2 - src/library/util.cpp | 32 +++---- 22 files changed, 168 insertions(+), 117 deletions(-) diff --git a/library/init/core.lean b/library/init/core.lean index 112d03b562..8de48b5414 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -155,6 +155,14 @@ prefix `¬` := not inductive eq {α : Sort u} (a : α) : α → Prop | refl : eq a +@[elab_as_eliminator, inline, reducible] +def {u1 u2} eq.ndrec {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : eq a b) : C b := +@eq.rec α a (λ α _, C α) m b h + +@[elab_as_eliminator, inline, reducible] +def {u1 u2} eq.ndrec_on {α : Sort u2} {a : α} {C : α → Sort u1} {b : α} (h : eq a b) (m : C a) : C b := +@eq.rec α a (λ α _, C α) m b h + /- Initialize the quotient module, which effectively adds the following definitions: @@ -201,7 +209,7 @@ attribute [refl] eq.refl @[elab_as_eliminator, subst] theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b := -eq.rec h₂ h₁ +eq.ndrec h₂ h₁ notation h1 ▸ h2 := eq.subst h1 h2 @@ -218,7 +226,7 @@ infix == := heq theorem eq_of_heq {α : Sort u} {a a' : α} (h : a == a') : a = a' := have ∀ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a') (h₂ : α = α'), (eq.rec_on h₂ a : α') = a', from λ (α' : Sort u) (a' : α') (h₁ : @heq α a α' a'), heq.rec_on h₁ (λ h₂ : α = α, rfl), -show (eq.rec_on (eq.refl α) a : α) = a', from +show (eq.ndrec_on (eq.refl α) a : α) = a', from this α a' h (eq.refl α) /- The following four lemmas could not be automatically generated when the @@ -616,8 +624,11 @@ assume hp, h₂ (h₁ hp) def trivial : true := ⟨⟩ +@[inline] def false.elim {C : Sort u} (h : false) : C := +false.rec (λ _, C) h + @[inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b := -false.rec b (h₂ h₁) +false.elim (h₂ h₁) theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha) @@ -625,9 +636,6 @@ theorem not.intro {a : Prop} (h : a → false) : ¬ a := h theorem not_false : ¬false := id -@[inline] def false.elim {C : Sort u} (h : false) : C := -false.rec C h - -- proof irrelevance is built in theorem proof_irrel {a : Prop} (h₁ h₂ : a) : h₁ = h₂ := rfl @@ -706,14 +714,22 @@ attribute [refl] heq.refl section variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ} +@[elab_as_eliminator] +theorem {u1 u2} heq.ndrec {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a == b) : C b := +@heq.rec α a (λ β b _, C b) m β b h + +@[elab_as_eliminator] +theorem {u1 u2} heq.ndrec_on {α : Sort u2} {a : α} {C : Π {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a == b) (m : C a) : C b := +@heq.rec α a (λ β b _, C b) m β b h + theorem heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a == b) (h₂ : p a) : p b := eq.rec_on (eq_of_heq h₁) h₂ theorem heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a == b) (h₂ : p α a) : p β b := -heq.rec_on h₁ h₂ +heq.ndrec_on h₁ h₂ @[symm] theorem heq.symm (h : a == b) : b == a := -heq.rec_on h (heq.refl a) +heq.ndrec_on h (heq.refl a) theorem heq_of_eq (h : a = a') : a == a' := eq.subst h (heq.refl a) @@ -728,7 +744,7 @@ heq.trans h₁ (heq_of_eq h₂) heq.trans (heq_of_eq h₁) h₂ def type_eq_of_heq (h : a == b) : α = β := -heq.rec_on h (eq.refl α) +heq.ndrec_on h (eq.refl α) end theorem eq_rec_heq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p @@ -745,9 +761,6 @@ theorem heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} theorem of_heq_true {a : Prop} (h : a == true) : a := of_eq_true (eq_of_heq h) -theorem eq_rec_compose : ∀ {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a -| α _ _ rfl rfl a := rfl - theorem cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a == a | α _ rfl a := heq.refl a @@ -772,7 +785,8 @@ assume not_em : ¬(a ∨ ¬a), def not_not_em := non_contradictory_em -theorem or.swap : a ∨ b → b ∨ a := or.rec or.inr or.inl +theorem or.swap (h : a ∨ b) : b ∨ a := +or.elim h or.inr or.inl def or.symm := @or.swap @@ -780,7 +794,8 @@ def or.symm := @or.swap def xor (a b : Prop) := (a ∧ ¬ b) ∨ (b ∧ ¬ a) @[recursor 5] -theorem iff.elim : ((a → b) → (b → a) → c) → (a ↔ b) → c := iff.rec +theorem iff.elim (h₁ : (a → b) → (b → a) → c) (h₂ : a ↔ b) : c := +iff.rec h₁ h₂ theorem iff.elim_left : (a ↔ b) → a → b := iff.mp @@ -833,7 +848,7 @@ iff.intro (λ hr, h) theorem iff_false_intro (h : ¬a) : a ↔ false := -iff.intro h (false.rec a) +iff.intro h (false.rec (λ _, a)) theorem imp_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) := iff.intro @@ -971,13 +986,13 @@ iff_true_intro (or.inr trivial) iff_true_intro (or.inl trivial) @[simp] theorem or_false (a : Prop) : a ∨ false ↔ a := -iff.intro (or.rec id false.elim) or.inl +iff.intro (λ h, or.elim h id false.elim) or.inl @[simp] theorem false_or (a : Prop) : false ∨ a ↔ a := iff.trans or_comm (or_false a) @[simp] theorem or_self (a : Prop) : a ∨ a ↔ a := -iff.intro (or.rec id id) or.inl +iff.intro (λ h, or.elim h id id) or.inl theorem not_or {a b : Prop} : ¬ a → ¬ b → ¬ (a ∨ b) | hna hnb (or.inl ha) := absurd ha hna @@ -1185,7 +1200,7 @@ else is_false (assume h : p ∧ q, hp (and.left h)) instance [decidable p] [decidable q] : decidable (p ∨ q) := if hp : p then is_true (or.inl hp) else if hq : q then is_true (or.inr hq) else - is_false (or.rec hp hq) + is_false (λ h, or.elim h hp hq) instance [decidable p] : decidable (¬p) := if hp : p then is_false (absurd hp) else is_true hp @@ -1206,11 +1221,11 @@ else instance [decidable p] [decidable q] : decidable (xor p q) := if hp : p then - if hq : q then is_false (or.rec (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p))) + if hq : q then is_false (λ h, or.elim h (λ ⟨_, h⟩, h hq : ¬(p ∧ ¬ q)) (λ ⟨_, h⟩, h hp : ¬(q ∧ ¬ p))) else is_true $ or.inl ⟨hp, hq⟩ else if hq : q then is_true $ or.inr ⟨hq, hp⟩ - else is_false (or.rec (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p))) + else is_false (λ h, or.elim h (λ ⟨h, _⟩, hp h : ¬(p ∧ ¬ q)) (λ ⟨h, _⟩, hq h : ¬(q ∧ ¬ p))) instance exists_prop_decidable {p} (P : p → Prop) [decidable p] [s : ∀ h, decidable (P h)] : decidable (∃ h, P h) := if h : p then decidable_of_decidable_of_iff (s h) @@ -1240,7 +1255,7 @@ instance : decidable_eq bool def decidable_eq_of_bool_pred {α : Sort u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α := assume x y : α, if hp : p x y = tt then is_true (h₁ hp) - else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z, ¬p z y = tt) _ hxy hp)) + else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z _, ¬p z y = tt) _ hxy hp)) theorem decidable_eq_inl_refl {α : Sort u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) := match (h a a) with @@ -1272,10 +1287,10 @@ match h with | (is_false hnc) := rfl theorem implies_of_if_pos {c t e : Prop} [decidable c] (h : ite c t e) : c → t := -assume hc, eq.rec_on (if_pos hc : ite c t e = t) h +assume hc, eq.ndrec_on (if_pos hc : ite c t e = t) h theorem implies_of_if_neg {c t e : Prop} [decidable c] (h : ite c t e) : ¬c → e := -assume hnc, eq.rec_on (if_neg hnc : ite c t e = e) h +assume hnc, eq.ndrec_on (if_neg hnc : ite c t e = e) h theorem if_ctx_congr {α : Sort u} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c] {x y u v : α} @@ -1495,11 +1510,11 @@ match h with /- Equalities for rewriting let-expressions -/ theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ a₂ : α} (b : α → β) : a₁ = a₂ → (let x : α := a₁ in b x) = (let x : α := a₂ in b x) := -λ h, eq.rec_on h rfl +λ h, eq.ndrec_on h rfl theorem let_value_heq {α : Sort v} {β : α → Sort u} {a₁ a₂ : α} (b : Π x : α, β x) : a₁ = a₂ → (let x : α := a₁ in b x) == (let x : α := a₂ in b x) := -λ h, eq.rec_on h (heq.refl (b a₁)) +λ h, eq.ndrec_on h (heq.refl (b a₁)) theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : Π x : α, β x} : (∀ x, b₁ x = b₂ x) → (let x : α := a in b₁ x) = (let x : α := a in b₂ x) := @@ -1507,7 +1522,7 @@ theorem let_body_eq {α : Sort v} {β : α → Sort u} (a : α) {b₁ b₂ : Π theorem let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β} : a₁ = a₂ → (∀ x, b₁ x = b₂ x) → (let x : α := a₁ in b₁ x) = (let x : α := a₂ in b₂ x) := -λ h₁ h₂, eq.rec_on h₁ (h₂ a₁) +λ h₁ h₂, eq.ndrec_on h₁ (h₂ a₁) section relation variables {α : Sort u} {β : Sort v} (r : β → β → Prop) @@ -1546,6 +1561,22 @@ theorem inv_image.irreflexive (f : α → β) (h : irreflexive r) : irreflexive inductive tc {α : Sort u} (r : α → α → Prop) : α → α → Prop | base : ∀ a b, r a b → tc a b | trans : ∀ a b c, tc a b → tc b c → tc a c + +@[elab_as_eliminator] +theorem {u1 u2} tc.ndrec {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} + (m₁ : ∀ (a b : α), r a b → C a b) + (m₂ : ∀ (a b c : α), tc r a b → tc r b c → C a b → C b c → C a c) + {a b : α} (h : tc r a b) : C a b := +@tc.rec α r (λ a b _, C a b) m₁ m₂ a b h + +@[elab_as_eliminator] +theorem {u1 u2} tc.ndrec_on {α : Sort u} {r : α → α → Prop} {C : α → α → Prop} + {a b : α} (h : tc r a b) + (m₁ : ∀ (a b : α), r a b → C a b) + (m₂ : ∀ (a b c : α), tc r a b → tc r b c → C a b → C b c → C a c) + : C a b := +@tc.rec α r (λ a b _, C a b) m₁ m₂ a b h + end relation section binary @@ -1822,7 +1853,7 @@ quot.ind (λ (a : α), eq.refl (quot.indep f a).1) q protected def rec (f : Π a, β ⟦a⟧) (h : ∀ (a b : α) (p : r a b), (eq.rec (f a) (sound p) : β ⟦b⟧) = f b) (q : quot r) : β q := -eq.rec_on (quot.lift_indep_pr1 f h q) ((lift (quot.indep f) (quot.indep_coherent f h) q).2) +eq.ndrec_on (quot.lift_indep_pr1 f h q) ((lift (quot.indep f) (quot.indep_coherent f h) q).2) @[reducible, elab_as_eliminator] protected def rec_on @@ -1965,7 +1996,7 @@ private theorem rel.refl : ∀ q : quotient s, q ~ q := λ q, quot.induction_on q (λ a, setoid.refl a) private theorem eq_imp_rel {q₁ q₂ : quotient s} : q₁ = q₂ → q₁ ~ q₂ := -assume h, eq.rec_on h (rel.refl q₁) +assume h, eq.ndrec_on h (rel.refl q₁) theorem exact {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b := assume h, eq_imp_rel h diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index eae4ad12ab..dfffbf5f05 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -14,6 +14,14 @@ inductive less_than_or_equal (a : nat) : nat → Prop | refl : less_than_or_equal a | step : Π {b}, less_than_or_equal b → less_than_or_equal (succ b) +@[elab_as_eliminator] +theorem less_than_or_equal.ndrec {a : nat} {C : nat → Prop} (m₁ : C a) (m₂ : ∀ (b : nat), less_than_or_equal a b → C b → C (succ b)) {b : ℕ} (h : less_than_or_equal a b) : C b := +@less_than_or_equal.rec a (λ b _, C b) m₁ m₂ b h + +@[elab_as_eliminator] +theorem less_than_or_equal.ndrec_on {a : nat} {C : nat → Prop} {b : ℕ} (h : less_than_or_equal a b) (m₁ : C a) (m₂ : ∀ (b : nat), less_than_or_equal a b → C b → C (succ b)) : C b := +@less_than_or_equal.rec a (λ b _, C b) m₁ m₂ b h + instance : has_le nat := ⟨nat.less_than_or_equal⟩ @@ -183,7 +191,7 @@ theorem le_succ (n : nat) : n ≤ succ n := less_than_or_equal.step (nat.le_refl n) theorem succ_le_succ {n m : nat} : n ≤ m → succ n ≤ succ m := -λ h, less_than_or_equal.rec (nat.le_refl (succ n)) (λ a b, less_than_or_equal.step) h +λ h, less_than_or_equal.ndrec (nat.le_refl (succ n)) (λ a b, less_than_or_equal.step) h theorem succ_lt_succ {n m : nat} : n < m → succ n < succ m := succ_le_succ @@ -204,7 +212,7 @@ theorem not_lt_zero (n : nat) : ¬ n < 0 := not_succ_le_zero n theorem pred_le_pred {n m : nat} : n ≤ m → pred n ≤ pred m := -λ h, less_than_or_equal.rec_on h +λ h, less_than_or_equal.ndrec_on h (nat.le_refl (pred n)) (λ n, nat.rec (λ a b, b) (λ a b c, less_than_or_equal.step) n) @@ -243,7 +251,7 @@ protected theorem lt_irrefl (n : nat) : ¬n < n := not_succ_le_self n protected theorem le_trans {n m k : nat} (h1 : n ≤ m) : m ≤ k → n ≤ k := -less_than_or_equal.rec h1 (λ p h2, less_than_or_equal.step) +less_than_or_equal.ndrec h1 (λ p h2, less_than_or_equal.step) theorem pred_le : ∀ (n : nat), pred n ≤ n | 0 := less_than_or_equal.refl 0 diff --git a/library/init/wf.lean b/library/init/wf.lean index e119d02fa6..49865d53d4 100644 --- a/library/init/wf.lean +++ b/library/init/wf.lean @@ -11,6 +11,19 @@ universes u v inductive acc {α : Sort u} (r : α → α → Prop) : α → Prop | intro (x : α) (h : ∀ y, r y x → acc y) : acc x +@[elab_as_eliminator, inline, reducible] +def {u1 u2} acc.ndrec {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} + (m : Π (x : α) (h : ∀ (y : α), r y x → acc r y), (Π (y : α) (a : r y x), C y) → C x) + {a : α} (n : acc r a) : C a := +@acc.rec α r (λ α _, C α) m a n + +@[elab_as_eliminator, inline, reducible] +def {u1 u2} acc.ndrec_on {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} + {a : α} (n : acc r a) + (m : Π (x : α) (h : ∀ (y : α), r y x → acc r y), (Π (y : α) (a : r y x), C y) → C x) + : C a := +@acc.rec α r (λ α _, C α) m a n + namespace acc variables {α : Sort u} {r : α → α → Prop} @@ -49,7 +62,7 @@ acc.rec_on a (λ x₁ ac₁ ih, F x₁ ih) theorem fix_F_eq (x : α) (acx : acc r x) : fix_F F x acx = F x (λ (y : α) (p : y ≺ x), fix_F F y (acc.inv acx p)) := -acc.drec (λ x r ih, rfl) acx +acc.rec (λ x r ih, rfl) acx end variables {α : Sort u} {C : α → Sort v} {r : α → α → Prop} @@ -95,8 +108,8 @@ parameters (f : α → β) parameters (h : well_founded r) private def acc_aux {b : β} (ac : acc r b) : ∀ (x : α), f x = b → acc (inv_image r f) x := -acc.rec_on ac (λ x acx ih z e, - acc.intro z (λ y lt, eq.rec_on e (λ acx ih, ih (f y) lt y rfl) acx ih)) +acc.ndrec_on ac (λ x acx ih z e, + acc.intro z (λ y lt, eq.ndrec_on e (λ acx ih, ih (f y) lt y rfl) acx ih)) def accessible {a : α} (ac : acc r (f a)) : acc (inv_image r f) a := acc_aux ac a rfl @@ -113,9 +126,9 @@ parameters {α : Sort u} {r : α → α → Prop} local notation `r⁺` := tc r def accessible {z : α} (ac : acc r z) : acc (tc r) z := -acc.rec_on ac (λ x acx ih, +acc.ndrec_on ac (λ x acx ih, acc.intro x (λ y rel, - tc.rec_on rel + tc.ndrec_on rel (λ a b rab acx ih, ih a rab) (λ a b c rab rbc ih₁ ih₂ acx ih, acc.inv (ih₂ acx ih) rab) acx ih)) @@ -172,11 +185,11 @@ parameters {ra : α → α → Prop} {rb : β → β → Prop} local infix `≺`:50 := lex ra rb def lex_accessible {a} (aca : acc ra a) (acb : ∀ b, acc rb b): ∀ b, acc (lex ra rb) (a, b) := -acc.rec_on aca (λ xa aca iha b, - acc.rec_on (acb b) (λ xb acb ihb, +acc.ndrec_on aca (λ xa aca iha b, + acc.ndrec_on (acb b) (λ xb acb ihb, acc.intro (xa, xb) (λ p lt, have aux : xa = xa → xb = xb → acc (lex ra rb) p, from - @prod.lex.rec_on α β ra rb (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁) + @prod.lex.rec_on α β ra rb (λ p₁ p₂ _, fst p₂ = xa → snd p₂ = xb → acc (lex ra rb) p₁) p (xa, xb) lt (λ a₁ b₁ a₂ b₂ h (eq₂ : a₂ = xa) (eq₃ : b₂ = xb), iha a₁ (eq.rec_on eq₂ h) b₁) (λ a b₁ b₂ h (eq₂ : a = xa) (eq₃ : b₂ = xb), eq.rec_on eq₂.symm (ihb b₁ (eq.rec_on eq₃ h))), @@ -188,7 +201,7 @@ def lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra -- relational product is a subrelation of the lex def rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b := -λ a b h, prod.rprod.rec_on h (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb b₁ b₂ h₁) +@prod.rprod.rec _ _ ra rb (λ a b _, lex ra rb a b) (λ a₁ b₁ a₂ b₂ h₁ h₂, lex.left rb b₁ b₂ h₁) -- The relational product of well founded relations is well-founded def rprod_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (rprod ra rb) := @@ -219,14 +232,14 @@ local infix `≺`:50 := lex r s def lex_accessible {a} (aca : acc r a) (acb : ∀ a, well_founded (s a)) : ∀ (b : β a), acc (lex r s) ⟨a, b⟩ := -acc.rec_on aca +acc.ndrec_on aca (λ xa aca (iha : ∀ y, r y xa → ∀ b : β y, acc (lex r s) ⟨y, b⟩), - λ b : β xa, acc.rec_on (well_founded.apply (acb xa) b) + λ b : β xa, acc.ndrec_on (well_founded.apply (acb xa) b) (λ xb acb (ihb : ∀ (y : β xa), s xa y xb → acc (lex r s) ⟨xa, y⟩), acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩), have aux : xa = xa → xb == xb → acc (lex r s) p, from - @psigma.lex.rec_on α β r s (λ p₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex r s) p₁) + @psigma.lex.rec_on α β r s (λ p₁ p₂ _, p₂.1 = xa → p₂.2 == xb → acc (lex r s) p₁) p ⟨xa, xb⟩ lt (λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb), have aux : (∀ (y : α), r y xa → ∀ (b : β y), acc (lex r s) ⟨y, b⟩) → @@ -286,7 +299,7 @@ acc.rec_on acb (λ xa aca (iha : ∀ y, r y xa → acc (rev_lex r s) (mk y xb)), acc.intro ⟨xa, xb⟩ (λ p (lt : p ≺ ⟨xa, xb⟩), have aux : xa = xa → xb = xb → acc (rev_lex r s) p, from - @rev_lex.rec_on α β r s (λ p₁ p₂, fst p₂ = xa → snd p₂ = xb → acc (rev_lex r s) p₁) + @rev_lex.rec_on α β r s (λ p₁ p₂ _, fst p₂ = xa → snd p₂ = xb → acc (rev_lex r s) p₁) p ⟨xa, xb⟩ lt (λ a₁ a₂ b (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b = xb), show acc (rev_lex r s) ⟨a₁, b⟩, from diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 68ed08e741..046fa760a4 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1137,6 +1137,7 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< trace_elab_debug(tout() << "motive:\n " << instantiate_mvars(motive) << "\n";); expr motive_arg = new_args[info.m_motive_idx]; + trace_elab_debug(tout() << "motive_arg:\n " << motive_arg << "\n";); if (!is_def_eq_all_approx(motive_arg, motive)) { throw elaborator_exception(ref, "\"eliminator\" elaborator failed to compute the motive"); } diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 230f027964..b410e61fe1 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -1176,8 +1176,6 @@ struct structure_cmd_fn { name cases_on_name(m_name, "cases_on"); add_rec_on_alias(cases_on_name); m_env = add_aux_recursor(m_env, cases_on_name); - if (is_inductive_predicate(m_env, m_name)) - m_env = mk_drec(m_env, m_name); } // Return the parent names without namespace prefix diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index b3d439d0c3..7b64e51b75 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -518,10 +518,7 @@ struct add_inductive_fn { /** \brief Initialize m_dep_elim flag. */ void set_dep_elim() { - if (is_zero(m_it_level)) - m_dep_elim = false; - else - m_dep_elim = true; + m_dep_elim = true; } /** \brief Given t of the form (I As is) where I is the inductive datatypes being defined, @@ -734,6 +731,7 @@ struct add_inductive_fn { declare_intro_rules(); certified_inductive_decl c = mk_certified_decl(declare_elim_rule()); m_env = c.add_core(m_env, true); + // std::cout << ">> " << m_decl.m_name << " declared\n"; return mk_pair(m_env, c); } }; diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index f8c2025ab1..1d1ae50e1d 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -604,7 +604,7 @@ public: return ::lean::mk_app({mk_constant(get_heq_trans_name(), {lvl}), A1, B1, B2, a1, b1, b2, H1, H2}); } - expr mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) { + expr mk_eq_ndrec(expr const & motive, expr const & H1, expr const & H2) { if (is_constant(get_app_fn(H2), get_eq_refl_name())) return H1; expr p = m_ctx.relaxed_whnf(m_ctx.infer(H2)); @@ -620,11 +620,11 @@ public: throw app_builder_exception(); } level l_1 = sort_level(binding_body(mtype)); - name const & eqrec = get_eq_rec_name(); + name const & eqrec = get_eq_ndrec_name(); return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2}); } - expr mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) { + expr mk_eq_rec(expr const & motive, expr const & H1, expr const & H2) { if (is_constant(get_app_fn(H2), get_eq_refl_name())) return H1; expr p = m_ctx.relaxed_whnf(m_ctx.infer(H2)); @@ -640,7 +640,7 @@ public: throw app_builder_exception(); } level l_1 = sort_level(binding_body(binding_body(mtype))); - name const & eqrec = get_eq_drec_name(); + name const & eqrec = get_eq_rec_name(); return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2}); } @@ -856,12 +856,12 @@ expr mk_heq_trans(type_context_old & ctx, expr const & H1, expr const & H2) { return app_builder(ctx).mk_heq_trans(H1, H2); } -expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2) { - return app_builder(ctx).mk_eq_rec(C, H1, H2); +expr mk_eq_ndrec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2) { + return app_builder(ctx).mk_eq_ndrec(C, H1, H2); } -expr mk_eq_drec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2) { - return app_builder(ctx).mk_eq_drec(C, H1, H2); +expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2) { + return app_builder(ctx).mk_eq_rec(C, H1, H2); } expr mk_eq_of_heq(type_context_old & ctx, expr const & H) { diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 070e059f52..9217d4850e 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -113,7 +113,7 @@ expr mk_heq_trans(type_context_old & ctx, expr const & H1, expr const & H2); H2 : a = b The resultant application is @eq.rec A a C H1 b H2 */ -expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2); +expr mk_eq_ndrec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2); /** \brief Create a (dependent) eq.drec application. C is the motive. The expected types for C, H1 and H2 are @@ -122,7 +122,7 @@ expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr con H2 : a = b The resultant application is @eq.drec A a C H1 b H2 */ -expr mk_eq_drec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2); +expr mk_eq_rec(type_context_old & ctx, expr const & C, expr const & H1, expr const & H2); expr mk_eq_of_heq(type_context_old & ctx, expr const & H); expr mk_heq_of_eq(type_context_old & ctx, expr const & H); diff --git a/src/library/congr_lemma.cpp b/src/library/congr_lemma.cpp index 64153d6900..37956f00cb 100644 --- a/src/library/congr_lemma.cpp +++ b/src/library/congr_lemma.cpp @@ -95,9 +95,9 @@ struct congr_lemma_manager { } expr minor = cast(e, new_type, tail(deps), eqs); if (use_drec) { - return mk_eq_drec(m_ctx, motive, minor, *major); - } else { return mk_eq_rec(m_ctx, motive, minor, *major); + } else { + return mk_eq_ndrec(m_ctx, motive, minor, *major); } } } @@ -157,7 +157,7 @@ struct congr_lemma_manager { expr x1_refl = mk_eq_refl(m_ctx, x_1); new_rhs = instantiate(abstract(new_rhs, major), x1_refl); expr minor = mk_congr_proof(i+1, lhs, new_rhs, eqs); - return mk_eq_drec(m_ctx, motive, minor, major); + return mk_eq_rec(m_ctx, motive, minor, major); } } @@ -500,7 +500,7 @@ struct congr_lemma_manager { if (is_heq(m_ctx.infer(eq_pr))) major = mk_eq_of_heq(m_ctx, eq_pr); motive = m_ctx.mk_lambda({b}, motive); - return m_ctx.mk_lambda({a, b, eq_pr}, mk_eq_rec(m_ctx, motive, minor, major)); + return m_ctx.mk_lambda({a, b, eq_pr}, mk_eq_ndrec(m_ctx, motive, minor, major)); } } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 91b1410fb8..0179cf5c87 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -44,10 +44,10 @@ name const * g_empty = nullptr; name const * g_Exists = nullptr; name const * g_eq = nullptr; name const * g_eq_cases_on = nullptr; -name const * g_eq_drec = nullptr; +name const * g_eq_rec = nullptr; name const * g_eq_mp = nullptr; name const * g_eq_mpr = nullptr; -name const * g_eq_rec = nullptr; +name const * g_eq_ndrec = nullptr; name const * g_eq_refl = nullptr; name const * g_eq_subst = nullptr; name const * g_eq_symm = nullptr; @@ -298,10 +298,10 @@ void initialize_constants() { g_Exists = new name{"Exists"}; g_eq = new name{"eq"}; g_eq_cases_on = new name{"eq", "cases_on"}; - g_eq_drec = new name{"eq", "drec"}; + g_eq_rec = new name{"eq", "rec"}; g_eq_mp = new name{"eq", "mp"}; g_eq_mpr = new name{"eq", "mpr"}; - g_eq_rec = new name{"eq", "rec"}; + g_eq_ndrec = new name{"eq", "ndrec"}; g_eq_refl = new name{"eq", "refl"}; g_eq_subst = new name{"eq", "subst"}; g_eq_symm = new name{"eq", "symm"}; @@ -553,10 +553,10 @@ void finalize_constants() { delete g_Exists; delete g_eq; delete g_eq_cases_on; - delete g_eq_drec; + delete g_eq_rec; delete g_eq_mp; delete g_eq_mpr; - delete g_eq_rec; + delete g_eq_ndrec; delete g_eq_refl; delete g_eq_subst; delete g_eq_symm; @@ -807,10 +807,10 @@ name const & get_empty_name() { return *g_empty; } 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; } -name const & get_eq_drec_name() { return *g_eq_drec; } +name const & get_eq_rec_name() { return *g_eq_rec; } name const & get_eq_mp_name() { return *g_eq_mp; } name const & get_eq_mpr_name() { return *g_eq_mpr; } -name const & get_eq_rec_name() { return *g_eq_rec; } +name const & get_eq_ndrec_name() { return *g_eq_ndrec; } name const & get_eq_refl_name() { return *g_eq_refl; } name const & get_eq_subst_name() { return *g_eq_subst; } name const & get_eq_symm_name() { return *g_eq_symm; } diff --git a/src/library/constants.h b/src/library/constants.h index c812341f1e..a838f8c608 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -46,10 +46,10 @@ name const & get_empty_name(); name const & get_Exists_name(); name const & get_eq_name(); name const & get_eq_cases_on_name(); -name const & get_eq_drec_name(); +name const & get_eq_rec_name(); name const & get_eq_mp_name(); name const & get_eq_mpr_name(); -name const & get_eq_rec_name(); +name const & get_eq_ndrec_name(); name const & get_eq_refl_name(); name const & get_eq_subst_name(); name const & get_eq_symm_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index acced321d1..66021d054c 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -39,10 +39,10 @@ empty Exists eq eq.cases_on -eq.drec +eq.rec eq.mp eq.mpr -eq.rec +eq.ndrec eq.refl eq.subst eq.symm diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 5493dfcb66..a40098922a 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -215,10 +215,10 @@ environment mk_no_confusion(environment const & env, name const & n) { gen = Fun(H11, gen); // Now, we use gen to build the final proof using eq.rec // - // eq.rec InductiveType v1 (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) gen v2 H12 H12 + // eq.ndrec InductiveType v1 (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) gen v2 H12 H12 // level eq_rec_l1 = head(ls); - expr eq_rec = mk_app(mk_constant(get_eq_rec_name(), {eq_rec_l1, v_lvl}), v_type, v1); + expr eq_rec = mk_app(mk_constant(get_eq_ndrec_name(), {eq_rec_l1, v_lvl}), v_type, v1); // create eq_rec type_former // (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) expr a = mk_local(ngen.next(), "a", v_type, binder_info()); diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index a581e93348..0db6c99c75 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -1159,7 +1159,7 @@ struct elim_match_fn { expr id_M2 = mk_app(ctx1, get_id_name(), M_2); expr eqrec_minor = mk_app(id_M2, g_x1); expr eqrec_major = mk_app(ctx1, f_g_eq_name, x1); - eqrec = mk_eq_rec(ctx1, eqrec_motive, eqrec_minor, eqrec_major); + eqrec = mk_eq_ndrec(ctx1, eqrec_motive, eqrec_minor, eqrec_major); } catch (app_builder_exception &) { throw_error("equation compiler failed, when trying to build " "'eq.rec'-application for transport step (use 'set_option trace.eqn_compiler.elim_match true' " diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 728a00e518..bc4c87d985 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -455,7 +455,7 @@ static optional find_if_neg_hypothesis(type_context_old & ctx, expr const @eq.rec A a - (fun x : A, (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a)) + (fun (x : A) (_ : a = x), (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a)) (fun H : f a = f a, eq.refl (h a)) (g (f a)) (eq.symm (g_f_eq a)) @@ -518,8 +518,10 @@ static optional prove_eq_rec_invertible_aux(type_context_old & ctx, e expr eq_rec2 = mk_app(rec_fn, {B, f_x, C, h_x, f_a, H}); /* (@eq.rec B (f x) C (h x) (f a) H) = h a */ expr eq_rec2_eq = mk_eq(ctx, eq_rec2, h_a); - /* (fun x : A, (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a)) */ - expr pr_motive = ctx.mk_lambda(x, ctx.mk_pi(H, eq_rec2_eq)); + expr a_eq_x = mk_eq(ctx, a, x); + expr h_a_eq_x = aux_locals.push_local("_h'", a_eq_x); + /* (fun (x : A) (h' : a = x), (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a)) */ + expr pr_motive = ctx.mk_lambda(x, ctx.mk_lambda(h_a_eq_x, ctx.mk_pi(H, eq_rec2_eq))); expr g_f_eq_a = mk_app(ctx, g_f_name, a); /* (eq.symm (g_f_eq a)) */ expr pr_major = mk_eq_symm(ctx, g_f_eq_a); @@ -564,6 +566,8 @@ static optional prove_eq_rec_invertible(type_context_old & ctx, expr if (optional g_H = prove_eq_rec_invertible_aux(ctx, f)) { expr g, H; std::tie(g, H) = *g_H; + tout() << "H: " << H << "\n"; + tout() << ">>>>> " << ctx.infer(H) << "\n"; for (unsigned i = 6; i < args.size(); i++) { // congr_fun : ∀ {α : Sort u_1} {β : α → Sort u_2} {f g : Π (x : α), β x}, f = g → ∀ (a : α), f a = g a expr f_type = ctx.relaxed_whnf(ctx.infer(f)); diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index 16f6350cfc..dbf063eaf4 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -80,34 +80,39 @@ class add_basic_inductive_decl_fn { bool gen_cases_on = get_inductive_cases_on(m_opts); bool gen_no_confusion = get_inductive_no_confusion(m_opts); - if (is_inductive_predicate(m_env, ind_name)) - m_env = mk_drec(m_env, ind_name); + // if (is_inductive_predicate(m_env, ind_name)) + // m_env = mk_drec(m_env, ind_name); + lean_trace(name({"inductive_compiler"}), tout() << ">> generate rec_on\n";); if (gen_rec_on) m_env = mk_rec_on(m_env, ind_name); if (has_unit) { + lean_trace(name({"inductive_compiler"}), tout() << ">> generate cases_on\n";); if (gen_cases_on) m_env = mk_cases_on(m_env, ind_name); if (gen_cases_on && gen_no_confusion && has_eq && has_heq) { + lean_trace(name({"inductive_compiler"}), tout() << ">> generate no_confusion\n";); m_env = mk_no_confusion(m_env, ind_name); + lean_trace(name({"inductive_compiler"}), tout() << ">> generate injective\n";); m_env = mk_injective_lemmas(m_env, ind_name); } if (gen_brec_on && has_prod) { + lean_trace(name({"inductive_compiler"}), tout() << ">> generate below\n";); m_env = mk_below(m_env, ind_name); + lean_trace(name({"inductive_compiler"}), tout() << ">> generate ibelow\n";); m_env = mk_ibelow(m_env, ind_name); } } if (gen_brec_on && has_unit && has_prod) { + lean_trace(name({"inductive_compiler"}), tout() << ">> generate brec_on\n";); m_env = mk_brec_on(m_env, ind_name); + lean_trace(name({"inductive_compiler"}), tout() << ">> generate binduction_on\n";); m_env = mk_binduction_on(m_env, ind_name); } - - // if (!m_is_meta) - // m_env = mk_has_sizeof(m_env, ind_name); } void send_to_kernel() { @@ -151,6 +156,7 @@ environment add_basic_inductive_decl(environment const & env, options const & op } void initialize_inductive_compiler_basic() { + register_trace_class(name({"inductive_compiler"})); register_trace_class(name({"inductive_compiler", "basic"})); register_trace_class(name({"inductive_compiler", "basic", "ind"})); register_trace_class(name({"inductive_compiler", "basic", "irs"})); diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 07ebc86dc1..ead1c0564c 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -1242,7 +1242,7 @@ class add_nested_inductive_decl_fn { expr e = m_tctx.relaxed_whnf(lhs); buffer rec_args; expr rec_fn = get_app_args(e, rec_args); - if (is_constant(rec_fn, get_eq_rec_name())) { + if (is_constant(rec_fn, get_eq_ndrec_name())) { lean_assert(rec_args.size() == 6); simp_result r_first = force_eq_rec(rec_fn, rec_args); simp_result r_rest = force_recursors_core(r_first.get_new()); @@ -1254,7 +1254,7 @@ class add_nested_inductive_decl_fn { simp_result force_eq_rec(expr const & rec_fn, buffer const & rec_args) { // See comments above prove_eq_rec_invertible(type_context_old & ctx, expr const & e) at equation_compiler/util.cpp. - lean_assert(is_constant(rec_fn, get_eq_rec_name()) && rec_args.size() == 6); + lean_assert(is_constant(rec_fn, get_eq_ndrec_name()) && rec_args.size() == 6); expr B = rec_args[0]; expr from = rec_args[1]; /* (f (g (f a))) */ expr C = rec_args[2]; @@ -1300,16 +1300,16 @@ class add_nested_inductive_decl_fn { expr f_x_eq_f_a = mk_eq(m_tctx, f_x, f_a); expr H = aux_locals.push_local("_H", f_x_eq_f_a); expr h_x = mk_app(h, x); - /* (@eq.rec B (f x) C (h x) (f a) H) */ + /* (@eq.ndrec B (f x) C (h x) (f a) H) */ expr eq_rec2 = mk_app(rec_fn, {B, f_x, C, h_x, f_a, H}); - /* (@eq.rec B (f x) C (h x) (f a) H) = h a */ + /* (@eq.ndrec B (f x) C (h x) (f a) H) = h a */ expr eq_rec2_eq = mk_eq(m_tctx, eq_rec2, h_a); /* (fun x : A, (forall H : f x = f a, @eq.rec B (f x) C (h x) (f a) H = h a)) */ expr pr_motive = m_tctx.mk_lambda(x, m_tctx.mk_pi(H, eq_rec2_eq)); expr g_f_eq_a = mk_app(m_tctx, g_f_name, a); /* (eq.symm (g_f_eq a)) */ expr pr_major = mk_eq_symm(m_tctx, g_f_eq_a); - expr pr = mk_app(mk_constant(get_eq_rec_name(), {mk_level_zero(), A_lvl}), + expr pr = mk_app(mk_constant(get_eq_ndrec_name(), {mk_level_zero(), A_lvl}), {A, a, pr_motive, pr_minor, g_f_a, pr_major, major}); return simp_result(h_a, pr); } @@ -1668,7 +1668,7 @@ class add_nested_inductive_decl_fn { assert_type_correct(m_outer.m_env, rest); assert_type_correct(m_outer.m_env, equality_proof); - return mk_eq_rec(m_outer.m_tctx, motive, rest, equality_proof); + return mk_eq_ndrec(m_outer.m_tctx, motive, rest, equality_proof); } public: diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 5558083c4b..b45a28ad72 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -95,7 +95,7 @@ static vm_obj rewrite_core(expr h, expr e, rewrite_cfg const & cfg, tactic_state } catch (exception & ex) { throw nested_exception("rewrite tactic failed, motive is not type correct", std::current_exception()); } - expr prf = mk_eq_rec(ctx, motive, mk_eq_refl(ctx, e), h); + expr prf = mk_eq_ndrec(ctx, motive, mk_eq_refl(ctx, e), h); tactic_state new_s = set_mctx_goals(s, ctx.mctx(), append(cons(head(s.goals()), to_list(new_goals)), tail(s.goals()))); return tactic::mk_success(mk_vm_pair(to_obj(new_e), mk_vm_pair(to_obj(prf), to_obj(to_list(metas)))), new_s); } diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 77b0bfde91..373dceb3e2 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -170,7 +170,7 @@ expr simplify_core_fn::remove_unnecessary_casts(expr const & e) { buffer cast_args; expr f_cast = get_app_args(args[i], cast_args); name n_f = const_name(f_cast); - if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name()) { + if (n_f == get_eq_ndrec_name() || n_f == get_eq_rec_name()) { lean_assert(cast_args.size() == 6); expr major_premise = cast_args[5]; expr f_major_premise = get_app_fn(major_premise); diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index 6abfb8e2b3..a3e82fdfc9 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -95,7 +95,7 @@ expr subst(environment const & env, options const & opts, transparency_mode cons expr major = symm ? H2 : mk_eq_symm(ctx2, H2); expr mvar3 = ctx2.mk_metavar_decl(lctx, new_type); expr minor = mvar3; - expr new_val = depH2 ? mk_eq_drec(ctx2, motive, minor, major) : mk_eq_rec(ctx2, motive, minor, major); + expr new_val = depH2 ? mk_eq_rec(ctx2, motive, minor, major) : mk_eq_ndrec(ctx2, motive, minor, major); mctx = ctx2.mctx(); mctx.assign(*mvar2, new_val); expr mvar4 = clear(mctx, mvar3, H2); diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index fff9f8de1b..c9d0b20fd1 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -102,8 +102,6 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional num_args, major_pos, params_pos, indices_pos, produce_motive); } else if (is_aux_recursor(env, r) && (strcmp(r.get_string(), "cases_on") == 0 || - strcmp(r.get_string(), "dcases_on") == 0 || - strcmp(r.get_string(), "drec_on") == 0 || strcmp(r.get_string(), "rec_on") == 0 || strcmp(r.get_string(), "brec_on") == 0)) { name I = r.get_prefix(); diff --git a/src/library/util.cpp b/src/library/util.cpp index fa05239f0f..9e5972205f 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -720,9 +720,16 @@ expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs) { return mk_app(mk_constant(get_heq_name(), {lvl}), A, lhs, B, rhs); } -bool is_eq_rec_core(expr const & e) { +bool is_eq_ndrec_core(expr const & e) { expr const & fn = get_app_fn(e); - return is_constant(fn) && const_name(fn) == get_eq_rec_name(); + return is_constant(fn) && const_name(fn) == get_eq_ndrec_name(); +} + +bool is_eq_ndrec(expr const & e) { + expr const & fn = get_app_fn(e); + if (!is_constant(fn)) + return false; + return const_name(fn) == get_eq_ndrec_name(); } bool is_eq_rec(expr const & e) { @@ -732,13 +739,6 @@ bool is_eq_rec(expr const & e) { return const_name(fn) == get_eq_rec_name(); } -bool is_eq_drec(expr const & e) { - expr const & fn = get_app_fn(e); - if (!is_constant(fn)) - return false; - return const_name(fn) == get_eq_drec_name(); -} - bool is_eq(expr const & e) { return is_app_of(e, get_eq_name(), 3); } @@ -1066,18 +1066,12 @@ expr mk_bool_tt() { return *g_bool_tt; } expr mk_bool_ff() { return *g_bool_ff; } expr to_bool_expr(bool b) { return b ? mk_bool_tt() : mk_bool_ff(); } -name get_dep_recursor(environment const & env, name const & n) { - if (is_inductive_predicate(env, n)) - return name(n, "drec"); - else - return name(n, "rec"); +name get_dep_recursor(environment const &, name const & n) { + return name(n, "rec"); } -name get_dep_cases_on(environment const & env, name const & n) { - if (is_inductive_predicate(env, n)) - return name(n, "dcases_on"); - else - return name(n, "cases_on"); +name get_dep_cases_on(environment const &, name const & n) { + return name(n, "cases_on"); } static char const * g_aux_meta_rec_prefix = "_meta_aux";