feat(init/meta/congr_tactic.lean): tactic to apply congruence rules

library/init/meta/congr_tactic.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2017 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+-/
+prelude
+import init.meta.tactic init.meta.congr_lemma init.meta.relation_tactics init.function
+
+namespace tactic
+
+meta def apply_congr_core (clemma : congr_lemma) : tactic unit :=
+do assert `H_congr_lemma clemma.type,
+   exact clemma.proof,
+   get_local `H_congr_lemma >>= apply,
+   all_goals $ get_local `H_congr_lemma >>= clear
+
+meta def apply_eq_congr_core (tgt : expr) : tactic unit :=
+do (lhs, rhs) ← match_eq tgt,
+   guard lhs.is_app,
+   clemma ← mk_specialized_congr_lemma lhs,
+   apply_congr_core clemma
+
+meta def apply_heq_congr_core (tgt : expr) : tactic unit :=
+do (lhs, rhs) ← (match_eq tgt <|> do (α, lhs, β, rhs) ← match_heq tgt, return (lhs, rhs)),
+   guard lhs.is_app,
+   clemma ← mk_hcongr_lemma lhs.get_app_fn lhs.get_app_num_args,
+   apply_congr_core clemma
+
+meta def apply_rel_iff_congr_core (tgt : expr) : tactic unit :=
+do (lhs, rhs) ← match_iff tgt,
+   guard lhs.is_app,
+   clemma ← mk_rel_iff_congr_lemma lhs.get_app_fn,
+   apply_congr_core clemma
+
+meta def apply_rel_eq_congr_core (tgt : expr) : tactic unit :=
+do (lhs, rhs) ← match_eq tgt,
+   guard lhs.is_app,
+   clemma ← mk_rel_eq_congr_lemma lhs.get_app_fn,
+   apply_congr_core clemma
+
+meta def congr_core : tactic unit :=
+do tgt ← target,
+   apply_eq_congr_core tgt
+   <|> apply_heq_congr_core tgt
+   <|> fail "congr tactic failed"
+
+meta def rel_congr_core : tactic unit :=
+do tgt ← target,
+   apply_rel_iff_congr_core tgt
+   <|> apply_rel_eq_congr_core tgt
+   <|> fail "rel_congr tactic failed"
+
+meta def congr : tactic unit :=
+do focus1 (congr_core >> all_goals (try reflexivity >> try congr))
+
+meta def rel_congr : tactic unit :=
+do focus1 (rel_congr_core >> all_goals (try reflexivity))
+
+end tactic

library/init/meta/default.lean

@@ -15,4 +15,4 @@ import init.meta.simp_tactic init.meta.set_get_option_tactics
 import init.meta.interactive init.meta.converter init.meta.vm
 import init.meta.comp_value_tactics init.meta.smt
 import init.meta.async_tactic init.meta.ref init.meta.coinductive_predicates
-import init.meta.hole_command
+import init.meta.hole_command init.meta.congr_tactic

library/init/meta/expr.lean

@@ -286,6 +286,10 @@ meta def is_or : expr → option (expr × expr)
 | `(or %%α %%β) := some (α, β)
 | _             := none
 
+meta def is_iff : expr → option (expr × expr)
+| `((%%a : Prop) ↔ %%b) := some (a, b)
+| _                     := none
+
 meta def is_eq : expr → option (expr × expr)
 | `((%%a : %%_) = %%b) := some (a, b)
 | _                    := none

library/init/meta/tactic.lean

@@ -578,6 +578,12 @@ match (expr.is_or e) with
 | none     := fail "expression is not a disjunction"
 end
 
+meta def match_iff (e : expr) : tactic (expr × expr) :=
+match (expr.is_iff e) with
+| (some (lhs, rhs)) := return (lhs, rhs)
+| none              := fail "expression is not an iff"
+end
+
 meta def match_eq (e : expr) : tactic (expr × expr) :=
 match (expr.is_eq e) with
 | (some (lhs, rhs)) := return (lhs, rhs)

tests/lean/run/congr_tactic.lean

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2017 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+-/
+open tactic
+
+namespace test1
+-- Recursive with props and subsingletons
+
+constants (α β γ : Type) (P : α → Prop) (Q : β → Prop) (SS : α → Type)
+          (SS_ss : ∀ (x : α), subsingleton (SS x))
+          (f : Π (x : α), P x → β → SS x → γ) (p₁ p₂ : ∀ (x : α), P x) (h : β → β) (k₁ k₂ : ∀ (x : α), SS x)
+
+attribute [instance] SS_ss
+
+example (x₁ x₂ x₁' x₂' x₃ x₃' : α) (y₁ y₁' : β) (H : y₁ = y₁') :
+f x₁ (p₁ x₁) (h $ h $ h y₁) (k₁ x₁) = f x₁ (p₂ x₁) (h $ h $ h y₁') (k₂ x₁) :=
+begin
+congr,
+exact H,
+end
+
+end test1
+
+namespace test2
+
+-- Specializing to the prefix with props and subsingletons
+constants (γ : Type) (f : Π (α : Type*) (β : Sort*), α → β → γ)
+          (X : Type) (X_ss : subsingleton X)
+          (Y : Prop)
+
+attribute [instance] X_ss
+
+example (x₁ x₂ : X) (y₁ y₂ : Y) : f X Y x₁ y₁ = f X Y x₂ y₂ := by congr
+
+end test2
+
+namespace test3
+-- Edge case: goal proved by apply, not refl
+constants (f : ℕ → ℕ)
+
+example (n : ℕ) : f n = f n := by congr
+
+end test3
+
+namespace test4
+-- Heq result
+
+constants (α : Type) (β : α → Type) (γ : Type) (f : Π (x : α) (y : β x), γ)
+
+example (x x' : α) (y : β x) (y' : β x') (H_x : x = x') (H_y : y == y') : f x y = f x' y' :=
+begin
+congr,
+exact H_x,
+exact H_y
+end
+
+end test4
+
+namespace test5
+-- heq in the goal
+constants (α : Type) (β : α → Type) (γ : Π (x : α), β x → Type) (f : Π (x : α) (y : β x), γ x y)
+
+example (x x' : α) (y : β x) (y' : β x') (H_x : x = x') (H_y : y == y') : f x y == f x' y' :=
+begin
+congr,
+exact H_x,
+exact H_y
+end
+
+end test5
+
+namespace test6
+-- iff relation
+
+constants (α : Type*)
+          (R : α → α → Prop)
+          (R_refl : ∀ x, R x x)
+          (R_symm : ∀ x y, R x y → R y x)
+          (R_trans : ∀ x y z, R x y → R y z → R x z)
+
+attribute [refl] R_refl
+attribute [symm] R_symm
+attribute [trans] R_trans
+
+example (x₁ x₁' x₂ x₂' : α) (H₁ : R x₁ x₁') (H₂ : R x₂ x₂') : R x₁ x₂ ↔ R x₁' x₂' :=
+begin
+rel_congr,
+exact H₁,
+exact H₂
+end
+
+-- eq relation
+example (x₁ x₁' x₂ x₂' : α) (H₁ : R x₁ x₁') (H₂ : R x₂ x₂') : R x₁ x₂ = R x₁' x₂' :=
+begin
+rel_congr,
+exact H₁,
+exact H₂
+end
+
+end test6