Hi Lu, I saw that Thomas already provided a solution. Here's another simpler proof of your example goal:
val th = prove( ``!p1 p2. PEQ p1 p2 ==> PEQ p2 p3 ==> PEQ p1 p3``, SIMP_TAC std_ss [PEW_cases,FORALL_PROD]) where PEW_cases came from: > val (PEQ_rules, PEQ_ind, PEW_cases) = Hol_reln ` > (!l1:num a1:num l2:num a2:num. (l1 = l2) ==> PEQ (l1,a1) (l2,a2))` Cheers, Magnus 2009/10/16 Lu Zhao <[email protected]>: > Hi, > > I'm having a problem in matching pairs when using inductive relation for > proof. It can be demonstrated by the following example. > > Suppose I define a relation: > > val (PEQ_rules, PEQ_ind, PEW_cases) = Hol_reln ` > (!l1:num a1:num l2:num a2:num. (l1 = l2) ==> PEQ (l1,a1) (l2,a2))` > > val [PEQ_INS] = CONJUNCTS PEQ_rules > > Then, I'd like to prove the following goal: > > g`!p1 p2 p3. PEQ p1 p2 ==> PEQ p2 p3 ==> PEQ p1 p3` > > Everything is fine, after these two tactics: > > NTAC 3 STRIP_TAC THEN > RULE_INDUCT_THEN PEQ_ind ASSUME_TAC ASSUME_TAC > > However, problem begins to show up. I need to change the tuple of > (l2,a2) into a single variable in order to use RULE_INDUCT_THEN one more > time. However, this obscures the relation of "l2 = FST p3." > RULE_INDUCT_THEN introduces a free variable for (FST p3), which is not > related to l2, resulting in the failure of proof. > > `?p2. (l2,a2) = p2` by METIS_TAC [] \\ ASM_REWRITE_TAC [] > RULE_INDUCT_THEN PEQ_ind ASSUME_TAC ASSUME_TAC > > RULE_TAC PEQ_INS > > This example may be resolved by using Define for PEQ, but I'm deal with > sets and other customized operations which do not have a constructor. > Using inductive relation is the only option in my mind. Any method to > solve this or an alternative way is very welcomed. > > Thank you very much. > Lu > > ------------------------------------------------------------------------------ > Come build with us! The BlackBerry(R) Developer Conference in SF, CA > is the only developer event you need to attend this year. Jumpstart your > developing skills, take BlackBerry mobile applications to market and stay > ahead of the curve. Join us from November 9 - 12, 2009. Register now! > http://p.sf.net/sfu/devconference > _______________________________________________ > Hol-developers mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-developers > ------------------------------------------------------------------------------ Come build with us! The BlackBerry(R) Developer Conference in SF, CA is the only developer event you need to attend this year. Jumpstart your developing skills, take BlackBerry mobile applications to market and stay ahead of the curve. Join us from November 9 - 12, 2009. Register now! http://p.sf.net/sfu/devconference _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
