mathlib docs: meta.coinductive

source

meta def monotonicity :

(user_attribute unit)

source

theorem monotonicity.pi {α : Sort u} {p q : α → Prop} :

(∀ (a : α), implies (p a) (q a)) → implies (∀ (a : α), p a) (∀ (a : α), q a)

source

theorem monotonicity.imp {p p' q q' : Prop} :

implies p' q' → 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} :

(∀ (a : α), implies (p a) (q a)) → implies (∃ (a : α), p a) (∃ (a : α), q a)

source

theorem monotonicity.and {p p' q q' : Prop} :

implies p p' → implies q q' → implies (p ∧ q) (p' ∧ q')

source

theorem monotonicity.or {p p' q q' : Prop} :

implies p p' → implies q q' → implies (p ∨ q) (p' ∨ q')

source

theorem monotonicity.not {p q : Prop} :

implies p q → implies (¬q) (¬p)

source

meta def tactic.mono :

expr → list expr → tactic unit

source

meta structure tactic.add_coinductive_predicate.coind_rule :

Type

orig_nm : name
func_nm : name
type : expr
loc_type : expr
args : list expr
loc_args : list expr
concl : expr
insts : list expr

source

meta structure tactic.add_coinductive_predicate.coind_pred :

Type

u_names : list name
params : list expr
pd_name : name
type : expr
intros : list tactic.add_coinductive_predicate.coind_rule
locals : list expr
f₁ : expr
f₂ : expr
u_f : level

source

meta def tactic.add_coinductive_predicate.coind_pred.u_params :

tactic.add_coinductive_predicate.coind_pred → list level

source

meta def tactic.add_coinductive_predicate.coind_pred.f₁_l :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.f₂_l :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.pred :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.func :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.func_g :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.pred_g :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.impl_locals :

tactic.add_coinductive_predicate.coind_pred → list expr

source

meta def tactic.add_coinductive_predicate.coind_pred.impl_params :

tactic.add_coinductive_predicate.coind_pred → list expr

source

meta def tactic.add_coinductive_predicate.coind_pred.le :

tactic.add_coinductive_predicate.coind_pred → expr → expr → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.corec_functional :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.mono :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.rec' :

tactic.add_coinductive_predicate.coind_pred → tactic expr

source

meta def tactic.add_coinductive_predicate.coind_pred.construct :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.destruct :

tactic.add_coinductive_predicate.coind_pred → expr

source

meta def tactic.add_coinductive_predicate.coind_pred.add_theorem :

tactic.add_coinductive_predicate.coind_pred → name → expr → tactic unit → tactic expr

source

meta def tactic.add_coinductive_predicate :

list name → list expr → list (expr × list expr) → tactic unit

source

meta def tactic.coinductive_predicate :

interactive.decl_meta_info → interactive.parse (lean.parser.tk "coinductive") → lean.parser unit

source

meta def tactic.coinduction :

expr → 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 :

interactive.parse lean.parser.ident → interactive.parse interactive.types.with_ident_list → interactive.parse (optional (lean.parser.tk "generalizing" *> lean.parser.many lean.parser.ident)) → tactic unit

mathlib documentation

meta.coinductive_predicates

General documentation

Additional documentation

Library

mathlib documentation

meta.​coinductive_predicates

General documentation

Additional documentation

Library

meta.coinductive_predicates