search

u5943321 / ETCSprover

0 stars 0 forks source link

Parser bugs summary #2

Open u5943321 opened 3 years ago

u5943321 commented 3 years ago

"ALL X. ALL Y. ALL f0. ALL f1. isrefl(f0:X->Y,f1:X->Y) <=> EXISTS d:Y->X.f0 o d = id(Y) & f1 o d = id(Y)" fvf it; val it = HOLset{("f0", ar (Bound 3, Bound 2)), ("f0", ar (Bound 4, Bound 3)), ("f1", ar (Bound 3, Bound 2)), ("f1", ar (Bound 4, Bound 3))}: (string * sort) set,

rapf "!X.!Y.!f0.!f1. isrefl(f0:X->Y,f1:X->Y) <=> ?d:Y->X.f0 o d = id(Y) & f1 o d = id(Y)"; fvf it = {} rapf "!X.!Y.!f0.!f1. isrefl(f0:X->Y,f1:X->Y) <=> ?d:Y->X.f0 o d = id(Y) & f1 o d = id(Y)" = rpf "!X.!Y.!f0.!f1. isrefl(f0:X->Y,f1:X->Y) <=> ?d:Y->X.f0 o d = id(Y) & f1 o d = id(Y)"; val it = true: bool no extra change.

u5943321 commented 3 years ago

rapg "~ (i1(X,X) o (t:1->X) = i2(X,X) o t)":

Exception- UNIFY "occurs check(pt):pv X : psv 1 ptu 1" raised

also need the "()" after "~"

after previous change, have:

rapf "~i1(X,X) o (t:1->X) = i2(X,X) o t" = rpf "~ i1(X,X) o (t:1->X) = i2(X,X) o t"; and checked rpf does not need () as well, and works well with (), but do no extra edit.

u5943321 commented 3 years ago

rapf "P(a) & P(b) ==> ALL s.Q(s) & Q(c)"; Exception- ERR "err in parsing bound variable" raised

not a problem, not accpeted by the parser because s is a constant, maybe raise a more helpful error message here.

u5943321 commented 3 years ago

val f1 = rapf "~(EXISTS x1 : 1 -> X. EXISTS x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1)"; Exception- UNIFY "occurs check(pt):pv X : psv 0 ptu 0" raised

rapf "~(?x1 : 1 -> X.?x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1)" = rpf "~(?x1 : 1 -> X.?x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1)"; val it = true: bool

rapf "~?x1 : 1 -> X.?x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1" = rpf "~(?x1 : 1 -> X.?x0 : 1 -> X. i2(X, X) o t = i1(X, X) o x0 & i2(X, X) o (t:1->X) = i2(X, X) o x1)"; val it = true: bool

nothing extra.

u5943321 commented 3 years ago

rapf "p2(A, B) o g:X->A * B = p2(A, B) o f" not an infix operator

rapf "p2(A, B) o g:X->(A B) = p2(A, B) o f" = rpf "p2(A, B) o (g:X->A B)= p2(A, B) o f"; val it = true: bool

() around A * B is critical. other wise it misread the formula and UNIFY complains. no extra change.

u5943321 commented 3 years ago

rapf "((i:B->A) o m:A-> B) o h = (i o m) o g" Exception- ERR "not an infix operator" raised

fixed 2021-6-30 2.47

u5943321 commented 3 years ago

(rapf "h = eqinduce (f1:A-> B,f2,eqa(f1,f2) o g:X -> eqo(f1,f2))")

not an infix operator error

rapf "h = eqinduce (f1:A-> B,f2,eqa(f1,f2) o g:X -> eqo(f1,f2))" = rpf "h = eqinduce (f1:A-> B,f2,eqa(f1,f2) o g:X -> eqo(f1,f2))"; val it = true: bool

previous error caused by prec of : -> is too low.

u5943321 commented 3 years ago

(rapg "~(copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1)))")

Exception- UNIFY "occurs check(pt):i1 psv 4(1 pob,1 pob) ptu 4" raised

rapf "~(copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1)))" = rpf "~(copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1)))"; val it = true: bool

rapf "~copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1))" = rpf "~(copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1)))"; val it = true: bool rapf "~copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1))" = rpf "~copa(i1(1,1),i2(1,1)) = copa(i2(1,1),i1(1,1))"; val it = true: bool

after the edits, no extra change to fix this.

u5943321 commented 3 years ago

rapf "~(EXISTS x0:1->A. a o x0 = x)"; Exception- UNIFY "occurs check(pt):pv x0 : (1 pob,pob)-->(pv A : psv 0,pob) ptu 0" raised

fixed in 2021-6.30 2 commit around 2.37.

u5943321 commented 3 years ago

rapf "h o <id(AN),(f:AN->B)> = (f:A * N ->B) o <p1(A,N),s o p2(A,N)>"

if do not annotate the first f, it thinks the f is to C.

have rpf "h o pa(id(A N),f) = f o pa(p1(A,N),s o p2(A,N))" = rapf "h o <id(A N),(f:(A N)->B)> = (f:(A N) ->B) o <p1(A,N),s o p2(A,N)>"; val it = true: bool

rpf "h o pa(id(A N),f) = f o pa(p1(A,N),s o p2(A,N))" = rapf "h o <id(A N),f> = (f:(A * N) ->B) o <p1(A,N),s o p2(A,N)>"; val it = true: bool

after the previous edits, but do nothing extra.

u5943321 commented 3 years ago

just record:

readf gives: val it = Pred ("<=>", [Var ("f", ob), Var ("g", ob)]): form no need to edit if done with rapf.

