#with_goal tactic#1430
Conversation
There was a problem hiding this comment.
Hi Jean-Paul.
-
If there are problems with assume, please open an issue with an example, and propose a separate PR to solve that problem.
-
A more general approach to with_goal, not requiring gconf.ml, would be to generate a unification problem goal == Prf ?M, solve it to instantiate ?M and, in case of success, handle the tactic (t ?M).
Yes but I suppose this would need another tactic to solve the unification problem automatically.
| let rec as_prop g = | ||
| match is_prf g with | ||
| | Some u -> u | ||
| | None -> match g with |
There was a problem hiding this comment.
matching on terms must always be of the form match unfold t with ...
| match is_prf g with | ||
| | Some u -> u | ||
| | None -> match g with | ||
| | Prod(p,bi) when binder_name bi = "_" -> |
There was a problem hiding this comment.
testing binder_names is not sound; you should use binder_occur instead
| require open tests.OK.Tactic; | ||
|
|
||
| injective symbol σ: Prop → Set; | ||
| rule π $P ↪ τ (σ $P); |
There was a problem hiding this comment.
Using this, a unique profile for #assume can be used for both Set and Prop. The idea is to say that each object of type Prop can itself be seen as a type, which is given by the function σ.
|
I see the problem with assume. I'll fix it this afternoon. |
2 participants
The tactic term with_goal (only available in eval) calls its parameter tactic with the current goal seen as a Prop. It uses builtins to transform lambdapi Pi and -> into 1st order forall and =>.
I have also modified assume - the created variable was not passed to the tactic and the type of #refine in Tactic.lp
In order to use #assume for both sets and props, I have added in the test example a conversion \sigma from Prop to Set. It would be better to convert both Prop and Set to Type: TYPE