search

data61 / PSL

Other
65 stars 9 forks source link

Abduction: another filter of bad conjectures (false assumption) #195

Closed yutakang closed 11 months ago

yutakang commented 1 year ago

Since we are not using the cases tactic, the case_tac tactic, or any explicit conjecturing that introduces meta-assumptions, when a conjecture has a meta-assumption that is equivalent to False even though the original goal does not contain a meta-assumption that is equivalent to False, then the conjecture is bad.

yutakang commented 1 year ago

An example for this is qrevflat var_0 nil2 = var_1 ==> qrevflat var_0 (x var_2 nil2) = x var_1 var_2 in Prop-28.

yutakang commented 1 year ago

Probably these harmful conjectures are produced by proof by induction followed by some explicit conjecturing.

yutakang commented 11 months ago

This was done a while ago.