search

u5943321 / ETCSprover

0 stars 0 forks source link

match_mp_tac desired features #3

Open u5943321 opened 3 years ago

u5943321 commented 3 years ago

Work for chained implication like:

f o h = g o h ==> eqa(f, g) o x0 = h ==> x0 = eqinduce(f, g, h): thm

u5943321 commented 3 years ago

want solve

(A : ob), (B : ob), (f : A -> B), (g : A -> B), (i : 0 -> A) f o i = g o i, isiso(i)

f = g

from the thm

(A : ob), (B : ob), (C : ob), (f : B -> C), (g : B -> C), (i : A -> B)

|- isiso(i) & f o i = g o i ==> f = g: thm

TODO: bug match_mp if use match_mp_tac o_iso_eq_eq, then # Exception- ERR "VALIDInvalid tactic: theorem has extra variable involved i" raised

The i is the i:A->B, not the one from 0, and i is not matched anywhere.

u5943321 commented 3 years ago

TODO: match_mp_tac iso_trans gives the wrong thing (A : ob), (X : ob), (Y : ob) Y areiso A, X areiso A

X areiso Y & Y areiso Y

u5943321 commented 3 years ago

Let A areiso 0 ==> ~EXISTS (x : 1 -> A). T(): thm

work for goal F

u5943321 commented 3 years ago

Transform ALL B. areiso(B?, 0) ==> ALL A. ALL (f : A? -> B?). areiso(A?, 0) into ALL B. ALL A. areiso(B?, 0) /\ ?f:A->B. T ==> areiso(A,0)

u5943321 commented 3 years ago

match_mp_tac iso_trans gives the wrong thing (A : ob), (X : ob), (Y : ob) Y areiso A, X areiso A

X areiso Y & Y areiso Y