match_mp_tac desired features

[u5943321]

Work for chained implication like:

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

[u5943321]

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]

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]

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

work for goal F

[u5943321]

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]

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