From 77c20e99ff1ba662514249a23bfa8f7dbbc0e4fd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 14 May 2015 23:32:54 +0200 Subject: [PATCH] feat(library/tactic/inversion_tactic): consistent orientation of generated equalities Generated equalities in proof irrelevant environments were inverted compared with the documentation and the proof relevant case, which resulted in newly generated local vars replacing equivalent old ones instead of the other way around. --- library/init/nat.lean | 4 ++-- src/library/tactic/inversion_tactic.cpp | 8 ++++---- tests/lean/cases_tac.lean | 4 ++-- tests/lean/cases_tac.lean.expected.out | 10 +++++----- tests/lean/run/inversion1.lean | 4 ++-- tests/lean/run/vector.lean | 8 ++++---- 6 files changed, 19 insertions(+), 19 deletions(-) diff --git a/library/init/nat.lean b/library/init/nat.lean index 7a37e4a1f..e2c694cca 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -138,9 +138,9 @@ namespace nat theorem le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b := begin - cases H with b' hlt, + cases H with b hlt, apply H₁, - apply H₂ b' hlt + apply H₂ b hlt end theorem lt.irrefl (a : nat) : ¬ a < a := diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 59d7fef91..bf420eafc 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -156,10 +156,10 @@ class inversion_tac { constraint_seq cs; if (m_tc.is_def_eq(lhs_type, rhs_type, justification(), cs) && !cs) { return mk_pair(mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs), - mk_app(mk_constant(get_eq_refl_name(), to_list(l)), rhs_type, rhs)); + mk_app(mk_constant(get_eq_refl_name(), to_list(l)), lhs_type, lhs)); } else { return mk_pair(mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs), - mk_app(mk_constant(get_heq_refl_name(), to_list(l)), rhs_type, rhs)); + mk_app(mk_constant(get_heq_refl_name(), to_list(l)), lhs_type, lhs)); } } @@ -274,7 +274,7 @@ class inversion_tac { expr t_type = binding_domain(d); expr t = mk_local(m_ngen.next(), g.get_unused_name(t_prefix, nidx), t_type, binder_info()); expr const & index = I_args[i]; - add_eq(t, index); + add_eq(index, t); h_new_type = mk_app(h_new_type, t); hyps.push_back(t); ts.push_back(t); @@ -282,7 +282,7 @@ class inversion_tac { } expr h_new = mk_local(m_ngen.next(), h_new_name, h_new_type, local_info(h)); if (m_dep_elim) - add_eq(h_new, h); + add_eq(h, h_new); hyps.push_back(h_new); expr new_type = Pi(eqs, g.get_type()); expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps); diff --git a/tests/lean/cases_tac.lean b/tests/lean/cases_tac.lean index e84ccb53d..cb7456f2c 100644 --- a/tests/lean/cases_tac.lean +++ b/tests/lean/cases_tac.lean @@ -13,7 +13,7 @@ mk : Π a b : A, foo₂ a b example (A : Type) (B : A → Type) (f : A → A) (a : A) (H : foo₂ (f a) a) (Hb : H = H) (Hc : a = a) : A := begin - cases H with [c, d], + cases H, state, - exact d + exact a end diff --git a/tests/lean/cases_tac.lean.expected.out b/tests/lean/cases_tac.lean.expected.out index 3a160486a..2926b0c60 100644 --- a/tests/lean/cases_tac.lean.expected.out +++ b/tests/lean/cases_tac.lean.expected.out @@ -1,14 +1,14 @@ cases_tac.lean:7:2: proof state A : Type, B : A → Type, -a_1 : A, -Hb : B a_1 +a : A, +Hb : B a ⊢ A cases_tac.lean:17:2: proof state A : Type, B : A → Type, f : A → A, -d : A, -Hc : d = d, -Hb : foo₂.mk (f d) d = foo₂.mk (f d) d +a : A, +Hc : a = a, +Hb : foo₂.mk (f a) a = foo₂.mk (f a) a ⊢ A diff --git a/tests/lean/run/inversion1.lean b/tests/lean/run/inversion1.lean index f246488e7..fcfbc2022 100644 --- a/tests/lean/run/inversion1.lean +++ b/tests/lean/run/inversion1.lean @@ -13,8 +13,8 @@ namespace fin (f : fin (succ n)) : C n f := begin cases f, - apply (H₁ n_1), - apply (H₂ n_1 a) + apply (H₁ n), + apply (H₂ n a) end end fin diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean index 9ac6f64e3..94061c22c 100644 --- a/tests/lean/run/vector.lean +++ b/tests/lean/run/vector.lean @@ -107,14 +107,14 @@ namespace vector @vector.brec_on A P n w (λ (n : nat) (w : vector A n), begin - cases w with [n₁, h₁, t₁], + cases w with [n', h₁, t₁], show @below A P zero vnil → vector B zero → vector C zero, from λ b v, vnil, - show @below A P (succ n₁) (h₁ :: t₁) → vector B (succ n₁) → vector C (succ n₁), from + show @below A P (succ n') (h₁ :: t₁) → vector B (succ n') → vector C (succ n'), from λ b v, begin - cases v with [n₂, h₂, t₂], - have r : vector B n₂ → vector C n₂, from pr₁ b, + cases v with [n', h₂, t₂], + have r : vector B n' → vector C n', from pr₁ b, exact ((f h₁ h₂) :: r t₂), end end) v