Michael Soegtrop (Sep 20 2020 at 17:08): Michael Soegtrop (Sep 20 2020 at 17:08):I have a question on reduction in the type of a tintro. I tried to do the following:
TT.tintro (fun c : rcbv <some reducible mess> => TT.demote)
When I run this with mrun I get the hypothesis:
c : rcbv <some reducible mess>
But I would like to have the type of c cbv reduced as if I would do a cbv in c after the mrun. I also tried to use `@TT.tintro (rcbv <some reducible mess>) but the result is the same.
How can I achieve a reduction in the type of c?
Janno (Sep 21 2020 at 08:40):reduce and all derived functions are only actually reduced if they are let bound and in a position of type M _. So for your example I recommend let binding rcbv ... before the call to TT.tintro. Does that work?
Michael Soegtrop (Sep 21 2020 at 10:00):Does that work?
Not immediately. I get some issues with dependent types. What I have is:
(TT.tintro (fun b : b_type =>
let a_type := rcbv (<a_type_expr - depends on b>) in
(TT.tintro (fun a : a_type =>
TT.demote
))))
and I get:
b : b_type
a_type := rcbv (<a_type_expr - depends on b>) : Type
The term "tintro (fun a : a_type => demote)" has type "ttac (forall x : a_type, ?P1 x)"
while it is expected to have type "ttac (?P0 b)"
(cannot instantiate "?P0" because "a_type" is not in its scope: available arguments are <some vars outside of this>)
If I substitute rcbv (<a_type_expr - depends on b>) for a_type it works. I guess I somehow need to explicitly state the dependency on b but I start to feel I need an Agda style editor ;-)
Janno (Sep 21 2020 at 13:26):Ah, that is unfortunate.. I've been running into this particular issue a lot recently and I wonder why Coq doesn't just reduce the binding.
Beta Ziliani (Sep 21 2020 at 13:41):I'm busy chasing some unsoundness bugs (one is solved, but another one is under inspection). what happens if you do let a_type b := ... and then tintro (fun a : a_type b => ...)?
Michael Soegtrop (Sep 21 2020 at 13:49):I agree that it is unexpected that simply let abstracting a term breaks the type checking. What does type check is introducing an additional function abstraction as in:
(TT.tintro (fun b : b_type =>
(TT.tintro (fun a => let a_type := rcbv (<a_type_expr - depends on b>) in
(fun a' : a_type => TT.demote) a
))))
but then I again get the unreduced type for the Hypothesis.
@Beta Ziliani : checking ...
Beta Ziliani (Sep 21 2020 at 13:51):wanna gist it and we'll make it work?
Janno (Sep 21 2020 at 13:56):That would still leave an unreduced application I suppose, wouldn't it?
Michael Soegtrop (Sep 21 2020 at 13:56):@Beta Ziliani : For your suggestion I get the same error "a_type" is not in its scope.
Since I cannot publish the stuff I am working on and since it is a bit of work to get to this level of complexity, it would be a bit of work to come up with a gist. @Janno : since you said you had similar issues recently, do you have something which can be published? If not I will see what I can do. It might make sense to construct a little play ground also for tutorial purposes.
Michael Soegtrop (Sep 21 2020 at 13:58):@Janno: the result is the same - I do apply the inner function to the argument of the outer function and mrun has to reduce it to get to the demote, I guess.
Beta Ziliani (Sep 21 2020 at 15:01):I'll try to reproduce. It doesn't sound so complicated to me the code (a couple of tintro's with a reduced type in the second one)
Beta Ziliani (Sep 21 2020 at 19:22):OK, this works, although it requires repeating in the type the let-binding:
Definition test: ttac (forall x, 2 + x > 0 -> True) :=
tintro (fun y=>
let e := rcbv (2 + y > 0) in
(tintro (fun _ : e => demote)
: let e := rcbv (2 + y > 0) in ttac (2 + y > 0 -> True))).
Goal forall x, 2 + x > 0 -> True.
MProof.
(match_goal with
| [[ |- forall x, 2 + x > 0 -> True]] => test
end)%MC%TT.
(of course test can be embedded in the match_goal, I just did it like that to fight one thing at a time with the typechecker)
Michael Soegtrop (Sep 21 2020 at 20:33):@Beta Ziliani thanks! This works as long as the inner tactic is just demote - when I exchange this with apply some_lemma <**> demote it fails to typecheck when I replace the type of the function argument with a let define of the same term. I guess I can fix that by putting in an additional type spec, but it gets a but unwieldy then.
Btw.: I also tried to do a let directly in the type as in
(TT.tintro (fun b : b_type =>
(TT.tintro (fun a => (fun a' : (let a_type := rcbv (<a_type_expr - depends on b>) in a_type) => TT.demote) a
))))
This type checks but it doesn't do the simplification. Shouldn't this work? Maybe mrun doesn't look for lets in types?
Beta Ziliani (Sep 21 2020 at 20:46):Sorry, I'm not sure I understand. This works:
Definition test: ttac (forall x, 2 + x > 0 -> True /\ True) :=
tintro (fun y=>
let e := rcbv (2 + y > 0) in
(tintro (fun _ : e => apply (@conj _ _) <**> apply I <**> demote)
: let e := rcbv (2 + y > 0) in ttac (2 + y > 0 -> True /\ True))).
@Beta Ziliani : My case is a bit more complicated in that some parameter of the lemma I apply depend on the computed type, which is then not in scope for the lemma application.
Can you tell why the let immediately in the type, that is (fun x : (let t := rcbv <type expr> in t) => ...) does not do the reduction in the type? It does type check, so if this would do the reduction, this would be the easiest solution. Does it match your expectation that the rcbv reduction is not done although it is inside of a let assignment?
Btw.: In your term you can remove the second let binding - the bound variable e is not used in the in expression. So it is a bit simpler than it looks.
Janno (Sep 22 2020 at 08:22):The rcbv call does not match the second condition: the let binding needs to be in position of type M _. (Actually, the condition is that the let binding needs to be in the execution path of the metaprogram. That means it needs to be "in the way" of running the program.)
Michael Soegtrop (Sep 22 2020 at 09:06):@Janno: Thanks for the explanation! I am not sure what you mean by "position of type M _" but the explanation of "in the execution path" is clear.
I will try to wrap the intro + simplify operation into one function - maybe I can steer type checking into the right direction this way.
Janno (Sep 22 2020 at 09:13):Ah, I just mean that the overall type of the let binding needs to be M <something>.
Janno (Sep 22 2020 at 09:14):I suppose that means the let binding's body (not the term that is bound but its continuation) needs to be of type M <something>
Janno (Sep 22 2020 at 09:14):It's not really a sufficient condition. The intuition about the execution path is the correct one so if you only remember that one you'll be fine :)
Michael Soegtrop (Sep 22 2020 at 09:52):@Janno : hmm, I guess I need both "in the execution path" and "of type M _". I tried this:
Definition tintro_cbv (A : Type) {P} (f: forall (x:A), ttac (P x))
: ttac (forall (x:A), P x) :=
M.nu (FreshFrom f) mNone (fun x=>
let A_cbv := rcbv A in
'(m: v, gs) <- f (x : A_cbv);
a <- M.abs_fun x v;
b <- T.close_goals x (mmap (fun g=>(m: tt, g)) gs);
let b := mmap msnd b in
M.ret (m: a, b)).
This works in the sense that it type checks and that I see the rcbv in the type of the introduced hypothesis (it is not in the value I give for parameter A), but it does not execute the rcbv - I guess because the type is not M _. I tried to fix this by using rcbv (M.ret A) and trying to get the type with bind, but this is beyond my current skill level.
Michael Soegtrop (Sep 22 2020 at 09:55):Btw.: in @Beta Ziliani 's example let e := rcbv (2 + y > 0) in the argument of rcbv does not have type M _ either, but there it does the reduction. I am confused ...
Janno (Sep 22 2020 at 10:41):It's the continuation that needs to be of type M _, not the let-bound term.
Janno (Sep 22 2020 at 10:41):I really don't know the right words to describe what I mean. Sorry about that.
Janno (Sep 22 2020 at 10:42):f in your code is hardcoded to A so I am afraid the cast to the reduced A won't make any difference.
Janno (Sep 22 2020 at 10:43):I had no idea this stuff would be so complicated..
Michael Soegtrop (Sep 22 2020 at 13:52):@Janno
It's the continuation that needs to be of type M _, not the let-bound term.
Ah you mean the term after the in in a let ... in ... needs to be of type M _? As physicist I lack a bit the vocabulary of logicians.
so I am afraid the cast to the reduced A won't make any difference.
Well it does make a difference in so far as the rcbv is actually visible in the generated hypothesis. Without the cast the rcbv is not there. As far as I understand this the type of x is unified with A but assuming this unification works the type remains what I casted it to. I will put in some prints - maybe this helps me to understand what is going on.
So to summarize I need to make the in term of type M _?
Janno (Sep 22 2020 at 13:58):So to summarize I need to make the in term of type M _?
Yes, and the whole things needs to be run, i.e. executed.
Michael Soegtrop (Sep 22 2020 at 16:09):@Janno : I put in a few prints in the tintro_cbv function. I see the reduced term printed, but I see rcbv term as type of the hypothesis.
I guess what happens is that the type is determined during type checking before execution with mrun, so it does see the rcbv bot not the evaluated term. More thinking ... I guess I have to sneak in the mrun evaluation during type checking with eval somehow.
Janno (Sep 22 2020 at 16:15):I guess I have to sneak in the mrun evaluation during type checking with eval somehow.
I don't think that will work. The actual value of A is only (I assume) only known at tactic runtime, not a tactic typechecking time. Sadly I don't have time right now to look into this more but I hope I can make some time soon.
Michael Soegtrop (Sep 22 2020 at 17:30):Tadaaa - this simple solution does work:
Definition tintro_cbv2 (A : Type) {P} (f: forall (x:A), ttac (P x))
: ttac (forall (x:A), P x) :=
let A_cbv := rcbv A in @tintro A_cbv P f.
I can't say I understand why, though - it is more a result of random walk black box exploration ...
Beta Ziliani (Sep 22 2020 at 17:35):Ha! you bit me! I was going to try that same thing, although I was going to parametrize the reduction strategy because why not. It works because the type is the same of tintro, although the actual introduction is performed with the reduced type.
Michael Soegtrop (Sep 22 2020 at 17:35):Applied to the example of @Beta Ziliani :
From Mtac2 Require Import Mtac2 Ttactics Sorts.
Import TT TT.notations.
Definition tintro_cbv2 (A : Type) {P} (f: forall (x:A), ttac (P x))
: ttac (forall (x:A), P x) :=
let A_cbv := rcbv A in @tintro A_cbv P f.
Definition test: ttac (forall x, 2 + x > 0 -> True) :=
tintro (fun y => tintro_cbv2 (2 + y > 0) (fun _ => demote)).
Goal forall x, 2 + x > 0 -> True.
MProof.
(match_goal with
| [[ |- forall x, 2 + x > 0 -> True]] => test
end)%MC%TT.
although I was going to parametrize the reduction strategy because why not
Yes, for a final solution I would also do this. I also think one doesn't need to make the parameter A explicit - in the above adoption to your example I can also give _ to tintro_cbv2. So one can have a tintro_red with the same interface as tintro, just with an additional reduction strategy.
So Mtac2 is really pretty cool - thank's for it! What is missing are some more intricate example - I guess I will find something on my way soon which can be isolated.
Last updated: Feb 06 2023 at 05:03 UTC