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?

`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?

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

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.

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 => ...)`

?

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

wanna gist it and we'll make it work?

That would still leave an unreduced application I suppose, wouldn't it?

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

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

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)

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)

@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?

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.

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

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

Ah, I just mean that the overall type of the let binding needs to be `M <something>`

.

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

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

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

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

It's the continuation that needs to be of type `M _`

, not the let-bound term.

I really don't know the right words to describe what I mean. Sorry about that.

`f`

in your code is hardcoded to `A`

so I am afraid the cast to the reduced `A`

won't make any difference.

I had no idea this stuff would be so complicated..

@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 _`

?

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.

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

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.

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

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.

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