leodemoura/lean — pull request #3 by soonhokong (2013-09-24 02:15:31+00:00)
Title: Rewrite module

Leo,

Could you take a look at the code when you have some time? It contains theorem/orelse/then rewriters. One thing I changed from the discussion that we had is the type of rewriter. Now it's

RW : (CTX * term * type) -> (term * proof)

I've added 'type' part to handle 'then' case. To construct the proof for 'then' case, we need to use 'Trans' whose definition is as follows.

Trans (A : Type U) (a b c : A) (H1 : a = b) (H2 : b = c) : a = c := Trans H1 H2

Without 'type' of the term, we can think of some solutions:

1) I might just put H1 and H2 with four placeholders (for A, a, b, c) and call lean elaborator to fill the placeholders. But to do so, we need to pass frontend and as an argument (right?).
2) I could infer the type of the term using type_checker. But we still need to pass environment.
3) Explicitly pass the type. This is the option that I implemented.

Do you think this is a good one? If you have any better idea?

Also, do you think we need to add 'type' to the rhs? I mean,

RW : (CTX * term * type) -> (term * type * proof)

to support theorems which has a heterogeneous equality? But to do so, we still need to infer type of the rewritten term. This requires an environment again..

Thank you,
Soonho