[isabelle-dev] Stymied by cryptic failure in Product_type.thy

[Lars Noschinski]

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>