The equational compiler was failing to generate equational lemmas for
equations such as:
def f : nat → nat → nat
| (x+1) (y+1) := f (x+10) y
| _ _ := 1
It would fail when trying to prove the following equation:
forall x, f 0 x = 1
using a "refl" proof. This equation does not hold definitionally.
It is not blocked by the internal pattern matching based on the
cases_on recursor, but it is blocked by the outer most brec_on
used to implement structural recursion. The solution is to
"complete" the set of equations. So, the structural_rec
module will replace the equation above with
def f : nat → nat → nat
| (x+1) (y+1) := f (x+10) y
| _ 0 := 1
| _ (y+1) := 1
and then (as before)
def f : Pi (x y : nat), below y → nat
| (x+1) (y+1) F := F^.fst^.fst (x+10)
| _ 0 F := 1
| _ (y+1) F := 1
@gebner I used the __builtin_expect trick to optimize the vm_nat module.
Most of the time, we are processing small numbers.
In the following example, the runtime went from 7.27 secs to 6.6 secs
on my machine.
def mk (a : nat) : nat → list nat
| 0 := []
| (nat.succ n) := a :: mk n
def Sum : list nat → nat → nat
| [] r := r
| (n::ns) r := Sum ns (r + n)
def loop : nat → nat → nat
| s 0 := s
| s (nat.succ n) := loop (s + (Sum (mk (n % 2) 1000000) 0)) n
vm_eval timeit "time" $ loop 0 30
Suppose we have
def foo : some_proposition :=
by non_trivial_automation
Moreover, assume non_trivial_automation generates a huge proof.
Since this definition is marked with `def`, it is sent to the VM
compiler. In this kind of scenario, the compiler preprocessor was
spending a long time applying "useless" preprocessing steps.
We say they are useless because in the end everything is erased.
I think we should make sure every definition has some bytecode
associated with it in the VM even if the type of the definition
is a proposition. In this way, we have a simple invariant:
every definition has a vm_decl associated with it.
So, we workaround the performance problem above by short-circuiting
the preprocessor for propositions.
There were two performance bottlenecks in the recursive equation
compiler. Both bottlenecks were due to conversion checking.
1- We allow patterns such as (x+1) in the left-hand-side of a
recursive equation. This is kind of pattern has to be reduced
since it is not a constructor. Moreover, when we are trying to
compile using structural recursion, we need to find an element
that is structurally smaller in recursive applications.
Again, we need to use reduction since the pattern may be (x+2),
and in the recursive application we have (x+1). Now, consider
the following equation
f (x+1) (y+1) := f complex_term y
It will first check whether complex_term is structurally smaller
than (x+1), and the compiler will timeout trying to reduce
complex_term.
This commit adds the following workaround. The structural
recursion module from now on will only unfold reducible constants
and constants marked as patterns. This is not a complete
solution. It will timeout in the following equation:
f (x+1) (y+1) := f (x+1000000000000) y
For this one, we need to add a whnf "fuel" option to type_context
2- Equational lemma generation was producing lemmas that are too
expensive to check. Suppose we the following two definitions
| f x 0 := 1
| f x (y+1) := f complex_term y
and
| g 0 y := 1
| g (x+1) y := g x complex_term
Before this commit, we would generate the following proofs for
the second equation of each definition:
eq.refl (f complex_term y)
eq.refl (g x complex_term)
This proof triggers the following definitionally equality test:
f x (y+1) =?= f complex_term y
g (x+1) y =?= g x complex_term
Since, we have f/g on both sides, the type checker will try
first to unify the arguments, and may timeout trying to solve
x =?= complex_term
y =?= complex_term
since it may take a long time to reduce `complex_term`.
We workaround this problem by creating a slightly different
proof.
eq.refl (unfold_of(f x (y+1)))
eq.refl (unfold_of(g (x+1) y))
where unfold_of(t) is the result of applying one delta reduction
step.
