mathlib documentation

meta.coinductive_predicates

source
meta def monotonicity  :
(user_attribute unit)

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

source
theorem monotonicity.imp {p p' q q' : Prop} (h₁ : implies p' q') (h₂ : implies q p) :
implies (p → p') (q → q')

source
theorem monotonicity.const (p : Prop) :
implies p p

source
theorem monotonicity.true (p : Prop) :
implies p true

source
theorem monotonicity.false (p : Prop) :
implies false p

source
theorem monotonicity.exists {α : Sort u} {p q : α → Prop} (h : ∀ (a : α), implies (p a) (q a)) :
implies (∃ (a : α), p a) (∃ (a : α), q a)

source
theorem monotonicity.and {p p' q q' : Prop} (hp : implies p p') (hq : implies q q') :
implies (p ∧ q) (p' ∧ q')

source
theorem monotonicity.or {p p' q q' : Prop} (hp : implies p p') (hq : implies q q') :
implies (p ∨ q) (p' ∨ q')

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

source
meta def tactic.mono (e : expr) (hs : list expr) :
tactic unit

source
meta structure tactic.add_coinductive_predicate.coind_rule  :
Type

source
meta structure tactic.add_coinductive_predicate.coind_pred  :
Type

source
meta def tactic.add_coinductive_predicate.coind_pred.u_params (pd : tactic.add_coinductive_predicate.coind_pred) :
list level

source
meta def tactic.add_coinductive_predicate.coind_pred.f₁_l (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.f₂_l (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.pred (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.func (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.func_g (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.pred_g (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.impl_locals (pd : tactic.add_coinductive_predicate.coind_pred) :
list expr

source
meta def tactic.add_coinductive_predicate.coind_pred.impl_params (pd : tactic.add_coinductive_predicate.coind_pred) :
list expr

source
meta def tactic.add_coinductive_predicate.coind_pred.le (pd : tactic.add_coinductive_predicate.coind_pred) (f₁ f₂ : expr) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.corec_functional (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.mono (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.rec' (pd : tactic.add_coinductive_predicate.coind_pred) :
tactic expr

source
meta def tactic.add_coinductive_predicate.coind_pred.construct (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.destruct (pd : tactic.add_coinductive_predicate.coind_pred) :
expr

source
meta def tactic.add_coinductive_predicate.coind_pred.add_theorem (pd : tactic.add_coinductive_predicate.coind_pred) (n : name) (type : expr) (tac : tactic unit) :
tactic expr

source
meta def tactic.add_coinductive_predicate (u_names : list name) (params : list expr) (preds : list (expr × list expr)) :
tactic unit

source
meta def tactic.coinductive_predicate (meta_info : interactive.decl_meta_info) (_x : interactive.parse (lean.parser.tk "coinductive")) :
lean.parser unit

source
meta def tactic.coinduction (rule : expr) (ns : list name) :
tactic unit

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

Current version: do not support mutual inductive rules

source
meta def tactic.interactive.coinduction (corec_name : interactive.parse lean.parser.ident) (ns : interactive.parse interactive.types.with_ident_list) (revert : interactive.parse (lean.parser.tk "generalizing" *> lean.parser.ident * )?) :
tactic unit