Make proofs from a congruence closure #
The monad for the cc
tactic stores the current state of the tactic.
Equations
Instances For
Run a computation in the CCM
monad.
Equations
Instances For
Update the cache
field of the state.
Equations
Instances For
Read the cache
field of the state.
Equations
Instances For
Use the normalizer to normalize e
.
If no normalizer was configured, returns e
itself.
Equations
Instances For
Return the root expression of the expression's congruence class.
Equations
Instances For
Is e
the root of its congruence class?
Equations
Instances For
Return true iff the given function application are congruent
e₁
should have the form f a
and e₂
the form g b
.
See paper: Congruence Closure for Intensional Type Theory.
Try to find a congruence theorem for an application of fn
with nargs
arguments, with support
for HEq
.
Equations
Instances For
Treat the entry associated with e
as a first-order function.
Equations
Instances For
Update the modification time of the congruence class of e
.
In a delayed way, apply symmetry to H
, which is an Eq
or a HEq
.
- If
heqProofs
is true, ensure the result is aHEq
(otherwise it is assumed to beEq
). - If
flipped
is true, applysymm
, otherwise keep the same direction.
Equations
Instances For
Are e₁
and e₂
known to be in the same equivalence class?
Equations
Instances For
Is e₁ ≠ e₂
known to be true?
Note that this is stronger than not (isEqv e₁ e₂)
:
only if we can prove they are distinct this returns true
.
Equations
Instances For
Is the proposition e
known to be true?
Equations
Instances For
Is the proposition e
known to be false?
Equations
Instances For
Use congruence on arguments to prove lhs = rhs
.
That is, tries to prove that lhsFn lhsArgs[0] ... lhsArgs[n-1] = lhsFn rhsArgs[0] ... rhsArgs[n-1]
by showing that lhsArgs[i] = rhsArgs[i]
for all i
.
Fails if the head function of lhs
is not that of rhs
.
If e₁ : R lhs₁ rhs₁
, e₂ : R lhs₂ rhs₂
and lhs₁ = rhs₂
, where R
is a symmetric relation,
prove R lhs₁ rhs₁
is equivalent to R lhs₂ rhs₂
.
- if
lhs₁
is known to equallhs₂
, returnnone
- if
lhs₁
is not known to equalrhs₂
, fail.
Turn a delayed proof into an actual proof term.
Use the format of H
to try and construct a proof or lhs = rhs
:
Build a proof for a = b
. Fails if a
and b
are not known to be equal.
Equations
Instances For
Return the proof of e₁ = e₂
using ac_rfl
tactic.
Equations
Instances For
Given tr := t*r
sr := s*r
tEqs : t = s
, return a proof for tr = sr
We use a*b
to denote an AC application. That is, (a*b)*(c*a)
is the term a*a*b*c
.
Equations
Instances For
Given e := lhs * r
and H : lhs = rhs
, return rhs * r
and the proof of e = rhs * r
.
Equations
Instances For
The single step of simplifyAC
.
Simplifies an expression e
by either simplifying one argument to the AC operator, or the whole
expression.
Equations
Instances For
If e
can be simplified by the AC module, return the simplified term and the proof term of the
equality.