mathlib documentation

meta.coinductive_predicates

theorem monotonicity.pi {α : Sort u} {p q : α → Prop} (h : ∀ (a : α), implies (p a) (q a)) :
implies (∀ (a : α), p a) (∀ (a : α), q a)
theorem monotonicity.imp {p p' q q' : Prop} (h₁ : implies p' q') (h₂ : implies q p) :
implies (p → p') (q → q')
theorem monotonicity.const (p : Prop) :
theorem monotonicity.true (p : Prop) :
theorem monotonicity.false (p : Prop) :
theorem monotonicity.exists {α : Sort u} {p q : α → Prop} (h : ∀ (a : α), implies (p a) (q a)) :
implies (∃ (a : α), p a) (∃ (a : α), q a)
theorem monotonicity.and {p p' q q' : Prop} (hp : implies p p') (hq : implies q q') :
implies (p q) (p' q')
theorem monotonicity.or {p p' q q' : Prop} (hp : implies p p') (hq : implies q q') :
implies (p q) (p' q')
theorem monotonicity.not {p q : Prop} (h : implies p q) :
implies (¬q) (¬p)
meta def tactic.mono (e : expr) (hs : list expr) :
meta def tactic.add_coinductive_predicate (u_names : list name) (params : list expr) (preds : list (expr × list expr)) :
meta def tactic.coinduction (rule : expr) (ns : list name) :

Prepares coinduction proofs. This tactic constructs the coinduction invariant from the quantifiers in the current goal.

Current version: do not support mutual inductive rules