[MetaPRL Users] Term extraction problem

[Aleksey Nogin]

Hi Wojtek,

On 31.08.2006 10:43, Wojtek Moczydlowski wrote:

 > The tutorial tells me to use
> term_of_extract command, but then I get the following message:
[...]
>             # term_of_extract [];;
>             Incomplete proof: /wojtek/impl_elim

The term_of_extract function was originally added as a "low-level" 
function (for debugging purposes primarily) and it does not fully 
validate its inputs, which is leading to the wrong error message here. 
The real problem is that when using in on a derived rule that has 
assumptions, the argument to the term_of_extract needs to get the list 
of extracts for each of the assumptions.

For example, if you have a derived rule of a form:

sequent { <H>; 'A >- 'B } -->
sequent { <H> >- ...}

then the term_of_extract will need to take a singleton list with the 
extract schema for the assumption, as in:

term_of_extract [ << sequent { <H>; x: 'A >- 'f<|H|>['x] } >> ]

If you would want to use the command-line proof extraction more often, 
we can add a more user-friendly version of this function. For now, I 
fixed the function to give a more meaningful error message:

> # cd "/itt_test/extraction_test"
> /itt_tests/itt_test/extraction_test : string
> # refine autoT
> 
> * <*>
> ....main....
> <Γ>; A Type; B Type; C Type ⊢ (A ∧ B ═⇒ C) ═⇒ A ═⇒ B ═⇒ C
> 
> BY autoT
> 
> () : unit
> # term_of_extract [];;
> <Γ>; A Type; B Type; C Type ⊢ λ_.λ_.λ_._ (_,_) : term
> # term_of_extract [<<'x>>];;
> Refine error:
>     Refine.extract_term:
>        itt_test!extraction_test
>        - supplied assumption extracts list length mismatch -
>        assumptions in rule/rewrite: 0
>        received assumption extracts: 1

P.S. BTW, in MetaPRL command line, contrary to how it is done in OCaml, 
the ";;" at the end of the line is optional.

-- 
Aleksey Nogin

Home Page: http://nogin.org/
E-Mail: nogin at cs.caltech.edu (office), aleksey at nogin.org (personal)
Office: Moore 04, tel: (626) 395-2200