[isabelle-dev] Stymied by cryptic failure in Product_type.thy
Lars Noschinski
noschinl at in.tum.de
Tue Feb 18 08:19:56 CET 2014
On 17.02.2014 19:55, Josh Tilles wrote:
> I'm experimenting with separating the intuitionistic parts of HOL from
> the classical parts. (If anyone is interested, I'd be happy to
> describe my goals and/or motivations in more detail; for now I'll
> stick to just the problem description)
> Renaming HOL.thy to IHOL.thy did not cause any problems. I.e.,
> `./bin/isabelle build HOL` still succeeded after commit 122bc618d6
> <https://github.com/MerelyAPseudonym/isabelle/tree/122bc618d65927d16877b1107e91224ba3bfbaf8>.
> I then started extracting everything in (I)HOL.thy that depended on
> the axiom `True_or_False` to a file named CHOL.thy. Many of the
> ensuing failures I was able to handle, but I don't know what to make
> of this one from Product_type.thy:
>
> ```
>
> free_constructors case_prod for Pair fst snd
> proof -
> fix P :: bool and p :: "'a × 'b"
> show "(?x1 x2. p = Pair x1 x2 ? P) ? P"
> by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
> next
> fix a c :: 'a and b d :: 'b
> have "Pair_Rep a b = Pair_Rep c d ? a = c ? b = d"
> by (auto simp add: Pair_Rep_def fun_eq_iff)
> moreover have "Pair_Rep a b ? prod" and "Pair_Rep c d ? prod"
> by (auto simp add: prod_def)
> ultimately show "Pair a b = Pair c d ? a = c ? b = d"
> by (simp add: Pair_def Abs_prod_inject)
> qed
>
> ```
>
> jEdit underlines "qed" in red, claiming that:
> ```
>
> Tactic failed
> The error(s) above occurred for the goal statement:
> P (local.prod.case_prod f prod) = (?x1 x2. prod = Pair x1 x2 ? P
> (f x1 x2))
>
> ```
The position of the error message is a bit misleading. It is not the qed
which fails. Instead, after finishing the proof, the free_constructors
command tries to prove something on its own -- and fails. Probably, its
internal tactics depend on the choice axiom.
BTW: Whoever wrote this proof: The first case would be better stated as
assume "?x1 x2. p = Pair x1 x2 ? P" then show "P"
because meta-implication in show-statements may lead to
counter-intuitive behaviour.
Best regards,
Lars
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140218/1f5c03d9/attachment-0002.html>
More information about the isabelle-dev
mailing list