fix(tactic/apply): fix ordering of goals produced by apply (#3777)

src/tactic/apply.lean

@@ -30,8 +30,9 @@ namespace tactic
 `new_g` to rearrange the dependent goals to either drop them, push them to the end of the list
 or leave them in place. The `bool` values in `gs` indicates whether the goal is dependent or not. -/
 def reorder_goals {α} (gs : list (bool × α)) : new_goals → list α
-| new_goals.non_dep_first := (gs.filter $ coe ∘ bnot ∘ prod.fst).map prod.snd ++
-  (gs.filter $ coe ∘ prod.fst).map prod.snd
+| new_goals.non_dep_first :=
+  let ⟨dep,non_dep⟩ := gs.partition (coe ∘ prod.fst) in
+  non_dep.map prod.snd ++ dep.map prod.snd
 | new_goals.non_dep_only := (gs.filter (coe ∘ bnot ∘ prod.fst)).map prod.snd
 | new_goals.all := gs.map prod.snd
 
@@ -61,7 +62,7 @@ focus1 (do {
      unify t tgt,
      exact e,
      gs' ← get_goals,
-     let r := reorder_goals gs cfg.new_goals,
+     let r := reorder_goals gs.reverse cfg.new_goals,
      set_goals (gs' ++ r.map prod.snd),
      return r }) <|>
 do (expr.pi n bi d b) ← infer_type e >>= whnf | apply_core e cfg,

test/apply.lean

@@ -7,9 +7,9 @@ example : ∀ n m : ℕ, n + m = m + n :=
 begin
   apply' nat.rec,
   -- refine nat.rec _ _,
+  { intro m, ring },
   { intros n h m,
     ring, },
-  { intro m, ring }
 end
 
 instance : partial_order unit :=
@@ -22,16 +22,21 @@ instance : partial_order unit :=
 
 example : unit.star ≤ unit.star :=
 begin
+  have u : unit := unit.star,
   apply' le_trans,
   -- refine le_trans _ _,
   -- exact unit.star,
-  refl', refl'
+  do { gs ← tactic.get_goals, guard (gs.length = 3) },
+  change () ≤ u,
+  all_goals { cases u, refl', } ,
   -- refine le_refl _, refine le_refl _,
 end
 
 example {α β : Type*} [partial_order β] (x y z : α → β) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
 begin
-  transitivity'; assumption
+  transitivity',
+  do { gs ← tactic.get_goals, guard (gs.length = 2) },
+  exact h₀, exact h₁,
 end
 example : continuous (λ (x : ℝ), x + x) :=
 begin
@@ -40,3 +45,11 @@ begin
   guard_target' continuous (λ (x : ℝ), x), apply @continuous_id ℝ _,
   -- guard_target' has_continuous_add ℝ, admit,
 end
+
+example (y : ℝ) : continuous (λ (x : ℝ), x + y) :=
+begin
+  apply' continuous.add,
+  guard_target' continuous (λ (x : ℝ), x), apply @continuous_id ℝ _,
+  guard_target' continuous (λ (x : ℝ), y), apply @continuous_const ℝ _ _,
+  -- guard_target' has_continuous_add ℝ, admit,
+end