mathlib3 documentation

meta.coinductive_predicates

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

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.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