u5943321 commented 3 years ago

Think new parser is okay now, but want it to read formulas as !a b c (f:A->C)....

u5943321 commented 3 years ago

"!A.!B.!X.!fg: X -> (A * B).!f: X -> A.!g: X -> B. p1(A,B) o fg = f & p2(A,B) o fg = g <=> fg = pa(f,g)"

need (A * B)

u5943321 commented 3 years ago

want parser to parse !f:A B ->C g:C->D. How to distinguish the space in A B and the space between C and g?

u5943321 commented 3 years ago

fvt (rastt"x0: X -> eqo(f:A->B,g)"); val it = HOLset{("A", ob), ("B", ob), ("X", ob), ("f", A -> B), ("g", ob), ("x0", X -> eqo(f, g))}: (string * sort) set

fvt (rastt"x0: X -> eqo(f:A->B,g:A->B)"); val it = HOLset{("A", ob), ("B", ob), ("X", ob), ("f", A -> B), ("g", A -> B), ("x0", X -> eqo(f, g))}: (string * sort) set

u5943321 commented 3 years ago

fvt (rastt"x0: X -> eqo(f:A->B,g)"); val it = HOLset{("A", ob), ("B", ob), ("X", ob), ("f", A -> B), ("g", ob), ("x0", X -> eqo(f, g))}: (string * sort) set

fvt (rastt"x0: X -> eqo(f:A->B,g:A->B)"); val it = HOLset{("A", ob), ("B", ob), ("X", ob), ("f", A -> B), ("g", A -> B), ("x0", X -> eqo(f, g))}: (string * sort) set

fixed

u5943321 commented 3 years ago

rapf "!X. ~ areiso(X,0) ==> ?x: 1 -> X. T"; val it = !X. ~areiso(X#, 0) ==> ?(x : 1 -> X#). T: form

assume it; val it =

!X. ~areiso(X#, 0) ==> ?(x : 1 -> X#). T |- !X. ~areiso(X#, 0) ==> ?(x : 1 -> X#). T: thm

spec_all it; val it = (X : ob) !X. ~areiso(X#, 0) ==> ?(x : 1 -> X#). T |- ~areiso(X, 0) ==> ?(x : 1 -> X). T: thm contrapos it; Exception- ERR ("contrapos.not a implication: ", [], [], [Conn ("~", [Conn ("==>", [Pred ("areiso", [X, 0]), Quant ("?", "x", 1 -> X, Pred ("T", []))])])]) raised

u5943321 commented 3 years ago

al i1_i2_disjoint' = (A : ob), (B : ob), (c1 : A -> B + B), (c2 : ob), (ca : B + B -> coeqo(c1, c2)), (t : 1 -> eqo(ca o i1(B, B), ca o i2(B, B)))

|- i1(eqo((ca o i1(B, B)), (ca o i2(B, B))), eqo((ca o i1(B, B)), (ca o i2(B, B)))) o t = i2(eqo((ca o i1(B, B)), (ca o i2(B, B))), eqo((ca o i1(B, B)), (ca o i2(B, B)))) o t ==> F: thm

val i1_i2_disjoint' = i1_i2_disjoint |> specl [rastt "eqo((ca: (B + B) -> coeqo(c1:A-> (B + B),c2)) o i1(B, B), ca o i2(B, B))", rastt "t:1->eqo((ca: (B + B) -> coeqo(c1:A->(B + B),c2)) o i1(B, B), ca o i2(B, B))"] |> eqF_intro |> dimpl2r

u5943321 commented 3 years ago

But rastt "ca: (B + B) -> coeqo(c1:A-> (B + B),c2)" is parsed correctly (c2.)

u5943321 commented 3 years ago

(rapf "k' o i1(B,B) o q' = (k':(B+B)->coeqo(c1,c2)) o i2(B,B) o q':eqo(c3,c4:B->coeqo(c1,c2:A->(B+B))) -> B")

assume it; val it = (B : ob), (c1 : ob), (c2 : ob), (c3 : ob), (c4 : B -> coeqo(c1, c2)), (k' : B + B -> coeqo(c1, c2)), (q' : eqo(c3, c4) -> B) k' o i1(B, B) o q' = k' o i2(B, B) o q' |- k' o i1(B, B) o q' = k' o i2(B, B) o q': thm

u5943321 commented 3 years ago

rapf "c40= c4:B->coeqo(c1,c2:A->(B+B))"; val it = c40 = c4: form

rapf "q0 :eqo(c3,c4) -> B= q':eqo(c3,c4:B->coeqo(c1,c2:A->(B+B))) -> B"; Exception- TER ("match_sort.cannot match ob with ar: ", [ar (Var ("A", ob), Var ("B", ob)), ob], []) raised rapf "q0 :eqo(c3,c4:B->coeqo(c1,c2:A->(B+B))) -> B= q':eqo(c3,c4) -> B"; val it = q0 = q': form assume it; val it = (A : ob), (B : ob), (c1 : A -> B + B), (c2 : A -> B + B), (c3 : B -> coeqo(c1, c2)), (c4 : B -> coeqo(c1, c2)), (q' : eqo(c3, c4) -> B), (q0 : eqo(c3, c4) -> B) q0 = q' |- q0 = q': thm

u5943321 commented 3 years ago

rastt "eqa(q0 :eqo(c3,c4:B->coeqo(c1,c2:X->Y)) -> B, q':eqo(c3,c4) -> B)"; Exception- TER ("match_sort.cannot match ob with ar: ", [ar (Var ("A", ob), Var ("B", ob)), ob], []) raised