# mathlibdocumentation

meta.coinductive_predicates

meta def monotonicity  :
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₂ : p) :
implies (p → p') (q → q')
theorem monotonicity.const (p : Prop) :
p
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 : p') (hq : q') :
implies (p q) (p' q')
theorem monotonicity.or {p p' q q' : Prop} (hp : p') (hq : q') :
implies (p q) (p' q')
theorem monotonicity.not {p q : Prop} (h : q) :
implies (¬q) (¬p)
meta def tactic.mono (e : expr) (hs : list expr) :
meta def tactic.compact_relation  :
list × list

compact_relation bs as_ps: Product a relation of the form: R := λ as, ∃ bs, Λ_i a_i = p_i[bs] This relation is user visible, so we compact it by removing each b_j where a p_i = b_j, and hence a_i = b_j. We need to take care when there are p_i and p_j with p_i = p_j = b_k.

meta def tactic.add_coinductive_predicate (u_names : list name) (params : list expr) (preds : list ) :
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