mathlib3 documentation

meta.coinductive_predicates

meta def monotonicity :

(user_attribute unit)

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) :

implies false p

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 structure tactic.add_coinductive_predicate.coind_rule :

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

meta structure tactic.add_coinductive_predicate.coind_pred :

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

meta def tactic.add_coinductive_predicate.coind_pred.u_params (pd : tactic.add_coinductive_predicate.coind_pred) :

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

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

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

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

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

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

meta def tactic.add_coinductive_predicate.coind_pred.impl_locals (pd : tactic.add_coinductive_predicate.coind_pred) :

meta def tactic.add_coinductive_predicate.coind_pred.impl_params (pd : tactic.add_coinductive_predicate.coind_pred) :

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

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

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

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

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

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

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

meta def tactic.compact_relation :

list expr → list (expr × expr) → list expr × list (expr × expr)

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 (expr × list expr)) :

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

lean.parser unit

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

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