Hello,
2018-01-08 18:08 GMT+01:00 Michael Beeson <profbee...@gmail.com>:
> Falling script can be run after loading vectors.ml
>
>
> # let lemma300 = VECTOR_ARITH `!x:real^2 y:real^2 z:real^2. (x + y = z)
> <=> (y = z-x)`;;
>
> val lemma300 : thm = |- !x y z. x + y = z <=> y = z - x
>
> # let test = ASSUME `!a:real^2 b:real^2 c:real^2 d:real^2 . tarea(d,a,b)
> + tarea(c,a,d) = tarea(a,b,c)`;;
>
The problem is in the previous line. The type of + is inferred by
overloading.
Hence you need a type annotation to force the inference
`(+):real^2->real^2->real^2.
For instance (notice the annotation :real^2 added at the end):
let test = ASSUME `!a:real^2 b:real^2 c:real^2 d:real^2.
tarea(d,a,b) + tarea(c,a,d) = tarea(a,b,c):real^2`;;
Now the rewrite works as expected:
REWRITE_RULE[lemma300] test;;
val it : thm = !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
|- !a b c d. tarea (c,a,d) = tarea (a,b,c) - tarea (d,a,b)
Marco
> val test : thm = !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
>
> |- !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
>
> # REWRITE_RULE[lemma300] test;;
>
> val it : thm = !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
>
> |- !a b c d. tarea (d,a,b) + tarea (c,a,d) = tarea (a,b,c)
>
> #
>
>
> I was expecting
>
> tarea(c,a,d) = tarea(a,b,c)-tarea(d,a,b) in the conclusion
>
> (and maybe in the assumptions too). Note that no type variables
>
> are involved, so whatever the problem is here, it has nothing to do
>
> with type variables.
>
>
>
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
