mathlib documentation

meta.coinductive_predicates

theorem monotonicity.pi {α : Sort u} {p q : α → Prop} :
(∀ (a : α), implies (p a) (q a))implies (∀ (a : α), p a) (∀ (a : α), q a)

theorem monotonicity.imp {p p' q q' : Prop} :
implies p' q'implies q pimplies (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} :
(∀ (a : α), implies (p a) (q a))implies (∃ (a : α), p a) (∃ (a : α), q a)

theorem monotonicity.and {p p' q q' : Prop} :
implies p p'implies q q'implies (p q) (p' q')

theorem monotonicity.or {p p' q q' : Prop} :
implies p p'implies q q'implies (p q) (p' q')

theorem monotonicity.not {p q : Prop} :
implies p qimplies (¬q) (¬p)

meta def tactic.mono  :

meta def tactic.coinduction  :

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

Current version: do not support mutual inductive rules