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

@@ -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 :=

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);

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

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,
+a : A,
-Hb : B a_1
+Hb : B a
 ⊢ A
 cases_tac.lean:17:2: proof state
 A : Type,
 B : A → Type,
 f : A → A,
-d : A,
+a : A,
-Hc : d = d,
+Hc : a = a,
-Hb : foo₂.mk (f d) d = foo₂.mk (f d) d
+Hb : foo₂.mk (f a) a = foo₂.mk (f a) a
 ⊢ A

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),
-    apply (H₂ n_1 a)
+    apply (H₂ n a)
   end
 
 end fin

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₂],
+           cases v with [n', h₂, t₂],
-           have r : vector B n₂ → vector C n₂, from pr₁ b,
+           have r : vector B n' → vector C n', from pr₁ b,
            exact ((f h₁ h₂) :: r t₂),
          end
      end) v